Popularity
9.3
Growing
Activity
7.8
Growing
118
11
9

Monthly Downloads: 7
Programming language: Haskell
License: BSD 3-clause "New" or "Revised" License
Latest version: v0.6.0

toysolver alternatives and similar packages

Based on the "Algorithms" category

Do you think we are missing an alternative of toysolver or a related project?

Add another 'Algorithms' Package

README

toysolver

Join the chat at https://gitter.im/msakai/toysolver

Build Status (Travis CI) Build Status (AppVeyor) Coverage Status Hackage Hackage Deps License

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'.

Installation

  • unpack
  • cd toysolver
  • cabal install

Usage

This package includes several commands.

toysolver

Arithmetic solver for the following problems:

  • Mixed Integer Liner 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 --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

toysat

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 --lp [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

toysmt

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.

toyfmf

SAT-based finite model finder for first order logic (FOL).

Usage:

toyfmf [file.tptp] [size]

toyconvert

Converter between various problem files.

Usage:

toyconvert -o [outputfile] [inputfile]

Supported formats:

  • Input formats: .cnf .wcnf .opb .wbo .gcnf .lp .mps
  • Output formats: .cnf .wcnf .opb .wbo .lsp .lp .mps .smp .smt2 .ys

Bindings


*Note that all licence references and agreements mentioned in the toysolver README section above are relevant to that project's source code only.