SAT for Rustaceans
summary
Open-sourced SAT solver Resolvo implements CDCL-style solving for the Pixie package manager, reducing clause blowup with binary encoding (from gigabytes to practical sizes) and using two-literal watcher indexing and chunked arenas for fast lookups; a nonzero-u32 trick cuts memory by about 50%. Resolver exposes traits to support multiple packaging ecosystems, offers a single code path that marries sync and async via a pluggable block_on runtime, and is production-ready and available on GitHub.
AI-written summary · about
chapters (8)
- 0:00Introduction and context
- 2:45The package management problem
- 6:01Introduction to SAT solvers
- 9:39Boolean logic basics
- 12:34Encoding package rules
- 17:00How CDCL solvers work
- 24:04Optimizations and patterns
- 35:42Closing and Q&A
related talks
54mUse a Rust SAT Solver to play better pickleball!
29mBridging the worlds: pixi reimplements pip and conda in Rust
40mRust’s approach of getting things right
31mBuilding an extremely fast Python package manager, in Rust
19mRavencheck: Effectively-Propositional Reasoning for Rust
19mSuki: Choreographed Distributed Dataflow in Rust
56mRust for Safe and Scalable Automotive: Insights from
25m"Eternal Sunshine of the Rustfmt'ed Mind"