The toysolver package

[Tags: bsd3, library, program]

Toy-level implementation of some decision procedures


[Skip to ReadMe]

Properties

Versions0.0.2, 0.0.3, 0.0.4, 0.0.4.1, 0.0.5, 0.0.6, 0.1.0, 0.2.0, 0.3.0, 0.4.0
Change logCHANGELOG.markdown
Dependenciesarray (>=0.4.0.0), base (>=4.6 && <5), bytestring (>=0.9.2.1 && <0.11), bytestring-builder, containers (>=0.5.0), data-default-class, data-interval (>=1.0.1 && <1.3.0), deepseq, exceptions (==0.5 || >=0.6), extended-reals (>=0.1 && <1.0), filepath, finite-field (>=0.7.0 && <1.0.0), ghc-prim, hashable (>=1.1.2.5 && <1.3.0.0), haskeline (==0.7.*), heaps, intern (>=0.9.1.2 && <1.0.0.0), loop (>=0.2.0 && <1.0.0), MemoTrie (<=0.6.2), mtl (>=2.1.2), multiset, mwc-random (>=0.13.1 && <0.14), old-locale, OptDir, parse-dimacs, parsec (>=3.1.2 && <4), prettyclass (>=1.0.0), primes, process (>=1.1.0.2), pseudo-boolean (>=0.1.3.0 && <0.2.0.0), queue, semigroups (>=0.17), sign (>=0.2.0 && <1.0.0), split, stm (>=2.3), template-haskell, temporary (>=1.2), time, toysolver, transformers (>=0.2), transformers-compat (>=0.3), type-level-numbers (>=0.1.1.0 && <0.2.0.0), unbounded-delays, unordered-containers (>=0.2.3 && <0.3.0), vector, vector-space (>=0.8.6) [details]
LicenseBSD3
AuthorMasahiro Sakai (masahiro.sakai@gmail.com)
Maintainermasahiro.sakai@gmail.com
CategoryAlgorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic
Bug trackerhttps://github.com/msakai/toysolver/issues
Source repositoryhead: git clone git://github.com/msakai/toysolver.git
Executablespbverify, maxsatverify, pigeonhole, svm2lp, htc, knapsack, nqueens, nonogram, sudoku, pbconvert, lpconvert, toyfmf, toysmt, toysat, toysolver
UploadedMon Jan 25 13:10:40 UTC 2016 by MasahiroSakai
DistributionsNixOS:0.4.0
Downloads1409 total (43 in last 30 days)
Votes
0 []
StatusDocs pending
Build status unknown [no reports yet]

Modules

Flags

NameDescriptionDefaultType
forcechar8set default encoding to char8 (not to use iconv)DisabledManual
linuxstaticbuild statically linked binariesDisabledManual
buildtoyfmfbuild toyfmf commandDisabledManual
buildsampleprogramsbuild sample programsDisabledManual
buildmiscprogramsbuild misc programsDisabledManual
exceptions06use exceptions >=0.6EnabledAutomatic
time15use time >=1.5.0EnabledAutomatic
transformers051use transformers >=0.5.1EnabledAutomatic
usehaskelineuse haskeline packageEnabledManual

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for toysolver-0.4.0

toysolver

Join the chat at <a href="https://gitter.im/msakai/toysolver">https://gitter.im/msakai/toysolver</a>

Build Status Build status Coverage Status Hackage

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

Usage

This package includes several commands.

toysolver

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

toysat

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:

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]

lpconvert

Converter between LP/MIP/SAT-related formats

Usage:

lpconvert -o [outputfile] [inputfile]

Supported formats:

pbconvert

Converter between SAT/PB-related formats

Usage:

pbconvert -o [outputfile] [inputfile]

Supported formats:

Bindings

TODO