Peaceable Queens

library(ggplot2)
library(purrr)
library(satire)
library(picosatire)

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
# Let's try 5 of each color
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_exactly_k(sat, white, 5)
sat_card_exactly_k(sat, black, 5)
sat

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

However, attempting to solve with 5 queens of each color returns NULL - this indicates that the problem is unsatisfiable i.e. impossible!

pico_solve_satire(sat)

#> NULL

Now reconstruct the problem with the constraint that there must be only 4 of each color

sat <- sat_new()
sat_add_exprs(sat, all_exprs)
sat_card_exactly_k(sat, white, 4)
sat_card_exactly_k(sat, black, 4)

# Solve the problem.
# Remove some variables from the output as they are dummy, temporary or
# indicator variables.  This helps in removing duplicate solutions.
sol <- pico_solve_satire(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 TRUE FALSE FALSE FALSE FALSE FALSE
#>     w34   w35   w41   w42  w43   w44   w45   w51   w52   w53   w54   w55   b11
#> 1 FALSE FALSE FALSE FALSE TRUE FALSE FALSE 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 FALSE FALSE
#>    b35   b41   b42   b43   b44   b45  b51   b52   b53   b54  b55
#> 1 TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE TRUE

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

#> [1] "w12" "w14" "w23" "w43" "b31" "b35" "b51" "b55"

Plotting these queen locations shows the solution!