What is Boolean Satisfiability?
The Boolean Satisfiability Problem (SAT) asks: Given a Boolean formula in propositional logic, does there exist an assignment of truth values to its variables that makes the formula evaluate to true?
For example, consider the formula: (x₁ ∨ ¬x₂) ∧ (x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃)
Can we find values for x₁, x₂, x₃ that satisfy all three clauses simultaneously?
Why SAT Matters
Despite being NP-complete (believed to be computationally hard), SAT solving has become incredibly practical because:
- Wide Applicability: Many problems can be encoded as SAT
- Modern Solvers: State-of-the-art solvers can handle millions of variables
- Average-Case Performance: Most instances are solvable quickly despite worst-case hardness
- Hardware Verification: Essential for checking chip designs
Normal Forms for SAT
Conjunctive Normal Form (CNF)
CNF is the standard form for SAT solvers. It's a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals.
Example: (a ∨ ¬b ∨ c) ∧ (¬a ∨ d) ∧ (b ∨ ¬d)
Each clause is called a k-SAT clause if it contains k literals. 3-SAT is NP-complete, while 2-SAT is solvable in polynomial time.
Key SAT Solving Algorithms
DPLL Algorithm (Davis-Putnam-Logemann-Loveland)
The foundation of modern SAT solvers, DPLL uses:
- Unit Propagation: If a clause has only one unassigned literal, assign it to satisfy the clause
- Pure Literal Elimination: If a literal appears only in one polarity, assign it to true
- Backtracking: When a conflict occurs, backtrack to explore other branches
Conflict-Driven Clause Learning (CDCL)
Modern SAT solvers enhance DPLL with:
- Clause Learning: Learn new clauses from conflicts to prune search space
- Non-Chronological Backtracking: Jump back multiple levels when conflicts are detected
- Restart Heuristics: Periodically restart with learned clauses
- Variable Selection Heuristics: Choose branch variables intelligently
Practical SAT Solvers
Widely Used Solvers
- MiniSat: Influential open-source solver, basis for many modern solvers
- Glucose: Focus on clause learning and restart strategies
- Lingeling: High performance, competitive in SAT competitions
- CaDiCaL: Recent solver with strong empirical results
- Kissat: Modern solver with advanced techniques
Applications of SAT Solving
Hardware Verification
Checking that hardware designs satisfy specifications by encoding verification conditions as SAT problems.
Software Verification
Proving program correctness by converting verification goals to SAT instances.
Planning and Scheduling
Solving planning problems by encoding them as satisfiability problems.
Cryptanalysis
Finding key collisions and analyzing cryptographic algorithms.
Bounded Model Checking
Verifying system properties up to a bounded number of steps.
Encoding Problems as SAT
To use SAT solvers, we must encode our problem as a Boolean formula. Example: Graph 3-coloring
- Variables: For each node n and color c, variable x_{n,c} = true if node n has color c
- Constraints: Each node gets exactly one color, adjacent nodes have different colors
Limitations and Challenges
- Encoding Overhead: Problem encoding can create large formulas
- Symmetry: Many problems have symmetries that SAT solvers may not exploit
- Randomness: Performance can vary significantly based on random choices
- Theory Integration: Reasoning about arithmetic requires extensions like SMT
Next Steps
Building on SAT solving foundations, the next part explores SMT (Satisfiability Modulo Theories) solvers, which extend SAT with reasoning about mathematical theories like arithmetic and data structures.