exploding runtime in case of repeated calls for satisfiability
If the same VariableOrder is set in the solver (or a new instance of an VariableOrder, that is identically configured) and again run solver.isSatisfiable() the required runtime for the single call increases by about the factor of 1.5 each time this is done.
e.g. the following code-snipped will increase the runtime of a single isSatisfiable()-call by approximately the factor of 3000 (1.5^20)
for(int i=0; i<20, i++) {
solver.setOrder(o);
solver.isSatisfiable();
}
The problem is not existing in case of using Sat4j up to revision 1176, but is visible in each newer revision - I have tested multiple revisions. Moreover, in case of revisions between 1177 and 1206 the behavior is even worse (I was even not able to get the same variable order evaluated multiple times, e.g. i get a timeout). Thus, it could be seen with revision 1207 and is still existing in the lates revision. (checked up to revision 1732)
What I also could find out and what confused me a bit (and what seems to cause the runtime-explosion) is, that with the same variable order and variable settings, each "multiple call of setOrder() and isSatisfiable()" causes immensly increase in the number of found conflics and, thus, required thousands or millons of search() calls within the solver.
Regards, Sebastian