6 releases (breaking)

0.6.0 Jan 20, 2025
0.5.0 Jan 12, 2021
0.4.0 May 6, 2020
0.3.1 Jan 23, 2019
0.2.0 Dec 4, 2018

#348 in Algorithms

Download history 661/week @ 2024-12-07 928/week @ 2024-12-14 323/week @ 2024-12-21 534/week @ 2024-12-28 568/week @ 2025-01-04 249/week @ 2025-01-11 489/week @ 2025-01-18 482/week @ 2025-01-25 665/week @ 2025-02-01 358/week @ 2025-02-08 804/week @ 2025-02-15 477/week @ 2025-02-22 124/week @ 2025-03-01 1259/week @ 2025-03-08 739/week @ 2025-03-15 1231/week @ 2025-03-22

3,405 downloads per month
Used in rustsat-batsat

MIT license

160KB
3.5K SLoC

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)

Dependencies

~125KB