Closed Gbury closed 5 years ago
The mc2 fork ( https://github.com/c-cube/mc2 ) has achieved great performances gains by refactoring some code. Ideally, both mc2 and msat should have the same performances on pure sat problems.
I think this is mostly fixed by #11 (although proof checking can still be improved). Should we close?
Goal
mSAT currently compares quite unfavorably with other available sat solvers (see https://github.com/Gbury/sat-bench/blob/master/problems/pigeon/results ). It would be interesting to study how to improve performances either by:
Testing
Test files can be found under the
tests
directory. Additionally, the https://github.com/Gbury/sat-bench is meant to provide interesting problems on which to test and benchmark the various sat solvers, including mSAT. The problems in the repository should provide good runs on which to profile mSAT.Current status
The
profile
branch contains the necessary instrumentation using the landmarks library. A simplemake bench
in that branch should compile the instrumented binary, and execute it on a reasonably sized problem, which takes about 10s currently.The current bottleneck is, unsurprisingly, the propagation of atoms. One point of particular interest is why the
propagate_in_clause
function makes up such a small proportion of thepropagate_atom
function, and similarly, how the time spent inpropagate_in_clause
is distributed. In these two cases, the automatic instrumentation of landmarks seems to not be enough to have precise enough information.