Assertion has(k) in intmap.h is hit when calling SimpSolver::AddClause

[Andreas Morgenstern]

Hello all,

in order to get all possible solutions of a formula, I generate an
activation literal a (with its variable frozen to prevent removal).
Then, I call the solve method with Solve(a) which gives
me a new satisfying assignment c. I then use
addclause(not a, "not c") to prevent minisat from
returning me this solution again.
This works fine for most of my problems. However,
for one problem, the addclause-operation fails
with the following assertion: assert(has k) in intmap.h.
Inspecting the bug gives me that he doesn't know about the
variable of the activation literal.
This is strange, because it works for say 15 calls and then crashes,
althoug the activation literal does not change.
It seems however, that the map that is checked in intmap.h changes
its sizes between the last call that succeeded and the failed call.
It seems to me that at some point some simplification is done.

Any ideas about that problem ?

Andreas
 


 

[Niklas Sörensson]

Hello Andreas,

Nope, I can't say what goes on here unless you give more details or
show me an example. Maybe you can post a GDB backtrace or something?

On a side note, are you sure you want to use preprocessing within the
enumeration loop? If it is possible, it is often good if preprocessing
can be done just once, then turned off before a sequence of solve
calls is used. This will release some memory used for preprocessing
for instance and one can avoid performance problems due to too much
spent on preprocessing. Of course, sometimes incremental preprocessing
is helpful, and the implementation is designed to be incremental in
the sense that if nothing was added or changed, then preprocessing
should be a no-op. But the trouble is when a small amount changed,
then the amount of time spent on preprocessing can be unpredictable
and it makes sense to take some care and perhaps call it manually at
specific points rather than allowing solve to call it always.

Regards,
Niklas

[Andreas Morgenstern]

Hello Niklas,

the problem is that I call Minisat from within C# via a native call.
And therefore I can't post a GDB backtrack. I'm trying to elaborate on
that.

I already turned of preprocessing (you mean turn of simp in solve, or not ?)

Thanks for your help,

Andreas

[Niklas Sörensson]

Hi Andreas,

To just do preprocessing and the turn it off, do the following:

solver.eliminate(true);

After that you don't need to care about freezing any new variables.

Regards,
Niklas

[Andreas Morgenstern]

Hello Niklas,

thanks. That seems to help.

Andreas

[Andreas Morgenstern]

Hello again,

for some other examples this does not help.
Is it possible that I (unintentionally) turn on simplification again?
Which functions turn on simplifcation ? I found only eliminate.

Thanks,

Andreas

[Andreas Morgenstern]

Hello,

it was an error of mine. Sorry for that.

Andreas