Scalable Floating-Point Satisfiability via Staged Optimization
summary
StageSAT reframes floating-point SAT as three optimization stages: a fast projection-aided square residuals descent to find a trustworthy basin, a bit-precise ULP^2 continuous optimizer, and an n-ULP lattice refinement that tweaks integer ULP offsets. Implementation runs on SMT-COMP'25 and prior benchmarks, solving 439/443 cases on the largest suite, achieving 99.4% recall with 0% false SAT, often 5–10× faster than bit-precise SMT solvers, and ships with evaluated, reusable artifacts.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:57SMT solver challenges
- 3:03Toy example: objective function
- 4:07Three-stage optimization pipeline
- 8:21Stage two: bit-level correctness
- 9:03Stage three: lattice search for near misses
- 10:27Overall procedure and certification
- 11:29Evaluation results
- 13:57Timeout rates and set recall
- 14:17Conclusion and future directions
- 14:39Q&A
related talks
19mSolving Floating-Point Constraints with Continuous Optimization
19mSMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
13mProgram Analysis via Efficient Symbolic Abstraction
35mA Peek Inside SAT Solvers
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
15mSatune: Synthesizing Efficient SAT Encoders
17mSatisfiability Algorithms Based on Concentrated Shrinkage
40mReasoning Under Uncertainty in SMT Solving, Research, and Life