Satune: synthesizing efficient SAT encoders
Satune: synthesizing efficient SAT encoders
复制标题
DOI：
10.1145/3428214
复制
发表时间：
2020-11
影响因子：
--
通讯作者：
Hamed Gorjiara;G. Xu;Brian Demsky
中科院分区：
文献类型：
--
作者：
Hamed Gorjiara;G. Xu;Brian Demsky
现代SAT求解器在解决布尔可满足性问题方面非常有效，可以使用广泛的技术来检查，验证和验证真实世界的程序。不过，仍然具有挑战性的是如何对域问题进行编码（例如，模型检查）转换为SAT公式，因为同一个问题可能有多个不同的编码，这可能会产生数量级不同的性能结果，而不管使用的底层求解器。我们开发Satune，一个工具，可以自动合成SAT编码器为不同的问题域。Satune采用了一种DSL，允许开发人员在高层次上表达领域问题，并采用了一种搜索算法，可以有效地找到有效的解决方案。搜索过程由对示例编码及其域性能的观察指导，因此Satune可以通过结合来自示例的模式来快速合成高性能编码器，从而产生良好的性能。对JMCR、SyPet、Dirk、Hexiom、Sudoku和KillerSudoku的全面评估表明，Satune可以轻松地为不同的领域合成高性能编码器，包括模型检查、合成和游戏。这些编码器生成的约束问题通常比工具使用的原始编码快几个数量级。
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.