From: msoos Date: Thu, 22 Apr 2010 11:34:23 +0000 (+0000) Subject: Updating CMS2 to fix some bugs X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=238d688c137cacb67e5ab3d0682a5ab36c2984c7;p=francis%2Fstp.git Updating CMS2 to fix some bugs * Conglomerate was freeing the same clause. Fixed. * Gaussian elimination is now disabled (was broken) * Some code cleanup * After solution extension, propagate was not called when decisionLevel was 0. This lead to assertion failure when adding clause during library usage git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@699 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index d147e17..e9d5479 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -46,14 +46,14 @@ void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, con if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num()) return; - int i,j; + uint32_t i,j; for (i = j = 0; i < cs.size(); i++) { if (satisfied(*cs[i])) solver.removeClause(*cs[i]); else cs[j++] = cs[i]; } - cs.shrink_(i - j); + cs.shrink(i - j); lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); } diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index 770c88a..96855d7 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -505,8 +505,7 @@ const bool Conglomerate::addRemovedClauses() FILE* backup_libraryCNFfile = solver.libraryCNFFile; solver.libraryCNFFile = NULL; if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) { - for (;it != end; it++) - free(&c); + for (;it != end; it++) free(*it); calcAtFinish.clear(); return false; } diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp index 171f9c7..da5f5ad 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.cpp +++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp @@ -304,7 +304,7 @@ end: if (solver.ok && (numFailed || goodBothSame)) { double time = cpuTime(); - if ((int)origHeapSize - (int)solver.order_heap.size() > origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) { + if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) { solver.clauses_literals = 0; solver.learnts_literals = 0; for (uint32_t i = 0; i < solver.nVars(); i++) { diff --git a/src/sat/cryptominisat2/FindUndef.cpp b/src/sat/cryptominisat2/FindUndef.cpp index 4e35dc1..836dc6b 100644 --- a/src/sat/cryptominisat2/FindUndef.cpp +++ b/src/sat/cryptominisat2/FindUndef.cpp @@ -36,7 +36,7 @@ void FindUndef::fillPotential() int trail = solver.decisionLevel()-1; while(trail > 0) { - assert(trail < solver.trail_lim.size()); + assert(trail < (int)solver.trail_lim.size()); uint at = solver.trail_lim[trail]; assert(at > 0); diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index 441b4a0..d7deda8 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -759,13 +759,16 @@ void Logger::printstats() const print_assign_var_order(); print_branch_depth_distrib(); print_learnt_clause_distrib(); + #ifdef USE_GAUSS print_matrix_stats(); + #endif //USE_GAUSS print_learnt_unitaries(0," Unitary clauses learnt until now"); print_learnt_unitaries(last_unitary_learnt_clauses, " Unitary clauses during this restart"); print_advanced_stats(); print_general_stats(); } +#ifdef USE_GAUSS void Logger::print_matrix_stats() const { print_footer(); @@ -795,6 +798,7 @@ void Logger::print_matrix_stats() const print_footer(); } +#endif //USE_GAUSS void Logger::print_advanced_stats() const { diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index 8315c29..0118702 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -3,7 +3,7 @@ include $(TOP)/scripts/Makefile.common MTL = mtl MTRAND = MTRand -SOURCES = Logger.cpp Solver.cpp Gaussian.cpp PackedRow.cpp XorFinder.cpp Conglomerate.cpp MatrixFinder.cpp VarReplacer.cpp FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp Clause.cpp FailedVarSearcher.cpp PartFinder.cpp Subsumer.cpp PartHandler.cpp XorSubsumer.cpp +SOURCES = Logger.cpp Solver.cpp PackedRow.cpp XorFinder.cpp Conglomerate.cpp VarReplacer.cpp FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp Clause.cpp FailedVarSearcher.cpp PartFinder.cpp Subsumer.cpp PartHandler.cpp XorSubsumer.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/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 4b0d541..b08fb5c 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -32,8 +32,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "VarReplacer.h" #include "FindUndef.h" -#include "Gaussian.h" -#include "MatrixFinder.h" #include "Conglomerate.h" #include "XorFinder.h" #include "ClauseCleaner.h" @@ -43,6 +41,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "PartHandler.h" #include "XorSubsumer.h" +#ifdef USE_GAUSS +#include "Gaussian.h" +#include "MatrixFinder.h" +#endif //USE_GAUSS + #ifdef _MSC_VER #define __builtin_prefetch(a,b,c) //#define __builtin_prefetch(a,b) @@ -143,7 +146,9 @@ Solver::~Solver() for (uint32_t i = 0; i != clauses.size(); i++) clauseFree(clauses[i]); for (uint32_t i = 0; i != binaryClauses.size(); i++) clauseFree(binaryClauses[i]); for (uint32_t i = 0; i != xorclauses.size(); i++) free(xorclauses[i]); + #ifdef USE_GAUSS clearGaussMatrixes(); + #endif delete varReplacer; delete conglomerate; delete clauseCleaner; @@ -509,9 +514,10 @@ void Solver::cancelUntil(int level) if (decisionLevel() > level) { + #ifdef USE_GAUSS for (vector::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) (*gauss)->canceling(trail_lim[level]); - + #endif //USE_GAUSS for (int c = trail.size()-1; c >= (int)trail_lim[level]; c--) { Var x = trail[c].var(); @@ -542,12 +548,14 @@ void Solver::needLibraryCNFFile(const char* fileName) assert(libraryCNFFile != NULL); } +#ifdef USE_GAUSS void Solver::clearGaussMatrixes() { for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; gauss_matrixes.clear(); } +#endif //USE_GAUSS inline bool Solver::defaultPolarity() { @@ -1478,10 +1486,12 @@ lbool Solver::search(int nof_conflicts, int nof_conflicts_fullrestart, const boo else dynStarts++; + #ifdef USE_GAUSS for (vector::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) { ret = (*gauss)->full_init(); if (ret != l_Nothing) return ret; } + #endif //USE_GAUSS for (;;) { Clause* confl = propagate(update); @@ -1490,6 +1500,7 @@ lbool Solver::search(int nof_conflicts, int nof_conflicts_fullrestart, const boo ret = handle_conflict(learnt_clause, confl, conflictC, update); if (ret != l_Nothing) return ret; } else { + #ifdef USE_GAUSS bool at_least_one_continue = false; for (vector::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) { ret = (*gauss)->find_truths(learnt_clause, conflictC); @@ -1497,6 +1508,7 @@ lbool Solver::search(int nof_conflicts, int nof_conflicts_fullrestart, const boo else if (ret != l_Nothing) return ret; } if (at_least_one_continue) continue; + #endif //USE_GAUSS ret = new_decision(nof_conflicts, nof_conflicts_fullrestart, conflictC); if (ret != l_Nothing) return ret; } @@ -1698,6 +1710,7 @@ double Solver::progressEstimate() const return progress / nVars(); } +#ifdef USE_GAUSS void Solver::print_gauss_sum_stats() const { if (gauss_matrixes.size() == 0) { @@ -1726,6 +1739,7 @@ void Solver::print_gauss_sum_stats() const printf(" %3.0lf%% |\n", 100.0-(double)disabled/(double)gauss_matrixes.size()*100.0); } } +#endif //USE_GAUSS inline void Solver::chooseRestartType(const uint& lastFullRestart) { @@ -1752,7 +1766,8 @@ inline void Solver::chooseRestartType(const uint& lastFullRestart) lastSelectedRestartType = static_restart; if (verbosity >= 2) printf("c | Decided on static restart strategy |\n"); - + + #ifdef USE_GAUSS if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) { double time = cpuTime(); MatrixFinder m(*this); @@ -1760,6 +1775,7 @@ inline void Solver::chooseRestartType(const uint& lastFullRestart) if (verbosity >=1) printf("c | Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes); } + #endif //USE_GAUSS } restartType = tmp; restartTypeChooser->reset(); @@ -1867,7 +1883,9 @@ end: const bool Solver::checkFullRestart(int& nof_conflicts, int& nof_conflicts_fullrestart, uint& lastFullRestart) { if (nof_conflicts_fullrestart > 0 && conflicts >= nof_conflicts_fullrestart) { + #ifdef USE_GAUSS clearGaussMatrixes(); + #endif //USE_GAUSS if (verbosity >= 2) printf("c | Fully restarting |\n"); nof_conflicts = restart_first + (double)restart_first*restart_inc; @@ -1906,7 +1924,6 @@ inline void Solver::performStepsBeforeSolve() && !subsumer->simplifyBySubsumption()) return; - const uint32_t lastReplacedVars = varReplacer->getNumReplacedVars(); if (findBinaryXors && binaryClauses.size() < MAX_CLAUSENUM_XORFIND) { XorFinder xorFinder(this, binaryClauses, ClauseCleaner::binaryClauses); if (!xorFinder.doNoPart(2, 2)) return; @@ -1916,7 +1933,7 @@ inline void Solver::performStepsBeforeSolve() if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) { XorFinder xorFinder(this, clauses, ClauseCleaner::clauses); - if (!xorFinder.doNoPart(3, 10)) return; + if (!xorFinder.doNoPart(3, 7)) return; } if (xorclauses.size() > 1) { @@ -1965,7 +1982,9 @@ lbool Solver::solve(const vec& assumps) model.clear(); conflict.clear(); + #ifdef USE_GAUSS clearGaussMatrixes(); + #endif //USE_GAUSS setDefaultRestartType(); totalSumOfDecisionLevel = 0; conflictsAtLastSolve = conflicts; @@ -2028,9 +2047,11 @@ lbool Solver::solve(const vec& assumps) } printEndSearchStat(); + #ifdef USE_GAUSS for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; gauss_matrixes.clear(); + #endif //USE_GAUSS #ifdef VERBOSE_DEBUG if (status == l_True) @@ -2096,6 +2117,12 @@ lbool Solver::solve(const vec& assumps) for (Var var = 0; var < nVars(); var++) { if (assigns[var] == l_Undef && s.model[var] != l_Undef) uncheckedEnqueue(Lit(var, s.model[var] == l_False)); } + ok = (propagate() == NULL); + if (!ok) { + printf("c ERROR! Extension of model failed!\n"); + assert(ok); + exit(-1); + } } #ifndef NDEBUG //checkSolution(); @@ -2103,7 +2130,6 @@ lbool Solver::solve(const vec& assumps) //Copy model: model.growTo(nVars()); for (Var var = 0; var != nVars(); var++) model[var] = value(var); - } if (status == l_False) { @@ -2248,8 +2274,12 @@ void Solver::printRestartStat() const #else if (verbosity >= 2) { #endif - printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)nClauses(), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart+nbCompensateSubsumer), (int)nLearnts(), (double)learnts_literals/nLearnts()); + printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)nClauses(), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart+nbCompensateSubsumer), (int)nLearnts(), (double)learnts_literals/nLearnts()); + #ifdef USE_GAUSS print_gauss_sum_stats(); + #else //USE_GAUSS + printf(" |\n"); + #endif //USE_GAUSS } } @@ -2261,7 +2291,11 @@ void Solver::printEndSearchStat() const if (verbosity >= 1) { #endif printf("c ===================================================================="); + #ifdef USE_GAUSS print_gauss_sum_stats(); + #else //USE_GAUSS + printf("\n"); + #endif //USE_GAUSS } } diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 9fcda6a..66010b6 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -38,10 +38,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "MersenneTwister.h" #include "SolverTypes.h" #include "Clause.h" -#include "GaussianConfig.h" #include "Logger.h" #include "constants.h" #include "BoundedQueue.h" +#include "GaussianConfig.h" namespace MINISAT { @@ -157,6 +157,7 @@ public: bool greedyUnbound; //If set, then variables will be greedily unbounded (set to l_Undef) RestartType fixRestartType; // If set, the solver will always choose the given restart strategy GaussianConfig gaussconfig; + enum { polarity_true = 0, polarity_false = 1, polarity_rnd = 3, polarity_auto = 4, polarity_manual = 5}; @@ -179,9 +180,11 @@ public: void needLibraryCNFFile(const char* fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file. protected: - vector gauss_matrixes; + #ifdef USE_GAUSS void print_gauss_sum_stats() const; void clearGaussMatrixes(); + vector gauss_matrixes; + #endif //USE_GAUSS friend class Gaussian; template diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp index cf711e4..73a86c3 100644 --- a/src/sat/cryptominisat2/Subsumer.cpp +++ b/src/sat/cryptominisat2/Subsumer.cpp @@ -55,9 +55,8 @@ void Subsumer::extendModel(Solver& solver2) vec tmp; typedef map > > elimType; for (elimType::iterator it = elimedOutVar.begin(), end = elimedOutVar.end(); it != end; it++) { - Var var = it->first; - #ifdef VERBOSE_DEBUG + Var var = it->first; std::cout << "Reinserting elimed var: " << var+1 << std::endl; #endif @@ -793,7 +792,7 @@ const bool Subsumer::simplifyBySubsumption() numVarsElimed = 0; blockTime = 0.0; - //if (solver.clauses.size() < 2000000) addAllXorAsNorm(); + //if (solver.xorclauses.size() < 30000 && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/10) addAllXorAsNorm(); //For VE touched_list.clear(); @@ -933,7 +932,6 @@ const bool Subsumer::simplifyBySubsumption() for (bool first = true; numMaxElim > 0; first = false){ uint32_t vars_elimed = 0; - int clauses_before = solver.nClauses(); vec order; if (first) { @@ -978,7 +976,7 @@ const bool Subsumer::simplifyBySubsumption() numVarsElimed += vars_elimed; #ifdef BIT_MORE_VERBOSITY - printf("c #clauses-removed: %-8d #var-elim: %d\n", clauses_before - solver.nClauses(), vars_elimed); + printf("c #var-elim: %d\n", vars_elimed); std::cout << "c time until the end of varelim: " << cpuTime() - myTime << std::endl; #endif } @@ -1012,10 +1010,10 @@ const bool Subsumer::simplifyBySubsumption() addBackToSolver(); solver.nbCompensateSubsumer += origNLearnts-solver.learnts.size(); - /*if (solver.findNormalXors && solver.clauses.size() < MAX_CLAUSENUM_XORFIND) { + if (solver.findNormalXors && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/8) { XorFinder xorFinder(&solver, solver.clauses, ClauseCleaner::clauses); - if (!xorFinder.doNoPart(3, 4)) return false; - }*/ + if (!xorFinder.doNoPart(3, 7)) return false; + } if (solver.verbosity >= 1) { std::cout << "c | lits-rem: " << std::setw(9) << literals_removed @@ -1322,7 +1320,7 @@ void Subsumer::orderVarsForElim(vec& order) { order.clear(); vec > cost_var; - for (int i = 0; i < touched_list.size(); i++){ + for (uint32_t i = 0; i < touched_list.size(); i++){ Var x = touched_list[i]; touched[x] = 0; cost_var.push(std::make_pair( occur[Lit(x, false).toInt()].size() * occur[Lit(x, true).toInt()].size() , x )); @@ -1331,7 +1329,7 @@ void Subsumer::orderVarsForElim(vec& order) touched_list.clear(); std::sort(cost_var.getData(), cost_var.getData()+cost_var.size(), myComp()); - for (int x = 0; x < cost_var.size(); x++) { + for (uint32_t x = 0; x < cost_var.size(); x++) { if (cost_var[x].first != 0) order.push(cost_var[x].second); } @@ -1709,7 +1707,9 @@ void Subsumer::addAllXorAsNorm() solver.removeClause(**i); } solver.xorclauses.shrink(i-j); - std::cout << "Added XOR as norm:" << added << std::endl; + if (solver.verbosity >= 1) { + std::cout << "c | Added XOR as norm:" << added << std::endl; + } } void Subsumer::addXorAsNormal3(XorClause& c) diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 43593b7..c9c4944 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,2 @@ CryptoMiniSat -GIT revision: fb8c4dc98c93f0034e20ce4b068457215a4047e8 +GIT revision: 9653102935b2e707c0aae731704e28809c4b548d diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 261288e..580b27a 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -152,7 +152,7 @@ const bool VarReplacer::replace_set(vec& cs) bool changed = false; Var origVar1 = c[0].var(); Var origVar2 = c[1].var(); - for (Lit *l = &c[0], *lend = l + c.size(); l != lend; l++) { + for (Lit *l = &c[0], *end2 = l + c.size(); l != end2; l++) { Lit newlit = table[l->var()]; if (newlit.var() != l->var()) { changed = true; @@ -242,7 +242,7 @@ const bool VarReplacer::replace_set(vec& cs) bool changed = false; Lit origLit1 = c[0]; Lit origLit2 = c[1]; - for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + for (Lit *l = c.getData(), *end2 = l + c.size(); l != end2; l++) { if (table[l->var()].var() != l->var()) { changed = true; *l = table[l->var()] ^ l->sign(); diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h index a223c7c..4c94beb 100644 --- a/src/sat/cryptominisat2/constants.h +++ b/src/sat/cryptominisat2/constants.h @@ -33,3 +33,4 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define RESTART_TYPE_DECIDER_UNTIL 7 //#define VERBOSE_DEBUG_XOR //#define VERBOSE_DEBUG +//#define USE_GAUSS