toysolver alternatives and similar packages
Based on the "Algorithms" category.
Alternatively, view toysolver alternatives based on common mentions on social networks and blogs.
-
arithmoi
Number theory: primes, arithmetic functions, modular computations, special sequences -
imj-animation
Monorepo for a multi-player game engine, and game examples -
text-metrics
Calculate various string metrics efficiently in Haskell -
search-algorithms
Haskell library containing common graph search algorithms -
lca
Improves the known complexity of online lowest common ancestor search to O(log h) persistently, and without preprocessing -
integer-logarithms
Integer logarithms, originally split from arithmoi package -
incremental-sat-solver
Simple, Incremental SAT Solving as a Haskell Library -
treeviz
Haskell library for visualizing algorithmic decomposition of computations. -
nonlinear-optimization-ad
Wrapper of nonlinear-optimization package for using with ad and backprop packages -
GraphSCC
Tarjan's algorithm for computing strongly connected components -
infinite-search
An implementation of Martin Escardo's exhaustively searchable sets in Haskell. -
edit-distance-vector
Calculate edit scripts and distances between Vectors. -
primesieve
A collection of packages related to math, algorithms and science, in Haskell. -
adp-multi
Prototype of ADP for MCFL (multiple context-free languages) -
graph-generators
A Haskell library for creating random Data.Graph instances using several pop -
edit-distance-linear
Levenshtein edit distance in linear memory (also turns out to be faster than C++) -
epanet-haskell
Call the EPANET toolkit via Haskell's Foreign Function Interface -
bordacount
Haskell implementation of the Borda count election method
Build time-series-based applications quickly and at scale.
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of toysolver or a related project?
README
toysolver
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]
toyconvert
Converter between various problem files.
Usage:
toyconvert -o [outputfile] [inputfile]
Supported formats:
- Input formats: .cnf .wcnf .opb .wbo .gcnf .lp .mps
- Output formats: .cnf .wcnf .opb .wbo .lsp .lp .mps .smp .smt2 .ys
Bindings
- ersatz-toysat - toysat backend driver for ersatz
- satchmo-toysat - toysat backend driver for satchmo
*Note that all licence references and agreements mentioned in the toysolver README section above
are relevant to that project's source code only.