OCaml-minisat 0.5 just landed on opam.
This library has bindings to the classic minisat SAT solver. It should have decently low overhead (no ctypes, runtime lock released, etc.) and be useful for general purpose SAT solving. Minisat is not really state of the art anymore, but it’s still pretty damn good for a lot of use cases.
Just out of interest, what is the state of the art, and what are these use cases?
State of the art is, roughly,
Cadical and
Kissa (yes, both are from Armin
Biere). They’re better on hard SAT instances, the ones that still take a
while to solve.
These minisat bindings could be updated at least to Glucose (a known
patch to minisat with better heuristics), maybe I’ll do that at some
point.
The use cases: anything where you want to solve a NP-complete problem
(register allocation for example; sudoku solving; also a lot of
verification problems can benefit from a SAT encoding somewhere). Using
an API instead of calling a process is useful because you can access
more things and perform incremental solving easily: instead of solving a
single SAT problem, you can solve a series of increasingly big problems
without starting from scratch each time.
Glancing through the repo and tracker, it’s not clear whether Kissat now has an API and performs incremental solving or unsat core extraction. Do you know?
I have no idea, really :-). For unsat core extractions I suppose the
best bet is to look at the incremental tracks.
I think Cadical at least must have incremental solving.
Bindings to either could be very useful (in a different library), but in
first approximation minisat will be enough for many use cases, and
handily beat any ad-hoc solver written in OCaml by non-experts.
It’s also just very predictable and robust.
It didn’t take long, but here’s minisat 0.6 which actually switches to the C++ minisat from the C minisat that was used so far. That means new functions such as unsat_core are now available!