Last page LERIA Faculty of Sciences University of Angers
Version française


A Chessboard Coloring Problem for SAT Solvers ( download instances)


The original chessboard coloring problem was proposed as the first problem of the Fifth Annual U.S.A Mathematical Olympiad, in 1976. First, one should prove that there is no way to color either black or white each square of a $ 4\times 7$ chessboard, such that the four distinct corners of all rectangles included in the chessboard are not all of the same color, as the thin one in figure 1. A rectangle with 4 corners of the same color is then called a chromatic rectangle (CR) (plain line in figure 1). Therefore, chessboards containing at least one CR will be called CR chessboard and those containing no CR will be NCR boards. The second part of the problem was to exhibit a black-white coloring of a $ 4 \times 6$ chessboard, with the above property (see figure 1).

Figure 1: A $ 4\times 7$ CR board (left) and a $ 4\times 6$ NCR board (right)
\includegraphics[width=3cm,height=3cm]{4-7CB.eps} \includegraphics[width=3cm,height=3cm]{4-6CB.eps}

Beresin, Levine, and Winn [1] give the proof for the first part, and a solution for the second part. Further, they generalize their results to any $ m \times n$ chessboard painted with $ t$ colors. They establish conditions under which the chessboard must have at least a CR. Applying their principle and the above properties to the two and the three colors cases, they find necessary and sufficient conditions on $ n$ and $ m$ to decide if a $ m \times n$ board is a CR-board or a NCR-board. To summarize, the problem of deciding if a $ m \times n$ board is CR or NCR board is solved for two and three colors.

Encoding this problem in a SAT problem


An instance of the SAT problem is defined by a set of boolean variables (also called atoms) $ {\cal X}$ and a boolean formula $ \phi \colon \{0,1\}^n \to \{0,1\}$. A literal is a variable or its negation. A clause is a disjunction of literals. The formula $ \phi$ is in conjunctive normal form (CNF) if it is a conjunction of clauses. A (truth) assignment is a function $ v \colon {\cal X} \to \{0,1\}$. The formula is said to be satisfiable if there exists an assignment satisfying $ \phi$ and unsatisfiable otherwise. In this problem, $ \phi$ will be in CNF.

Given a chessboard of size $ n \times n$, the set of its squares $ {\cal B} = [1..n] \times [1..n]$ is of size $ n^2$, therefore elements of $ {\cal B}$ can be mapped to a set of variables $ \{X_1,..X_{n^2}\}$ by an isomorphism:

$\displaystyle flat \colon {\cal B} \to \{X_1,..X_{n^2}\} $

$\displaystyle \forall X=(x,y) \in {\cal B}, flat(X)=X_{x + n\times y} $

This function provides a flatten representation of the board.

A rectangle in the chessboard can be associated to any pair of points $ A=(a_1,a_2)$ and $ B=(b_1,b_2)$ such that $ \forall i, a_i \neq b_i$. The corresponding rectangle is then fully defined by its 4 corners:

\begin{displaymath} \begin{array}{ l} R(A,B) = (X_{a_1+n\times a_2},X_{b_1+n\times a_2},X_{a_1+n\times b_2},X_{b_1+n\times b_2})\\ \end{array} \end{displaymath}

Note that each rectangle can be referred to by two complementary pairs of points (i.e. $ R((x_1,y_1),(x_2,y_2))=R((x_1,y_2),(x_2,y_1))$). We consider $ {\cal R}$ the set of all distinct rectangles for a given chessboard.

From now on, instances of the problem can be fully defined by their two main parameters: number of allowed colors $ N_{col}$ and size of the board $ n$.

Given $ n$ and $ N_{col}$, we first introduce a set of propositional variables $ \{ X_{ij} \mid i \in [1..n^2],j \in [1..N_{col}]\}$ ($ X_{ij}$ is true when the $ i^{th}$ variable of the initial problem is of color $ j$). We have to state that each square has one and only one color:

$\displaystyle \forall i \in [1..n^2] ( \bigvee_{j\in [1..N_{col}]} X_{ij} \wedg... ...! \bigwedge_{j,k\in [1..N_{col}],j \neq k} \!\!(\neg X_{ij} \vee \neg X_{ik})) $

Then, we state that there are no chromatic rectangle, by using our previous characterization of the rectangles :

$\displaystyle \forall i_1,i_2,i_3,i_4, (X_{i_1},X_{i_2},X_{i_3},X_{i_4}) \in {\... ...col}]} (\neg X_{i_1k} \vee \neg X_{i_2k}\vee \neg X_{i_3k} \vee \neg X_{i_4k}) $

This states that for a given color $ k$ the four propositional variables $ X_{i_1k},X_{i_2k},X_{i_3k}$ and $ X_{i_4k}$ forming a rectangle are not simultaneously true.

Therefore, our SAT problem consists of the conjunction of these statements.

Bibliography

1
May Beresin, Eugene Levine, and John Winn.
A chessboard coloring problem.
The College Mathematics Journal, 20(2):106-114, 1989.



Download: