Skip to content

pdx-cs-ai/foursquares

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

12 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

foursquare-sat: Solve Foursquare puzzles using a SAT engine

Bart Massey

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?

Our solution strategy will involve:

  • Creating a SAT formula from the instance
  • Solving that formula with an off-the-shelf solver
  • Interpreting the SAT soln as an instance solution

Running

You must have picosat installed to use this code as-is. It can be easily modified for other DIMACS-format SAT solvers. To try it out:

sh foursquare-sat.sh puzzles/orig.txt

You should see the puzzle and its solution.

You can say python3 puzgen.py to get more puzzles. Puzzle format is one piece per row with the edge numbers listed in counterclockwise order.

Modeling Foursquares

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
    

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)
    

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)
    

About

four-squares sat rep in python

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published