Massive proofs for the masses
summary
Claims that cloud-backed distributed solvers dramatically outperform sequential tools—example: a distributed solver reaches ~250 benchmarks solved within 200s versus ~100 for older tools—by running Amazon Trusted Solver (ATS) jobs that spawn many instances and use CVC5 and Z3 in portfolio mode, clause-sharing over a bus (malib), and cube-and-conquer style cubing. Techniques include eager translation to SAT for some theories, storing and reusing lemmas, synthesizing tuned local heuristics from distributed runs, precomputing string complements on burn‑in datacenters, and trading cost for much shorter proofs.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:29Automated reasoning at AWS
- 5:39Trusted Solver service overview
- 8:10Distributed solvers challenges
- 10:38Distributed reasoning ingredients
- 13:50Cost and efficiency of solving
- 16:17Hard domains like strings and quantifiers
- 18:28Q&A
related talks
35mA Peek Inside SAT Solvers
19mSol: Fast Distributed Computation Over Slow Networks
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
22mDIZK: A Distributed Zero Knowledge Proof System
15mInter-theory Dependency Analysis for SMT String Solvers
57mResearch on Different Time Horizons (and an Example with Machine-Checked Proofs)
27mProducing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective