batsat
| Crates.io | batsat |
| lib.rs | batsat |
| version | 0.6.0 |
| created_at | 2018-12-04 22:09:59.910696+00 |
| updated_at | 2025-01-20 02:24:48.162981+00 |
| description | Extensible SAT solver in Rust |
| homepage | https://github.com/c-cube/batsat |
| repository | https://github.com/c-cube/batsat |
| max_upload_size | |
| id | 100117 |
| size | 159,418 |
Simon Cruanes (c-cube)
documentation
README
BatSat 
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)