# SAT Encoding: Common Constraint Patterns And Their Encodings

If you have read SAT encoding and are interested in ways to encode a problem as a SAT problem, then here is a list of common constraint patterns that can be used to easily encode the constraints of a problem and its solution as a CNF formula.

In the below exposition, due to the limitation of the presentation medium, equal symbol (=) is used to denote equivalence. Also, all variables are propositional variables.

# Simple Patterns (S)

1. x and y: `x & y = x & y`
2. x or y: `x|y = (x|y)`
3. x implies y: `x->y = (!x|y)`
4. x is equivalent to y: `x<->y = x->y & y->x = (!x|y) & (!y|x)`
5. there exists xi: `Exists(xi) = (x1|x2|x3|...|xn|F)` False is added at the end to account for the situation when there are no `xi`s.
6. for all xi: `ForAll(xi) = (x1 & x2 & x3 & ... & xn & T)` True is added at the end to account for the situation when there are no `xi`s.

In the below exposition, we will not explicitly add False and True when transforming `Exists` and `ForAll` quantifiers.

# Compound Patterns (C)

1. x implies (y and z): `x -> (y & z) = (x->y) & (x->z) = (!x|y) & (!x|z)`
2. x implies (y or z): `x -> (y|z) = (!x|y|z)`
3. (x and y) implies z: `(x & y) -> z = (!(x & y)|z) = (!x|!y|z)`
4. (x or y) implies z: `(x|y) -> z = (x->z) & (y->z) = (!x|z) & (!y|z)`
5. x implies there exists yi: `x -> Exists(yi) = (!x|y1|y2|...|yn)`
6. x implies for all yi: `x -> ForAll(yi) = (x->y1) & (x->y2) & ... & (x->yn) = (!x|y1) & (!x|y2) & ... & (!x|yn)`
7. (there exists yi) implies x: `Exists(yi) -> x = (y1|y2|...|yn) -> x = (y1->x) & (y2->x) & ... & (yn->x) = (!y1|x) & (!y2|x) & ... & (!yn|x)`
8. (for all yi) implies x: `ForAll(yi) -> x = (y1 & y2 & … & yn) -> x = (!y1|!y2|…|!yn|x)`
9. (p and q) or (x and y)
`(p & q)|(x & y) = (t1|t2) & (t1<->(p & q)) & (t2<->(x & y))= (t1|t2) &  (t1->(p & q)) & ((p & q)->t1) &   (t2->(x & y)) & ((x & y)->t2)= (t1|t2) &   (!t1|p) & (!t1|q) & (!p|!q|t1) &  (!t2|x) & (!t2|y) & (!x|!y|t2)`

The above encoding uses Tseitin transformation: a new variable `tn` is introduced for a sub-formula, all occurrences of the sub-formula is replaced by `tn`, and new clauses are added to establish the equivalence of `tn` and the sub-formula.

# Complex Patterns (X)

1. x implies (there exists (yi & zi))

`x -> Exists(yi & zi)= x -> ((y1 & z1) | (y2 & z2) | ... | (yn & zn))= (!x|(y1 & z1)|(y2 & z2)|...|(yn & zn))= (!x|t1|t2|...|tn) &   ((y1 & z1) <-> t1) & ((y2 & z2) <-> t2) & ... & ((yn & zn) <-> tn)= (!x|t1|t2|...|tn) &   ((y1 & z1) -> t1) & ((y2 & z2) -> t2) & ... & ((yn & zn) -> tn) &  (t1 -> (y1 & z1)) & (t2 -> (y2 & z2)) & ... & (tn -> (yn & zn))  = (!x|t1|t2|...|tn) &   (!y1|!z1|!t1) & (!y2|!z2|!t2) & ... & (!yn|!zn|!tn) &  (!t1|y1) & (!t1|z1) & (!t2|y2) & (!t2|z2) & ... &   (!tn|yn) & (!tn|zn)`

2. x implies (there exists (yi|zi))

`x -> Exists(yi|zi)= x -> ((y1|z1) | (y2|z2) | ... | (yn|zn))= x -> (y1|z1|y2|z2|...|yn|zn) = (!x|y1|z1|y2|z2|...|yn|zn)`

3. x implies (for all (yi & zi))

`x -> ForAll(yi & zi)= x -> ((y1 & z1) & (y2 & z2) & ... & (yn & zn))= x -> (y1 & z1 & y2 & z2 & ... & yn & zn)= (!x|y1) & (!x|z1) & (!x|y2) & (!x|z2) & ... & (!x|yn) & (!x|zn)`

4. x implies (for all (yi|zi))

`x -> ForAll(yi|zi)= x -> ((y1|z1) & (y2|z2) & ... & (yn|zn))= (x -> (y1|z1)) & (x -> (y2|z2)) & ... & (x -> (yn|zn))= (!x|y1|z1) & (!x|y2|z2) & ... & (!x|yn|zn)`

5. At least one of xi is true

`AtLeastOne(x1,x2,...,xn)= Exists(xi)= (x1|x2|x3|...|xn)`

6. At most one of xi is true

`AtMostOne(x1,x2,...,xn)= x1->ForAll(!xj where j<>1) &   x2->ForAll(!xj where j<>2) &  ... &   xn->ForAll(!xj where j<>n)= x1->!x2 & x1->!x3 & ... & x1->!xn &   x2->!x1 & x2->!x3 & ... & x2->!xn &   ... &   xn->!x1 & xn->!x2 & ... & xn->!xm            [where m=n-1]= (!x1|!x2) & (!x1|!x3) & ... & (!x1|!xn) &   (!x2|!x1) & (!x2|!x3) & ... & (!x2|!xn) &   ... &   (!xn|!x1) & (!xn|!x2) & ... & (!xn|!xm)`

7. Exactly one of xi is true

`ExactlyOneOf(x1,x2,...,xn)= Atleast(x1,x2,...,xn) & AtMostOne(x1, x2,...,xn)`

8. At least two of xi is true

`AtLeastTwo(x1,x2,...,xn)= (x1->AtLeastOne(x2,x3,...,xn)) &   (x2->AtLeastOne(x1,x3,...,xn)) &  ... &  (xn->AtLeastOne(x1,x2,...,xm)     [where m=n-1]= (!x1|x2|x3|...|xn) &   (!x2|x1|x3|...|xn) &  ... &  (!xn|x1|x2|...|xm)`

9. At most two of xi is true

`AtMostTwo(x1,x2,...,xn)= (x1 & x2)->ForAll(!xj where j<>1 & j<>2) &   (x1 & x3)->ForAll(!xj where j<>1 & j<>3) & ... &   (x1 & xn)->ForAll(!xj where j<>1 & j<>n) &  (x2 & x3)->ForAll(!xj where j<>2 & j<>3) &   (x2 & x4)->ForAll(!xj where j<>2 & j<>4) & ... &   (x2 & xn)->ForAll(!xj where j<>2 & j<>n) &  ... &  (xm & xn)->ForAll(!xj where j<>m & j<>n)      [where m=n-1]= (x1 & x2)->!x3 & (x1 & x2)->!x4 & ... & (x1 & x2)->!xn &  (x1 & x3)->!x2 & (x1 & x3)->!x4 & ... & (x1 & x3)->!xn & ... &  (x1 & xn)->!x2 & (x1 & xn)->!x3 & ... & (x1 & xn)->!xm &  (x2 & x3)->!x1 & (x2 & x3)->!x4 & ... & (x2 & x3)->!xn &  (x2 & x4)->!x1 & (x2 & x4)->!x3 & ... & (x2 & x4)->!xn & ... &  (x2 & xn)->!x1 & (x2 & xn)->!x3 & ... & (x2 & xn)->!xm &  ... &  (xm & xn)->!x1 & (xm & xn)->!x2 & ... & (xm & xn)->!xl        [where l=m-1]= (!x1|!x2|!x3) & (!x1|!x2|!x4) & ... & (!x1|!x2|!xn) &   (!x1|!x3|!x2) & (!x1|!x3|!x4) & ... & (!x1|!x3|!xn) & ... &  (!x1|!xn|!x2) & (!x1|!xn|!x3) & ... & (!x1|!xn|!xm) &   (!x2|!x3|!x1) & (!x2|!x3|!x4) & ... & (!x2|!x3|!xn) &  (!x2|!x4|!x1) & (!x2|!x4|!x3) & ... & (!x2|!x4|!xn) & ... &  (!x2|!xn|!x2) & (!x2|!xn|!x3) & ... & (!x2|!xn|!xm) &  ... &  (!xm|!xn|!x1) & (!xm|!xn|!x2) & ... & (!xm|!xn|!xl)`

# For You To Do

The encoding for the converse of the complex patterns 1, 2, 3, and 4 can be identified using the equivalence `x->y = !y->!x`. Try deriving these encodings.

# What next?

Next time, I will solve a simple version of Sudoku by encoding it as a SAT problem.

--

--