From: Utz-Uwe Haus Date: Thu, 17 Jun 2010 14:14:14 +0000 (+0200) Subject: Fix call to minisat solve() X-Git-Url: https://repo.or.cz/w/cl-satwrap.git/commitdiff_plain/bba7695d091f711f840657ea3d00216f35c3a096 Fix call to minisat solve() Assumptions don't play well with presolve. Forum answer by Niklas: "I could repeat the problem and realized that it has to do with one of the undocumented constraints of the solver-API. More specificly, it has to do with preprocessing. If you turn that off it gives consistent results: both turning on the literal as an assumption or as a unit clause gives an unsatisfiable result. The cause of this problem is that when you call solve the first time you specify that the preprocessing should be turned off at the end of the call. This means that all data-structures that has to do with preprocessing are deleted, and it is no longer possible to refer to any of the variables that may have been removed by the preprocessor. In this case the literal you pass as an assumption was indeed removed. The way to work around this is to either use preprocessing throughout, by replacing all calls of the form "solve(xxx, true, true)" with calls to "solve(xxx)", or to initially turn off all preprocessing, which can be done with a call to "eliminate(true)" before anything else. Which alternative works best depends on your application, but as preprocessing can be pretty unpredictable in some incremental settings your best bet may be to turn it off. I hope this helps," Signed-off-by: Utz-Uwe Haus --- diff --git a/backends/minisat/minisat_wrap.cc b/backends/minisat/minisat_wrap.cc index bdc31b6..07ed230 100644 --- a/backends/minisat/minisat_wrap.cc +++ b/backends/minisat/minisat_wrap.cc @@ -56,7 +56,7 @@ minisat_solve(struct minisat_solver *s) int res; /* solve */ - res=s->solver->solve(*(s->assumptions),true,true); + res=s->solver->solve(*(s->assumptions)); /* res=s->solver->solve(s->assumptions); */ if(res)