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 -
search-algorithms
Haskell library containing common graph search algorithms -
imj-animation
Monorepo for a multi-player game engine, and game examples -
text-metrics
Calculate various string metrics efficiently in Haskell -
lca
Improves the known complexity of online lowest common ancestor search to O(log h) persistently, and without preprocessing -
treeviz
Haskell library for visualizing algorithmic decomposition of computations. -
incremental-sat-solver
Simple, Incremental SAT Solving as a Haskell Library -
integer-logarithms
Integer logarithms, originally split from arithmoi package -
GraphSCC
Tarjan's algorithm for computing strongly connected components -
graph-generators
A Haskell library for creating random Data.Graph instances using several pop -
infinite-search
An implementation of Martin Escardo's exhaustively searchable sets in Haskell. -
nonlinear-optimization-ad
Several Haskell packages for numerical optimizations. -
primesieve
A collection of packages related to math, algorithms and science, in Haskell. -
edit-distance-vector
Calculate edit scripts and distances between Vectors. -
adp-multi
Prototype of ADP for MCFL (multiple context-free languages) -
edit-distance-linear
Levenshtein edit distance in linear memory (also turns out to be faster than C++) -
dgim
:chart_with_upwards_trend: Implementation of the DGIM algorithm in Haskell. -
MIP
Libraries for reading/writing MIP problem files, invoking external MIP solvers, etc. in Haskell -
epanet-haskell
Call the EPANET toolkit via Haskell's Foreign Function Interface
WorkOS - The modern identity platform for B2B SaaS
* 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.