search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.16k stars 1.47k forks source link

Accelerate model finding in SAT solver #2272

Closed rainoftime closed 5 years ago

rainoftime commented 5 years ago

It seems that some heuristics in CDCL solver can perform better on satisfiable instances. Suppose we have a set of SAT instances (e.g., bit-blasted from bit-vector constraints), and most of them tend to be satisfiable. Is there any suggestion for configuring the SAT engine to improve its empirical performance? (E.g., the restarting strategy, branching heuristics, and in-processing algorithms).

Thank you!

NikolajBjorner commented 5 years ago

Generally a question that is attracting attention. You can try to disable/delay restarts. Enabling several threads tends to help on satisfiable instances. The csp branch includes some other improvements that are good for at least some satisfiable instances, such as chronological backtracking.