Peaceable Queens

library(purrr)
library(satire)

The Peaceable Queens Puzzle

The Peaceable Queens puzzle

Peaceable coexisting armies of queens: the maximum number m such that m white queens and m black queens can coexist on an n X n chessboard without attacking each other.

I.e. how can you place equal armies of black and white queens on a chessboard, and not have the opposing armies attack each other?

Nomenclature

Constructing a SAT problem involves setting up a lot of Boolean variables, assigning meaning to them, and defining relationships between them.

At a high level, the constraints on this problem are:

equal number of black and white queens
a white queen on any cell means that a black queen cannot also be there (and vide versa)
a white queen o row, column or diagonal means that a black queen cannot also be there (and vice versa).

This problem will be solved for a 5x5 chess board.

Individual squares

There will be 25 variables to indicate the position of white queens on the board (w11 to w55), and similarly for black queens. When a variable is TRUE, it means that a queen of that color exists at that location.

Row variables

For both the black and white queens, define row variables which are TRUE when any square in that row contains a queen of that color.

Similar define column variables and diagonal variables for each queen color.

Basic pieces in R

white <- matrix(c(
  'w11', 'w12', 'w13', 'w14', 'w15', 
  'w21', 'w22', 'w23', 'w24', 'w25', 
  'w31', 'w32', 'w33', 'w34', 'w35', 
  'w41', 'w42', 'w43', 'w44', 'w45', 
  'w51', 'w52', 'w53', 'w54', 'w55' 
), 5, 5, byrow = TRUE)


black <- matrix(c(
  'b11', 'b12', 'b13', 'b14', 'b15', 
  'b21', 'b22', 'b23', 'b24', 'b25', 
  'b31', 'b32', 'b33', 'b34', 'b35', 
  'b41', 'b42', 'b43', 'b44', 'b45', 
  'b51', 'b52', 'b53', 'b54', 'b55' 
), 5, 5, byrow = TRUE)


diag_up <- matrix(c(
  1, 2, 3, 4, 5, 
  2, 3, 4, 5, 6,
  3, 4, 5, 6, 7,
  4, 5, 6, 7, 8,
  5, 6, 7, 8, 9
), 5, 5, byrow = TRUE)

diag_down <- diag_up[, 5:1]

Boolean Expressions

Expressions constraining the row/column indicator variables (for white)

Row indicator variables (e.g. wrow1) are variables which signal that there exists a queen (a white one) in that row.

That is, if a square in a row contains a queen, then the indicator variable should also be set. In Boolean terms “a square having a queen implies that the row variable is true”.

To write that a variable implies that another is true:

w11 -> wrow1

This says “If w11 is TRUE then wrow1 must be TRUE”.

This is true for all locations in the first row i.e.

(w11 -> wrow1) & (w12 -> wrow1) & (w13 -> wrow1) & (w14 -> wrow1) & (w15 -> wrow1)

This logic is repeated for all row and column indicator variables for white queens

white_rows <- map(1:5, \(row) {
  glue::glue("w{row}{1:5} -> wrow{row}")
}) |> flatten_chr()
white_rows

#>  [1] "w11 -> wrow1" "w12 -> wrow1" "w13 -> wrow1" "w14 -> wrow1" "w15 -> wrow1"
#>  [6] "w21 -> wrow2" "w22 -> wrow2" "w23 -> wrow2" "w24 -> wrow2" "w25 -> wrow2"
#> [11] "w31 -> wrow3" "w32 -> wrow3" "w33 -> wrow3" "w34 -> wrow3" "w35 -> wrow3"
#> [16] "w41 -> wrow4" "w42 -> wrow4" "w43 -> wrow4" "w44 -> wrow4" "w45 -> wrow4"
#> [21] "w51 -> wrow5" "w52 -> wrow5" "w53 -> wrow5" "w54 -> wrow5" "w55 -> wrow5"

white_cols <- map(1:5, \(col) {
  glue::glue("w{1:5}{col} -> wcol{col}")
}) |> flatten_chr()
white_cols

#>  [1] "w11 -> wcol1" "w21 -> wcol1" "w31 -> wcol1" "w41 -> wcol1" "w51 -> wcol1"
#>  [6] "w12 -> wcol2" "w22 -> wcol2" "w32 -> wcol2" "w42 -> wcol2" "w52 -> wcol2"
#> [11] "w13 -> wcol3" "w23 -> wcol3" "w33 -> wcol3" "w43 -> wcol3" "w53 -> wcol3"
#> [16] "w14 -> wcol4" "w24 -> wcol4" "w34 -> wcol4" "w44 -> wcol4" "w54 -> wcol4"
#> [21] "w15 -> wcol5" "w25 -> wcol5" "w35 -> wcol5" "w45 -> wcol5" "w55 -> wcol5"

Expressions constraining the row/column indicator variables (for black)

This logic is repeated for the indicator variables for black queens in each row and column

black_rows <- map(1:5, \(row) {
  glue::glue("b{row}{1:5} -> brow{row}")
}) |> flatten_chr()
black_rows

#>  [1] "b11 -> brow1" "b12 -> brow1" "b13 -> brow1" "b14 -> brow1" "b15 -> brow1"
#>  [6] "b21 -> brow2" "b22 -> brow2" "b23 -> brow2" "b24 -> brow2" "b25 -> brow2"
#> [11] "b31 -> brow3" "b32 -> brow3" "b33 -> brow3" "b34 -> brow3" "b35 -> brow3"
#> [16] "b41 -> brow4" "b42 -> brow4" "b43 -> brow4" "b44 -> brow4" "b45 -> brow4"
#> [21] "b51 -> brow5" "b52 -> brow5" "b53 -> brow5" "b54 -> brow5" "b55 -> brow5"

black_cols <- map(1:5, \(col) {
  glue::glue("b{1:5}{col} -> bcol{col}")
}) |> flatten_chr()
black_cols

#>  [1] "b11 -> bcol1" "b21 -> bcol1" "b31 -> bcol1" "b41 -> bcol1" "b51 -> bcol1"
#>  [6] "b12 -> bcol2" "b22 -> bcol2" "b32 -> bcol2" "b42 -> bcol2" "b52 -> bcol2"
#> [11] "b13 -> bcol3" "b23 -> bcol3" "b33 -> bcol3" "b43 -> bcol3" "b53 -> bcol3"
#> [16] "b14 -> bcol4" "b24 -> bcol4" "b34 -> bcol4" "b44 -> bcol4" "b54 -> bcol4"
#> [21] "b15 -> bcol5" "b25 -> bcol5" "b35 -> bcol5" "b45 -> bcol5" "b55 -> bcol5"

Exclusivity of white/black indicator variables

In order to force the constraint that white and black queens are not in a position to attack each other, it must be the case that wrow1 and brow1 cannot both be true at the same time i.e. one of them must be false.

So for all row/column indicator variables, add logic that the black indicator variables cannot be true at the same time as the equivalent white indicator variables.

exclusive_rows <- glue::glue("!wrow{1:5} | !brow{1:5}")
exclusive_rows

#> !wrow1 | !brow1
#> !wrow2 | !brow2
#> !wrow3 | !brow3
#> !wrow4 | !brow4
#> !wrow5 | !brow5

exclusive_cols <- glue::glue("!wcol{1:5} | !bcol{1:5}")
exclusive_cols

#> !wcol1 | !bcol1
#> !wcol2 | !bcol2
#> !wcol3 | !bcol3
#> !wcol4 | !bcol4
#> !wcol5 | !bcol5

Expressions constraining the diagonals

A similar process is carried out for each diagonal on the board. That is, an indicator variable for each diagonal is true when one of its squares contains the queen of the specified color. Then exclusivity in the indicator variables is enforced so that a single diagonal cannot contain both black and white queens.

white_diag_up <- map(2:8, \(diag) {
  vars <- white[which(diag_up == diag)]
  glue::glue("{vars} -> wup{diag}")
}) |> flatten_chr()
white_diag_up

#>  [1] "w21 -> wup2" "w12 -> wup2" "w31 -> wup3" "w22 -> wup3" "w13 -> wup3"
#>  [6] "w41 -> wup4" "w32 -> wup4" "w23 -> wup4" "w14 -> wup4" "w51 -> wup5"
#> [11] "w42 -> wup5" "w33 -> wup5" "w24 -> wup5" "w15 -> wup5" "w52 -> wup6"
#> [16] "w43 -> wup6" "w34 -> wup6" "w25 -> wup6" "w53 -> wup7" "w44 -> wup7"
#> [21] "w35 -> wup7" "w54 -> wup8" "w45 -> wup8"

white_diag_down <- map(2:8, \(diag) {
  vars <- white[which(diag_down == diag)]
  glue::glue("{vars} -> wdown{diag}")
}) |> flatten_chr()
white_diag_down

#>  [1] "w14 -> wdown2" "w25 -> wdown2" "w13 -> wdown3" "w24 -> wdown3"
#>  [5] "w35 -> wdown3" "w12 -> wdown4" "w23 -> wdown4" "w34 -> wdown4"
#>  [9] "w45 -> wdown4" "w11 -> wdown5" "w22 -> wdown5" "w33 -> wdown5"
#> [13] "w44 -> wdown5" "w55 -> wdown5" "w21 -> wdown6" "w32 -> wdown6"
#> [17] "w43 -> wdown6" "w54 -> wdown6" "w31 -> wdown7" "w42 -> wdown7"
#> [21] "w53 -> wdown7" "w41 -> wdown8" "w52 -> wdown8"

black_diag_up <- map(2:8, \(diag) {
  vars <- black[which(diag_up == diag)]
  glue::glue("{vars} -> bup{diag}")
}) |> flatten_chr()
black_diag_up

#>  [1] "b21 -> bup2" "b12 -> bup2" "b31 -> bup3" "b22 -> bup3" "b13 -> bup3"
#>  [6] "b41 -> bup4" "b32 -> bup4" "b23 -> bup4" "b14 -> bup4" "b51 -> bup5"
#> [11] "b42 -> bup5" "b33 -> bup5" "b24 -> bup5" "b15 -> bup5" "b52 -> bup6"
#> [16] "b43 -> bup6" "b34 -> bup6" "b25 -> bup6" "b53 -> bup7" "b44 -> bup7"
#> [21] "b35 -> bup7" "b54 -> bup8" "b45 -> bup8"

black_diag_down <- map(2:8, \(diag) {
  vars <- black[which(diag_down == diag)]
  glue::glue("{vars} -> bdown{diag}")
}) |> flatten_chr()
black_diag_down

#>  [1] "b14 -> bdown2" "b25 -> bdown2" "b13 -> bdown3" "b24 -> bdown3"
#>  [5] "b35 -> bdown3" "b12 -> bdown4" "b23 -> bdown4" "b34 -> bdown4"
#>  [9] "b45 -> bdown4" "b11 -> bdown5" "b22 -> bdown5" "b33 -> bdown5"
#> [13] "b44 -> bdown5" "b55 -> bdown5" "b21 -> bdown6" "b32 -> bdown6"
#> [17] "b43 -> bdown6" "b54 -> bdown6" "b31 -> bdown7" "b42 -> bdown7"
#> [21] "b53 -> bdown7" "b41 -> bdown8" "b52 -> bdown8"

exclusive_diag_down <- glue::glue("!wdown{2:8} | !bdown{2:8}")
exclusive_diag_down

#> !wdown2 | !bdown2
#> !wdown3 | !bdown3
#> !wdown4 | !bdown4
#> !wdown5 | !bdown5
#> !wdown6 | !bdown6
#> !wdown7 | !bdown7
#> !wdown8 | !bdown8

exclusive_diag_up   <- glue::glue("!wup{2:8} | !bup{2:8}")
exclusive_diag_up

#> !wup2 | !bup2
#> !wup3 | !bup3
#> !wup4 | !bup4
#> !wup5 | !bup5
#> !wup6 | !bup6
#> !wup7 | !bup7
#> !wup8 | !bup8

Creating the SAT problem in `{satire}`

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Create a SAT problem
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat <- sat_new()

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Add all the expressions 
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
all_exprs <- c(
  white_rows, white_cols,
  black_rows, black_cols,
  exclusive_rows,
  exclusive_cols,
  white_diag_up, white_diag_down,
  black_diag_up, black_diag_down,
  exclusive_diag_down,
  exclusive_diag_up
)

sat_add_exprs(sat, all_exprs)
sat

#> <sat> vars = 98 , clauses = 216

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# The solution must also contain the same number of queens of each color
#
# If we try to make this N = 5 queens, then the problem is unsatisfiable - 
# i.e. sat_solve_dpll() will return NULL (after 10 minutes!)
# This means there is no solution for 5 queens of each color.
# So let's try it with 4 queens of each color
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_exactly_k(sat, white, 4)
sat_card_exactly_k(sat, black, 4)
sat

#> <sat> vars = 1298 , clauses = 2662

Constraining the solution to a particular count of queens adds 1200 new dummy variables and 2500 new Boolean statements!

Solving

Solving via the pure R DPLL solver (sat_solver_dpll()) takes around 20 seconds on an M2 Mac.

The form of the solution is a data.frame where each column is a variable in the problem, and each row is a solution.

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Takes about 20s on an M2 mac
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sol <- sat_solve_dpll(sat, remove = "^dummy|row|col|up|down")
sol

#>     w11  w12   w13  w14   w15   w21   w22   w23   w24  w25   w31   w32   w33
#> 1 FALSE TRUE FALSE TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE
#>     w34   w35   w41   w42   w43   w44  w45   w51   w52   w53   w54   w55   b11
#> 1 FALSE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE FALSE FALSE
#>     b12   b13   b14   b15   b21   b22   b23   b24   b25  b31   b32  b33   b34
#> 1 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE TRUE FALSE TRUE FALSE
#>     b35   b41   b42   b43   b44   b45  b51   b52  b53   b54   b55
#> 1 FALSE FALSE FALSE FALSE FALSE FALSE TRUE FALSE TRUE FALSE FALSE

The solution to the puzzle is where the queens exist on the board i.e. the variables which are TRUE

#> [1] "w12" "w14" "w25" "w45" "b31" "b33" "b51" "b53"

Plotting these queen locations shows the solution!

Solving with an external solver

The built-in solvers in the {satire} package are written in pure R. They are for demonstration and education, and are easily out-classed by external solvers such as minisat, picosat, kissat etc.

DIMACS export

The easiest way to use an external solver is to export the problem in DIMACS format and run the solver manually.

e.g.

writeLines(sat$dimacs, "pqueens.cnf")
# Run a sat solver at the command line
# satsolver pqueens.cnf