* SAT Solver Search

The Four Squares Puzzle

• Given these four pieces

  +-----+  +-----+  +-----+  +-----+
  |  3  |  |  3  |  |  2  |  |  1  |
  |4   1|  |2   4|  |4   1|  |2   4|
  |  2  |  |  1  |  |  3  |  |  3  |
  +-----+  +-----+  +-----+  +-----+
  

  we can rearrange and rotate them arbitrarily and assemble them into a square

  +-----+-----+
  |  4  |  3  |
  |3   1|1   4|
  |  2  |  2  |
  +-----+-----+
  |  2  |  4  |
  |3   1|2   3|
  |  4  |  1  |
  +-----+-----+
  

  Can we make a square such that all the edges match?

• Obvious approach: Plain ol' state space search. Pain to code, but should run very fast: 3! × 4^4 = 1536 states

• Ah, but 3×3, 4×4, etc…

Four Squares using QPROP

• Let's solve this puzzle by

  • Writing a QPROP formula whose models are solutions

  • Converting the formula to a big PROP formula

  • Looking for SAT model

  • Translating the model back to a puzzle solution

• PROP SAT solvers are scary fast, incorporating piles of clever search techniques we don't want to rewrite from scratch

Modeling Four Squares: Setup

• Number the pieces 1..4, the positions in the square 1..4. We will number the square positions clockwise starting from the upper left. We will number the edges of the piece counterclockwise starting from the right edge.

  l(s, p) iff piece p is in square s  (location)
  

• Number the coordinates of the edges of each square 1..4

  m(s, e, n) iff piece in square s at edge e is n (match)
  

• Number the edges of each piece 1..4

  v(p, e, n) iff piece p at edge e is n (value)
  

• Number the rotations of each piece 0..3. Rotations will be counterclockwise.

  r(p, k) iff piece p has rotation k
  

Modeling Four Squares: Basic Constraints

• Every piece is at some location

  forall s . exists p . l(s, p)
  

• No location contains more than one piece

  forall s . forall p1, p2 | p1 =/= p2 . not l(s, p1) or not l(s, p2)
  

• First piece is in first corner (remove rotational symmetry)

  l(1, 1)
  

• Every location has a piece

  forall p . exists s . l(s, p)
  

• No piece is at more than one location

  forall p . forall s1, s2 | s1 =/= s2 . not l(s1, p) or not l(s2, p)
  

• Every piece is at some rotation

  forall p . exists k . r(p, k)
  

• No piece has more than one rotation

  forall p . forall k1, k2 | k1 =/= k2 . not r(p, k1) or not r(p, k2)
  

Modeling Four Squares: Fancy Constraints

• Square coordinates are a function of piece location and rotation

  forall s, p, k, e, n .
      m(s, e, n) if l(p, s) and r(p, k) and v(p, (4 - k + e) mod 4, n)
  

• No square edge can have more than one value

  forall s, e . forall n1, n2 | n1 =/= n2 .
      not m(s, e, n1) or not m(s, e, n2)
  

• Edges must match

  forall s1, e1, s2, e2 |
     s1 = 1 and e1 = 1 and s2 = 2 and e2 = 3 or … .
         forall n . m(s1, e1, n) iff m(s2, e2, n)
  

"Grounding" As PROP

• Treat predicates as subscripted atoms: l(s, p) → L#s#p

• Build a numbering function so that atoms run A1…An

• Write for loops that generate CNF clauses

• Basic constraints are already CNF; fancy constraints need some work

• Fancy constraint first clause count 256, total clause count less than 10× that

• Number of atoms for m predicate 64, total variable count less than 10× that

Solving An Instance of Four Squares

• Add in clauses describing the instance pieces

  v(1, 1, 1)
  v(1, 2, 3)
  …
  

• Run the SAT solver

• Take model (yes, this problem is solvable) and find the l and r atoms that are true. This gives the location and rotation of each piece!

Extending To Nine Squares And Beyond

• Extend the piece and square numbering

• Modify the fancy matching constraint

• That's it!

Sudoku Example

• Sudoku SAT generator / solver in Haskell sudoku-sat-hs