From f4dbc58bf0d40fd3409f4a7003342ecaf1e2f946 Mon Sep 17 00:00:00 2001 From: msoos Date: Mon, 7 Dec 2009 20:03:13 +0000 Subject: [PATCH] Updating CryptoMiniSat2 to r577 git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@479 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/ClauseCleaner.cpp | 18 ++++++ src/sat/cryptominisat2/Conglomerate.cpp | 1 + src/sat/cryptominisat2/Solver.cpp | 25 +++++--- src/sat/cryptominisat2/Solver.h | 2 +- src/sat/cryptominisat2/VERSION | 4 +- src/sat/cryptominisat2/VarReplacer.cpp | 32 +++++++--- src/sat/cryptominisat2/VarReplacer.h | 1 + src/sat/cryptominisat2/XorFinder.cpp | 81 ------------------------ src/sat/cryptominisat2/XorFinder.h | 1 - 9 files changed, 63 insertions(+), 102 deletions(-) diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index 36d277e..e7e23cf 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -4,6 +4,8 @@ namespace MINISAT { using namespace MINISAT; +//#define DEBUG_CLEAN + ClauseCleaner::ClauseCleaner(Solver& _solver) : solver(_solver) { @@ -15,6 +17,10 @@ ClauseCleaner::ClauseCleaner(Solver& _solver) : void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) { + #ifdef DEBUG_CLEAN + assert(solver.decisionLevel() == 0); + #endif + if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num()) return; @@ -32,6 +38,10 @@ void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) { + #ifdef DEBUG_CLEAN + assert(solver.decisionLevel() == 0); + #endif + if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num()) return; @@ -76,6 +86,10 @@ bool ClauseCleaner::cleanClause(Clause& c) void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) { + #ifdef DEBUG_CLEAN + assert(solver.decisionLevel() == 0); + #endif + if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num()) return; @@ -92,6 +106,10 @@ void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) { + #ifdef DEBUG_CLEAN + assert(solver.decisionLevel() == 0); + #endif + if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num()) return; diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index e71c9c4..e4454f6 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -208,6 +208,7 @@ bool Conglomerate::dealWithNewClause(vec& ps, const bool inverted, const ui if (S->assigns[ps[0].var()] == l_Undef) { assert(S->decisionLevel() == 0); + blocked[ps[0].var()] = true; S->uncheckedEnqueue(Lit(ps[0].var(), inverted)); } else if (S->assigns[ps[0].var()] != boolToLBool(!inverted)) { #ifdef VERBOSE_DEBUG diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index d8c5a3c..59fda20 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -182,12 +182,16 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro return false; // Check if clause is satisfied and remove false/duplicate literals: + if (toReplace->getNumReplacedLits()) { + for (int i = 0; i != ps.size(); i++) { + ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); + } + } + sort(ps); Lit p; int i, j; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - if (toReplace->getNumReplacedLits()) - ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); xor_clause_inverted ^= ps[i].sign(); ps[i] ^= ps[i].sign(); @@ -259,12 +263,16 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) return false; // Check if clause is satisfied and remove false/duplicate literals: + if (toReplace->getNumReplacedLits()) { + for (int i = 0; i != ps.size(); i++) { + ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); + } + } + sort(ps); Lit p; int i, j; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - if (toReplace->getNumReplacedLits()) - ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); if (value(ps[i]) == l_True || ps[i] == ~p) return true; else if (value(ps[i]) != l_False && ps[i] != p) @@ -406,7 +414,7 @@ void Solver::cancelUntil(int level) for (int c = trail.size()-1; c >= trail_lim[level]; c--) { Var x = trail[c].var(); #ifdef VERBOSE_DEBUG - cout << "Canceling var " << x+1 << " sublevel:" << c << endl; + cout << "Canceling var " << x+1 << " sublevel: " << c << endl; #endif assigns[x] = l_Undef; insertVarOrder(x); @@ -417,7 +425,7 @@ void Solver::cancelUntil(int level) } #ifdef VERBOSE_DEBUG - cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel:" << trail.size()-1 << ")" << endl; + cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel: " << trail.size()-1 << ")" << endl; #endif } @@ -467,7 +475,7 @@ void Solver::set_gaussian_decision_until(const uint to) Lit Solver::pickBranchLit(int polarity_mode) { #ifdef VERBOSE_DEBUG - cout << "decision level:" << decisionLevel() << " "; + cout << "decision level: " << decisionLevel() << " "; #endif Var next = var_Undef; @@ -521,6 +529,7 @@ Lit Solver::pickBranchLit(int polarity_mode) } else { Lit lit(next,sign); #ifdef VERBOSE_DEBUG + assert(decision_var[lit.var()]); cout << "decided on: " << lit.var()+1 << " to set:" << !lit.sign() << endl; #endif return lit; @@ -740,7 +749,7 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) void Solver::uncheckedEnqueue(Lit p, Clause* from) { #ifdef VERBOSE_DEBUG - cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel:" << trail.size() << endl; + cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel: " << trail.size() << endl; #endif assert(value(p) == l_Undef); diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 65a0752..d6ab797 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -344,7 +344,7 @@ inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); #ifdef VERBOSE_DEBUG - cout << "New decision level:" << trail_lim.size() << endl; + cout << "New decision level: " << trail_lim.size() << endl; #endif } /*inline int Solver::nbPropagated(int level) { diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index b18870e..ddf9a02 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,3 +1,3 @@ CryptoMiniSat -SVN revision: 565 -GIT revision: a83e40474c31b7a0b902addfc37ff99a188d0ad3 +SVN revision: 577 +GIT revision: 2db0ff9414cbeae2c64bb74a0ec4fc2199b30c8a diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 62d840d..8dcabfd 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -19,6 +19,7 @@ namespace MINISAT VarReplacer::VarReplacer(Solver *_S) : replacedLits(0) , replacedVars(0) + , lastReplacedVars(0) , addedNewClause(false) , S(_S) { @@ -34,13 +35,6 @@ void VarReplacer::performReplace() { #ifdef VERBOSE_DEBUG cout << "Replacer started." << endl; - { - uint i = 0; - for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { - if (it->var() == i) continue; - cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") << it->var()+1 << endl; - } - } #endif S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses); @@ -51,12 +45,25 @@ void VarReplacer::performReplace() S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts); S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); - if (!addedNewClause || replacedVars == 0) return; + if (!addedNewClause && replacedVars == lastReplacedVars) return; + + #ifdef VERBOSE_DEBUG + { + uint i = 0; + for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { + if (it->var() == i) continue; + cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") << it->var()+1 << endl; + } + } + #endif uint i = 0; const vector& removedVars = S->conglomerate->getRemovedVars(); for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { if (it->var() == i) continue; + #ifdef VERBOSE_DEBUG + cout << "Setting var " << i+1 << " to a non-decision var" << endl; + #endif S->setDecisionVar(i, false); if (!removedVars[it->var()]) S->setDecisionVar(it->var(), true); @@ -76,6 +83,7 @@ void VarReplacer::performReplace() printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits); addedNewClause = false; + lastReplacedVars = replacedVars; if (S->ok) S->ok = (S->propagate() == NULL); @@ -105,6 +113,7 @@ void VarReplacer::replace_set(vec& cs, const bool isAttached) if (isAttached && changed && handleUpdatedClause(c, origVar1, origVar2)) { c.mark(1); + S->freeLater.push(&c); r++; } else { *a++ = *r++; @@ -133,6 +142,11 @@ const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, co } c.shrink(i - j); + #ifdef VERBOSE_DEBUG + cout << "xor-clause after replacing: "; + c.plain_print(); + #endif + switch (c.size()) { case 0: S->detachModifiedClause(origVar1, origVar2, origSize, &c); @@ -293,7 +307,7 @@ void VarReplacer::extendModel() const void VarReplacer::replace(vec& ps, const bool xor_clause_inverted, const uint group) { #ifdef VERBOSE_DEBUG - cout << "replace() called with var " << ps[0]+1 << " and var " << ps[1]+1 << " with xor_clause_inverted " << xor_clause_inverted << endl; + cout << "replace() called with var " << ps[0].var()+1 << " and var " << ps[1].var()+1 << " with xor_clause_inverted " << xor_clause_inverted << endl; #endif #ifdef DEBUG_REPLACER diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 6739304..a61b99b 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -49,6 +49,7 @@ class VarReplacer uint replacedLits; uint replacedVars; + uint lastReplacedVars; bool addedNewClause; Solver* S; }; diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 4490a22..c61a12d 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -68,87 +68,6 @@ uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSiz return found; } -uint XorFinder::doByPart(uint& sumLengths, const uint minSize, const uint maxSize) -{ - toRemove.clear(); - toRemove.resize(cls.size(), false); - - uint sumUsage = 0; - vector varUsage(S->nVars(), 0); - for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++) { - const uint size = (*it)->size(); - if ( size > maxSize || size < minSize) continue; - - for (const Lit *l = &(**it)[0], *end = l + size; l != end; l++) { - varUsage[l->var()]++; - sumUsage++; - } - } - - uint found = 0; - #ifdef VERBOSE_DEBUG - uint sumNumClauses = 0; - #endif - - const uint limit = 800000; - uint from = 0; - uint until = 0; - while (until < varUsage.size()) { - uint estimate = 0; - for (; until < varUsage.size(); until++) { - estimate += varUsage[until]; - if (estimate >= limit) break; - } - #ifdef VERBOSE_DEBUG - printf("Xor-finding: Vars from: %d, until: %d\n", from, until); - uint numClauses = 0; - #endif - - table.clear(); - table.reserve(estimate/2); - uint i = 0; - for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++, i++) { - if (toRemove[i]) continue; - const uint size = (*it)->size(); - if ( size > maxSize || size < minSize) continue; - - for (Lit *l = &(**it)[0], *end = l + size; l != end; l++) { - if (l->var() >= from && l->var() <= until) { - table.push_back(make_pair(*it, i)); - #ifdef VERBOSE_DEBUG - numClauses++; - #endif - break; - } - } - } - #ifdef VERBOSE_DEBUG - printf("numClauses in range: %d\n", numClauses); - sumNumClauses += numClauses; - #endif - - uint lengths; - found += findXors(lengths); - sumLengths += lengths; - #ifdef VERBOSE_DEBUG - printf("Found in this range: %d\n", found); - #endif - - from = until+1; - } - - clearToRemove(); - - if (S->ok != false) - S->ok = (S->propagate() == NULL); - - #ifdef VERBOSE_DEBUG - cout << "Overdone work due to partitioning:" << (double)sumNumClauses/(double)cls.size() << "x" << endl; - #endif - - return found; -} - uint XorFinder::findXors(uint& sumLengths) { #ifdef VERBOSE_DEBUG diff --git a/src/sat/cryptominisat2/XorFinder.h b/src/sat/cryptominisat2/XorFinder.h index 11d2624..9ba3104 100644 --- a/src/sat/cryptominisat2/XorFinder.h +++ b/src/sat/cryptominisat2/XorFinder.h @@ -34,7 +34,6 @@ class XorFinder public: XorFinder(Solver* S, vec& cls); - uint doByPart(uint& sumLengths, const uint minSize, const uint maxSize); uint doNoPart(uint& sumLengths, const uint minSize, const uint maxSize); private: -- 2.47.3