# Logic: representation and inference

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

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