8. SAT Heuristics and Synthesis
Historical Materialist Hook
[RESEARCH REQUIRED: Conclude the historical arc by evaluating how DPLL and CDCL heuristics navigate immense state spaces, acting as algorithmic proxies for administrative planning.]
Core Technical Synthesis
[RESEARCH REQUIRED: Explain how DPLL and modern CDCL heuristics dynamically navigate massive state spaces to find valid variable assignments. Introduce the final SAT Solver Challenge: isolating structural constraints from a combinatorial puzzle and translating them into DIMACS CNF for computational verification.]
Guided Example: The SAT Solver Challenge
The Problem: You must schedule three workers (A, B, C) across two shifts (1, 2). Constraints: 1. Every worker must work exactly one shift. 2. Worker A cannot work the same shift as Worker B.
You will translate these constraints into propositional logic, normalize them to CNF, generate the DIMACS mapping, and execute the solution using an online SAT solver.
Problem Set
Final Project: The SAT Solver Challenge
Document your entire workflow for the SAT Solver Challenge. List the formal constraints, your CNF normalization steps, the final DIMACS file content, and the verified model output from the SAT solver.
Dictionary Reference Map
- For DPLL and CDCL heuristics: Logic in Computer Science (Huth & Ryan 2004, Sec. 1.5.3–1.6.2)
- For advanced SAT solving techniques: Handbook of Satisfiability (Biere et al. 2021, Sec. 3.2)