The toysolver package

[Tags:bsd3, library, program]

Toy-level implementation of some decision procedures


[Skip to Readme]

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.2.0, 0.3.0, 0.4.0
Change log CHANGELOG.markdown
Dependencies array (>=0.4.0.0), base (>=4.6 && <5), 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 && <1.0.0), ghc-prim, hashable (>=1.1.2.5 && <1.3.0.0), haskeline (==0.7.*), 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]
License BSD3
Author Masahiro Sakai (masahiro.sakai@gmail.com)
Maintainer masahiro.sakai@gmail.com
Stability Unknown
Category Algorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic
Bug tracker https://github.com/msakai/toysolver/issues
Source repository head: git clone git://github.com/msakai/toysolver.git
Uploaded Mon Jan 25 13:10:40 UTC 2016 by MasahiroSakai
Distributions
Downloads 1521 total (28 in the last 30 days)
Votes
0 []
Status Docs pending
Build status unknown [no reports yet]

Modules

  • ToySolver
    • Arith
      • ToySolver.Arith.BoundsInference
      • ToySolver.Arith.CAD
      • ToySolver.Arith.ContiTraverso
      • ToySolver.Arith.Cooper
        • ToySolver.Arith.Cooper.Base
        • ToySolver.Arith.Cooper.FOL
      • ToySolver.Arith.FourierMotzkin
        • ToySolver.Arith.FourierMotzkin.Base
        • ToySolver.Arith.FourierMotzkin.FOL
        • ToySolver.Arith.FourierMotzkin.Optimization
      • ToySolver.Arith.LPSolver
      • ToySolver.Arith.LPSolverHL
      • ToySolver.Arith.LPUtil
      • ToySolver.Arith.MIPSolver2
      • ToySolver.Arith.MIPSolverHL
      • ToySolver.Arith.OmegaTest
        • ToySolver.Arith.OmegaTest.Base
      • ToySolver.Arith.Simplex
      • ToySolver.Arith.Simplex2
      • ToySolver.Arith.VirtualSubstitution
    • Combinatorial
      • HittingSet
        • ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
        • ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
        • ToySolver.Combinatorial.HittingSet.HTCBDD
        • ToySolver.Combinatorial.HittingSet.SHD
        • ToySolver.Combinatorial.HittingSet.Simple
      • Knapsack
        • ToySolver.Combinatorial.Knapsack.BB
        • ToySolver.Combinatorial.Knapsack.DPDense
        • ToySolver.Combinatorial.Knapsack.DPSparse
      • ToySolver.Combinatorial.SubsetSum
    • 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
    • Data
      • AlgebraicNumber
        • ToySolver.Data.AlgebraicNumber.Complex
        • ToySolver.Data.AlgebraicNumber.Real
        • ToySolver.Data.AlgebraicNumber.Root
        • ToySolver.Data.AlgebraicNumber.Sturm
      • ToySolver.Data.BoolExpr
      • ToySolver.Data.Boolean
      • ToySolver.Data.DNF
      • ToySolver.Data.Delta
      • FOL
        • ToySolver.Data.FOL.Arith
        • ToySolver.Data.FOL.Formula
      • ToySolver.Data.LA
        • ToySolver.Data.LA.FOL
      • ToySolver.Data.LBool
      • ToySolver.Data.MIP
        • ToySolver.Data.MIP.Base
        • ToySolver.Data.MIP.LPFile
        • ToySolver.Data.MIP.MPSFile
      • ToySolver.Data.OrdRel
      • ToySolver.Data.Polynomial
        • Factorization
          • ToySolver.Data.Polynomial.Factorization.FiniteField
          • ToySolver.Data.Polynomial.Factorization.Hensel
            • ToySolver.Data.Polynomial.Factorization.Hensel.Internal
          • 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
          • ToySolver.Data.Polynomial.Interpolation.Lagrange
      • ToySolver.Data.Var
    • EUF
      • ToySolver.EUF.CongruenceClosure
      • ToySolver.EUF.EUFSolver
      • ToySolver.EUF.FiniteModelFinder
    • Internal
      • Data
        • ToySolver.Internal.Data.IOURef
        • ToySolver.Internal.Data.IndexedPriorityQueue
        • ToySolver.Internal.Data.PriorityQueue
        • ToySolver.Internal.Data.SeqQueue
        • ToySolver.Internal.Data.Vec
      • ToySolver.Internal.ProcessUtil
      • ToySolver.Internal.TextUtil
      • ToySolver.Internal.Util
    • ToySolver.SAT
      • ToySolver.SAT.Integer
      • ToySolver.SAT.MUS
        • ToySolver.SAT.MUS.CAMUS
        • ToySolver.SAT.MUS.DAA
        • ToySolver.SAT.MUS.QuickXplain
        • ToySolver.SAT.MUS.Types
      • ToySolver.SAT.PBNLC
      • ToySolver.SAT.PBO
        • ToySolver.SAT.PBO.BC
        • ToySolver.SAT.PBO.BCD
        • ToySolver.SAT.PBO.BCD2
        • ToySolver.SAT.PBO.Context
        • ToySolver.SAT.PBO.MSU4
        • ToySolver.SAT.PBO.UnsatBased
      • ToySolver.SAT.Printer
      • ToySolver.SAT.TheorySolver
      • ToySolver.SAT.TseitinEncoder
      • ToySolver.SAT.Types
    • ToySolver.SMT
    • Text
      • ToySolver.Text.GCNF
      • ToySolver.Text.GurobiSol
      • ToySolver.Text.MaxSAT
      • ToySolver.Text.SDPFile
    • ToySolver.Version
    • ToySolver.Wang

Flags

NameDescriptionDefaultType
forcechar8set default encoding to char8 (not to use iconv)DisabledManual
linuxstaticbuild statically linked binariesDisabledManual
buildtoyfmfbuild toyfmf commandDisabledManual
buildsampleprogramsbuild sample programsDisabledManual
buildmiscprogramsbuild misc programsDisabledManual
exceptions06use exceptions >=0.6EnabledAutomatic
time15use time >=1.5.0EnabledAutomatic
transformers051use transformers >=0.5.1EnabledAutomatic
usehaskelineuse haskeline packageEnabledManual

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

Downloads

Maintainer's Corner

For package maintainers and hackage trustees

Readme for toysolver

Readme for toysolver-0.4.0

toysolver

Join the chat at <a href="https://gitter.im/msakai/toysolver">https://gitter.im/msakai/toysolver</a>

Build Status Build status Coverage Status Hackage

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

TODO

  • Local search
  • Survey propagation