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 xis.
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 xis.

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.