toysolver: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc
This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.
Warnings:
- Exposed modules use unallocated top-level names: ToySolver
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.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 | None available |
| Dependencies | array, base (>=4.4 && <5), bytestring, containers (>=0.4.2), data-interval (>=0.6.0 && <1.0.0), deepseq, exceptions (==0.5 || >=0.6), filepath, finite-field (>=0.7.0 && <1.0.0), 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] |
| License | BSD-3-Clause |
| Author | Masahiro Sakai (masahiro.sakai@gmail.com) |
| Maintainer | masahiro.sakai@gmail.com |
| 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 |
| Uploaded | by MasahiroSakai at 2014-09-13T03:03:03Z |
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 (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees
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