From 0eb2a0362fee06023f0668e94bb566b69f4a7cda Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 12 Nov 2010 04:39:54 +0000 Subject: [PATCH] Some bug fixes in the SAT for lemmas, and an experiment with a more complete (wr propagation) splitter in arithmetic. --- src/prop/minisat/core/Solver.cc | 30 +++++++++++++++++++----------- src/prop/prop_engine.cpp | 2 +- src/theory/arith/theory_arith.cpp | 12 +++++++++++- 3 files changed, 31 insertions(+), 13 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3e1fbba17..a24772581 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -181,7 +181,6 @@ bool Solver::addClause_(vec& ps, ClauseType type) { if (!ok) return false; - // If a lemma propagates the literal, we mark this bool propagate_first_literal = false; // Check if clause is satisfied and remove false/duplicate literals: @@ -196,12 +195,15 @@ bool Solver::addClause_(vec& ps, ClauseType type) ps[j++] = p = ps[i]; ps.shrink(i - j); } else { - // Lemma - vec assigned_lits; + // Lemma + vec assigned_lits; + Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << endl; + bool lemmaSatisfied = false; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { if (ps[i] == ~p) { // We don't add clauses that represent splits directly, they are decision literals // so they will get decided upon and sent to the theory + Debug("minisat::lemmas") << "Lemma is a tautology." << endl; return true; } if (value(ps[i]) == l_Undef) { @@ -212,24 +214,24 @@ bool Solver::addClause_(vec& ps, ClauseType type) } else { // If the literal has a value it gets added to the end of the clause p = ps[i]; + if (value(p) == l_True) lemmaSatisfied = true; assigned_lits.push(p); Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << endl; } } - Assert(j >= 1, "You are asserting a falsified lemma, produce a conflict instead!"); + Assert(j >= 1 || lemmaSatisfied, "You are asserting a falsified lemma, produce a conflict instead!"); // If only one literal we could have unit propagation - if (j == 1) propagate_first_literal = true; + if (j == 1 && !lemmaSatisfied) propagate_first_literal = true; int max_level = -1; int max_level_j = -1; for (int assigned_i = 0; assigned_i < assigned_lits.size(); ++ assigned_i) { ps[j++] = p = assigned_lits[assigned_i]; - if (value(p) == l_True) propagate_first_literal = false; - else if (level(var(p)) > max_level) { + if (level(var(p)) > max_level && value(p) == l_False) { max_level = level(var(p)); max_level_j = j - 1; } } - if (value(ps[1]) != l_Undef) { + if (value(ps[1]) != l_Undef && max_level != -1) { swap(ps[1], ps[max_level_j]); } ps.shrink(i - j); @@ -343,7 +345,9 @@ void Solver::cancelUntil(int level) { propagating_lemmas[j++] = propagating_lemmas[i]; } } - propagating_lemmas.shrink(i - j); + Assert(i >= j); + propagating_lemmas.shrink(propagating_lemmas.size() - j); + Assert(propagating_lemmas_lim.size() >= level); propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level); } } @@ -960,9 +964,13 @@ lbool Solver::search(int nof_conflicts) // If we have more assertions from lemmas, we continue if (problem_extended) { + Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl; + for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) { - Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl; - uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); + if (value(var(lemma_propagated_literals[i])) == l_Undef) { + Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl; + uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); + } } lemma_propagated_literals.clear(); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 45d941553..d89b8ec2f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -82,7 +82,7 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertLemma(TNode node) { Assert(d_inCheckSat, "Sat solver should be in solve()!"); - Debug("prop::lemma") << "assertLemma(" << node << ")" << endl; + Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; // Assert as removable d_cnfStream->convertAndAssert(node, true, false); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 7b768d9af..7cedbcd20 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -416,7 +416,17 @@ void TheoryArith::check(Effort effortLevel){ Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode; - d_out->lemma(lemma); + + // < => !> + Node imp1 = NodeBuilder<2>(kind::IMPLIES) << ltNode << gtNode.notNode(); + // < => != + Node imp2 = NodeBuilder<2>(kind::IMPLIES) << ltNode << eq.notNode(); + // > => != + Node imp3 = NodeBuilder<2>(kind::IMPLIES) << gtNode << eq.notNode(); + // All the implication + Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3; + + d_out->lemma(lemma.andNode(impClosure)); } } } -- 2.30.2