SAT Solvers and Phase Saving

DPLL SAT solvers typically apply a Phase Saving heuristic. The idea is to remember the last assignment of each variable and use it first in branching.

To experiment with the effects of branching polarity and phase saving, I tried several SAT solvers and modified the phase settings. All are Windows 64-bit ports, run in single-threaded mode. I always used the same example input of moderate complexity (5619 variables, 11261 clauses, in the solution 4% of all variable are true, 96% false).

The resulting run-times are listed below:

It might be just (bad) luck, but the differences are remarkably big. It is a special surprise, that MiniSat outperformed all modern solvers for my example.

My question:

Are there any explanations for the differences?
Best practices for polarity and phase saving?

Nothing conclusive can be deduced from your test. DPLL and solvers based on it are known to exhibit heavy-tailed behavior depending on initial search conditions. This means the same solver can have both short and long runtimes on the same instance depending on factors like when random restarts occur. Search times across different solvers can vary wildly depending on (for example) how they choose decision variables, even without the added complications of phase saving and random restarts.