CDCL SAT Solving and Applications to Optimization Problems
summary
Concise primer on CDCL specifics (GRASP vs Chaff, two-watched literals, BCP internals, first-UIP clause conflict extraction and the tradeoff between chronological and non‑chronological backtracking) followed by a concrete optimizer: the Polosat algorithm queries a black‑box objective under SAT assumptions, uses polarity‑biasing and conflict thresholds, and is deployed in Intel’s cell‑placement flow where it produces a measurable capacity improvement and serves inside NuWLS‑c, winner of MaxSAT Evaluation 2022 incomplete categories.
AI-written summary · about
chapters (10)
- 0:00CDCL SAT solving intro
- 4:22DPLL to CDCL SAT solvers
- 10:25Boolean constraint propagation
- 19:10Conflict analysis in CDCL
- 26:41Modern CDCL solver improvements
- 28:36Optimization with SAT solvers
- 31:14Polosat for black-box optimization
- 37:19Industrial cell placement optimization
- 45:19Future of SAT in non-linear optimization
- 48:16Q&A
related talks
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
34mAbstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
24mBuilding Information Modeling Using Constraint Logic Programming (Extended Ab...
36mSpecification-Guided Component-Based Synthesis from Effectful Libraries
28mBounded Model Checking of PLC ST Programs using Rewriting Modulo SMT
40mUtilizing Structure in Combinatorial Solving and Reasoning
30mUnconstrained Variable Oracles for Faster Static Analyses