Improve performances

[Gbury]

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:

• finely tune the flambda options of the compiler to fully profit from the optimizations available
• identify bottlenecks in the code using the spacetime profiler, and propose modifications to the code

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 simple make 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 the propagate_atom function, and similarly, how the time spent in propagate_in_clause is distributed. In these two cases, the automatic instrumentation of landmarks seems to not be enough to have precise enough information.

[Gbury]

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.

[c-cube]

I think this is mostly fixed by #11 (although proof checking can still be improved). Should we close?