Satune: Synthesizing Efficient SAT Encoders
summary
Satune synthesizes and auto-tunes SAT encoders from a small sample of domain problems, providing a DSL for total and partial orders, integers and booleans, a pipeline of optimizations (order graph simplification, polarity analyses, vertex elimination) and a simulated annealing tuner that returns multiple complementary encoders. Evaluated on SyPet, Dirk, JMCR and puzzles using Z3, sat4j and glucose, it produces a 10x performance improvement on average and exposes graph-based encoding and Satune DSL for reuse.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:14Software Analysis Frameworks
- 0:44Using General-Purpose SAT Solvers
- 1:09Experiment on Different Encodings
- 1:31Encoding Challenges
- 2:12State of the Art
- 2:38Our Key Insight
- 3:43Satune's Domain-specific Language (DSL)
- 4:51Order Optimizations
- 7:52Graph-based Encoding
- 8:43Constraint Subgraph
- 9:47Encoding Graph
- 10:38Encoding - Example
- 11:06Tuner Framework
- 12:13Score-based Simulated Annealing
- 13:06Evaluation
- 13:32JMCR
related talks
35mA Peek Inside SAT Solvers
18mScalable Floating-Point Satisfiability via Staged Optimization
20mOptimal Program Synthesis via Abstract Interpretation
35mThe Mastermind behind Refinement Types
54mUse a Rust SAT Solver to play better pickleball!
15mEquality Saturation Theory Exploration à la Carte
31mLetting users do the undecidable: lessons from program synthesis
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)