From: msoos Date: Thu, 10 Dec 2009 15:19:30 +0000 (+0000) Subject: Updating CryptoMiniSat2 to r614. dynamicRestart is now automatic, and turns off gauss... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=aa83f558f4fd15ace513aef752801d7fef98f2ed;p=francis%2Fstp.git Updating CryptoMiniSat2 to r614. dynamicRestart is now automatic, and turns off gauss automatically. Cleanclauses and performReplace are now used only when they seem to provide benefit. Gauss depth is now set to 100 in STP. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@497 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index d5ff134..a9ad03f 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -21,17 +21,15 @@ namespace BEEV { bm->CreateNode(NOT, query)); //solver instantiated here -#if defined CORE || defined CRYPTOMINISAT +#if defined CORE || defined CRYPTOMINISAT || defined CRYPTOMINISAT2 MINISAT::Solver NewSolver; #endif #if defined CRYPTOMINISAT2 - MINISAT::Solver NewSolver; if(bm->UserFlags.print_cnf_flag) { NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename); } - NewSolver.dynamicRestarts = false; #endif #ifdef SIMP diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index 114a3df..5a376a7 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -32,13 +32,13 @@ ClauseCleaner::ClauseCleaner(Solver& _solver) : } } -void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) +void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, const uint limit) { #ifdef DEBUG_CLEAN assert(solver.decisionLevel() == 0); #endif - if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num()) + if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num()) return; int i,j; @@ -53,13 +53,13 @@ void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); } -void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) +void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, const uint limit) { #ifdef DEBUG_CLEAN assert(solver.decisionLevel() == 0); #endif - if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num()) + if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num()) return; int i,j; @@ -74,110 +74,123 @@ void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type) lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); } -bool ClauseCleaner::cleanClause(Clause& c) +inline const bool ClauseCleaner::cleanClause(Clause& c) { - assert(c.size() >= 2); - Lit first = c[0]; - Lit second = c[1]; + Lit origLit1 = c[0]; + Lit origLit2 = c[1]; + uint32_t origSize = c.size(); Lit *i, *j, *end; - uint at = 0; - for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { - if (solver.value(*i) == l_Undef) { + for (i = j = c.getData(), end = i + c.size(); i != end; i++) { + lbool val = solver.value(*i); + if (val == l_Undef) { *j = *i; j++; - } else assert(at > 1); - assert(solver.value(*i) != l_True); + } + if (val == l_True) { + solver.detachModifiedClause(origLit1, origLit2, origSize, &c); + return true; + } } + if ((c.size() > 2) && (c.size() - (i-j) == 2)) { - solver.detachModifiedClause(first, second, c.size(), &c); + solver.detachModifiedClause(origLit1, origLit2, c.size(), &c); c.shrink(i-j); solver.attachClause(c); } else c.shrink(i-j); - assert(c.size() > 1); - - return (i-j > 0); + return false; } -void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) +void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type, const uint limit) { #ifdef DEBUG_CLEAN assert(solver.decisionLevel() == 0); #endif - if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num()) + if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num()) return; - uint useful = 0; - for (int s = 0; s < cs.size(); s++) - useful += cleanClause(*cs[s]); + Clause **s, **ss, **end; + for (s = ss = cs.getData(), end = s + cs.size(); s != end;) { + if (cleanClause(**s)) { + free(*s); + s++; + } else { + *ss++ = *s++; + } + } + cs.shrink(s-ss); lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); #ifdef VERBOSE_DEBUG - cout << "cleanClauses(Clause) useful:" << useful << endl; + cout << "cleanClauses(Clause) useful ?? Removed: " << s-ss << endl; #endif } -void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) +void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type, const uint limit) { #ifdef DEBUG_CLEAN assert(solver.decisionLevel() == 0); #endif - if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num()) + if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num()) return; - uint useful = 0; XorClause **s, **ss, **end; for (s = ss = cs.getData(), end = s + cs.size(); s != end;) { - XorClause& c = **s; - #ifdef VERBOSE_DEBUG - std::cout << "Cleaning clause:"; - c.plain_print(); - solver.printClause(c);std::cout << std::endl; - #endif - - Lit *i, *j, *end; - uint at = 0; - for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { - const lbool& val = solver.assigns[i->var()]; - if (val.isUndef()) { - *j = *i; - j++; - } else /*assert(at>1),*/ c.invert(val.getBool()); - } - c.shrink(i-j); - if (i-j > 0) useful++; - - if (c.size() == 2) { - vec ps(2); - ps[0] = c[0].unsign(); - ps[1] = c[1].unsign(); - solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.group); - solver.removeClause(c); + if (cleanClause(**s)) { + (**s).mark(1); + solver.freeLater.push(*s); s++; - } else + } else { *ss++ = *s++; - - #ifdef VERBOSE_DEBUG - std::cout << "Cleaned clause:"; - c.plain_print(); - solver.printClause(c);std::cout << std::endl; - #endif - assert(c.size() > 1); + } } cs.shrink(s-ss); lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); #ifdef VERBOSE_DEBUG - cout << "cleanClauses(XorClause) useful:" << useful << endl; + cout << "cleanClauses(XorClause) useful: ?? Removed: " << s-ss << endl; #endif } +inline const bool ClauseCleaner::cleanClause(XorClause& c) +{ + Lit *i, *j, *end; + Var origVar1 = c[0].var(); + Var origVar2 = c[1].var(); + uint32_t origSize = c.size(); + for (i = j = c.getData(), end = i + c.size(); i != end; i++) { + const lbool& val = solver.assigns[i->var()]; + if (val.isUndef()) { + *j = *i; + j++; + } else c.invert(val.getBool()); + } + c.shrink(i-j); + + switch (c.size()) { + case 0: { + solver.detachModifiedClause(origVar1, origVar2, origSize, &c); + return true; + } + case 2: { + vec ps(2); + ps[0] = c[0].unsign(); + ps[1] = c[1].unsign(); + solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.group); + solver.detachModifiedClause(origVar1, origVar2, origSize, &c); + return true; + } + default: + return false; + } +} + bool ClauseCleaner::satisfied(const Clause& c) const { for (uint i = 0; i < c.size(); i++) diff --git a/src/sat/cryptominisat2/ClauseCleaner.h b/src/sat/cryptominisat2/ClauseCleaner.h index f9a66d1..d59948e 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.h +++ b/src/sat/cryptominisat2/ClauseCleaner.h @@ -30,15 +30,17 @@ class ClauseCleaner enum ClauseSetType {clauses, xorclauses, learnts, conglomerate}; - void cleanClauses(vec& cs, ClauseSetType type); - void cleanClauses(vec& cs, ClauseSetType type); - void removeSatisfied(vec& cs, ClauseSetType type); - void removeSatisfied(vec& cs, ClauseSetType type); + void cleanClauses(vec& cs, ClauseSetType type, const uint limit = 0); + void cleanClauses(vec& cs, ClauseSetType type, const uint limit = 0); + void removeSatisfied(vec& cs, ClauseSetType type, const uint limit = 0); + void removeSatisfied(vec& cs, ClauseSetType type, const uint limit = 0); + void removeAndCleanAll(); bool satisfied(const Clause& c) const; bool satisfied(const XorClause& c) const; private: - bool cleanClause(Clause& c); + const bool cleanClause(Clause& c); + const bool cleanClause(XorClause& c); uint lastNumUnitarySat[4]; uint lastNumUnitaryClean[4]; @@ -46,6 +48,15 @@ class ClauseCleaner Solver& solver; }; -}; +inline void ClauseCleaner::removeAndCleanAll() +{ + uint limit = (double)solver.order_heap.size() * PERCENTAGEPERFORMREPLACE; + + cleanClauses(solver.clauses, ClauseCleaner::clauses, limit); + cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses, limit); + cleanClauses(solver.learnts, ClauseCleaner::learnts, limit); +} + +}; #endif //CLAUSECLEANER_H diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index f8ecf0c..0694463 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -120,7 +120,6 @@ uint Conglomerate::conglomerateXors() cout << "Finding conglomerate xors started" << endl; #endif - S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses); S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); toRemove.clear(); diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index f589ee8..bfbd7a5 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -79,11 +79,11 @@ inline void Gaussian::set_matrixset_to_cur() llbool Gaussian::full_init() { if (!should_init()) return l_Nothing; + reset_stats(); bool do_again_gauss = true; while (do_again_gauss) { do_again_gauss = false; - solver.clauseCleaner->removeSatisfied(solver.xorclauses, ClauseCleaner::xorclauses); solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); init(); Clause* confl; diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h index 00e9eb5..a6f5eb6 100644 --- a/src/sat/cryptominisat2/Gaussian.h +++ b/src/sat/cryptominisat2/Gaussian.h @@ -53,7 +53,6 @@ public: //statistics void print_stats() const; - void reset_stats(); void print_matrix_stats() const; const uint get_called() const; const uint get_useful_prop() const; @@ -144,6 +143,7 @@ protected: bool should_init() const; bool should_check_gauss(const uint decisionlevel, const uint starts) const; void disable_if_necessary(); + void reset_stats(); private: diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index 064dfea..70bec67 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -2,7 +2,7 @@ include ../../../scripts/Makefile.common MTL = mtl MTRAND = MTRand -SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp ClauseCleaner.cpp +SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp ClauseCleaner.cpp RestartTypeChooser.cpp OBJECTS = $(SOURCES:.cpp=.o) LIB = libminisat.a CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp index f4acd1d..07d1ff8 100644 --- a/src/sat/cryptominisat2/MatrixFinder.cpp +++ b/src/sat/cryptominisat2/MatrixFinder.cpp @@ -80,7 +80,6 @@ const uint MatrixFinder::findMatrixes() if (S->xorclauses.size() == 0) return 0; - S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses); S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) { @@ -188,10 +187,10 @@ const uint MatrixFinder::setMatrixes() realMatrixNum++; } else { - if (S->verbosity >=1) + if (S->verbosity >=1 && numXorInMatrix[a].second >= 20) cout << "| Unused Matrix "; } - if (S->verbosity >=1) { + if (S->verbosity >=1 && numXorInMatrix[a].second >= 20) { cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size(); cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%"; cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg; diff --git a/src/sat/cryptominisat2/RestartTypeChooser.cpp b/src/sat/cryptominisat2/RestartTypeChooser.cpp new file mode 100644 index 0000000..afeb9c5 --- /dev/null +++ b/src/sat/cryptominisat2/RestartTypeChooser.cpp @@ -0,0 +1,87 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#include "RestartTypeChooser.h" +#include "Solver.h" + +//#define VERBOSE_DEBUG + +namespace MINISAT +{ +using namespace MINISAT; + +RestartTypeChooser::RestartTypeChooser(const Solver* const _S) : + S(_S) + , topX(100) + , limit(40) +{ +} + +const RestartType RestartTypeChooser::choose() +{ + firstVarsOld = firstVars; + calcHeap(); + uint sameIn = 0; + if (!firstVarsOld.empty()) { + for (uint i = 0; i < 100; i++) { + if (std::find(firstVars.begin(), firstVars.end(), firstVarsOld[i]) != firstVars.end()) + sameIn++; + } + #ifdef VERBOSE_DEBUG + std::cout << " Same vars in first&second first 100: " << sameIn << std::endl; + #endif + sameIns.push_back(sameIn); + } else + return static_restart; + + #ifdef VERBOSE_DEBUG + std::cout << "Avg same vars in first&second first 100: " << avg() << std::endl; + #endif + + if (avg() > (double)limit) + return static_restart; + else + return dynamic_restart; +} + +const double RestartTypeChooser::avg() const +{ + double sum = 0.0; + for (uint i = 0; i != sameIns.size(); i++) + sum += sameIns[i]; + return (sum/(double)sameIns.size()); +} + +void RestartTypeChooser::calcHeap() +{ + firstVars.resize(100); + #ifdef VERBOSE_DEBUG + std::cout << "First vars:" << std::endl; + #endif + Heap tmp(S->order_heap); + for (uint i = 0; i != 100; i++) { + #ifdef VERBOSE_DEBUG + std::cout << tmp.removeMin()+1 << ", "; + #endif + firstVars[i] = tmp.removeMin(); + } + #ifdef VERBOSE_DEBUG + std::cout << std::endl; + #endif +} + +}; diff --git a/src/sat/cryptominisat2/RestartTypeChooser.h b/src/sat/cryptominisat2/RestartTypeChooser.h new file mode 100644 index 0000000..0ec37c3 --- /dev/null +++ b/src/sat/cryptominisat2/RestartTypeChooser.h @@ -0,0 +1,51 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef RESTARTTYPECHOOSER_H +#define RESTARTTYPECHOOSER_H + +#include "SolverTypes.h" +#include +#include +using std::vector; + +namespace MINISAT +{ + +class Solver; + +class RestartTypeChooser +{ + public: + RestartTypeChooser(const Solver* const S); + const RestartType choose(); + + private: + void calcHeap(); + const double avg() const; + + const Solver* const S; + const uint topX; + const uint limit; + vector sameIns; + + vector firstVars, firstVarsOld; +}; + +}; + +#endif //RESTARTTYPECHOOSER_H diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index e76028c..e3fc0bf 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -37,6 +37,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Conglomerate.h" #include "XorFinder.h" #include "ClauseCleaner.h" +#include "RestartTypeChooser.h" namespace MINISAT { @@ -57,11 +58,10 @@ Solver::Solver() : , polarity_mode (polarity_user) , verbosity (0) , restrictedPickBranch(0) - , useRealUnknowns (false) , xorFinder (true) , performReplace (true) , greedyUnbound (false) - , dynamicRestarts (false) + , restartType (static_restart) // Statistics: (formerly in 'SolverStats') // @@ -102,7 +102,7 @@ Solver::~Solver() for (int i = 0; i < learnts.size(); i++) free(learnts[i]); for (int i = 0; i < clauses.size(); i++) free(clauses[i]); for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]); - for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; + clearGaussMatrixes(); for (uint i = 0; i < freeLater.size(); i++) free(freeLater[i]); delete varReplacer; delete conglomerate; @@ -184,9 +184,10 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro p = lit_Undef; if (!assigns[ps[i].var()].isUndef()) xor_clause_inverted ^= assigns[ps[i].var()].getBool(); - } else if (value(ps[i]) == l_Undef) //just add + } else if (assigns[ps[i].var()].isUndef()) //just add ps[j++] = p = ps[i]; - else xor_clause_inverted ^= (value(ps[i]) == l_True); //modify xor_clause_inverted instead of adding + else //modify xor_clause_inverted instead of adding + xor_clause_inverted ^= (assigns[ps[i].var()].getBool()); } ps.shrink(i - j); @@ -199,7 +200,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro return ok = false; } case 1: { - assert(value(ps[0]) == l_Undef); + assert(assigns[ps[0].var()].isUndef()); uncheckedEnqueue(ps[0] ^ xor_clause_inverted); if (dynamic_behaviour_analysis) logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::add_clause_type, group); @@ -256,7 +257,7 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) Lit p; int i, j; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - if (value(ps[i]) == l_True || ps[i] == ~p) + if (value(ps[i]).getBool() || ps[i] == ~p) return true; else if (value(ps[i]) != l_False && ps[i] != p) ps[j++] = p = ps[i]; @@ -412,13 +413,6 @@ void Solver::cancelUntil(int level) #endif } -void Solver::setRealUnknown(const uint var) -{ - if (realUnknowns.size() < var+1) - realUnknowns.resize(var+1, false); - realUnknowns[var] = true; -} - void Solver::printLit(const Lit l) const { printf("%s%d:%c", l.sign() ? "-" : "", l.var()+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X')); @@ -435,6 +429,13 @@ void Solver::set_gaussian_decision_until(const uint to) gaussconfig.decision_until = to; } +void Solver::clearGaussMatrixes() +{ + for (uint i = 0; i < gauss_matrixes.size(); i++) + delete gauss_matrixes[i]; + gauss_matrixes.clear(); +} + //================================================================================================= // Major methods: @@ -543,8 +544,7 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int const uint my_var = q.var(); if (!seen[my_var] && level[my_var] > 0) { - if (!useRealUnknowns || (my_var < realUnknowns.size() && realUnknowns[my_var])) - varBumpActivity(my_var); + varBumpActivity(my_var); seen[my_var] = 1; if (level[my_var] >= decisionLevel()) { pathC++; @@ -719,7 +719,7 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from) cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel: " << trail.size() << endl; #endif - assert(value(p) == l_Undef); + assert(assigns[p.var()].isUndef()); const Var v = p.var(); assigns [v] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient level [v] = decisionLevel(); @@ -760,13 +760,12 @@ Clause* Solver::propagate(const bool xor_as_well) for(WatchedBin *k = wbin.getData(), *end = k + wbin.size(); k != end; k++) { Lit imp = k->impliedLit; lbool val = value(imp); - if (val == l_False) - return k->clause; - if (val == l_Undef) { + if (val.isUndef()) { uncheckedEnqueue(imp, k->clause); if (dynamic_behaviour_analysis) logger.propagation(imp, Logger::simple_propagation_type, k->clause->group); - } + } else if (val == l_False) + return k->clause; } //Next, propagate normal clauses @@ -791,7 +790,7 @@ Clause* Solver::propagate(const bool xor_as_well) *j++ = &c; } else { // Look for new watch: - for (uint k = 2; k != c.size(); k++) + for (int k = 2; k != c.size(); k++) if (value(c[k]) != l_False) { c[1] = c[k]; c[k] = false_lit; @@ -1134,7 +1133,8 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) { // Reached bound on number of conflicts? - if (dynamicRestarts) { + switch (restartType) { + case dynamic_restart: if (nbDecisionLevelHistory.isvalid() && ((nbDecisionLevelHistory.getavg()*0.7) > (totalSumOfDecisionLevel / conf4Stats))) { nbDecisionLevelHistory.fastclear(); @@ -1145,7 +1145,8 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) } return l_Undef; } - } else { + break; + case static_restart: if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { progress_estimate = progressEstimate(); cancelUntil(0); @@ -1153,6 +1154,7 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) logger.end(Logger::restarting); return l_Undef; } + break; } // Simplify the set of problem clauses: @@ -1237,7 +1239,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf learnt_clause.clear(); analyze(confl, learnt_clause, backtrack_level, nbLevels); conf4Stats++; - if (dynamicRestarts) { + if (restartType == dynamic_restart) { nbDecisionLevelHistory.push(nbLevels); totalSumOfDecisionLevel += nbLevels; } @@ -1331,57 +1333,55 @@ void Solver::print_gauss_sum_stats() const } } -lbool Solver::solve(const vec& assumps) +inline void Solver::chooseRestartType(const lbool& status, RestartTypeChooser& restartTypeChooser) { - if (libraryCNFFile) - fprintf(libraryCNFFile, "c Solver::solve() called\n"); - - model.clear(); - conflict.clear(); - if (dynamicRestarts) { - nbDecisionLevelHistory.fastclear(); - nbDecisionLevelHistory.initSize(100); - totalSumOfDecisionLevel = 0; + if (status.isUndef() && starts > 2 && starts < 8) { + RestartType tmp = restartTypeChooser.choose(); + if (starts == 7) { + if (tmp == dynamic_restart) { + nbDecisionLevelHistory.fastclear(); + nbDecisionLevelHistory.initSize(100); + totalSumOfDecisionLevel = 0; + clearGaussMatrixes(); + if (verbosity >= 1) + printf("| Decided on dynamic restart strategy |\n"); + } else { + if (verbosity >= 1) + printf("| Decided on static restart strategy |\n"); + } + restartType = tmp; + } + } else { + #ifdef VERBOSE_DEBUG + restartTypeChooser.choose(); + #endif } +} - if (!ok) return l_False; - - assumps.copyTo(assumptions); - - double nof_conflicts = restart_first; - lbool status = l_Undef; - - if (nClauses() * learntsize_factor < nbclausesbeforereduce) { - if (nClauses() * learntsize_factor < nbclausesbeforereduce/2) - nbclausesbeforereduce = nbclausesbeforereduce/4; - else - nbclausesbeforereduce = (nClauses() * learntsize_factor)/2; - } - - conglomerate->addRemovedClauses(); - - if (performReplace) { +inline void Solver::performStepsBeforeSolve() +{ + if (performReplace + && ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) { varReplacer->performReplace(); - if (!ok) return l_False; + if (!ok) return; } - + if (xorFinder) { double time; if (clauses.size() < 400000) { time = cpuTime(); - clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses); - clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses); uint sumLengths = 0; XorFinder xorFinder(this, clauses); uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10); - if (!ok) return l_False; + if (!ok) return; if (verbosity >=1) printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); - if (performReplace) { + if (performReplace + && ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) { varReplacer->performReplace(); - if (!ok) return l_False; + if (!ok) return; } } @@ -1396,7 +1396,7 @@ lbool Solver::solve(const vec& assumps) uint foundCong = conglomerate->conglomerateXors(); if (verbosity >=1) printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong); - if (!ok) return l_False; + if (!ok) return; uint new_total = 0; uint new_num_cls = xorclauses.size(); @@ -1408,9 +1408,10 @@ lbool Solver::solve(const vec& assumps) printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total); } - if (performReplace) { + if (performReplace + && ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) { varReplacer->performReplace(); - if (!ok) return l_False; + if (!ok) return; } } } @@ -1422,6 +1423,36 @@ lbool Solver::solve(const vec& assumps) if (verbosity >=1) printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes); } +} + +lbool Solver::solve(const vec& assumps) +{ + if (libraryCNFFile) + fprintf(libraryCNFFile, "c Solver::solve() called\n"); + + model.clear(); + conflict.clear(); + clearGaussMatrixes(); + restartType = static_restart; + conglomerate->addRemovedClauses(); + starts = 0; + + if (!ok) return l_False; + + assumps.copyTo(assumptions); + + double nof_conflicts = restart_first; + lbool status = l_Undef; + + if (nClauses() * learntsize_factor < nbclausesbeforereduce) { + if (nClauses() * learntsize_factor < nbclausesbeforereduce/2) + nbclausesbeforereduce = nbclausesbeforereduce/4; + else + nbclausesbeforereduce = (nClauses() * learntsize_factor)/2; + } + + performStepsBeforeSolve(); + if (!ok) return l_False; if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { @@ -1433,28 +1464,24 @@ lbool Solver::solve(const vec& assumps) if (dynamic_behaviour_analysis) logger.end(Logger::done_adding_clauses); - + + RestartTypeChooser restartTypeChooser(this); + // Search: while (status == l_Undef && starts < maxRestarts) { - clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses); - clauseCleaner->removeSatisfied(xorclauses, ClauseCleaner::xorclauses); - clauseCleaner->removeSatisfied(learnts, ClauseCleaner::learnts); - - clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses); - clauseCleaner->cleanClauses(xorclauses, ClauseCleaner::xorclauses); - clauseCleaner->cleanClauses(learnts, ClauseCleaner::learnts); + clauseCleaner->removeAndCleanAll(); if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nbclausesbeforereduce*curRestart, nLearnts(), (double)learnts_literals/nLearnts()); print_gauss_sum_stats(); } - for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++) - (*gauss)->reset_stats(); if (dynamic_behaviour_analysis) logger.begin(); status = search((int)nof_conflicts); nof_conflicts *= restart_inc; + + chooseRestartType(status, restartTypeChooser); } if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { @@ -1577,4 +1604,5 @@ void Solver::checkLiteralCount() } } + }; diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 5c407d9..4ab8561 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -37,6 +37,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Logger.h" #include "constants.h" #include "BoundedQueue.h" +#include "RestartTypeChooser.h" #ifdef _MSC_VER #include @@ -96,8 +97,6 @@ public: void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. void setSeed (const uint32_t seed); // Sets the seed to be the given number - void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown - void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on) void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value void set_gaussian_decision_until(const uint to); template @@ -137,13 +136,11 @@ public: int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0) Var restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all]) - bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true - vector realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable bool xorFinder; // Automatically find xor-clauses and convert them bool performReplace; // Should var-replacing be performed? friend class FindUndef; bool greedyUnbound; //If set, then variables will be greedily unbounded (set to l_Undef) - bool dynamicRestarts; // If set to true, the restart strategy will be dynamic + RestartType restartType; // If set to true, the restart strategy will be dynamic enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 }; @@ -169,6 +166,7 @@ protected: vector gauss_matrixes; GaussianConfig gaussconfig; void print_gauss_sum_stats() const; + void clearGaussMatrixes(); friend class Gaussian; @@ -296,9 +294,12 @@ protected: friend class MatrixFinder; friend class VarReplacer; friend class ClauseCleaner; + friend class RestartTypeChooser; Conglomerate* conglomerate; VarReplacer* varReplacer; ClauseCleaner* clauseCleaner; + void chooseRestartType(const lbool& status, RestartTypeChooser& restartTypeChooser); + void performStepsBeforeSolve(); // Debug: void printLit (const Lit l) const; @@ -431,10 +432,6 @@ inline void Solver::setVariableName(int var, char* name) if (dynamic_behaviour_analysis) logger.set_variable_name(var, name); } // Sets the varible 'var'-s name to 'name' in the logger -inline void Solver::needRealUnknowns() -{ - useRealUnknowns = true; -} inline const uint Solver::get_unitary_learnts_num() const { if (decisionLevel() > 0) diff --git a/src/sat/cryptominisat2/SolverTypes.h b/src/sat/cryptominisat2/SolverTypes.h index c95be2e..cb5d252 100644 --- a/src/sat/cryptominisat2/SolverTypes.h +++ b/src/sat/cryptominisat2/SolverTypes.h @@ -39,6 +39,7 @@ using namespace MINISAT; typedef uint32_t Var; #define var_Undef (0xffffffffU >>1) +enum RestartType {dynamic_restart, static_restart}; class Lit { diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 9476115..ab0c398 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,3 +1,3 @@ CryptoMiniSat -SVN revision: 594 -GIT revision: 4b4477ffe685caf5a034f65063c93c20929440f8 +SVN revision: 614 +GIT revision: 7c6e2b5d2a1d4da60a0d70a3f0745c69f12d8ed2 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index a8b9379..ba12931 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -54,10 +54,6 @@ void VarReplacer::performReplace() cout << "Replacer started." << endl; #endif - S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses); - S->clauseCleaner->removeSatisfied(S->learnts, ClauseCleaner::learnts); - S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses); - S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses); S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts); S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses); @@ -283,6 +279,11 @@ const uint VarReplacer::getNumLastReplacedVars() const return lastReplacedVars; } +const uint VarReplacer::getNewToReplaceVars() const +{ + return replacedVars-lastReplacedVars; +} + const vector& VarReplacer::getReplaceTable() const { return table; diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 278baa4..c13f9ec 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -45,6 +45,7 @@ class VarReplacer const uint getNumReplacedLits() const; const uint getNumReplacedVars() const; const uint getNumLastReplacedVars() const; + const uint getNewToReplaceVars() const; const vector getReplacingVars() const; const vector& getReplaceTable() const; const vec& getClauses() const; diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 1dabb10..ba263fe 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -22,6 +22,7 @@ along with this program. If not, see . #include #include "Solver.h" #include "VarReplacer.h" +#include "ClauseCleaner.h" namespace MINISAT { @@ -45,6 +46,8 @@ XorFinder::XorFinder(Solver* _S, vec& _cls) : uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSize) { + S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses); + toRemove.clear(); toRemove.resize(cls.size(), false); diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h index 0633f0f..7936493 100644 --- a/src/sat/cryptominisat2/constants.h +++ b/src/sat/cryptominisat2/constants.h @@ -21,6 +21,5 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define RATIOREMOVECLAUSES 2 #define NBCLAUSESBEFOREREDUCE 20000 #define DYNAMICNBLEVEL -#define CONSTANTREMOVECLAUSE #define UPDATEVARACTIVITY -#define BLOCK +#define PERCENTAGEPERFORMREPLACE 0.03 diff --git a/src/sat/cryptominisat2/mtl/Heap.h b/src/sat/cryptominisat2/mtl/Heap.h index 6647a94..dcea08f 100644 --- a/src/sat/cryptominisat2/mtl/Heap.h +++ b/src/sat/cryptominisat2/mtl/Heap.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define Heap_h #include "Vec.h" +#include "string.h" namespace MINISAT { @@ -76,6 +77,12 @@ class Heap { public: Heap(const Comp& c) : lt(c) { } + Heap(const Heap& other) : lt(other.lt) { + heap.growTo(other.heap.size()); + memcpy(heap.getData(), other.heap.getData(), sizeof(int)*other.heap.size()); + indices.growTo(other.indices.size()); + memcpy(indices.getData(), other.indices.getData(), sizeof(int)*other.indices.size()); + } int size () const { return heap.size(); } bool empty () const { return heap.size() == 0; } diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 262d827..3a257cb 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -136,7 +136,7 @@ namespace BEEV #endif #if defined CRYPTOMINISAT2 - //newSolver.set_gaussian_decision_until(50); + newSolver.set_gaussian_decision_until(100); newSolver.performReplace = false; newSolver.xorFinder = false; #endif