Repository files navigation

Note that this is reimplementation, not bindings.

Original minisat links:

• https://github.com/niklasso/minisat
• http://minisat.se/

Pretty much identical to original minisat. The only difference is using pair of dashesbefore each argument instead of just one.So, instead of something like:

$ minisat -verb=2 -rsync input.cnf

we have:

$ minisat-rust --verb=2 --rsync input.cnf

This is because I am too lazy to reimplement minisat's custom argument parsing and usedexisting library instead :)

Just use Cargo. You should have minisat in your path if you want to run big testthat solves bunch of cnf files and compares output to minisat.

• Reading (gzipped) CNF from stdin.
• Proper allocation/reallocation of clauses (GC log messages are fake to test outputagainst minisat). Probably need to wait Rust allocation features stabilizationbefore implementing it.
• Proper Ctrl-C handling.
• Writing DIMACS when solving is interrupted.

There are a few reasons for reimplementing instead of just writing bindings:

• Evaluate how Rust is suitable for relatively big projects
• Estimate performance degradation (~1.5 -- 2 times for now; maybe I am just bad at Rust).
• Minisat code is quite complicated having big structure randomly mutated by bunch ofmethods. Rust encourages splitting it into smaller more tractable parts that couldhelp understanding how minisat actually works and verify it with Rust type system.
• Maybe find some minisat bugs as a result of previous point.Indeed at least one was found:Issue 26.