search

niklasso / minisat

A minimalistic and high-performance SAT solver
minisat.se
Other
1.01k stars 382 forks source link

assertion is hit in SimpSolver::relocAll #3

Open vkhomenko opened 12 years ago

vkhomenko commented 12 years ago

Consider the following sequence of calls:

SimpSolver::eliminate calls Solver::simplify, which calls Solver::removeSatisfied (which eliminates many clauses, as the solver is used incrementally, and those clauses were deleted) and then Solver::checkGarbage, which decides to relocate memory and calls (virtually) SimpSolver::garbageCollect which calls SimpSolver::relocAll

Now, the following assertion in SimpSolver::relocAll is hit:

assert(subsumption_queue.size() == 0);

(because some clauses were incrementally added, and SimpSolver::addClause_ inserts things into subsumption_queue).

Note that this scenario might be difficult to reproduce, as Solver::checkGarbage rarely calls garbageCollect, and when it does, it's usually deep in the search rather than optimisation.

vladrich commented 11 years ago

I am bit by this right now. Here's a small example triggering the assertion.

#include <minisat/core/Solver.h>
#include <minisat/simp/SimpSolver.h>

using namespace std;

int main(int argc, char *argv[])
{

    Minisat::SimpSolver solver;
    solver.newVar();
    solver.newVar();
    solver.newVar();
    solver.newVar();
    solver.newVar();
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    solver.solve();

    return 0;

}