---
title: "Peaceable Queens"
output: rmarkdown::html_vignette
vignette: >
  %\VignetteIndexEntry{Peaceable Queens}
  %\VignetteEngine{knitr::rmarkdown}
  %\VignetteEncoding{UTF-8}
---

```{r, include = FALSE}
knitr::opts_chunk$set(
  collapse = FALSE,
  comment = "#>"
)
```


```{r setup}
library(ggplot2)
library(purrr)
library(satire)
library(picosatire)
```

## The Peaceable Queens Puzzle

The [Peaceable Queens puzzle](https://oeis.org/A250000)
    
    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.

```{r echo=FALSE}
board <- function(n = 5, cols = c('grey95', 'grey80')) {
  b <- expand.grid(x = seq(n), y = seq(n))
  b$col <- with(b, ifelse(y %% 2 == 0, x %% 2 == 0, x %% 2 == 1))
  ggplot(b) +
    geom_raster(aes(x, y, fill = col)) + 
    scale_fill_manual(values = cols, guide = 'none') +
    coord_equal() + 
    scale_y_reverse() +
    theme_void()
}
```

#### 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.

```{r echo=FALSE}
N <- 5

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# White queens
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
queens    <- expand.grid(row = seq(N), col = seq(N)) 
queens$nm <- with(queens, paste0("w", row, col))

board() + 
  geom_text(data = queens, aes(col, row, label = nm))


#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Black queens
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
queens    <- expand.grid(row = seq(N), col = seq(N)) 
queens$nm <- with(queens, paste0("b", row, col))

board() + 
  geom_text(data = queens, aes(col, row, label = nm))
```


#### 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.


```{r echo=FALSE, fig.width = 5, fig.height = 5}
N <- 6

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# White queens
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
queens    <- expand.grid(row = seq(N), col = seq(N)) 
queens$nm <- with(
  queens, 
  ifelse(
    row > 5, 
    paste0("wcol", col),
    ifelse(
      col > 5,
      paste0("wrow", row),
      paste0("w", row, col)
    )
  )
)
queens <- queens[queens$nm != 'wcol6', ] 

board() + 
  geom_text(data = queens, aes(col, row, label = nm)) +
  expand_limits(x = 6.2)
```





```{r echo=FALSE, fig.width = 5, fig.height = 5}
N <- 6

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# White queens
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
queens    <- expand.grid(row = seq(N), col = seq(N)) 
queens$nm <- with(
  queens, 
  ifelse(
    row ==4 & col > 5, 
    "wdown3",
    ifelse(
      col > 5,
      "",
      ifelse(
        col==1 & row > 5,
        "wup6",   
        ifelse(
          row > 5,
          "",
          paste0("w", row, col)
        )
      )
    )
  )
)

board() + 
  geom_text(data = queens, aes(col, row, label = nm)) + 
  annotate('segment', x = 3, y = 1, xend = 6, yend = 4, color = 'red' , linetype = 2) + 
  annotate('segment', x = 1, y = 6, xend = 5, yend = 2, color = 'blue', linetype = 2) +
  expand_limits(x = 6.2)
```


#### Basic pieces in R

```{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

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

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


### 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

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

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

### 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.

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

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


### 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.

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

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

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

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

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

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

## Creating the SAT problem in `{satire}`

```{r}
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# 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

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# 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
```

However, attempting to solve with 5 queens of each color returns `NULL` - this
indicates that the problem is unsatisfiable i.e. impossible!
```{r}
pico_solve_satire(sat)
```


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

```{r}
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
```


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


```{r echo=FALSE}
ss <- names(sol)[unlist(sol)]
ss
```

Plotting these queen locations shows the solution!

```{r echo=FALSE, fig.width = 6, fig.height = 6}
N <- 5
solqueens    <- expand.grid(row = seq(N), col = seq(N)) 
solqueens$w <- with(solqueens, paste0("w", row, col))
solqueens$b <- with(solqueens, paste0("b", row, col))
wq <- solqueens[solqueens$w %in% ss, ]
bq <- solqueens[solqueens$b %in% ss, ]


board() + 
  geom_label(data = wq, aes(col, row, label = 'Q'), fill = 'black', color = 'white', size = 12) + 
  geom_label(data = bq, aes(col, row, label = 'Q'), fill = 'white', color = 'black', size = 12)
```