Problem Representation

  • Solving a problem with a computer:

    • Accurately describe the problem
    • Choose an instance representation in the computer
    • Select an algorithm to manipulate the representation
    • Execute

Properties of Representations

  • What properties of representations are important?

    • compactness: must be able to represent big instances efficiently

    • utility: must be compatible with good solution algorithms

    • soundness: should not report untruths

    • completeness: should not lose information

    • generality: should be able to represent all or most instances of interesting problems

    • transparency: reasoning about/with representation is efficient, easy

Standard Representations

  • What instance representations do people choose?

    • database: collection of facts
    • neural net: collection of "neuron weights"
    • functional: collection of functions
    • logical: collection of sentences

Prop Logic: A Review

  • Propositional Formula ("PROP"):

    • "Atoms" that can be either true or false. Names are commonly subscripted

    • "Connectives": and, or, not + parentheses

  • Things to do:

    • Normalization: transform a formula into some standard form (polytime)

    • Checking: for a given assignment, is a formula true or false? (polytime)

    • Satisfiability ("SAT"): is there an assignment that makes the formula true? (NP-complete)

    • Tautology: does every assignment make the formula true? (NP-complete, extra variables) AKA theorem-proving

First-Order Logic: A Review

  • First-order Formula:

    • "Predicates": Atoms that can take arguments (other predicates, variables)

    • "Variables": Value is predicate

    • "Quantifiers": "exists" and "forall" "bind" variables

  • Things to do: Normalization (polytime), checking (polytime), sat (undecidable), tautology (undecidable)

Quantified Propositional Logic

  • Quantified Propositional Formula ("QPROP"): First-order logic, but all variables are bound and have a given set of discrete values they could take on

  • Can turn (small) QPF into (large) PROP:

    • forall → and, exists → or

    • predicates are replaced by subscripted atoms

  • Compact notation for PROP, reduces mistakes

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

Last modified: Wednesday, 30 October 2019, 4:03 PM