Satune

Satune: Synthesizing Efficient SAT Encoders

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.

Getting Started

If you haven’t done so already, you may download SATune using git:

  git clone git://plrg.ics.uci.edu/satune.git
  git checkout incremental

Get the SAT solver library:

  git clone git://plrg.ics.uci.edu/satlib.git

You can build any SAT solvers and use it with Satune. For example, you may build Glucose and rename the execution file to ‘sat_solver’, so it can be used by Satune. Here is how it can be done:

cd satlib/glucose-syrup/incremental
make
mv glucose /path/to/satune/src/sat_solver

Then build Satune and run the test cases after

cd satune/src
./Scripts/setup.sh
cd bin
./run.sh elemequalunsattest

Disclaimer

We make no warranties that Satune is free of errors. Please read the paper and the documentation file so that you understand what the tool is supposed to do.

Contact

Please feel free to contact us for more information. Bug reports are welcome, and we are happy to hear from our users.

Contact Hamed Gorjiara at hgorjiar@uci.edu or Brian Demsky at bdemsky@uci.edu for questions about Satune.

Copyright

Copyright © 2020 Regents of the University of California. All rights reserved.

Acknowledgments

This work is supported by the National Science Foundation grants CNS-1703598, OAC-1740210, CNS-1703598, CNS-1763172, CCF-2006948, CNS-2007737, and CNS-2006437, as well as Office of Naval Research grants N00014-16-1-2913 and N00014-18-1-2037.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.