From ea24eec6b7914550c84cb09c569b7fc80304d8e7 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 13 Jun 2018 15:16:24 -0700 Subject: [PATCH] Workaround for incremental unsat cores (#1962) This commit implements a workaround for computing unsat cores while doing incremental solving to address #1349. Currently, our resolution proofs do not handle clauses with a lower-than-assertion-level correctly because the resolution proofs for them get removed when popping the context but the SAT solver keeps using them. The workaround changes the behavior of the SAT solver to add clauses always at the current level if incremental solving and unsat cores are enabled. This makes sure that all learned clauses are removed when we pop below the level that they were learned at. This may degrade performance because the SAT solver has to relearn clauses. --- src/prop/minisat/core/Solver.cc | 143 ++++++++++++++++++++------------ 1 file changed, 91 insertions(+), 52 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index aa59f18e1..3c8023395 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -26,7 +26,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include "base/output.h" +#include "options/main_options.h" #include "options/prop_options.h" +#include "options/smt_options.h" #include "proof/clause_id.h" #include "proof/proof_manager.h" #include "proof/sat_proof.h" @@ -40,6 +42,22 @@ using namespace CVC4::prop; namespace CVC4 { namespace Minisat { +namespace { +/* + * Returns true if the solver should add all clauses at the current assertion + * level. + * + * FIXME: This is a workaround. Currently, our resolution proofs do not + * handle clauses with a lower-than-assertion-level correctly because the + * resolution proofs get removed when popping the context but the SAT solver + * keeps using them. + */ +bool assertionLevelOnly() +{ + return options::unsatCores() && options::incrementalSolving(); +} +} // namespace + //================================================================================================= // Options: @@ -242,43 +260,60 @@ CRef Solver::reason(Var x) { // Compute the assertion level for this clause int explLevel = 0; - int i, j; - Lit prev = lit_Undef; - for (i = 0, j = 0; i < explanation.size(); ++ i) { - // This clause is valid theory propagation, so its level is the level of the top literal - explLevel = std::max(explLevel, intro_level(var(explanation[i]))); - - Assert(value(explanation[i]) != l_Undef); - Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i]))); - - // Always keep the first literal - if (i == 0) { + if (assertionLevelOnly()) + { + explLevel = assertionLevel; + } + else + { + int i, j; + Lit prev = lit_Undef; + for (i = 0, j = 0; i < explanation.size(); ++i) + { + // This clause is valid theory propagation, so its level is the level of + // the top literal + explLevel = std::max(explLevel, intro_level(var(explanation[i]))); + + Assert(value(explanation[i]) != l_Undef); + Assert(i == 0 + || trail_index(var(explanation[0])) + > trail_index(var(explanation[i]))); + + // Always keep the first literal + if (i == 0) + { + prev = explanation[j++] = explanation[i]; + continue; + } + // Ignore duplicate literals + if (explanation[i] == prev) + { + continue; + } + // Ignore zero level literals + if (level(var(explanation[i])) == 0 + && user_level(var(explanation[i]) == 0)) + { + continue; + } + // Keep this literal prev = explanation[j++] = explanation[i]; - continue; - } - // Ignore duplicate literals - if (explanation[i] == prev) { - continue; - } - // Ignore zero level literals - if (level(var(explanation[i])) == 0 && user_level(var(explanation[i]) == 0)) { - continue; } - // Keep this literal - prev = explanation[j++] = explanation[i]; - } - explanation.shrink(i - j); + explanation.shrink(i - j); - Debug("pf::sat") << "Solver::reason: explanation = " ; - for (int i = 0; i < explanation.size(); ++i) { - Debug("pf::sat") << explanation[i] << " "; - } - Debug("pf::sat") << std::endl; + Debug("pf::sat") << "Solver::reason: explanation = "; + for (int i = 0; i < explanation.size(); ++i) + { + Debug("pf::sat") << explanation[i] << " "; + } + Debug("pf::sat") << std::endl; - // We need an explanation clause so we add a fake literal - if (j == 1) { - // Add not TRUE to the clause - explanation.push(mkLit(varTrue, true)); + // We need an explanation clause so we add a fake literal + if (j == 1) + { + // Add not TRUE to the clause + explanation.push(mkLit(varTrue, true)); + } } // Construct the reason @@ -306,13 +341,15 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) Lit p; int i, j; // Which user-level to assert this clause at - int clauseLevel = removable ? 0 : assertionLevel; + int clauseLevel = (removable && !assertionLevelOnly()) ? 0 : assertionLevel; // Check the clause for tautologies and similar int falseLiteralsCount = 0; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { // Update the level - clauseLevel = std::max(clauseLevel, intro_level(var(ps[i]))); + clauseLevel = assertionLevelOnly() + ? assertionLevel + : std::max(clauseLevel, intro_level(var(ps[i]))); // Tautologies are ignored if (ps[i] == ~p) { id = ClauseIdUndef; @@ -1221,22 +1258,23 @@ lbool Solver::search(int nof_conflicts) PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); ) } else { - CRef cr = ca.alloc(max_level, learnt_clause, true); - clauses_removable.push(cr); - attachClause(cr); - claBumpActivity(ca[cr]); - uncheckedEnqueue(learnt_clause[0], cr); - PROOF( - ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); - PSTATS( - std::unordered_set cl_levels; - for (int i = 0; i < learnt_clause.size(); ++i) { - cl_levels.insert(level(var(learnt_clause[i]))); - } - ProofManager::getSatProof()->storeClauseGlue(id, cl_levels.size()); - ) - ProofManager::getSatProof()->endResChain(id); - ); + CRef cr = + ca.alloc(assertionLevelOnly() ? assertionLevel : max_level, + learnt_clause, + true); + clauses_removable.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); + uncheckedEnqueue(learnt_clause[0], cr); + PROOF(ClauseId id = + ProofManager::getSatProof()->registerClause(cr, LEARNT); + PSTATS(std::unordered_set cl_levels; + for (int i = 0; i < learnt_clause.size(); ++i) { + cl_levels.insert(level(var(learnt_clause[i]))); + } ProofManager::getSatProof() + ->storeClauseGlue(id, cl_levels.size());) + ProofManager::getSatProof() + ->endResChain(id);); } varDecayActivity(); @@ -1748,7 +1786,8 @@ CRef Solver::updateLemmas() { if (lemma.size() > 1) { // If the lemmas is removable, we can compute its level by the level int clauseLevel = assertionLevel; - if (removable) { + if (removable && !assertionLevelOnly()) + { clauseLevel = 0; for (int i = 0; i < lemma.size(); ++ i) { clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i]))); -- 2.30.2