From: Andres Noetzli Date: Sat, 9 Jun 2018 04:05:01 +0000 (-0700) Subject: Reset decisions at SAT level after solving (#2059) X-Git-Tag: cvc5-1.0.0~4972 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6104c154e07b6d343b4d08c7bd185f6d74c89da8;p=cvc5.git Reset decisions at SAT level after solving (#2059) Some quick background: CVC4 has two primary contexts: the assertion context (which corresponds to the push/pops issued by the user) and the decision/SAT context (which corresponds to the push/pops done by the user and each decision made by MiniSat. Before 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77, we had an additonal push/pop when doing the actual solving. With these removed, it could happen that we get a wrong result when doing incremental solving: ``` ... ; check-sat call returns sat, the decision level in the SAT solver is ; non-zero at this point (check-sat) ; Solver::addClause_() determines that we cannot add the clause to the ; SAT solver directly because the decision level is non-zero (i.e. the ; clause is treated like a theory lemma), thus it is added to the lemmas ; list. (assert false) ; The solver stores some information about the current state, including ; the value of the "ok" flag in Solver, which indicates whether the ; current constraints are unsatisfiable. Note that "ok" is true at this ; point. (push) ; Now, in Solver::updateLemmas(), we add clauses from the lemmas list. ; The problem is that empty clauses (which "false" is after removing "false" ; literals) and unit clauses are not added like normal clauses. Instead, ; the empty clause, essentially just results in the "ok" flag being set to ; false (unit clauses are added to the decision trail). (check-sat) ; Here, the solver restores the information stored during ; (push), including the "ok" flag, which is now true again. (pop) ; At this point, the solver has "forgotten" about (assert false) since ; the "ok" flag is back to true and it answers sat. (check-sat) ``` There are multiple ways to look at the problem and to fix it: - One could argue that an input assertion should always be added directly to the clauses in the SAT solver, i.e. the solver should always be at decision level 0 when we are adding input clauses. The advantage of this is that it is relatively easy to implement, corresponds to what the original MiniSat code does (it calls Solver::cancelUntil(0) after solving), and is no worse than what we had before commit 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 (push/pop do a strict superset of what resetting the decision at the current assertion level does). The disadvantage is that we might throw away some useful work. - One could argue that is fine that (assert false) is treated like a theory lemma. The advantage being that it might result in more efficient solving and the disadvantage being that it is much trickier to implement. Unfortunately, it is not quite clear from the code what the original intention was but we decided to implement the first solution. This commit exposes a method in MiniSat to reset the decisions at the current assertion level. We call this method from SmtEngine after solving. Resetting the decisions directly after solving while we are still in MiniSat does not work because it causes issues with datastructures in the SMT solver that use the decision context (e.g. TheoryEngine::d_incomplete seems to be reset too early, resulting in us answering sat instead of unknown). --- diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 2136f22df..aa59f18e1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -344,8 +344,9 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // Fit to size ps.shrink(i - j); - // If we are in solve or decision level > 0 - if (minisat_busy || decisionLevel() > 0) { + // If we are in solve_ or propagate + if (minisat_busy) + { Debug("pf::sat") << "Add clause adding a new lemma: "; for (int k = 0; k < ps.size(); ++k) { Debug("pf::sat") << ps[k] << " "; @@ -369,6 +370,8 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; // lemmas_proof_id.push(proof_id); } else { + assert(decisionLevel() == 0); + // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { if(PROOF_ON()) { @@ -534,9 +537,7 @@ void Solver::cancelUntil(int level) { } } -void Solver::popTrail() { - cancelUntil(0); -} +void Solver::resetTrail() { cancelUntil(0); } //================================================================================================= // Major methods: @@ -1391,7 +1392,7 @@ lbool Solver::solve_() ScopedBool scoped_bool(minisat_busy, true); - popTrail(); + assert(decisionLevel() == 0); model.clear(); conflict.clear(); @@ -1580,8 +1581,8 @@ void Solver::garbageCollect() void Solver::push() { assert(enable_incremental); + assert(decisionLevel() == 0); - popTrail(); ++assertionLevel; Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; trail_ok.push(ok); @@ -1596,8 +1597,6 @@ void Solver::pop() { assert(enable_incremental); - // Pop the trail to 0 level - popTrail(); assert(decisionLevel() == 0); // Pop the trail below the user level diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 99c47e045..c27d8a18b 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -169,6 +169,11 @@ public: void push (); void pop (); + /* + * Reset the decisions in the DPLL(T) SAT solver at the current assertion + * level. + */ + void resetTrail(); // addClause returns the ClauseId corresponding to the clause added in the // reference parameter id. bool addClause (const vec& ps, bool removable, ClauseId& id); // Add a clause to the solver. @@ -393,7 +398,6 @@ protected: void theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Adds lemmas. CRef updateLemmas (); // Add the lemmas, backtraking if necessary and return a conflict if there is one void cancelUntil (int level); // Backtrack until a certain level. - void popTrail (); // Backtrack the trail to the previous push position int analyze (CRef confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - true if p is redundant diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 514338fd9..73a6f0d5e 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -232,6 +232,8 @@ void MinisatSatSolver::pop() { d_minisat->pop(); } +void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); } + /// Statistics for MinisatSatSolver MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) : diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 58e02179c..ea673a15d 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -74,6 +74,8 @@ public: void pop() override; + void resetTrail() override; + void requirePhase(SatLiteral lit) override; bool flipDecision() override; diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 9b551fa70..96fea2147 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -120,7 +120,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) toDimacs(); return l_Undef; } - popTrail(); + assert(decisionLevel() == 0); vec extra_frozen; lbool result = l_True; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 23f7ea6b5..b09e7a088 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -281,6 +281,12 @@ void PropEngine::pop() { Debug("prop") << "pop()" << endl; } +void PropEngine::resetTrail() +{ + d_satSolver->resetTrail(); + Debug("prop") << "resetTrail()" << endl; +} + unsigned PropEngine::getAssertionLevel() const { return d_satSolver->getAssertionLevel(); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f3a69be96..edc828418 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -213,6 +213,12 @@ public: */ void pop(); + /* + * Reset the decisions in the DPLL(T) SAT solver at the current assertion + * level. + */ + void resetTrail(); + /** * Get the assertion level of the SAT solver. */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 4dc95e060..86e0f1577 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -148,6 +148,12 @@ public: virtual void pop() = 0; + /* + * Reset the decisions in the DPLL(T) SAT solver at the current assertion + * level. + */ + virtual void resetTrail() = 0; + virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0; virtual void requirePhase(SatLiteral lit) = 0; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2836f73b4..69cea8b06 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4709,6 +4709,8 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, } } + d_propEngine->resetTrail(); + // Pop the context if (didInternalPush) { diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 4a7267a60..d25da1b62 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -570,6 +570,7 @@ REG0_TESTS = \ regress0/push-pop/boolean/fuzz_48.smt2 \ regress0/push-pop/boolean/fuzz_49.smt2 \ regress0/push-pop/boolean/fuzz_50.smt2 \ + regress0/push-pop/bug1990.smt2 \ regress0/push-pop/bug233.cvc \ regress0/push-pop/bug654-dd.smt2 \ regress0/push-pop/bug691.smt2 \ diff --git a/test/regress/regress0/push-pop/bug1990.smt2 b/test/regress/regress0/push-pop/bug1990.smt2 new file mode 100644 index 000000000..f0cde3113 --- /dev/null +++ b/test/regress/regress0/push-pop/bug1990.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +(set-logic QF_SAT) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(assert (or v1 v2)) +(check-sat) +(assert false) +(push) +(check-sat) +(pop) +(check-sat)