It provides solver implementations of various problems including SAT, SMT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic.
In particular it contains moderately-fast pure-Haskell SAT solver 'toysat'.
See INSTALL.md.
This package includes several commands.
Arithmetic solver for the following problems:
Usage:
toysolver [OPTION...] [file.lp|file.mps]
toysolver --lp [OPTION...] [file.lp|file.mps]
toysolver --sat [OPTION...] [file.cnf]
toysolver --pb [OPTION...] [file.opb]
toysolver --wbo [OPTION...] [file.wbo]
toysolver --maxsat [OPTION...] [file.cnf|file.wcnf]
-h --help show help
-v --version show version number
--solver=SOLVER mip (default), omega-test, cooper, cad, old-mip, ct
SAT-based solver for the following problems:
Usage:
toysat [file.cnf|-]
toysat --sat [file.cnf|-]
toysat --mus [file.gcnf|file.cnf|-]
toysat --pb [file.opb|-]
toysat --wbo [file.wbo|-]
toysat --maxsat [file.cnf|file.wcnf|-]
toysat --lp [file.lp|file.mps|-]
PB'12 competition result:
SMT solver based on toysat.
Usage:
toysmt [file.smt2]
Currently only QF_UF, QF_RDL, QF_LRA, QF_UFRDL and QF_UFLRA logic are supported.
SAT-based finite model finder for first order logic (FOL).
Usage:
toyfmf [file.tptp] [size]
Converter between various problem files.
Usage:
toyconvert -o [outputfile] [inputfile]
Supported formats: