N queens puzzle

library(satire)
library(ggplot2)

The N-queens puzzle

The N queens puzzle is a challenge to place N queens on an N x N chessboard so that no queens threaten each other.

This requires that no two queens share the same row, column or diagonal. For an 8x8 chessboard there are 92 solutions - one possible solution is pictured below.

In this vignette, the N-queens problem (with N = 4) will be formulated and solved using SAT techniques.

The 4-queens puzzle

This vignette will formulate and then solve the 4-queens puzzle i.e. placing 4 queens on a 4x4 chessboard so that no queens threaten each other.

First take an empty 4x4 chessboard

A Boolean variable (q11 - q44) is assigned to each square. When a variable is true it means that there is a queen at this location, and false means there is no queen at this location.

If 4 queens are placed at the following locations, then this is definitely not a solution as the lower two queens can attach each other.

What constraints exist?

To place 4 queens such that no queens can attack requires:

Each row can only contain 1 queen
Each column can only contain 1 queen
Each diagonal can only contain 1 queen (must be true for diagonals in both directions)

Defining the problem

sat <- sat_new()


#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Impose a constraint on the cardinality of each row
# i.e. Exactly 1 member of each row must be true
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_exactly_one(sat, c("q11", "q12", "q13", "q14"))
sat_card_exactly_one(sat, c("q21", "q22", "q23", "q24"))
sat_card_exactly_one(sat, c("q31", "q32", "q33", "q34"))
sat_card_exactly_one(sat, c("q41", "q42", "q43", "q44"))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Similarly, there can be only 1 queen in each column
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_exactly_one(sat, c("q11", "q21", "q31", "q41"))
sat_card_exactly_one(sat, c("q12", "q22", "q32", "q42"))
sat_card_exactly_one(sat, c("q13", "q23", "q33", "q43"))
sat_card_exactly_one(sat, c("q14", "q24", "q34", "q44"))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Similarly, there can be only 1 queen in each diagonal
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atmost_one(sat, c('q21', 'q12'))
sat_card_atmost_one(sat, c('q31', 'q22', 'q13'))
sat_card_atmost_one(sat, c('q41', 'q32', 'q23', 'q14'))
sat_card_atmost_one(sat, c('q42', 'q33', 'q24'))
sat_card_atmost_one(sat, c('q43', 'q34'))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Repeat for diagonals in the other direction
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atmost_one(sat, c('q13', 'q24'))
sat_card_atmost_one(sat, c('q12', 'q23', 'q34'))
sat_card_atmost_one(sat, c('q11', 'q22', 'q33', 'q44'))
sat_card_atmost_one(sat, c('q21', 'q32', 'q43'))
sat_card_atmost_one(sat, c('q31', 'q42'))


sat

#> <sat> vars = 16 , clauses = 84

Solve

There are only 16 variables in this problem which means an exhaustive search only requires checking 2^16 combinations. This is within the realm of the naive solver which pre-allocates all combinations and evaluates them in parallel using standard R evaluation.

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Solve using the built-in, naive, brute-force SAT solver
# There are 2 solutions!
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
solns <- sat_solve_naive(sat)
nrow(solns)

#> [1] 2

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Solution:
#   - columns = variable names
#   - row = a solution i.e. the boolean value of each variable in order to 
#           satisfy the problem
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
solns

#>     q11   q12   q13   q14   q21   q22   q23   q24   q31   q32   q33   q34   q41
#> 1 FALSE  TRUE FALSE FALSE FALSE FALSE FALSE  TRUE  TRUE FALSE FALSE FALSE FALSE
#> 2 FALSE FALSE  TRUE FALSE  TRUE FALSE FALSE FALSE FALSE FALSE FALSE  TRUE FALSE
#>     q42   q43   q44
#> 1 FALSE  TRUE FALSE
#> 2  TRUE FALSE FALSE

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Map these booleans to get the names of the variables which are TRUE
# i.e. the location of the queens
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
solns <- apply(solns, 1, \(x) names(solns)[which(x)], simplify = FALSE)
solns

#> [[1]]
#> [1] "q12" "q24" "q31" "q43"
#> 
#> [[2]]
#> [1] "q13" "q21" "q34" "q42"

Plot solution #1

solns[[1]]

#> [1] "q12" "q24" "q31" "q43"

Plot solution #2

solns[[2]]

#> [1] "q13" "q21" "q34" "q42"