From 451d5bfea7fe53ee45da3cbc7e311570cd827d47 Mon Sep 17 00:00:00 2001 From: msoos Date: Wed, 28 Apr 2010 12:24:57 +0000 Subject: [PATCH] Updating CMS2 There have been some bugs fixed, and some performance increases added. Hopefully these will fix up all remaining bugs git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@731 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/Clause.h | 8 +- src/sat/cryptominisat2/ClauseCleaner.cpp | 2 +- src/sat/cryptominisat2/FailedVarSearcher.cpp | 4 + src/sat/cryptominisat2/Logger.cpp | 12 +- src/sat/cryptominisat2/Makefile | 2 +- src/sat/cryptominisat2/SmallPtr.o | Bin 0 -> 1083 bytes src/sat/cryptominisat2/Solver.cpp | 25 ++- src/sat/cryptominisat2/Solver.h | 8 +- src/sat/cryptominisat2/Subsumer.cpp | 171 +++---------------- src/sat/cryptominisat2/VERSION | 2 +- src/sat/cryptominisat2/VarReplacer.cpp | 8 +- src/sat/cryptominisat2/XorFinder.cpp | 162 ++++++++++++++++-- src/sat/cryptominisat2/XorFinder.h | 9 +- 13 files changed, 225 insertions(+), 188 deletions(-) create mode 100644 src/sat/cryptominisat2/SmallPtr.o diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index 0438466..5969fd3 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifdef _MSC_VER #include #else +#include "SmallPtr.h" #include #endif //_MSC_VER #include @@ -384,10 +385,13 @@ inline void clauseFree(Clause* c) return ret; }*/ -//typedef sptr ClausePtr; -//typedef sptr XorClausePtr; +#ifdef _MSC_VER typedef Clause* ClausePtr; typedef XorClause* XorClausePtr; +#else +typedef sptr ClausePtr; +typedef sptr XorClausePtr; +#endif //_MSC_VER #pragma pack(push) #pragma pack(1) diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index e9d5479..7f4610b 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -76,7 +76,7 @@ void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, const else *j++ = *i; } - cs.shrink_(i - j); + cs.shrink(i - j); lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); } diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp index da5f5ad..3d0e86f 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.cpp +++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp @@ -29,6 +29,10 @@ using std::set; #include "VarReplacer.h" #include "ClauseCleaner.h" +#ifdef _MSC_VER +#define __builtin_prefetch(a,b,c) +#endif //_MSC_VER + //#define VERBOSE_DEUBUG namespace MINISAT diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index d7deda8..94b0d0a 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -125,22 +125,18 @@ void Logger::set_group_name(const uint group, char* name_tmp) return; string name; - if (name_tmp == NULL) - name = ""; - else - name = name_tmp; + if (name_tmp == NULL) return; + else name = name_tmp; new_group(group); cut_name_to_size(name); - - if (name.length() == 0) return; - if (name == "Noname" || name == "") return; + if (name == "Noname") return; if (groupnames[group] == "Noname") { groupnames[group] = name; } else if (groupnames[group] != name) { - printf("Error! Group no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", group, groupnames[group].c_str(), name.c_str()); + std::cout << "Error! Group no. " << group << "has been named twice. First, as '" << groupnames[group] << "', then second as '" << name << "'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line" << std::endl; exit(-1); } } diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index 0118702..a38b19e 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 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 +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 SmallPtr.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/SmallPtr.o b/src/sat/cryptominisat2/SmallPtr.o new file mode 100644 index 0000000000000000000000000000000000000000..7bcff5ca55bdbc0a44006de501e9c0d4eea57d0f GIT binary patch literal 1083 zcmbVL%}&BV5FRL^Tuiu;c&R5L$_Dv~z`@jDB}64A=*3If;zo@Wn(iL-_5w(P(Jb&zb*B zS9X_lNxL~{#H3@lTgNT=>D%=%Vi8+1%2@+|@V7uvU!sUM_=HTbR{`XK3JS#M9LQoF z1Z*X})mktzp58UNpo^Ex75*dkWJt}SY=j*{qbwoOxGz!VEyH)T-Z6YrAIQ4$%=}#E zY>fz}K9U7>ehV8k&NX%nU-hbm*h}%apkE(pk>Z#`t15|kcU8l@i;Wu1ywXLZN6DJr z6n~FuM%(hi`PEdDTow7`o&TlH%eX6fndc{!EK_|Y`2NYd8)f}XFI%;8zlpkE-VK$% zmEAxqOP*}5U1?NP`{NuAV?Wv7#^5ZV%jJ!T$RZ5EyPuw1Po|UE+3kRbBJzCs5A1oI PJ#sg{*jGg_prH%D`B+IF literal 0 HcmV?d00001 diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index b08fb5c..cd45412 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -65,6 +65,7 @@ using namespace MINISAT; Solver::Solver() : // Parameters: (formerly in 'SearchParams') random_var_freq(0.02) + , clause_decay (1 / 0.999) , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1) // More parameters: @@ -529,7 +530,7 @@ void Solver::cancelUntil(int level) } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); - trail_lim.shrink_(trail_lim.size() - level); + trail_lim.shrink(trail_lim.size() - level); } #ifdef VERBOSE_DEBUG @@ -1119,7 +1120,7 @@ Clause* Solver::propagate(const bool update) FoundWatch: ; } - ws.shrink_(i - j); + ws.shrink(i - j); //Finally, propagate XOR-clauses if (xorclauses.size() > 0 && !confl) confl = propagate_xors(p); @@ -1296,7 +1297,7 @@ void Solver::reduceDB() for (; i < learnts.size(); i++) { learnts[j++] = learnts[i]; } - learnts.shrink_(i - j); + learnts.shrink(i - j); } const vec& Solver::get_learnts() const @@ -1434,7 +1435,7 @@ lbool Solver::simplify() if (ok == false) return l_False; - XorFinder xorFinder(this, binaryClauses, ClauseCleaner::binaryClauses); + XorFinder xorFinder(*this, binaryClauses, ClauseCleaner::binaryClauses); if (xorFinder.doNoPart(2, 2) == false) return l_False; @@ -1692,6 +1693,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf } varDecayActivity(); + if (update && restartType == static_restart) claDecayActivity(); return l_Nothing; } @@ -1864,6 +1866,17 @@ const lbool Solver::simplifyProblem(const uint32_t numConfls, const uint64_t num } } + /*if (findNormalXors && xorclauses.size() > 200 && clauses.size() < MAX_CLAUSENUM_XORFIND/8) { + XorFinder xorFinder(*this, clauses, ClauseCleaner::clauses); + if (!xorFinder.doNoPart(3, 7)) { + status = l_False; + goto end; + } + } else*/ if (xorclauses.size() <= 200 && xorclauses.size() > 0 && nClauses() > 10000) { + XorFinder x(*this, clauses, ClauseCleaner::clauses); + x.addAllXorAsNorm(); + } + end: random_var_freq = backup_random_var_freq; if (verbosity >= 2) @@ -1925,14 +1938,14 @@ inline void Solver::performStepsBeforeSolve() return; if (findBinaryXors && binaryClauses.size() < MAX_CLAUSENUM_XORFIND) { - XorFinder xorFinder(this, binaryClauses, ClauseCleaner::binaryClauses); + XorFinder xorFinder(*this, binaryClauses, ClauseCleaner::binaryClauses); if (!xorFinder.doNoPart(2, 2)) return; if (performReplace && !varReplacer->performReplace(true)) return; } if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) { - XorFinder xorFinder(this, clauses, ClauseCleaner::clauses); + XorFinder xorFinder(*this, clauses, ClauseCleaner::clauses); if (!xorFinder.doNoPart(3, 7)) return; } diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 66010b6..7947c86 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -128,6 +128,7 @@ public: // Mode of operation: // double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) + double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999) int restart_first; // The initial restart limit. (default 100) double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) @@ -152,7 +153,6 @@ public: bool doSubsume1; // Perform clause contraction through resolution bool failedVarSearch; // Should search for failed vars and doulbly propagated vars bool libraryUsage; // Set true if not used as a library - bool sateliteUsed; // whether satielite was used on CNF before calling friend class FindUndef; 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 @@ -422,7 +422,11 @@ inline void Solver::claBumpActivity (Clause& c) cla_inc *= 1e-20; } } - + +inline void Solver::claDecayActivity() +{ + cla_inc *= clause_decay; +} inline bool Solver::enqueue (Lit p, Clause* from) { diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp index 73a86c3..24a2481 100644 --- a/src/sat/cryptominisat2/Subsumer.cpp +++ b/src/sat/cryptominisat2/Subsumer.cpp @@ -84,11 +84,16 @@ const bool Subsumer::unEliminate(const Var var) vec tmp; typedef map > > elimType; elimType::iterator it = elimedOutVar.find(var); - assert(it != elimedOutVar.end()); solver.setDecisionVar(var, true); var_elimed[var] = false; numElimed--; + + //If the variable was removed because of + //pure literal removal (by blocked clause + //elimination, there are no clauses to re-insert + if (it == elimedOutVar.end()) return solver.ok; + FILE* backup_libraryCNFfile = solver.libraryCNFFile; solver.libraryCNFFile = NULL; for (vector >::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) { @@ -100,8 +105,7 @@ const bool Subsumer::unEliminate(const Var var) solver.libraryCNFFile = backup_libraryCNFfile; elimedOutVar.erase(it); - if (!solver.ok) return false; - return true; + return solver.ok; } bool selfSubset(uint32_t A, uint32_t B) @@ -144,7 +148,6 @@ uint32_t Subsumer::subsume0(Clause& ps) #ifdef VERBOSE_DEBUG cout << "subsume0 orig clause:"; ps.plainPrint(); - cout << "pointer:" << &ps << endl; #endif vec subs; @@ -532,7 +535,7 @@ void Subsumer::smaller_database() registerIteration(s1); #ifdef BIT_MORE_VERBOSITY - printf(" FIXED-POINT\n"); + printf("c FIXED-POINT\n"); #endif // Fixed-point for 1-subsumption: @@ -548,7 +551,7 @@ void Subsumer::smaller_database() assert(solver.qhead == solver.trail.size()); #ifdef BIT_MORE_VERBOSITY - printf("s1.size()=%d cl_touched.size()=%d\n", s1.size(), cl_touched.size()); + printf("c s1.size()=%d cl_touched.size()=%d\n", s1.size(), cl_touched.size()); #endif for (CSet::iterator it = s1.begin(), end = s1.end(); it != end; ++it) { @@ -729,8 +732,7 @@ void Subsumer::subsume0LearntSet(vec& cs) Clause** a = cs.getData(); Clause** b = a; for (Clause** end = a + cs.size(); a != end; a++) { - if (numMaxSubsume0 == 0) break; - if (!(*a)->subsume0IsFinished()) { + if (numMaxSubsume0 > 0 && !(*a)->subsume0IsFinished()) { numMaxSubsume0--; uint32_t index = subsume0(**a, calcAbstraction(**a)); if (index != std::numeric_limits::max()) { @@ -751,8 +753,12 @@ void Subsumer::subsume0LearntSet(vec& cs) clauses.push(c); subsume1(c); numMaxSubsume1--; - if (!solver.ok) + if (!solver.ok) { + for (; a != end; a++) + *b++ = *a; + cs.shrink(a-b); return; + } assert(clauses[c.index].clause != NULL); clauses.pop(); clauseID--; @@ -856,6 +862,13 @@ const bool Subsumer::simplifyBySubsumption() else fullSubsume = false; + //For debugging post-c32s-gcdm16-22.cnf --- an instance that is turned SAT to UNSAT if a bug is in the code + //numMaxBlockToVisit = std::numeric_limits::max(); + //numMaxElim = std::numeric_limits::max(); + //numMaxSubsume0 = std::numeric_limits::max(); + //numMaxSubsume1 = std::numeric_limits::max(); + //numMaxBlockVars = std::numeric_limits::max(); + #ifdef BIT_MORE_VERBOSITY std::cout << "c num clauses:" << clauses.size() << std::endl; std::cout << "c time to link in:" << cpuTime()-myTime << std::endl; @@ -891,10 +904,8 @@ const bool Subsumer::simplifyBySubsumption() #endif if (clauses.size() > 10000000) goto endSimplifyBySubsumption; - + if (solver.doBlockedClause && numCalls % 3 == 1) blockedClauseRemoval(); do{ - if (solver.doBlockedClause && numCalls % 3 == 1) blockedClauseRemoval(); - #ifdef BIT_MORE_VERBOSITY std::cout << "c time before the start of almost_all/smaller: " << cpuTime() - myTime << std::endl; #endif @@ -946,8 +957,8 @@ const bool Subsumer::simplifyBySubsumption() const Var var = touched_list[i]; if (!var_elimed[var] && !cannot_eliminate[var] && solver.decision_var[var] && solver.assigns[var] == l_Undef) { order.push(touched_list[i]); - touched[touched_list[i]] = 0; } + touched[var] = 0; } touched_list.clear(); } @@ -980,7 +991,7 @@ const bool Subsumer::simplifyBySubsumption() std::cout << "c time until the end of varelim: " << cpuTime() - myTime << std::endl; #endif } - }while (cl_added.size() > 100); + }while (cl_added.size() > 100 && numMaxElim > 0); endSimplifyBySubsumption: if (!solver.ok) return false; @@ -990,7 +1001,7 @@ const bool Subsumer::simplifyBySubsumption() return false; } - #ifndef DNDEBUG + #ifndef NDEBUG verifyIntegrity(); #endif @@ -1010,10 +1021,6 @@ const bool Subsumer::simplifyBySubsumption() addBackToSolver(); solver.nbCompensateSubsumer += origNLearnts-solver.learnts.size(); - if (solver.findNormalXors && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/8) { - XorFinder xorFinder(&solver, solver.clauses, ClauseCleaner::clauses); - if (!xorFinder.doNoPart(3, 7)) return false; - } if (solver.verbosity >= 1) { std::cout << "c | lits-rem: " << std::setw(9) << literals_removed @@ -1692,132 +1699,6 @@ const bool Subsumer::tryOneSetting(const Lit lit, const Lit negLit) return returnVal; } -void Subsumer::addAllXorAsNorm() -{ - uint32_t added = 0; - XorClause **i = solver.xorclauses.getData(), **j = i; - for (XorClause **end = solver.xorclauses.getDataEnd(); i != end; i++) { - if ((*i)->size() > 3) { - *j++ = *i; - continue; - } - added++; - if ((*i)->size() == 3) addXorAsNormal3(**i); - //if ((*i)->size() == 4) addXorAsNormal4(**i); - solver.removeClause(**i); - } - solver.xorclauses.shrink(i-j); - if (solver.verbosity >= 1) { - std::cout << "c | Added XOR as norm:" << added << std::endl; - } -} - -void Subsumer::addXorAsNormal3(XorClause& c) -{ - assert(c.size() == 3); - Clause *tmp; - vec vars; - vec vars2(c.size()); - const bool inverted = c.xor_clause_inverted(); - - for (uint32_t i = 0; i < c.size(); i++) { - vars.push(c[i].var()); - } - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); -} - -void Subsumer::addXorAsNormal4(XorClause& c) -{ - assert(c.size() == 4); - Clause *tmp; - vec vars; - vec vars2(c.size()); - const bool inverted = !c.xor_clause_inverted(); - - for (uint32_t i = 0; i < c.size(); i++) { - vars.push(c[i].var()); - } - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], false ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], false ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], false ^ inverted); - tmp = solver.addClauseInt(vars2, c.getGroup()); - if (tmp) solver.clauses.push(tmp); -} - /*vector Subsumer::merge() { vector var_merged(solver.nVars(), false); diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index c9c4944..3f5b5c4 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,2 @@ CryptoMiniSat -GIT revision: 9653102935b2e707c0aae731704e28809c4b548d +GIT revision: 36df8dc9098df142071729c19f78002311987863 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 580b27a..93239f9 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -115,7 +115,7 @@ const bool VarReplacer::performReplaceInternal() assert(solver.order_heap.heapProperty()); if (solver.verbosity >= 2) - std::cout << "c | Replacing " << std::setw(8) << replacedVars-lastReplacedVars << " vars"; + std::cout << "c | Replacing " << std::setw(8) << replacedVars-lastReplacedVars << " vars" << std::flush; lastReplacedVars = replacedVars; @@ -130,9 +130,9 @@ end: clauses.clear(); if (solver.verbosity >= 2) { - std::cout << "c | Replaced " << std::setw(8) << replacedLits<< " lits" - << " Time: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime()-time << " s " - << std::setw(12) << " |" << std::endl; + std::cout << " Replaced " << std::setw(8) << replacedLits<< " lits" + << " Time: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime()-time << " s " + << std::setw(10) << " |" << std::endl; } replacedLits = 0; diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index 847a5af..c2186fd 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -42,10 +42,10 @@ using namespace MINISAT; using std::make_pair; -XorFinder::XorFinder(Solver* _s, vec& _cls, ClauseCleaner::ClauseSetType _type) : +XorFinder::XorFinder(Solver& _solver, vec& _cls, ClauseCleaner::ClauseSetType _type) : cls(_cls) , type(_type) - , S(_s) + , solver(_solver) { } @@ -54,8 +54,8 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize) uint sumLengths = 0; double time = cpuTime(); foundXors = 0; - S->clauseCleaner->cleanClauses(cls, type); - if (S->ok == false) + solver.clauseCleaner->cleanClauses(cls, type); + if (solver.ok == false) return false; toRemove.clear(); @@ -84,9 +84,9 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize) if (!sorted) break; } if (!sorted) { - S->detachClause(c); + solver.detachClause(c); std::sort(c.getData(), c.getData()+c.size()); - S->attachClause(c); + solver.attachClause(c); } } else { std::sort(c.getData(), c.getData()+c.size()); @@ -140,14 +140,17 @@ const bool XorFinder::doNoPart(const uint minSize, const uint maxSize) #endif //DEBUG_XORFIND if (findXors(sumLengths) == false) goto end; - S->ok = (S->propagate() == NULL); + solver.ok = (solver.propagate() == NULL); end: - if (S->verbosity >= 2) { - if (minSize == maxSize && minSize == 2) + if (minSize == maxSize && minSize == 2) { + if (solver.verbosity >= 2 || (solver.conflicts == 0 && solver.verbosity >= 1)) { printf("c | Finding binary XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); - else + } + } else { + if (solver.verbosity >= 2 || (solver.verbosity >= 1 && foundXors > 0)) { printf("c | Finding non-binary XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); + } } i = 0; @@ -168,7 +171,7 @@ end: } cls.shrink(i-j); - return S->ok; + return solver.ok; } const bool XorFinder::findXors(uint& sumLengths) @@ -201,12 +204,12 @@ const bool XorFinder::findXors(uint& sumLengths) it->first->plainPrint(); #endif toRemove[it->second] = true; - S->removeClause(*it->first); + solver.removeClause(*it->first); } switch(lits.size()) { case 2: { - S->varReplacer->replace(lits, impair, old_group); + solver.varReplacer->replace(lits, impair, old_group); #ifdef VERBOSE_DEBUG XorClause* x = XorClause_new(lits, impair, old_group); @@ -218,8 +221,8 @@ const bool XorFinder::findXors(uint& sumLengths) } default: { XorClause* x = XorClause_new(lits, impair, old_group); - S->xorclauses.push(x); - S->attachClause(*x); + solver.xorclauses.push(x); + solver.attachClause(*x); #ifdef VERBOSE_DEBUG cout << "- Final xor-clause: "; @@ -232,7 +235,7 @@ const bool XorFinder::findXors(uint& sumLengths) sumLengths += lits.size(); } - return S->ok; + return solver.ok; } void XorFinder::clearToRemove() @@ -362,4 +365,131 @@ void XorFinder::countImpairs(const ClauseTable::iterator& begin, const ClauseTab } } +void XorFinder::addAllXorAsNorm() +{ + uint32_t added = 0; + XorClause **i = solver.xorclauses.getData(), **j = i; + for (XorClause **end = solver.xorclauses.getDataEnd(); i != end; i++) { + if ((*i)->size() > 3) { + *j++ = *i; + continue; + } + added++; + if ((*i)->size() == 3) addXorAsNormal3(**i); + //if ((*i)->size() == 4) addXorAsNormal4(**i); + solver.removeClause(**i); + } + solver.xorclauses.shrink(i-j); + if (solver.verbosity >= 1) { + std::cout << "c | Added XOR as norm:" << added << std::endl; + } +} + +void XorFinder::addXorAsNormal3(XorClause& c) +{ + assert(c.size() == 3); + Clause *tmp; + vec vars; + vec vars2(c.size()); + const bool inverted = c.xor_clause_inverted(); + + for (uint32_t i = 0; i < c.size(); i++) { + vars.push(c[i].var()); + } + + vars2[0] = Lit(vars[0], false ^ inverted); + vars2[1] = Lit(vars[1], false ^ inverted); + vars2[2] = Lit(vars[2], false ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], true ^ inverted); + vars2[1] = Lit(vars[1], true ^ inverted); + vars2[2] = Lit(vars[2], false ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], true ^ inverted); + vars2[1] = Lit(vars[1], false ^ inverted); + vars2[2] = Lit(vars[2], true ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], false ^ inverted); + vars2[1] = Lit(vars[1], true ^ inverted); + vars2[2] = Lit(vars[2], true ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); +} + +void XorFinder::addXorAsNormal4(XorClause& c) +{ + assert(c.size() == 4); + Clause *tmp; + vec vars; + vec vars2(c.size()); + const bool inverted = !c.xor_clause_inverted(); + + for (uint32_t i = 0; i < c.size(); i++) { + vars.push(c[i].var()); + } + + vars2[0] = Lit(vars[0], false ^ inverted); + vars2[1] = Lit(vars[1], false ^ inverted); + vars2[2] = Lit(vars[2], false ^ inverted); + vars2[3] = Lit(vars[3], true ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], false ^ inverted); + vars2[1] = Lit(vars[1], true ^ inverted); + vars2[2] = Lit(vars[2], false ^ inverted); + vars2[3] = Lit(vars[3], false ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], false ^ inverted); + vars2[1] = Lit(vars[1], false ^ inverted); + vars2[2] = Lit(vars[2], true ^ inverted); + vars2[3] = Lit(vars[3], false ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], false ^ inverted); + vars2[1] = Lit(vars[1], false ^ inverted); + vars2[2] = Lit(vars[2], false ^ inverted); + vars2[3] = Lit(vars[3], true ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], false ^ inverted); + vars2[1] = Lit(vars[1], true ^ inverted); + vars2[2] = Lit(vars[2], true ^ inverted); + vars2[3] = Lit(vars[3], true ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], true ^ inverted); + vars2[1] = Lit(vars[1], false ^ inverted); + vars2[2] = Lit(vars[2], true ^ inverted); + vars2[3] = Lit(vars[3], true ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], true ^ inverted); + vars2[1] = Lit(vars[1], true ^ inverted); + vars2[2] = Lit(vars[2], false ^ inverted); + vars2[3] = Lit(vars[3], true ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); + + vars2[0] = Lit(vars[0], true ^ inverted); + vars2[1] = Lit(vars[1], true ^ inverted); + vars2[2] = Lit(vars[2], true ^ inverted); + vars2[3] = Lit(vars[3], false ^ inverted); + tmp = solver.addClauseInt(vars2, c.getGroup()); + if (tmp) solver.clauses.push(tmp); +} + + }; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/XorFinder.h b/src/sat/cryptominisat2/XorFinder.h index f07190f..038afa0 100644 --- a/src/sat/cryptominisat2/XorFinder.h +++ b/src/sat/cryptominisat2/XorFinder.h @@ -43,8 +43,9 @@ class XorFinder { public: - XorFinder(Solver* S, vec& cls, ClauseCleaner::ClauseSetType _type); + XorFinder(Solver& _solver, vec& cls, ClauseCleaner::ClauseSetType _type); const bool doNoPart(const uint minSize, const uint maxSize); + void addAllXorAsNorm(); private: typedef vector > ClauseTable; @@ -126,6 +127,10 @@ class XorFinder void clearToRemove(); uint32_t foundXors; + //For adding xor as norm + void addXorAsNormal3(XorClause& c); + void addXorAsNormal4(XorClause& c); + vec& cls; ClauseCleaner::ClauseSetType type; @@ -134,7 +139,7 @@ class XorFinder void countImpairs(const ClauseTable::iterator& begin, const ClauseTable::iterator& end, uint& numImpair, uint& numPair) const; bool isXor(const uint32_t size, const ClauseTable::iterator& begin, const ClauseTable::iterator& end, bool& impair); - Solver* S; + Solver& solver; }; }; //NAMESPACE MINISAT -- 2.47.3