The prototype Stochastic Boolean satisfiability solver based on quantifier elimination.
- pybind11
- For building the python binding of
UniqueforManthan.
- For building the python binding of
- Boost Library
- Require for
Unique.
- Require for
- We give a script for installing and compiling dependencies. Use the following command.
./build.sh
- The solver is built in the abc system as a command. To execute the solver, use the following command.
./abc -q "ssat" <sdimacs>
-
We provide three toy cases for testing purpose. You can found them in
benchmarkfolder. -
The full benchmarks can be found in the repository of ClauSSAT.
If you have any problems or suggestions, feel free to create an issue or contact us through r09943108@ntu.edu.tw.