Lib.rs

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

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

#1575 in Algorithms

Download history 10/week @ 2024-03-13 7/week @ 2024-03-20 15/week @ 2024-03-27 9/week @ 2024-04-03 82/week @ 2024-04-10 4/week @ 2024-04-17 6/week @ 2024-04-24 1/week @ 2024-05-01 6/week @ 2024-05-08 10/week @ 2024-05-15 9/week @ 2024-05-22 6/week @ 2024-06-05 24/week @ 2024-06-12 12/week @ 2024-06-19 28/week @ 2024-06-26

70 downloads per month

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

~120KB