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 ]
Modules
[Index]
- ToySolver
- ToySolver.BoundsInference
- ToySolver.CAD
- ToySolver.CongruenceClosure
- ToySolver.ContiTraverso
- Converter
- ToySolver.Converter.MIP2SMT
- ToySolver.Converter.MaxSAT2IP
- ToySolver.Converter.MaxSAT2NLPB
- ToySolver.Converter.MaxSAT2WBO
- ToySolver.Converter.ObjType
- ToySolver.Converter.PB2IP
- ToySolver.Converter.PB2LSP
- ToySolver.Converter.PB2SMP
- ToySolver.Converter.PB2WBO
- ToySolver.Converter.PBSetObj
- ToySolver.Converter.SAT2IP
- ToySolver.Converter.SAT2PB
- ToySolver.Converter.WBO2PB
- ToySolver.Cooper
- Data
- AlgebraicNumber
- ToySolver.Data.ArithRel
- ToySolver.Data.Boolean
- ToySolver.Data.DNF
- ToySolver.Data.Delta
- FOL
- ToySolver.Data.LA
- ToySolver.Data.LBool
- ToySolver.Data.MIP
- ToySolver.Data.Polynomial
- Factorization
- ToySolver.Data.Polynomial.Factorization.FiniteField
- ToySolver.Data.Polynomial.Factorization.Hensel
- ToySolver.Data.Polynomial.Factorization.Integer
- ToySolver.Data.Polynomial.Factorization.Kronecker
- ToySolver.Data.Polynomial.Factorization.Rational
- ToySolver.Data.Polynomial.Factorization.SquareFree
- ToySolver.Data.Polynomial.Factorization.Zassenhaus
- ToySolver.Data.Polynomial.GroebnerBasis
- Interpolation
- Factorization
- ToySolver.Data.Var
- ToySolver.Data.Vec
- ToySolver.FOLModelFinder
- ToySolver.FourierMotzkin
- ToySolver.HittingSet
- Internal
- ToySolver.Knapsack
- ToySolver.LPSolver
- ToySolver.LPSolverHL
- ToySolver.LPUtil
- ToySolver.MIPSolver2
- ToySolver.MIPSolverHL
- ToySolver.OmegaTest
- ToySolver.SAT
- ToySolver.Simplex
- ToySolver.Simplex2
- Text
- ToySolver.Version
Flags
Manual Flags
| Name | Description | Default |
|---|---|---|
| forcechar8 | set default encoding to char8 (not to use iconv) | Disabled |
| buildtoyfmf | build toyfmf command | Disabled |
| buildmiscprograms | build misc programs | Disabled |
Automatic Flags
| Name | Description | Default |
|---|---|---|
| exceptions06 | use exceptions >=0.6 | Enabled |
| random1013 | use random >=1.0.1.3 | Enabled |
Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info
Downloads
- toysolver-0.1.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
For package maintainers and hackage trustees
Candidates
| 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, 0.9.0 |
|---|---|
| Dependencies | array, base (>=4.4 && <5), bytestring, containers (>=0.4.2), data-interval (>=0.6.0 && <1.0.0), deepseq (<1.4), exceptions (==0.5 || >=0.6), filepath, finite-field (>=0.7.0 && <0.9), ghc-prim, hashable (>=1.1.2.5 && <1.3.0.0), heaps, intern (>=0.9.1.2 && <1.0.0.0), loop (>=0.2.0 && <1.0.0), mtl (>=2.1.2), multiset, old-locale, OptDir, parse-dimacs, parsec, prettyclass (>=1.0.0), primes, process (>=1.1.0.2), queue, random, sign (>=0.2.0 && <1.0.0), stm (>=2.3), temporary (>=1.2), time, toysolver, type-level-numbers (>=0.1.1.0 && <0.2.0.0), unbounded-delays, unordered-containers (>=0.2.3 && <0.3.0), vector-space (>=0.8.6) [details] |
| Tested with | ghc ==7.4.2, ghc ==7.6.3, ghc ==7.8.2 |
| License | BSD-3-Clause |
| Author | Masahiro Sakai (masahiro.sakai@gmail.com) |
| Maintainer | masahiro.sakai@gmail.com |
| Uploaded | by MasahiroSakai at 2014-09-13T03:05:58Z |
| Revised | Revision 2 made by sjakobi at 2021-11-18T05:09:47Z |
| Category | Algorithms, Optimisation, Optimization, Theorem Provers, Constraints |
| Bug tracker | https://github.com/msakai/toysolver/issues |
| Source repo | head: git clone git://github.com/msakai/toysolver.git |
| Distributions | |
| Reverse Dependencies | 4 direct, 0 indirect [details] |
| Executables | pbverify, maxsatverify, pigeonhole, pbconvert, lpconvert, toyfmf, toysat, toysolver |
| Downloads | 16120 total (72 in the last 30 days) |
| Rating | (no votes yet) [estimated by Bayesian average] |
| Your Rating | |
| Status | Docs uploaded by user Build status unknown [no reports yet] |
Readme for toysolver-0.1.0
[back to package description]toysolver
Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc.
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)
- Real Closed Field
- 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, cad, old-mip, ct
toysat
SAT-based solver for the following problems:
- SAT
- Minimally Unsatisfiable Subset (MUS)
- 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 --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
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:
- Input formats: lp, mps, cnf, wcnf, opb, wbo
- Output formats: lp, smt2, ys
pbconvert
Converter between SAT/PB-related formats
Usage:
pbconvert -o <outputile> <inputfile>
Supported formats:
- Input formats: cnf, wcnf, opb, wbo
- Output formats: opb, wbo, lsp, lp, mps, smp, smt2, ys
TODO
- Local search
- Suvery propagation