The toysolver package

[Tags:bsd3, library, program]

Toy-level implementation of some decision procedures


[Skip to Readme]

Properties

Versions 0.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
Dependencies array, base (==4.*), bytestring, containers (>=0.4.2), deepseq, filepath, mtl, old-locale, OptDir, parse-dimacs, parsec, queue, random, stm (>=2.3), time [details]
License BSD3
Author Masahiro Sakai (masahiro.sakai@gmail.com)
Maintainer masahiro.sakai@gmail.com
Stability Unknown
Category Algorithms
Bug tracker https://github.com/msakai/toysolver/issues
Source repository head: git clone git://github.com/msakai/toysolver.git
Uploaded Thu Sep 27 23:12:02 UTC 2012 by MasahiroSakai
Distributions NixOS:0.4.0
Downloads 1554 total (32 in the last 30 days)
Votes
0 []
Status Docs not available [build log]
All reported builds failed as of 2015-11-25 [all 5 reports]

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

Maintainer's Corner

For package maintainers and hackage trustees

Readme for toysolver

Readme for toysolver-0.0.2

toysolver

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)
  • LA(Q), LA(Z) (NOT IMPLEMENTED YET)

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

-h  --help           show help
-v  --version        show version number
    --solver=SOLVER  mip (default), omega-test, cooper, old-mip

toysat

SAT-based solver for the following problems:

  • SAT
  • PB
    • Pseudo Boolean Satisfaction (PBS)
    • Pseudo Boolean Optimization (PBO)
    • Weighted Boolean Optimization (WBO)
  • Max-SAT
  • Integer Programming (all variables must be bounded)

Usage:

toysat [file.cnf||-]
toysat --pb [file.opb|-]
toysat --wbo [file.wbo|-]
toysat --maxsat [file.cnf|file.wcnf|-]
toysat --lp [file.lp|-]

lp2yices

Converter from LP file to Yices input file.

Usage: lp2yice [file.lp|-]

-h  --help      show help
    --optimize  output optimiality condition which uses quantifiers
    --no-check  do not output "(check)"

cnf2lp

Converter from DIMACS .cnf file to .lp file.

Usage: cnf2lp [file.cnf|-]

maxsat2lp

Converter from .cnf/.wcnf file to .lp file.

Usage: maxsat2lp [file.cnf|file.wcnf|-]

pb2lp

Converter from .opb/.wbo file to .lp file.

Usage: pb2lp [--wbo] [file.opb|file.wbo|-]

TODO

  • Gröbner basis
  • Cylindrical algebraic decomposition
  • Local search
  • Suvery propagation