From 44b09e2dc6b27935b1317cf0ec05ad099f793a24 Mon Sep 17 00:00:00 2001 From: Francis Russell Date: Wed, 20 Apr 2011 00:17:09 +0100 Subject: [PATCH] Merge current CryptoMiniSat head. --- src/sat/cryptominisat2/BitArray.h | 10 + src/sat/cryptominisat2/BothCache.cpp | 113 ++ src/sat/cryptominisat2/BothCache.h | 16 + src/sat/cryptominisat2/CSet.h | 1 + src/sat/cryptominisat2/Clause.h | 51 +- src/sat/cryptominisat2/ClauseAllocator.cpp | 20 +- src/sat/cryptominisat2/ClauseCleaner.cpp | 2 + src/sat/cryptominisat2/ClauseVivifier.cpp | 57 +- src/sat/cryptominisat2/ClauseVivifier.h | 7 +- .../CompleteDetachReattacher.cpp | 2 +- src/sat/cryptominisat2/DataSync.cpp | 279 ++++- src/sat/cryptominisat2/DataSync.h | 73 +- src/sat/cryptominisat2/DimacsParser.cpp | 29 +- src/sat/cryptominisat2/DimacsParser.h | 9 +- src/sat/cryptominisat2/FailedLitSearcher.cpp | 377 +++++- src/sat/cryptominisat2/FailedLitSearcher.h | 29 +- src/sat/cryptominisat2/Gaussian.cpp | 29 +- src/sat/cryptominisat2/Gaussian.h | 2 +- src/sat/cryptominisat2/Logger.cpp | 107 +- src/sat/cryptominisat2/Logger.h | 14 +- src/sat/cryptominisat2/MTSolver.cpp | 284 +++++ src/sat/cryptominisat2/MTSolver.h | 242 ++++ src/sat/cryptominisat2/Main.cpp | 185 +-- src/sat/cryptominisat2/Main.h | 19 +- src/sat/cryptominisat2/Makefile | 2 +- src/sat/cryptominisat2/PartFinder.cpp | 119 +- src/sat/cryptominisat2/PartFinder.h | 12 +- src/sat/cryptominisat2/PartHandler.cpp | 92 +- src/sat/cryptominisat2/PartHandler.h | 3 +- src/sat/cryptominisat2/RestartTypeChooser.cpp | 51 +- src/sat/cryptominisat2/RestartTypeChooser.h | 14 +- src/sat/cryptominisat2/SCCFinder.cpp | 20 +- src/sat/cryptominisat2/SCCFinder.h | 1 + src/sat/cryptominisat2/SharedData.h | 44 +- src/sat/cryptominisat2/Solver.cpp | 638 ++++++---- src/sat/cryptominisat2/Solver.h | 241 ++-- src/sat/cryptominisat2/SolverConf.cpp | 7 +- src/sat/cryptominisat2/SolverConf.h | 8 +- src/sat/cryptominisat2/SolverDebug.cpp | 16 +- src/sat/cryptominisat2/SolverMisc.cpp | 56 +- src/sat/cryptominisat2/SolverTypes.h | 16 +- src/sat/cryptominisat2/StateSaver.cpp | 7 + src/sat/cryptominisat2/Subsumer.cpp | 1099 +++++++++++++---- src/sat/cryptominisat2/Subsumer.h | 133 +- src/sat/cryptominisat2/TransCache.h | 114 ++ src/sat/cryptominisat2/UselessBinRemover.cpp | 4 +- src/sat/cryptominisat2/VERSION | 2 +- src/sat/cryptominisat2/VarReplacer.cpp | 31 +- src/sat/cryptominisat2/VarReplacer.h | 6 +- src/sat/cryptominisat2/XorFinder.cpp | 2 +- src/sat/cryptominisat2/XorSubsumer.cpp | 2 +- src/sat/cryptominisat2/constants.h | 12 +- src/sat/cryptominisat2/mtl/Vec.h | 2 + 53 files changed, 3543 insertions(+), 1168 deletions(-) create mode 100644 src/sat/cryptominisat2/BothCache.cpp create mode 100644 src/sat/cryptominisat2/BothCache.h create mode 100644 src/sat/cryptominisat2/MTSolver.cpp create mode 100644 src/sat/cryptominisat2/MTSolver.h create mode 100644 src/sat/cryptominisat2/TransCache.h diff --git a/src/sat/cryptominisat2/BitArray.h b/src/sat/cryptominisat2/BitArray.h index c9e0b37..4dd64f8 100644 --- a/src/sat/cryptominisat2/BitArray.h +++ b/src/sat/cryptominisat2/BitArray.h @@ -94,6 +94,16 @@ public: return *this; } + template + BitArray& removeTheseLit(const T& rem) + { + for (uint32_t i = 0; i < rem.size(); i++) { + clearBit(rem[i].var()); + } + + return *this; + } + void resize(uint32_t _size, const bool fill) { _size = _size/64 + (bool)(_size%64); diff --git a/src/sat/cryptominisat2/BothCache.cpp b/src/sat/cryptominisat2/BothCache.cpp new file mode 100644 index 0000000..37d6007 --- /dev/null +++ b/src/sat/cryptominisat2/BothCache.cpp @@ -0,0 +1,113 @@ +/*************************************************************************** +CryptoMiniSat -- Copyright (c) 2010 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 "BothCache.h" +#include "time_mem.h" +#include +#include "VarReplacer.h" +#include "Subsumer.h" +#include "XorSubsumer.h" +#include "PartHandler.h" + +BothCache::BothCache(Solver& _solver) : + solver(_solver) +{}; + +const bool BothCache::tryBoth(const vector& cache) +{ + vec seen(solver.nVars(), 0); + vec val(solver.nVars(), 0); + vec tmp; + uint32_t bProp = 0; + uint32_t bXProp = 0; + double myTime = cpuTime(); + uint32_t backupTrailSize = solver.trail.size(); + + for (Var var = 0; var < solver.nVars(); var++) { + if (solver.value(var) != l_Undef + || solver.subsumer->getVarElimed()[var] + || solver.xorSubsumer->getVarElimed()[var] + || solver.varReplacer->getReplaceTable()[var].var() != var + || solver.partHandler->getSavedState()[var] != l_Undef) + continue; + + Lit lit = Lit(var, false); + vector const* cache1; + vector const* cache2; + + bool startWithTrue; + if (cache[lit.toInt()].lits.size() < cache[(~lit).toInt()].lits.size()) { + cache1 = &cache[lit.toInt()].lits; + cache2 = &cache[(~lit).toInt()].lits; + startWithTrue = false; + } else { + cache1 = &cache[(~lit).toInt()].lits; + cache2 = &cache[lit.toInt()].lits; + startWithTrue = true; + } + + if (cache1->size() == 0) continue; + + for (vector::const_iterator it = cache1->begin(), end = cache1->end(); it != end; it++) { + seen[it->getLit().var()] = true; + val[it->getLit().var()] = it->getLit().sign(); + } + + for (vector::const_iterator it = cache2->begin(), end = cache2->end(); it != end; it++) { + if (seen[it->getLit().var()]) { + Var var2 = it->getLit().var(); + if (solver.subsumer->getVarElimed()[var2] + || solver.xorSubsumer->getVarElimed()[var2] + || solver.varReplacer->getReplaceTable()[var2].var() != var2 + || solver.partHandler->getSavedState()[var2] != l_Undef) + continue; + + if (val[it->getLit().var()] == it->getLit().sign()) { + tmp.clear(); + tmp.push(it->getLit()); + solver.addClauseInt(tmp, 0, true); + if (!solver.ok) goto end; + bProp++; + } else { + tmp.clear(); + tmp.push(Lit(var, false)); + tmp.push(Lit(it->getLit().var(), false)); + bool sign = true ^ startWithTrue ^ it->getLit().sign(); + solver.addXorClauseInt(tmp, sign , 0); + if (!solver.ok) goto end; + bXProp++; + } + } + } + + for (vector::const_iterator it = cache1->begin(), end = cache1->end(); it != end; it++) { + seen[it->getLit().var()] = false; + } + } + + end: + if (solver.conf.verbosity >= 1) { + std::cout << "c Cache " << + " BProp: " << bProp << + " Set: " << (solver.trail.size() - backupTrailSize) << + " BXProp: " << bXProp << + " T: " << (cpuTime() - myTime) << + std::endl; + } + + return solver.ok; +} \ No newline at end of file diff --git a/src/sat/cryptominisat2/BothCache.h b/src/sat/cryptominisat2/BothCache.h new file mode 100644 index 0000000..630e257 --- /dev/null +++ b/src/sat/cryptominisat2/BothCache.h @@ -0,0 +1,16 @@ +#ifndef BOTHCACHE_H +#define BOTHCACHE_H + +#include "Solver.h" + +class BothCache +{ + public: + BothCache(Solver& solver); + const bool tryBoth(const vector& cache); + + private: + Solver& solver; +}; + +#endif //BOTHCACHE_H \ No newline at end of file diff --git a/src/sat/cryptominisat2/CSet.h b/src/sat/cryptominisat2/CSet.h index 6ad2f78..e35a79f 100644 --- a/src/sat/cryptominisat2/CSet.h +++ b/src/sat/cryptominisat2/CSet.h @@ -27,6 +27,7 @@ NOTE: On 64-bit systems, this datastructure needs 128 bits :O class ClauseSimp { public: + ClauseSimp() {}; ClauseSimp(Clause* c, const uint32_t _index) : clause(c) , index(_index) diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index eb99785..2b55dcf 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -68,9 +68,7 @@ protected: uint32_t isRemoved:1; /// getMiniSatAct()) - setMiniSatAct(other.getMiniSatAct()); } }; @@ -339,7 +326,7 @@ public: void print(FILE* to = stdout) const { plainPrint(to); - fprintf(to, "c clause learnt %s glue %d miniSatAct %.3f group %d\n", (learnt() ? "yes" : "no"), getGlue(), getMiniSatAct(), getGroup()); + fprintf(to, "c clause learnt %s glue %d group %d\n", (learnt() ? "yes" : "no"), getGlue(), getGroup()); } void plainPrint(FILE* to = stdout) const diff --git a/src/sat/cryptominisat2/ClauseAllocator.cpp b/src/sat/cryptominisat2/ClauseAllocator.cpp index b1d58d8..274ca0e 100644 --- a/src/sat/cryptominisat2/ClauseAllocator.cpp +++ b/src/sat/cryptominisat2/ClauseAllocator.cpp @@ -29,6 +29,7 @@ along with this program. If not, see . //#include "VarReplacer.h" #include "PartHandler.h" #include "Gaussian.h" +#include //For mild debug info: //#define DEBUG_CLAUSEALLOCATOR @@ -46,7 +47,7 @@ along with this program. If not, see . ClauseAllocator::ClauseAllocator() { assert(MIN_LIST_SIZE < MAXSIZE); - assert(sizeof(Clause) + 2*sizeof(Lit) > sizeof(NewPointerAndOffset)); + assert(sizeof(Clause) + 2*sizeof(Lit) >= sizeof(NewPointerAndOffset)); } /** @@ -55,7 +56,7 @@ ClauseAllocator::ClauseAllocator() ClauseAllocator::~ClauseAllocator() { for (uint32_t i = 0; i < dataStarts.size(); i++) { - delete [] dataStarts[i]; + free(dataStarts[i]); } } @@ -83,10 +84,9 @@ template Clause* ClauseAllocator::Clause_new(const XorClause& ps, const unsigned template XorClause* ClauseAllocator::XorClause_new(const T& ps, const bool xorEqualFalse, const unsigned int group) { - assert(ps.size() > 0); + assert(ps.size() > 2); void* mem = allocEnough(ps.size()); XorClause* real= new (mem) XorClause(ps, xorEqualFalse, group); - //assert(!(ps.size() == 2 && !real->wasBin())); return real; } @@ -155,8 +155,11 @@ void* ClauseAllocator::allocEnough(const uint32_t size) << ")" << std::endl; #endif //DEBUG_CLAUSEALLOCATOR - uint32_t *dataStart = new uint32_t[nextSize]; + uint32_t *dataStart; + posix_memalign((void**)&dataStart, getpagesize(), sizeof(uint32_t) * nextSize); assert(dataStart != NULL); + int err = madvise(dataStart, sizeof(uint32_t) * nextSize, MADV_RANDOM); + assert(err == 0); dataStarts.push(dataStart); sizes.push(0); maxSizes.push(nextSize); @@ -342,7 +345,10 @@ void ClauseAllocator::consolidate(Solver* solver) newSizes.push(0); newOrigClauseSizes.push(); uint32_t* pointer; - pointer = new uint32_t[newMaxSizes[i]]; + posix_memalign((void**)&pointer, getpagesize(), sizeof(uint32_t) * newMaxSizes[i]); + assert(pointer != NULL); + int err = madvise(pointer, sizeof(uint32_t) * newMaxSizes[i], MADV_RANDOM); + assert(err == 0); newDataStartsPointers.push(pointer); newDataStarts.push(pointer); } @@ -383,7 +389,7 @@ void ClauseAllocator::consolidate(Solver* solver) updateAllOffsetsAndPointers(solver); for (uint32_t i = 0; i < dataStarts.size(); i++) - delete [] dataStarts[i]; + free(dataStarts[i]); dataStarts.clear(); maxSizes.clear(); diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index e9ff050..2181d28 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -103,6 +103,7 @@ void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type, const uin __builtin_prefetch(*(s+1), 1, 0); if (cleanClause(*s)) { solver.clauseAllocator.clauseFree(*s); + if (type == learnts) solver.nbCompensateSubsumer++; } else { *ss++ = *s; } @@ -151,6 +152,7 @@ inline const bool ClauseCleaner::cleanClause(Clause*& cc) } else if (c.size() == 3) { solver.detachModifiedClause(origLit1, origLit2, origLit3, origSize, &c); solver.attachClause(c); + solver.dataSync->signalNewTriClause(c); } else { if (c.learnt()) solver.learnts_literals -= i-j; diff --git a/src/sat/cryptominisat2/ClauseVivifier.cpp b/src/sat/cryptominisat2/ClauseVivifier.cpp index b2413e3..ce18227 100644 --- a/src/sat/cryptominisat2/ClauseVivifier.cpp +++ b/src/sat/cryptominisat2/ClauseVivifier.cpp @@ -28,6 +28,29 @@ ClauseVivifier::ClauseVivifier(Solver& _solver) : , solver(_solver) {} +const bool ClauseVivifier::vivify() +{ + assert(solver.ok); + #ifdef VERBOSE_DEBUG + std::cout << "c clauseVivifier started" << std::endl; + //solver.printAllClauses(); + #endif //VERBOSE_DEBUG + + solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses); + numCalls++; + + if (numCalls >= 2) { + if (solver.conf.doCacheOTFSSR) { + if (!vivifyClausesCache(solver.clauses)) return false; + if (!vivifyClausesCache(solver.learnts)) return false; + } + } + + if (!vivifyClausesNormal()) return false; + + return true; +} + /** @brief Performs clause vivification (by Hamadi et al.) @@ -37,22 +60,9 @@ it is not part of failed literal probing, really. However, it is here because it seems to be a function that fits into the idology of failed literal probing. Maybe I am off-course and it should be in another class, or a class of its own. */ -const bool ClauseVivifier::vivifyClauses() +const bool ClauseVivifier::vivifyClausesNormal() { assert(solver.ok); - #ifdef VERBOSE_DEBUG - std::cout << "c clauseVivifier started" << std::endl; - //solver.printAllClauses(); - #endif //VERBOSE_DEBUG - - - solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses); - numCalls++; - - if (solver.ok && solver.conf.doCacheOTFSSR) { - if (!vivifyClauses2(solver.clauses)) return false; - if (/*solver.lastSelectedRestartType == static_restart &&*/ !vivifyClauses2(solver.learnts)) return false; - } bool failed; uint32_t effective = 0; @@ -134,8 +144,8 @@ const bool ClauseVivifier::vivifyClauses() } } done += i2; - failed = (!solver.propagate(false).isNULL()); - if (numCalls > 3 && failed) break; + failed = (!solver.propagate(false).isNULL()); + if (failed) break; } solver.cancelUntilLight(); assert(solver.ok); @@ -191,7 +201,7 @@ const bool ClauseVivifier::vivifyClauses() } -const bool ClauseVivifier::vivifyClauses2(vec& clauses) +const bool ClauseVivifier::vivifyClausesCache(vec& clauses) { assert(solver.ok); @@ -208,8 +218,7 @@ const bool ClauseVivifier::vivifyClauses2(vec& clauses) vec lits; bool needToFinish = false; double myTime = cpuTime(); - - if (numCalls < 3) return true; + const vector& cache = solver.transOTFCache; Clause** i = clauses.getData(); Clause** j = i; @@ -229,10 +238,10 @@ const bool ClauseVivifier::vivifyClauses2(vec& clauses) if (seen[l->toInt()] == 0) continue; Lit lit = *l; - countTime += solver.transOTFCache[l->toInt()].lits.size(); - for (vector::const_iterator it2 = solver.transOTFCache[l->toInt()].lits.begin() - , end2 = solver.transOTFCache[l->toInt()].lits.end(); it2 != end2; it2++) { - seen[(~(*it2)).toInt()] = 0; + countTime += cache[l->toInt()].lits.size(); + for (vector::const_iterator it2 = cache[l->toInt()].lits.begin() + , end2 = cache[l->toInt()].lits.end(); it2 != end2; it2++) { + seen[(~(it2->getLit())).toInt()] = 0; } } @@ -246,7 +255,7 @@ const bool ClauseVivifier::vivifyClauses2(vec& clauses) countTime += cl.size()*10; solver.detachClause(cl); clShrinked++; - Clause* c2 = solver.addClauseInt(lits, cl.getGroup(), cl.learnt(), cl.getGlue(), cl.getMiniSatAct()); + Clause* c2 = solver.addClauseInt(lits, cl.getGroup(), cl.learnt(), cl.getGlue()); solver.clauseAllocator.clauseFree(&cl); if (c2 != NULL) *j++ = c2; diff --git a/src/sat/cryptominisat2/ClauseVivifier.h b/src/sat/cryptominisat2/ClauseVivifier.h index d890e40..672f25f 100644 --- a/src/sat/cryptominisat2/ClauseVivifier.h +++ b/src/sat/cryptominisat2/ClauseVivifier.h @@ -23,11 +23,14 @@ along with this program. If not, see . class ClauseVivifier { public: ClauseVivifier(Solver& solver); - const bool vivifyClauses(); - const bool vivifyClauses2(vec& clauses); + const bool vivify(); + const bool vivifyClausesCache(vec& clauses); private: + //Actual algorithms used + const bool vivifyClausesNormal(); + /** @brief Records data for asymmBranch() diff --git a/src/sat/cryptominisat2/CompleteDetachReattacher.cpp b/src/sat/cryptominisat2/CompleteDetachReattacher.cpp index 97a53e2..613b424 100644 --- a/src/sat/cryptominisat2/CompleteDetachReattacher.cpp +++ b/src/sat/cryptominisat2/CompleteDetachReattacher.cpp @@ -78,7 +78,7 @@ const bool CompleteDetachReatacher::reattachNonBins() cleanAndAttachClauses(solver.xorclauses); solver.clauseCleaner->removeSatisfiedBins(); - if (solver.ok) solver.ok = (solver.propagate().isNULL()); + if (solver.ok) solver.ok = (solver.propagate().isNULL()); return solver.ok; } diff --git a/src/sat/cryptominisat2/DataSync.cpp b/src/sat/cryptominisat2/DataSync.cpp index 1c927e1..8f8c78b 100644 --- a/src/sat/cryptominisat2/DataSync.cpp +++ b/src/sat/cryptominisat2/DataSync.cpp @@ -19,26 +19,38 @@ along with this program. If not, see . #include "Subsumer.h" #include "VarReplacer.h" #include "XorSubsumer.h" +#include "PartHandler.h" #include +#include "omp.h" DataSync::DataSync(Solver& _solver, SharedData* _sharedData) : - lastSyncConf(0) - , sentUnitData(0) + sentUnitData(0) , recvUnitData(0) + , sentBinData(0) + , recvBinData(0) + , sentTriData(0) + , recvTriData(0) + , lastSyncConf(0) + , numCalls(0) , sharedData(_sharedData) , solver(_solver) -{} +{ +} void DataSync::newVar() { syncFinish.push(0); syncFinish.push(0); + syncFinishTri.push(0); + syncFinishTri.push(0); seen.push(false); seen.push(false); } const bool DataSync::syncData() { + numCalls++; + if (solver.numThreads == 1) return true; if (sharedData == NULL || lastSyncConf + SYNC_EVERY_CONFL >= solver.conflicts) return true; @@ -46,17 +58,60 @@ const bool DataSync::syncData() assert(solver.decisionLevel() == 0); bool ok; - #pragma omp critical (unitData) - ok = shareUnitData(); - if (!ok) return false; + #pragma omp critical (ERSync) + { + if (!sharedData->EREnded + && sharedData->threadAddingVars == solver.threadNum + && solver.subsumer->getFinishedAddingVars()) + syncERVarsFromHere(); + + if (sharedData->EREnded + && sharedData->threadAddingVars != solver.threadNum + && sharedData->othersSyncedER.find(solver.threadNum) == sharedData->othersSyncedER.end()) + syncERVarsToHere(); + + if (sharedData->othersSyncedER.size() == (uint32_t)(solver.numThreads-1)) { + sharedData->threadAddingVars = (sharedData->threadAddingVars+1) % solver.numThreads; + sharedData->EREnded = false; + sharedData->othersSyncedER.clear(); + } + + #pragma omp critical (unitData) + ok = shareUnitData(); + if (!ok) goto end; + + #pragma omp critical (binData) + ok = shareBinData(); + if (!ok) goto end; - #pragma omp critical (binData) - ok = shareBinData(); - if (!ok) return false; + #pragma omp critical (triData) + ok = shareTriData(); + if (!ok) goto end; + + end:; + } lastSyncConf = solver.conflicts; - return true; + return solver.ok; +} + +void DataSync::syncERVarsToHere() +{ + for (uint32_t i = 0; i < sharedData->numNewERVars; i++) { + Var var = solver.newVar(); + solver.subsumer->setVarNonEliminable(var); + } + solver.subsumer->incNumERVars(sharedData->numNewERVars); + sharedData->othersSyncedER.insert(solver.threadNum); +} + +void DataSync::syncERVarsFromHere() +{ + sharedData->EREnded = true; + sharedData->numNewERVars = solver.subsumer->getNumERVars() - sharedData->lastNewERVars; + sharedData->lastNewERVars = solver.subsumer->getNumERVars(); + solver.subsumer->setFinishedAddingVars(false); } const bool DataSync::shareBinData() @@ -76,11 +131,10 @@ const bool DataSync::shareBinData() || solver.value(lit1.var()) != l_Undef ) continue; - vector& bins = shared.bins[wsLit]; - vec& ws = solver.watches[wsLit]; + vector& bins = shared.bins[wsLit]; if (bins.size() > syncFinish[wsLit] - && !syncBinFromOthers(lit1, bins, syncFinish[wsLit], ws)) return false; + && !syncBinFromOthers(lit1, bins, syncFinish[wsLit])) return false; } syncBinToOthers(); @@ -94,50 +148,202 @@ const bool DataSync::shareBinData() } template -void DataSync::signalNewBinClause(T& ps) +void DataSync::signalNewBinClause(const T& ps, const bool learnt) { assert(ps.size() == 2); - signalNewBinClause(ps[0], ps[1]); + signalNewBinClause(ps[0], ps[1], learnt); } +template void DataSync::signalNewBinClause(const Clause& ps, const bool learnt); +template void DataSync::signalNewBinClause(const XorClause& ps, const bool learnt); +template void DataSync::signalNewBinClause(const vec& ps, const bool learnt); -void DataSync::signalNewBinClause(Lit lit1, Lit lit2) +void DataSync::signalNewBinClause(Lit lit1, Lit lit2, const bool learnt) { if (lit1.toInt() > lit2.toInt()) std::swap(lit1, lit2); - newBinClauses.push_back(std::make_pair(lit1, lit2)); + newBinClauses.push_back(BinClause(lit1, lit2, learnt)); } -template void DataSync::signalNewBinClause(Clause& ps); -template void DataSync::signalNewBinClause(XorClause& ps); -template void DataSync::signalNewBinClause(vec& ps); +template +void DataSync::signalNewTriClause(const T& ps, const bool learnt) +{ + assert(ps.size() == 3); + signalNewTriClause(ps[0], ps[1], ps[2], learnt); +} +template void DataSync::signalNewTriClause(const Clause& ps, const bool learnt); +template void DataSync::signalNewTriClause(const vec& ps, const bool learnt); -const bool DataSync::syncBinFromOthers(const Lit lit, const vector& bins, uint32_t& finished, vec& ws) +void DataSync::signalNewTriClause(const Lit lit1, const Lit lit2, const Lit lit3, const bool learnt) +{ + Lit lits[3]; + lits[0] = lit1; + lits[1] = lit2; + lits[2] = lit3; + std::sort(lits + 0, lits + 3); + newTriClauses.push_back(TriClause(lits[0], lits[1], lits[2], learnt)); +} + +const bool DataSync::shareTriData() +{ + uint32_t oldRecvTriData = recvTriData; + uint32_t oldSentTriData = sentTriData; + + SharedData& shared = *sharedData; + if (shared.tris.size() != solver.nVars()*2) + shared.tris.resize(solver.nVars()*2); + + for (uint32_t wsLit = 0; wsLit < solver.nVars()*2; wsLit++) { + Lit lit1 = ~Lit::toLit(wsLit); + lit1 = solver.varReplacer->getReplaceTable()[lit1.var()] ^ lit1.sign(); + if (solver.subsumer->getVarElimed()[lit1.var()] + || solver.xorSubsumer->getVarElimed()[lit1.var()] + || solver.partHandler->getSavedState()[lit1.var()] != l_Undef + || solver.value(lit1.var()) != l_Undef + ) continue; + + vector& tris = shared.tris[wsLit]; + + if (tris.size() > syncFinishTri[wsLit] + && !syncTriFromOthers(lit1, tris, syncFinishTri[wsLit])) return false; + } + + syncTriToOthers(); + + if (solver.conf.verbosity >= 3) { + std::cout << "c got tris " << std::setw(10) << (recvTriData - oldRecvTriData) + << std::setw(10) << " sent tris " << (sentTriData - oldSentTriData) << std::endl; + } + + return true; +} + +const bool DataSync::syncTriFromOthers(const Lit lit1, const vector& tris, uint32_t& finished) +{ + assert(solver.ok); + assert(solver.varReplacer->getReplaceTable()[lit1.var()].var() == lit1.var()); + assert(solver.subsumer->getVarElimed()[lit1.var()] == false); + assert(solver.xorSubsumer->getVarElimed()[lit1.var()] == false); + assert(solver.partHandler->getSavedState()[lit1.var()] == l_Undef); + + vec tmp; + for (uint32_t i = finished; i < tris.size(); i++) { + const TriClause& cl = tris[i]; + + Lit lit2 = solver.varReplacer->getReplaceTable()[cl.lit2.var()] ^ cl.lit2.sign(); + if (solver.subsumer->getVarElimed()[lit2.var()] + || solver.xorSubsumer->getVarElimed()[lit2.var()] + || solver.partHandler->getSavedState()[lit2.var()] != l_Undef + ) continue; + + Lit lit3 = solver.varReplacer->getReplaceTable()[cl.lit3.var()] ^ cl.lit3.sign(); + if (solver.subsumer->getVarElimed()[lit3.var()] + || solver.xorSubsumer->getVarElimed()[lit3.var()] + || solver.partHandler->getSavedState()[lit3.var()] != l_Undef + ) continue; + + bool alreadyInside = false; + const vec& ws = solver.watches[(~lit1).toInt()]; + for (const Watched *it = ws.getData(), *end = ws.getDataEnd(); it != end; it++) { + if (it->isTriClause()) { + if (it->getOtherLit() == lit2 + && it->getOtherLit2() == lit3) alreadyInside = true; + + if (it->getOtherLit2() == lit2 + && it->getOtherLit() == lit3) alreadyInside = true; + } + } + if (alreadyInside) continue; + + const vec& ws2 = solver.watches[(~lit2).toInt()]; + for (const Watched *it = ws2.getData(), *end = ws2.getDataEnd(); it != end; it++) { + if (it->isTriClause()) { + if (it->getOtherLit() == lit1 + && it->getOtherLit2() == lit3) alreadyInside = true; + + if (it->getOtherLit2() == lit3 + && it->getOtherLit() == lit1) alreadyInside = true; + } + } + if (alreadyInside) continue; + + tmp.clear(); + tmp.growTo(3); + tmp[0] = lit1; + tmp[1] = lit2; + tmp[2] = lit3; + Clause* c = solver.addClauseInt(tmp, 0, cl.learnt, 3, true); + if (c != NULL) solver.learnts.push(c); + if (!solver.ok) return false; + recvTriData++; + } + finished = tris.size(); + + return true; +} + +void DataSync::syncTriToOthers() +{ + for(vector::const_iterator it = newTriClauses.begin(), end = newTriClauses.end(); it != end; it++) { + addOneTriToOthers(it->lit1, it->lit2, it->lit3); + sentTriData++; + } + + for (uint32_t i = 0; i < sharedData->tris.size(); i++) { + syncFinishTri[i] = sharedData->tris[i].size(); + } + + newTriClauses.clear(); +} + +void DataSync::addOneTriToOthers(const Lit lit1, const Lit lit2, const Lit lit3) +{ + assert(lit1.toInt() < lit2.toInt()); + assert(lit2.toInt() < lit3.toInt()); + + vector& tris = sharedData->tris[(~lit1).toInt()]; + for (vector::const_iterator it = tris.begin(), end = tris.end(); it != end; it++) { + if (it->lit2 == lit2 + && it->lit3 == lit3) return; + } + + tris.push_back(TriClause(lit1, lit2, lit3)); +} + +const bool DataSync::syncBinFromOthers(const Lit lit, const vector& bins, uint32_t& finished) { assert(solver.varReplacer->getReplaceTable()[lit.var()].var() == lit.var()); assert(solver.subsumer->getVarElimed()[lit.var()] == false); assert(solver.xorSubsumer->getVarElimed()[lit.var()] == false); + assert(solver.partHandler->getSavedState()[lit.var()] == l_Undef); vec addedToSeen; - for (Watched *it = ws.getData(), *end = ws.getDataEnd(); it != end; it++) { + const vec& ws = solver.watches[(~lit).toInt()]; + for (const Watched *it = ws.getData(), *end = ws.getDataEnd(); it != end; it++) { if (it->isBinary()) { addedToSeen.push(it->getOtherLit()); seen[it->getOtherLit().toInt()] = true; } } + const vector& cache = solver.transOTFCache[(~lit).toInt()].lits; + for (vector::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) { + addedToSeen.push(it->getLit()); + seen[it->getLit().toInt()] = true; + } vec lits(2); for (uint32_t i = finished; i < bins.size(); i++) { - if (!seen[bins[i].toInt()]) { - Lit otherLit = bins[i]; + if (!seen[bins[i].lit2.toInt()]) { + Lit otherLit = bins[i].lit2; otherLit = solver.varReplacer->getReplaceTable()[otherLit.var()] ^ otherLit.sign(); if (solver.subsumer->getVarElimed()[otherLit.var()] || solver.xorSubsumer->getVarElimed()[otherLit.var()] + || solver.partHandler->getSavedState()[otherLit.var()] != l_Undef || solver.value(otherLit.var()) != l_Undef ) continue; recvBinData++; lits[0] = lit; lits[1] = otherLit; - solver.addClauseInt(lits, 0, true, 2, 0, true); + solver.addClauseInt(lits, 0, bins[i].learnt, 2, true); lits.clear(); lits.growTo(2); if (!solver.ok) goto end; @@ -154,24 +360,28 @@ const bool DataSync::syncBinFromOthers(const Lit lit, const vector& bins, u void DataSync::syncBinToOthers() { - for(vector >::const_iterator it = newBinClauses.begin(), end = newBinClauses.end(); it != end; it++) { - addOneBinToOthers(it->first, it->second); + for(vector::const_iterator it = newBinClauses.begin(), end = newBinClauses.end(); it != end; it++) { + addOneBinToOthers(it->lit1, it->lit2, it->learnt); + sentBinData++; + } + + for (uint32_t i = 0; i < sharedData->bins.size(); i++) { + syncFinish[i] = sharedData->bins[i].size(); } newBinClauses.clear(); } -void DataSync::addOneBinToOthers(const Lit lit1, const Lit lit2) +void DataSync::addOneBinToOthers(const Lit lit1, const Lit lit2, const bool learnt) { assert(lit1.toInt() < lit2.toInt()); - vector& bins = sharedData->bins[(~lit1).toInt()]; - for (vector::const_iterator it = bins.begin(), end = bins.end(); it != end; it++) { - if (*it == lit2) return; + vector& bins = sharedData->bins[(~lit1).toInt()]; + for (vector::const_iterator it = bins.begin(), end = bins.end(); it != end; it++) { + if (it->lit2 == lit2 && it->learnt == learnt) return; } - bins.push_back(lit2); - sentBinData++; + bins.push_back(BinClause(lit1, lit2, learnt)); } const bool DataSync::shareUnitData() @@ -202,10 +412,11 @@ const bool DataSync::shareUnitData() Lit litToEnqueue = thisLit ^ (otherVal == l_False); if (solver.subsumer->getVarElimed()[litToEnqueue.var()] || solver.xorSubsumer->getVarElimed()[litToEnqueue.var()] + || solver.partHandler->getSavedState()[litToEnqueue.var()] != l_Undef ) continue; solver.uncheckedEnqueue(litToEnqueue); - solver.ok = solver.propagate().isNULL(); + solver.ok = solver.propagate().isNULL(); if (!solver.ok) return false; thisGotUnitData++; continue; diff --git a/src/sat/cryptominisat2/DataSync.h b/src/sat/cryptominisat2/DataSync.h index b049fc4..fadd36c 100644 --- a/src/sat/cryptominisat2/DataSync.h +++ b/src/sat/cryptominisat2/DataSync.h @@ -25,33 +25,55 @@ class DataSync void newVar(); const bool syncData(); + //New clause signalation + template void signalNewBinClause(const T& ps, const bool learnt = true); + void signalNewBinClause(Lit lit1, Lit lit2, const bool learnt = true); + template void signalNewTriClause(const T& ps, const bool learnt = true); + void signalNewTriClause(const Lit lit1, const Lit lit2, const Lit lit3, const bool learnt = true); - template void signalNewBinClause(T& ps); - void signalNewBinClause(Lit lit1, Lit lit2); - + //Get methods const uint32_t getSentUnitData() const; const uint32_t getRecvUnitData() const; const uint32_t getSentBinData() const; const uint32_t getRecvBinData() const; + const uint32_t getSentTriData() const; + const uint32_t getRecvTriData() const; + const int getThreadAddingVars() const; + const bool getEREnded() const; private: - //functions + //unitary shring functions const bool shareUnitData(); - const bool syncBinFromOthers(const Lit lit, const vector& bins, uint32_t& finished, vec& ws); - void syncBinToOthers(); - void addOneBinToOthers(const Lit lit1, const Lit lit2); - const bool shareBinData(); + uint32_t sentUnitData; + uint32_t recvUnitData; - //stuff to sync - vector > newBinClauses; + //bin sharing functions + const bool shareBinData(); + vector newBinClauses; + const bool syncBinFromOthers(const Lit lit, const vector& bins, uint32_t& finished); + void syncBinToOthers(); + void addOneBinToOthers(const Lit lit1, const Lit lit2, const bool leanrt); + vec syncFinish; + uint32_t sentBinData; + uint32_t recvBinData; + + //tri sharing functions + const bool shareTriData(); + vector newTriClauses; + const bool syncTriFromOthers(const Lit lit1, const vector& tris, uint32_t& finished); + void syncTriToOthers(); + void addOneTriToOthers(const Lit lit1, const Lit lit2, const Lit lit3); + vec syncFinishTri; + uint32_t sentTriData; + uint32_t recvTriData; + + //ER sharing + void syncERVarsToHere(); + void syncERVarsFromHere(); //stats uint64_t lastSyncConf; - vec syncFinish; - uint32_t sentUnitData; - uint32_t recvUnitData; - uint32_t sentBinData; - uint32_t recvBinData; + uint32_t numCalls; //misc vec seen; @@ -81,3 +103,24 @@ inline const uint32_t DataSync::getRecvBinData() const return recvBinData; } +inline const uint32_t DataSync::getSentTriData() const +{ + return sentTriData; +} + +inline const uint32_t DataSync::getRecvTriData() const +{ + return recvTriData; +} + +inline const int DataSync::getThreadAddingVars() const +{ + if (sharedData == NULL) return 0; + else return sharedData->threadAddingVars; +} + +inline const bool DataSync::getEREnded() const +{ + if (sharedData == NULL) return false; + return sharedData->EREnded; +} diff --git a/src/sat/cryptominisat2/DimacsParser.cpp b/src/sat/cryptominisat2/DimacsParser.cpp index e8c4671..ace9f60 100644 --- a/src/sat/cryptominisat2/DimacsParser.cpp +++ b/src/sat/cryptominisat2/DimacsParser.cpp @@ -11,7 +11,7 @@ Modifications for CryptoMiniSat are under GPLv3 licence. #include #include -#include "Solver.h" +#include "MTSolver.h" #ifdef VERBOSE_DEBUG #define DEBUG_COMMENT_PARSING @@ -19,12 +19,11 @@ Modifications for CryptoMiniSat are under GPLv3 licence. //#define DEBUG_COMMENT_PARSING -DimacsParser::DimacsParser(Solver* _solver, const bool _debugLib, const bool _debugNewVar, const bool _grouping, const bool _addAsLearnt): +DimacsParser::DimacsParser(MTSolver* _solver, const bool _debugLib, const bool _debugNewVar, const bool _grouping): solver(_solver) , debugLib(_debugLib) , debugNewVar(_debugNewVar) , grouping(_grouping) - , addAsLearnt(_addAsLearnt) , groupId(0) {} @@ -175,7 +174,7 @@ void DimacsParser::printHeader(StreamBuffer& in) if (match(in, "p cnf")) { int vars = parseInt(in, len); int clauses = parseInt(in, len); - if (solver->conf.verbosity >= 1) { + if (solver->getVerbosity() >= 1) { std::cout << "c -- header says num vars: " << std::setw(12) << vars << std::endl; std::cout << "c -- header says num clauses:" << std::setw(12) << clauses << std::endl; } @@ -254,7 +253,7 @@ void DimacsParser::parseComments(StreamBuffer& in, const std::string str) /** @brief Parses clause parameters given as e.g. "c clause learnt yes glue 4 miniSatAct 5.2" */ -void DimacsParser::parseClauseParameters(StreamBuffer& in, bool& learnt, uint32_t& glue, float& miniSatAct) +void DimacsParser::parseClauseParameters(StreamBuffer& in, bool& learnt, uint32_t& glue) { std::string str; uint32_t len; @@ -290,15 +289,6 @@ void DimacsParser::parseClauseParameters(StreamBuffer& in, bool& learnt, uint32_ glue = parseInt(in, len); //std::cout << "glue: " << glue << std::endl; - //Parse in MiniSat activity - ++in; - parseString(in, str); - if (str != "miniSatAct") goto addTheClause; - //std::cout << "read MINISATACT" << std::endl; - ++in; - miniSatAct = parseFloat(in); - //std::cout << "MiniSatAct:" << miniSatAct << std::endl; - addTheClause: skipLine(in); return; @@ -319,8 +309,7 @@ void DimacsParser::readFullClause(StreamBuffer& in) { bool xor_clause = false; bool learnt = false; - uint32_t glue = 100.0; - float miniSatAct = 10.0; + uint32_t glue = 100; std::string name; std::string str; uint32_t len; @@ -359,7 +348,7 @@ void DimacsParser::readFullClause(StreamBuffer& in) ++in; parseString(in, str); if (str == "clause") { - parseClauseParameters(in, learnt, glue, miniSatAct); + parseClauseParameters(in, learnt, glue); } else { needToParseComments = true; } @@ -373,8 +362,8 @@ void DimacsParser::readFullClause(StreamBuffer& in) solver->addXorClause(lits, xorEqualFalse, groupId, name.c_str()); numXorClauses++; } else { - if (addAsLearnt || learnt) { - solver->addLearntClause(lits, groupId, NULL, glue, miniSatAct); + if (learnt) { + solver->addLearntClause(lits, groupId, NULL, glue); numLearntClauses++; } else { solver->addClause(lits, groupId, name.c_str()); @@ -434,7 +423,7 @@ void DimacsParser::parse_DIMACS(T input_stream) StreamBuffer in(input_stream); parse_DIMACS_main(in); - if (solver->conf.verbosity >= 1) { + if (solver->getVerbosity() >= 1) { std::cout << "c -- clauses added: " << std::setw(12) << numLearntClauses << " learnts, " diff --git a/src/sat/cryptominisat2/DimacsParser.h b/src/sat/cryptominisat2/DimacsParser.h index f264637..56bfd30 100644 --- a/src/sat/cryptominisat2/DimacsParser.h +++ b/src/sat/cryptominisat2/DimacsParser.h @@ -29,7 +29,7 @@ Modifications for CryptoMiniSat are under GPLv3 licence. #include "Logger.h" #endif //STATS_NEEDED -class Solver; +class MTSolver; /** @brief Parses up a DIMACS file that my be zipped @@ -37,7 +37,7 @@ class Solver; class DimacsParser { public: - DimacsParser(Solver* solver, const bool debugLib, const bool debugNewVar, const bool grouping, const bool addAsLearnt = false); + DimacsParser(MTSolver* solver, const bool debugLib, const bool debugNewVar, const bool grouping); template void parse_DIMACS(T input_stream); @@ -51,7 +51,7 @@ class DimacsParser float parseFloat(StreamBuffer& in); void parseString(StreamBuffer& in, std::string& str); void readClause(StreamBuffer& in, vec& lits); - void parseClauseParameters(StreamBuffer& in, bool& learnt, uint32_t& glue, float& miniSatAct); + void parseClauseParameters(StreamBuffer& in, bool& learnt, uint32_t& glue); void readFullClause(StreamBuffer& in); bool match(StreamBuffer& in, const char* str); void printHeader(StreamBuffer& in); @@ -59,11 +59,10 @@ class DimacsParser std::string stringify(uint32_t x); - Solver *solver; + MTSolver *solver; const bool debugLib; const bool debugNewVar; const bool grouping; - const bool addAsLearnt; uint32_t debugLibPart; /// 0) { + BothCache bothCache(solver); + if (!bothCache.tryBoth(solver.transOTFCache)) return false; + } - uint64_t numProps = 100 * 1000000; + uint64_t numProps = 80 * 1000000; uint64_t numPropsDifferent = (double)numProps*2.0; solver.testAllClauseAttach(); @@ -208,11 +214,12 @@ const bool FailedLitSearcher::search() //For HyperBin addedBin = 0; + addedCacheBin = 0; unPropagatedBin.resize(solver.nVars(), 0); needToVisit.resize(solver.nVars(), 0); dontRemoveAncestor.resize(solver.nVars(), 0); hyperbinProps = 0; - maxHyperBinProps = numProps/4; + maxHyperBinProps = numProps/3; removedUselessLearnt = 0; removedUselessNonLearnt = 0; @@ -230,7 +237,21 @@ const bool FailedLitSearcher::search() } lastTimeStopped = (lastTimeStopped + i) % solver.nVars(); + calcNegPosDist(); + origProps = solver.propagations; + /*hyperbinProps = 0; + for (uint32_t i = 0; i < solver.negPosDist.size(); i++) { + Var var = solver.negPosDist[i].var; + if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) + continue; + if (solver.propagations >= origProps + numPropsDifferent) { + break; + } + if (!tryBoth(Lit(var, false), Lit(var, true))) + goto end; + }*/ + while (!order_heap_copy.empty()) { Var var = order_heap_copy.removeMin(); if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) @@ -241,12 +262,10 @@ const bool FailedLitSearcher::search() if (!tryBoth(Lit(var, false), Lit(var, true))) goto end; } - - if (solver.conf.verbosity >= 1) printResults(myTime); - + //if (!tryMultiLevelAll()) goto end; end: - bool removedOldLearnts = false; + if (solver.conf.verbosity >= 1) printResults(myTime); solver.order_heap.filter(Solver::VarFilter(solver)); @@ -257,7 +276,6 @@ end: reattacher.detachNonBinsNonTris(true); const bool ret = reattacher.reattachNonBins(); release_assert(ret == true); - removedOldLearnts = true; } else { solver.clauseCleaner->removeAndCleanAll(); } @@ -297,9 +315,10 @@ void FailedLitSearcher::printResults(const double myTime) const " Blit: " << std::setw(6) << goodBothSame << " bXBeca: " << std::setw(4) << newBinXor << " bXProp: " << std::setw(4) << bothInvert << - " Bins:" << std::setw(7) << addedBin << + " Bin:" << std::setw(7) << addedBin << " BRemL:" << std::setw(7) << removedUselessLearnt << " BRemN:" << std::setw(7) << removedUselessNonLearnt << + " CBin: " << std::setw(7) << addedCacheBin << " P: " << std::setw(4) << std::fixed << std::setprecision(1) << (double)(solver.propagations - origProps)/1000000.0 << "M" " T: " << std::setw(5) << std::fixed << std::setprecision(2) << cpuTime() - myTime << std::endl; @@ -326,13 +345,16 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) investigateXor.clear(); } - propagated.setZero(); + propagated.removeThese(propagatedBitSet); + assert(propagated.isZero()); + propagatedBitSet.clear(); twoLongXors.clear(); bothSame.clear(); binXorToAdd.clear(); #ifdef DEBUG_HYPERBIN assert(propagatedVars.empty()); assert(unPropagatedBin.isZero()); + assert(addBinLater.empty()); #endif //DEBUG_HYPERBIN #ifdef DEBUG_USELESS_LEARNT_BIN_REMOVAL dontRemoveAncestor.isZero(); @@ -341,25 +363,23 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit1); - failed = (!solver.propagate(false).isNULL()); + failed = (!solver.propagate(false).isNULL()); if (failed) { solver.cancelUntilLight(); numFailed++; solver.uncheckedEnqueue(~lit1); - solver.ok = (solver.propagate(false).isNULL()); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; return true; } assert(solver.decisionLevel() > 0); - Solver::TransCache& lit1OTFCache = solver.transOTFCache[(~lit1).toInt()]; - if (solver.conf.doCacheOTFSSR) { - lit1OTFCache.conflictLastUpdated = solver.conflicts; - lit1OTFCache.lits.clear(); - } + //vector oldCache; + vector lit1OTFCache; for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { Var x = solver.trail[c].var(); propagated.setBit(x); + propagatedBitSet.push_back(x); if (solver.conf.doHyperBinRes) { unPropagatedBin.setBit(x); @@ -371,9 +391,13 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) if (binXorFind) removeVarFromXors(x); if (solver.conf.doCacheOTFSSR && c != (int)solver.trail_lim[0]) { - lit1OTFCache.lits.push_back(solver.trail[c]); + lit1OTFCache.push_back(LitExtra(solver.trail[c], false)); } } + if (solver.conf.doCacheOTFSSR) { + solver.transOTFCache[(~lit1).toInt()].merge(lit1OTFCache); + solver.transOTFCache[(~lit1).toInt()].conflictLastUpdated = solver.conflicts; + } if (binXorFind) { for (uint32_t *it = investigateXor.getData(), *end = investigateXor.getDataEnd(); it != end; it++) { @@ -389,36 +413,30 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) solver.cancelUntilLight(); - //Hyper-binary resolution, and its accompanying data-structure cleaning - if (solver.conf.doHyperBinRes) { - if (hyperbinProps < maxHyperBinProps) hyperBinResolution(lit1); - unPropagatedBin.removeThese(propagatedVars); - propagatedVars.clear(); - } + if (solver.conf.doHyperBinRes) hyperBinResAll(lit1/*, oldCache*/); + //oldCache.clear(); + if (!performAddBinLaters()) return false; #ifdef DEBUG_HYPERBIN assert(propagatedVars.empty()); assert(unPropagatedBin.isZero()); + assert(addBinLater.empty()); #endif //DEBUG_HYPERBIN solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit2); - failed = (!solver.propagate(false).isNULL()); + failed = (!solver.propagate(false).isNULL()); if (failed) { solver.cancelUntilLight(); numFailed++; solver.uncheckedEnqueue(~lit2); - solver.ok = (solver.propagate(false).isNULL()); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; return true; } assert(solver.decisionLevel() > 0); - Solver::TransCache& lit2OTFCache = solver.transOTFCache[(~lit2).toInt()]; - if (solver.conf.doCacheOTFSSR) { - lit2OTFCache.conflictLastUpdated = solver.conflicts; - lit2OTFCache.lits.clear(); - } + vector lit2OTFCache; for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { Var x = solver.trail[c].var(); if (propagated[x]) { @@ -426,18 +444,10 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) //they both imply the same bothSame.push(Lit(x, !propValue[x])); } else if (c != (int)solver.trail_lim[0]) { - bool invert; - if (lit1.var() == lit2.var()) { - assert(lit1.sign() == false && lit2.sign() == true); - tmpPs[0] = Lit(lit1.var(), false); - tmpPs[1] = Lit(x, false); - invert = propValue[x]; - } else { - tmpPs[0] = Lit(lit1.var(), false); - tmpPs[1] = Lit(lit2.var(), false); - invert = lit1.sign() ^ lit2.sign(); - } - binXorToAdd.push_back(BinXorToAdd(tmpPs[0], tmpPs[1], invert, 0)); + assert(lit1.var() == lit2.var()); + tmpPs[0] = Lit(lit1.var(), false); + tmpPs[1] = Lit(x, false); + binXorToAdd.push_back(BinXorToAdd(tmpPs[0], tmpPs[1], propValue[x], 0)); bothInvert += solver.varReplacer->getNewToReplaceVars() - toReplaceBefore; toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); } @@ -453,9 +463,13 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) if (binXorFind) removeVarFromXors(x); if (solver.conf.doCacheOTFSSR && c != (int)solver.trail_lim[0]) { - lit2OTFCache.lits.push_back(solver.trail[c]); + lit2OTFCache.push_back(LitExtra(solver.trail[c], false)); } } + if (solver.conf.doCacheOTFSSR) { + solver.transOTFCache[(~lit2).toInt()].merge(lit2OTFCache); + solver.transOTFCache[(~lit2).toInt()].conflictLastUpdated = solver.conflicts; + } //We now add the two-long xors that have been found through longer //xor-shortening @@ -480,17 +494,15 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) } solver.cancelUntilLight(); - if (solver.conf.doHyperBinRes) { - if (hyperbinProps < maxHyperBinProps) hyperBinResolution(lit2); - unPropagatedBin.removeThese(propagatedVars); - propagatedVars.clear(); - } + if (solver.conf.doHyperBinRes) hyperBinResAll(lit2/*, oldCache*/); + //oldCache.clear(); + if (!performAddBinLaters()) return false; for(uint32_t i = 0; i != bothSame.size(); i++) { solver.uncheckedEnqueue(bothSame[i]); } goodBothSame += bothSame.size(); - solver.ok = (solver.propagate(false).isNULL()); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; for (uint32_t i = 0; i < binXorToAdd.size(); i++) { @@ -505,6 +517,47 @@ const bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) return true; } +const bool FailedLitSearcher::performAddBinLaters() +{ + assert(solver.ok); + for (vector >::const_iterator it = addBinLater.begin(), end = addBinLater.end(); it != end; it++) { + tmpPs[0] = it->first; + tmpPs[1] = it->second; + Clause *c = solver.addClauseInt(tmpPs, 0, true); + release_assert(c == NULL); + tmpPs.clear(); + tmpPs.growTo(2); + if (!solver.ok) return false; + addedCacheBin++; + } + addBinLater.clear(); + + return true; +} + +void FailedLitSearcher::hyperBinResAll(const Lit litProp/*, const vector& oldCache*/) +{ + /*if (solver.conf.doAddBinCache) { + //Not forgetting stuff already known at one point from cache + for (vector::const_iterator it = oldCache.begin(), end = oldCache.end(); it != end; it++) { + const Lit lit = *it; + if (solver.value(lit.var()) != l_Undef + || solver.subsumer->getVarElimed()[lit.var()] + || solver.xorSubsumer->getVarElimed()[lit.var()] + || solver.varReplacer->getReplaceTable()[lit.var()].var() != lit.var() + || solver.partHandler->getSavedState()[lit.var()] != l_Undef) + continue; + + if (!unPropagatedBin[it->var()]) addBinLater.push_back(std::make_pair(~litProp, *it)); + } + }*/ + + //Hyper-binary resolution + if (hyperbinProps < maxHyperBinProps) hyperBinResolution(litProp); + unPropagatedBin.removeThese(propagatedVars); + propagatedVars.clear(); +} + /** @brief Adds hyper-binary clauses @@ -556,7 +609,7 @@ void FailedLitSearcher::hyperBinResolution(const Lit lit) continue; } - Var ancestorVar = solver.binPropData[it->var()].lev2Ancestor.var(); + Var ancestorVar = solver.binPropData[it->var()].lev1Ancestor.var(); dontRemoveAncestor.setBit(ancestorVar); toClearDontRemoveAcestor.push(ancestorVar); } @@ -622,23 +675,15 @@ void FailedLitSearcher::hyperBinResolution(const Lit lit) //difference between UP and BTC is in unPropagatedBin for (Lit *l = toVisit.getData(), *end = toVisit.getDataEnd(); l != end; l++) { if (!needToVisit[l->var()]) continue; + if (!solver.binPropData[l->var()].hasChildren) continue; fillImplies(*l); - for (const Var *var = myImpliesSet.getData(), *end2 = myImpliesSet.getDataEnd(); var != end2; var++) { - - /*Lit otherLit = Lit(*var, !propValue[*var]); - std::cout << "adding Bin:" << (~*l) << " , " << otherLit << std::endl; - std::cout << PropByFull(solver.reason[otherLit.var()], solver.failBinLit, solver.clauseAllocator) << std::endl;*/ - - addBin(~*l, Lit(*var, !propValue[*var])); - unPropagatedBin.clearBit(*var); - difference--; - } + addMyImpliesSetAsBins(*l, difference); assert(difference >= 0); myImpliesSet.clear(); if (difference == 0) { - needToVisit.setZero(); - goto end; + needToVisit.removeTheseLit(toVisit); + break; } } #ifdef DEBUG_HYPERBIN @@ -650,6 +695,66 @@ void FailedLitSearcher::hyperBinResolution(const Lit lit) hyperbinProps += solver.propagations - oldProps + extraTime; } +void FailedLitSearcher::addMyImpliesSetAsBins(Lit lit, int32_t& difference) +{ + if (myImpliesSet.size() == 0) return; + if (myImpliesSet.size() == 1) { + Var var = myImpliesSet[0]; + Lit l2 = Lit(var, !propValue[var]); + addBin(~lit, l2); + unPropagatedBin.clearBit(var); + difference--; + return; + } + + vector litsAddedEach; + uint32_t i = 0; + for (const Var *var = myImpliesSet.getData(), *end2 = myImpliesSet.getDataEnd(); var != end2; var++, i++) { + Lit l2 = Lit(*var, !propValue[*var]); + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(l2); + failed = (!solver.propagateBin(uselessBin).isNULL()); + assert(!failed); + uselessBin.clear(); + + BinAddData addData; + addData.lit = l2; + assert(solver.decisionLevel() > 0); + for (int sublevel = solver.trail.size()-1; sublevel > (int)solver.trail_lim[0]; sublevel--) { + Lit x = solver.trail[sublevel]; + addData.lits.push_back(x); + } + solver.cancelUntilLight(); + litsAddedEach.push_back(addData); + } + std::sort(litsAddedEach.begin(), litsAddedEach.end(), BinAddDataSorter()); + + while(!litsAddedEach.empty()) { + assert(!litsAddedEach.empty()); + BinAddData b = *litsAddedEach.begin(); + litsAddedEach.erase(litsAddedEach.begin()); + + addBin(~lit, b.lit); + assert(unPropagatedBin[b.lit.var()]); + unPropagatedBin.clearBit(b.lit.var()); + difference--; + for (uint32_t i = 0; i < b.lits.size(); i++) { + Lit alsoAddedLit = b.lits[i]; + if (unPropagatedBin[alsoAddedLit.var()]) { + unPropagatedBin.clearBit(alsoAddedLit.var()); + difference--; + for (vector::iterator it2 = litsAddedEach.begin(); it2 != litsAddedEach.end(); it2++) { + if (it2->lit == alsoAddedLit) { + litsAddedEach.erase(it2); + break; + } + } + } + } + } + assert(litsAddedEach.empty()); +} + /** @brief Fills myimplies and myimpliesSet by propagating lit at a binary level @@ -661,7 +766,7 @@ void FailedLitSearcher::fillImplies(const Lit lit) { solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit); - failed = (!solver.propagate(false).isNULL()); + failed = (!solver.propagate(false).isNULL()); assert(!failed); assert(solver.decisionLevel() > 0); @@ -697,3 +802,149 @@ void FailedLitSearcher::addBin(const Lit lit1, const Lit lit2) assert(solver.ok); addedBin++; } + +void FailedLitSearcher::fillToTry(vec& toTry) +{ + uint32_t max = std::min(solver.negPosDist.size()-1, (size_t)300); + while(true) { + Var var = solver.negPosDist[solver.mtrand.randInt(max)].var; + if (solver.value(var) != l_Undef + || solver.subsumer->getVarElimed()[var] + || solver.xorSubsumer->getVarElimed()[var] + || solver.partHandler->getSavedState()[var] != l_Undef + ) continue; + + bool OK = true; + for (uint32_t i = 0; i < toTry.size(); i++) { + if (toTry[i] == var) { + OK = false; + break; + } + } + if (OK) { + toTry.push(var); + return; + } + } +} + +void FailedLitSearcher::calcNegPosDist() +{ + uint32_t varPolCount = 0; + for (vector >::iterator it = solver.lTPolCount.begin(), end = solver.lTPolCount.end(); it != end; it++, varPolCount++) { + UIPNegPosDist tmp; + tmp.var = varPolCount; + int64_t pos = it->first; + int64_t neg = it->second; + int64_t diff = std::abs((long int) (pos-neg)); + tmp.dist = pos*pos + neg*neg - diff*diff; + if (it->first > 4 && it->second > 4) + solver.negPosDist.push_back(tmp); + } + std::sort(solver.negPosDist.begin(), solver.negPosDist.end(), NegPosSorter()); +} + +const bool FailedLitSearcher::tryMultiLevelAll() +{ + assert(solver.ok); + uint32_t backupNumUnits = solver.trail.size(); + double myTime = cpuTime(); + uint32_t numTries = 0; + uint32_t finished = 0; + uint64_t beforeProps = solver.propagations; + uint32_t enqueued = 0; + uint32_t numFailed = 0; + + + + if (solver.negPosDist.size() < 30) return true; + + propagated.resize(solver.nVars(), 0); + propagated2.resize(solver.nVars(), 0); + propValue.resize(solver.nVars(), 0); + assert(propagated.isZero()); + assert(propagated2.isZero()); + + vec toTry; + while(solver.propagations < beforeProps + 300*1000*1000) { + toTry.clear(); + for (uint32_t i = 0; i < 3; i++) { + fillToTry(toTry); + } + numTries++; + if (!tryMultiLevel(toTry, enqueued, finished, numFailed)) goto end; + } + + end: + assert(propagated.isZero()); + assert(propagated2.isZero()); + + std::cout + << "c multiLevelBoth tried " << numTries + << " finished: " << finished + << " units: " << (solver.trail.size() - backupNumUnits) + << " enqueued: " << enqueued + << " numFailed: " << numFailed + << " time: " << (cpuTime() - myTime) + << std::endl; + + return solver.ok; +} + +const bool FailedLitSearcher::tryMultiLevel(const vec& vars, uint32_t& enqueued, uint32_t& finished, uint32_t& numFailed) +{ + assert(solver.ok); + + vec toEnqueue; + bool first = true; + bool last = false; + //std::cout << "//////////////////" << std::endl; + for (uint32_t comb = 0; comb < (1U << vars.size()); comb++) { + last = (comb == (1U << vars.size())-1); + solver.newDecisionLevel(); + for (uint32_t i = 0; i < vars.size(); i++) { + solver.uncheckedEnqueueLight(Lit(vars[i], comb&(0x1 << i))); + //std::cout << "lit: " << Lit(vars[i], comb&(1U << i)) << std::endl; + } + //std::cout << "---" << std::endl; + bool failed = !(solver.propagate(false).isNULL()); + if (failed) { + solver.cancelUntilLight(); + if (!first) propagated.setZero(); + numFailed++; + return true; + } + + for (int sublevel = solver.trail.size()-1; sublevel > (int)solver.trail_lim[0]; sublevel--) { + Var x = solver.trail[sublevel].var(); + if (first) { + propagated.setBit(x); + if (solver.assigns[x].getBool()) propValue.setBit(x); + else propValue.clearBit(x); + } else if (last) { + if (propagated[x] && solver.assigns[x].getBool() == propValue[x]) + toEnqueue.push(Lit(x, !propValue[x])); + } else { + if (solver.assigns[x].getBool() == propValue[x]) { + propagated2.setBit(x); + } + } + } + solver.cancelUntilLight(); + if (!first && !last) propagated &= propagated2; + propagated2.setZero(); + if (propagated.isZero()) return true; + first = false; + } + propagated.setZero(); + finished++; + + for (Lit *l = toEnqueue.getData(), *end = toEnqueue.getDataEnd(); l != end; l++) { + enqueued++; + solver.uncheckedEnqueue(*l); + } + solver.ok = solver.propagate().isNULL(); + //exit(-1); + + return solver.ok; +} diff --git a/src/sat/cryptominisat2/FailedLitSearcher.h b/src/sat/cryptominisat2/FailedLitSearcher.h index b092497..2e16ab6 100644 --- a/src/sat/cryptominisat2/FailedLitSearcher.h +++ b/src/sat/cryptominisat2/FailedLitSearcher.h @@ -57,7 +57,7 @@ class FailedLitSearcher { private: //Main const bool tryBoth(const Lit lit1, const Lit lit2); - const bool tryAll(const Lit* begin, const Lit* end); + const bool bothCache(); void printResults(const double myTime) const; Solver& solver; /// propagatedBitSet; BitArray propagated; ///& binPropData; }; + struct BinAddData + { + vector lits; + Lit lit; + }; + struct BinAddDataSorter + { + const bool operator() (const BinAddData& a, const BinAddData& b) const + { + return (a.lits.size() > b.lits.size()); + } + }; uint32_t addedBin; + void hyperBinResAll(const Lit litProp/*, const vector& oldCache*/); void hyperBinResolution(const Lit lit); BitArray unPropagatedBin; BitArray needToVisit; @@ -176,6 +191,12 @@ class FailedLitSearcher { void fillImplies(const Lit lit); vec myImpliesSet; /// > addBinLater; + uint32_t addedCacheBin; //bin-removal within hyper-bin-res vec uselessBin; @@ -190,6 +211,12 @@ class FailedLitSearcher { */ uint64_t maxHyperBinProps; + //Multi-level + void calcNegPosDist(); + const bool tryMultiLevel(const vec& vars, uint32_t& enqueued, uint32_t& finished, uint32_t& numFailed); + const bool tryMultiLevelAll(); + void fillToTry(vec& toTry); + //Temporaries vec tmpPs; diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index 3088a0f..a350177 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -100,7 +100,7 @@ const bool Gaussian::full_init() case propagation: unit_truths += last_trail_size - solver.trail.size(); do_again_gauss = true; - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; break; case nothing: @@ -571,7 +571,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(PropBy& confl, const matrix const bool xorEqualFalse = !m.matrix.getVarsetAt(best_row).is_true(); const bool wasUndef = m.matrix.getVarsetAt(best_row).fill(tmp_clause, solver.assigns, col_to_var_original); - assert(!wasUndef); + release_assert(!wasUndef); #ifdef VERBOSE_DEBUG cout << "(" << matrix_no << ")matrix confl clause:" @@ -640,7 +640,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(PropBy& confl, const matrix #endif uint32_t maxsublevel_at = UINT_MAX; - for (uint32_t i = 0, size = cla.size(); i != size; i++) if (solver.level[cla[i].var()] == (int32_t)curr_dec_level) { + for (uint32_t i = 0, size = cla.size(); i != size; i++) if (solver.level[cla[i].var()] == curr_dec_level) { uint32_t tmp = find_sublevel(cla[i].var()); if (tmp >= maxsublevel) { maxsublevel = tmp; @@ -664,7 +664,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(PropBy& confl, const matrix Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint32_t last_row, PropBy& confl) { - int32_t maxlevel = std::numeric_limits::max(); + uint32_t maxlevel = std::numeric_limits::max(); uint32_t size = UINT_MAX; uint32_t best_row = UINT_MAX; @@ -676,7 +676,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint analyse_confl(m, row, maxlevel, size, best_row); } - if (maxlevel != std::numeric_limits::max()) + if (maxlevel != std::numeric_limits::max()) return handle_matrix_confl(confl, m, size, maxlevel, best_row); #ifdef DEBUG_GAUSS @@ -739,9 +739,6 @@ void Gaussian::cancel_until_sublevel(const uint32_t until_sublevel) cout << "(" << matrix_no << ")Canceling var " << var+1 << endl; #endif - #ifdef USE_OLD_POLARITIES - solver.polarity[var] = solver.oldPolarity[var]; - #endif //USE_OLD_POLARITIES solver.assigns[var] = l_Undef; solver.insertVarOrder(var); } @@ -752,7 +749,7 @@ void Gaussian::cancel_until_sublevel(const uint32_t until_sublevel) #endif } -void Gaussian::analyse_confl(const matrixset& m, const uint32_t row, int32_t& maxlevel, uint32_t& size, uint32_t& best_row) const +void Gaussian::analyse_confl(const matrixset& m, const uint32_t row, uint32_t& maxlevel, uint32_t& size, uint32_t& best_row) const { assert(row < m.num_rows); @@ -770,7 +767,7 @@ void Gaussian::analyse_confl(const matrixset& m, const uint32_t row, int32_t& ma #endif #endif - int32_t this_maxlevel = 0; + uint32_t this_maxlevel = 0; unsigned long int var = 0; uint32_t this_size = 0; while (true) { @@ -792,7 +789,7 @@ void Gaussian::analyse_confl(const matrixset& m, const uint32_t row, int32_t& ma || (this_maxlevel == maxlevel && this_size < size) || (this_size <= 1) )) { - assert(maxlevel != std::numeric_limits::max()); + assert(maxlevel != std::numeric_limits::max()); #ifdef VERBOSE_DEBUG cout << "(" << matrix_no << ")Other found conflict just as good or better."; @@ -836,6 +833,12 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint32_t cout << endl; #endif + #ifdef DEBUG_ATTACH + for (uint32_t i = 0; i < tmp_clause.size(); i++) { + if (i > 0) assert(tmp_clause[i-1].var() != tmp_clause[i].var()); + } + #endif //DEBUG_ATTACH + switch(tmp_clause.size()) { case 0: //This would mean nothing, empty = true, always true in xors @@ -850,8 +853,8 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint32_t tmp_clause[0] = tmp_clause[0].unsign(); tmp_clause[1] = tmp_clause[1].unsign(); XorClause* cl = solver.addXorClauseInt(tmp_clause, xorEqualFalse, 0); - assert(cl == NULL); - assert(solver.ok); + release_assert(cl == NULL); + release_assert(solver.ok); return unit_propagation; break; } diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h index f3c27ea..02feddd 100644 --- a/src/sat/cryptominisat2/Gaussian.h +++ b/src/sat/cryptominisat2/Gaussian.h @@ -138,7 +138,7 @@ protected: //conflict&propagation handling gaussian_ret handle_matrix_prop_and_confl(matrixset& m, uint32_t row, PropBy& confl); - void analyse_confl(const matrixset& m, const uint32_t row, int32_t& maxlevel, uint32_t& size, uint32_t& best_row) const; // analyse conflcit to find the best conflict. Gets & returns the best one in 'maxlevel', 'size' and 'best row' (these are all UINT_MAX when calling this function first, i.e. when there is no other possible conflict to compare to the new in 'row') + void analyse_confl(const matrixset& m, const uint32_t row, uint32_t& maxlevel, uint32_t& size, uint32_t& best_row) const; // analyse conflcit to find the best conflict. Gets & returns the best one in 'maxlevel', 'size' and 'best row' (these are all UINT_MAX when calling this function first, i.e. when there is no other possible conflict to compare to the new in 'row') gaussian_ret handle_matrix_confl(PropBy& confl, const matrixset& m, const uint32_t size, const uint32_t maxlevel, const uint32_t best_row); gaussian_ret handle_matrix_prop(matrixset& m, const uint32_t row); // Handle matrix propagation at row 'row' vec tmp_clause; diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index f76fbb7..0858be5 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -106,7 +106,7 @@ string Logger::cut_name_to_size(const string& name) const ret.resize(len-1); len--; } - + if (len > SND_WIDTH-3) { ret[SND_WIDTH-3] = '\0'; ret[SND_WIDTH-4] = '.'; @@ -121,7 +121,7 @@ void Logger::set_group_name(const uint group, const char* name_tmp) { if (!statistics_on && !proof_graph_on) return; - + string name; if (name_tmp == NULL) return; else name = name_tmp; @@ -156,19 +156,16 @@ string Logger::get_var_name(const Var var) const } // sets the variable's name -void Logger::set_variable_name(const uint var, char* name_tmp) +void Logger::set_variable_name(const uint var, const string& name_tmp) { if (!statistics_on && !proof_graph_on) return; - + new_var(var); - + string name; - if (name_tmp == NULL) - name = ""; - else - name = name_tmp; - + name = name_tmp; + if (varnames[var] == "Noname") { varnames[var] = name; } else if (varnames[var] != name) { @@ -181,7 +178,7 @@ void Logger::first_begin() { if (begin_called) return; - + begin(); } @@ -191,7 +188,7 @@ void Logger::begin() if (proof_graph_on) { std::stringstream filename; filename << "proofs/" << runid << "-proof" << proofStarts++ << "-" << S->starts << ".dot"; - + if (S->starts == 0) history.push_back(uniqueid); else { @@ -217,13 +214,13 @@ void Logger::conflict(const confl_type type, const uint goback_level, const uint { first_begin(); assert(!(proof == NULL && proof_graph_on)); - + const uint goback_sublevel = S->trail_lim[goback_level]; if (proof_graph_on) { uniqueid++; fprintf(proof,"node%d [shape=polygon,sides=5,label=\"",uniqueid); - + if (!mini_proof) { for (uint32_t i = 0; i != learnt_clause.size(); i++) { if (learnt_clause[i].sign()) fprintf(proof,"-"); @@ -242,7 +239,7 @@ void Logger::conflict(const confl_type type, const uint goback_level, const uint else fprintf(proof,"%s\"", groupnames[group].c_str()); fprintf(proof,"];\n"); - + if (!mini_proof) history.resize(goback_sublevel+1); else @@ -254,12 +251,12 @@ void Logger::conflict(const confl_type type, const uint goback_level, const uint times_group_caused_conflict[group]++; depths_of_conflicts_for_group[group].sum += S->decisionLevel(); depths_of_conflicts_for_group[group].num ++; - + no_conflicts++; sum_conflict_depths += S->trail.size() - S->trail_lim[0]; sum_decisions_on_branches += S->decisionLevel(); sum_propagations_on_branches += S->trail.size() - S->trail_lim[0] - S->decisionLevel(); - + if (branch_depth_distrib.size() <= S->decisionLevel()) branch_depth_distrib.resize(S->decisionLevel()+1, 0); branch_depth_distrib[S->decisionLevel()]++; @@ -275,7 +272,7 @@ void Logger::propagation(const Lit lit, Clause* c) { first_begin(); assert(!(proof == NULL && proof_graph_on)); - + uint group; prop_type type; if (c == NULL) { @@ -292,7 +289,7 @@ void Logger::propagation(const Lit lit, Clause* c) //graph if (proof_graph_on && (!mini_proof || type == guess_type)) { uniqueid++; - + fprintf(proof,"node%d [shape=box, label=\"",uniqueid);; if (lit.sign()) fprintf(proof,"-"); @@ -302,16 +299,16 @@ void Logger::propagation(const Lit lit, Clause* c) fprintf(proof,"Var: %d\"];\n",lit.var()); fprintf(proof,"node%d -> node%d [label=\"",history[history.size()-1],uniqueid); - + switch (type) { case simple_propagation_type: fprintf(proof,"%s\"];\n", groupnames[group].c_str()); break; - + case add_clause_type: fprintf(proof,"red. from clause\"];\n"); break; - + case guess_type: fprintf(proof,"guess\",style=bold];\n"); break; @@ -336,7 +333,7 @@ void Logger::propagation(const Lit lit, Clause* c) case guess_type: no_decisions++; times_var_guessed[lit.var()]++; - + depths_of_assigns_for_var[lit.var()].sum += S->decisionLevel(); depths_of_assigns_for_var[lit.var()].num ++; break; @@ -349,7 +346,7 @@ void Logger::end(const finish_type finish) { first_begin(); assert(!(proof == NULL && proof_graph_on)); - + if (proof_graph_on) { uniqueid++; switch (finish) { @@ -377,7 +374,7 @@ void Logger::end(const finish_type finish) if (finish == restarting) reset_statistics(); } - + if (model_found || unsat_model_found) begin_called = false; } @@ -531,7 +528,7 @@ void Logger::print_vars(const vector >& to_print) const uint i = 0; for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) print_line(it->second+1, cut_name_to_size(varnames[it->second]), it->first); - + print_footer(); } @@ -541,7 +538,7 @@ void Logger::print_vars(const vector >& to_print) const for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { print_line(it->second+1, cut_name_to_size(varnames[it->second]), it->first); } - + print_footer(); } @@ -585,7 +582,7 @@ void Logger::print_branch_depth_distrib() const ofstream branch_depth_file; branch_depth_file.open(ss.str().c_str()); i = 0; - + for (map::iterator it = range_stat.begin(); it != range_stat.end(); it++, i++) { std::stringstream ss2; ss2 << it->first*range << " - " << it->first*range + range-1; @@ -610,50 +607,50 @@ void Logger::print_learnt_clause_distrib() const { map learnt_sizes; const vec& learnts = S->get_learnts(); - + uint maximum = 0; - + for (uint i = 0; i < learnts.size(); i++) { uint size = learnts[i]->size(); maximum = std::max(maximum, size); - + map::iterator it = learnt_sizes.find(size); if (it == learnt_sizes.end()) learnt_sizes[size] = 1; else it->second++; } - + learnt_sizes[0] = S->get_unitary_learnts_num(); - + uint slice = (maximum+1)/max_print_lines + (bool)((maximum+1)%max_print_lines); - + print_footer(); print_simple_line(" Learnt clause length distribution"); print_line("Length between", "no. cl."); print_footer(); - + uint until = slice; uint from = 0; while(until < maximum+1) { std::stringstream ss2; ss2 << from << " - " << until-1; - + uint sum = 0; for (; from < until; from++) { map::const_iterator it = learnt_sizes.find(from); if (it != learnt_sizes.end()) sum += it->second; } - + print_line(ss2.str(), sum); - + until += slice; } - + print_footer(); - + print_leearnt_clause_graph_distrib(maximum, learnt_sizes); } @@ -677,16 +674,16 @@ void Logger::print_leearnt_clause_graph_distrib(const uint maximum, const map 0; i--) { cout << "| "; if (height-1-i >= middle && height-1-i-middle < yaxis.size()) @@ -754,7 +751,7 @@ void Logger::printstats() const uint len2 = len + tmp.str().length()%2 + (fullwidth-2)%2; cout << "||" << std::setfill('*') << std::setw(len) << "*" << tmp.str() << std::setw(len2) << "*" << "||" << endl; cout << "+" << std::setfill('=') << std::setw(fullwidth) << "=" << std::setfill(' ') << "+" << endl; - + cout.setf(std::ios_base::left); cout.precision(2); print_statistics_note(); @@ -781,7 +778,7 @@ void Logger::print_matrix_stats() const print_footer(); print_simple_line(" Matrix statistics"); print_footer(); - + uint i = 0; for (vector::const_iterator it = S->gauss_matrixes.begin(), end = S->gauss_matrixes.end(); it != end; it++, i++) { std::stringstream s; @@ -789,20 +786,20 @@ void Logger::print_matrix_stats() const std::stringstream tmp; tmp << std::boolalpha << !(*it)->get_disabled(); print_line(s.str(), tmp.str()); - + s.str(""); s << "Matrix " << i << " called"; print_line(s.str(), (*it)->get_called()); - + s.str(""); s << "Matrix " << i << " propagations"; print_line(s.str(), (*it)->get_useful_prop()); - + s.str(""); s << "Matrix " << i << " conflicts"; print_line(s.str(), (*it)->get_useful_confl()); } - + print_footer(); } #endif //USE_GAUSS @@ -817,18 +814,18 @@ void Logger::print_advanced_stats() const print_line("Avg. branch depth", (double)sum_conflict_depths/(double)no_conflicts); print_line("No. decisions", no_decisions); print_line("No. propagations",no_propagations); - + //printf("no progatations/no decisions (i.e. one decision gives how many propagations on average *for the whole search graph*): %f\n", (double)no_propagations/(double)no_decisions); //printf("no propagations/sum decisions on branches (if you look at one specific branch, what is the average number of propagations you will find?): %f\n", (double)no_propagations/(double)sum_decisions_on_branches); - + print_simple_line("sum decisions on branches/no. branches"); print_simple_line(" (in a given branch, what is the avg."); print_line(" no. of decisions?)",(double)sum_decisions_on_branches/(double)no_conflicts); - + print_simple_line("sum propagations on branches/no. branches"); print_simple_line(" (in a given branch, what is the"); print_line(" avg. no. of propagations?)",(double)sum_propagations_on_branches/(double)no_conflicts); - + print_footer(); } @@ -849,7 +846,7 @@ void Logger::reset_statistics() assert(S->decisionLevel() == 0); assert(times_var_guessed.size() == times_var_propagated.size()); assert(times_group_caused_conflict.size() == times_group_caused_propagation.size()); - + typedef vector::iterator vecit; for (vecit it = times_var_guessed.begin(); it != times_var_guessed.end(); it++) *it = 0; @@ -887,7 +884,7 @@ void Logger::reset_statistics() } for (uint i = 0; i < depths_of_assigns_unit.size(); i++) depths_of_assigns_unit[i] = false; - + for (uint i = 0; i < depths_of_propagations_unit.size(); i++) depths_of_propagations_unit[i] = false; diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h index a7c4dc3..4983f70 100644 --- a/src/sat/cryptominisat2/Logger.h +++ b/src/sat/cryptominisat2/Logger.h @@ -51,7 +51,7 @@ public: sum(0) , num(0) {} - + uint sum; uint num; }; @@ -74,7 +74,7 @@ public: //functions to add/name variables void new_var(const Var var); - void set_variable_name(const uint var, char* name_tmp); + void set_variable_name(const uint var, const std::string& name_tmp); //function to name clause groups void set_group_name(const uint group, const char* name_tmp); @@ -90,11 +90,11 @@ public: bool proof_graph_on; bool mini_proof; bool statistics_on; - + private: void new_group(const uint group); string cut_name_to_size(const string& name) const; - + void print_groups(const vector >& to_print) const; void print_groups(const vector >& to_print) const; void print_vars(const vector >& to_print) const; @@ -120,7 +120,7 @@ private: void print_line(const string& str, const T& num) const; void print_simple_line(const string& str) const; void print_center_line(const string& str) const; - + void print_confl_order() const; void print_prop_order() const; void print_assign_var_order() const; @@ -173,9 +173,9 @@ private: //message display properties const int& verbosity; - + const Solver* S; - + void first_begin(); bool begin_called; uint proofStarts; diff --git a/src/sat/cryptominisat2/MTSolver.cpp b/src/sat/cryptominisat2/MTSolver.cpp new file mode 100644 index 0000000..6bcb06e --- /dev/null +++ b/src/sat/cryptominisat2/MTSolver.cpp @@ -0,0 +1,284 @@ +/*************************************************************************** +CryptoMiniSat -- Copyright (c) 2010 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 "MTSolver.h" + +#include +#include +#include +#include + +#if defined( _WIN32 ) || defined( _WIN64 ) +#include +#endif + +#ifdef _MSC_VER +using namespace std; +#endif + +void MTSolver::printNumThreads() const +{ + if (conf.verbosity >= 1) { + std::cout << "c Using " << numThreads << " thread(s)" << std::endl; + } +} + +MTSolver::MTSolver(const int _numThreads, const SolverConf& _conf, const GaussConf& _gaussConfig) : + conf(_conf) + , gaussConfig(_gaussConfig) + , numThreads(_numThreads) +{ + solvers.resize(numThreads, NULL); + + for (int i = 0; i < numThreads; i++) { + setupOneSolver(i); + } + finishedThread = 0; +} + +MTSolver::~MTSolver() +{ + for (uint32_t i = 0; i < solvers.size(); i++) { + delete solvers[i]; + } +} + +void MTSolver::setupOneSolver(const int num) +{ + SolverConf myConf = conf; + myConf.origSeed = num; + if (num > 0) { + if (num % 6 == 0) myConf.fixRestartType = dynamic_restart; + else if (num % 6 == 4) myConf.fixRestartType = static_restart; + #ifdef _MSC_VER + myConf.simpBurstSConf *= 1.0f + max(0.2f*(float)num, 2.0f); + myConf.simpStartMult *= 1.0f - max(0.1f*(float)num, 0.7f); + myConf.simpStartMMult *= 1.0f - max(0.1f*(float)num, 0.7f); + #else + myConf.simpBurstSConf *= 1.0f + std::max(0.2f*(float)num, 2.0f); + myConf.simpStartMult *= 1.0f - std::max(0.1f*(float)num, 0.7f); + myConf.simpStartMMult *= 1.0f - std::max(0.1f*(float)num, 0.7f); + #endif //_MSC_VER + + if (num % 6 == 5) { + myConf.doVarElim = false; + myConf.polarity_mode = polarity_false; + } + } + if (num != 0) myConf.verbosity = 0; + + Solver* solver = new Solver(myConf, gaussConfig, &sharedData); + solvers[num] = solver; +} + + + +const lbool MTSolver::solve(const vec& assumps) +{ + std::set finished; + lbool retVal; + + omp_set_num_threads(numThreads); + int numThreadsLocal; + #pragma omp parallel + { + #pragma omp single + numThreadsLocal = omp_get_num_threads(); + + int threadNum = omp_get_thread_num(); + vec assumpsLocal(assumps); + lbool ret = solvers[threadNum]->solve(assumpsLocal, numThreadsLocal, threadNum); + + #pragma omp critical (finished) + { + finished.insert(threadNum); + } + + #pragma omp single + { + int numNeededInterrupt = 0; + for(int i = 0; i < numThreadsLocal; i++) { + if (i != threadNum) { + solvers[i]->setNeedToInterrupt(); + numNeededInterrupt++; + } + #pragma omp flush //flush needToInterrupt on other threads + } + assert(numNeededInterrupt == numThreadsLocal-1); + + bool mustWait = true; + while (mustWait) { + #pragma omp critical (finished) + if (finished.size() == (unsigned)numThreadsLocal) mustWait = false; + + #if defined( _WIN32 ) || defined( _WIN64 ) + Sleep(1); + #else + timespec req, rem; + req.tv_nsec = 10000000; + req.tv_sec = 0; + nanosleep(&req, &rem); + #endif + } + + //Sync ER-ed vars + if (ret != l_False) { + //Finish the adding of currently selected thread + //May Sync a bit, but maybe not all(!!) + for (int i = 0; i < numThreadsLocal; i++) { + solvers[i]->finishAddingVars(); + solvers[i]->syncData(); + } + //Sync all + for (int i = 0; i < numThreadsLocal; i++) { + solvers[i]->syncData(); + } + } + + finishedThread = threadNum; + retVal = ret; + setUpFinish(retVal, threadNum); + } + } + + if (numThreads != numThreadsLocal) { + for (int i = numThreadsLocal; i < numThreads; i++) { + delete solvers[i]; + } + numThreads = numThreadsLocal; + solvers.resize(numThreads); + } + + for(int i = 0; i < numThreads; i++) { + solvers[i]->setNeedToInterrupt(false); + } + + return retVal; +} + +void MTSolver::setUpFinish(const lbool retVal, const int threadNum) +{ + Solver& solver = *solvers[threadNum]; + model.clear(); + if (retVal == l_True) { + model.growTo(solver.model.size()); + std::copy(solver.model.getData(), solver.model.getDataEnd(), model.getData()); + } + + conflict.clear(); + if (retVal == l_False) { + conflict.growTo(solver.conflict.size()); + std::copy(solver.conflict.getData(), solver.conflict.getDataEnd(), conflict.getData()); + } +} + +Var MTSolver::newVar(bool dvar) +{ + uint32_t ret = 0; + for (uint32_t i = 0; i < solvers.size(); i++) { + ret = solvers[i]->newVar(dvar); + } + + return ret; +} + +template bool MTSolver::addClause (T& ps, const uint32_t group, const char* group_name) +{ + bool globalRet = true; + for (uint32_t i = 0; i < solvers.size(); i++) { + vec copyPS(ps.size()); + std::copy(ps.getData(), ps.getDataEnd(), copyPS.getData()); + bool ret = solvers[i]->addClause(copyPS, group, group_name); + if (ret == false) { + #pragma omp critical + globalRet = false; + } + } + + return globalRet; +} +template bool MTSolver::addClause(vec& ps, const uint32_t group, const char* group_name); +template bool MTSolver::addClause(Clause& ps, const uint32_t group, const char* group_name); + +template bool MTSolver::addLearntClause(T& ps, const uint32_t group, const char* group_name, const uint32_t glue) +{ + bool globalRet = true; + for (uint32_t i = 0; i < solvers.size(); i++) { + vec copyPS(ps.size()); + std::copy(ps.getData(), ps.getDataEnd(), copyPS.getData()); + bool ret = solvers[i]->addLearntClause(copyPS, group, group_name, glue); + if (ret == false) { + #pragma omp critical + globalRet = false; + } + } + + return globalRet; +} +template bool MTSolver::addLearntClause(vec& ps, const uint32_t group, const char* group_name, const uint32_t glue); +template bool MTSolver::addLearntClause(Clause& ps, const uint32_t group, const char* group_name, const uint32_t glue); + +template bool MTSolver::addXorClause (T& ps, bool xorEqualFalse, const uint32_t group, const char* group_name) +{ + bool globalRet = true; + for (uint32_t i = 0; i < solvers.size(); i++) { + vec copyPS(ps.size()); + std::copy(ps.getData(), ps.getDataEnd(), copyPS.getData()); + bool ret = solvers[i]->addXorClause(copyPS, xorEqualFalse, group, group_name); + if (ret == false) { + globalRet = false; + } + } + + return globalRet; +} +template bool MTSolver::addXorClause(vec& ps, bool xorEqualFalse, const uint32_t group, const char* group_name); +template bool MTSolver::addXorClause(XorClause& ps, bool xorEqualFalse, const uint32_t group, const char* group_name); + + +void MTSolver::printStats() +{ + Solver& solver = *solvers[finishedThread]; + solver.printStats(numThreads); +} + +void MTSolver::setNeedToInterrupt() +{ + for (uint32_t i = 0; i < solvers.size(); i++) { + solvers[i]->setNeedToInterrupt(); + } +} + +void MTSolver::dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize) +{ + solvers[finishedThread]->dumpSortedLearnts(fileName, maxSize); +} + +void MTSolver::dumpOrigClauses(const std::string& fileName) const +{ + solvers[finishedThread]->dumpOrigClauses(fileName); +} + +void MTSolver::setVariableName(const Var var, const std::string& name) +{ + for (uint32_t i = 0; i < solvers.size(); i++) { + solvers[i]->setVariableName(var, name); + } +} + +//void needLibraryCNFFile(const std::string& fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file. + diff --git a/src/sat/cryptominisat2/MTSolver.h b/src/sat/cryptominisat2/MTSolver.h new file mode 100644 index 0000000..370397b --- /dev/null +++ b/src/sat/cryptominisat2/MTSolver.h @@ -0,0 +1,242 @@ +/*************************************************************************** +CryptoMiniSat -- Copyright (c) 2010 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 "Solver.h" +#include "SharedData.h" +#include + +class MTSolver +{ +public: + MTSolver(const int numThreads, const SolverConf& conf = SolverConf(), const GaussConf& _gaussConfig = GaussConf()); + ~MTSolver(); + + Var newVar (bool dvar = true); // Add a new variable with parameters specifying variable mode. + template + bool addClause (T& ps, const uint32_t group = 0, const char* group_name = NULL); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + template + bool addLearntClause(T& ps, const uint32_t group = 0, const char* group_name = NULL, const uint32_t glue = 10); + template + bool addXorClause (T& ps, bool xorEqualFalse, const uint32_t group = 0, const char* group_name = NULL); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! + + // Solving: + // + const lbool solve (const vec& assumps); /// model; /// conflict; ///& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses + const vec& get_learnts() const; //Get all learnt clauses that are >1 long + const vector get_unitary_learnts() const; //return the set of unitary learnt clauses + const uint32_t get_unitary_learnts_num() const; //return the number of unitary learnt clauses + void dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize); // Dumps all learnt clauses (including unitary ones) into the file + void needLibraryCNFFile(const std::string& fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file. + void dumpOrigClauses(const std::string& fileNam) const; + + #ifdef USE_GAUSS + const uint32_t get_sum_gauss_called() const; + const uint32_t get_sum_gauss_confl() const; + const uint32_t get_sum_gauss_prop() const; + const uint32_t get_sum_gauss_unit_truths() const; + #endif //USE_GAUSS + + //Printing statistics + void printStats(); + const uint32_t getNumElimSubsume() const; /// solvers; + SharedData sharedData; + int finishedThread; +}; + +inline const uint32_t MTSolver::nVars() const +{ + return solvers[0]->nVars(); +} + +inline const uint32_t MTSolver::getVerbosity() const +{ + return conf.verbosity; +} + +inline const bool MTSolver::getNeedToDumpLearnts() const +{ + return conf.needToDumpLearnts; +} + +inline const bool MTSolver::getNeedToDumpOrig() const +{ + return conf.needToDumpOrig; +} + +#ifdef USE_GAUSS +inline const uint32_t MTSolver::get_sum_gauss_called() const +{ + return solvers[finishedThread]->get_sum_gauss_called(); +} + +inline const uint32_t MTSolver::get_sum_gauss_confl() const +{ + return solvers[finishedThread]->get_sum_gauss_confl(); +} + +inline const uint32_t MTSolver::get_sum_gauss_prop() const +{ + return solvers[finishedThread]->get_sum_gauss_prop(); +} + +inline const uint32_t MTSolver::get_sum_gauss_unit_truths() const +{ + return solvers[finishedThread]->get_sum_gauss_unit_truths(); +} + +#endif //USE_GAUSS + + +inline const lbool MTSolver::modelValue (const Lit p) const +{ + return solvers[finishedThread]->modelValue(p); +} + +inline const uint32_t MTSolver::nAssigns() const +{ + return solvers[finishedThread]->nAssigns(); +} + +inline const uint32_t MTSolver::nClauses() const +{ + return solvers[finishedThread]->nClauses(); +} + +inline const uint32_t MTSolver::nLiterals() const +{ + return solvers[finishedThread]->nLiterals(); +} + +inline const uint32_t MTSolver::nLearnts() const +{ + return solvers[finishedThread]->nLearnts(); +} + +inline const bool MTSolver::okay() const +{ + return solvers[finishedThread]->okay(); +} + +inline const lbool MTSolver::solve() +{ + vec tmp; + return solve(tmp); +} + +inline const uint32_t MTSolver::getNumElimSubsume() const +{ + return solvers[finishedThread]->getNumElimSubsume(); +} + +inline const uint32_t MTSolver::getNumElimXorSubsume() const +{ + return solvers[finishedThread]->getNumElimXorSubsume(); +} + +inline const uint32_t MTSolver::getNumXorTrees() const +{ + return solvers[finishedThread]->getNumXorTrees(); +} + +inline const uint32_t MTSolver::getNumXorTreesCrownSize() const +{ + return solvers[finishedThread]->getNumXorTreesCrownSize(); +} + +inline const double MTSolver::getTotalTimeSubsumer() const +{ + return solvers[finishedThread]->getTotalTimeSubsumer(); +} + +inline const double MTSolver::getTotalTimeFailedLitSearcher() const +{ + return solvers[finishedThread]->getTotalTimeFailedLitSearcher(); +} + +inline const double MTSolver::getTotalTimeSCC() const +{ + return solvers[finishedThread]->getTotalTimeSCC(); +} + +inline const double MTSolver::getTotalTimeXorSubsumer() const +{ + return solvers[finishedThread]->getTotalTimeXorSubsumer(); +} diff --git a/src/sat/cryptominisat2/Main.cpp b/src/sat/cryptominisat2/Main.cpp index 7433cae..d50bb29 100644 --- a/src/sat/cryptominisat2/Main.cpp +++ b/src/sat/cryptominisat2/Main.cpp @@ -37,7 +37,6 @@ Here is a picture of of the above process in more detail: #include #include #include -#include #ifdef _MSC_VER #include #else @@ -76,7 +75,7 @@ Main::Main(int _argc, char** _argv) : { } -std::map solversToInterrupt; +MTSolver* solversToInterrupt; std::set finished; /** @@ -89,25 +88,22 @@ is used to achieve this */ void SIGINT_handler(int signum) { - #pragma omp critical - { - Solver& solver = *solversToInterrupt.begin()->second; - printf("\n"); - std::cerr << "*** INTERRUPTED ***" << std::endl; - if (solver.conf.needToDumpLearnts || solver.conf.needToDumpOrig) { - solver.needToInterrupt = true; - std::cerr << "*** Please wait. We need to interrupt cleanly" << std::endl; - std::cerr << "*** This means we might need to finish some calculations" << std::endl; - } else { - if (solver.conf.verbosity >= 1) solver.printStats(); - exit(1); - } + MTSolver& solver = *solversToInterrupt; + printf("\n"); + std::cerr << "*** INTERRUPTED ***" << std::endl; + if (solver.getNeedToDumpLearnts() || solver.getNeedToDumpOrig()) { + solver.setNeedToInterrupt(); + std::cerr << "*** Please wait. We need to interrupt cleanly" << std::endl; + std::cerr << "*** This means we might need to finish some calculations" << std::endl; + } else { + if (solver.getVerbosity() >= 1) solver.printStats(); + exit(1); } } -void Main::readInAFile(const std::string& filename, Solver& solver) +void Main::readInAFile(const std::string& filename, MTSolver& solver) { - if (solver.conf.verbosity >= 1) { + if (conf.verbosity >= 1) { std::cout << "c Reading file '" << filename << "'" << std::endl; } @@ -137,9 +133,9 @@ void Main::readInAFile(const std::string& filename, Solver& solver) #endif // DISABLE_ZLIB } -void Main::readInStandardInput(Solver& solver) +void Main::readInStandardInput(MTSolver& solver) { - if (solver.conf.verbosity >= 1) { + if (solver.getVerbosity()) { std::cout << "c Reading from standard input... Use '-h' or '--help' for help." << std::endl; } #ifdef DISABLE_ZLIB @@ -163,7 +159,7 @@ void Main::readInStandardInput(Solver& solver) -void Main::parseInAllFiles(Solver& solver) +void Main::parseInAllFiles(MTSolver& solver) { double myTime = cpuTime(); @@ -184,7 +180,7 @@ void Main::parseInAllFiles(Solver& solver) readInAFile(filename, solver); } - if (solver.conf.verbosity >= 1) { + if (conf.verbosity >= 1) { std::cout << "c Parsing time: " << std::fixed << std::setw(5) << std::setprecision(2) << (cpuTime() - myTime) << " s" << std::endl; @@ -311,6 +307,9 @@ void Main::printUsage(char** argv) printf(" --maxglue = [0 - 2^%d-1] default: %d. Glue value above which we\n", MAX_GLUE_BITS, conf.maxGlue); printf(" throw the clause away on backtrack.\n"); printf(" --threads = Num threads (default is 1)\n"); + printf(" --nogatefind = Don't find gates&do ER\n"); + printf(" --noer = Don't do ER\n"); + printf(" --noalwaysfmin = Don't always try to further minimise -- only sometimes\n"); printf("\n"); } @@ -324,7 +323,7 @@ const char* Main::hasPrefix(const char* str, const char* prefix) return NULL; } -void Main::printResultFunc(const Solver& S, const lbool ret, FILE* res) +void Main::printResultFunc(const MTSolver& S, const lbool ret, FILE* res) { if (res != NULL) { if (ret == l_True) { @@ -602,6 +601,12 @@ void Main::parseCommandLine() conf.doCacheOTFSSR = false; } else if ((value = hasPrefix(argv[i], "--noremlbins"))) { conf.doRemUselessLBins = false; + } else if ((value = hasPrefix(argv[i], "--nogatefind"))) { + conf.doGateFind = false; + } else if ((value = hasPrefix(argv[i], "--noer"))) { + conf.doER = false; + } else if ((value = hasPrefix(argv[i], "--noalwaysfmin"))) { + conf.doAlwaysFMinim = false; } else if ((value = hasPrefix(argv[i], "--maxglue="))) { int glue = 0; if (sscanf(value, "%d", &glue) < 0 || glue < 2) { @@ -710,12 +715,13 @@ void Main::printVersionInfo(const uint32_t verbosity) } } -const int Main::singleThreadSolve() +const int Main::solve() { - Solver solver(conf, gaussconfig); - solversToInterrupt[0] = &solver; + MTSolver solver(numThreads, conf, gaussconfig); + solversToInterrupt = &solver; printVersionInfo(conf.verbosity); + solver.printNumThreads(); setDoublePrecision(conf.verbosity); parseInAllFiles(solver); @@ -776,130 +782,6 @@ int Main::correctReturnValue(const lbool ret) const return retval; } -const int Main::oneThreadSolve() -{ - int numThreads = omp_get_num_threads(); - SolverConf myConf = conf; - int num = omp_get_thread_num(); - myConf.origSeed = num; - if (num > 0) { - if (num % 4 == 3) myConf.fixRestartType = dynamic_restart; - if (num % 4 == 2) myConf.doCalcReach = false; - //else myConf.fixRestartType = static_restart; - myConf.simpBurstSConf *= 1 + num; - myConf.simpStartMult *= 1.0 + 0.2*(double)num; - myConf.simpStartMMult *= 1.0 + 0.2*(double)num; - if (num == numThreads-1) { - //myConf.doVarElim = false; - myConf.doPerformPreSimp = false; - myConf.polarity_mode = polarity_false; - } - } - if (num != 0) myConf.verbosity = 0; - - Solver solver(myConf, gaussconfig, &sharedData); - #pragma omp critical (solversToInterr) - { - solversToInterrupt[num] = &solver; - //std::cout << "Solver num " << num << " is to be interrupted " << std::endl; - } - - printVersionInfo(myConf.verbosity); - setDoublePrecision(myConf.verbosity); - - parseInAllFiles(solver); - lbool ret = solver.solve(); - #pragma omp critical (finished) - { - finished.insert(num); - } - - int retval = 0; - #pragma omp single - { - int numNeededInterrupt = 0; - while(numNeededInterrupt != numThreads-1) { - #pragma omp critical (solversToInterr) - { - for(int i = 0; i < numThreads; i++) { - if (i != num - && solversToInterrupt.find(i) != solversToInterrupt.end() - && solversToInterrupt[i]->needToInterrupt == false - ) { - solversToInterrupt[i]->needToInterrupt = true; - numNeededInterrupt++; - } - } - } - } - bool mustWait = true; - while (mustWait) { - #pragma omp critical (finished) - if (finished.size() == (unsigned)numThreads) mustWait = false; - } - if (conf.needToDumpLearnts) { - solver.dumpSortedLearnts(conf.learntsFilename, conf.maxDumpLearntsSize); - if (conf.verbosity >= 1) { - std::cout << "c Sorted learnt clauses dumped to file '" - << conf.learntsFilename << "'" << std::endl; - } - } - if (conf.needToDumpOrig) { - solver.dumpOrigClauses(conf.origFilename); - if (conf.verbosity >= 1) - std::cout << "c Simplified original clauses dumped to file '" - << conf.origFilename << "'" << std::endl; - } - - FILE* res = openOutputFile(); - if (conf.verbosity >= 1) solver.printStats(); - printResultFunc(solver, ret, res); - - retval = correctReturnValue(ret); - exit(retval); - } - return retval; -} - -const int Main::multiThreadSolve() -{ - bool exitHere = false; - if (max_nr_of_solutions > 1) { - std::cerr << "ERROR: When multi-threading, only one solution can be found" << std::endl; - exitHere = true; - } - if (debugLib) { - std::cerr << "ERROR: When multi-threading, --debuglib cannot be used" << std::endl; - exitHere = true; - } - if (exitHere) { - std::cerr << "libarary in this version of CryptoMS is not multi-threaded :(" << std::endl; - std::cerr << "Please set option '--threads=1' on the command line." << std::endl; - exit(-1); - } - - int finalRetVal; - if (numThreads != -1) { - assert(numThreads > 0); - omp_set_num_threads(numThreads); - } - #pragma omp parallel - { - #pragma omp single - { - if (conf.verbosity >= 1) - std::cout << "c Using " << omp_get_num_threads() - << " threads" << std::endl; - } - int retval = oneThreadSolve(); - - #pragma omp single - finalRetVal = retval; - } - - return finalRetVal; -} - int main(int argc, char** argv) { Main main(argc, argv); @@ -907,8 +789,5 @@ int main(int argc, char** argv) signal(SIGINT, SIGINT_handler); //signal(SIGHUP,SIGINT_handler); - if (main.numThreads == 1) - return main.singleThreadSolve(); - else - return main.multiThreadSolve(); + return main.solve(); } diff --git a/src/sat/cryptominisat2/Main.h b/src/sat/cryptominisat2/Main.h index f3d56a7..d21c88b 100644 --- a/src/sat/cryptominisat2/Main.h +++ b/src/sat/cryptominisat2/Main.h @@ -16,7 +16,7 @@ using std::string; #include #endif // DISABLE_ZLIB -#include "Solver.h" +#include "MTSolver.h" #include "SharedData.h" class Main @@ -26,22 +26,18 @@ class Main void parseCommandLine(); - const int singleThreadSolve(); - const int oneThreadSolve(); - const int multiThreadSolve(); - - int numThreads; + const int solve(); private: void printUsage(char** argv); const char* hasPrefix(const char* str, const char* prefix); - void printResultFunc(const Solver& S, const lbool ret, FILE* res); + void printResultFunc(const MTSolver& S, const lbool ret, FILE* res); //File reading - void readInAFile(const std::string& filename, Solver& solver); - void readInStandardInput(Solver& solver); - void parseInAllFiles(Solver& solver); + void readInAFile(const std::string& filename, MTSolver& solver); + void readInStandardInput(MTSolver& solver); + void parseInAllFiles(MTSolver& solver); FILE* openOutputFile(); void setDoublePrecision(const uint32_t verbosity); @@ -50,6 +46,7 @@ class Main SolverConf conf; GaussConf gaussconfig; + int numThreads; bool grouping; bool debugLib; @@ -60,8 +57,6 @@ class Main bool twoFileNamesPresent; std::vector filesToRead; - SharedData sharedData; - int argc; char** argv; }; diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index 30a3a66..77e88f2 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -15,7 +15,7 @@ SOURCES = Logger.cpp Solver.cpp PackedRow.cpp \ CompleteDetachReattacher.cpp \ ClauseVivifier.cpp SolverMisc.cpp \ DimacsParser.cpp SolverDebug.cpp \ - SCCFinder.cpp + SCCFinder.cpp BothCache.cpp OBJECTS = $(SOURCES:.cpp=.o) LIB = libminisat.a CFLAGS += -I../.. -I$(MTL) -I$(MTRAND) -DDISABLE_ZLIB -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c diff --git a/src/sat/cryptominisat2/PartFinder.cpp b/src/sat/cryptominisat2/PartFinder.cpp index 325b5ec..b39e9bc 100644 --- a/src/sat/cryptominisat2/PartFinder.cpp +++ b/src/sat/cryptominisat2/PartFinder.cpp @@ -64,10 +64,13 @@ const bool PartFinder::findParts() if (!solver.ok) return false; } + removeVarsOnlyInLearnts(); addToPart(solver.clauses); addToPartBins(); addToPart(solver.xorclauses); + //checkLearntBinAdded(); + const uint32_t parts = setParts(); #ifndef NDEBUG @@ -88,6 +91,117 @@ const bool PartFinder::findParts() return true; } +void PartFinder::checkLearntBinAdded() +{ + uint32_t wsLit = 0; + for (vec *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) { + Lit lit = ~Lit::toLit(wsLit); + vec& ws = *it; + Watched* i = ws.getData(); + for (const Watched *end2 = ws.getDataEnd(); i != end2; i++) { + if (i->isBinary() && i->getLearnt()) { + if (table[lit.var()] == std::numeric_limits::max() + || table[i->getOtherLit().var()] == std::numeric_limits::max() + ) { + std::cout << " max: " << lit << " , " << i->getOtherLit() << std::endl; + } + } + } + } +} + +void PartFinder::removeVarsOnlyInLearnts() +{ + vec usedVar(solver.nVars(), false); + + addClausesToUsed(solver.clauses, usedVar); + addClausesToUsed(solver.xorclauses, usedVar); + addBinsToUsed(usedVar); + + removeLearntClausesNotInVars(usedVar); + removeBinClausesNotInVars(usedVar); +} + +void PartFinder::removeLearntClausesNotInVars(vec& usedVar) +{ + Clause** i = solver.learnts.getData(); + Clause** j = i; + for (Clause **end = solver.learnts.getDataEnd(); i != end; i++) { + Clause& cl = **i; + assert(cl.learnt()); + + bool removeIt = false; + for (Lit *l = cl.getData(), *end2 = cl.getDataEnd(); l != end2; l++) { + if (!usedVar[l->var()]) { + removeIt = true; + break; + } + } + + if (removeIt) { + solver.detachClause(cl); + solver.clauseAllocator.clauseFree(&cl); + } else { + *j++ = *i; + } + } + solver.learnts.shrink_(i-j); +} + +void PartFinder::removeBinClausesNotInVars(vec& usedVar) +{ + uint64_t removedHalfLearnt = 0; + + uint32_t wsLit = 0; + for (vec *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) { + Lit lit = ~Lit::toLit(wsLit); + vec& ws = *it; + Watched* i = ws.getData(); + Watched* j = i; + for (const Watched *end2 = ws.getDataEnd(); i != end2; i++) { + if (i->isBinary() && i->getLearnt()) { + if (usedVar[lit.var()] && usedVar[i->getOtherLit().var()]) + *j++ = *i; + else + removedHalfLearnt++; + } else { + *j++ = *i; + } + } + ws.shrink_(i-j); + } + + solver.learnts_literals -= removedHalfLearnt; + solver.numBins -= removedHalfLearnt/2; +} + +template +void PartFinder::addClausesToUsed(const vec& cs, vec& usedVar) +{ + for (T *const*c = cs.getData(), *const*end = cs.getDataEnd(); c != end; c++) { + const T& cl = **c; + if (cl.learnt()) continue; + + for (const Lit *l = cl.getData(), *end2 = cl.getDataEnd(); l != end2; l++) + usedVar[l->var()] = true; + } +} + +void PartFinder::addBinsToUsed(vec& usedVar) +{ + uint32_t wsLit = 0; + for (const vec *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) { + Lit lit = ~Lit::toLit(wsLit); + const vec& ws = *it; + for (const Watched *it2 = ws.getData(), *end2 = ws.getDataEnd(); it2 != end2; it2++) { + if (it2->isBinary() && lit < it2->getOtherLit() && !it2->getLearnt()) { + usedVar[lit.var()] = true; + usedVar[it2->getOtherLit().var()] = true; + } + } + } +} + template void PartFinder::addToPart(const vec& cs) { @@ -106,8 +220,7 @@ void PartFinder::addToPartBins() lits[0] = lit; const vec& ws = *it; for (const Watched *it2 = ws.getData(), *end2 = ws.getDataEnd(); it2 != end2; it2++) { - if (it2->isBinary() && lit.toInt() < it2->getOtherLit().toInt()) { - if (it2->getLearnt()) continue; + if (it2->isBinary() && lit < it2->getOtherLit() && !it2->getLearnt()) { lits[1] = it2->getOtherLit(); addToPartClause(lits); } @@ -116,7 +229,7 @@ void PartFinder::addToPartBins() } template -void PartFinder::addToPartClause(T& cl) +void PartFinder::addToPartClause(const T& cl) { set tomerge; vector newSet; diff --git a/src/sat/cryptominisat2/PartFinder.h b/src/sat/cryptominisat2/PartFinder.h index 27a7921..643615f 100644 --- a/src/sat/cryptominisat2/PartFinder.h +++ b/src/sat/cryptominisat2/PartFinder.h @@ -46,9 +46,18 @@ class PartFinder { const vector& getPartVars(const uint32_t part); private: + //removing learnt clauses that contain vars that are no longer in any clauses + void removeVarsOnlyInLearnts(); + template + void addClausesToUsed(const vec& cs, vec& usedVar); + void addBinsToUsed(vec& usedVar); + void removeLearntClausesNotInVars(vec& usedVar); + void removeBinClausesNotInVars(vec& usedVar); + void checkLearntBinAdded(); + const uint32_t setParts(); void addToPartBins(); - template void addToPartClause(T& cl); + template void addToPartClause(const T& cl); template void addToPart(const vec& cs); struct mysorter @@ -83,6 +92,7 @@ inline const vector& PartFinder::getTable() const inline const uint32_t PartFinder::getVarPart(const Var var) const { + if (var >= table.size()) return false; return table[var]; } diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp index 0bba710..cff31d4 100644 --- a/src/sat/cryptominisat2/PartHandler.cpp +++ b/src/sat/cryptominisat2/PartHandler.cpp @@ -68,8 +68,8 @@ const bool PartHandler::handle() moveBinClauses(newSolver, part, partFinder); moveClauses(solver.clauses, newSolver, part, partFinder); - moveClauses(solver.xorclauses, newSolver, part, partFinder); - moveLearntClauses(solver.learnts, newSolver, part, partFinder); + moveClauses(solver.learnts, newSolver, part, partFinder); + moveXorClauses(solver.xorclauses, newSolver, part, partFinder); assert(checkClauseMovement(newSolver, part, partFinder)); lbool status = newSolver.solve(); @@ -84,6 +84,9 @@ const bool PartHandler::handle() //Check that the newly found solution is really unassigned in the //original solver for (Var var = 0; var < newSolver.nVars(); var++) { + //Check for vars added through extended resolution + if (partFinder.getVarPart(var) != part) continue; + if (newSolver.model[var] != l_Undef) { assert(solver.assigns[var] == l_Undef); } @@ -91,12 +94,18 @@ const bool PartHandler::handle() assert(newSolver.decisionLevel() == 0); for (uint32_t i = 0; i < newSolver.trail.size(); i++) { + //Check for vars added through extended resolution + if (partFinder.getVarPart(newSolver.trail[i].var()) != part) continue; + solver.uncheckedEnqueue(newSolver.trail[i]); } - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); assert(solver.ok); for (Var var = 0; var < newSolver.nVars(); var++) { + //Check for vars added through extended resolution + if (partFinder.getVarPart(var) != part) continue; + if (newSolver.model[var] != l_Undef) { //Must have been decision var in the old solver!?? //assert(std::find(decisionVarRemoved.getData(), decisionVarRemoved.getDataEnd(), var) != decisionVarRemoved.getDataEnd()); @@ -153,11 +162,12 @@ void PartHandler::configureNewSolver(Solver& newSolver) const newSolver.gaussconfig = solver.gaussconfig; //Memory-usage reduction - newSolver.conf.doSchedSimp = false; - newSolver.conf.doSatELite = false; - newSolver.conf.doXorSubsumption = false; + //newSolver.conf.doSchedSimp = false; + //newSolver.conf.doSatELite = false; + //newSolver.conf.doXorSubsumption = false; newSolver.conf.doPartHandler = false; - newSolver.conf.doSubsWNonExistBins = false; + newSolver.conf.libraryUsage = true; + //newSolver.conf.doSubsWNonExistBins = false; } /** @@ -244,7 +254,12 @@ const bool PartHandler::checkOnlyThisPartBin(const Solver& thisSolver, const uin if (partFinder.getVarPart(lit.var()) != part || partFinder.getVarPart(it2->getOtherLit().var()) != part ) { - std::cout << "bin incorrectly moved to this part:" << lit << " , " << it2->getOtherLit() << std::endl; + std::cout << "bin incorrectly moved to this part:" << lit << " , " << it2->getOtherLit() + << ", learnt: "<< it2->getLearnt() << std::endl; + std::cout << "this part: " << part + << ", lit1 " << lit << " part : " << partFinder.getVarPart(lit.var()) + << ", lit2 " << it2->getOtherLit() << " part : " << partFinder.getVarPart(it2->getOtherLit().var()) + << std::endl; retval = false; } } @@ -303,7 +318,8 @@ void PartHandler::moveClauses(vec& cs, Solver& newSolver, const uint32_ std::copy(c.getData(), c.getDataEnd(), tmp.getData()); newSolver.addClause(tmp, c.getGroup()); //NOTE: we need the tmp because otherwise, the addClause could have changed "c", which we need to re-add later! - clausesRemoved.push(*i); + if (!c.learnt()) clausesRemoved.push(*i); + else solver.clauseAllocator.clauseFree(*i); } cs.shrink(i-j); } @@ -345,10 +361,10 @@ void PartHandler::moveBinClauses(Solver& newSolver, const uint32_t part, PartFin assert(partFinder.getVarPart(lit2.var()) == part); if (i->getLearnt()) { newSolver.addLearntClause(lits); - binClausesRemoved.push_back(std::make_pair(lit, lit2)); numRemovedHalfLearnt++; } else { newSolver.addClause(lits); + binClausesRemoved.push_back(std::make_pair(lit, lit2)); numRemovedHalfNonLearnt++; } } else { @@ -373,7 +389,7 @@ void PartHandler::moveBinClauses(Solver& newSolver, const uint32_t part, PartFin The variables that form part of the part will determine if the clause is in the part or not */ -void PartHandler::moveClauses(vec& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder) +void PartHandler::moveXorClauses(vec& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder) { XorClause **i, **j, **end; for (i = j = cs.getData(), end = i + cs.size(); i != end; i++) { @@ -396,60 +412,6 @@ void PartHandler::moveClauses(vec& cs, Solver& newSolver, const uint cs.shrink(i-j); } -/** -@brief Move learnt clauses from original to the part - -The variables that form part of the part will determine if the clause is in the -part or not. - -Note that learnt clauses might be in both the orignal and the sub-part. In this -case, the learnt clause is deleted, since it unneccesarily connects two -components that otherwise would be distinct -*/ -void PartHandler::moveLearntClauses(vec& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder) -{ - Clause **i, **j, **end; - for (i = j = cs.getData(), end = i + cs.size() ; i != end; i++) { - if (!(**i).learnt()) { - *j++ = *i; - continue; - } - - Clause& c = **i; - assert(c.size() > 0); - uint32_t clause_part = partFinder.getVarPart(c[0].var()); - bool removed = false; - for (const Lit* l = c.getData(), *end = l + c.size(); l != end; l++) { - if (partFinder.getVarPart(l->var()) != clause_part) { - #ifdef VERBOSE_DEBUG - std::cout << "Learnt clause in both parts:"; c.plainPrint(); - #endif - - removed = true; - solver.removeClause(c); - break; - } - } - if (removed) continue; - if (clause_part == part) { - #ifdef VERBOSE_DEBUG - //std::cout << "Learnt clause in this part:"; c.plainPrint(); - #endif - - solver.detachClause(c); - newSolver.addLearntClause(c, c.getGroup(), NULL, c.getGlue(), c.getMiniSatAct()); - solver.clauseAllocator.clauseFree(&c); - } else { - #ifdef VERBOSE_DEBUG - std::cout << "Learnt clause in other part:"; c.plainPrint(); - #endif - - *j++ = *i; - } - } - cs.shrink(i-j); -} - /** @brief Adds the saved states to the final solutions diff --git a/src/sat/cryptominisat2/PartHandler.h b/src/sat/cryptominisat2/PartHandler.h index 7751d2b..5a44307 100644 --- a/src/sat/cryptominisat2/PartHandler.h +++ b/src/sat/cryptominisat2/PartHandler.h @@ -61,9 +61,8 @@ class PartHandler //For moving clauses void moveBinClauses(Solver& newSolver, const uint32_t part, PartFinder& partFinder); - void moveClauses(vec& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder); + void moveXorClauses(vec& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder); void moveClauses(vec& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder); - void moveLearntClauses(vec& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder); //Checking moved clauses const bool checkClauseMovement(const Solver& thisSolver, const uint32_t part, const PartFinder& partFinder) const; diff --git a/src/sat/cryptominisat2/RestartTypeChooser.cpp b/src/sat/cryptominisat2/RestartTypeChooser.cpp index dcda986..0cf6a66 100644 --- a/src/sat/cryptominisat2/RestartTypeChooser.cpp +++ b/src/sat/cryptominisat2/RestartTypeChooser.cpp @@ -26,8 +26,8 @@ using std::pair; RestartTypeChooser::RestartTypeChooser(const Solver& s) : solver(s) - , topX(100) - , limit(40) + , topXPerc(0.01) + , limitPerc(0.0018) { } @@ -39,6 +39,18 @@ accumulate data. Finally, choose() is called to choose the restart type */ void RestartTypeChooser::addInfo() { + if (firstVarsOld.empty()) { + double size = std::max(solver.order_heap.size(), 10000U); + topX = (uint32_t)(topXPerc*size) + 1; + limit = (uint32_t)(limitPerc*size) + 1; + #ifdef VERBOSE_DEBUG + std::cout << "c topX for chooser: " << topX << std::endl; + std::cout << "c limit for chooser: " << limit << std::endl; + #endif + } + assert(topX != 0); + assert(limit != 0); + firstVarsOld = firstVars; calcHeap(); uint32_t sameIn = 0; @@ -49,13 +61,13 @@ void RestartTypeChooser::addInfo() sameIn++; } #ifdef VERBOSE_DEBUG - std::cout << " Same vars in first&second first 100: " << sameIn << std::endl; + std::cout << "c Same vars in first&second: " << sameIn << std::endl; #endif sameIns.push_back(sameIn); } #ifdef VERBOSE_DEBUG - std::cout << "Avg same vars in first&second first 100: " << avg() << " standard Deviation:" << stdDeviation(sameIns) < mypair = countVarsDegreeStDev(); - if ((mypair.second < 80 && - (avg() > (double)limit || ((avg() > (double)(limit*0.9) && stdDeviation(sameIns) < 5)))) - || - (mypair.second < 80 && (double)solver.xorclauses.size() > (double)solver.nClauses()*0.1)) + #ifdef VERBOSE_DEBUG + std::cout << "c restart choosing time. Avg: " << avg() << + " , stdDeviation : " << stdDeviation(sameIns) << std::endl; + std::cout << "c topX for chooser: " << topX << std::endl; + std::cout << "c limit for chooser: " << limit << std::endl; + #endif + //pair mypair = countVarsDegreeStDev(); + if ((avg() > (double)limit + || ((avg() > (double)(limit*0.9) && stdDeviation(sameIns) < 5))) + || ((double)solver.xorclauses.size() > (double)solver.nClauses()*0.1) + || (solver.order_heap.size() < 10000) + ) { + #ifdef VERBOSE_DEBUG + std::cout << "c restartTypeChooser chose STATIC restarts" << std::endl; + #endif return static_restart; - else + } else { + #ifdef VERBOSE_DEBUG + std::cout << "c restartTypeChooser chose DYNAMIC restarts" << std::endl; + #endif return dynamic_restart; + } } /** @@ -102,7 +128,6 @@ const double RestartTypeChooser::stdDeviation(vector& measure) const void RestartTypeChooser::calcHeap() { firstVars.clear(); - firstVars.reserve(topX); #ifdef PRINT_VARS std::cout << "First vars:" << std::endl; #endif @@ -119,7 +144,7 @@ void RestartTypeChooser::calcHeap() #endif } -const std::pair RestartTypeChooser::countVarsDegreeStDev() const +/*const std::pair RestartTypeChooser::countVarsDegreeStDev() const { vector degrees; degrees.resize(solver.nVars(), 0); @@ -175,5 +200,5 @@ void RestartTypeChooser::addDegreesBin(vector& degrees) const } } } -} +}*/ diff --git a/src/sat/cryptominisat2/RestartTypeChooser.h b/src/sat/cryptominisat2/RestartTypeChooser.h index 446b1e9..ab68ff8 100644 --- a/src/sat/cryptominisat2/RestartTypeChooser.h +++ b/src/sat/cryptominisat2/RestartTypeChooser.h @@ -53,17 +53,20 @@ class RestartTypeChooser private: void calcHeap(); const double avg() const; - const std::pair countVarsDegreeStDev() const; const double stdDeviation(vector& measure) const; + /*const std::pair countVarsDegreeStDev() const; template void addDegrees(const vec& cs, vector& degrees) const; - void addDegreesBin(vector& degrees) const; + void addDegreesBin(vector& degrees) const;*/ const Solver& solver; - const uint32_t topX; /// sameIns; + uint32_t topX; + uint32_t limit; vector firstVars; /// firstVarsOld; ///. #include "time_mem.h" #include "Subsumer.h" #include "XorSubsumer.h" +#include "PartHandler.h" SCCFinder::SCCFinder(Solver& _solver) : solver(_solver) , varElimed1(_solver.subsumer->getVarElimed()) , varElimed2(_solver.xorSubsumer->getVarElimed()) + , varPartHandled(_solver.partHandler->getSavedState()) , replaceTable(_solver.varReplacer->getReplaceTable()) , totalTime(0.0) {} @@ -86,20 +88,20 @@ void SCCFinder::tarjan(const uint32_t vertex) doit(lit, vertex); } - if (solver.conf.doExtendedSCC) { + if (solver.conf.doExtendedSCC && solver.conf.doCacheOTFSSR) { Lit vertLit = Lit::toLit(vertex); - vector& transCache = solver.transOTFCache[(~Lit::toLit(vertex)).toInt()].lits; - vector::iterator it = transCache.begin(); - vector::iterator it2 = it; + vector& transCache = solver.transOTFCache[(~vertLit).toInt()].lits; + vector::iterator it = transCache.begin(); + vector::iterator it2 = it; uint32_t newSize = 0; - for (vector::iterator end = transCache.end(); it != end; it++) { - Lit lit = *it; + for (vector::iterator end = transCache.end(); it != end; it++) { + Lit lit = it->getLit(); lit = replaceTable[lit.var()] ^ lit.sign(); - if (lit == vertLit || varElimed1[lit.var()] || varElimed2[lit.var()]) continue; - *it2++ = lit; + if (lit == vertLit || varElimed1[lit.var()] || varElimed2[lit.var()] || varPartHandled[lit.var()] != l_Undef) continue; + *it2++ = LitExtra(lit, it->getOnlyNLBin()); newSize++; - doit(lit, vertex); + if (lit != ~vertLit) doit(lit, vertex); } transCache.resize(newSize); } diff --git a/src/sat/cryptominisat2/SCCFinder.h b/src/sat/cryptominisat2/SCCFinder.h index 9b60b35..0737955 100644 --- a/src/sat/cryptominisat2/SCCFinder.h +++ b/src/sat/cryptominisat2/SCCFinder.h @@ -45,6 +45,7 @@ class SCCFinder { Solver& solver; const vec& varElimed1; const vec& varElimed2; + const vec& varPartHandled; const vector& replaceTable; double totalTime; }; diff --git a/src/sat/cryptominisat2/SharedData.h b/src/sat/cryptominisat2/SharedData.h index 8688f98..ed701c7 100644 --- a/src/sat/cryptominisat2/SharedData.h +++ b/src/sat/cryptominisat2/SharedData.h @@ -22,12 +22,54 @@ along with this program. If not, see . #include "SolverTypes.h" #include +#include + +class BinClause { + public: + BinClause() {}; + BinClause(const Lit _lit1, const Lit _lit2, const bool _learnt = true) : + lit1(_lit1) + , lit2(_lit2) + , learnt(_learnt) + {} + Lit lit1; + Lit lit2; + bool learnt; +}; + +class TriClause { + public: + TriClause() {}; + TriClause(const Lit _lit1, const Lit _lit2, const Lit _lit3, const bool _learnt = true) : + lit1(_lit1) + , lit2(_lit2) + , lit3(_lit3) + , learnt(_learnt) + {} + Lit lit1; + Lit lit2; + Lit lit3; + bool learnt; +}; class SharedData { public: + SharedData() : + threadAddingVars(0) + , EREnded(false) + , numNewERVars(0) + , lastNewERVars(0) + {} vec value; - std::vector > bins; + std::vector > bins; + std::vector > tris; + + int threadAddingVars; + bool EREnded; + std::set othersSyncedER; + uint32_t numNewERVars; + uint32_t lastNewERVars; }; #endif //SHARED_DATA_H diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 79fe687..4e831a0 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -36,15 +36,12 @@ Modifications for CryptoMiniSat are under GPLv3 licence. #include "MatrixFinder.h" #include "DataSync.h" -#ifdef _MSC_VER -#define __builtin_prefetch(a,b,c) -//#define __builtin_prefetch(a,b) -#endif //_MSC_VER - #ifdef VERBOSE_DEBUG #define UNWINDING_DEBUG +#define VERBOSE_DEBUG_GATE #endif + //#define DEBUG_UNCHECKEDENQUEUE_LEVEL0 //#define VERBOSE_DEBUG_POLARITIES //#define DEBUG_DYNAMIC_RESTART @@ -60,8 +57,8 @@ Modifications for CryptoMiniSat are under GPLv3 licence. Solver::Solver(const SolverConf& _conf, const GaussConf& _gaussconfig, SharedData* sharedData) : // Parameters: (formerly in 'SearchParams') conf(_conf) - , gaussconfig(_gaussconfig) , needToInterrupt (false) + , gaussconfig(_gaussconfig) #ifdef USE_GAUSS , sum_gauss_called (0) , sum_gauss_confl (0) @@ -78,10 +75,11 @@ Solver::Solver(const SolverConf& _conf, const GaussConf& _gaussconfig, SharedDat , moreRecurMinLDo(0) , updateTransCache(0) , nbClOverMaxGlue(0) + , OTFGateRemLits(0) + , OTFGateRemSucc(0) , ok (true) , numBins (0) - , cla_inc (1) , qhead (0) , mtrand ((unsigned long int)0) @@ -102,9 +100,10 @@ Solver::Solver(const SolverConf& _conf, const GaussConf& _gaussconfig, SharedDat , learnt_clause_group(0) , libraryCNFFile (NULL) , restartType (static_restart) - , lastSelectedRestartType (static_restart) + , subRestartType (static_restart) , simplifying (false) , totalSimplifyTime(0.0) + , numSimplifyRounds(0) , simpDB_assigns (-1) , simpDB_props (0) { @@ -167,13 +166,14 @@ Var Solver::newVar(bool dvar) watches .push(); // (list for negative literal) reason .push(PropBy()); assigns .push(l_Undef); - level .push(-1); + level .push(std::numeric_limits::max()); binPropData.push(); activity .push(0); seen .push_back(0); seen .push_back(0); permDiff .push(0); unWindGlue.push(NULL); + popularity.push(0); //Transitive OTF self-subsuming resolution seen2 .push_back(0); @@ -184,12 +184,11 @@ Var Solver::newVar(bool dvar) litReachable.push_back(LitReachData()); polarity .push_back(defaultPolarity()); - #ifdef USE_OLD_POLARITIES - oldPolarity.push_back(defaultPolarity()); - #endif //USE_OLD_POLARITIES + //Variable heap, long-term polarity count decision_var.push_back(dvar); insertVarOrder(v); + lTPolCount.push_back(std::make_pair(0,0)); varReplacer->newVar(); partHandler->newVar(); @@ -253,7 +252,7 @@ XorClause* Solver::addXorClauseInt(T& ps, bool xorEqualFalse, const uint32_t gro } case 1: { uncheckedEnqueue(Lit(ps[0].var(), xorEqualFalse)); - ok = (propagate().isNULL()); + ok = (propagate().isNULL()); return NULL; } case 2: { @@ -355,8 +354,8 @@ and only internally */ template Clause* Solver::addClauseInt(T& ps, uint32_t group - , const bool learnt, const uint32_t glue, const float miniSatActivity - , const bool inOriginalInput) + , const bool learnt, const uint32_t glue + , const bool inOriginalInput, const bool attach) { assert(ok); @@ -379,25 +378,34 @@ Clause* Solver::addClauseInt(T& ps, uint32_t group return NULL; } else if (ps.size() == 1) { uncheckedEnqueue(ps[0]); - ok = (propagate().isNULL()); + ok = (propagate().isNULL()); return NULL; } + //Randomise clause + assert(ps.size() >= 2); + for(uint32_t i2 = 0; i2 < (uint32_t)(ps.size()-1); i2++) { + uint32_t r = mtrand.randInt(ps.size()-i2-1); + std::swap(ps[i2], ps[i2+r]); + } + + if (ps.size() > 2) { Clause* c = clauseAllocator.Clause_new(ps, group); - if (learnt) c->makeLearnt(glue, miniSatActivity); - attachClause(*c); + if (learnt) c->makeLearnt(glue); + if (attach) attachClause(*c); + if (ps.size() == 3 && !inOriginalInput) dataSync->signalNewTriClause(ps, learnt); return c; } else { attachBinClause(ps[0], ps[1], learnt); - if (!inOriginalInput) dataSync->signalNewBinClause(ps); + if (!inOriginalInput) dataSync->signalNewBinClause(ps, learnt); numNewBin++; return NULL; } } -template Clause* Solver::addClauseInt(Clause& ps, const uint32_t group, const bool learnt, const uint32_t glue, const float miniSatActivity, const bool inOriginalInput); -template Clause* Solver::addClauseInt(vec& ps, const uint32_t group, const bool learnt, const uint32_t glue, const float miniSatActivity, const bool inOriginalInput); +template Clause* Solver::addClauseInt(Clause& ps, const uint32_t group, const bool learnt, const uint32_t glue, const bool inOriginalInput, const bool attach); +template Clause* Solver::addClauseInt(vec& ps, const uint32_t group, const bool learnt, const uint32_t glue, const bool inOriginalInput, const bool attach); template const bool Solver::addClauseHelper(T& ps, const uint32_t group, const char* group_name) { @@ -457,7 +465,7 @@ bool Solver::addClause(T& ps, const uint32_t group, const char* group_name) std::cout << "addClause() called with new clause: " << ps << std::endl; #endif //VERBOSE_DEBUG if (!addClauseHelper(ps, group, group_name)) return false; - Clause* c = addClauseInt(ps, group, false, 0, 0, true); + Clause* c = addClauseInt(ps, group, false, 0, true); if (c != NULL) clauses.push(c); return ok; @@ -468,17 +476,17 @@ template bool Solver::addClause(Clause& ps, const uint32_t group, const char* gr template -bool Solver::addLearntClause(T& ps, const uint32_t group, const char* group_name, const uint32_t glue, const float miniSatActivity) +bool Solver::addLearntClause(T& ps, const uint32_t group, const char* group_name, const uint32_t glue) { if (!addClauseHelper(ps, group, group_name)) return false; - Clause* c = addClauseInt(ps, group, true, glue, miniSatActivity, true); + Clause* c = addClauseInt(ps, group, true, glue, true); if (c != NULL) learnts.push(c); return ok; } -template bool Solver::addLearntClause(vec& ps, const uint32_t group, const char* group_name, const uint32_t glue, const float miniSatActivity); -template bool Solver::addLearntClause(Clause& ps, const uint32_t group, const char* group_name, const uint32_t glue, const float miniSatActivity); +template bool Solver::addLearntClause(vec& ps, const uint32_t group, const char* group_name, const uint32_t glue); +template bool Solver::addLearntClause(Clause& ps, const uint32_t group, const char* group_name, const uint32_t glue); /** @@ -539,11 +547,11 @@ void Solver::attachClause(Clause& c) { assert(c.size() > 2); #ifdef DEBUG_ATTACH - assert(c[0].var() != c[1].var()); assert(assigns[c[0].var()] == l_Undef); assert(value(c[1]) == l_Undef || value(c[1]) == l_False); for (uint32_t i = 0; i < c.size(); i++) { + if (i > 0) assert(c[i-1].var() != c[i].var()); assert(!subsumer->getVarElimed()[c[i].var()]); assert(!xorSubsumer->getVarElimed()[c[i].var()]); } @@ -640,11 +648,20 @@ void Solver::detachModifiedClause(const Var var1, const Var var2, const uint32_t clauses_literals -= origSize; } +void Solver::syncData() +{ + dataSync->syncData(); +} + +void Solver::finishAddingVars() +{ + subsumer->setFinishedAddingVars(true); +} + /** @brief Revert to the state at given level -Also reverts all stuff in Gass-elimination, as well as resetting the old -default polarities if USE_OLD_POLARITIES is set (which is by default NOT set). +Also reverts all stuff in Gass-elimination */ void Solver::cancelUntil(int level) { @@ -666,9 +683,6 @@ void Solver::cancelUntil(int level) #ifdef VERBOSE_DEBUG cout << "Canceling var " << var+1 << " sublevel: " << sublevel << endl; #endif - #ifdef USE_OLD_POLARITIES - polarity[var] = oldPolarity[var]; - #endif //USE_OLD_POLARITIES assigns[var] = l_Undef; insertVarOrder(var); if (unWindGlue[var] != NULL) { @@ -882,21 +896,27 @@ void Solver::calcReachability() if (value(lit.var()) != l_Undef || subsumer->getVarElimed()[lit.var()] || xorSubsumer->getVarElimed()[lit.var()] + || varReplacer->getReplaceTable()[lit.var()].var() != lit.var() || partHandler->getSavedState()[lit.var()] != l_Undef || !decision_var[lit.var()]) continue; - vector& cache = transOTFCache[(~lit).toInt()].lits; + vector& cache = transOTFCache[(~lit).toInt()].lits; uint32_t cacheSize = cache.size(); - for (vector::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) { + for (vector::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) { /*if (solver.value(it->var()) != l_Undef || solver.subsumer->getVarElimed()[it->var()] - || solver.xorSubsumer->getVarElimed()[it->var()]) + || solver.xorSubsumer->getVarElimed()[it->var()] + || partHandler->getSavedState()[lit.var()] != l_Undef) continue;*/ - if ((*it == lit) || (*it == ~lit)) continue; - if (litReachable[it->toInt()].lit == lit_Undef || litReachable[it->toInt()].numInCache < cacheSize) { - litReachable[it->toInt()].lit = lit; - litReachable[it->toInt()].numInCache = cacheSize; + if (it->getLit() == lit || it->getLit() == ~lit) continue; + + if (litReachable[it->getLit().toInt()].lit == lit_Undef + || litReachable[it->getLit().toInt()].numInCache toInt()].numInCache == cacheSize && mtrand.randInt(1) == 0) continue; + litReachable[it->getLit().toInt()].lit = lit; + litReachable[it->getLit().toInt()].numInCache = cacheSize; } } } @@ -923,14 +943,15 @@ void Solver::saveOTFData() assert(decisionLevel() == 1); Lit lev0Lit = trail[trail_lim[0]]; - Solver::TransCache& oTFCache = transOTFCache[(~lev0Lit).toInt()]; + TransCache& oTFCache = transOTFCache[(~lev0Lit).toInt()]; oTFCache.conflictLastUpdated = conflicts; - oTFCache.lits.clear(); + vector lits; for (int sublevel = trail.size()-1; sublevel > (int)trail_lim[0]; sublevel--) { Lit lit = trail[sublevel]; - oTFCache.lits.push_back(lit); + lits.push_back(LitExtra(lit, false)); } + oTFCache.merge(lits); } //================================================================================================= @@ -987,7 +1008,7 @@ Lit Solver::pickBranchLit() if (!simplifying && value(next) == l_Undef && decision_var[next]) { signSet = true; if (avgBranchDepth.isvalid()) - signSetTo = polarity[next] ^ (mtrand.randInt(avgBranchDepth.getAvgUInt() * ((lastSelectedRestartType == static_restart) ? 2 : 1) ) == 1); + signSetTo = polarity[next] ^ (mtrand.randInt(avgBranchDepth.getAvgUInt() * ((subRestartType == static_restart) ? 2 : 1) ) == 1); else signSetTo = polarity[next]; Lit nextLit = Lit(next, signSetTo); @@ -1014,7 +1035,7 @@ Lit Solver::pickBranchLit() sign = mtrand.randInt(1); #ifdef RANDOM_LOOKAROUND_SEARCHSPACE else if (avgBranchDepth.isvalid()) - sign = polarity[next] ^ (mtrand.randInt(avgBranchDepth.getAvgUInt() * ((lastSelectedRestartType == static_restart) ? 2 : 1) ) == 1); + sign = polarity[next] ^ (mtrand.randInt(avgBranchDepth.getAvgUInt() * ((subRestartType == static_restart) ? 2 : 1) ) == 1); #endif else sign = polarity[next]; @@ -1077,7 +1098,7 @@ current decision level. @return NULL if the conflict doesn't on-the-fly subsume the last clause, and the pointer of the clause if it does */ -Clause* Solver::analyze(PropBy conflHalf, vec& out_learnt, int& out_btlevel, uint32_t &glue, const bool update) +Clause* Solver::analyze(PropBy conflHalf, vec& out_learnt, uint32_t& out_btlevel, uint32_t &glue, const bool update) { int pathC = 0; Lit p = lit_Undef; @@ -1094,9 +1115,6 @@ Clause* Solver::analyze(PropBy conflHalf, vec& out_learnt, int& out_btlevel do { assert(!confl.isNULL()); // (otherwise should be UIP) - if (update && restartType == static_restart && confl.isClause() && confl.getClause()->learnt()) - claBumpActivity(*confl.getClause()); - for (uint32_t j = (p == lit_Undef) ? 0 : 1, size = confl.size(); j != size; j++) { Lit q = confl[j]; const Var my_var = q.var(); @@ -1104,11 +1122,11 @@ Clause* Solver::analyze(PropBy conflHalf, vec& out_learnt, int& out_btlevel if (!seen[my_var] && level[my_var] > 0) { varBumpActivity(my_var); seen[my_var] = 1; - assert(level[my_var] <= (int)decisionLevel()); - if (level[my_var] >= (int)decisionLevel()) { + assert(level[my_var] <= decisionLevel()); + if (level[my_var] >= decisionLevel()) { pathC++; #ifdef UPDATE_VAR_ACTIVITY_BASED_ON_GLUE - if (lastSelectedRestartType == dynamic_restart + if (subRestartType == dynamic_restart && reason[q.var()].isClause() && !reason[q.var()].isNULL() && clauseAllocator.getPointer(reason[q.var()].getClause())->learnt()) @@ -1165,10 +1183,19 @@ Clause* Solver::analyze(PropBy conflHalf, vec& out_learnt, int& out_btlevel for (uint32_t j = 0; j != analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared) + if (conf.doMinimLearntMore && out_learnt.size() > 1) minimiseLeartFurther(out_learnt, calcNBLevels(out_learnt)); glue = calcNBLevels(out_learnt); tot_literals += out_learnt.size(); + #ifdef VERBOSE_DEBUG_GATE + std::cout << "Final clause: " << out_learnt << std::endl; + for (uint32_t i = 0; i < out_learnt.size(); i++) { + std::cout << "val out_learnt[" << i << "]:" << value(out_learnt[i]) << std::endl; + std::cout << "lev out_learnt[" << i << "]:" << level[out_learnt[i].var()] << std::endl; + } + #endif + // Find correct backtrack level: // if (out_learnt.size() == 1) @@ -1181,17 +1208,20 @@ Clause* Solver::analyze(PropBy conflHalf, vec& out_learnt, int& out_btlevel std::swap(out_learnt[max_i], out_learnt[1]); out_btlevel = level[out_learnt[1].var()]; } + #ifdef VERBOSE_DEBUG_GATE + std::cout << "out_btlevel: " << out_btlevel << std::endl; + #endif - if (lastSelectedRestartType == dynamic_restart) { - #ifdef UPDATE_VAR_ACTIVITY_BASED_ON_GLUE + #ifdef UPDATE_VAR_ACTIVITY_BASED_ON_GLUE + if (subRestartType == dynamic_restart) { for(uint32_t i = 0; i != lastDecisionLevel.size(); i++) { PropBy cl = reason[lastDecisionLevel[i]]; if (cl.isClause() && clauseAllocator.getPointer(cl.getClause())->getGlue() < glue) varBumpActivity(lastDecisionLevel[i]); } lastDecisionLevel.clear(); - #endif } + #endif //We can only on-the-fly subsume clauses that are not 2- or 3-long //furthermore, we cannot subsume a clause that is marked for deletion @@ -1217,12 +1247,15 @@ form to carry out the forward-self-subsuming resolution */ void Solver::minimiseLeartFurther(vec& cl, const uint32_t glue) { + if (!conf.doCacheOTFSSR || !conf.doMinimLMoreRecur) return; //80 million is kind of a hack. It seems that the longer the solving //the slower this operation gets. So, limiting the "time" with total //number of conflict literals is maybe a good way of doing this bool clDoMinLRec = false; - if (conf.doCacheOTFSSR && conf.doMinimLMoreRecur) { - switch(lastSelectedRestartType) { + if (conf.doAlwaysFMinim) + clDoMinLRec = true; + else { + switch(subRestartType) { case dynamic_restart : clDoMinLRec |= glue < 0.6*glueHistory.getAvgAllDouble(); //NOTE: No "break;" here on purpose @@ -1240,19 +1273,128 @@ void Solver::minimiseLeartFurther(vec& cl, const uint32_t glue) //To count the "amount of time" invested in doing transitive on-the-fly //self-subsuming resolution - uint32_t moreRecurProp = 0; + //uint32_t moreRecurProp = 0; for (uint32_t i = 0; i < cl.size(); i++) seen[cl[i].toInt()] = 1; + + if (conf.doGateFind) { + bool gateRemSuccess = false; + vec oldCl = cl; + while (true) { + for (Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) { + const vector& gates = subsumer->getGateOcc(*l); + if (gates.empty()) continue; + + for (vector::const_iterator it2 = gates.begin(), end2 = gates.end(); it2 != end2; it2++) { + OrGate& gate = **it2; + + gate.eqLit = varReplacer->getReplaceTable()[gate.eqLit.var()] ^ gate.eqLit.sign(); + if (subsumer->getVarElimed()[gate.eqLit.var()] + || xorSubsumer->getVarElimed()[gate.eqLit.var()] + || partHandler->getSavedState()[gate.eqLit.var()] != l_Undef + || !decision_var[gate.eqLit.var()]) continue; + + bool OK = true; + for (uint32_t i = 0; i < gate.lits.size(); i++) { + if (!seen[gate.lits[i].toInt()]) { + OK = false; + break; + } + } + if (!OK) continue; + + //Treat gate + #ifdef VERBOSE_DEBUG_GATE + std::cout << "Gate: eqLit " << gate.eqLit << " lits "; + for (uint32_t i = 0; i < gate.lits.size(); i++) { + std::cout << gate.lits[i] << ", "; + } + std::cout << " origclause: "; + for (uint32_t i = 0; i < gate.origCl.size(); i++) { + std::cout << gate.origCl[i] << ", "; + } + std::cout << std::endl; + #endif + + bool firstInside = false; + Lit *lit1 = cl.getData(); + Lit *lit2 = cl.getData(); + bool first = true; + for (Lit *end3 = cl.getDataEnd(); lit1 != end3; lit1++, first = false) { + bool in = false; + for (uint32_t i = 0; i < gate.lits.size(); i++) { + if (*lit1 == gate.lits[i]) { + in = true; + if (first) firstInside = true; + } + } + if (in) { + seen[lit1->toInt()] = false; + } else { + *lit2++ = *lit1; + } + } + if (!seen[gate.eqLit.toInt()]) { + *lit2++ = gate.eqLit; + seen[gate.eqLit.toInt()] = true; + } + assert(!seen[(~gate.eqLit).toInt()]); + cl.shrink_(lit1-lit2); + OTFGateRemLits += lit1-lit2; + #ifdef VERBOSE_DEBUG_GATE + std::cout << "Old clause: " << oldCl << std::endl; + for (uint32_t i = 0; i < oldCl.size(); i++) { + std::cout << "-> Lit " << oldCl[i] << " lev: " << level[oldCl[i].var()] << " val: " << value(oldCl[i]) < Lit " << cl[i] << " lev: " << level[cl[i].var()] << " val: " << value(cl[i]) << std::endl; + } + #endif + + if (firstInside) { + uint32_t swapWith = std::numeric_limits::max(); + for (uint32_t i = 0; i < cl.size(); i++) { + if (cl[i] == gate.eqLit) swapWith = i; + } + std::swap(cl[swapWith], cl[0]); + } + #ifdef VERBOSE_DEBUG_GATE + std::cout << "New clause2: " << cl << std::endl; + for (uint32_t i = 0; i < cl.size(); i++) { + std::cout << "-> Lit " << cl[i] << " lev: " << level[cl[i].var()] << std::endl; + } + #endif + + gateRemSuccess = true; + + //Do this recurively, again + goto next; + } + } + break; + next:; + } + OTFGateRemSucc += gateRemSuccess; + #ifdef VERBOSE_DEBUG_GATE + if (gateRemSuccess) std::cout << "--------" << std::endl; + #endif + } + + uint32_t moreRecurProp = 0; + for (Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) { if (seen[l->toInt()] == 0) continue; Lit lit = *l; - if (clDoMinLRec) { - if (moreRecurProp > 450 + if (clDoMinLRec && conf.doCacheOTFSSR) { + if (moreRecurProp >= 450 || (transOTFCache[l->toInt()].conflictLastUpdated != std::numeric_limits::max() - && (transOTFCache[l->toInt()].conflictLastUpdated + thisUpdateTransOTFSSCache >= conflicts))) { - for (vector::const_iterator it = transOTFCache[l->toInt()].lits.begin(), end2 = transOTFCache[l->toInt()].lits.end(); it != end2; it++) { - seen[(~(*it)).toInt()] = 0; + && (transOTFCache[l->toInt()].conflictLastUpdated + thisUpdateTransOTFSSCache >= conflicts)) + ) { + const TransCache& cache1 = transOTFCache[l->toInt()]; + for (vector::const_iterator it = cache1.lits.begin(), end2 = cache1.lits.end(); it != end2; it++) { + seen[(~(it->getLit())).toInt()] = 0; } } else { updateTransCache++; @@ -1280,7 +1422,7 @@ void Solver::minimiseLeartFurther(vec& cl, const uint32_t glue) //watches are mostly sorted, so it's more-or-less OK to break // if non-bi or non-tri is encountered - break; + //break; } } @@ -1305,35 +1447,33 @@ void Solver::minimiseLeartFurther(vec& cl, const uint32_t glue) void Solver::transMinimAndUpdateCache(const Lit lit, uint32_t& moreRecurProp) { - vector& allAddedToSeen2 = transOTFCache[lit.toInt()].lits; - allAddedToSeen2.clear(); + assert(conf.doCacheOTFSSR); + vector lits; - toRecursiveProp.push(lit); + toRecursiveProp.push(~lit); while(!toRecursiveProp.empty()) { Lit thisLit = toRecursiveProp.top(); toRecursiveProp.pop(); - //watched is messed: lit is in watched[~lit] - vec& ws = watches[(~thisLit).toInt()]; + vec& ws = watches[thisLit.toInt()]; moreRecurProp += ws.size() +10; for (Watched* i = ws.getData(), *end = ws.getDataEnd(); i != end; i++) { if (i->isBinary()) { moreRecurProp += 5; Lit otherLit = i->getOtherLit(); //don't do indefinite recursion, and don't remove "a" when doing self-subsuming-resolution with 'a OR b' - if (seen2[otherLit.toInt()] != 0 || otherLit == ~lit) break; + if (seen2[otherLit.toInt()] != 0 || otherLit == ~lit) continue; seen2[otherLit.toInt()] = 1; - allAddedToSeen2.push_back(otherLit); - toRecursiveProp.push(~otherLit); - } else { - break; + lits.push_back(LitExtra(otherLit, false)); + toRecursiveProp.push(otherLit); } } } assert(toRecursiveProp.empty()); + transOTFCache[lit.toInt()].merge(lits); - for (vector::const_iterator it = allAddedToSeen2.begin(), end = allAddedToSeen2.end(); it != end; it++) { - seen[(~(*it)).toInt()] = 0; - seen2[it->toInt()] = 0; + for (vector::const_iterator it = transOTFCache[lit.toInt()].lits.begin(), end = transOTFCache[lit.toInt()].lits.end(); it != end; it++) { + seen[(~(it->getLit())).toInt()] = 0; + seen2[it->getLit().toInt()] = 0; } transOTFCache[lit.toInt()].conflictLastUpdated = conflicts; @@ -1421,15 +1561,14 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) Call this when a fact has been found. Sets the value, enqueues it for propagation, sets its level, sets why it was propagated, saves the polarity, -and does some logging if logging is enabled. May also save the "old" polarity -(i.e. polarity that was in polarities[] at p.var()] of the variable if -USE_OLD_POLARITIES is set +and does some logging if logging is enabled @p p the fact to enqueue @p from Why was it propagated (binary clause, tertiary clause, normal clause) */ -void Solver::uncheckedEnqueue(const Lit p, const PropBy& from) +void Solver::uncheckedEnqueue(const Lit p, const PropBy from) { + __builtin_prefetch(watches.getData()+p.toInt(), 1, 0); #ifdef DEBUG_UNCHECKEDENQUEUE_LEVEL0 #ifndef VERBOSE_DEBUG if (decisionLevel() == 0) @@ -1444,18 +1583,27 @@ void Solver::uncheckedEnqueue(const Lit p, const PropBy& from) } #endif //DEBUG_UNCHECKEDENQUEUE_LEVEL0 - //assert(decisionLevel() == 0 || !subsumer->getVarElimed()[p.var()]); + #ifdef UNCHECKEDENQUEUE_DEBUG + assert(decisionLevel() == 0 || !subsumer->getVarElimed()[p.var()]); + assert(decisionLevel() == 0 || !xorSubsumer->getVarElimed()[p.var()]); + Var repl = varReplacer->getReplaceTable()[p.var()].var(); + if (repl != p.var()) { + assert(!subsumer->getVarElimed()[repl]); + assert(!xorSubsumer->getVarElimed()[repl]); + assert(partHandler->getSavedState()[repl] == l_Undef); + } + #endif - assert(assigns[p.var()].isUndef()); const Var v = p.var(); + assert(value(v).isUndef()); assigns [v] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient level [v] = decisionLevel(); reason [v] = from; - #ifdef USE_OLD_POLARITIES - oldPolarity[p.var()] = polarity[p.var()]; - #endif //USE_OLD_POLARITIES - polarity[p.var()] = p.sign(); + if (!from.isNULL()) increaseAgility(polarity[p.var()] != p.sign()); + polarity[v] = p.sign(); trail.push(p); + __builtin_prefetch(watches[p.toInt()].getData(), 1, 0); + popularity[v]++; #ifdef STATS_NEEDED if (dynamic_behaviour_analysis) @@ -1463,17 +1611,16 @@ void Solver::uncheckedEnqueue(const Lit p, const PropBy& from) #endif } -/*_________________________________________________________________________________________________ -| -| propagate : [void] -> [Clause*] -| -| Description: -| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, -| otherwise NULL. -| -| Post-conditions: -| * the propagation queue is empty, even if there was a conflict. -|________________________________________________________________________________________________@*/ +void Solver::uncheckedEnqueueExtend(const Lit p, const PropBy& from) +{ + 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(); + reason [v] = from; + trail.push(p); +} + /** @brief Propagates a binary clause @@ -1481,12 +1628,13 @@ Need to be somewhat tricky if the clause indicates that current assignement is incorrect (i.e. both literals evaluate to FALSE). If conflict if found, sets failBinLit */ -inline const bool Solver::propBinaryClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl) +template +inline const bool Solver::propBinaryClause(Watched* i,Watched *end, const Lit p, PropBy& confl) { - *j++ = *i; lbool val = value(i->getOtherLit()); if (val.isUndef()) { - uncheckedEnqueue(i->getOtherLit(), PropBy(p)); + if (full) uncheckedEnqueue(i->getOtherLit(), PropBy(p)); + else uncheckedEnqueueLight(i->getOtherLit()); } else if (val == l_False) { confl = PropBy(p); failBinLit = i->getOtherLit(); @@ -1504,15 +1652,17 @@ Need to be somewhat tricky if the clause indicates that current assignement is incorrect (i.e. all 3 literals evaluate to FALSE). If conflict is found, sets failBinLit */ -inline const bool Solver::propTriClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl) +template +inline const bool Solver::propTriClause(Watched* i, Watched *end, const Lit p, PropBy& confl) { - *j++ = *i; lbool val = value(i->getOtherLit()); lbool val2 = value(i->getOtherLit2()); if (val.isUndef() && val2 == l_False) { - uncheckedEnqueue(i->getOtherLit(), PropBy(p, i->getOtherLit2())); + if (full) uncheckedEnqueue(i->getOtherLit(), PropBy(p, i->getOtherLit2())); + else uncheckedEnqueueLight(i->getOtherLit()); } else if (val == l_False && val2.isUndef()) { - uncheckedEnqueue(i->getOtherLit2(), PropBy(p, i->getOtherLit())); + if (full) uncheckedEnqueue(i->getOtherLit2(), PropBy(p, i->getOtherLit())); + else uncheckedEnqueueLight(i->getOtherLit2()); } else if (val == l_False && val2 == l_False) { confl = PropBy(p, i->getOtherLit2()); failBinLit = i->getOtherLit(); @@ -1524,11 +1674,12 @@ inline const bool Solver::propTriClause(Watched* &i, Watched* &j, Watched *end, } /** -@brief Propagates a tertiary (3-long) clause +@brief Propagates a normal (n-long where n > 3) clause We have blocked literals in this case in the watchlist. That must be checked and updated. */ +template inline const bool Solver::propNormalClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl, const bool update) { if (value(i->getBlockedLit()).getBool()) { @@ -1585,7 +1736,11 @@ inline const bool Solver::propNormalClause(Watched* &i, Watched* &j, Watched *en qhead = trail.size(); return false; } else { - uncheckedEnqueue(c[0], offset); + #ifdef VERBOSE_DEBUG + printf("PropNorm causing propagation\n"); + #endif + if (full) uncheckedEnqueue(c[0], PropBy(offset)); + else uncheckedEnqueueLight(c[0]); #ifdef DYNAMICALLY_UPDATE_GLUE if (update && c.learnt() && c.getGlue() > 2) { // GA uint32_t glue = calcNBLevels(c); @@ -1601,7 +1756,7 @@ inline const bool Solver::propNormalClause(Watched* &i, Watched* &j, Watched *en } /** -@brief Propagates a tertiary (3-long) clause +@brief Propagates an XOR clause Strangely enough, we need to have 4 literals in the wathclists: for the first two varialbles, BOTH negations (v and ~v). This means quite some @@ -1610,6 +1765,7 @@ better memory-accesses since the watchlist is already in the memory... \todo maybe not worth it, and a variable-based watchlist should be used */ +template inline const bool Solver::propXorClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl) { ClauseOffset offset = i->getXorOffset(); @@ -1645,7 +1801,8 @@ inline const bool Solver::propXorClause(Watched* &i, Watched* &j, Watched *end, if (assigns[c[0].var()].isUndef()) { c[0] = c[0].unsign()^final; - uncheckedEnqueue(c[0], offset); + if (full) uncheckedEnqueue(c[0], PropBy(offset)); + else uncheckedEnqueueLight(c[0]); } else if (!final) { confl = PropBy(offset); qhead = trail.size(); @@ -1665,6 +1822,7 @@ inline const bool Solver::propXorClause(Watched* &i, Watched* &j, Watched *end, Basically, it goes through the watchlists recursively, and calls the appropirate propagaton function */ +template PropBy Solver::propagate(const bool update) { PropBy confl; @@ -1678,11 +1836,8 @@ PropBy Solver::propagate(const bool update) Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. vec& ws = watches[p.toInt()]; __builtin_prefetch(ws.getData(), 1, 0); - Watched *i, *j; + Watched *i, *j, *i2; num_props += ws.size()/2 + 2; - if (qhead < trail.size()) { - __builtin_prefetch(watches[trail[qhead].toInt()].getData(), 1, 1); - } #ifdef VERBOSE_DEBUG cout << "Propagating lit " << p << endl; @@ -1690,8 +1845,9 @@ PropBy Solver::propagate(const bool update) #endif i = j = ws.getData(); + i2 = i+1; Watched *end = ws.getDataEnd(); - for (; i != end; i++) { + for (; i != end; i++, i2++) { #ifdef VERBOSE_DEBUG cout << "end-i: " << end-i << endl; cout << "end-j: " << end-j << endl; @@ -1701,19 +1857,26 @@ PropBy Solver::propagate(const bool update) << " as i of prop: " << *clauseAllocator.getPointer(i->getNormOffset()) << std::endl; #endif + + if (i2 != end && i2->isClause() && !value(i2->getBlockedLit()).getBool()) { + __builtin_prefetch(clauseAllocator.getPointer(i2->getNormOffset()), 0, 0); + } + if (i->isBinary()) { - if (!propBinaryClause(i, j, end, p, confl)) break; + *j++ = *i; + if (!propBinaryClause(i, end, p, confl)) break; else continue; } //end BINARY if (i->isTriClause()) { - if (!propTriClause(i, j, end, p, confl)) break; + *j++ = *i; + if (!propTriClause(i, end, p, confl)) break; else continue; } //end TRICLAUSE if (i->isClause()) { num_props += 4; - if (!propNormalClause(i, j, end, p, confl, update)) break; + if (!propNormalClause(i, j, end, p, confl, update)) break; else { #ifdef VERBOSE_DEBUG std::cout << "clause num " << i->getNormOffset() << " after propNorm: " << *clauseAllocator.getPointer(i->getNormOffset()) << std::endl; @@ -1724,14 +1887,17 @@ PropBy Solver::propagate(const bool update) if (i->isXorClause()) { num_props += 10; - if (!propXorClause(i, j, end, p, confl)) break; + if (!propXorClause(i, j, end, p, confl)) break; else continue; } //end XORCLAUSE } if (i != end) { i++; //copy remaining watches - memmove(j, i, sizeof(Watched)*(end-i)); + for(Watched *ii = i, *jj = j; ii != end; ii++) { + *jj++ = *ii; + } + //memmove(j, i, sizeof(Watched)*(end-i)); } assert(i >= j); ws.shrink_(i-j); @@ -1745,6 +1911,8 @@ PropBy Solver::propagate(const bool update) return confl; } +template PropBy Solver::propagate (const bool update); +template PropBy Solver::propagate (const bool update); /** @brief Only propagates binary clauses @@ -1760,24 +1928,35 @@ PropBy Solver::propagateBin(vec& uselessBin) while (qhead < trail.size()) { Lit p = trail[qhead++]; - uint32_t lev = binPropData[p.var()].lev + 1; - - Lit lev2Ancestor; - if (lev == 2) lev2Ancestor = p; - else if (lev < 1) lev2Ancestor = lit_Undef; - else binPropData[p.var()].lev2Ancestor; + //setting up binPropData + uint32_t lev = binPropData[p.var()].lev; + Lit lev1Ancestor; + switch (lev) { + case 0 : + lev1Ancestor = lit_Undef; + break; + case 1: + lev1Ancestor = p; + break; + default: + lev1Ancestor = binPropData[p.var()].lev1Ancestor; + } + lev++; const bool learntLeadHere = binPropData[p.var()].learntLeadHere; + bool& hasChildren = binPropData[p.var()].hasChildren; + hasChildren = false; //std::cout << "lev: " << lev << " ~p: " << ~p << std::endl; const vec & ws = watches[p.toInt()]; propagations += ws.size()/2 + 2; for(const Watched *k = ws.getData(), *end = ws.getDataEnd(); k != end; k++) { + hasChildren = true; if (!k->isBinary()) continue; //std::cout << (~p) << ", " << k->getOtherLit() << " learnt: " << k->getLearnt() << std::endl; lbool val = value(k->getOtherLit()); if (val.isUndef()) { - uncheckedEnqueueLight2(k->getOtherLit(), lev, lev2Ancestor, learntLeadHere || k->getLearnt()); + uncheckedEnqueueLight2(k->getOtherLit(), lev, lev1Ancestor, learntLeadHere || k->getLearnt()); } else if (val == l_False) { return PropBy(p); } else { @@ -1786,10 +1965,10 @@ PropBy Solver::propagateBin(vec& uselessBin) if (lev > 1 && level[lit2.var()] != 0 && binPropData[lit2.var()].lev == 1 - && binPropData[lit2.var()].lev2Ancestor != lev2Ancestor) { - //Was propagated at level 1, and again here, this binary clause is useless + && lev1Ancestor != lit2) { + //Was propagated at level 1, and again here, original level 1 binary clause is useless binPropData[lit2.var()].lev = lev; - binPropData[lit2.var()].lev2Ancestor = lev2Ancestor; + binPropData[lit2.var()].lev1Ancestor = lev1Ancestor; binPropData[lit2.var()].learntLeadHere = learntLeadHere || k->getLearnt(); uselessBin.push(lit2); } @@ -1802,9 +1981,12 @@ PropBy Solver::propagateBin(vec& uselessBin) } /** -@brief Only propagates binary clauses +@brief Only propagates non-learnt binary clauses This is used in special algorithms outside the main Solver class +Beware, it MUST have the watchlist sorted to work properly: will "break;" on +learnt binary or any non-binary or clause in watchlist (example sort: +Subsumer::BinSorter2 ) */ PropBy Solver::propagateNonLearntBin() { @@ -1907,16 +2089,6 @@ inline const uint32_t Solver::calcNBLevels(const T& ps) | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked | clauses are clauses that are reason to some assignment. Binary clauses are never removed. |________________________________________________________________________________________________@*/ -bool reduceDB_ltMiniSat::operator () (const Clause* x, const Clause* y) { - const uint32_t xsize = x->size(); - const uint32_t ysize = y->size(); - - assert(xsize > 2 && ysize > 2); - if (x->getMiniSatAct() == y->getMiniSatAct()) - return xsize > ysize; - else return x->getMiniSatAct() < y->getMiniSatAct(); -} - bool reduceDB_ltGlucose::operator () (const Clause* x, const Clause* y) { const uint32_t xsize = x->size(); const uint32_t ysize = y->size(); @@ -1938,10 +2110,7 @@ void Solver::reduceDB() uint32_t i, j; nbReduceDB++; - if (lastSelectedRestartType == dynamic_restart) - std::sort(learnts.getData(), learnts.getDataEnd(), reduceDB_ltGlucose()); - else - std::sort(learnts.getData(), learnts.getDataEnd(), reduceDB_ltMiniSat()); + std::sort(learnts.getData(), learnts.getDataEnd(), reduceDB_ltGlucose()); #ifdef VERBOSE_DEBUG std::cout << "Cleaning clauses" << std::endl; @@ -1953,18 +2122,19 @@ void Solver::reduceDB() #endif - const uint32_t removeNum = (double)learnts.size() * (double)RATIOREMOVECLAUSES; + uint32_t removeNum = (double)learnts.size() * (double)RATIOREMOVECLAUSES; uint32_t totalNumRemoved = 0; uint32_t totalNumNonRemoved = 0; uint64_t totalGlueOfRemoved = 0; uint64_t totalSizeOfRemoved = 0; uint64_t totalGlueOfNonRemoved = 0; uint64_t totalSizeOfNonRemoved = 0; - for (i = j = 0; i != removeNum; i++){ - if (i+1 < removeNum) __builtin_prefetch(learnts[i+1], 0, 0); + uint32_t numThreeLongLearnt = 0; + for (i = j = 0; i < std::min(removeNum, learnts.size()); i++){ + if (i+1 < learnts.size()) __builtin_prefetch(learnts[i+1], 0, 0); assert(learnts[i]->size() > 2); if (!locked(*learnts[i]) - && (lastSelectedRestartType == static_restart || learnts[i]->getGlue() > 2) + && learnts[i]->getGlue() > 2 && learnts[i]->size() > 3) { //we cannot update activity of 3-longs because of wathclists totalGlueOfRemoved += learnts[i]->getGlue(); @@ -1975,6 +2145,8 @@ void Solver::reduceDB() totalGlueOfNonRemoved += learnts[i]->getGlue(); totalSizeOfNonRemoved += learnts[i]->size(); totalNumNonRemoved++; + numThreeLongLearnt += (learnts[i]->size()==3); + removeNum++; learnts[j++] = learnts[i]; } } @@ -1982,6 +2154,7 @@ void Solver::reduceDB() totalGlueOfNonRemoved += learnts[i]->getGlue(); totalSizeOfNonRemoved += learnts[i]->size(); totalNumNonRemoved++; + numThreeLongLearnt += (learnts[i]->size()==3); learnts[j++] = learnts[i]; } learnts.shrink_(i - j); @@ -1997,6 +2170,8 @@ void Solver::reduceDB() << std::fixed << std::setw(5) << std::setprecision(2) << ((double)totalGlueOfNonRemoved/(double)totalNumNonRemoved) << " avgSize " << std::fixed << std::setw(6) << std::setprecision(2) << ((double)totalSizeOfNonRemoved/(double)totalNumNonRemoved) + << " 3-long: " + << std::setw(6) << numThreeLongLearnt << std::endl; } @@ -2021,7 +2196,7 @@ const bool Solver::simplify() testAllClauseAttach(); assert(decisionLevel() == 0); - if (!ok || !propagate().isNULL()) { + if (!ok || !propagate().isNULL()) { ok = false; return false; } @@ -2080,6 +2255,7 @@ const bool Solver::simplify() totalSimplifyTime += cpuTime() - myTime; testAllClauseAttach(); + checkNoWrongAttach(); return true; } @@ -2096,7 +2272,7 @@ clauseset is found. If all variables are decision variables, this means that the clause set is satisfiable. 'l_False' if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. */ -lbool Solver::search(const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const bool update) +lbool Solver::search(const uint64_t nof_conflicts, const uint64_t maxNumConfl, const bool update) { assert(ok); uint64_t conflictC = 0; @@ -2109,6 +2285,9 @@ lbool Solver::search(const uint64_t nof_conflicts, const uint64_t nof_conflicts_ else dynStarts++; } glueHistory.fastclear(); + agility = 0.0; + numAgilityTooHigh = 0; + lastConflAgilityTooHigh = std::numeric_limits::max(); #ifdef USE_GAUSS for (vector::iterator gauss = gauss_matrixes.begin(), end = gauss_matrixes.end(); gauss != end; gauss++) { @@ -2125,13 +2304,22 @@ lbool Solver::search(const uint64_t nof_conflicts, const uint64_t nof_conflicts_ #endif //VERBOSE_DEBUG for (;;) { assert(ok); - PropBy confl = propagate(update); + PropBy confl = propagate(update); #ifdef VERBOSE_DEBUG std::cout << "c Solver::search() has finished propagation" << std::endl; //printAllClauses(); #endif //VERBOSE_DEBUG if (!confl.isNULL()) { + /*if (conflicts % 100 == 99) { + std::cout << "dyn: " << (restartType == dynamic_restart) + << ", confl: " << std::setw(6) << conflictC + << ", rest: " << std::setw(6) << starts + << ", agility : " << std::setw(6) << std::fixed << std::setprecision(2) << agility + << ", agilityTooHigh: " << std::setw(4) << numAgilityTooHigh + << ", agilityLimit : " << std::setw(6) << std::fixed << std::setprecision(2) << conf.agilityLimit << std::endl; + }*/ + ret = handle_conflict(learnt_clause, confl, conflictC, update); if (ret != l_Nothing) return ret; } else { @@ -2147,7 +2335,7 @@ lbool Solver::search(const uint64_t nof_conflicts, const uint64_t nof_conflicts_ assert(ok); if (conf.doCacheOTFSSR && decisionLevel() == 1) saveOTFData(); - ret = new_decision(nof_conflicts, nof_conflicts_fullrestart, conflictC); + ret = new_decision(nof_conflicts, maxNumConfl, conflictC); if (ret != l_Nothing) return ret; } } @@ -2159,10 +2347,10 @@ lbool Solver::search(const uint64_t nof_conflicts, const uint64_t nof_conflicts_ @returns l_Undef if it should restart instead. l_False if it reached UNSAT (through simplification) */ -llbool Solver::new_decision(const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const uint64_t conflictC) +llbool Solver::new_decision(const uint64_t nof_conflicts, const uint64_t maxNumConfl, const uint64_t conflictC) { - if (conflicts >= nof_conflicts_fullrestart || needToInterrupt) { + if (conflicts >= maxNumConfl || needToInterrupt) { #ifdef STATS_NEEDED if (dynamic_behaviour_analysis) progress_estimate = progressEstimate(); @@ -2172,10 +2360,17 @@ llbool Solver::new_decision(const uint64_t nof_conflicts, const uint64_t nof_con } // Reached bound on number of conflicts? + if (conflictC > MIN_GLUE_RESTART/2 + && ((agility < conf.agilityLimit && lastConflAgilityTooHigh != conflictC) + /*|| (glueHistory.isvalid() && 0.6*glueHistory.getAvgDouble() > glueHistory.getAvgAllDouble())*/)) { + numAgilityTooHigh++; + lastConflAgilityTooHigh = conflictC; + } + switch (restartType) { case dynamic_restart: - if (glueHistory.isvalid() && - 0.95*glueHistory.getAvgDouble() > glueHistory.getAvgAllDouble()) { + if ((numAgilityTooHigh > MIN_GLUE_RESTART/2) + /*|| (glueHistory.isvalid() && 0.95*glueHistory.getAvgDouble() > glueHistory.getAvgAllDouble())*/) { #ifdef DEBUG_DYNAMIC_RESTART if (glueHistory.isvalid()) { @@ -2191,6 +2386,7 @@ llbool Solver::new_decision(const uint64_t nof_conflicts, const uint64_t nof_con if (dynamic_behaviour_analysis) progress_estimate = progressEstimate(); #endif + cancelUntil(0); return l_Undef; } @@ -2273,7 +2469,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, PropBy confl, uint64_t& cout << endl; #endif - int backtrack_level; + uint32_t backtrack_level; uint32_t glue; conflicts++; @@ -2286,7 +2482,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, PropBy confl, uint64_t& #ifdef RANDOM_LOOKAROUND_SEARCHSPACE avgBranchDepth.push(decisionLevel()); #endif //RANDOM_LOOKAROUND_SEARCHSPACE - if (restartType == dynamic_restart) glueHistory.push(glue); + glueHistory.push(glue); conflSizeHist.push(learnt_clause.size()); } @@ -2314,6 +2510,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, PropBy confl, uint64_t& #endif //Normal learnt } else { + bumpUIPPolCount(learnt_clause); if (learnt_clause.size() == 2) { attachBinClause(learnt_clause[0], learnt_clause[1], true); numNewBin++; @@ -2357,11 +2554,20 @@ llbool Solver::handle_conflict(vec& learnt_clause, PropBy confl, uint64_t& } varDecayActivity(); - if (update && restartType == static_restart) claDecayActivity(); return l_Nothing; } +void Solver::bumpUIPPolCount(const vec& lits) +{ + for (const Lit *l = lits.getData(), *end = lits.getDataEnd(); l != end; l++) { + uint32_t factor = 0; + if (l == lits.getData()) factor = 1; + if (l->sign()) lTPolCount[l->var()].second += factor; + else lTPolCount[l->var()].first += factor; + } +} + /** @brief After a full restart, determines which restar type to use @@ -2377,25 +2583,26 @@ const bool Solver::chooseRestartType(const uint32_t& lastFullRestart) if (relativeStart == (RESTART_TYPE_DECIDER_UNTIL-1)) { RestartType tmp; - if (conf.fixRestartType == auto_restart) + if (conf.fixRestartType == auto_restart) { tmp = restartTypeChooser->choose(); - else + } else tmp = conf.fixRestartType; if (tmp == dynamic_restart) { - glueHistory.fastclear(); - if (conf.verbosity >= 3) + if (conf.verbosity >= 1) std::cout << "c Decided on dynamic restart strategy" << std::endl; + conf.agilityLimit = 0.2; } else { if (conf.verbosity >= 1) std::cout << "c Decided on static restart strategy" << std::endl; - - if (!matrixFinder->findMatrixes()) return false; + conf.agilityLimit = 0.1; } - lastSelectedRestartType = tmp; - restartType = tmp; + if (!matrixFinder->findMatrixes()) return false; + + subRestartType = tmp; + restartType = dynamic_restart; restartTypeChooser->reset(); } } @@ -2413,7 +2620,7 @@ inline void Solver::setDefaultRestartType() conflSizeHist.clear(); conflSizeHist.initSize(1000); - lastSelectedRestartType = restartType; + subRestartType = restartType; } /** @@ -2446,9 +2653,10 @@ const lbool Solver::simplifyProblem(const uint32_t numConfls) restartType = static_restart; printRestartStat("S"); - while(status == l_Undef && conflicts-origConflicts < numConfls) { + while(status == l_Undef && conflicts-origConflicts < numConfls && needToInterrupt == false) { status = search(100, std::numeric_limits::max(), false); } + if (needToInterrupt) return l_Undef; printRestartStat("S"); if (status != l_Undef) goto end; #endif //BURST_SEARCH @@ -2457,7 +2665,10 @@ const lbool Solver::simplifyProblem(const uint32_t numConfls) if (conf.doFailedLit && !failedLitSearcher->search()) goto end; + if (needToInterrupt) return l_Undef; + if (conf.doSatELite && !subsumer->simplifyBySubsumption(false)) goto end; + if (conf.doClausVivif && !clauseVivifier->vivify()) goto end; if (conf.doSatELite && !subsumer->simplifyBySubsumption(true)) goto end; /*if (findNormalXors && xorclauses.size() > 200 && clauses.size() < MAX_CLAUSENUM_XORFIND/8) { @@ -2471,13 +2682,21 @@ const lbool Solver::simplifyProblem(const uint32_t numConfls) x.addAllXorAsNorm(); } - if (conf.doClausVivif && !clauseVivifier->vivifyClauses()) goto end; - //addSymmBreakClauses(); if (conf.doSortWatched) sortWatched(); if (conf.doCacheOTFSSR && conf.doCalcReach) calcReachability(); + //Free memory if possible + for (Var var = 0; var < nVars(); var++) { + if (value(var) != l_Undef) { + vector tmp1; + transOTFCache[Lit(var, false).toInt()].lits.swap(tmp1); + vector tmp2; + transOTFCache[Lit(var, true).toInt()].lits.swap(tmp2); + } + } + end: #ifdef BURST_SEARCH if (conf.verbosity >= 3) @@ -2491,6 +2710,8 @@ end: status = l_False; testAllClauseAttach(); + checkNoWrongAttach(); + numSimplifyRounds++; if (!ok) return l_False; return status; @@ -2503,38 +2724,35 @@ If so, we also do the things to be done if the full restart is effected. Currently, this means we try to find disconnected components and solve them with sub-solvers using class PartHandler */ -const bool Solver::checkFullRestart(uint64_t& nof_conflicts, uint64_t& nof_conflicts_fullrestart, uint32_t& lastFullRestart) +const bool Solver::fullRestart(uint32_t& lastFullRestart) { - if (nof_conflicts_fullrestart > 0 && conflicts >= nof_conflicts_fullrestart) { - #ifdef USE_GAUSS - clearGaussMatrixes(); - #endif //USE_GAUSS - nof_conflicts = conf.restart_first + (double)conf.restart_first*conf.restart_inc; - nof_conflicts_fullrestart = (double)nof_conflicts_fullrestart * FULLRESTART_MULTIPLIER_MULTIPLIER; - restartType = static_restart; - lastFullRestart = starts; - - if (conf.verbosity >= 3) - std::cout << "c Fully restarting" << std::endl; - printRestartStat("F"); - - /*if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) { - XorFinder xorFinder(this, clauses, ClauseCleaner::clauses); - if (!xorFinder.doNoPart(3, 10)) - return false; - }*/ + #ifdef USE_GAUSS + clearGaussMatrixes(); + #endif //USE_GAUSS + + restartType = static_restart; + subRestartType = static_restart; + lastFullRestart = starts; + fullStarts++; - if (conf.doPartHandler && !partHandler->handle()) + if (conf.verbosity >= 3) + std::cout << "c Fully restarting" << std::endl; + printRestartStat("F"); + + /*if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) { + XorFinder xorFinder(this, clauses, ClauseCleaner::clauses); + if (!xorFinder.doNoPart(3, 10)) return false; + }*/ - //calculateDefaultPolarities(); - if (conf.polarity_mode != polarity_auto) { - for (uint32_t i = 0; i < polarity.size(); i++) { - polarity[i] = defaultPolarity(); - } - } + if (conf.doPartHandler && !partHandler->handle()) + return false; - fullStarts++; + //calculateDefaultPolarities(); + if (conf.polarity_mode != polarity_auto) { + for (uint32_t i = 0; i < polarity.size(); i++) { + polarity[i] = defaultPolarity(); + } } return true; @@ -2560,7 +2778,7 @@ void Solver::performStepsBeforeSolve() if (conf.doReplace && !varReplacer->performReplace()) return; if (conf.doClausVivif && !conf.libraryUsage - && !clauseVivifier->vivifyClauses()) return; + && !clauseVivifier->vivify()) return; bool saveDoHyperBin = conf.doHyperBinRes; conf.doHyperBinRes = false; @@ -2643,8 +2861,10 @@ polarities, and start the loop. Finally, we either report UNSAT or extend the found solution with all the intermediary simplifications (e.g. variable elimination, etc.) and output the solution. */ -lbool Solver::solve(const vec& assumps) +const lbool Solver::solve(const vec& assumps, const int _numThreads , const int _threadNum) { + numThreads = _numThreads; + threadNum = _threadNum; #ifdef VERBOSE_DEBUG std::cout << "Solver::solve() called" << std::endl; #endif @@ -2659,7 +2879,6 @@ lbool Solver::solve(const vec& assumps) assumps.copyTo(assumptions); initialiseSolver(); uint64_t nof_conflicts = conf.restart_first; //Geometric restart policy, start with this many - uint64_t nof_conflicts_fullrestart = conf.restart_first * FULLRESTART_MULTIPLIER + conflicts; //at this point, do a full restart uint32_t lastFullRestart = starts; //last time a full restart was made was at this number of restarts lbool status = l_Undef; //Current status uint64_t nextSimplify = conf.restart_first * conf.simpStartMult + conflicts; //Do simplifyProblem() at this number of conflicts @@ -2692,7 +2911,14 @@ lbool Solver::solve(const vec& assumps) lastConflPrint = conflicts; nextSimplify = std::min((uint64_t)((double)conflicts * conf.simpStartMMult), conflicts + MAX_CONFL_BETWEEN_SIMPLIFY); if (status != l_Undef) break; + + if ((numSimplifyRounds == 1 || numSimplifyRounds % 5 == 3)) { + if (!fullRestart(lastFullRestart)) return l_False; + nof_conflicts = conf.restart_first; + } + if (numSimplifyRounds % 3 == 0) nof_conflicts = conf.restart_first; } + if (!chooseRestartType(lastFullRestart)) return l_False; #ifdef STATS_NEEDED if (dynamic_behaviour_analysis) { @@ -2701,18 +2927,14 @@ lbool Solver::solve(const vec& assumps) } #endif - status = search(nof_conflicts, std::min(nof_conflicts_fullrestart, nextSimplify)); + status = search(nof_conflicts, nextSimplify); if (needToInterrupt) { cancelUntil(0); return l_Undef; } + if (status != l_Undef) break; nof_conflicts = (double)nof_conflicts * conf.restart_inc; - if (status != l_Undef) break; - if (!checkFullRestart(nof_conflicts, nof_conflicts_fullrestart , lastFullRestart)) - return l_False; - if (!chooseRestartType(lastFullRestart)) - return l_False; } printEndSearchStat(); @@ -2819,9 +3041,9 @@ void Solver::handleSATSolution() std::cout << "Solution extending finished. Enqueuing results" << std::endl; #endif 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)); + if (assigns[var] == l_Undef && s.model[var] != l_Undef) uncheckedEnqueueExtend(Lit(var, s.model[var] == l_False)); } - ok = (propagate().isNULL()); + ok = (propagate().isNULL()); release_assert(ok && "c ERROR! Extension of model failed!"); } checkSolution(); diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 97d291a..532fd0e 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -50,6 +50,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "GaussianConfig.h" #include "ClauseAllocator.h" #include "SolverConf.h" +#include "TransCache.h" #define release_assert(a) \ do { \ @@ -60,6 +61,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA } \ } while (0) +#ifndef __GNUC__ +#define __builtin_prefetch(a,b,c) +#endif //__GNUC__ + class Gaussian; class MatrixFinder; class Conglomerate; @@ -78,12 +83,14 @@ class SCCFinder; class ClauseVivifier; class SharedData; class DataSync; +class BothCache; namespace BEEV { class CryptoMinisat; } + #ifdef VERBOSE_DEBUG #define DEBUG_UNCHECKEDENQUEUE_LEVEL0 using std::cout; @@ -93,14 +100,23 @@ using std::endl; //================================================================================================= // Solver -- the main class: -struct reduceDB_ltMiniSat +struct reduceDB_ltGlucose { bool operator () (const Clause* x, const Clause* y); }; -struct reduceDB_ltGlucose +struct UIPNegPosDist { - bool operator () (const Clause* x, const Clause* y); + int64_t dist; + Var var; +}; + +struct NegPosSorter +{ + const bool operator() (const UIPNegPosDist& a, const UIPNegPosDist& b) const + { + return (a.dist < b.dist); + } }; /** @@ -124,7 +140,7 @@ public: // Constructor/Destructor: // - Solver(const SolverConf& conf = SolverConf(), const GaussConf& _gaussconfig = GaussConf(), SharedData* sharedUnitData = NULL); + Solver(const SolverConf& conf = SolverConf(), const GaussConf& _gaussconfig = GaussConf(), SharedData* sharedData = NULL); ~Solver(); // Problem specification: @@ -133,17 +149,15 @@ public: template bool addClause (T& ps, const uint32_t group = 0, const char* group_name = NULL); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! template - bool addLearntClause(T& ps, const uint32_t group = 0, const char* group_name = NULL, const uint32_t glue = 10, const float miniSatActivity = 10.0); + bool addLearntClause(T& ps, const uint32_t group = 0, const char* group_name = NULL, const uint32_t glue = 10); template bool addXorClause (T& ps, bool xorEqualFalse, const uint32_t group = 0, const char* group_name = NULL); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! // Solving: // - lbool solve (const vec& assumps); ///& assumps, const int numThreads = 1, const int threadNum = 0); /// model; /// conflict; ///& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses const vec& get_learnts() const; //Get all learnt clauses that are >1 long const vector get_unitary_learnts() const; //return the set of unitary learnt clauses @@ -190,8 +198,11 @@ public: const uint32_t get_sum_gauss_unit_truths() const; #endif //USE_GAUSS + void syncData(); + void finishAddingVars(); + //Printing statistics - void printStats(); + void printStats(const int numThreads = 1); const uint32_t getNumElimSubsume() const; /// gauss_matrixes; #ifdef USE_GAUSS @@ -277,6 +310,8 @@ protected: uint64_t moreRecurMinLDo; /// learnts; ///< List of learnt clauses. uint32_t numBins; vec freeLater; ///< xor clauses that need to be freed later (this is needed due to Gauss) \todo Get rid of this - float cla_inc; ///< Amount to bump learnt clause oldActivity with vec > watches; ///< 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec assigns; ///< The current assignments vector decision_var; ///< Declares if a variable is eligible for selection in the decision heuristic. vec trail; ///< Assignment stack; stores all assigments made in the order they were made. vec trail_lim; ///< Separator indices for different decision levels in 'trail'. vec reason; ///< 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. - vec level; ///< 'level[var]' contains the level at which the assignment was made. + vec level; ///< 'level[var]' contains the level at which the assignment was made. vec binPropData; uint32_t qhead; ///< Head of queue (as index into the trail) Lit failBinLit; ///< Used to store which watches[~lit] we were looking through when conflict occured @@ -331,6 +365,9 @@ protected: Heap order_heap; ///< A priority queue of variables ordered with respect to the variable activity. All variables here MUST be decision variables. If you changed the decision variables, you MUST filter this vec activity; ///< A heuristic measurement of the activity of a variable. uint32_t var_inc; ///< Amount to bump next variable with. + vector > lTPolCount; + void bumpUIPPolCount(const vec& lit); + vector negPosDist; ///////////////// // Learnt clause cleaning @@ -352,6 +389,12 @@ protected: bqueue glueHistory; ///< Set of last decision levels in (glue of) conflict clauses. Used for dynamic restarting vec unWindGlue; + // For agility-based restarts + void increaseAgility(const bool flipped); + double agility; + uint32_t numAgilityTooHigh; + uint64_t lastConflAgilityTooHigh; + // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is // used, exept 'seen' wich is used in several places. // @@ -362,15 +405,6 @@ protected: //////////// // Transitive on-the-fly self-subsuming resolution /////////// - class TransCache { - public: - TransCache() : - conflictLastUpdated(std::numeric_limits::max()) - {}; - - vector lits; - uint64_t conflictLastUpdated; - }; class LitReachData { public: LitReachData() : @@ -390,6 +424,7 @@ protected: void saveOTFData(); vectorlitReachable; void calcReachability(); + const bool cacheContainsBinCl(const Lit lit1, const Lit lit2, const bool learnt) const; //////////// //Logging @@ -406,7 +441,8 @@ protected: //////////////// Lit pickBranchLit (); // Return the next decision variable. void newDecisionLevel (); // Begins a new decision level. - void uncheckedEnqueue (const Lit p, const PropBy& from = PropBy()); // Enqueue a literal. Assumes value of literal is undefined. + void uncheckedEnqueue (const Lit p, const PropBy from = PropBy()); // Enqueue a literal. Assumes value of literal is undefined. + void uncheckedEnqueueExtend (const Lit p, const PropBy& from = PropBy()); void uncheckedEnqueueLight (const Lit p); void uncheckedEnqueueLight2(const Lit p, const uint32_t binPropDatael, const Lit lev2Ancestor, const bool learntLeadHere); PropBy propagateBin(vec& uselessBin); @@ -414,10 +450,16 @@ protected: bool multiLevelProp; const bool propagateBinExcept(const Lit exceptLit); const bool propagateBinOneLevel(); - PropBy propagate(const bool update = true); // Perform unit propagation. Returns possibly conflicting clause. - const bool propTriClause (Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl); - const bool propBinaryClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl); + template + PropBy propagate(const bool update = true); // Perform unit propagation. Returns possibly conflicting clause. + template + const bool propTriClause (Watched* i, Watched *end, const Lit p, PropBy& confl); + template + const bool propBinaryClause(Watched* i, Watched *end, const Lit p, PropBy& confl); + vec popularity; + template const bool propNormalClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl, const bool update); + template const bool propXorClause (Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl); void sortWatched(); @@ -426,7 +468,7 @@ protected: /////////////// void cancelUntil (int level); // Backtrack until a certain level. void cancelUntilLight(); - Clause* analyze (PropBy confl, vec& out_learnt, int& out_btlevel, uint32_t &nblevels, const bool update); + Clause* analyze (PropBy confl, vec& out_learnt, uint32_t& out_btlevel, uint32_t &nblevels, const bool update); void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. @@ -434,24 +476,28 @@ protected: ///////////////// // Searching ///////////////// - lbool search (const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const bool update = true); // Search for a given number of conflicts. + lbool search (const uint64_t nof_conflicts, const uint64_t maxNumConfl, const bool update = true); // Search for a given number of conflicts. llbool handle_conflict (vec& learnt_clause, PropBy confl, uint64_t& conflictC, const bool update);// Handles the conflict clause - llbool new_decision (const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const uint64_t conflictC); // Handles the case when all propagations have been made, and now a decision must be made + llbool new_decision (const uint64_t nof_conflicts, const uint64_t maxNumConfl, const uint64_t conflictC); // Handles the case when all propagations have been made, and now a decision must be made + + /////////////// + // Solution handling + /////////////// + void handleSATSolution(); /// const bool addClauseHelper(T& ps, const uint32_t group, const char* group_name); template - Clause* addClauseInt(T& ps, uint32_t group, const bool learnt = false, const uint32_t glue = 10, const float miniSatActivity = 10.0, const bool inOriginalInput = false); + Clause* addClauseInt(T& ps, uint32_t group, const bool learnt = false, const uint32_t glue = 10, const bool inOriginalInput = false, const bool attach = true); template XorClause* addXorClauseInt(T& ps, bool xorEqualFalse, const uint32_t group, const bool learnt = false); void attachBinClause(const Lit lit1, const Lit lit2, const bool learnt); @@ -477,8 +523,8 @@ protected: // Misc: // - uint32_t decisionLevel () const; // Gives the current decisionlevel. - uint32_t abstractLevel (const Var x) const; // Used to represent an abstraction of sets of decision levels. + const uint32_t decisionLevel () const; // Gives the current decisionlevel. + const uint32_t abstractLevel (const Var x) const; // Used to represent an abstraction of sets of decision levels. ///////////////////////// //Classes that must be friends, since they accomplish things on our datastructures @@ -506,6 +552,7 @@ protected: friend class SCCFinder; friend class ClauseVivifier; friend class DataSync; + friend class BothCache; Conglomerate* conglomerate; VarReplacer* varReplacer; ClauseCleaner* clauseCleaner; @@ -523,9 +570,9 @@ protected: ///////////////////////// const bool chooseRestartType(const uint32_t& lastFullRestart); void setDefaultRestartType(); - const bool checkFullRestart(uint64_t& nof_conflicts, uint64_t& nof_conflicts_fullrestart, uint32_t& lastFullRestart); + const bool fullRestart(uint32_t& lastFullRestart); RestartType restartType; ///& cs, vec& votes) const; void setPolarity(Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. vector polarity; // The preferred polarity of each variable. - #ifdef USE_OLD_POLARITIES - vector oldPolarity; // The polarity before the last setting. Good for unsetting polairties that have been changed since the last conflict - #endif //USE_OLD_POLARITIES }; //================================================================================================= // Implementation of inline methods: +inline const uint32_t Solver::getVerbosity() const +{ + return conf.verbosity; +} + +inline void Solver::setNeedToInterrupt(const bool value) +{ + needToInterrupt = value; +} + +inline const bool Solver::getNeedToInterrupt() const +{ + return needToInterrupt; +} + +inline const bool Solver::getNeedToDumpLearnts() const +{ + return conf.needToDumpLearnts; +} + +inline const bool Solver::getNeedToDumpOrig() const +{ + return conf.needToDumpOrig; +} inline void Solver::insertVarOrder(Var x) { @@ -620,21 +690,6 @@ inline void Solver::varBumpActivity(Var v) order_heap.decrease(v); } -inline void Solver::claBumpActivity (Clause& c) -{ - if ( (c.getMiniSatAct() += cla_inc) > 1e20 ) { - // Rescale: - for (uint32_t i = 0; i < learnts.size(); i++) - learnts[i]->getMiniSatAct() *= 1e-17; - cla_inc *= 1e-20; - } -} - -inline void Solver::claDecayActivity() -{ - //cla_inc *= clause_decay; -} - inline bool Solver::locked(const Clause& c) const { if (c.size() <= 3) return true; //we don't know in this case :I @@ -654,43 +709,43 @@ inline void Solver::newDecisionLevel() return trail.size() - trail_lim[level-1] - 1; return trail_lim[level] - trail_lim[level-1] - 1; }*/ -inline uint32_t Solver::decisionLevel () const +inline const uint32_t Solver::decisionLevel () const { return trail_lim.size(); } -inline uint32_t Solver::abstractLevel (const Var x) const +inline const uint32_t Solver::abstractLevel (const Var x) const { return 1 << (level[x] & 31); } -inline lbool Solver::value (const Var x) const +inline const lbool Solver::value (const Var x) const { return assigns[x]; } -inline lbool Solver::value (const Lit p) const +inline const lbool Solver::value (const Lit p) const { return assigns[p.var()] ^ p.sign(); } -inline lbool Solver::modelValue (const Lit p) const +inline const lbool Solver::modelValue (const Lit p) const { return model[p.var()] ^ p.sign(); } -inline uint32_t Solver::nAssigns () const +inline const uint32_t Solver::nAssigns () const { return trail.size(); } -inline uint32_t Solver::nClauses () const +inline const uint32_t Solver::nClauses () const { return clauses.size() + xorclauses.size(); } -inline uint32_t Solver::nLiterals () const +inline const uint32_t Solver::nLiterals () const { return clauses_literals + learnts_literals; } -inline uint32_t Solver::nLearnts () const +inline const uint32_t Solver::nLearnts () const { return learnts.size(); } -inline uint32_t Solver::nVars () const +inline const uint32_t Solver::nVars () const { return assigns.size(); } @@ -705,12 +760,12 @@ inline void Solver::setDecisionVar(Var v, bool b) insertVarOrder(v); } } -inline lbool Solver::solve () +inline const lbool Solver::solve (const int _numThreads, const int _threadNum) { vec tmp; - return solve(tmp); + return solve(tmp, numThreads, threadNum); } -inline bool Solver::okay () const +inline const bool Solver::okay () const { return ok; } @@ -725,14 +780,14 @@ inline void Solver::needProofGraph() dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate proof graphs during solving logger.proof_graph_on = true; } -inline void Solver::setVariableName(const Var var, const char* name) +inline void Solver::setVariableName(const Var var, const std::string& name) { while (var >= nVars()) newVar(); if (dynamic_behaviour_analysis) logger.set_variable_name(var, name); } // Sets the varible 'var'-s name to 'name' in the logger #else -inline void Solver::setVariableName(const Var var, const char* name) +inline void Solver::setVariableName(const Var var, const std::string& name) {} #endif @@ -822,6 +877,10 @@ inline void Solver::testAllClauseAttach() const { return; } +inline void Solver::checkNoWrongAttach() const +{ + return; +} inline void Solver::findAllAttach() const { return; @@ -830,21 +889,31 @@ inline void Solver::findAllAttach() const inline void Solver::uncheckedEnqueueLight(const Lit p) { + __builtin_prefetch(watches.getData()+p.toInt(), 1, 0); assert(assigns[p.var()] == l_Undef); assigns [p.var()] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient trail.push(p); + __builtin_prefetch(watches[p.toInt()].getData(), 1, 0); } inline void Solver::uncheckedEnqueueLight2(const Lit p, const uint32_t binSubLevel, const Lit lev2Ancestor, const bool learntLeadHere) { + __builtin_prefetch(watches.getData()+p.toInt(), 1, 0); assert(assigns[p.var()] == l_Undef); assigns [p.var()] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient trail.push(p); binPropData[p.var()].lev = binSubLevel; - binPropData[p.var()].lev2Ancestor = lev2Ancestor; + binPropData[p.var()].lev1Ancestor = lev2Ancestor; binPropData[p.var()].learntLeadHere = learntLeadHere; + __builtin_prefetch(watches[p.toInt()].getData(), 1, 0); +} + +inline void Solver::increaseAgility(const bool flipped) +{ + agility *= conf.agilityG; + if (flipped) agility += 1.0 - conf.agilityG; } //================================================================================================= diff --git a/src/sat/cryptominisat2/SolverConf.cpp b/src/sat/cryptominisat2/SolverConf.cpp index b4d7eaf..b2eed05 100644 --- a/src/sat/cryptominisat2/SolverConf.cpp +++ b/src/sat/cryptominisat2/SolverConf.cpp @@ -20,10 +20,11 @@ along with this program. If not, see . SolverConf::SolverConf() : random_var_freq(0.02) - , clause_decay (1 / 0.999) , restart_first(100) , restart_inc(1.5) , learntsize_factor((double)1/(double)3) + , agilityG(0.9999) + , agilityLimit(0.1) , expensive_ccmin (true) , polarity_mode (polarity_auto) @@ -65,7 +66,11 @@ SolverConf::SolverConf() : , doMaxGlueDel (false) , doPrintAvgBranch (false) , doCacheOTFSSR (true) + , doCacheNLBins (true) , doExtendedSCC (true) + , doGateFind (true) + , doAlwaysFMinim (true) + , doER (true) , doCalcReach (true) , maxRestarts (std::numeric_limits::max()) diff --git a/src/sat/cryptominisat2/SolverConf.h b/src/sat/cryptominisat2/SolverConf.h index 2abf702..81df856 100644 --- a/src/sat/cryptominisat2/SolverConf.h +++ b/src/sat/cryptominisat2/SolverConf.h @@ -27,11 +27,11 @@ class SolverConf SolverConf(); double random_var_freq; /// 0) assert(cl[i-1].var() != cl[i].var()); + } + } +} +#endif //DEBUG_ATTACH_FULL + void Solver::printAllClauses() { for (uint32_t i = 0; i < clauses.size(); i++) { @@ -250,4 +264,4 @@ void Solver::printAllClauses() } } -} \ No newline at end of file +} diff --git a/src/sat/cryptominisat2/SolverMisc.cpp b/src/sat/cryptominisat2/SolverMisc.cpp index a42b37e..bf7320b 100644 --- a/src/sat/cryptominisat2/SolverMisc.cpp +++ b/src/sat/cryptominisat2/SolverMisc.cpp @@ -86,10 +86,7 @@ void Solver::dumpSortedLearnts(const std::string& fileName, const uint32_t maxSi fprintf(outfile, "c \nc --------------------\n"); fprintf(outfile, "c clauses from learnts\n"); fprintf(outfile, "c --------------------\n"); - if (lastSelectedRestartType == dynamic_restart) - std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose()); - else - std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat()); + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose()); for (int i = learnts.size()-1; i >= 0 ; i--) { if (learnts[i]->size() <= maxSize) { learnts[i]->print(outfile); @@ -145,7 +142,7 @@ void Solver::dumpBinClauses(const bool alsoLearnt, const bool alsoNonLearnt, FIL Lit lit = ~Lit::toLit(wsLit); const vec& ws = *it; for (const Watched *it2 = ws.getData(), *end2 = ws.getDataEnd(); it2 != end2; it2++) { - if (it2->isBinary() && lit.toInt() < it2->getOtherLit().toInt()) { + if (it2->isBinary() && lit < it2->getOtherLit()) { bool toDump = false; if (it2->getLearnt() && alsoLearnt) toDump = true; if (!it2->getLearnt() && alsoNonLearnt) toDump = true; @@ -318,10 +315,7 @@ const vec& Solver::get_learnts() const const vec& Solver::get_sorted_learnts() { - if (lastSelectedRestartType == dynamic_restart) - std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose()); - else - std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat()); + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose()); return learnts; } @@ -393,6 +387,9 @@ void Solver::printStatHeader() const << std::setw(space) << "Learnts" << std::setw(space) << "ClLits" << std::setw(space) << "LtLits" + << std::setw(space) << "MTavgCS" + << std::setw(space) << "LTAvgG" + //<< std::setw(space) << "STAvgG" << std::endl; } } @@ -414,16 +411,22 @@ void Solver::printRestartStat(const char* type) << std::setw(space) << clauses_literals << std::setw(space) << learnts_literals; + if (conflSizeHist.isvalid()) { + std::cout << std::setw(space) << std::fixed << std::setprecision(2) << conflSizeHist.getAvgDouble(); + } else { + std::cout << std::setw(space) << "no data"; + } + if (glueHistory.getTotalNumeElems() > 0) { std::cout << std::setw(space) << std::fixed << std::setprecision(2) << glueHistory.getAvgAllDouble(); } else { std::cout << std::setw(space) << "no data"; } - if (glueHistory.isvalid()) { + /*if (glueHistory.isvalid()) { std::cout << std::setw(space) << std::fixed << std::setprecision(2) << glueHistory.getAvgDouble(); } else { std::cout << std::setw(space) << "no data"; - } + }*/ #ifdef RANDOM_LOOKAROUND_SEARCHSPACE if (conf.doPrintAvgBranch) { @@ -561,7 +564,8 @@ void Solver::addSymmBreakClauses() } - DimacsParser parser(this, false, false, false, true); + /* + DimacsParser parser(this, false, false, false); #ifdef DISABLE_ZLIB FILE * in = fopen("output", "rb"); @@ -574,6 +578,7 @@ void Solver::addSymmBreakClauses() #else gzclose(in); #endif // DISABLE_ZLIB + */ std::cout << "c Finished saucy, time: " << (cpuTime() - myTime) << std::endl; } @@ -620,17 +625,11 @@ void Solver::printStatsLine(std::string left, T value, std::string extra) Prints all sorts of statistics, like number of restarts, time spent in SatELite-type simplification, number of unit claues found, etc. */ -void Solver::printStats() +void Solver::printStats(const int numThreads) { double cpu_time = cpuTime(); uint64_t mem_used = memUsed(); -#ifdef _OPENMP - const int numThreads = omp_get_num_threads(); -#else - const int numThreads = 1; -#endif - if (numThreads > 1) { std::cout << "c Following stats are for *FIRST FINISHED THREAD ONLY*" << std::endl; #if !defined(_MSC_VER) && !defined(RUSAGE_THREAD) @@ -668,8 +667,8 @@ void Solver::printStats() printStatsLine("c bin xor find time", getTotalTimeSCC()); //OTF clause improvement stats - printStatsLine("c OTF clause improved", improvedClauseNo, (double)improvedClauseNo/(double)conflicts, "clauses/conflict"); - printStatsLine("c OTF impr. size diff", improvedClauseSize, (double)improvedClauseSize/(double)improvedClauseNo, " lits/clause"); + printStatsLine("c OTF clause subsumed", improvedClauseNo, (double)improvedClauseNo/(double)conflicts, "clauses/conflict"); + printStatsLine("c OTF subs. size diff", improvedClauseSize, (double)improvedClauseSize/(double)improvedClauseNo, " lits/clause"); //Clause-shrinking through watchlists printStatsLine("c OTF cl watch-shrink", numShrinkedClause, (double)numShrinkedClause/(double)conflicts, "clauses/conflict"); @@ -677,12 +676,17 @@ void Solver::printStats() printStatsLine("c tried to recurMin cls", moreRecurMinLDo, (double)moreRecurMinLDo/(double)conflicts*100.0, " % of conflicts"); printStatsLine("c updated cache", updateTransCache, updateTransCache/(double)moreRecurMinLDo, " lits/tried recurMin"); + printStatsLine("c OTF Gate-Rem cl", OTFGateRemSucc, (double)OTFGateRemSucc/(double)conflicts, "clauses/conflict"); + printStatsLine("c OTF Gate-rem lits", OTFGateRemLits, (double)OTFGateRemLits/(double)OTFGateRemSucc, "lits/confl"); + //Multi-threading if (numThreads > 1) { printStatsLine("c unit cls received", dataSync->getRecvUnitData(), (double)dataSync->getRecvUnitData()/(double)get_unitary_learnts_num()*100.0, "% of units"); printStatsLine("c unit cls sent", dataSync->getSentUnitData(), (double)dataSync->getSentUnitData()/(double)get_unitary_learnts_num()*100.0, "% of units"); printStatsLine("c bin cls received", dataSync->getRecvBinData()); printStatsLine("c bin cls sent", dataSync->getSentBinData()); + printStatsLine("c tri cls recevied", dataSync->getRecvTriData()); + printStatsLine("c tri cls sent", dataSync->getSentTriData()); } #ifdef USE_GAUSS @@ -718,3 +722,13 @@ void Solver::printStats() printStatsLine("c CPU time", cpu_time, " s"); } } + +const bool Solver::cacheContainsBinCl(const Lit lit1, const Lit lit2, const bool learnt) const +{ + const vector& cache = transOTFCache[(~lit1).toInt()].lits; + for (vector::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) { + if (it->getLit() == lit2 && (!learnt || it->getOnlyNLBin())) return true; + } + + return false; +} diff --git a/src/sat/cryptominisat2/SolverTypes.h b/src/sat/cryptominisat2/SolverTypes.h index f7fc751..d1cc09e 100644 --- a/src/sat/cryptominisat2/SolverTypes.h +++ b/src/sat/cryptominisat2/SolverTypes.h @@ -23,6 +23,8 @@ Modifications for CryptoMiniSat are under GPLv3 licence. #include #include #include "constants.h" +#include +#include //================================================================================================= // Variables, literals, lifted booleans, clauses: @@ -80,6 +82,9 @@ public: bool operator < (const Lit& p) const { return x < p.x; // '<' guarantees that p, ~p are adjacent in the ordering. } + bool operator > (const Lit& p) const { + return x > p.x; + } inline void print(FILE* outfile = stdout) const { fprintf(outfile,"%s%d ", sign() ? "-" : "", var()+1); @@ -97,10 +102,12 @@ public: const Lit lit_Undef(var_Undef, false); // Useful special constants. const Lit lit_Error(var_Undef, true ); // -inline std::ostream& operator<<(std::ostream& cout, const Lit& lit) +inline std::ostream& operator<<(std::ostream& os, const Lit& lit) { - cout << (lit.sign() ? "-" : "") << (lit.var() + 1); - return cout; + std::stringstream ss; + ss << (lit.sign() ? "-" : "") << (lit.var() + 1); + os << std::setw(6) << ss.str(); + return os; } inline std::ostream& operator<<(std::ostream& cout, const vec& lits) @@ -233,8 +240,9 @@ enum { polarity_true = 0, polarity_false = 1, polarity_rnd = 3, polarity_auto = struct BinPropData { uint32_t lev; - Lit lev2Ancestor; + Lit lev1Ancestor; bool learntLeadHere; + bool hasChildren; }; diff --git a/src/sat/cryptominisat2/StateSaver.cpp b/src/sat/cryptominisat2/StateSaver.cpp index 22b7cc1..a9c9d42 100644 --- a/src/sat/cryptominisat2/StateSaver.cpp +++ b/src/sat/cryptominisat2/StateSaver.cpp @@ -16,6 +16,7 @@ along with this program. If not, see . **************************************************************************************************/ #include "StateSaver.h" +#include "PartHandler.h" StateSaver::StateSaver(Solver& _solver) : solver(_solver) @@ -45,4 +46,10 @@ void StateSaver::restore() //Finally, clear the order_heap from variables set/non-decisionned solver.order_heap.filter(Solver::VarFilter(solver)); + + for (Var var = 0; var < solver.nVars(); var++) { + if (solver.decision_var[var] + && solver.value(var) == l_Undef + && solver.partHandler->getSavedState()[var] == l_Undef) solver.insertVarOrder(var); + } } diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp index d511e7f..806fde5 100644 --- a/src/sat/cryptominisat2/Subsumer.cpp +++ b/src/sat/cryptominisat2/Subsumer.cpp @@ -20,6 +20,9 @@ Modifications for CryptoMiniSat are under GPLv3 licence. #include "OnlyNonLearntBins.h" #include "UselessBinRemover.h" #include "DataSync.h" +#include "BothCache.h" +#include +#include "PartHandler.h" #ifdef _MSC_VER #define __builtin_prefetch(a,b,c) @@ -28,10 +31,12 @@ Modifications for CryptoMiniSat are under GPLv3 licence. //#define VERBOSE_DEBUG #ifdef VERBOSE_DEBUG #define BIT_MORE_VERBOSITY +#define VERBOSE_ORGATE_REPLACE #endif //#define BIT_MORE_VERBOSITY //#define TOUCH_LESS +//#define VERBOSE_ORGATE_REPLACE #ifdef VERBOSE_DEBUG using std::cout; @@ -42,7 +47,9 @@ Subsumer::Subsumer(Solver& s): solver(s) , totalTime(0.0) , numElimed(0) - , numCalls(1) + , numERVars(0) + , finishedAddingVars(false) + , numCalls(0) , alsoLearnt(false) { }; @@ -213,8 +220,6 @@ void Subsumer::subsume0(Clause& ps) if (!ret.subsumedNonLearnt) { if (ps.getGlue() > ret.glue) ps.setGlue(ret.glue); - if (ps.getMiniSatAct() < ret.act) - ps.setMiniSatAct(ret.act); } else { solver.nbCompensateSubsumer++; ps.makeNonLearnt(); @@ -237,7 +242,6 @@ Subsumer::subsume0Happened Subsumer::subsume0Orig(const T& ps, uint32_t abs) subsume0Happened ret; ret.subsumedNonLearnt = false; ret.glue = std::numeric_limits::max(); - ret.act = std::numeric_limits< float >::min(); vec subs; findSubsumed(ps, abs, subs); @@ -250,7 +254,6 @@ Subsumer::subsume0Happened Subsumer::subsume0Orig(const T& ps, uint32_t abs) Clause* tmp = subs[i].clause; if (tmp->learnt()) { ret.glue = std::min(ret.glue, tmp->getGlue()); - ret.act = std::max(ret.act, tmp->getMiniSatAct()); } else { ret.subsumedNonLearnt = true; } @@ -259,71 +262,7 @@ Subsumer::subsume0Happened Subsumer::subsume0Orig(const T& ps, uint32_t abs) return ret; } -/** -@brief Backward-subsumption&self-subsuming resolution for binary clause sets - -Takes in a set of binary clauses: -lit1 OR lits[0] -lit1 OR lits[1] -... -and backward-subsumes clauses in the occurence lists with it, as well as -performing self-subsuming resolution using these binary clauses on clauses in -the occurrence lists. - -@param[in] lit1 As defined above -@param[in] lits The abstraction of the clause -*/ -void Subsumer::subsume0BIN(const Lit lit1, const vec& lits, const uint32_t abst) -{ - vec subs; - vec subs2; - vec subs2Lit; - - vec& cs = occur[lit1.toInt()]; - for (ClauseSimp *it = cs.getData(), *end = it + cs.size(); it != end; it++){ - if (it+1 != end) __builtin_prefetch((it+1)->clause, 0, 1); - if (it->clause == NULL) continue; - - Clause& c = *it->clause; - if ((c.getAbst() & abst) == 0) continue; - extraTimeNonExist += c.size()*2; - bool removed = false; - bool removedLit = false; - for (uint32_t i = 0; i < c.size(); i++) { - if (lits[c[i].toInt()]) { - subs.push(*it); - removed = true; - break; - } - - if (!removedLit && lits[(~c[i]).toInt()]) { - subs2.push(*it); - subs2Lit.push(c[i]); - removedLit = true; - } - } - if (removed && removedLit) { - subs2.pop(); - subs2Lit.pop(); - } - } - - for (uint32_t i = 0; i < subs.size(); i++){ - unlinkClause(subs[i]); - } - - for (uint32_t i = 0; i < subs2.size(); i++) { - strenghten(subs2[i], subs2Lit[i]); - if (!solver.ok) break; - } - - #ifdef VERBOSE_DEBUG - if (!solver.ok) { - std::cout << "solver.ok is false when returning from subsume0BIN()" << std::endl; - } - #endif //VERBOSE_DEBUG -} /** @brief Backward subsumption and self-subsuming resolution @@ -398,6 +337,7 @@ parameter is different from var_Undef. void Subsumer::unlinkClause(ClauseSimp c, const Var elim) { Clause& cl = *c.clause; + assert(!defOfOrGate[c.index]); for (uint32_t i = 0; i < cl.size(); i++) { if (elim != var_Undef) numMaxElim -= occur[cl[i].toInt()].size()/2; @@ -484,32 +424,6 @@ const bool Subsumer::cleanClause(Clause& ps) return retval; } -const bool Subsumer::cleanClause(vec& ps) const -{ - bool retval = false; - - Lit *i = ps.getData(); - Lit *j = i; - for (Lit *end = ps.getDataEnd(); i != end; i++) { - lbool val = solver.value(*i); - if (val == l_Undef) { - *j++ = *i; - continue; - } - if (val == l_False) - continue; - if (val == l_True) { - *j++ = *i; - retval = true; - continue; - } - assert(false); - } - ps.shrink(i-j); - - return retval; -} - /** @brief Removes a literal from a clause @@ -533,10 +447,16 @@ void Subsumer::strenghten(ClauseSimp& c, const Lit toRemoveLit) #ifndef TOUCH_LESS touch(toRemoveLit, c.clause->learnt()); #endif + + handleUpdatedClause(c); +} + +const bool Subsumer::handleUpdatedClause(ClauseSimp& c) +{ if (cleanClause(*c.clause)) { unlinkClause(c); c.clause = NULL; - return; + return true; } switch (c.clause->size()) { @@ -545,12 +465,12 @@ void Subsumer::strenghten(ClauseSimp& c, const Lit toRemoveLit) std::cout << "Strenghtened clause to 0-size -> UNSAT"<< std::endl; #endif //VERBOSE_DEBUG solver.ok = false; - break; + return false; case 1: { - handleSize1Clause((*c.clause)[0]); + solver.uncheckedEnqueue((*c.clause)[0]); unlinkClause(c); c.clause = NULL; - break; + return solver.ok; } case 2: { solver.attachBinClause((*c.clause)[0], (*c.clause)[1], (*c.clause).learnt()); @@ -559,11 +479,14 @@ void Subsumer::strenghten(ClauseSimp& c, const Lit toRemoveLit) clBinTouched.push_back(NewBinaryClause((*c.clause)[0], (*c.clause)[1], (*c.clause).learnt())); unlinkClause(c); c.clause = NULL; - break; + return solver.ok; } default: + if (c.clause->size() == 3) solver.dataSync->signalNewTriClause(*c.clause); cl_touched.add(c); } + + return true; } const bool Subsumer::handleClBinTouched() @@ -602,26 +525,6 @@ const bool Subsumer::handleClBinTouched() return true; } -/** -@brief Handles if a clause became 1-long (unitary) - -Either sets&propagates the value, ignores the value (if already set), -or sets solver.ok = FALSE - -@param[in] lit The single literal the clause has -*/ -inline void Subsumer::handleSize1Clause(const Lit lit) -{ - if (solver.value(lit) == l_False) { - solver.ok = false; - } else if (solver.value(lit) == l_Undef) { - solver.uncheckedEnqueue(lit); - solver.ok = solver.propagate().isNULL(); - } else { - assert(solver.value(lit) == l_True); - } -} - /** @brief Executes subsume1() recursively on all clauses @@ -638,14 +541,7 @@ const bool Subsumer::subsume0AndSubsume1() if (addedClauseLits > 1500000) clTouchedTodo /= 2; if (addedClauseLits > 3000000) clTouchedTodo /= 2; if (addedClauseLits > 10000000) clTouchedTodo /= 2; - if (alsoLearnt) { - clTouchedTodo /= 2; - /*clTouchedTodo = std::max(clTouchedTodo, (uint32_t)20000); - clTouchedTodo = std::min(clTouchedTodo, (uint32_t)5000);*/ - } else { - /*clTouchedTodo = std::max(clTouchedTodo, (uint32_t)20000); - clTouchedTodo = std::min(clTouchedTodo, (uint32_t)5000);*/ - } + if (alsoLearnt) clTouchedTodo /= 8; if (!solver.conf.doSubsume1) clTouchedTodo = 0; @@ -788,13 +684,16 @@ Increments clauseID */ ClauseSimp Subsumer::linkInClause(Clause& cl) { - ClauseSimp c(&cl, clauseID++); + ClauseSimp c(&cl, clauses.size()); clauses.push(c); + defOfOrGate.push(false); + assert(defOfOrGate.size() == clauses.size()); + for (uint32_t i = 0; i < cl.size(); i++) { occur[cl[i].toInt()].push(c); - touch(cl[i], cl.learnt()); + if (cl.getStrenghtened()) touch(cl[i], cl.learnt()); } - cl_touched.add(c); + if (cl.getStrenghtened()) cl_touched.add(c); return c; } @@ -823,16 +722,8 @@ const uint64_t Subsumer::addFromSolver(vec& cs) continue; } - ClauseSimp c(*i, clauseID++); - clauses.push(c); - Clause& cl = *c.clause; - for (uint32_t i = 0; i < cl.size(); i++) { - occur[cl[i].toInt()].push(c); - //if (cl.getStrenghtened()) touch(cl[i], cl.learnt()); - } - numLitsAdded += cl.size(); - - if (cl.getStrenghtened()) cl_touched.add(c); + linkInClause(**i); + numLitsAdded += (*i)->size(); } cs.shrink(i-j); @@ -897,6 +788,43 @@ void Subsumer::removeWrong(vec& cs) cs.shrink(i-j); } +void Subsumer::removeBinsAndTris(const Var var) +{ + uint32_t numRemovedLearnt = 0; + + Lit lit = Lit(var, false); + + numRemovedLearnt += removeBinAndTrisHelper(lit, solver.watches[(~lit).toInt()]); + numRemovedLearnt += removeBinAndTrisHelper(~lit, solver.watches[lit.toInt()]); + + solver.learnts_literals -= numRemovedLearnt*2; + solver.numBins -= numRemovedLearnt; + +} + +const uint32_t Subsumer::removeBinAndTrisHelper(const Lit lit, vec& ws) +{ + uint32_t numRemovedLearnt = 0; + + Watched* i = ws.getData(); + Watched* j = i; + for (Watched *end = ws.getDataEnd(); i != end; i++) { + if (i->isTriClause()) continue; + + if (i->isBinary()) { + assert(i->getLearnt()); + removeWBin(solver.watches[(~(i->getOtherLit())).toInt()], lit, i->getLearnt()); + numRemovedLearnt++; + continue; + } + + assert(false); + } + ws.shrink_(i - j); + + return numRemovedLearnt; +} + void Subsumer::removeWrongBinsAndAllTris() { uint32_t numRemovedHalfLearnt = 0; @@ -1003,32 +931,6 @@ const bool Subsumer::subsumeWithBinaries() return true; } -const bool Subsumer::subsWNonExitsBinsFullFull() -{ - double myTime = cpuTime(); - clauses_subsumed = 0; - literals_removed = 0; - for (vec *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++) { - if (it->size() < 2) continue; - std::sort(it->getData(), it->getDataEnd(), BinSorter2()); - } - - uint32_t oldTrailSize = solver.trail.size(); - if (!subsWNonExistBinsFull()) return false; - - if (solver.conf.verbosity >= 1) { - std::cout << "c Subs w/ non-existent bins: " << std::setw(6) << clauses_subsumed - << " l-rem: " << std::setw(6) << literals_removed - << " v-fix: " << std::setw(5) << solver.trail.size() - oldTrailSize - << " done: " << std::setw(6) << doneNum - << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << (cpuTime() - myTime) << " s" - << std::endl; - } - - totalTime += cpuTime() - myTime; - return true; -} - void Subsumer::makeNonLearntBin(const Lit lit1, const Lit lit2, const bool learnt) { assert(learnt == true); @@ -1048,12 +950,17 @@ inferred from non-existing binary clauses, and the strenghtening (through self- subsuming resolution) of clauses that could be strenghtened using non-existent binary clauses. */ -const bool Subsumer::subsWNonExistBinsFull() +const bool Subsumer::subsWNonExistBinsFill() { + double myTime = cpuTime(); + for (vec *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++) { + if (it->size() < 2) continue; + std::sort(it->getData(), it->getDataEnd(), BinSorter2()); + } + + uint32_t oldTrailSize = solver.trail.size(); uint64_t oldProps = solver.propagations; - uint64_t maxProp = MAX_BINARY_PROP*7; - toVisitAll.clear(); - toVisitAll.growTo(solver.nVars()*2, false); + uint64_t maxProp = MAX_BINARY_PROP; extraTimeNonExist = 0; OnlyNonLearntBins* onlyNonLearntBins = NULL; if (solver.clauses_literals < 10*1000*1000) { @@ -1062,22 +969,22 @@ const bool Subsumer::subsWNonExistBinsFull() solver.multiLevelProp = true; } - doneNum = 0; + doneNumNonExist = 0; uint32_t startFrom = solver.mtrand.randInt(solver.order_heap.size()); for (uint32_t i = 0; i < solver.order_heap.size(); i++) { Var var = solver.order_heap[(startFrom + i) % solver.order_heap.size()]; if (solver.propagations + extraTimeNonExist*150 > oldProps + maxProp) break; if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue; - doneNum++; + doneNumNonExist++; extraTimeNonExist += 5; Lit lit(var, true); if (onlyNonLearntBins != NULL && onlyNonLearntBins->getWatchSize(lit) == 0) goto next; - if (!subsWNonExistBins(lit, onlyNonLearntBins)) { + if (!subsWNonExistBinsFillHelper(lit, onlyNonLearntBins)) { if (!solver.ok) return false; solver.cancelUntilLight(); solver.uncheckedEnqueue(~lit); - solver.ok = solver.propagate().isNULL(); + solver.ok = solver.propagate().isNULL(); if (!solver.ok) return false; continue; } @@ -1088,11 +995,11 @@ const bool Subsumer::subsWNonExistBinsFull() if (solver.assigns[var] != l_Undef) continue; lit = ~lit; if (onlyNonLearntBins != NULL && onlyNonLearntBins->getWatchSize(lit) == 0) continue; - if (!subsWNonExistBins(lit, onlyNonLearntBins)) { + if (!subsWNonExistBinsFillHelper(lit, onlyNonLearntBins)) { if (!solver.ok) return false; solver.cancelUntilLight(); solver.uncheckedEnqueue(~lit); - solver.ok = solver.propagate().isNULL(); + solver.ok = solver.propagate().isNULL(); if (!solver.ok) return false; continue; } @@ -1101,6 +1008,16 @@ const bool Subsumer::subsWNonExistBinsFull() if (onlyNonLearntBins) delete onlyNonLearntBins; + + if (solver.conf.verbosity >= 1) { + std::cout << "c Calc non-exist non-lernt bins" + << " v-fix: " << std::setw(5) << solver.trail.size() - oldTrailSize + << " done: " << std::setw(6) << doneNumNonExist + << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << (cpuTime() - myTime) << " s" + << std::endl; + } + totalTime += cpuTime() - myTime; + return true; } @@ -1116,12 +1033,11 @@ binary clauses (this literal is the starting point in the binary graph) @param onlyNonLearntBins This class is initialised before calling this function and contains all the non-learnt binary clauses */ -const bool Subsumer::subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* onlyNonLearntBins) +const bool Subsumer::subsWNonExistBinsFillHelper(const Lit& lit, OnlyNonLearntBins* onlyNonLearntBins) { #ifdef VERBOSE_DEBUG std::cout << "subsWNonExistBins called with lit " << lit << std::endl; #endif //VERBOSE_DEBUG - toVisit.clear(); solver.newDecisionLevel(); solver.uncheckedEnqueueLight(lit); bool failed; @@ -1130,14 +1046,12 @@ const bool Subsumer::subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* onlyNo else failed = !onlyNonLearntBins->propagate(); if (failed) return false; - uint32_t abst = 0; + vector lits; assert(solver.decisionLevel() > 0); for (int sublevel = solver.trail.size()-1; sublevel > (int)solver.trail_lim[0]; sublevel--) { Lit x = solver.trail[sublevel]; - toVisit.push(x); - abst |= 1 << (x.var() & 31); - toVisitAll[x.toInt()] = true; + lits.push_back(LitExtra(x, true)); solver.assigns[x.var()] = l_Undef; } solver.assigns[solver.trail[solver.trail_lim[0]].var()] = l_Undef; @@ -1146,18 +1060,8 @@ const bool Subsumer::subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* onlyNo solver.trail_lim.shrink_(solver.trail_lim.size()); //solver.cancelUntilLight(); - if ((onlyNonLearntBins != NULL && toVisit.size() <= onlyNonLearntBins->getWatchSize(lit)) - || (!solver.multiLevelProp)) { - //This has been performed above, with subsume1Partial of binary clauses: - //this toVisit.size()<=1, there mustn't have been more than 1 binary - //clause in the watchlist, so this has been performed above. - } else { - subsume0BIN(~lit, toVisitAll, abst); - } - - for (uint32_t i = 0; i < toVisit.size(); i++) - toVisitAll[toVisit[i].toInt()] = false; - + solver.transOTFCache[(~lit).toInt()].conflictLastUpdated = solver.conflicts; + solver.transOTFCache[(~lit).toInt()].merge(lits); return solver.ok; } /** @@ -1177,7 +1081,9 @@ void Subsumer::clearAll() } clauses.clear(); cl_touched.clear(); + defOfOrGate.clear(); addedClauseLits = 0; + numLearntBinVarRemAdded = 0; } const bool Subsumer::eliminateVars() @@ -1189,7 +1095,6 @@ const bool Subsumer::eliminateVars() orderVarsForElim(init_order); // (will untouch all variables) for (bool first = true; numMaxElim > 0 && numMaxElimVars > 0; first = false) { - uint32_t vars_elimed = 0; vec order; if (first) { @@ -1212,16 +1117,14 @@ const bool Subsumer::eliminateVars() std::cout << "Order size:" << order.size() << std::endl; #endif + uint32_t oldNumElimed = numElimed; for (uint32_t i = 0; i < order.size() && numMaxElim > 0 && numMaxElimVars > 0; i++) { - if (maybeEliminate(order[i])) { - if (!solver.ok) return false; - vars_elimed++; - numMaxElimVars--; - } + if (solver.mtrand.randInt(7) != 0 && !dontElim[order[i]] && !maybeEliminate(order[i])) + return false; } - if (vars_elimed == 0) break; + if (numElimed - oldNumElimed == 0) break; - numVarsElimed += vars_elimed; + numVarsElimed += numElimed - oldNumElimed; #ifdef BIT_MORE_VERBOSITY std::cout << "c #var-elim: " << vars_elimed << std::endl; #endif @@ -1305,8 +1208,8 @@ const bool Subsumer::simplifyBySubsumption(const bool _alsoLearnt) || solver.clauses_literals > 500000000) return true; double myTime = cpuTime(); - clauseID = 0; clearAll(); + if (!alsoLearnt) numCalls++; //if (solver.xorclauses.size() < 30000 && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/10) addAllXorAsNorm(); @@ -1314,11 +1217,6 @@ const bool Subsumer::simplifyBySubsumption(const bool _alsoLearnt) return false; fillCannotEliminate(); - uint32_t expected_size = solver.clauses.size(); - if (alsoLearnt) expected_size += solver.learnts.size(); - clauses.reserve(expected_size); - cl_touched.reserve(expected_size); - solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses); if (alsoLearnt) { solver.clauseCleaner->cleanClauses(solver.learnts, ClauseCleaner::learnts); @@ -1340,6 +1238,7 @@ const bool Subsumer::simplifyBySubsumption(const bool _alsoLearnt) if (alsoLearnt) { numMaxSubsume1 = 500*1000*1000; if (solver.conf.doSubsWBins && !subsumeWithBinaries()) return false; + subsumeNonExist(); addedClauseLits += addFromSolver(solver.clauses); } else { if ((solver.conf.doBlockedClause || numCalls == 2) @@ -1351,7 +1250,12 @@ const bool Subsumer::simplifyBySubsumption(const bool _alsoLearnt) subsumeBinsWithBins(); numMaxSubsume1 = 2*1000*1000*1000; if (solver.conf.doSubsWBins && !subsumeWithBinaries()) return false; - if (solver.conf.doSubsWNonExistBins && !subsWNonExitsBinsFullFull()) return false; + if (solver.conf.doSubsWNonExistBins + && solver.conf.doCacheNLBins) { + if (numCalls > 3) makeAllBinsNonLearnt(); + if (!subsWNonExistBinsFill()) return false; + if (!subsumeNonExist()) return false; + } if (!handleClBinTouched()) return false; if (solver.conf.doReplace && solver.conf.doRemUselessBins) { @@ -1401,8 +1305,12 @@ const bool Subsumer::simplifyBySubsumption(const bool _alsoLearnt) } while (cl_touched.nElems() > 100); endSimplifyBySubsumption: - if (!solver.ok) return false; + if (solver.conf.doGateFind + && solver.conf.doCacheNLBins + && alsoLearnt && numCalls > 3 + && !findOrGatesAndTreat()) return false; + assert(solver.ok); assert(verifyIntegrity()); removeWrong(solver.learnts); @@ -1422,10 +1330,18 @@ const bool Subsumer::simplifyBySubsumption(const bool _alsoLearnt) << " time: " << std::setprecision(2) << std::setw(5) << (cpuTime() - myTime) << " s" //<< " blkClRem: " << std::setw(5) << numblockedClauseRemoved << std::endl; + + std::cout << "c learnt bin added due to v-elim: " << numLearntBinVarRemAdded << std::endl; } totalTime += cpuTime() - myTime; + if (!alsoLearnt) { + BothCache bothCache(solver); + if (!bothCache.tryBoth(solver.transOTFCache)) return false; + } + solver.testAllClauseAttach(); + solver.checkNoWrongAttach(); return true; } @@ -1472,17 +1388,14 @@ void Subsumer::setLimits() } if (addedClauseLits < 1000000) { - numMaxElim *= 4; - numMaxSubsume0 *= 4; - numMaxSubsume1 *= 4; + numMaxElim *= 3; + numMaxSubsume0 *= 3; + numMaxSubsume1 *= 3; } numMaxElimVars = (solver.order_heap.size()/3)*numCalls; - if (solver.order_heap.size() > 200000) - numMaxBlockVars = (uint32_t)((double)solver.order_heap.size() / 3.5 * (0.8+(double)(numCalls)/4.0)); - else - numMaxBlockVars = (uint32_t)((double)solver.order_heap.size() / 1.5 * (0.8+(double)(numCalls)/4.0)); + numMaxBlockVars = (uint32_t)((double)solver.order_heap.size() / 1.5 * (0.8+(double)(numCalls)/4.0)); if (!solver.conf.doSubsume1) numMaxSubsume1 = 0; @@ -1494,11 +1407,9 @@ void Subsumer::setLimits() if (alsoLearnt) { numMaxElim = 0; numMaxElimVars = 0; - numMaxSubsume0 /= 2; - numMaxSubsume1 /= 2; + numMaxSubsume0 /= 3; + numMaxSubsume1 /= 5; numMaxBlockVars = 0; - } else { - numCalls++; } //For debugging @@ -1752,16 +1663,17 @@ idea to eliminate a variable or not. */ bool Subsumer::maybeEliminate(const Var var) { + assert(solver.ok); assert(!var_elimed[var]); assert(!cannot_eliminate[var]); assert(solver.decision_var[var]); - if (solver.value(var) != l_Undef) return false; + if (solver.value(var) != l_Undef) return true; Lit lit = Lit(var, false); //Only exists in binary clauses -- don't delete it then /*if (occur[lit.toInt()].size() == 0 && occur[(~lit).toInt()].size() == 0) - return false;*/ + return true;*/ const uint32_t numNonLearntPos = numNonLearntBins(lit); const uint32_t posSize = occur[lit.toInt()].size() + numNonLearntPos; @@ -1772,7 +1684,7 @@ bool Subsumer::maybeEliminate(const Var var) numMaxElim -= posSize + negSize; // Heuristic CUT OFF: - if (posSize >= 10 && negSize >= 10) return false; + if (posSize >= 10 && negSize >= 10) return true; // Count clauses/literals before elimination: uint32_t before_literals = numNonLearntNeg*2 + numNonLearntPos*2; @@ -1782,13 +1694,13 @@ bool Subsumer::maybeEliminate(const Var var) // Heuristic CUT OFF2: if ((posSize >= 3 && negSize >= 3 && before_literals > 300) && clauses.size() > 700000) - return false; + return true; if ((posSize >= 5 && negSize >= 5 && before_literals > 400) && clauses.size() <= 700000 && clauses.size() > 100000) - return false; + return true; if ((posSize >= 8 && negSize >= 8 && before_literals > 700) && clauses.size() <= 100000) - return false; + return true; vec posAll, negAll; fillClAndBin(posAll, poss, lit); @@ -1807,7 +1719,7 @@ bool Subsumer::maybeEliminate(const Var var) bool ok = merge(posAll[i], negAll[j], lit, ~lit, dummy); if (ok){ after_clauses++; - if (after_clauses > before_clauses) return false; + if (after_clauses > before_clauses) return true; } } @@ -1815,6 +1727,7 @@ bool Subsumer::maybeEliminate(const Var var) numMaxElim -= posSize * negSize + before_literals; poss.clear(); negs.clear(); + if (numCalls >= 4) addLearntBinaries(var); removeClauses(posAll, negAll, var); #ifndef NDEBUG @@ -1842,51 +1755,65 @@ bool Subsumer::maybeEliminate(const Var var) } #endif - if (cleanClause(dummy)) continue; #ifdef VERBOSE_DEBUG std::cout << "Adding new clause due to varelim: " << dummy << std::endl; #endif - switch (dummy.size()) { - case 0: - solver.ok = false; - break; - case 1: { - handleSize1Clause(dummy[0]); - break; - } - case 2: { - if (findWBin(solver.watches, dummy[0], dummy[1])) { - Watched& w = findWatchedOfBin(solver.watches, dummy[0], dummy[1]); - if (w.getLearnt()) { - w.setLearnt(false); - findWatchedOfBin(solver.watches, dummy[1], dummy[0], true).setLearnt(false); - solver.learnts_literals -= 2; - solver.clauses_literals += 2; - } - } else { - solver.attachBinClause(dummy[0], dummy[1], false); - solver.numNewBin++; - } - subsume1(dummy, false); - break; - } - default: { - Clause* cl = solver.clauseAllocator.Clause_new(dummy, group_num); - ClauseSimp c = linkInClause(*cl); - if (numMaxSubsume1 > 0) subsume1(*c.clause); - else subsume0(*c.clause); - } + Clause* newCl = solver.addClauseInt(dummy, group_num, false, 0, true, false); + if (newCl != NULL) { + ClauseSimp newClSimp = linkInClause(*newCl); + if (numMaxSubsume1 > 0) subsume1(*newCl); + else subsume0(*newCl); } - if (!solver.ok) return true; + if (!solver.ok) return false; } + //removeBinsAndTris(var); + assert(occur[lit.toInt()].size() == 0 && occur[(~lit).toInt()].size() == 0); var_elimed[var] = true; numElimed++; + numMaxElimVars--; solver.setDecisionVar(var, false); return true; } +void Subsumer::addLearntBinaries(const Var var) +{ + vec tmp; + Lit lit = Lit(var, false); + const vec& ws = solver.watches[lit.toInt()]; + const vec& ws2 = solver.watches[(~lit).toInt()]; + + for (const Watched *w1 = ws.getData(), *end1 = ws.getDataEnd(); w1 != end1; w1++) { + if (!w1->isBinary()) continue; + const bool numOneIsLearnt = w1->getLearnt(); + const Lit lit1 = w1->getOtherLit(); + if (solver.value(lit1) != l_Undef || var_elimed[lit1.var()]) continue; + + for (const Watched *w2 = ws2.getData(), *end2 = ws2.getDataEnd(); w2 != end2; w2++) { + if (!w2->isBinary()) continue; + const bool numTwoIsLearnt = w2->getLearnt(); + if (!numOneIsLearnt && !numTwoIsLearnt) { + //At least one must be learnt + continue; + } + + const Lit lit2 = w2->getOtherLit(); + if (solver.value(lit2) != l_Undef || var_elimed[lit2.var()]) continue; + + tmp.clear(); + tmp.growTo(2); + tmp[0] = lit1; + tmp[1] = lit2; + Clause* tmpOK = solver.addClauseInt(tmp, 0, true, 2, true); + numLearntBinVarRemAdded++; + release_assert(tmpOK == NULL); + release_assert(solver.ok); + } + } + assert(solver.value(lit) == l_Undef); +} + /** @brief Resolves two clauses on a variable @@ -2099,7 +2026,8 @@ void Subsumer::blockedClauseRemoval() if (solver.value(vo.var) != l_Undef || !solver.decision_var[vo.var] - || cannot_eliminate[vo.var]) + || cannot_eliminate[vo.var] + || dontElim[vo.var]) continue; triedToBlock++; @@ -2208,3 +2136,650 @@ const bool Subsumer::checkElimedUnassigned() const return true; } + +class NewGateData +{ + public: + NewGateData(const Lit _lit1, const Lit _lit2, const uint32_t _numLitRem, const uint32_t _numClRem) : + lit1(_lit1) + , lit2(_lit2) + , numLitRem(_numLitRem) + , numClRem(_numClRem) + {} + const bool operator<(const NewGateData& n2) const + { + uint32_t value1 = numClRem*ANDGATEUSEFUL + numLitRem; + uint32_t value2 = n2.numClRem*ANDGATEUSEFUL + n2.numLitRem; + if (value1 != value2) return(value1 > value2); + if (lit1 != n2.lit1) return(lit1 > n2.lit1); + if (lit2 != n2.lit2) return(lit2 > n2.lit2); + return false; + } + const bool operator==(const NewGateData& n2) const + { + return(lit1 == n2.lit1 + && lit2 == n2.lit2 + && numLitRem == n2.numLitRem + && numClRem == n2.numClRem); + } + Lit lit1; + Lit lit2; + uint32_t numLitRem; + uint32_t numClRem; +}; + +struct SecondSorter +{ + const bool operator() (const std::pair p1, const std::pair p2) + { + return p1.second > p2.second; + } +}; + +void Subsumer::createNewVar() +{ + double myTime = cpuTime(); + vector newGates; + vec lits; + vec subs; + numMaxSubsume0 = 300*1000*1000; + uint64_t numOp = 0; + + if (solver.negPosDist.size() == 0) return; + uint32_t size = std::min((uint32_t)solver.negPosDist.size()-1, 400U); + + + uint32_t tries = 0; + for (; tries < std::min(100000U, size*size/2); tries++) { + Var var1, var2; + var1 = solver.negPosDist[solver.mtrand.randInt(size)].var; + var2 = solver.negPosDist[solver.mtrand.randInt(size)].var; + if (var1 == var2) continue; + + if (solver.value(var1) != l_Undef + || solver.subsumer->getVarElimed()[var1] + || solver.xorSubsumer->getVarElimed()[var1] + || solver.partHandler->getSavedState()[var1] != l_Undef + ) continue; + + if (solver.value(var2) != l_Undef + || solver.subsumer->getVarElimed()[var2] + || solver.xorSubsumer->getVarElimed()[var2] + || solver.partHandler->getSavedState()[var2] != l_Undef + ) continue; + + Lit lit1 = Lit(var1, solver.mtrand.randInt(1)); + Lit lit2 = Lit(var2, solver.mtrand.randInt(1)); + if (lit1 > lit2) std::swap(lit1, lit2); + + lits.clear(); + lits.push(lit1); + lits.push(lit2); + + subs.clear(); + findSubsumed(lits, calcAbstraction(lits), subs); + + uint32_t potential = 0; + if (numOp < 100*1000*1000) { + OrGate gate; + gate.eqLit = Lit(0,false); + gate.lits.push_back(lit1); + gate.lits.push_back(lit2); + treatAndGate(gate, false, potential, numOp); + } + + if (potential > 5 || subs.size() > 100 + || (potential > 1 && subs.size() > 50)) { + newGates.push_back(NewGateData(lit1, lit2, subs.size(), potential)); + } + } + + std::sort(newGates.begin(), newGates.end()); + newGates.erase(std::unique(newGates.begin(), newGates.end() ), newGates.end() ); + + uint32_t addedNum = 0; + for (uint32_t i = 0; i < newGates.size(); i++) { + const NewGateData& n = newGates[i]; + if ((i > 50 && n.numLitRem < 1000 && n.numClRem < 25) + || i > ((double)solver.order_heap.size()*0.01) + || i > 100) break; + + const Var newVar = solver.newVar(); + dontElim[newVar] = true; + const Lit newLit = Lit(newVar, false); + OrGate orGate; + orGate.eqLit = newLit; + orGate.lits.push_back(n.lit1); + orGate.lits.push_back(n.lit2); + orGates.push_back(orGate); + + lits.clear(); + lits.push(newLit); + lits.push(~n.lit1); + Clause* cl = solver.addClauseInt(lits, 0); + assert(cl == NULL); + assert(solver.ok); + + lits.clear(); + lits.push(newLit); + lits.push(~n.lit2); + cl = solver.addClauseInt(lits, 0); + assert(cl == NULL); + assert(solver.ok); + + lits.clear(); + lits.push(~newLit); + lits.push(n.lit1); + lits.push(n.lit2); + cl = solver.addClauseInt(lits, 0, false, 0, false, false); + assert(cl != NULL); + assert(solver.ok); + ClauseSimp c = linkInClause(*cl); + defOfOrGate[c.index] = true; + + addedNum++; + numERVars++; + } + finishedAddingVars = true; + + if (solver.conf.verbosity >= 1) { + std::cout << "c Added " << addedNum << " vars " + << " tried: " << tries + << " time: " << (cpuTime() - myTime) << std::endl; + } + //std::cout << "c Added " << addedNum << " vars " + //<< " time: " << (cpuTime() - myTime) << " numThread: " << solver.threadNum << std::endl; +} + +const bool Subsumer::findOrGatesAndTreat() +{ + assert(solver.ok); + uint32_t old_clauses_subsumed = clauses_subsumed; + + double myTime = cpuTime(); + orGates.clear(); + for (size_t i = 0; i < gateOcc.size(); i++) gateOcc[i].clear(); + + totalOrGateSize = 0; + uint32_t oldNumVarToReplace = solver.varReplacer->getNewToReplaceVars(); + uint32_t oldNumBins = solver.numBins; + gateLitsRemoved = 0; + numOrGateReplaced = 0; + + findOrGates(false); + doAllOptimisationWithGates(); + + if (solver.conf.verbosity >= 1) { + std::cout << "c ORs : " << std::setw(6) << orGates.size() + << " avg-s: " << std::fixed << std::setw(4) << std::setprecision(1) << ((double)totalOrGateSize/(double)orGates.size()) + << " cl-sh: " << std::setw(5) << numOrGateReplaced + << " l-rem: " << std::setw(6) << gateLitsRemoved + << " b-add: " << std::setw(6) << (solver.numBins - oldNumBins) + << " v-rep: " << std::setw(3) << (solver.varReplacer->getNewToReplaceVars() - oldNumVarToReplace) + << " cl-rem: " << andGateNumFound + << " avg s: " << ((double)andGateTotalSize/(double)andGateNumFound) + << " T: " << std::fixed << std::setw(7) << std::setprecision(2) << (cpuTime() - myTime) << std::endl; + } + if (!solver.ok) return false; + + bool cannotDoER; + #pragma omp critical (ERSync) + cannotDoER = (solver.threadNum != solver.dataSync->getThreadAddingVars() + || solver.dataSync->getEREnded()); + + + if (solver.conf.doER && !cannotDoER) { + vector backupOrGates = orGates; + if (!carryOutER()) return false; + for (vector::const_iterator it = backupOrGates.begin(), end = backupOrGates.end(); it != end; it++) { + orGates.push_back(*it); + } + } + + for (vector::iterator it = orGates.begin(), end = orGates.end(); it != end; it++) { + OrGate& gate = *it; + for (uint32_t i = 0; i < gate.lits.size(); i++) { + Lit lit = gate.lits[i]; + gateOcc[lit.toInt()].push_back(&(*it)); + } + } + + clauses_subsumed = old_clauses_subsumed; + + return solver.ok; +} + +const bool Subsumer::carryOutER() +{ + double myTime = cpuTime(); + orGates.clear(); + totalOrGateSize = 0; + uint32_t oldNumVarToReplace = solver.varReplacer->getNewToReplaceVars(); + uint32_t oldNumBins = solver.numBins; + gateLitsRemoved = 0; + numOrGateReplaced = 0; + defOfOrGate.clear(); + defOfOrGate.growTo(clauses.size(), false); + + createNewVar(); + doAllOptimisationWithGates(); + + if (solver.conf.verbosity >= 1) { + std::cout << "c ORs : " << std::setw(6) << orGates.size() + << " avg-s: " << std::fixed << std::setw(4) << std::setprecision(1) << ((double)totalOrGateSize/(double)orGates.size()) + << " cl-sh: " << std::setw(5) << numOrGateReplaced + << " l-rem: " << std::setw(6) << gateLitsRemoved + << " b-add: " << std::setw(6) << (solver.numBins - oldNumBins) + << " v-rep: " << std::setw(3) << (solver.varReplacer->getNewToReplaceVars() - oldNumVarToReplace) + << " cl-rem: " << andGateNumFound + << " avg s: " << ((double)andGateTotalSize/(double)andGateNumFound) + << " T: " << std::fixed << std::setw(7) << std::setprecision(2) << (cpuTime() - myTime) << std::endl; + } + return solver.ok; +} + +const bool Subsumer::doAllOptimisationWithGates() +{ + assert(solver.ok); + for (uint32_t i = 0; i < orGates.size(); i++) { + std::sort(orGates[i].lits.begin(), orGates[i].lits.end()); + } + std::sort(orGates.begin(), orGates.end(), OrGateSorter2()); + + for (vector::const_iterator it = orGates.begin(), end = orGates.end(); it != end; it++) { + if (!shortenWithOrGate(*it)) return false; + } + + if (!treatAndGates()) return false; + if (!findEqOrGates()) return false; + + return true; +} + +const bool Subsumer::findEqOrGates() +{ + assert(solver.ok); + + vec tmp(2); + for (uint32_t i = 1; i < orGates.size(); i++) { + const OrGate& gate1 = orGates[i-1]; + const OrGate& gate2 = orGates[i]; + if (gate1.lits == gate2.lits + && gate1.eqLit.var() != gate2.eqLit.var() + ) { + tmp[0] = gate1.eqLit.unsign(); + tmp[1] = gate2.eqLit.unsign(); + const bool sign = true ^ gate1.eqLit.sign() ^ gate2.eqLit.sign(); + Clause *c = solver.addXorClauseInt(tmp, sign, 0); + tmp.clear(); + tmp.growTo(2); + assert(c == NULL); + if (!solver.ok) return false; + } + } + + return true; +} + +void Subsumer::findOrGates(const bool learntGatesToo) +{ + for (const ClauseSimp *it = clauses.getData(), *end = clauses.getDataEnd(); it != end; it++) { + if (it->clause == NULL) continue; + const Clause& cl = *it->clause; + if (!learntGatesToo && cl.learnt()) continue; + + uint8_t numSizeZeroCache = 0; + Lit which = lit_Undef; + for (const Lit *l = cl.getData(), *end2 = cl.getDataEnd(); l != end2; l++) { + Lit lit = *l; + const vector& cache = solver.transOTFCache[(~lit).toInt()].lits; + + if (cache.size() == 0) { + numSizeZeroCache++; + if (numSizeZeroCache > 1) break; + which = lit; + } + } + if (numSizeZeroCache > 1) continue; + + if (numSizeZeroCache == 1) { + findOrGate(~which, *it, learntGatesToo); + } else { + for (const Lit *l = cl.getData(), *end2 = cl.getDataEnd(); l != end2; l++) + findOrGate(~*l, *it, learntGatesToo); + } + } +} + +void Subsumer::findOrGate(const Lit eqLit, const ClauseSimp& c, const bool learntGatesToo) +{ + Clause& cl = *c.clause; + bool isEqual = true; + for (const Lit *l2 = cl.getData(), *end3 = cl.getDataEnd(); l2 != end3; l2++) { + if (*l2 == ~eqLit) continue; + Lit otherLit = *l2; + const vector& cache = solver.transOTFCache[(~otherLit).toInt()].lits; + + bool OK = false; + for (vector::const_iterator cacheLit = cache.begin(), endCache = cache.end(); cacheLit != endCache; cacheLit++) { + if ((learntGatesToo || cacheLit->getOnlyNLBin()) && + cacheLit->getLit() == eqLit) { + OK = true; + break; + } + } + if (!OK) { + isEqual = false; + break; + } + } + + if (isEqual) { + OrGate gate; + for (const Lit *l2 = cl.getData(), *end3 = cl.getDataEnd(); l2 != end3; l2++) { + if (*l2 == ~eqLit) continue; + gate.lits.push_back(*l2); + } + //std::sort(gate.lits.begin(), gate.lits.end()); + gate.eqLit = eqLit; + //gate.num = orGates.size(); + orGates.push_back(gate); + totalOrGateSize += gate.lits.size(); + defOfOrGate[c.index] = true; + + #ifdef VERBOSE_ORGATE_REPLACE + std::cout << "Found gate : " << gate << std::endl; + #endif + } +} + +const bool Subsumer::shortenWithOrGate(const OrGate& gate) +{ + assert(solver.ok); + + vec subs; + findSubsumed(gate.lits, calcAbstraction(gate.lits), subs); + for (uint32_t i = 0; i < subs.size(); i++) { + ClauseSimp c = subs[i]; + Clause* cl = subs[i].clause; + + if (defOfOrGate[c.index]) continue; + + bool inside = false; + for (Lit *l = cl->getData(), *end = cl->getDataEnd(); l != end; l++) { + if (gate.eqLit.var() == l->var()) { + inside = true; + break; + } + } + if (inside) continue; + + #ifdef VERBOSE_ORGATE_REPLACE + std::cout << "OR gate-based cl-shortening" << std::endl; + std::cout << "Gate used: " << gate << std::endl; + std::cout << "orig Clause: " << *cl << std::endl; + #endif + + numOrGateReplaced++; + + for (vector::const_iterator it = gate.lits.begin(), end = gate.lits.end(); it != end; it++) { + gateLitsRemoved++; + cl->strengthen(*it); + maybeRemove(occur[it->toInt()], cl); + #ifndef TOUCH_LESS + touch(*it, cl->learnt()); + #endif + } + + gateLitsRemoved--; + cl->add(gate.eqLit); //we can add, because we removed above. Otherwise this is segfault + occur[gate.eqLit.toInt()].push(c); + + #ifdef VERBOSE_ORGATE_REPLACE + std::cout << "new Clause : " << *cl << std::endl; + std::cout << "-----------" << std::endl; + #endif + + if (!handleUpdatedClause(c)) return false; + if (c.clause != NULL && !cl->learnt()) { + for (Lit *i2 = cl->getData(), *end2 = cl->getDataEnd(); i2 != end2; i2++) + touchChangeVars(*i2); + } + } + + return solver.ok; +} + +const bool Subsumer::subsumeNonExist() +{ + double myTime = cpuTime(); + + clauses_subsumed = 0; + for (const ClauseSimp *it = clauses.getData(), *end = clauses.getDataEnd(); it != end; it++) { + if (it->clause == NULL) continue; + const Clause& cl = *it->clause; + + + for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) { + seen_tmp[l->toInt()] = true; + } + + bool toRemove = false; + for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) { + const vector& cache = solver.transOTFCache[l->toInt()].lits; + for (vector::const_iterator cacheLit = cache.begin(), endCache = cache.end(); cacheLit != endCache; cacheLit++) { + if (cacheLit->getOnlyNLBin() && seen_tmp[cacheLit->getLit().toInt()]) { + toRemove = true; + break; + } + } + if (toRemove) break; + } + + for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) { + seen_tmp[l->toInt()] = false; + } + + if (toRemove) unlinkClause(*it); + } + + if (solver.conf.verbosity >= 1) { + std::cout << "c Subs w/ non-existent bins: " << std::setw(6) << clauses_subsumed + << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << (cpuTime() - myTime) << " s" + << std::endl; + } + totalTime += cpuTime() - myTime; + + return true; +} + + +const bool Subsumer::treatAndGates() +{ + assert(solver.ok); + + andGateNumFound = 0; + vec lits; + andGateTotalSize = 0; + uint32_t foundPotential; + //double myTime = cpuTime(); + uint64_t numOp = 0; + + for (vector::const_iterator it = orGates.begin(), end = orGates.end(); it != end; it++) { + const OrGate& gate = *it; + if (gate.lits.size() > 2) continue; + if (!treatAndGate(gate, true, foundPotential, numOp)) return false; + } + + //std::cout << "c andgate time : " << (cpuTime() - myTime) << std::endl; + + return true; +} + +const bool Subsumer::treatAndGate(const OrGate& gate, const bool reallyRemove, uint32_t& foundPotential, uint64_t& numOp) +{ + assert(gate.lits.size() == 2); + std::set clToUnlink; + ClauseSimp other; + foundPotential = 0; + + if (occur[(~(gate.lits[0])).toInt()].empty() || occur[(~(gate.lits[1])).toInt()].empty()) + return true; + + for (uint32_t i = 0; i < sizeSortedOcc.size(); i++) + sizeSortedOcc[i].clear(); + + const vec& csOther = occur[(~(gate.lits[1])).toInt()]; + //std::cout << "csother: " << csOther.size() << std::endl; + uint32_t abstraction = 0; + uint32_t maxSize = 0; + for (const ClauseSimp *it2 = csOther.getData(), *end2 = csOther.getDataEnd(); it2 != end2; it2++) { + const Clause& cl = *it2->clause; + numOp += cl.size(); + if (defOfOrGate[it2->index]) continue; + + maxSize = std::max(maxSize, cl.size()); + if (sizeSortedOcc.size() < maxSize+1) sizeSortedOcc.resize(maxSize+1); + sizeSortedOcc[cl.size()].push_back(*it2); + + for (uint32_t i = 0; i < cl.size(); i++) { + seen_tmp2[cl[i].toInt()] = true; + abstraction |= 1 << (cl[i].var() & 31); + } + } + abstraction |= 1 << (gate.lits[0].var() & 31); + + vec& cs = occur[(~(gate.lits[0])).toInt()]; + //std::cout << "cs: " << cs.size() << std::endl; + for (ClauseSimp *it2 = cs.getData(), *end2 = cs.getDataEnd(); it2 != end2; it2++) { + const Clause& cl = *it2->clause; + if (defOfOrGate[it2->index] + || (cl.getAbst() | abstraction) != abstraction + || cl.size() > maxSize + || sizeSortedOcc[cl.size()].empty()) continue; + numOp += cl.size(); + + bool OK = true; + for (uint32_t i = 0; i < cl.size(); i++) { + if (cl[i] == ~(gate.lits[0])) continue; + if ( cl[i].var() == ~(gate.lits[1].var()) + || cl[i].var() == gate.eqLit.var() + || !seen_tmp2[cl[i].toInt()] + ) { + OK = false; + break; + } + } + if (!OK) continue; + + uint32_t abst2 = 0; + for (uint32_t i = 0; i < cl.size(); i++) { + if (cl[i] == ~(gate.lits[0])) continue; + seen_tmp[cl[i].toInt()] = true; + abst2 |= 1 << (cl[i].var() & 31); + } + abst2 |= 1 << ((~(gate.lits[1])).var() & 31); + + numOp += sizeSortedOcc[cl.size()].size()*5; + const bool foundOther = findAndGateOtherCl(sizeSortedOcc[cl.size()], ~(gate.lits[1]), abst2, other); + foundPotential += foundOther; + if (reallyRemove && foundOther) { + assert(other.index != it2->index); + clToUnlink.insert(other.index); + clToUnlink.insert(it2->index); + if (!treatAndGateClause(other, gate, cl)) return false; + } + + for (uint32_t i = 0; i < cl.size(); i++) { + seen_tmp[cl[i].toInt()] = false; + } + } + + std::fill(seen_tmp2.getData(), seen_tmp2.getDataEnd(), 0); + + for(std::set::const_iterator it2 = clToUnlink.begin(), end2 = clToUnlink.end(); it2 != end2; it2++) { + unlinkClause(clauses[*it2]); + } + clToUnlink.clear(); + + return true; +} + +const bool Subsumer::treatAndGateClause(const ClauseSimp& other, const OrGate& gate, const Clause& cl) +{ + vec lits; + + #ifdef VERBOSE_ORGATE_REPLACE + std::cout << "AND gate-based cl rem" << std::endl; + std::cout << "clause 1: " << cl << std::endl; + std::cout << "clause 2: " << *other.clause << std::endl; + std::cout << "gate : " << gate << std::endl; + #endif + + lits.clear(); + for (uint32_t i = 0; i < cl.size(); i++) { + if (cl[i] != ~(gate.lits[0])) lits.push(cl[i]); + + assert(cl[i].var() != gate.eqLit.var()); + } + andGateNumFound++; + andGateTotalSize += cl.size(); + + lits.push(~(gate.eqLit)); + bool learnt = other.clause->learnt() && cl.learnt(); + uint32_t glue; + if (!learnt) glue = 0; + else glue = std::min(other.clause->getGlue(), cl.getGlue()); + + #ifdef VERBOSE_ORGATE_REPLACE + std::cout << "new clause:" << lits << std::endl; + std::cout << "-----------" << std::endl; + #endif + + Clause* c = solver.addClauseInt(lits, cl.getGroup(), learnt, glue, false, false); + if (c != NULL) linkInClause(*c); + if (!solver.ok) return false; + + return true; +} + +inline const bool Subsumer::findAndGateOtherCl(const vector& sizeSortedOcc, const Lit lit, const uint32_t abst2, ClauseSimp& other) +{ + for (vector::const_iterator it = sizeSortedOcc.begin(), end = sizeSortedOcc.end(); it != end; it++) { + const Clause& cl = *it->clause; + if (defOfOrGate[it->index] + || cl.getAbst() != abst2) continue; + + for (uint32_t i = 0; i < cl.size(); i++) { + if (cl[i] == lit) continue; + if (!seen_tmp[cl[i].toInt()]) goto next; + } + other = *it; + return true; + + next:; + } + + return false; +} + +void Subsumer::makeAllBinsNonLearnt() +{ + uint32_t changedHalfToNonLearnt = 0; + uint32_t wsLit = 0; + for (vec *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) { + Lit lit = ~Lit::toLit(wsLit); + vec& ws = *it; + + for (Watched *i = ws.getData(), *end2 = ws.getDataEnd(); i != end2; i++) { + if (i->isBinary() && i->getLearnt()) { + i->setLearnt(false); + changedHalfToNonLearnt++; + } + } + } + + assert(changedHalfToNonLearnt % 2 == 0); + solver.learnts_literals -= changedHalfToNonLearnt; + solver.clauses_literals += changedHalfToNonLearnt; +} diff --git a/src/sat/cryptominisat2/Subsumer.h b/src/sat/cryptominisat2/Subsumer.h index 19f44e4..6615573 100644 --- a/src/sat/cryptominisat2/Subsumer.h +++ b/src/sat/cryptominisat2/Subsumer.h @@ -16,7 +16,11 @@ Modifications for CryptoMiniSat are under GPLv3. #include #include #include +#include #include +#include +#include + using std::vector; using std::list; using std::map; @@ -25,6 +29,25 @@ using std::priority_queue; class ClauseCleaner; class OnlyNonLearntBins; +class OrGate { + public: + Lit eqLit; + vector lits; + //uint32_t num; +}; + +inline std::ostream& operator<<(std::ostream& os, const OrGate& gate) +{ + os << " gate "; + //os << " no. " << std::setw(4) << gate.num; + os << " lits: "; + for (uint32_t i = 0; i < gate.lits.size(); i++) { + os << gate.lits[i] << " "; + } + os << " eqLit: " << gate.eqLit; + return os; +} + /** @brief Handles subsumption, self-subsuming resolution, variable elimination, and related algorithms @@ -59,6 +82,12 @@ public: const double getTotalTime() const; const map > >& getElimedOutVar() const; const map > >& getElimedOutVarBin() const; + const uint32_t getNumERVars() const; + void incNumERVars(const uint32_t num); + void setVarNonEliminable(const Var var); + const bool getFinishedAddingVars() const; + void setFinishedAddingVars(const bool val); + const vector& getGateOcc(const Lit lit) const; private: @@ -79,6 +108,7 @@ private: vec iter_sets; /// cannot_eliminate;/// seen_tmp; /// seen_tmp2; /// @@ -164,7 +195,6 @@ private: struct subsume0Happened { bool subsumedNonLearnt; uint32_t glue; - float act; }; /** @brief Sort clauses according to size @@ -201,8 +231,6 @@ private: const bool subsume1(vec& ps, const bool wasLearnt); void strenghten(ClauseSimp& c, const Lit toRemoveLit); const bool cleanClause(Clause& ps); - const bool cleanClause(vec& ps) const; - void handleSize1Clause(const Lit lit); //Variable elimination /** @@ -238,15 +266,20 @@ private: Lit lit2; bool isBin; }; + uint32_t numLearntBinVarRemAdded; void orderVarsForElim(vec& order); const uint32_t numNonLearntBins(const Lit lit) const; bool maybeEliminate(Var x); + void addLearntBinaries(const Var var); void removeClauses(vec& posAll, vec& negAll, const Var var); void removeClausesHelper(vec& todo, const Var var, std::pair& removed); bool merge(const ClAndBin& ps, const ClAndBin& qs, const Lit without_p, const Lit without_q, vec& out_clause); const bool eliminateVars(); void fillClAndBin(vec& all, vec& cs, const Lit lit); + void removeBinsAndTris(const Var var); + const uint32_t removeBinAndTrisHelper(const Lit lit, vec& ws); + //Subsume with Nonexistent Bins struct BinSorter2 { const bool operator()(const Watched& first, const Watched& second) @@ -264,15 +297,12 @@ private: return false; }; }; - const bool subsWNonExitsBinsFullFull(); - const bool subsWNonExistBinsFull(); - const bool subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* OnlyNonLearntBins); - void subsume0BIN(const Lit lit, const vec& lits, const uint32_t abst); - bool subsNonExistentFinish; - uint32_t doneNum; + void makeAllBinsNonLearnt(); + const bool subsWNonExistBinsFill(); + const bool subsWNonExistBinsFillHelper(const Lit& lit, OnlyNonLearntBins* OnlyNonLearntBins); + const bool subsumeNonExist(); + uint32_t doneNumNonExist; uint64_t extraTimeNonExist; - vec toVisit; /// toVisitAll; /// gate2.lits.size()); + } + }; + struct OrGateSorter2 { + const bool operator() (const OrGate& gate1, const OrGate& gate2) { + if (gate1.lits.size() > gate2.lits.size()) return true; + if (gate1.lits.size() < gate2.lits.size()) return false; + + assert(gate1.lits.size() == gate2.lits.size()); + for (uint32_t i = 0; i < gate1.lits.size(); i++) { + if (gate1.lits[i] < gate2.lits[i]) return true; + if (gate1.lits[i] > gate2.lits[i]) return false; + } + + return false; + } + }; + const bool findOrGatesAndTreat(); + void findOrGates(const bool learntGatesToo); + void findOrGate(const Lit eqLit, const ClauseSimp& c, const bool learntGatesToo); + const bool shortenWithOrGate(const OrGate& gate); + int64_t gateLitsRemoved; + uint64_t totalOrGateSize; + vector orGates; + vector > gateOcc; + uint32_t numOrGateReplaced; + const bool findEqOrGates(); + vec defOfOrGate; + const bool carryOutER(); + void createNewVar(); + const bool doAllOptimisationWithGates(); + uint32_t andGateNumFound; + uint32_t andGateTotalSize; + vec dontElim; + uint32_t numERVars; + bool finishedAddingVars; + + const bool treatAndGates(); + const bool treatAndGate(const OrGate& gate, const bool reallyRemove, uint32_t& foundPotential, uint64_t& numOp); + const bool treatAndGateClause(const ClauseSimp& other, const OrGate& gate, const Clause& cl); + const bool findAndGateOtherCl(const vector& sizeSortedOcc, const Lit lit, const uint32_t abst2, ClauseSimp& other); + vector > sizeSortedOcc; //validity checking const bool verifyIntegrity(); @@ -306,7 +381,6 @@ private: uint32_t clauses_subsumed; ///()); + gateOcc.push_back(vector()); } inline const map > >& Subsumer::getElimedOutVar() const @@ -476,4 +555,34 @@ inline const double Subsumer::getTotalTime() const return totalTime; } +inline const uint32_t Subsumer::getNumERVars() const +{ + return numERVars; +} + +inline void Subsumer::incNumERVars(const uint32_t num) +{ + numERVars += num; +} + +inline void Subsumer::setVarNonEliminable(const Var var) +{ + dontElim[var] = true; +} + +inline const bool Subsumer::getFinishedAddingVars() const +{ + return finishedAddingVars; +} + +inline void Subsumer::setFinishedAddingVars(const bool val) +{ + finishedAddingVars = val; +} + +inline const vector& Subsumer::getGateOcc(const Lit lit) const +{ + return gateOcc[lit.toInt()]; +} + #endif //SIMPLIFIER_H diff --git a/src/sat/cryptominisat2/TransCache.h b/src/sat/cryptominisat2/TransCache.h new file mode 100644 index 0000000..382094d --- /dev/null +++ b/src/sat/cryptominisat2/TransCache.h @@ -0,0 +1,114 @@ +#ifndef TRANSCACHE_H +#define TRANSCACHE_H + +#include +#include +#include + +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "SolverTypes.h" + +class LitExtra { + public: + LitExtra() {}; + + LitExtra(const Lit l, const bool onlyNLBin) + { + x = onlyNLBin + (l.toInt() << 1); + } + + const Lit getLit() const + { + return Lit::toLit(x>>1); + } + + const bool getOnlyNLBin() const + { + return x&1; + } + + const bool operator<(const LitExtra other) const + { + if (getOnlyNLBin() && !other.getOnlyNLBin()) return false; + if (!getOnlyNLBin() && other.getOnlyNLBin()) return true; + return (getLit() < other.getLit()); + } + + const bool operator==(const LitExtra other) const + { + return x == other.x; + } + + const bool operator!=(const LitExtra other) const + { + return x != other.x; + } + private: + uint32_t x; + +}; + +class TransCache { + public: + TransCache() : + conflictLastUpdated(std::numeric_limits::max()) + {}; + + void merge(std::vector& otherLits) + { + std::sort(lits.begin(), lits.end()); + lits.erase(std::unique(lits.begin(), lits.end()), lits.end()); + std::sort(otherLits.begin(), otherLits.end()); + + //swap to keep original place if possible + std::vector oldLits(lits); + std::vector newLits; + newLits.swap(lits); + newLits.clear(); + + std::vector::iterator it = oldLits.begin(); + std::vector::iterator itOther = otherLits.begin(); + for (;itOther != otherLits.end() || it != oldLits.end();) { + if (it == oldLits.end()) { + newLits.push_back(*itOther); + itOther++; + continue; + } + if (itOther == otherLits.end()) { + newLits.push_back(*it); + it++; + continue; + } + + //now both of them contain something + if (it->getLit() == itOther->getLit()) { + bool onlyNLBin = it->getOnlyNLBin() || it->getOnlyNLBin(); + newLits.push_back(LitExtra(it->getLit(), onlyNLBin)); + it++; + itOther++; + continue; + } + + if (it->getLit() < itOther->getLit()) { + newLits.push_back(*it); + it++; + continue; + } + + assert(it->getLit() > itOther->getLit()); + newLits.push_back(*itOther); + it++; + } + lits.swap(newLits); + } + + std::vector lits; + uint64_t conflictLastUpdated; +}; + +#endif //TRANSCACHE_H \ No newline at end of file diff --git a/src/sat/cryptominisat2/UselessBinRemover.cpp b/src/sat/cryptominisat2/UselessBinRemover.cpp index 4014df8..d881614 100644 --- a/src/sat/cryptominisat2/UselessBinRemover.cpp +++ b/src/sat/cryptominisat2/UselessBinRemover.cpp @@ -66,7 +66,7 @@ const bool UselessBinRemover::removeUslessBinFull() fixed = true; solver.cancelUntilLight(); solver.uncheckedEnqueue(~lit); - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; continue; } @@ -76,7 +76,7 @@ const bool UselessBinRemover::removeUslessBinFull() fixed = true; solver.cancelUntilLight(); solver.uncheckedEnqueue(~lit); - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) return false; continue; } diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 02151f1..c607121 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,2 @@ CryptoMiniSat -GIT revision: 588152bb03adf98ffd581c4579e1d6c5eec92f8f +GIT revision: d28c9b8ba7b189113cdf9c8147a14ae2a9b546bd diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 42b3280..4d6aae5 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -141,6 +141,7 @@ const bool VarReplacer::performReplaceInternal() if (!replace_set(solver.learnts)) goto end; if (!replace_set(solver.xorclauses)) goto end; solver.testAllClauseAttach(); + solver.checkNoWrongAttach(); end: assert(solver.qhead == solver.trail.size() || !solver.ok); @@ -244,7 +245,7 @@ const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, co case 1: solver.detachModifiedClause(origVar1, origVar2, origSize, &c); solver.uncheckedEnqueue(Lit(c[0].var(), c.xorEqualFalse())); - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); return true; case 2: { solver.detachModifiedClause(origVar1, origVar2, origSize, &c); @@ -360,7 +361,7 @@ const bool VarReplacer::replaceBins() solver.clauses_literals -= removedNonLearnt; solver.numBins -= (removedLearnt + removedNonLearnt)/2; - if (solver.ok) solver.ok = (solver.propagate().isNULL()); + if (solver.ok) solver.ok = (solver.propagate().isNULL()); return solver.ok; } @@ -387,7 +388,10 @@ const bool VarReplacer::replace_set(vec& cs) } if (changed && handleUpdatedClause(c, origLit1, origLit2, origLit3)) { + if (c.learnt()) solver.nbCompensateSubsumer++; + solver.clauseAllocator.clauseFree(*r); if (!solver.ok) { + r++; #ifdef VERBOSE_DEBUG cout << "contradiction while replacing lits in normal clause" << std::endl; #endif @@ -445,7 +449,7 @@ const bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const return true; case 1 : solver.uncheckedEnqueue(c[0]); - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); return true; case 2: solver.attachBinClause(c[0], c[1], c.learnt()); @@ -453,6 +457,7 @@ const bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const solver.dataSync->signalNewBinClause(c); return true; default: + if (c.size() == 3) solver.dataSync->signalNewTriClause(c); solver.attachClause(c); return false; } @@ -504,7 +509,7 @@ void VarReplacer::extendModelPossible() const assert(solver.assigns[i].getBool() == (solver.assigns[it->var()].getBool() ^ it->sign())); } } - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); assert(solver.ok); } } @@ -568,6 +573,7 @@ const bool VarReplacer::replace(T& ps, const bool xorEqualFalse, const uint32_t std::cout << "replace() called with var " << ps[0].var()+1 << " and var " << ps[1].var()+1 << " with xorEqualFalse " << xorEqualFalse << std::endl; #endif + assert(solver.ok); assert(solver.decisionLevel() == 0); assert(ps.size() == 2); assert(!ps[0].sign()); @@ -610,11 +616,8 @@ const bool VarReplacer::replace(T& ps, const bool xorEqualFalse, const uint32_t lbool val1 = solver.value(lit1); lbool val2 = solver.value(lit2); if (val1 != l_Undef && val2 != l_Undef) { - if (val1 != val2) { - solver.ok = false; - return false; - } - return true; + if (val1 != val2) solver.ok = false; + return solver.ok; } if ((val1 != l_Undef && val2 == l_Undef) || (val2 != l_Undef && val1 == l_Undef)) { @@ -622,7 +625,7 @@ const bool VarReplacer::replace(T& ps, const bool xorEqualFalse, const uint32_t if (val1 != l_Undef) solver.uncheckedEnqueue(lit2 ^ (val1 == l_False)); else solver.uncheckedEnqueue(lit1 ^ (val2 == l_False)); - if (solver.ok) solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); return solver.ok; } @@ -630,7 +633,7 @@ const bool VarReplacer::replace(T& ps, const bool xorEqualFalse, const uint32_t assert(val1 == l_Undef && val2 == l_Undef); #endif //DEBUG_REPLACER - addBinaryXorClause(lit1, lit2 ^ true, group, false); + addBinaryXorClause(lit1, lit2 ^ true, group); if (reverseTable.find(lit1.var()) == reverseTable.end()) { reverseTable[lit2.var()].push_back(lit1.var()); @@ -665,14 +668,14 @@ so we add this to the binary clauses of Solver, and we recover it next time. \todo Clean this messy internal/external thing using a better datastructure. */ -void VarReplacer::addBinaryXorClause(Lit lit1, Lit lit2, const uint32_t group, const bool addBinAsLearnt) +void VarReplacer::addBinaryXorClause(Lit lit1, Lit lit2, const uint32_t group) { - solver.attachBinClause(lit1, lit2, addBinAsLearnt); + solver.attachBinClause(lit1, lit2, false); solver.dataSync->signalNewBinClause(lit1, lit2); lit1 ^= true; lit2 ^= true; - solver.attachBinClause(lit1, lit2, addBinAsLearnt); + solver.attachBinClause(lit1, lit2, false); solver.dataSync->signalNewBinClause(lit1, lit2); } diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index eebee76..cb3b614 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -1,4 +1,4 @@ -/*********************************************************************************** +/*************************************************************************** CryptoMiniSat -- Copyright (c) 2009 Mate Soos This program is free software: you can redistribute it and/or modify @@ -13,7 +13,7 @@ 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 VARREPLACER_H #define VARREPLACER_H @@ -75,7 +75,7 @@ class VarReplacer const bool replace_set(vec& cs); const bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2, const Lit origLit3); const bool handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2); - void addBinaryXorClause(Lit lit1, Lit lit2, const uint32_t group, const bool addBinAsLearnt = false); + void addBinaryXorClause(Lit lit1, Lit lit2, const uint32_t group); void setAllThatPointsHereTo(const Var var, const Lit lit); bool alreadyIn(const Var var, const Lit lit); diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index e7983d4..39f58e8 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -88,7 +88,7 @@ const bool XorFinder::fullFindXors(const uint32_t minSize, const uint32_t maxSiz std::sort(table.begin(), table.end(), clause_sorter_primary()); if (!findXors(sumLengths)) goto end; - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); end: diff --git a/src/sat/cryptominisat2/XorSubsumer.cpp b/src/sat/cryptominisat2/XorSubsumer.cpp index 8509ee2..906fe33 100644 --- a/src/sat/cryptominisat2/XorSubsumer.cpp +++ b/src/sat/cryptominisat2/XorSubsumer.cpp @@ -520,7 +520,7 @@ const bool XorSubsumer::simplifyBySubsumption() } propagated = (solver.qhead != solver.trail.size()); - solver.ok = (solver.propagate().isNULL()); + solver.ok = (solver.propagate().isNULL()); if (!solver.ok) { return false; } diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h index d1ec2b2..225443b 100644 --- a/src/sat/cryptominisat2/constants.h +++ b/src/sat/cryptominisat2/constants.h @@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA /////////////////// //Parameters for learnt-clause cleaning -#define RATIOREMOVECLAUSES 1.0/2.0 +#define RATIOREMOVECLAUSES (1.0/2.0) #define NBCLAUSESBEFOREREDUCE 20000 #define FIXCLEANREPLACE 30U @@ -34,9 +34,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define MAX_CLAUSENUM_XORFIND 1500000 #define BINARY_TO_XOR_APPROX 12.0 +#define ANDGATEUSEFUL 20 #define RANDOM_LOOKAROUND_SEARCHSPACE #define UPDATE_TRANSOTFSSR_CACHE 200000 -//#define USE_OLD_POLARITIES //Parameters controlling simplification rounds #define SIMPLIFY_MULTIPLIER 300 @@ -46,8 +46,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define NUM_CONFL_BURST_SEARCH 500 //Parameters controlling full restarts -#define FULLRESTART_MULTIPLIER 250 -#define FULLRESTART_MULTIPLIER_MULTIPLIER 3.5 #define RESTART_TYPE_DECIDER_FROM 2 #define RESTART_TYPE_DECIDER_UNTIL 7 @@ -94,7 +92,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define DEBUG_ATTACH #define DEBUG_REPLACER #define DEBUG_HYPERBIN -//#define DEBUG_USELESS_LEARNT_BIN_REMOVAL +#endif + +#ifdef MORE_DEBUG +#define UNCHECKEDENQUEUE_DEBUG +#define DEBUG_USELESS_LEARNT_BIN_REMOVAL #endif //#define DEBUG_ATTACH_FULL diff --git a/src/sat/cryptominisat2/mtl/Vec.h b/src/sat/cryptominisat2/mtl/Vec.h index 193eccd..90336e6 100644 --- a/src/sat/cryptominisat2/mtl/Vec.h +++ b/src/sat/cryptominisat2/mtl/Vec.h @@ -92,6 +92,7 @@ public: if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); + assert(data != NULL); } new (&data[sz]) T(); sz++; @@ -101,6 +102,7 @@ public: if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); + assert(data != NULL); } data[sz++] = elem; } -- 2.47.3