SAT-SOLVING-EXAMPREP/Encoding.md

CNF (Conjunctive Normal Form)

• Conjunction of Disjunctions
• 'AND' of 'OR's
• (0 \lor 1 \lor -2) \land (0 \lor -5)

DNF (Disjunctive Normal Form)

• Conjunction of Disjunctions
• 'AND' of 'OR's
• (15 \land 1 \land -2) \lor (1 \land -5)
• Easy to see if there is a SAT assignment
  • Is any Clause SAT?
  • Conversely In CNF finding an UNSAT assignment is easy

Variables as Integers

• x, y, z \mapsto 1, 2, 3
• Efficient representation
• Can store assignments in an array
• Negation -var has a literal meaning in code

Encoding Problems to boolean formula

• For example compile: if x then y else z \mapsto (x \land y) \lor (\lnot x \land z)
• What do you encode?
  • Equivalence of two programs?
  • compile(A) \cancel\leftrightarrow compile(B)
  • Encode this, if its SAT we have a counterexample

NNF / Negation Normal Form

• Mixture of 'AND's and 'OR's
• But negation can only be in front of Variables
• Can be made easily using De Morgan
• Naive transformation from NNF to CNF
  • by merging via 'OR-distribution'
  • Merge on: (a \lor b) \lor (c \land d) \mapsto (a \lor b \lor c) \land (a \lor b \lor d)
• Exponential Fan out

Tseitin Transformation

• Extract Formula nodes into new variables and create a constraint list
• ((a \leftrightarrow b) \land (c \lor \overline{d}))
  • x_1 \leftrightarrow (a \leftrightarrow b)
  • x_2 \leftrightarrow \overline d
  • x_2 \leftrightarrow (c \lor x_2)
  • x_4 \leftrightarrow (x_1 \land x_3)
• Then transform all of them to CNF and conjunct them !
• The resulting formula grows linearly in respect to the size of the original formula
• Sometimes taking dividing into binary operations is not optimal (xor optimum is 3)

Plaisted–Greenbaum (PG)

• Only use implication instead of equivalence \leftrightarrow
• Direction depends on polarity of the subformula's occurrence
  • Positive polarity: only need x \rightarrow \varphi
  • Negative polarity: only need \varphi \rightarrow x
  • Mixed polarity (e.g. under XOR/biconditional): need both, i.e. full Tseitin x \leftrightarrow \varphi
• Example x \leftrightarrow (a \land b): positive occurrence needs (\overline x \lor a) \land (\overline x \lor b); negative occurrence needs just (\overline a \lor \overline b \lor x)
  • Positive occurrence: x appears unnegated in F, e.g. F = x \lor c (as a\land b becomes true, F can only become 'more satisfied') \Rightarrow only need x \rightarrow (a \land b)
  • Negative occurrence: x appears negated in F, e.g. F = \overline x \lor c (mirror case, F becomes 'more satisfied' as a \land b becomes false) \Rightarrow only need (a \land b) \rightarrow x