Lib.rs

› Algorithms
#sat-solver #sat #minisat #interface #smt-solver #proof #mini-sat

batsat

Extensible SAT solver in Rust

by Simon Cruanes, Masaki Hara and 3 contributors

5 releases (3 breaking)

0.5.0 Jan 12, 2021
0.4.0 May 6, 2020
0.3.1 Jan 23, 2019
0.3.0 Jan 9, 2019
0.2.0 Dec 4, 2018

#1447 in Algorithms

Download history 1/week @ 2024-07-19 56/week @ 2024-08-02 44/week @ 2024-08-09 24/week @ 2024-08-16 10/week @ 2024-08-23 63/week @ 2024-08-30 38/week @ 2024-09-06 7/week @ 2024-09-13 18/week @ 2024-09-20 25/week @ 2024-09-27 10/week @ 2024-10-04 822/week @ 2024-10-11 814/week @ 2024-10-18 171/week @ 2024-10-25 265/week @ 2024-11-01

2,073 downloads per month
Used in rustsat-batsat

MIT license

155KB
3.5K SLoC

BatSat build status Latest Version

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

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)

Dependencies

~125KB