Hackage:

Dev:

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 a moderately fast pure-Haskell SAT solver toysat.

See INSTALL.md.

This package includes several commands.

Arithmetic solver for the following problems:

• Mixed Integer Linear Programming (MILP or MIP)
• Boolean SATisfiability problem (SAT)
• PB
  • Pseudo-Boolean Satisfaction (PBS)
  • Pseudo-Boolean Optimization (PBO)
  • Weighted Boolean Optimization (WBO)
• Max-SAT families
  • Max-SAT
  • Partial Max-SAT
  • Weighted Max-SAT
  • Weighted Partial Max-SAT
• Real Closed Field

Usage:

toysolver [OPTION...] [file.lp|file.mps] toysolver --mip [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:

• SAT
  • Boolean SATisfiability problem (SAT)
  • Minimally Unsatisfiable Subset (MUS)
  • Group-Oriented MUS (GMUS)
• PB
  • Pseudo-Boolean Satisfaction (PBS)
  • Pseudo-Boolean Optimization (PBO)
  • Weighted Boolean Optimization (WBO)
• Max-SAT families
  • Max-SAT
  • Partial Max-SAT
  • Weighted Max-SAT
  • Weighted Partial Max-SAT
• Integer Programming (all variables must be bounded)

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 --mip [file.lp|file.mps|-] 

PB'12 competition result:

• toysat placed 2nd in PARTIAL-BIGINT-LIN and SOFT-BIGINT-LIN categories
• toysat placed 4th in PARTIAL-SMALLINT-LIN and SOFT-SMALLINT-LIN categories
• toysat placed 8th in OPT-BIGINT-LIN category

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:

Solution checker for various problem files. Usage:

toysolver-check [OPTION...] [problem_file] [solution_file] toysolver-check --mip [OPTION...] [file.lp|file.mps] [file.sol] toysolver-check --sat [OPTION...] [file.cnf] [file.log] toysolver-check --pb [OPTION...] [file.opb] [file.log] toysolver-check --wbo [OPTION...] [file.wbo] [file.log] toysolver-check --maxsat [OPTION...] [file.cnf|file.wcnf] [file.log] --encoding ENCODING file encoding for LP/MPS files --pb-fast-parser use attoparsec-based parser instead of megaparsec-based one for speed --tol-integrality REAL If a value of integer variable is within this amount from its nearest integer, it is considered feasible. (default: 1.0e-5) --tol-feasibility REAL If the amount of violation of constraints is within this amount, it is considered feasible. (default: 1.0e-6) --tol-optimality REAL Feasibility tolerance of dual constraints. (default: 1.0e-6) 

• ersatz-toysat - toysat backend driver for ersatz
• satchmo-toysat - toysat backend driver for satchmo

• bytestring-encoding
• data-interval
• extended-reals
• finite-field
• MIP
• OptDir
• pseudo-boolean
• sign