Zhang Y., Zhou K., Darwiche A. Dsat: A Native SAT Solver for Discrete Logic. To Appear at The International Conferences on Theory and Applications of Satisfiability Testing (SAT), 2026.
- Requires gmp installed on system. Uses C++ 20. Tested on Ubuntu with Clang 20 and GCC 14.2, and on MacOS with Clang 17.
- To build the executable and run on an example discrete CNF:
./run.sh discrete_json/10.json. - Input format: for the current version, the executable expects the input discrete CNF to be specified as json files. Some examples of are in
discrete_json/. The json file should be an object{"vars": [(1, var 1 cardinality), (2, var 2 cardinality), ...], "clauses": [...]}. Each clause is a list of literals, and each literal is specified as[var index, states bit array],e.g.,[3, "1288820281924011008"]. For compactness, the states bit array is specified as a positive number (quoted as a string because more than 64 bits may be needed to represent it). This discrete CNF file format is not relevant when using Dsat as a Python module (discussed below).
- Can be built as a Python module with the
BUILD_PYTHON_BINDINGSflag (requires pybind11). Seebindings/dsatpy.cppfor the exported interface, andtest.pyfor example usage.
- Also see https://github.com/victorzhangyf/dsat-scripts for some scripts used to benchmark Dsat.
- Implement dynamically sized bitarray. An array of unsigned long is current used to represent the bitarray of a literal, and
STATE_ARR_SZspecifies array size.