toysolver: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

[ algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers ] [ Propose Tags ] [ Report a vulnerability ]

Toy-level implementation of some decision procedures

[Skip to Readme]

Modules

[Index]

ToySolver

Flags

Manual Flags

Name	Description	Default
forcechar8	set default encoding to char8 (not to use iconv)	Disabled
linuxstatic	build statically linked binaries	Disabled
buildtoyfmf	build toyfmf command	Disabled
buildsampleprograms	build sample programs	Disabled
buildmiscprograms	build misc programs	Disabled
usehaskeline	use haskeline package	Enabled

Automatic Flags

Name	Description	Default
exceptions06	use exceptions >=0.6	Enabled
time15	use time >=1.5.0	Enabled
transformers051	use transformers >=0.5.1	Enabled

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

Downloads

toysolver-0.4.0.tar.gz [browse] (Cabal source package)
Package description (revised from the package)

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

MasahiroSakai

For package maintainers and hackage trustees

edit package information

Candidates

0.1.0, 0.2.0, 0.3.0

Versions [RSS]	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, 0.5.0, 0.6.0, 0.7.0, 0.8.0, 0.8.1
Change log	CHANGELOG.markdown
Dependencies	array (>=0.4.0.0), base (>=4.6 && <4.11), 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 && <0.9.0), ghc-prim, hashable (>=1.1.2.5 && <1.3.0.0), haskeline (>=0.7 && <0.8), 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]
Tested with	ghc ==7.6.3, ghc ==7.8.3, ghc ==7.10.3
License	BSD-3-Clause
Author	Masahiro Sakai (masahiro.sakai@gmail.com)
Maintainer	masahiro.sakai@gmail.com
Revised	Revision 2 made by sjakobi at 2021-11-18T02:56:50Z
Category	Algorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic
Bug tracker	https://github.com/msakai/toysolver/issues
Source repo	head: git clone git://github.com/msakai/toysolver.git
Uploaded	by MasahiroSakai at 2016-01-25T13:10:40Z
Distributions
Reverse Dependencies	4 direct, 0 indirect [details]
Executables	pbverify, maxsatverify, pigeonhole, svm2lp, htc, knapsack, nqueens, nonogram, sudoku, pbconvert, lpconvert, toyfmf, toysmt, toysat, toysolver
Downloads	15366 total (18 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs available [build log] Last success reported on 2016-11-16 [all 1 reports]

Readme for toysolver-0.4.0

[back to package description]

toysolver

[![Join the chat at https://gitter.im/msakai/toysolver](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/msakai/toysolver?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)

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

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)
Boolean SATisfiability problem (SAT)
PB
- Pseudo Boolean Satisfaction (PBS)
- Pseudo Boolean Optimization (PBO)
- Weighted Boolean Optimization (WBO)
Max-SAT families
- Max-SAT
- Partial Max-SAT
- Weighted Max-SAT
- Weighted Partial Max-SAT
Real Closed Field

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:

SAT
- Boolean SATisfiability problem (SAT)
- Minimally Unsatisfiable Subset (MUS)
- Group-Oriented MUS (GMUS)
PB
- Pseudo Boolean Satisfaction (PBS)
- Pseudo Boolean Optimization (PBO)
- Weighted Boolean Optimization (WBO)
Max-SAT families
- Max-SAT
- Partial Max-SAT
- Weighted Max-SAT
- Weighted Partial Max-SAT
Integer Programming (all variables must be bounded)

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:

toysat placed 2nd in PARTIAL-BIGINT-LIN and SOFT-BIGINT-LIN categories
toysat placed 4th in PARTIAL-SMALLINT-LIN and SOFT-SMALLINT-LIN categories
toysat placed 8th in OPT-BIGINT-LIN category

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:

Input formats: lp, mps, cnf, wcnf, opb, wbo
Output formats: lp, .mps, smt2, ys

pbconvert

Converter between SAT/PB-related formats

Usage:

pbconvert -o [outputfile] [inputfile]

Supported formats:

Input formats: cnf, wcnf, opb, wbo
Output formats: opb, wbo, lsp, lp, mps, smp, smt2, ys

Bindings

ersatz-toysat - toysat backend driver for ersatz
satchmo-toysat - toysat backend driver for satchmo

TODO

Local search
Survey propagation