search

FlorentAvellaneda / EvalMaxSAT

State-of-the-art MaxSAT Solver & Library Based on Unsat Core Guided Techniques
GNU General Public License v3.0
14 stars 4 forks source link

Inconsistent Runtimes and Randomized Solutions #4

Closed francisol closed 8 months ago

francisol commented 9 months ago

When running EvalMaxSAT multiple times on the same input data during idle CPU time on my computer, I noticed inconsistent runtimes ranging from 283s to 1764s. Additionally, the solutions returned by EvalMaxSAT appear to have some randomness to them. maxsat.txt

1.out.txt 2.out.txt

3.out.txt 4.out.txt

FlorentAvellaneda commented 9 months ago

It is indeed possible that the resolution time changes and that the solutions found are not the same from one execution to another (but they should all be optimal). I think this is due to the 'multiSolveStrategy', which consists of spending a time proportional to the time used to find unsat cores, to look for better unsat cores. By disabling multiSolveStrategy with the option --noMS, this should make the solver deterministic. ./EvalMaxSAT_bin --noMS maxsat.txt