All Projects → c-cube → batsat

c-cube / batsat

Licence: other
A (parametrized) Rust SAT solver originally based on MiniSat

Programming Languages

rust
11053 projects
c
50402 projects - #5 most used programming language

Projects that are alternatives of or similar to batsat

togasat
A Header-Only CDCL SAT Solver for Programming Contest
Stars: ✭ 51 (+96.15%)
Mutual labels:  sat-solver, minisat
minisat-rust
Experimental minisat SAT solver reimplementation in Rust
Stars: ✭ 68 (+161.54%)
Mutual labels:  sat-solver, minisat
mSAT
A modular sat/smt solver with proof output.
Stars: ✭ 91 (+250%)
Mutual labels:  sat-solver
slime-sat-solver
A Free World Class High Performance SAT Solver
Stars: ✭ 15 (-42.31%)
Mutual labels:  sat-solver
mios
A SAT solver written in Haskell.
Stars: ✭ 33 (+26.92%)
Mutual labels:  sat-solver
haskell-picosat
Haskell bindings for PicoSAT solver
Stars: ✭ 15 (-42.31%)
Mutual labels:  sat-solver
discrete-math-python-scripts
Python code snippets from Discrete Mathematics for Computer Science specialization at Coursera
Stars: ✭ 98 (+276.92%)
Mutual labels:  sat-solver
gapt
GAPT: General Architecture for Proof Theory
Stars: ✭ 83 (+219.23%)
Mutual labels:  sat-solver
gini
A fast SAT solver
Stars: ✭ 139 (+434.62%)
Mutual labels:  sat-solver
minizinc-python
Access to all MiniZinc functionality directly from Python
Stars: ✭ 92 (+253.85%)
Mutual labels:  sat-solver
SAT-Solver-DPLL
A simple SAT solver that implements the DPLL algorithm with unit resolution
Stars: ✭ 37 (+42.31%)
Mutual labels:  sat-solver
PyMiniSolvers
A Python API for the MiniSat and MiniCard constraint solvers.
Stars: ✭ 18 (-30.77%)
Mutual labels:  minisat

BatSat Build Latest Version

This is a Rust SAT solver forked from ratsat, a reimplementation of MiniSat.

For reference, a simple benchmark comparing it to minisat on a set of (easy) problems.

License

MIT licensed.

Features and Goals

Batsat is originally based on ratsat, a clone of minisat. However we want to extend batsat further and to provide the following features:

  • proof production (in DRAT)
  • easy access to unsat-cores (as subset of assumptions)
  • ipasir interface for incremental solving
    • testing this interface
  • debug framework using log (optional)
  • OCaml bindings
  • templated API to write SMT solvers
  • simplification techniques from Minisat+ (as an optional internal structure)
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].