Fix call to minisat solve()minisat-backend
authorUtz-Uwe Haus <lisp@uuhaus.de>
Thu, 17 Jun 2010 14:14:14 +0000 (16:14 +0200)
committerUtz-Uwe Haus <lisp@uuhaus.de>
Thu, 17 Jun 2010 14:14:14 +0000 (16:14 +0200)
commitbba7695d091f711f840657ea3d00216f35c3a096
treeab1e0e66dc232a35c98f9f0c716d416363ba1858
parent7f0489362a3604706badf37757f4d2f5a6b7965c
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 <lisp@uuhaus.de>
backends/minisat/minisat_wrap.cc