batsat
| Crates.io | batsat |
| lib.rs | batsat |
| version | 0.5.0 |
| source | src |
| created_at | 2018-12-04 22:09:59.910696 |
| updated_at | 2021-01-12 18:39:32.13976 |
| 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 | 155,737 |
Simon Cruanes (c-cube)
documentation
README
BatSat 
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)