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

The toysolver package

[ Tags: algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, theorem-provers ] [ Propose Tags ]

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, 0.5.0
Dependencies array, base (>=4.4 && <5), bytestring, containers (>=0.4.2), data-interval (>=0.1.0), deepseq, filepath, heaps, lattices (>=1.2.1.1), logic-TPTP, mtl, old-locale, OptDir, parse-dimacs, parsec, primes, queue, random, stm (>=2.3), time, toysolver, unbounded-delays, vector-space (>=0.8.6) [details]
License BSD3
Author Masahiro Sakai (masahiro.sakai@gmail.com)
Maintainer masahiro.sakai@gmail.com
Category Algorithms, Optimisation, Optimization
Bug tracker https://github.com/msakai/toysolver/issues
Source repository head: git clone git://github.com/msakai/toysolver.git
Uploaded Wed Apr 10 14:05:29 UTC 2013 by MasahiroSakai
Distributions NixOS:0.4.0
Executables pbconvert, lpconvert, toyfmf, toysat, toysolver
Downloads 2028 total (116 in the last 30 days)
Rating 0.0 (0 ratings) [clear rating]
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-21 [all 7 reports]
Hackage Matrix CI

Modules

  • Algebra
    • Lattice
      • Algebra.Lattice.Boolean
  • Algorithm
    • Algorithm.BoundsInference
    • Algorithm.CAD
    • Algorithm.CongruenceClosure
    • Algorithm.ContiTraverso
    • Algorithm.Cooper
      • Algorithm.Cooper.Core
      • Algorithm.Cooper.FOL
    • Algorithm.FOLModelFinder
    • Algorithm.FourierMotzkin
      • Algorithm.FourierMotzkin.Core
      • Algorithm.FourierMotzkin.FOL
    • Algorithm.LPSolver
    • Algorithm.LPSolverHL
    • Algorithm.LPUtil
    • Algorithm.MIPSolver2
    • Algorithm.MIPSolverHL
    • Algorithm.OmegaTest
      • Algorithm.OmegaTest.Misc
    • Algorithm.Simplex
    • Algorithm.Simplex2
  • Converter
    • Converter.LP2SMT
    • Converter.MaxSAT2LP
    • Converter.MaxSAT2NLPB
    • Converter.MaxSAT2WBO
    • Converter.ObjType
    • Converter.PB2LP
    • Converter.PB2LSP
    • Converter.PB2SMP
    • Converter.PB2WBO
    • Converter.PBSetObj
    • Converter.SAT2LP
    • Converter.SAT2PB
    • Converter.WBO2PB
  • Data
    • Data.AlgebraicNumber
      • Data.AlgebraicNumber.Root
    • Data.ArithRel
    • Data.DNF
    • Data.Delta
    • FOL
      • Data.FOL.Arith
      • Data.FOL.Formula
    • Data.LA
      • Data.LA.FOL
    • Data.LBool
    • Data.Polynomial
      • Data.Polynomial.FactorZ
      • Data.Polynomial.GBase
      • Data.Polynomial.Lagrange
      • Data.Polynomial.Sturm
    • Data.Var
  • SAT
    • SAT.CAMUS
    • SAT.Integer
    • SAT.MUS
    • SAT.PBO
      • SAT.PBO.MSU4
      • SAT.PBO.UnsatBased
    • SAT.Printer
    • SAT.TheorySolver
    • SAT.TseitinEncoder
    • SAT.Types
  • Text
    • Text.GCNF
    • Text.GurobiSol
    • Text.LPFile
    • Text.MPSFile
    • Text.MaxSAT
    • Text.PBFile
    • Text.SDPFile
  • Util
  • Version

Flags

NameDescriptionDefaultType
forcechar8

set default encoding to char8 (not to use iconv)

DisabledAutomatic

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-0.0.4

[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

TODO

  • Local search
  • Suvery propagation