Chess Queens social distancing problem using an SMT (integer) and boolean solvers

Placing chess queens on a grid such that social distancing is maintained is a classic problem. We look here at a method for solving this popular problem using an SMT solver and compare integer and boolean solving logic modes. The queen placement problem is redescribed as lines of logic and passed to general purpose solvers. The solver results are then reformatted back to display the answer provided.

Chess Queens social distancing problem

A chess queen can move up, down, diagonally left and diagonally right any number of moves across the board. The classic queen placement problem is to put eight queens on an eight by eight square board in such a way that none of the queens can move directly onto another queens square. This puzzle can be tried at home using a chequered pattern board of any size and counters for queens.

Fig 1:Boards show the queens moves in red with correct and incorrect second queen placement

This puzzle is scalable, the board can be any size from five by five upwards but in every case the number of placed queens should be the same as the number of squares along an edge. Eight queens can be placed on a standard eight by eight chess board but much larger boards can be used. Any solution method provided should be applicable to any allowable board size without excessive delays on larger boards. For the rest of the article we will refer to boardEdgeSize being the numbers of squares along the edge of a board and use an eight by eight board for the worked examples with a larger sixteen by sixteen for the results.

Addressing the board squares

The first task is to define how each of the squares are numbered and how the positions of queens can be described. We can use either a row and column approach or number the squares sequentially. The width the board is known therefore it is quite simple to switch between row and column addresses to sequential number addresses and back again. To get the sequential square number multiply the rows by boardEdgeSize and add the column number. In the example below (Fig 2) the queen is located on [ row 3, col 4] which becomes 3 * 8 + 4 = sequential square number 28.  Going the other way has the row number divided by boardEdgeSize  28 / 8 = 3 with remainder 4 becoming the column number. Starting the row and column and sequential number addresses at 0 makes the sums easier and works more naturally in a programming context.

Fig 2: The queen is on square [3, 4] or 3*8+4 = 28.

Logical description

The logical description of the queen placement problem is to have one and only one queen on each row and each column. There must not be more than one queen on any diagonal line but as there are more than 8 diagonal lines not every diagonal will have a queen.

Board showing 13 diagonals but there are the same number again slanted the other way.

Firstly using integers where we consider a "queen in a square" as value 1 and an empty square as value 0 the final board will have the following conditions:

• The sum of each row and each column must equal one,
• The sum of each of the diagonals must equal one or zero.
• The total number of queens must equal boardEdgeSize 

Alternatively using a logical expressions true/false value for a "queen in a square" the rules are

• Each row must have only one square set true
• Each column must have only one square set true
• Each diagonal must have only one or no squares set true

Finding the rows and columns

A good way of working with a grid is to pre-calculate the squares that belong to each row, column and diagonals then use the lists of square addresses to build the logic lines. 

Using sequential numbering of squares, calculate the square numbers along any row X by starting at X * boardEdgeSize then adding 1 for boardEdgeSize times. For the columns start at X then add boardEdgeSize for boardEdgeSize times.

For boardEdgeSize of eight the following are the lists of squares in each row and column. 

#Rows

Rx 0=[0 1 2 3 4 5 6 7 ]

Rx 1=[8 9 10 11 12 13 14 15 ]

Rx 2=[16 17 18 19 20 21 22 23 ]

Rx 3=[24 25 26 27 28 29 30 31 ]

Rx 4=[32 33 34 35 36 37 38 39 ]

Rx 5=[40 41 42 43 44 45 46 47 ]

Rx 6=[48 49 50 51 52 53 54 55 ]

Rx 7=[56 57 58 59 60 61 62 63 ]

#Cols

Cy 0=[0 8 16 24 32 40 48 56 ]

Cy 1=[1 9 17 25 33 41 49 57 ]

Cy 2=[2 10 18 26 34 42 50 58 ]

Cy 3=[3 11 19 27 35 43 51 59 ]

Cy 4=[4 12 20 28 36 44 52 60 ]

Cy 5=[5 13 21 29 37 45 53 61 ]

Cy 6=[6 14 22 30 38 46 54 62 ]

Cy 7=[7 15 23 31 39 47 55 63 ]

Finding the diagonal squares

Regardless of how the squares are addressed using [row, col] or square-number, traversing diagonally in all directions is fiddly and error prone. Using [row, col] we would have to repeatedly add each of  [-1,1]  [1,1] [1,-1] and [ -1,-1] until either the row or column is out of range 0..boardEdgeSize. Using square numbers when traversing we would have to adjust by repeatedly adding [ - boardEdgeSize +1] [ - boardEdgeSize -1]  [ + boardEdgeSize -1] and  [ + boardEdgeSize + 1] until the address falls out side the range 0 .. (boardEdgeSize * boardEdgeSize). 

To find the squares on each of the diagonal lines a simple geometric trick can be employed. First rotate the board by 45 degrees (1/8 of a turn) around the 0,0 point then calculate the new position of the squares, using the [Row, Column] address method. With the board rotated by 45 degrees the diagonals lines become vertical and horizontal lines. All the points on the same diagonals will now show up on the same row or column. We see that squares on the same diagonal will have the same new row or column address.

The calculation to achieve this rotation is quite simple. In general terms the new coordinates (x′, y′) of the point (x, y) after rotation of 45 degrees are found using the formulas :

x′= x cos⁡(45) − y sin⁡(45) 

y′= x sin⁡(45) +  y cos⁡(45)

In our case this is quite simple because cos(45) and sin(45) are the same value 0.7071068. (Explanation of sin and cos here) 

The calculation to find the new position of any square [ x, y ] is 

x′ = x * 0.7071068  − y * 0.7071068

y′ = x * 0.7071068 +  y * 0.7071068

Lets try this out with the queens position on [ 4,3 ] and squares 63 aka [7,7] and square 49 aka [1,6] see fig 4. The squares 55 and 49 are aligned with the placed queen. Square 63 is not aligned with the placed queen (see fig 4) 

Fig 4 :Square 28 Shares diagonals with square 49 & 55 but not square 63

Calculating the new row and column values for the squares 28, 49 and 55 along with 63 (see table 1) we see that the new column value for square 49 is the same as for the placed queen on square 28 indicating that they are in vertical alignment. The same applies for square 55 the new row address is the same as for the queen on square 28 indicating horizontal alignment. Square 63 does not share either new column or row indicating the placed queen is not on the same diagonal as square 63. 

Table 1 The rotated positions of some squares

Calculating the rotated positions for all the squares is followed by sorting them into groups that share a new row or new column value. To avoid comparing real number for equality, which is prone to rounding errors, 7071068 is used instead of 0.7071068 for the multiplier constant.

#Squares 

    [ R C Nr Nc ]

s 0=[ 0 0 0 0 ]

s 1=[ 0 1 -70710678 70710678 ]

s 2=[ 0 2 -141421356 141421356 ]

s 3=[ 0 3 -212132034 212132034 ]

s 4=[ 0 4 -282842712 282842712 ]

s 5=[ 0 5 -353553390 353553390 ]

s 6=[ 0 6 -424264068 424264068 ]

s 7=[ 0 7 -494974746 494974746 ]

s 8=[ 1 0 70710678 70710678 ]

s 9=[ 1 1 0 141421356 ]

s 10=[ 1 2 -70710678 212132034 ]

…

s 16=[ 2 0 141421356 141421356 ]

.... and on to square 63. Immediately we see that squares pair 1 and 8, pair 3 and 10, line 2 and 9 and 16 each share diagonal alignment.

After grouping the new square addresses, by comparing the new row and new column positions, the diagonally aligned squares become clear.

#Diagx dx :

Dx -494974746=[7 ]

Dx -424264068=[6 15 ]

Dx -353553390=[5 14 23 ]

Dx -282842712=[4 13 22 31 ]

Dx -212132034=[3 12 21 30 39 ]

Dx -141421356=[2 11 20 29 38 47 ]

Dx -70710678=[1 10 19 28 37 46 55 ]

Dx 0=[0 9 18 27 36 45 54 63 ]

Dx 70710678=[8 17 26 35 44 53 62 ]

Dx 141421356=[16 25 34 43 52 61 ]

Dx 212132034=[24 33 42 51 60 ]

Dx 282842712=[32 41 50 59 ]

Dx 353553390=[40 49 58 ]

Dx 424264068=[48 57 ]

Dx 494974746=[56 ]

#Diag dy :

Dy 0=[0 ]

Dy 70710678=[1 8 ]

Dy 141421356=[2 9 16 ]

Dy 212132034=[3 10 17 24 ]

Dy 282842712=[4 11 18 25 32 ]

Dy 353553390=[5 12 19 26 33 40 ]

Dy 424264068=[6 13 20 27 34 41 48 ]

Dy 494974746=[7 14 21 28 35 42 49 56 ]

Dy 565685424=[15 22 29 36 43 50 57 ]

Dy 636396102=[23 30 37 44 51 58 ]

Dy 707106780=[31 38 45 52 59 ]

Dy 777817458=[39 46 53 60 ]

Dy 848528136=[47 54 61 ]

Dy 919238814=[55 62 ]

Dy 989949492=[63 ]

Now the lists show the squares on each of the rows, column and both of the diagonals to make generating the logic of the puzzle much easier.

Generating the SMT logic of the puzzle - Integer version

After some pre-amble we set up 63 variable and lock them to the range 0 .. 1

(declare-const V0 Int)

(assert (or (= V0 0 ) (= V0 1)))

(declare-const V1 Int)

(assert (or (= V1 0 ) (= V1 1)))

(declare-const V2 Int)

(assert (or (= V2 0 ) (= V2 1)))

.....

up to V63. Using the lists pre-generated above for the rows and columns each row and column is set to add up to 1. .

;Rows nx :

(assert (= 1 (+ V0 V1 V2 V3 V4 V5 V6 V7 )))

(assert (= 1 (+ V8 V9 V10 V11 V12 V13 V14 V15 )))

.....

;Cols ny :

(assert (= 1 (+ V0 V8 V16 V24 V32 V40 V48 V56 )))

(assert (= 1 (+ V1 V9 V17 V25 V33 V41 V49 V57 )))

....

Diagonals and similarly created but with different logic as a diagonal can have one or none queens placed. 

(assert (or (= 1 (+ 0 V7  )) (= 0 (+ 0 V7 ))))

(assert (or (= 1 (+ 0 V5 V14 V23  )) (= 0 (+ 0 V5 V14 V23 ))))

(assert (or (= 1 (+ 0 V4 V13 V22 V31  )) (= 0 (+ 0 V4 V13 V22 V31 ))))

(assert (or (= 1 (+ 0 V3 V12 V21 V30 V39  )) (= 0 (+ 0 V3 V12 V21 V30 V39 ))))

.....

After the usual post-amble we have the instructions to pass to the SMT solver. 

Generating the SMT logic of the puzzle - Boolean version

First 63 boolean variables are created, one for each square

(declare-const V0 Bool)

(declare-const V1 Bool)

(declare-const V2 Bool)

.... up to V63

Each row and column are described by two lines. The first asserts that we must not have all false values in the row. ie: there must be at least one queen placed per row

(assert (not (and (not V0) (not V1) (not V2) (not V3) (not V4) (not V5) (not V6) (not V7) )))

The second asserts that one value must be true and all others in the same group are false. 

(assert (or 

(and V0 (not V1) (not V2) (not V3) (not V4) (not V5) (not V6) (not V7) ) 

(and V1 (not V0) (not V2) (not V3) (not V4) (not V5) (not V6) (not V7) ) 

(and V2 (not V0) (not V1) (not V3) (not V4) (not V5) (not V6) (not V7) ) 

(and V3 (not V0) (not V1) (not V2) (not V4) (not V5) (not V6) (not V7) ) 

(and V4 (not V0) (not V1) (not V2) (not V3) (not V5) (not V6) (not V7) ) 

(and V5 (not V0) (not V1) (not V2) (not V3) (not V4) (not V6) (not V7) ) 

(and V6 (not V0) (not V1) (not V2) (not V3) (not V4) (not V5) (not V7) ) 

(and V7 (not V0) (not V1) (not V2) (not V3) (not V4) (not V5) (not V6) ) 

)) ; from V0 V1 V2 V3 V4 V5 V6 V7 

The diagonal lines have a single assertion with two phrases to set all squares on a diagonal as false or a single value true.

(assert (or 

(and (not V6) (not V15) ) 

(and V6 (not V15) ) (and V15 (not V6) )

)) ; from V6 V15

(assert (or 

(and (not V2) (not V11) (not V20) (not V29) (not V38) (not V47) ) 

(and V2 (not V11) (not V20) (not V29) (not V38) (not V47) ) 

(and V11 (not V2) (not V20) (not V29) (not V38) (not V47) ) 

(and V20 (not V2) (not V11) (not V29) (not V38) (not V47) ) 

(and V29 (not V2) (not V11) (not V20) (not V38) (not V47) ) 

(and V38 (not V2) (not V11) (not V20) (not V29) (not V47) ) 

(and V47 (not V2) (not V11) (not V20) (not V29) (not V38) ) 

)) ; from V2 V11 V20 V29 V38 V47

As a side note xor was considered a logical function that could be able to check for one queen set in a row or column of squares. However whilst the xor function works when two square are involved, for longer groups of squares xor provides true when there are an odd number of queens (1,3,5,7..) along a row or column.   

Running the solvers

The generator and display script ./quSMT.pl is used to create both versions of the logic and read back the solver answers to display the final grid. Linux commands are piped together to generate the final output. The m5 solver can read from standard input but solver Z3 reads from a temporary file. The script parameters for the integer runs is -S , for boolean runs -s. The parameter -n is used to set the boardEdgeSize. The tee command passes along the standard input to standard output as well as saving a copy of solver results in a file. 

$ ./quSMT.pl -S -n 16 | time ../solver_m5 | tee qu_Bool_n16_M5.res | ./quSMT.pl -r -n 16  > qu_n6_M5.html

$ ./quSMT.pl -S -n 16 > xx.txt ; time ../solver_z3 xx.txt | tee qu_Bool_n16_Z3.res | sed '/Bool/{N;s/\n//;}' |./quSMT.pl -r -n 16  > qu_n6_M5.html

The quSMT.pl script using -r and provided with the board size will generate an html version of the solver output lines. The resulting .html can be examined in a standard web browser.

The M5 solver generates result lines in the form 

$ head qu_Bool_n16_M5.res

sat

( (V0 false)

  (V1 false)

  (V2 false)

  (V3 false)

  (V4 false)

  (V5 false)

  (V6 false)

  (V7 false)

  (V8 false)

. . . 

The Z3 solver generates lines in the form 

$ head  qu_Bool_n16_Z3.res 

sat

(model 

  (define-fun V52 () Bool

    false)

  (define-fun V61 () Bool

    true)

  (define-fun V62 () Bool

    false)

  (define-fun V204 () Bool

    false)

…..

that are transformed into single lines for each value using the stream editor sed script in the command pipeline.

(define-fun V52 () Bool   false)

Results and timing scalability

Table 2 - Solution times

The Z3 solver is general faster on the non-trivial size boards. Both solvers, in integer logic mode, have very long run times once the boardEdgeSize is over eight. For comparison a simplistic "place next queen in next empty square" algorithm is listed. This simple strategy did not place all the queens on the board successfully. The solvers both placed the full compliments of queens in non-conflicting squares.

In the result images, for a boardEdgeSize of 16, (figs 5 and 6 ) the placed queens are numbered on a red background. The square numbers are on blue backgrounds. These are generated using boolean logic version of solvers. The checking text after the matrix is the count of queens on each Row, column and diagonal and show that valid solutions. In a correct answer none of the red queens should be on the same row, column or diagonal as any other queen.

Fig 6 : N=16 Solver MathSAT

Fig 7: N=16 Solver Z3

To show that the solution checking logic is working the steam editor sed is used on the command line to change a solver result line, effectively placing an extra "1" queen in the solution on board square 0.

$ ./quSMT.pl -s -n 16 | time ../solver_m5 | sed '/V0/s/false/true/' | ./quSMT.pl -r -n 16  > qu_n16_M5BAD.html

Fig 8 : N=16 Solver Z3 using Booleans with one result value manipulated and ERROR message showing for the extra placed queen

Conclusion

It can be seen in table 2 that sending the boolean descriptions of the problem to both solvers quickly generates results and scales well up to board sizes much larger than 100 * 100. Using the rotation method to pre-calculate the groups of squares that belong to the same row, column and diagonals is a very useful way to simplify the production of the SMT logic lines in this problem. Some further investigation is required to see why both solvers performs slowly on the larger board sizes in integer mode.

The largest board solved so far was 320 * 320 which generated a 1.4GB input file that took the Z3 solver about 20 minutes to correctly complete.

The queens social distancing problem has provided a good demonstration of a general purpose logic solver to tackle a specific problem. The general technique of reducing a problem to an abstract set of logic lines that can be sent to a solver is demonstrated. 

Other research has shown that using the combination of a puzzle logic generating scripts and established solver allows a wide range of other integer, placement and logic puzzles to be solved without the need to implement special solving algorithms for each different puzzle.  Sudoku of all types, shapes and sizes, Killer Sudoku (Kenken), Gogen, Hidato , Suguru and Kakuro have all been shown suitable for this problem reduction and solving technique. The classic four colour problem can also be solved using a logic solver. Harry Potter fans would describe solvers as the Bezoar of CompSci.

References

MathSAT the m5 solver used here.

Z3 the Z3 solver made by Microsoft - get it here

Eight Queens placement problem

Using SMT for sudoku puzzles

Programming Z3 Sudoku section from Section 8.1 page 139 uses python and a library to build logic lines.

Appendix qu_SMT.pl Script usage

        Look for the position of N queens by generating the positions of squares when rotated by 45 Degrees

        Usage : quSMT.pl -{s|S|m|M} -n n

        -n n size of square board or defaults to 8

        -m print out the coordinates and rotated coordinates table then exit

        -M do -m then print out the rows and cols and dx,dy groups then exit

        -s Generate smt2 Bool output then exit

        -S Generate smt2 Int output then exit (much slower in solver than Bool version)

        -r Read results from mathSAT M5 (or Z3 solver after processing) from STDIN and push out .html table

        -v n set verbose level Use -v above 3 to see workings

        -h print help

        

     if none of  M m s S are set then will display a simple "place on next empty square solver"

try      ./quSMT.pl -n 12 -v 6  # shows working by using pause at -v >5

try      ./quSMT.pl -s | ../solver_m5 | ./quSMT.pl -r > qu_n5sM5.html ; open qu_n5sM5.html

try      ./quSMT.pl -s -n 25 > qu_n25s.txt ;  time ../solver_z3 qu_n25s.txt | sed '/Bool/{N;s/\n//;}' | ./quSMT.pl -rn 25  > qu_n125sZ3.html

         then open qu_n125sZ3.html in a browser

        

Checking is done on Row,Col and Diag counts. Use this between solver and display to check error mechanism

        sed '/V0/s/false/true/'

Use this to adapt Z3 output lines for display by script

        sed '/Bool/ll//{N;s/\n//;}'