SAT Competition

[ahorn]

Hi,

Out of curiosity, have you considered submitting minisat-rust to the upcoming SAT Competition? If nothing else, it may provide some interesting data points how minisat-rust compares to the C++ implementation of minisat. It might also stir up some more interest in your project, although I don't know for sure of course. Either way, it's just a thought.

All best wishes,
A

[mishun]

It's probably not very interesting to submit it as is because it is designed to generate the same output verbatim as original minisat for same input file and also still lacks a few important implementation details like proper clause allocation (Rust's heap API is still unstable). I actually thought about adding a few features from more modern solvers and submitting it just to show that "Rust can do it too", but, again, clause allocation, and me not being any kind of modern SAT solver expert (my experience with minisat is from my M.Sc. days more than 7 years ago).

[dralley]

Looks like the API has stabilized

[ahorn]

For those interested, clause allocation in Rust is also discussed by @jix in a recent blog post.

[mishun]

Yeah, I've seen std::alloc. I actually implemented custom allocator that is very similar to original minisat's one just a few days ago:
https://github.com/mishun/minisat-rust/blob/master/src/sat/formula/allocator.rs
Although, it still takes a few bytes per clause more