Reasoning Under Uncertainty in SMT Solving, Research, and Life
summary
Argues that SMT progress rests on practical abstractions and shows how modern CDCL solvers actually work: CDCL (simplify, decide, learn) with unit clause / BCP propagation, conflict analysis that emits a learned clause plus a backtrack level, and heuristics for decisions. Gives concrete history: lattice-based data structures proved and implemented in Haskell, a non‑invasive Julia DSL that runs faster than plain Julia, time to publish taking three or four attempts, and SAT scaling from thousands to millions of clauses. Proposes building domain‑specific solvers (CASTLE) for distributed consistency.
AI-written summary · about
chapters (12)
- 0:00Start
- 4:53The Programming Language Design Space
- 5:41High-Performance Domain-Specific Languages
- 13:38How Hard Is the Sat Problem
- 16:04The Decide Phase
- 17:03Conflict Driven Clause Learning
- 17:45Simplify Phase
- 19:02Unit Clause Rule
- 27:14Analyze the Conflict
- 27:43Conflict Clause
- 28:46Backtracking Level
- 33:52When To Give Up and When To Try Again
related talks
35mThe Mastermind behind Refinement Types
35mA Peek Inside SAT Solvers
15mInter-theory Dependency Analysis for SMT String Solvers
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
32mReasoning About Hilbert’s Choice Operator in SMT
58mInvited Talk: Solvers, unite! A simple unified semantics for reasoning with assurance(…)
30mAnalyzing Programs with SMT Solvers
21mMassive proofs for the masses