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
Change logNone available
Dependenciesarray, base (>=4.4 && <5), bytestring, containers (>=0.4.2), data-interval (>=0.1.0), deepseq, filepath, heaps, lattices (>=1.2.1.1), logic-TPTP, mtl, old-locale, OptDir, parse-dimacs, parsec, primes, queue, random, stm (>=2.3), time, toysolver, unbounded-delays, vector-space (>=0.8.6) [details]
LicenseBSD3
AuthorMasahiro Sakai (masahiro.sakai@gmail.com)
Maintainermasahiro.sakai@gmail.com
CategoryAlgorithms, Optimisation, Optimization
Bug trackerhttps://github.com/msakai/toysolver/issues
Source repositoryhead: git clone git://github.com/msakai/toysolver.git
Executablespbconvert, lpconvert, toyfmf, toysat, toysolver
UploadedThu Apr 11 23:11:42 UTC 2013 by MasahiroSakai
DistributionsNixOS:0.3.0
Downloads1148 total (50 in last 30 days)
Votes
0 []
StatusDocs not available [build log]
All reported builds failed as of 2015-06-09 [all 2 reports]

Modules

Flags

NameDescriptionDefaultType
forcechar8set default encoding to char8 (not to use iconv)DisabledAutomatic

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

toysolver

Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc.

Installation

Usage

This package includes several commands.

toysolver

Arithmetic solver for the following problems:

Usage: toysolver [OPTION...] file.lp

-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 --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:

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 <outputile> <inputfile>

Supported formats:

pbconvert

Converter between SAT/PB-related formats

Usage:

pbconvert -o <outputile> <inputfile>

Supported formats:

TODO