SAT Solvers
Contents
SAT Solvers¶
Many problems can be solved by SAT Solvers. As programmers, we need to make a verification algorithm. A function that returns true when it has found the correct answer. If we can represent this verification as a boolean expression, we can ask a SAT solver what input makes it true. This input will be the solution to our problem.
The N-Queens Problem¶
The N-Queens Problem is a famous chess puzzle. It is also a good candidate for a verification problem. We can describe the properties a board needs to have. We can then find a solution that meets our constraints.
Chess Boards¶
A chess board is an \(n\) by \(n\) square. A traditional chess board is an 8 by 8 square. We will start with a smaller 4 by 4 square board.
We will only look at one piece, the Queen. The Queen can move in many directions. the queen can move to any space on a diagonal from it. The diagonal spaces are highlighted in orange below.
| ♕ | |||
The Queen can also move in straight lines. The following shows the straight line movements the places Queen can make.
| ♕ | |||
If a Queen can move into a space, then it can remove the piece in that space from the board. A Queen may take any piece in any of the orange spaces on the following board.
| ♕ | |||
There are four spaces on this board the Queen cannot move into. A piece places in any of these spaces cannot be taken by the Queen. We are focused on pieces that can be taken in a single move. In a real game, multiple moves would be made. Our focus is on a single snapshot of the board.
We can put another queen in the upper right hand corner. These two queens cannot take each other. Almost every other position on the board can be taken.
| ♕ | |||
| ♕ | |||
We can fit a third queen in the last open position. It cannot take any of the other queens and they cannot take it.
| ♕ | |||
| ♕ | |||
| ♕ |
The following board has three queens that cannot take each other in a single move. There is not one safe space on the board, but none of the pieces can immediately take each other.
| ♕ | |||
| ♕ | |||
| ♕ |
The N-Queens Problem¶
The N-Queens Problem is “given an n by n board, can you place n queens such that no queen can take another queen in one move.”
For our board, this would be realized as placing 4 queens on our 4 by 4 board.
We can solve the this board using backtracking.
Note
Backtracking is when we make guesses at the answer. When we reach an impossible situation, we backtrack to a previous choice and change it.
We start with an empty board.
We need to fit 4 queens on this board. Since a queen can move up and down, we can only fit one per column. This means we must fit one queen in each column.
Let’s try putting a queen in the first square of the first column. Every square it can take is colored in orange.
| ♕ | |||
There are two possible locations in the second column. We put a queen into the first one.
| ♕ | |||
| ♕ | |||
At this point, there is only one space left. It is impossible to fit two more queens on this board. We much have made a mistake. We backtrack and change the location of the second queen.
| ♕ | |||
| ♕ |
This seems more promising, there are two spaces left! We put a queen in the empty space in the third column.
| ♕ | |||
| ♕ | |||
| ♕ |
Sadly, this eliminated the final position. We only fit three queens. We tried both options in column three. That means, we must have made out mistake in column one. We backtrack all the way to the beginning.
We place the first queen into the second position in the first column.
| ♕ | |||
We only have one choice for the second queen. We take to take it.
| ♕ | |||
| ♕ |
There is only one option for the third queen. We place that queen.
| ♕ | |||
| ♕ | |||
| ♕ |
There is still one space left. We can place the fourth queen.
| ♕ | |||
| ♕ | |||
| ♕ | |||
| ♕ |
We successfully placed four queens on a 4 by 4 chess board such that no queen can take another queen in a single move. The final answer without the orange highlights is given below.
| ♕ | |||
| ♕ | |||
| ♕ | |||
| ♕ |
This method works well, but would need to be implemented as an algorithm for large scales. We don’t need to implement it ourselves. We can translate it into a SAT solver problem.
You can watch the problem being solved using backtracking in the video below.
4 Queens in CNF¶
To solve this problem with a SAT Solver, we need to write the constrains of the chess board as a Boolean Expression. If the expression is true, we have an answer.
First, we assign a number to each space on the board.
| 1 | 2 | 3 | 4 |
| 5 | 6 | 7 | 8 |
| 9 | 10 | 11 | 12 |
| 13 | 14 | 15 | 16 |
If a position in the board is true that means it has a queen. If it is false that means it does not have a queen. We will refer to the number in the subscript for example \(X_{2}\) means position 2. There must be at least one queen in the first one.
\( \begin{align} X_{1} \vee X_{2} \vee X_{3} \vee X_{4} \end{align} \)
This gives us at least one queen, but we can’t have two queens. We can use a conditional to handle this. If \(X_{1}\) has a queen, then \(X_{2}\) must not have a queen.
\( \begin{align} X_{1} \implies \neg X_{2} \\ X_{1} \implies \neg X_{3} \\ X_{1} \implies \neg X_{4} \end{align} \)
Eventually, we will want these in CNF. We apply the definition of implies.
\( \begin{align} \neg X_{1} \vee \neg X_{2} \\ \neg X_{1} \vee \neg X_{3} \\ \neg X_{1} \vee \neg X_{4} \end{align} \)
Each of these is pairing two spaces on the board. For example, \(\neg X_{1} \vee \neg X_{2}\) says that either \(X_{1}\) is true or \(X_{2}\) is true, but not both. We do allow both to be false, they just both cannot be true.
To say that there must be exactly one queen in the first row, we just need to put all the pieces together. Notice that we don’t need \(\neg X_{2} \vee \neg X_{1}\) because we already have \(\neg X_{1} \vee \neg X_{2}\).
\( \begin{align} &\left( X_{1} \vee X_{2} \vee X_{3} \vee X_{4} \right) \\ &\wedge ( \neg X_{1} \vee \neg X_{2}) \\ &\wedge ( \neg X_{1} \vee \neg X_{3}) \\ &\wedge ( \neg X_{1} \vee \neg X_{4}) \\ &\wedge ( \neg X_{2} \vee \neg X_{3}) \\ &\wedge ( \neg X_{2} \vee \neg X_{4}) \\ &\wedge ( \neg X_{3} \vee \neg X_{4}) \\ \end{align} \)
We would need to repeat this for each column. The DiMACs for all the rows is given below. This requires 28 clauses and 16 variables.
1 2 3 4 0
-1 -2 0
-1 -3 0
-1 -4 0
-2 -3 0
-2 -4 0
-3 -4 0
5 6 7 8 0
-5 -6 0
-5 -7 0
-5 -8 0
-6 -7 0
-6 -8 0
-7 -8 0
9 10 11 12 0
-9 -10 0
-9 -11 0
-9 -12 0
-10 -11 0
-10 -12 0
-11 -12 0
13 14 15 16 0
-13 -14 0
-13 -15 0
-13 -16 0
-14 -15 0
-14 -16 0
-15 -16 0
We also need to handle rows. The same logic applies.
| 1 | 2 | 3 | 4 |
| 5 | 6 | 7 | 8 |
| 9 | 10 | 11 | 12 |
| 13 | 14 | 15 | 16 |
For the first column, we need one of the four positions to be true, but cannot have two be true.
\( \begin{align} &\left( X_{1} \vee X_{5} \vee X_{9} \vee X_{13} \right) \\ &\wedge ( \neg X_{1} \vee \neg X_{5}) \\ &\wedge ( \neg X_{1} \vee \neg X_{9}) \\ &\wedge ( \neg X_{1} \vee \neg X_{13}) \\ &\wedge ( \neg X_{5} \vee \neg X_{9}) \\ &\wedge ( \neg X_{5} \vee \neg X_{13}) \\ &\wedge ( \neg X_{9} \vee \neg X_{13}) \\ \end{align} \)
We need to do this for all four columns. This adds another 28 clauses to our DiMACs code.
1 5 9 13 0
-1 -5 0
-1 -9 0
-1 -13 0
-5 -9 0
-5 -13 0
-9 -13 0
2 6 10 14 0
-2 -6 0
-2 -10 0
-2 -14 0
-6 -10 0
-6 -14 0
-10 -14 0
3 7 11 15 0
-3 -7 0
-3 -11 0
-3 -15 0
-7 -11 0
-7 -15 0
-11 -15 0
4 8 12 16 0
-4 -8 0
-4 -12 0
-4 -16 0
-8 -12 0
-8 -16 0
-12 -16 0
Finally, we need to ensure that only one queen is on each diagonal. We don’t care if diagonals are empty. We just need the implies statements for the diagonals.
| 1 | 2 | 3 | 4 |
| 5 | 6 | 7 | 8 |
| 9 | 10 | 11 | 12 |
| 13 | 14 | 15 | 16 |
The diagonals starting from the top row and going right are:
\(X_{1}, X_{6}, X_{11}, X_{16}\)
\(X_{2}, X_{7}, X_{12}\)
\(X_{3}, X_{8}\)
The diagonals starting from the first column and going right are:
\(X_{5}, X_{10}, X_{15}\)
\(X_{9}, X_{14}\)
The diagonals starting from the first row and going left are:
\(X_{2}, X_{5}\)
\(X_{3}, X_{6}, X_{9}\)
\(X_{4}, X_{7}, X_{10}, X_{13}\)
Lastly, we have the diagonals from the last column going left:
\(X_{8}, X_{11}, X_{14}\)
\(X_{12}, X_{15}\)
For each diagonal, we need to make \(\neg X_{i} \vee \neg X_{j}\) for any pairing \(i < j\). The DiMACs for this adds another 28 clauses.
-1 -6 0
-1 -11 0
-1 -16 0
-6 -11 0
-6 -16 0
-11 -16 0
-2 -7 0
-2 -12 0
-7 -12 0
-3 -8 0
-5 -10 0
-5 -15 0
-10 -15 0
-9 -14 0
-2 -5 0
-3 -6 0
-3 -9 0
-6 -9 0
-4 -7 0
-4 -10 0
-4 -13 0
-7 -10 0
-7 -13 0
-10 -13 0
-8 -11 0
-8 -14 0
-11 -14 0
-12 -15 0
Putting it all together gives us a full DiMACs file.
p cnf 16 84
1 2 3 4 0
-1 -2 0
-1 -3 0
-1 -4 0
-2 -3 0
-2 -4 0
-3 -4 0
5 6 7 8 0
-5 -6 0
-5 -7 0
-5 -8 0
-6 -7 0
-6 -8 0
-7 -8 0
9 10 11 12 0
-9 -10 0
-9 -11 0
-9 -12 0
-10 -11 0
-10 -12 0
-11 -12 0
13 14 15 16 0
-13 -14 0
-13 -15 0
-13 -16 0
-14 -15 0
-14 -16 0
-15 -16 0
1 5 9 13 0
-1 -5 0
-1 -9 0
-1 -13 0
-5 -9 0
-5 -13 0
-9 -13 0
2 6 10 14 0
-2 -6 0
-2 -10 0
-2 -14 0
-6 -10 0
-6 -14 0
-10 -14 0
3 7 11 15 0
-3 -7 0
-3 -11 0
-3 -15 0
-7 -11 0
-7 -15 0
-11 -15 0
4 8 12 16 0
-4 -8 0
-4 -12 0
-4 -16 0
-8 -12 0
-8 -16 0
-12 -16 0
-1 -6 0
-1 -11 0
-1 -16 0
-6 -11 0
-6 -16 0
-11 -16 0
-2 -7 0
-2 -12 0
-7 -12 0
-3 -8 0
-5 -10 0
-5 -15 0
-10 -15 0
-9 -14 0
-2 -5 0
-3 -6 0
-3 -9 0
-6 -9 0
-4 -7 0
-4 -10 0
-4 -13 0
-7 -10 0
-7 -13 0
-10 -13 0
-8 -11 0
-8 -14 0
-11 -14 0
-12 -15 0
Running this in CryptoMiniSAT gives the following result.
v -1 2 -3 -4 -5 -6 -7 8 9 -10 -11 -12 -13 -14 15 -16 0
We need to put queens in positions 2, 8, 9, and 15. The board is shown below.
| ♕ | |||
| ♕ | |||
| ♕ | |||
| ♕ |
We got a valid answer! This is actually a mirror of the board we figured out on our own.
Automated DiMACs¶
Writing the DiMACs expressions by hand is not a very good strategy. We can write code to generate the DiMACs for us. As long as it is easier to write this code then solve the problem directly, it is to our advantage.
We want to solve this for a general n by n board, by we will still use the 4 by 4 as our sanity check.
| 1 | 2 | 3 | 4 |
| 5 | 6 | 7 | 8 |
| 9 | 10 | 11 | 12 |
| 13 | 14 | 15 | 16 |
We will call the first row the \(0\)-th row. The \(i\)-th row contains values from \(i*n+1\) to \((i+1) * n\).
Row 0 starts at \(0 * 4+1=1\) and ends at \(1 * 4=4\). It increments by 1 each time. Row 1 starts at \(1 * 4 + 1 =5\) and ends at \( 2*4 + 8\). We can write a function to generate these sequences.
We need to generate sequences of integers.
;Generate a Sequence of numbers
;List starts at start and ends at stop
;Each element x is followed by x+step
;input-contract: (and (int? start) (int? stop) (int? step))
;output-contract: (list? (sequence start stop step))
(define (sequence start stop step)
(if (< stop start)
null
(cons start (sequence (+ start step) stop step))
)
)
We can generate rows by computing the start and stop values.
;Generate the ith row of an n by n chess board
;input-contract: (and (int? i) (int? n))
;output-contract: (list? (getRow i n))
(define (getRow i n)
(sequence (+ (* i n) 1) (* (+ i 1) n) 1)
)
(getRow 0 4) ;'(1 2 3 4)
(getRow 1 4) ;'(1 2 3 4)
(getRow 2 4) ;'(1 2 3 4)
(getRow 3 4) ;'(1 2 3 4)
For columns, we need to go at a different pace. For example, the 0-th column contains 1, 5, 9, and 13. We started at 1 then went at a rate of \(4\). The sequence for column \(i\) starts at \(i+1\). Then the second item is \(i+1+n\). The third element is \(i+1+2n\). The last position is \(i+1+(n-1)n\).
;Generate the ith column of an n by n chess board
;input-contract: (and (int? i) (int? n))
;output-contract: (list? (getCol i n))
(define (getCol i n)
(sequence (+ i 1) (+ i 1 (* (- n 1) n)) n)
)
(getCol 0 4) ;'(1 5 9 13)
(getCol 1 4) ;'(2 6 10 14)
(getCol 2 4) ;'(3 7 11 15)
(getCol 3 4) ;'(4 8 12 16)
For the diagonals going right, we need to go at a speed of \(n+1\). This will make the square 1 off each time. Our first guess might be to just stop at \(n*n\) since we know it is the largest value on the board.
(define (getRightDiag start n)
(if (> start (* n n))
null
(cons start (getRightDiag (+ start (+ n 1)) n))
)
)
Sadly, this approach doesn’t work. If we execute (getRightDiag 4 4) we get '(4 9 14). The diagonal roles over to the column with 9 and 14. We need to figure out how to stop at the right position. We know we need to start at a specific index start. We also know the rate we need to go at (+ n 1). We just need to predict the end of the diagonal.
If we tell it how long the diagonal is. Then we can predict the final value. If we want len values, the last one will be at \(\text{start}+(\text{len}-1) * \text{step}\).
This code and generate the right diagonals.
;Generate Columns Going Right
;Input start is the starting space
;input-contract: (and (int? start) (int? n) (int? len))
;output-contract: (list? (getRightDiag start n len))
(define (getRightDiag start n len)
(sequence start
;Last value we want is start+(len-1)*step
(+ start (* (- len 1) (+ n 1)))
;Step
(+ n 1))
)
(getRightDiag 1 4 4);'(1 6 11 16)
(getRightDiag 2 4 3);'(2 7 12)
(getRightDiag 3 4 2);'(3 8)
(getRightDiag 4 4 1);'(4)
(getRightDiag 5 4 3);'(5 10 15)
(getRightDiag 9 4 2);'(9 14)
(getRightDiag 13 4 1);'(13)
The left diagonals have the same structure, but go at speed \(n-1\) instead of \(n+1\).
;Generate Columns Going Left
;Input start is the starting space
;input-contract: (and (int? start) (int? n) (int? len))
;output-contract: (list? (getLeftDiag start n len))
(define (getLeftDiag start n len)
(sequence start
;Last value we want is start+(len-1)*step
(+ start (* (- len 1) (- n 1)))
;Step
(+ n -1))
)
(getLeftDiag 1 4 1) ;'(1)
(getLeftDiag 2 4 2) ;'(2 5)
(getLeftDiag 3 4 3) ;'(3 6 9)
(getLeftDiag 4 4 4) ;'(4 7 10 13)
(getLeftDiag 8 4 3) ;'(8 11 14)
(getLeftDiag 12 4 2);'(12 15)
(getLeftDiag 16 4 1);'(16)
At this point, we can generate lists with any row, column or diagonal. Now, we need to make expressions for DiMACs. We will make a list of strings, one for each row of the DiMACs file.
We need to make the at least one clause. For example, for row 1 we had \(X_{1} \vee X_{2} \vee X_{3} \vee X_{4}\).
We can make these DiMACs expressions with a function.
;At least one value in the list must be true
;OR all elements in the list
;input-contract: (list? L)
;output-contract: (string? (atLeastOne L))
(define (atLeastOne L)
(if (null? L)
"0\n"
(string-append (format "~v " (first L)) (atLeastOne (rest L)))
)
)
(atLeastOne (getRow 0 4));"1 2 3 4 0\n"
(atLeastOne (getRow 1 4));"5 6 7 8 0\n"
(atLeastOne (getRow 2 4));"9 10 11 12 0\n"
(atLeastOne (getRow 3 4));"13 14 15 16 0\n"
(atLeastOne (getCol 0 4));"1 5 9 13 0\n"
(atLeastOne (getCol 1 4));"2 6 10 14 0\n"
(atLeastOne (getCol 2 4));"3 7 11 15 0\n"
(atLeastOne (getCol 3 4));"4 8 12 16 0\n"
We also need to be able to say “at most one”. This is a little harder. Take the list '(1 2 3 4). We need to make three clauses with \(1\) then two clause with \(2\).
We make a helper function to make “at most one” easier. It takes a value a and a list L. It creates clauses \(\forall x \in L \left(\neg a \vee \neg x\right)\).
;Helper for At Most 1
;Does a -> every element in L
;input-contract: (and (int? a) (list? L))
;output-contract: (list? L)
(define (atMostHelper a L)
(if (null? L)
null
(cons (format "-~v -~v 0\n" a (first L))
(atMostHelper a (rest L)))
)
)
(atMostHelper 1 '(2 3 4))
;'("-1 -2 0\n" "-1 -3 0\n" "-1 -4 0\n")
Then we just need to run this for all the different values in the list to make all the clauses.
;At Most One
;At most one value in the list is true
;Returns a list of strings
;input-contact: (list? L)
;output-contract: (list? L)
(define (atMostOne L)
(if (< (length L) 2)
null ;nothing to compare
(append (atMostHelper (first L) (rest L))
(atMostOne (rest L)))
)
)
(atMostOne '(1 2 3 4))
;'("-1 -2 0\n" "-1 -3 0\n" "-1 -4 0\n" "-2 -3 0\n" "-2 -4 0\n" "-3 -4 0\n")
Once we have all these tools, we just need to generate the right DiMACs statements.
For every row, we need both “at most one” and “at least one” queen. Putting these together gives us “exactly one”.
;Requirements for a row
;input-contract: (and (int? c) (int? n))
;output-contract: (list? (rowRequirements c n))
(define (rowRequirement r n)
(let ((myRow (getRow r n)))
;At least one Element in this row is needed
(cons (atLeastOne myRow)
;At Most one Element in this row in needed
(atMostOne myRow))
)
)
(rowRequirement 0 4)
;("1 2 3 4 0\n" "-1 -2 0\n" "-1 -3 0\n" "-1 -4 0\n" "-2 -3 0\n" "-2 -4 0\n" "-3 -4 0\n")
We also need exactly one queen per column.
;Requirements for a column
;input-contract: (and (int? c) (int? n))
;output-contract: (list? (colRequirements c n))
(define (colRequirements c n)
(let ((myCol (getCol c n)))
(cons (atLeastOne myCol)
(atMostOne myCol)
))
)
To create the rules for all the rows, we just map over the possible rows and fold together the results.
;All the Requirements Related to Rows
;input-contract: (int? n)
;output-contract: (list? (allRows n))
(define (allRows n)
(foldr append null
(map (lambda (x) (rowRequirement x n))
(sequence 0 (- n 1) 1)
)
)
)
We need to do the same thing for the columns.
;All the Requirements Related to Columns
;input-contract: (int? n)
;output-contract: (list? (allCols n))
(define (allCols n)
(foldr append null
(map (lambda (x) (colRequirements x n))
(sequence 0 (- n 1) 1)
)
)
)
The diagonals only need “at most one”. We don’t care if some diagonals are left incomplete.
First, we do the diagonals going from the top row to the right.
;Handle Diagonals from top row going right
;input-contract: (int? n)
;output-contract: (list? (topRDiagonals n))
(define (topRDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getRightDiag x n (- n (- x 1))))
(sequence 1 (- n 1) 1))
))
)
We also need the top row going left instead.
;Handle Diagonals from top row going left
;input-contract: (int? n)
;output-contract: (list? (topLDiagonals n))
(define (topLDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getLeftDiag x n x))
(sequence 2 n 1)
)
)
)
)
We are still missing a few diagonals. We need to go right from the far left column.
;Handle Diagonals from Left Side
;input-contract: (int? n)
;output-contract: (list? (leftDiagonals n))
(define (leftDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getRightDiag x n (- n (quotient x n))))
(sequence (+ n 1) (+ (* (- n 2) n) 1) n)
)
)
)
)
We also need to go from the far right column towards the left side.
;Handle Diagonals from right side
;input-contract: (int? n)
;output-contract: (list? (rightDiagonals n))
(define (rightDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getLeftDiag x n (- n (- (quotient x n) 1))))
(sequence (* 2 n) (* (- n 1) n) n)
)
)
)
)
To make the entire board’s requirements, we just put all the pieces together and append them all.
;Make Requirements
;Put all the pieces together
;input-contract: (int? n)
;output-contract: (string? (makeRequirements n))
(define (makeRequirements n)
(append
(allRows n)
(allCols n)
(topRDiagonals n)
(leftDiagonals n)
(topLDiagonals n)
(rightDiagonals n)
)
)
We need to put all this into a file. THe next function adds the problem statement with the count of variables and clauses. It also uses foldr to make all the statements into one big string.
;Make a DiMACs file.
;Just uses all the above and merges together
;adds the problem statement header
;input-contract: (int? n)
;output-contract: (string? (makeDiMACs n))
(define (makeDiMACs n)
(let ((req (makeRequirements n)))
(foldr string-append ""
(cons (format "p cnf ~v ~v\n" (* n n) (length req))
req)
)
)
)
Then all we need to do is save the text into a file.
;Save the Result to a File
;input-contract: (and (int? n) (string? fname))
;output-contract: no result, writes file as side effect
(define (nqueens n fname)
(with-output-to-file
fname ;File to save into
;Text to Write to File
(lambda () (printf (makeDiMACs n)))
;Overwrite File if it exists
#:exists 'replace
)
)
We can now generate DiMACs code for as many N-Queens problems as we want.
N-Queens Solutions¶
We can use our functions to make solutions for other boards.
;Generate Some Files
(nqueens 4 "queens_4.txt")
(nqueens 5 "queens_5.txt")
(nqueens 8 "queens_8.txt")
(nqueens 20 "queens_20.txt")
The 4 by 4 board exactly matches our hand-written DiMACs.
| ♕ | |||
| ♕ | |||
| ♕ | |||
| ♕ |
The 5 by 5 board has 25 variables and 170 clauses. The answer we get from the SAT Solver is shown below.
v -1 -2 -3 -4 5 -6 7 -8 -9 -10 -11 -12 -13 14 -15 16 -17 -18 -19 -20 -21 -22 23
v -24 -25 0
| ♕ | ||||
| ♕ | ||||
| ♕ | ||||
| ♕ | ||||
| ♕ |
For the 8 by 8 board, we need 64 variables and 744 clauses. We get an answer almost instantly.
v -1 -2 -3 4 -5 -6 -7 -8 -9 10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22
v -23 24 -25 -26 -27 -28 -29 30 -31 -32 33 -34 -35 -36 -37 -38 -39 -40 -41 -42
v 43 -44 -45 -46 -47 -48 -49 -50 -51 -52 53 -54 -55 -56 -57 -58 -59 -60 -61 -62
v 63 -64 0
| ♕ | |||||||
| ♕ | |||||||
| ♕ | |||||||
| ♕ | |||||||
| ♕ | |||||||
| ♕ | |||||||
| ♕ | |||||||
| ♕ |
We can even do a 20 by 20 board with 400 variables and 12,580 clauses almost instantly. At this point, it becomes difficult to draw or manually verify the answer. We would need to write another script just to deal with this result.
v -1 -2 -3 -4 -5 -6 -7 8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22
v -23 -24 -25 -26 -27 -28 -29 30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41
v -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 55 -56 -57 -58 -59 -60
v -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 73 -74 -75 -76 -77 -78 -79
v -80 -81 -82 -83 -84 -85 86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98
v -99 -100 -101 -102 -103 -104 -105 -106 -107 -108 -109 -110 -111 -112 -113 -114
v -115 116 -117 -118 -119 -120 121 -122 -123 -124 -125 -126 -127 -128 -129 -130
v -131 -132 -133 -134 -135 -136 -137 -138 -139 -140 -141 -142 -143 -144 -145
v -146 -147 -148 -149 -150 151 -152 -153 -154 -155 -156 -157 -158 -159 -160
v -161 -162 -163 -164 -165 -166 167 -168 -169 -170 -171 -172 -173 -174 -175
v -176 -177 -178 -179 -180 -181 -182 -183 -184 185 -186 -187 -188 -189 -190
v -191 -192 -193 -194 -195 -196 -197 -198 -199 -200 -201 -202 203 -204 -205
v -206 -207 -208 -209 -210 -211 -212 -213 -214 -215 -216 -217 -218 -219 -220
v -221 -222 -223 -224 -225 -226 -227 -228 -229 -230 -231 -232 -233 234 -235
v -236 -237 -238 -239 -240 -241 -242 -243 -244 -245 -246 -247 -248 -249 -250
v -251 -252 -253 -254 -255 -256 257 -258 -259 -260 -261 -262 -263 -264 -265
v -266 -267 -268 -269 -270 -271 -272 -273 -274 -275 -276 -277 -278 279 -280
v -281 -282 -283 -284 -285 -286 -287 -288 -289 -290 -291 292 -293 -294 -295
v -296 -297 -298 -299 -300 -301 -302 -303 -304 -305 -306 -307 -308 309 -310
v -311 -312 -313 -314 -315 -316 -317 -318 -319 -320 -321 -322 -323 324 -325
v -326 -327 -328 -329 -330 -331 -332 -333 -334 -335 -336 -337 -338 -339 -340
v -341 342 -343 -344 -345 -346 -347 -348 -349 -350 -351 -352 -353 -354 -355
v -356 -357 -358 -359 -360 -361 -362 -363 -364 -365 -366 -367 -368 -369 -370
v -371 -372 -373 -374 -375 -376 -377 378 -379 -380 -381 -382 -383 -384 -385
v -386 -387 -388 -389 -390 -391 -392 -393 -394 -395 -396 -397 -398 -399 400 0
Conclusion¶
The important thing to remember about this example is, we never developed or implemented an algorithm to solve the N queens problems. Our program only generated the DiMACs file. The SAT solver did all the hard work for us.
For many problems, it is easier for a programmer to generate the logic expressions then to solve the problem themselves. If a SAT Solver is efficient enough, we can allow it to do all the work for us.
Full Source Code¶
#lang racket
;Mark Boady - Drexel University 2021
;This program generates DiMACs files
;to solve the n-queens chess problem.
;---------------------------------------------
;Section 1: Generate Lists of Numbers
;---------------------------------------------
;Generate a Sequence of numbers
;List starts at start and ends at stop
;Each element x is followed by x+step
;input-contract: (and (int? start) (int? stop) (int? step))
;output-contract: (list? (sequence start stop step))
(define (sequence start stop step)
(if (< stop start)
null
(cons start (sequence (+ start step) stop step))
)
)
;Generate the ith row of an n by n chess board
;input-contract: (and (int? i) (int? n))
;output-contract: (list? (getRow i n))
(define (getRow i n)
(sequence (+ (* i n) 1) (* (+ i 1) n) 1)
)
;Generate the ith column of an n by n chess board
;input-contract: (and (int? i) (int? n))
;output-contract: (list? (getCol i n))
(define (getCol i n)
(sequence (+ i 1) (+ i 1 (* (- n 1) n)) n)
)
;Generate Columns Going Right
;Input start is the starting space
;input-contract: (and (int? start) (int? n) (int? len))
;output-contract: (list? (getRightDiag start n len))
(define (getRightDiag start n len)
(sequence start
;Last value we want is start+(len-1)*step
(+ start (* (- len 1) (+ n 1)))
;Step
(+ n 1))
)
;Generate Columns Going Left
;Input start is the starting space
;input-contract: (and (int? start) (int? n) (int? len))
;output-contract: (list? (getLeftDiag start n len))
(define (getLeftDiag start n len)
(sequence start
;Last value we want is start+(len-1)*step
(+ start (* (- len 1) (- n 1)))
;Step
(+ n -1))
)
;---------------------------------------------
;Section 2: Boolean Expressions
;---------------------------------------------
;At least one value in the list must be true
;OR all elements in the list
;input-contract: (list? L)
;output-contract: (string? (atLeastOne L))
(define (atLeastOne L)
(if (null? L)
"0\n"
(string-append (format "~v " (first L)) (atLeastOne (rest L)))
)
)
;At Most One
;At most one value in the list is true
;Returns a list of strings
;input-contact: (list? L)
;output-contract: (list? L)
(define (atMostOne L)
(if (< (length L) 2)
null ;nothing to compare
(append (atMostHelper (first L) (rest L))
(atMostOne (rest L)))
)
)
;Helper for At Most 1
;Does a -> every element in L
;input-contract: (and (int? a) (list? L))
;output-contract: (list? L)
(define (atMostHelper a L)
(if (null? L)
null
(cons (format "-~v -~v 0\n" a (first L))
(atMostHelper a (rest L)))
)
)
;---------------------------------------------
;Section 3: Requirements for Board
;---------------------------------------------
;Requirements for a row
;input-contract: (and (int? c) (int? n))
;output-contract: (list? (rowRequirements c n))
(define (rowRequirement r n)
(let ((myRow (getRow r n)))
;At least one Element in this row is needed
(cons (atLeastOne myRow)
;At Most one Element in this row in needed
(atMostOne myRow))
)
)
;Requirements for a column
;input-contract: (and (int? c) (int? n))
;output-contract: (list? (colRequirements c n))
(define (colRequirements c n)
(let ((myCol (getCol c n)))
(cons (atLeastOne myCol)
(atMostOne myCol)
))
)
;All the Requirements Related to Rows
;input-contract: (int? n)
;output-contract: (list? (allRows n))
(define (allRows n)
(foldr append null
(map (lambda (x) (rowRequirement x n))
(sequence 0 (- n 1) 1)
)
)
)
;All the Requirements Related to Columns
;input-contract: (int? n)
;output-contract: (list? (allCols n))
(define (allCols n)
(foldr append null
(map (lambda (x) (colRequirements x n))
(sequence 0 (- n 1) 1)
)
)
)
;Handle Diagonals from top row going right
;input-contract: (int? n)
;output-contract: (list? (topRDiagonals n))
(define (topRDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getRightDiag x n (- n (- x 1))))
(sequence 1 (- n 1) 1))
))
)
;Handle Diagonals from top row going left
;input-contract: (int? n)
;output-contract: (list? (topLDiagonals n))
(define (topLDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getLeftDiag x n x))
(sequence 2 n 1)
)
)
)
)
;Handle Diagonals from Left Side
;input-contract: (int? n)
;output-contract: (list? (leftDiagonals n))
(define (leftDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getRightDiag x n (- n (quotient x n))))
(sequence (+ n 1) (+ (* (- n 2) n) 1) n)
)
)
)
)
;Handle Diagonals from right side
;input-contract: (int? n)
;output-contract: (list? (rightDiagonals n))
(define (rightDiagonals n)
(foldr append null
(map atMostOne
(map (lambda (x) (getLeftDiag x n (- n (- (quotient x n) 1))))
(sequence (* 2 n) (* (- n 1) n) n)
)
)
)
)
;---------------------------------------------
;Section 4: Generate Entire Board
;---------------------------------------------
;Make Requirements
;Put all the pieces together
;input-contract: (int? n)
;output-contract: (string? (makeRequirements n))
(define (makeRequirements n)
(append
(allRows n)
(allCols n)
(topRDiagonals n)
(leftDiagonals n)
(topLDiagonals n)
(rightDiagonals n)
)
)
;---------------------------------------------
;Section 5: Output File to DiMACs
;---------------------------------------------
;Make a DiMACs file.
;Just uses all the above and merges together
;adds the problem statement header
;input-contract: (int? n)
;output-contract: (string? (makeDiMACs n))
(define (makeDiMACs n)
(let ((req (makeRequirements n)))
(foldr string-append ""
(cons (format "p cnf ~v ~v\n" (* n n) (length req))
req)
)
)
)
;Save the Result to a File
;input-contract: (and (int? n) (string? fname))
;output-contract: no result, writes file as side effect
(define (nqueens n fname)
(with-output-to-file
fname ;File to save into
;Text to Write to File
(lambda () (printf (makeDiMACs n)))
;Overwrite File if it exists
#:exists 'replace
)
)
;Generate Some Files
(nqueens 4 "queens_4.txt")
(nqueens 5 "queens_5.txt")
(nqueens 8 "queens_8.txt")
(nqueens 20 "queens_20.txt")