Satune: synthesizing efficient SAT encoders
Abstract
Modern SAT solvers are extremely efficient at solving boolean satisfiability problems, enabling a wide spectrum of techniques for checking, verifying, and validating real-world programs. What remains challenging, though, is how to encode a domain problem (e.g., model checking) into a SAT formula because the same problem can have multiple distinct encodings, which can yield performance results that are orders-of-magnitude apart, regardless of the underlying solvers used. We develop Satune, a tool that can automatically synthesize SAT encoders for different problem domains. Satune employs a DSL that allows developers to express domain problems at a high level and a search algorithm that can effectively find efficient solutions. The search process is guided by observations made over example encodings and their performance for the domain and hence Satune can quickly synthesize a high-performance encoder by incorporating patterns from examples that yield good performance. A thorough evaluation with JMCR, SyPet, Dirk, Hexiom, Sudoku, and KillerSudoku demonstrates that Satune can easily synthesize high-performance encoders for different domains including model checking, synthesis, and games. These encoders generate constraint problems that are often several orders of magnitude faster to solve than the original encodings used by the tools.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Nov 13, 2020
- Source ID
- 10.1145/3428214
Entities
People
- Brian Demsky
- Guoqing Harry Xu
- Hamed Gorjiara
Organizations
- National Science Foundation
- Office of Naval Research
- University of California, Irvine
- University of California, Los Angeles