CS292C-5: Computer-Aided Reasoning for Software
Lecture 5: SAT Basics: CNF & DPLL.

by Yu Feng

Outline
Understand SAT Foundations
Learn propositional logic and Conjunctive Normal Form (CNF)
Master Formula Transformation
Explore NNF, CNF, and Tseitin transformation techniques
Implement DPLL Algorithm
Study unit propagation and practical SAT solving
Apply to Verification
Connect SAT solving to program analysis and verification
Why SAT Matters
Core Technology
SAT is the foundation for SMT, program analysis, synthesis, and model checking.
Powerful Solvers
Modern SAT solvers efficiently handle millions of variables.
Practical Applications
Understanding SAT enables implementation of verification tools.
Propositional Logic Syntax
Atoms
Basic proposition variables (p, q, r...) that represent atomic statements which can be either true or false.
Literals
An atom (p) or its negation (¬p). Literals are the basic building blocks of logical formulas.
Formulas
Expressions built from atoms using connectives:
  • F ::= ⊤ | ⊥ | p
  • F ::= ¬F
  • F ::= F ∧ F | F ∨ F
  • F ::= F → F | F ⇔ F
where ⊤ is true, ⊥ is false, p is an atom.
Propositional Logic Semantics
Interpretation
An interpretation I maps each atom to true or false.
Satisfaction
I ⊨ F means F is true under interpretation I.
Evaluation
Apply truth table rules to determine if formula is satisfied.
Truth Table Example
For I = {p ↦ true, q ↦ false}, we evaluate (p ∧ q) → (p ∨ ¬q).
Since p is true and q is false, (p ∧ q) is false and (p ∨ ¬q) is true.
Therefore, I ⊨ F (the formula is satisfied).
Validity vs. Satisfiability
Satisfiability
A formula is satisfiable if there exists at least one interpretation I under which the formula evaluates to true.
Example: p ∨ q is satisfiable because it's true when p is true, q is true, or both are true.
Non-example: p ∧ ¬p is unsatisfiable (never true).
Validity
A formula is valid (a tautology) if it evaluates to true under every possible interpretation I.
Example: p ∨ ¬p is valid because it's true regardless of p's value.
Non-example: p ∧ q is not valid (not always true).
Duality of satisfiability and validity: F is valid ⇔ ¬F is unsatisfiable
Why Normal Forms?

Solver Compatibility
SAT solvers require specific input formats
Standardization
Uniform representation simplifies algorithms
Optimization
Enables efficient implementation techniques
SAT solvers operate specifically on ???. Understanding and converting formulas efficiently is essential for practical applications.
Negation Normal Form (NNF)
Limited Operators
Only uses ¬, ∧, and ∨ connectives
Negation Placement
Negation (¬) only appears directly on atoms
Transformation Method
Apply DeMorgan's Laws to push negations down
Example: ¬(p ∧ q) becomes (¬p ∨ ¬q) in NNF
Disjunctive Normal Form (DNF)
DNF grammar: F ::= C₁ ∨ C₂ ∨ ... ∨ Cₙ where each C is a conjunction of literals
Structure
OR of ANDs: (a ∧ b) ∨ (¬c ∧ d)
Converting to DNF
First transform to NNF, then distribute ∧ over ∨: (F∧(G∨H)) ⟺ (F∧G)∨(F∧H)
Advantage
Easy for SAT: just find one satisfying conjunction
Disadvantage
Huge size explosion makes it impractical for complex formulas
Conjunctive Normal Form (CNF)
CNF grammar: F ::= C₁ ∧ C₂ ∧ ... ∧ Cₙ where each C is a disjunction of literals
Structure
AND of ORs: (a ∨ b) ∧ (¬c ∨ d) ∧ (e ∨ ¬f ∨ g)
Clauses
Each clause is a disjunction (OR) of literals
Literals
Variables or their negations (e.g., x or ¬x)
Requirements
Formula must be a conjunction (AND) of clauses
To obtain CNF, first transform to NNF, then distribute ∨ over ∧: (F ∨ (G ∧ H)) ⟺ (F ∨ G) ∧ (F ∨ H)
Conjunctive Normal Form Is The Standard
AND of ORs
(a ∨ b) ∧ (¬c ∨ d)
Industry Standard
Used by all SAT solvers
Conversion Challenge
Direct conversion can cause size explosion
Solution
Tseitin transformation
From Satisfiability to Equisatisfiability
Equisatisfiability
Formulas F and G are equisatisfiable if they are both satisfiable or they are both unsatisfiable.
Tseitin's transformation converts a propositional formula F into an equisatisfiable CNF formula that is linear in the size of F.
The Problem & Solution
Converting to CNF can cause exponential growth in formula size. Example: (a ∨ (b ∧ c)) would expand to a much larger CNF.
Tseitin introduces new variables to represent subformulas, keeping the CNF size linear relative to the original formula.
Tseitin Transformation Example
Original Formula
F = x → (y ∧ z)
New Variables
a1 ↔ (x → a2), a2 ↔ (y ∧ z)
Convert to CNF
Convert equivalences to clauses
Final Result
¬a1 ∨ ¬x ∨ a2
¬a2 ∨ y
¬a2 ∨ z
¬y ∨ ¬z ∨ a2
Tseitin Benefits
O(n)
Linear Size
CNF size grows linearly with original formula
100%
Preservation
Preserves equisatisfiability
1962
Historical Impact
Breakthrough in efficient SAT solving
While Tseitin preserves equisatisfiability, it does not maintain logical equivalence due to the introduction of new variables.
Resolution Rule
Resolution eliminates variables by combining clauses with complementary literals. This fundamental rule enables logical deduction in SAT solvers.
Formal Definition
From clauses containing complementary literals:
(α ∨ β) and (¬β ∨ γ)
―――――――――――――――――――――
         α ∨ γ
Purpose
Derive new consequences by eliminating variables from existing clauses. Enables proof by contradiction when deriving empty clause.
3
Foundation
Basis for many SAT solving techniques including DPLL algorithm. Central to conflict-driven clause learning in modern solvers.
Unit Resolution
Unit resolution is a special case of the resolution rule that efficiently prunes the search space by deducing variable assignments without guessing.
General Resolution Rule
(α ∨ β)    (¬β ∨ γ)
―――――――――――――――――
      α ∨ γ
Unit Resolution Rule
(x)    (¬x ∨ y₁ ∨ ... ∨ yₙ)
―――――――――――――――――――――――
      (y₁ ∨ ... ∨ yₙ)
When one clause is a unit clause (containing only one literal), we can directly infer the remaining literals, eliminating variables by combining clauses with complementary literals.
Unit Clause
A clause with only one literal (e.g., x)
Propagation
If x is true, remove all ¬x from other clauses
Iteration
Repeat until no more unit clauses can be applied
DPLL Algorithm
Simplify
Apply unit propagation (BCP)
Check
If formula is satisfied or unsatisfiable, return result
Choose
Select a variable to assign
4
4
Recurse
Try both true and false assignments recursively
DPLL (Davis–Putnam–Logemann–Loveland, 1962) combines recursive backtracking with unit propagation for efficient SAT solving.
DPLL Pseudocode
DPLL(F):
  F ← BCP(F)
  if F = ⊤ return true
  if F = ⊥ return false
  p ← choose variable
  return DPLL(F[p := true]) || DPLL(F[p := false])
BCP (Boolean Constraint Propagation) repeatedly applies unit resolution until reaching a fixpoint.
The algorithm tries both values for each variable, backtracking when necessary.
DPLL Example Walkthrough
Initial
(x ∨ y) ∧ (¬z ∨ w) ∧ (¬y ∨ z)
Choose
No unit clauses; Try x = false
Simplify
Formula: (y) ∧ (¬z ∨ w) ∧ (¬y ∨ z)
Propagate
Formula: (¬z ∨ w) ∧ (z)
Formula: w
Result
SAT: x = false, y = true, z = true, w = true
CNF Format for SAT Solvers
DIMACS CNF is the standard format for representing Boolean formulas used by SAT solvers.
File Structure
  • Header: "p cnf [variables] [clauses]"
  • Comments: Lines starting with 'c'
  • Clauses: Lists of literals ending with 0
Variable Representation
  • Positive integers for variables
  • Negative numbers for negated variables
  • 0 marks the end of each clause
Example
c Example CNF file
p cnf 3 2
1 -2 0
3 0
Formula: (x₁ ∨ ¬x₂) ∧ (x₃)
This format ensures interoperability between SAT solvers, benchmarking tools, and research implementations.
Use Cases of SAT
Solving puzzles
Encoding logic puzzles like Sudoku or cryptarithmetic problems as Boolean formulas that can be efficiently solved by SAT solvers.
Bounded model checking
Verifying finite-state systems by encoding the system behavior and properties as Boolean formulas to find potential errors.
Symbolic execution
Exploring multiple program paths simultaneously by representing program states symbolically to detect bugs and vulnerabilities.
Constraint-based synthesis
Automatically generating programs or designs that satisfy a given specification by encoding constraints as SAT problems.
What's Next
Implement a SAT solver (Homework 2)
Build your own implementation of a satisfiability solver based on the algorithms we've discussed.
Extend to symbolic execution and VC solving
Apply SAT solving techniques to more complex verification challenges through symbolic execution.
Prepare for SMT (next week!)
Read ahead on Satisfiability Modulo Theories as we expand beyond pure Boolean satisfiability.