Minisat::Solver says UNSAT but Minisat::SimpSolver says SAT (incremental solving)

[Clifford Wolf]

Hello,

I have an application that uses Minisat::Solver for incremental SAT solving. From tests with generated CNF files I know that Minisat::SimpSolver is much faster in my application than Minisat::Solver. However, when I switch to SimpSolver, a problem that was UNSAT before is now reported SAT with an incorrect model. I suspect that the bug is related to the incremental solving.

Is there anything special I need to know about Minisat::SimpSolver, or is it supposed to work as a drop-in replacement for Minisat::Solver?

If this seems to be a bug in minisat then I can try to create a stand-alone test case for this. (would probably still create a lot of clauses, it would just not need my entire application to do so)

I've tried this with the latest Minisat sourcecode from github.

regards,
- clifford

[Michael Tautschnig]

Hello Clifford,

> I have an application that uses Minisat::Solver for incremental SAT solving. From tests with generated CNF files I know that Minisat::SimpSolver is much faster in my application than Minisat::Solver. However, when I switch to SimpSolver, a problem that was UNSAT before is now reported SAT with an incorrect model. I suspect that the bug is related to the incremental solving.
>
> Is there anything special I need to know about Minisat::SimpSolver, or is it supposed to work as a drop-in replacement for Minisat::Solver?
>
> If this seems to be a bug in minisat then I can try to create a stand-alone test case for this. (would probably still create a lot of clauses, it would just not need my entire application to do so)
>

[...]

This is certainly not expected, and may have one of three reasons:

1. The way you use the solver breaks certain invariants (for instance, variables
may have been removed entirely unless you marked them frozen).
2. It is genuine bug.
3. You are running into one of the misoptimisation issues. Certain compiler
(version) are known to break Minisat when having optimisation switched on.

For 1. and 2. a stand-alone test case would surely help. But 3. is probably the
easiest to rule out: disable all optimisation and see whether your problem
persists (but obviously the solver will be a lot slower).

Best,
Michael

[Mate Soos]

Hi All,

On 03/06/2014 12:56 PM, Michael Tautschnig wrote:
>> I have an application that uses Minisat::Solver for incremental SAT
>> solving. From tests with generated CNF files I know that
>> Minisat::SimpSolver is much faster in my application than
>> Minisat::Solver. However, when I switch to SimpSolver, a problem
>> that was UNSAT before is now reported SAT with an incorrect model.
>> I suspect that the bug is related to the incremental solving.
>

> This is certainly not expected, and may have one of three reasons:
>
> 1. The way you use the solver breaks certain invariants (for
> instance, variables may have been removed entirely unless you marked
> them frozen). 2. It is genuine bug. 3. You are running into one of
> the misoptimisation issues. Certain compiler (version) are known to
> break Minisat when having optimisation switched on.
>
> For 1. and 2. a stand-alone test case would surely help. But 3. is
> probably the easiest to rule out: disable all optimisation and see
> whether your problem persists (but obviously the solver will be a lot
> slower).

Number (3) only happens with certain gcc versions. Just compile with
-fno-tree-pre, you don't need to disable all optimisations, just this one.

If it's not the gcc bug, then I would guess it to be (1). Check that you
freeze all variables that you later use between solve() calls. Also,
make sure that you don't re-use Solver instances for different problems
-- only the same problem, but with additional constraints. There were
some emails in the list before where someone misunderstood the nature of
the function clean(). If it's neither (3) or (1), then it would be great
if you could send an example C++ program that re-produces the bug.

Cheers,

Mate

[Clifford Wolf]

Hello,

sorry for replying so late. It first took a really long time for this post to be approved and when it did I did not check anymore because I have solve the problem already. Thanks for your replies anyways.

On Thursday, March 6, 2014 1:56:52 PM UTC+1, Michael Tautschnig wrote:

This is certainly not expected, and may have one of three reasons:

 

The problem was that I did not use the MiniSat::SimpSolver::setFrozen() API on all literals that I accessed in the assumptions during incremental solving. It looks like the use of this API was optional before commit 760d4f1 but is mandatory now. When minisat is recompiled without -D NDEBUG I also see that the assert that checks for this is triggered.

regards,

 - clifford