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