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