• Step 1: Define the Variables:

  For each position (i,j) on the chessboard, where 0 ≤ i,j< N, we introduce a Boolean variable x(i, j):

  • x(i, j) = True → there is a queen at position (i,j)

  • x(i, j) = False → there is no queen at position (i,j)

  So, for a 4×4 board, we have N^2=16 16 Boolean variables.

• Step 2: Add the Constraints: To make sure the solution is valid, we need to enforce three types of constraints:

  • Exactly one queen per row

    • In each row i, exactly one of the variables x(i,0),x(i,1),…,x(i,N−1) must be True.

    • This ensures every row has one queen.

  • Exactly one queen per column

    • In each column j, exactly one of the variables x(0,j),x(1,j),…,x(N−1,j) must be True.

    • This ensures every column has one queen.

  • At most one queen per diagonal:

    • Main diagonals: For all positions where i−j=k (with k=−N+1,…,N−1), at most one x(i,j) can be True.

    • Anti-diagonals: For all positions where i+j=k (with k=0,…,2N−2), at most one x(i,j) can be True.

    • These prevent queens from attacking each other diagonally.

• Step 3: Combine Everything

  All these constraints together form a SAT formula. A SAT solver can then find an assignment of True/False values for all x(i,j) x(i,j) that satisfies all constraints—this corresponds to a valid arrangement of queens.

4-queen.txt

;; Definitions of the 16 boolean variables

(declare-const x0y0 Bool)

(declare-const x0y1 Bool)

(declare-const x0y2 Bool)

(declare-const x0y3 Bool)

(declare-const x1y0 Bool)

(declare-const x1y1 Bool)

(declare-const x1y2 Bool)

(declare-const x1y3 Bool)

(declare-const x2y0 Bool)

(declare-const x2y1 Bool)

(declare-const x2y2 Bool)

(declare-const x2y3 Bool)

(declare-const x3y0 Bool)

(declare-const x3y1 Bool)

(declare-const x3y2 Bool)

(declare-const x3y3 Bool)

;;"at least one queen by line" clauses

(assert (or x0y0  x0y1  x0y2 x0y3))

(assert (or x1y0  x1y1  x1y2 x1y3))

(assert (or x2y0  x2y1  x2y2 x2y3))

(assert (or x3y0  x3y1  x3y2 x3y3))

;;"only one queen by line" clauses

(assert (not (or(and x0y1 x0y0)(and x0y2 x0y0)(and x0y2 x0y1)(and x0y3 x0y0)(and x0y3 x0y1)(and x0y3 x0y2))))

(assert (not (or(and x1y1 x1y0)(and x1y2 x1y0)(and x1y2 x1y1)(and x1y3 x1y0)(and x1y3 x1y1)(and x1y3 x1y2))))

(assert (not (or(and x2y1 x2y0)(and x2y2 x2y0)(and x2y2 x2y1)(and x2y3 x2y0)(and x2y3 x2y1)(and x2y3 x2y2))))

(assert (not (or(and x3y1 x3y0)(and x3y2 x3y0)(and x3y2 x3y1)(and x3y3 x3y0)(and x3y3 x3y1)(and x3y3 x3y2))))

;;"only one queen by column" clauses

(assert (not (or(and x1y0 x0y0)(and x2y0 x0y0)(and x2y0 x1y0)(and x3y0 x0y0)(and x3y0 x1y0)(and x3y0 x2y0))))

(assert (not (or(and x1y1 x0y1)(and x2y1 x0y1)(and x2y1 x1y1)(and x3y1 x0y1)(and x3y1 x1y1)(and x3y1 x2y1))))

(assert (not (or(and x1y2 x0y2)(and x2y2 x0y2)(and x2y2 x1y2)(and x3y2 x0y2)(and x3y2 x1y2)(and x3y2 x2y2))))

(assert (not (or(and x1y3 x0y3)(and x2y3 x0y3)(and x2y3 x1y3)(and x3y3 x0y3)(and x3y3 x1y3)(and x3y3 x2y3))))

;;"only one queen by diagonal" clauses

(assert (not (or (and x0y0 x1y1) (and x0y0 x2y2) (and x0y0 x3y3) (and x1y1 x2y2) (and x1y1 x3y3) (and x2y2 x3y3))))

(assert (not (or (and x0y1 x1y2) (and x0y1 x2y3) (and x1y2 x2y3))))

(assert (not (or (and x0y2 x1y3))))

(assert (not (or (and x1y0 x2y1) (and x1y0 x3y2) (and x2y1 x3y2))))

(assert (not (or (and x2y0 x3y1))))

(assert (not (or (and x1y1 x0y0) (and x2y2 x0y0) (and x3y3 x0y0) (and x2y2 x1y1) (and x3y3 x1y1) (and x3y3 x2y2))))

(assert (not (or (and x1y2 x0y1) (and x2y3 x0y1) (and x2y3 x1y2))))

(assert (not (or (and x1y3 x0y2))))

(assert (not (or (and x2y1 x1y0) (and x3y2 x1y0) (and x3y2 x2y1))))

(assert (not (or (and x3y1 x2y0))))

;;"only one queen by diagonal" clauses (other direction)

(assert (not (or (and x0y1 x1y0))))

(assert (not (or (and x0y2 x1y1) (and x0y2 x2y0) (and x1y1 x2y0))))

(assert (not (or (and x1y3 x1y2) (and x0y3 x2y1) (and x0y3 x3y0) (and x1y2 x2y1) (and x1y2 x3y0) (and x2y1 x3y0))))

(assert (not (or (and x1y3 x2y2) (and x1y3 x3y1) (and x2y2 x3y1))))

(assert (not (or (and x2y3 x3y2))))

;; Check if the generate model is satisfiable and output a model.

(check-sat)

(get-model)

shell

> z3 4-queen.txt
sat
(
  (define-fun x3y1 () Bool
    true)
  (define-fun x1y3 () Bool
    false)
  (define-fun x3y3 () Bool
    false)
  (define-fun x1y0 () Bool
    true)
  (define-fun x1y1 () Bool
    false)
  (define-fun x0y2 () Bool
    true)
  (define-fun x2y1 () Bool
    false)
  (define-fun x0y1 () Bool
    false)
  (define-fun x0y3 () Bool
    false)
  (define-fun x0y0 () Bool
    false)
  (define-fun x2y3 () Bool
    true)
  (define-fun x1y2 () Bool
    false)
  (define-fun x3y0 () Bool
    false)
  (define-fun x3y2 () Bool
    false)
  (define-fun x2y2 () Bool
    false)
  (define-fun x2y0 () Bool
    false)
)