Formal Methods 101: Boolean Satisfiability (SAT)

Introduction:

A Boolean-valued logic formula (predicate) is said to be Satisfiable (SAT) if a valid assignment (also known as a model) to the predicate variables exists that causes the formula to evaluate to TRUE.

Example 1:
- Predicate: P = (A ∧ ¬B)
- This predicate is satisfiable (SAT)
- Proof:
  - A = TRUE, B = FALSE
  - P = (TRUE ∧ ¬FALSE)
  - P = (TRUE ∧ TRUE)
  - P = TRUE

Example 2:
- Predicate: P = (A ∧ ¬A)
- This predicate is unsatisfiable (not SAT)
- Proof: Predicate variable A would have be both TRUE and FALSE simultaneously to make this predicate evaluate to TRUE. Therefore, this is predicate is unsatisfiable

Truth Table:

A common practice to find all possible states of a predicate is to build a truth table. This table represents all possible values for the predicate variables along with resultant Boolean values.

Predicate (A ∧ ¬B) ∨ C

Predicates (Boolean-valued functions) can be specified using Truth tables alone; rather than First-Order Logic.

Predicate: P(a,b)

Note: this predicate may also be specified using First-Order Logic as follows:
P = (A ∧ ¬B)

Conjunctive Normal Form (CNF)
- CNF is a conjunction (ANDs) of one or more predicates where the predicates are made up of disjunctions (ORs) predicates.
- Ex. (A ∨ B ∨ C) ∧ (D ∨ E ∨ F) ∧ (H ∨ I ∨ J)

Disjunction Normal Form (DNF)
- DNF is a disjunction (ORs) of one or more predicates where the predicates are made up of conjunctions (ANDs) predicates.
- Ex. (A ∧ B ∧ C) ∨ (D ∧ E ∧ F) ∨ (H ∧ I ∧ J)

Any propositional formula can be converted in CNF or DNF using the following logical equivalences: double negation elimination, De Morgan’s laws, and the distributive law.
This also means that CNF and DNF are interchangeable (one can be converted into the other) using the same logical equivalences.

Solver Algorithms:

Depth-First Search (DFS)
- DFS is a search algorithm for searching tree or graph data structure. DFS starts at the a root and explores a deep into a branch as possible before backtracking up the tree one level.
Breadth-First Search (BFS)
- BFS is a search algorithm for searching tree or graph data structure. BFS starts at the root and explores all of the neighbor nodes before proceeding down to the next layer in the tree.
Bounded Model Checking (BMC)
- BMC is a bounded-DFS approach. This is an iterative approach to DFS to K-depth with backtracking. If no SAT is found, then perform to (K+D)-depth and repeat; or stop when necessary. This approach prevents falling into the pitfalls of infinite loops.
Reduced-Order Binary Decision Diagrams (ROBDDs, or simply BBDs)
- ROBDDs are an approach to SAT (and reachable state-space representations). ROBDD procedure builds a compressed tree representation of predicate variable assignments and their results. It does this by selecting a predicate variable as a root node, building branches off of this node into variables; then merging isomorphic nodes (nodes representation the same variable with the same child nodes and results) and equivalent results (leaves).
Davis-Putnam-Logemann-Loveland (DPLL)
- DPLL (sometimes interchangeable with CNF-SAT) is a back-tracking search algorithm that utilizes conjunctive normal form (CNF). DPLL looks at all the CNF sub predicates (clauses), picks a predicate variable (literal) or its negation and assumed that its TRUE, compares the leftover sub predicates (clauses) that did not became true because of that assumption, removes the assigned predicate variable from the leftover sub predicates, then looks for conflicts among the other predicate variables of sub predicates (ex. Clause 1 = (A ∧ B), and Clause 2 = (¬A ∧ B), thus A is in conflict). If a conflict occurs, it backtracks and flips the previous variable assumption; if no conflict occurs, it picks a new variable assumption in the leftover sub predicates. This repeats until SAT is proven or not proven.

Depth-First Search (DFS):
- Predicate: (¬A ∧ B ∧ C )

Breath-First Search (BFS):
- Predicate: (¬A ∧ B ∧ C )

Bounded Model Checking (BMC):
- DFS to length K
- Predicate: (¬A ∧ B ∧ C )
- Ex. K = 2

Terminates as UNSAT!! (Its depth is too short never evaluates variable C, so it would terminate without prove SAT.)

Note: This is a little bit deceiving because this is not the true purpose of BMC. Usually, for BMC you search to the depth of the number of variables in the CNF (which is a standard DFS search). This is because your CNF would be created from a translation of your state transition system into CNF up to K time steps.

Bounded Model Checking (BMC):
- DFS to length K
- Predicate: (¬A ∧ B ∧ C )
- Ex. K = 3

Note: This is a little bit deceiving because this is not the true purpose of BMC. Usually, for BMC you search to the depth of the number of variables in the CNF (which is a standard DFS search). This is because your CNF would be created from a translation of your state transition system into CNF up to K time steps.

Unreduced Binary Decision Diagram:
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 1: Merge Isomorphic Subgraphs
  - Layer 3 – Process
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 1: Merge Isomorphic Subgraphs
  - Layer 3 – Result
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 2: Eliminate Nodes w/two Isomorphic Children
- Layer 2 – Process
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 2: Eliminate Nodes w/two Isomorphic Children
- Layer 2 – Result
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 1: Merge Isomorphic Nodes
- Layer 4 – Process
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 1: Merge Isomorphic Nodes
- Layer 3 – Result
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 2: Eliminate Nodes w/two Isomorphic Children
- Layer 3 – Process
- Predicate: (¬A ∧ B ∧ C )

Reduced-Order Binary Decision Diagram:
- Step 2: Eliminate Nodes w/two Isomorphic Children
  - Layer 3 – Result
  - FINAL RESULT
- Predicate: (¬A ∧ B ∧ C )

Note: Variable (node) ordering can affect the size of the ROBDD in larger predicates.

Davis-Putnam-Logemann-Loveland (DPLL)

Steps:

Choose a variable, R, from the CNF predicate, P, and assume it’s TRUE (preferably one that has a high multiplicity throughout the sub predicates). (Note: the negation of R could also be assumed true.)
Identify the sub predicates, Y, that DO NOT contain R.
- If Y is an empty set ∅, then terminate as SAT.
Remove from these sub predicate any references to ¬”R”.
Look for conflicts among the remaining variables of the predicates. (Example conflict is if one predicate only contained A, and another sub predicate only contained B.)
If a conflict exists to go back to step 1 and pick a variable, L, that you did not pick and assume it is TRUE (i.e. L ≠”R”). Then repeat steps 2 – 4.
- If no such variable exists, terminate as NOT SAT.
Repeat step 1 with, but pick a variable, T | (T ≠”R”), from Y, and assume it’s TRUE.
Repeat steps 2 to 6 with variable, T.

Example: CNF Predicate P: (¬A ∨ C ) ∧ (¬A ∨ B ∨ ¬C ) ∧ (A ∨ ¬B ∨ ¬C )

Assume A is TRUE
The sub predicate set P without A is Y = (¬A ∨ C ) ∧ (¬A ∨ B ∨ ¬C )
Remove ¬A from Y and get: (C) ∧ (B ∨ ¬C )
Assume B is TRUE
The sub predicate set Y without B is W = (C)
Assume C is TRUE
The sub predicate set W without B is the empty set, ∅
Therefore this predicate is SAT by A=1, B=1, C=1

There are other variants of the SAT problem:

MAJ-SAT
- The problem of finding out if the majority of all assignments make the predicate TRUE.
#SAT
- The problem of counting the number of variable assignments that make the predicate true.
UNIQUE-SAT
- The problem of determining if a predicate has exactly one assignment.
UNAMBIGUOUS-SAT
- A SAT problem when the formula’s given a guarantee that there is only one satisfying assignment.
MAX-SAT
- Find the Maximum number of sub predicates that can be satisfied by any assignment.
Etc…..