diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/FailedLitSearcher.cpp')
| -rw-r--r-- | src/prop/cryptominisat/Solver/FailedLitSearcher.cpp | 768 |
1 files changed, 0 insertions, 768 deletions
diff --git a/src/prop/cryptominisat/Solver/FailedLitSearcher.cpp b/src/prop/cryptominisat/Solver/FailedLitSearcher.cpp deleted file mode 100644 index a847c5e09..000000000 --- a/src/prop/cryptominisat/Solver/FailedLitSearcher.cpp +++ /dev/null @@ -1,768 +0,0 @@ -/************************************************************************** -CryptoMiniSat -- Copyright (c) 2009 Mate Soos - -This program is free software: you can redistribute it and/or modify -it under the terms of the GNU General Public License as published by -the Free Software Foundation, either version 3 of the License, or -(at your option) any later version. - -This program is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -GNU General Public License for more details. - -You should have received a copy of the GNU General Public License -along with this program. If not, see <http://www.gnu.org/licenses/>. -*****************************************************************************/ - -#include "FailedLitSearcher.h" - -#include <iomanip> -#include <utility> -#include <set> - -#include "Solver.h" -#include "ClauseCleaner.h" -#include "time_mem.h" -#include "VarReplacer.h" -#include "ClauseCleaner.h" -#include "StateSaver.h" -#include "CompleteDetachReattacher.h" - -//#define VERBOSE_DEUBUG - -using namespace CMSat; -using std::make_pair; -using std::set; - -/** -@brief Sets up variables that are used between calls to search() -*/ -FailedLitSearcher::FailedLitSearcher(Solver& _solver): - solver(_solver) - , tmpPs(2) - , totalTime(0) - , numPropsMultiplier(1.0) - , lastTimeFoundTruths(0) - , numCalls(0) -{ - lastTimeStopped = solver.mtrand.randInt(solver.nVars()); -} - -/** -@brief Initialises datastructures for 2-long xor finding by shortening longer xors -*/ -void FailedLitSearcher::addFromSolver(const vec< XorClause* >& cs) -{ - xorClauseSizes.clear(); - xorClauseSizes.growTo(cs.size()); - occur.resize(solver.nVars()); - for (Var var = 0; var < solver.nVars(); var++) { - occur[var].clear(); - } - - uint32_t i = 0; - for (XorClause * const*it = cs.getData(), * const*end = it + cs.size(); it != end; it++, i++) { - if (it+1 != end) __builtin_prefetch(*(it+1)); - - const XorClause& cl = **it; - xorClauseSizes[i] = cl.size(); - for (const Lit *l = cl.getData(), *end2 = l + cl.size(); l != end2; l++) { - occur[l->var()].push_back(i); - } - } -} - -/** -@brief Remove the assinged vars from the xors added by addFromSolver() - -The thus shortened xors are then treated if they are 2-long and if they -appear twice: by propagating "var" and by propagating "~var" -*/ -inline void FailedLitSearcher::removeVarFromXors(const Var var) -{ - vector<uint32_t>& occ = occur[var]; - if (occ.empty()) return; - - for (uint32_t *it = &occ[0], *end = it + occ.size(); it != end; it++) { - xorClauseSizes[*it]--; - if (!xorClauseTouched[*it]) { - xorClauseTouched.setBit(*it); - investigateXor.push(*it); - } - } -} - -/** -@brief Undoes what removeVarFromXors() has done -*/ -inline void FailedLitSearcher::addVarFromXors(const Var var) -{ - vector<uint32_t>& occ = occur[var]; - if (occ.empty()) return; - - for (uint32_t *it = &occ[0], *end = it + occ.size(); it != end; it++) { - xorClauseSizes[*it]++; - } -} - -/** -@brief Returns the 2-long xor clause that has been made of the longer xor-clause under current assignement - -We KNOW that the xorclause "c" passed as a parameter must be 2-long. We just -need it so that we can work with it. We KNOW it's 2-long because of the -data structures and functions in place - -@p[in] c MUST be a 2-long xor clause under current assignement -*/ -FailedLitSearcher::TwoLongXor FailedLitSearcher::getTwoLongXor(const XorClause& c) -{ - TwoLongXor tmp; - uint32_t num = 0; - tmp.inverted = c.xorEqualFalse(); - - for(const Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { - if (solver.assigns[l->var()] == l_Undef) { - assert(num < 2); - tmp.var[num] = l->var(); - num++; - } else { - tmp.inverted ^= (solver.assigns[l->var()] == l_True); - } - } - - #ifdef VERBOSE_DEUBUG - if (num != 2) { - std::cout << "Num:" << num << std::endl; - c.plainPrint(); - } - #endif - - std::sort(&tmp.var[0], &tmp.var[0]+2); - assert(num == 2); - return tmp; -} - -/** -@brief The main function. Initialises data and calls tryBoth() for heavy-lifting - -It sets up the ground for tryBoth() and calls it as many times as it sees fit. -One afther the other, the different optimisations' data structures are -initialised, and their limits are set. Then tryBoth is called in two different -forms: somewhat sequentially on varaibles x...z and then on randomly picked -variables. -*/ -bool FailedLitSearcher::search() -{ - assert(solver.decisionLevel() == 0); - if (solver.nVars() == 0) return solver.ok; - - uint64_t numProps = 130 * 1000000; - uint64_t numPropsDifferent = (double)numProps*2.0; - - solver.testAllClauseAttach(); - double myTime = cpuTime(); - uint32_t origHeapSize = solver.order_heap.size(); - StateSaver savedState(solver); - Heap<Solver::VarOrderLt> order_heap_copy(solver.order_heap); //for hyperbin - - //General Stats - numFailed = 0; - goodBothSame = 0; - numCalls++; - - //If failed var searching is going good, do successively more and more of it - if ((double)lastTimeFoundTruths > (double)solver.order_heap.size() * 0.10) numPropsMultiplier = std::max(numPropsMultiplier*1.3, 2.0); - else numPropsMultiplier = 1.0; - numProps = (uint64_t) ((double)numProps * numPropsMultiplier * solver.conf.failedLitMultiplier); - - //For BothSame - propagated.resize(solver.nVars(), 0); - propValue.resize(solver.nVars(), 0); - - //For calculating how many variables have really been set - origTrailSize = solver.trail.size(); - - //For 2-long xor (rule 6 of Equivalent literal propagation in the DLL procedure by Chu-Min Li) - toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); - lastTrailSize = solver.trail.size(); - binXorFind = true; - twoLongXors.clear(); - if (solver.xorclauses.size() < 5 || - solver.xorclauses.size() > 30000 || - solver.order_heap.size() > 30000 || - solver.nClauses() > 100000) - binXorFind = false; - if (binXorFind) { - solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); - addFromSolver(solver.xorclauses); - } - xorClauseTouched.resize(solver.xorclauses.size(), 0); - newBinXor = 0; - - //For 2-long xor through Le Berre paper - bothInvert = 0; - - //For HyperBin - addedBin = 0; - unPropagatedBin.resize(solver.nVars(), 0); - needToVisit.resize(solver.nVars(), 0); - dontRemoveAncestor.resize(solver.nVars(), 0); - hyperbinProps = 0; - maxHyperBinProps = numProps/4; - if (solver.order_heap.size() < 20000) - maxHyperBinProps*=2; - removedUselessLearnt = 0; - removedUselessNonLearnt = 0; - - //uint32_t fromBin; - origProps = solver.propagations; - uint32_t i; - for (i = 0; i < solver.nVars(); i++) { - Var var = (lastTimeStopped + i) % solver.nVars(); - if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) - continue; - if (solver.propagations >= origProps + numProps) - break; - if (!tryBoth(Lit(var, false), Lit(var, true))) - goto end; - } - lastTimeStopped = (lastTimeStopped + i) % solver.nVars(); - - origProps = solver.propagations; - while (!order_heap_copy.empty()) { - Var var = order_heap_copy.removeMin(); - 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; - } - - if (solver.conf.verbosity >= 1) printResults(myTime); - - -end: - solver.order_heap.filter(Solver::VarFilter(solver)); - - if (solver.ok && (numFailed || goodBothSame)) { - double time = cpuTime(); - if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) { - CompleteDetachReatacher reattacher(solver); - reattacher.detachNonBinsNonTris(true); - const bool ret = reattacher.reattachNonBins(); - release_assert(ret == true); - } else { - solver.clauseCleaner->removeAndCleanAll(); - } - if (solver.conf.verbosity >= 1 && numFailed + goodBothSame > 100) { - std::cout << "c Cleaning up after failed var search: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime() - time << " s " - << std::endl; - } - } - - lastTimeFoundTruths = solver.trail.size() - origTrailSize; - totalTime += cpuTime() - myTime; - - savedState.restore(); - - solver.testAllClauseAttach(); - return solver.ok; -} - - -/** -@brief Prints results of failed litaral probing - -Printed: -1) Num failed lits -2) Num lits that have been propagated by both "var" and "~var" -3) 2-long Xor clauses that have been found because when propagating "var" and - "~var", they have been produced by normal xor-clauses shortening to this xor - clause -4) If var1 propagates var2 and ~var1 propagates ~var2, then var=var2, and this - is a 2-long XOR clause -5) Number of propagations -6) Time in seconds -*/ -void FailedLitSearcher::printResults(const double myTime) const -{ - std::cout << "c Flit: "<< std::setw(5) << numFailed << - " Blit: " << std::setw(6) << goodBothSame << - " bXBeca: " << std::setw(4) << newBinXor << - " bXProp: " << std::setw(4) << bothInvert << - " Bins:" << std::setw(7) << addedBin << - " BRemL:" << std::setw(7) << removedUselessLearnt << - " BRemN:" << std::setw(7) << removedUselessNonLearnt << - " 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; -} - -/** -@brief The main function of search() doing almost everything in this class - -Tries to branch on both lit1 and lit2 and then both-propagates them, fail-lits -them, and hyper-bin resolves them, etc. It is imperative that from the -SAT point of view, EITHER lit1 or lit2 MUST hold. So, if lit1 = ~lit2, it's OK. -Also, if there is a binary clause 'lit1 or lit2' it's also OK. -*/ -bool FailedLitSearcher::tryBoth(const Lit lit1, const Lit lit2) -{ - if (binXorFind) { - if (lastTrailSize < solver.trail.size()) { - for (uint32_t i = lastTrailSize; i != solver.trail.size(); i++) { - removeVarFromXors(solver.trail[i].var()); - } - } - lastTrailSize = solver.trail.size(); - xorClauseTouched.setZero(); - investigateXor.clear(); - } - - propagated.removeThese(propagatedBitSet); - #ifdef DEBUG_FAILEDLIT - assert(propagated.isZero()); - #endif - propagatedBitSet.clear(); - twoLongXors.clear(); - bothSame.clear(); - binXorToAdd.clear(); - #ifdef DEBUG_HYPERBIN - assert(propagatedVars.empty()); - assert(unPropagatedBin.isZero()); - #endif //DEBUG_HYPERBIN - #ifdef DEBUG_USELESS_LEARNT_BIN_REMOVAL - dontRemoveAncestor.isZero(); - assert(uselessBin.empty()); - #endif - - solver.newDecisionLevel(); - solver.uncheckedEnqueueLight(lit1); - failed = (!solver.propagate<false>(false).isNULL()); - if (failed) { - solver.cancelUntilLight(); - numFailed++; - solver.uncheckedEnqueue(~lit1); - solver.ok = (solver.propagate<false>(false).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(); - } - 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); - propagatedVars.push(x); - } - - if (solver.assigns[x].getBool()) propValue.setBit(x); - else propValue.clearBit(x); - - if (binXorFind) removeVarFromXors(x); - if (solver.conf.doCacheOTFSSR && c != (int)solver.trail_lim[0]) { - lit1OTFCache.lits.push_back(solver.trail[c]); - } - } - - if (binXorFind) { - for (uint32_t *it = investigateXor.getData(), *end = investigateXor.getDataEnd(); it != end; it++) { - if (xorClauseSizes[*it] == 2) - twoLongXors.insert(getTwoLongXor(*solver.xorclauses[*it])); - } - for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { - addVarFromXors(solver.trail[c].var()); - } - xorClauseTouched.setZero(); - investigateXor.clear(); - } - - 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(); - } - - #ifdef DEBUG_HYPERBIN - assert(propagatedVars.empty()); - assert(unPropagatedBin.isZero()); - #endif //DEBUG_HYPERBIN - - solver.newDecisionLevel(); - solver.uncheckedEnqueueLight(lit2); - failed = (!solver.propagate<false>(false).isNULL()); - if (failed) { - solver.cancelUntilLight(); - numFailed++; - solver.uncheckedEnqueue(~lit2); - solver.ok = (solver.propagate<false>(false).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(); - } - for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { - Var x = solver.trail[c].var(); - if (propagated[x]) { - if (propValue[x] == solver.assigns[x].getBool()) { - //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)); - bothInvert += solver.varReplacer->getNewToReplaceVars() - toReplaceBefore; - toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); - } - } - - if (solver.conf.doHyperBinRes) { - unPropagatedBin.setBit(x); - propagatedVars.push(x); - } - - if (solver.assigns[x].getBool()) propValue.setBit(x); - else propValue.clearBit(x); - - if (binXorFind) removeVarFromXors(x); - if (solver.conf.doCacheOTFSSR && c != (int)solver.trail_lim[0]) { - lit2OTFCache.lits.push_back(solver.trail[c]); - } - } - - //We now add the two-long xors that have been found through longer - //xor-shortening - if (binXorFind) { - if (twoLongXors.size() > 0) { - for (uint32_t *it = investigateXor.getData(), *end = it + investigateXor.size(); it != end; it++) { - if (xorClauseSizes[*it] == 2) { - TwoLongXor tmp = getTwoLongXor(*solver.xorclauses[*it]); - if (twoLongXors.find(tmp) != twoLongXors.end()) { - tmpPs[0] = Lit(tmp.var[0], false); - tmpPs[1] = Lit(tmp.var[1], false); - binXorToAdd.push_back(BinXorToAdd(tmpPs[0], tmpPs[1], tmp.inverted)); - newBinXor += solver.varReplacer->getNewToReplaceVars() - toReplaceBefore; - toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); - } - } - } - } - for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { - addVarFromXors(solver.trail[c].var()); - } - } - solver.cancelUntilLight(); - - if (solver.conf.doHyperBinRes) { - if (hyperbinProps < maxHyperBinProps) hyperBinResolution(lit2); - unPropagatedBin.removeThese(propagatedVars); - propagatedVars.clear(); - } - - for(uint32_t i = 0; i != bothSame.size(); i++) { - solver.uncheckedEnqueue(bothSame[i]); - } - goodBothSame += bothSame.size(); - solver.ok = (solver.propagate<false>(false).isNULL()); - if (!solver.ok) return false; - - if (solver.conf.doBXor) { - for (uint32_t i = 0; i < binXorToAdd.size(); i++) { - tmpPs[0] = binXorToAdd[i].lit1; - tmpPs[1] = binXorToAdd[i].lit2; - solver.addXorClauseInt(tmpPs, binXorToAdd[i].isEqualFalse); - tmpPs.clear(); - tmpPs.growTo(2); - if (!solver.ok) return false; - } - } - - return true; -} - -/** -@brief Adds hyper-binary clauses - -At this point, unPropagatedBin is set, and propagatedVars is filled with lits -that have been propagated. Here, we propagate ONLY at the binary level, -and compare with propagatedVars and unPropagatedBin. If they match, it's OK. If -not, then we add the relevant binary clauses at the right point. The "right" -point is the point which has the highest in-degree. We approximated the degrees -beforehand with orderLits() -*/ -void FailedLitSearcher::hyperBinResolution(const Lit lit) -{ - #ifdef VERBOSE_DEBUG - std::cout << "Checking one BTC vs UP" << std::endl; - #endif //VERBOSE_DEBUG - - #ifdef DEBUG_HYPERBIN - assert(needToVisit.isZero()); - #endif //DEBUG_HYPERBIN - - uint64_t oldProps = solver.propagations; - vec<Lit> toVisit; - uint64_t extraTime = 0; - - solver.newDecisionLevel(); - solver.uncheckedEnqueueLight2(lit, 0, lit_Undef, false); - failed = (!solver.propagateBin(uselessBin).isNULL()); - assert(!failed); - - if (solver.conf.doRemUselessLBins && !uselessBin.empty()) { - for (const Lit *it = uselessBin.getData(), *end = uselessBin.getDataEnd(); it != end; it++) { - if (dontRemoveAncestor[it->var()]) continue; - - extraTime += solver.watches[lit.toInt()].size()/2; - extraTime += solver.watches[(~*it).toInt()].size()/2; - if (findWBin(solver.watches, ~lit, *it, true)) { - removeWBin(solver.watches[lit.toInt()], *it, true); - removeWBin(solver.watches[(~*it).toInt()], ~lit, true); - solver.learnts_literals -= 2; - solver.numBins--; - removedUselessLearnt++; - } else if (!solver.binPropData[it->var()].learntLeadHere) { - removeWBin(solver.watches[lit.toInt()], *it, false); - removeWBin(solver.watches[(~*it).toInt()], ~lit, false); - solver.clauses_literals -= 2; - solver.numBins--; - removedUselessNonLearnt++; - } else { - continue; - } - - Var ancestorVar = solver.binPropData[it->var()].lev1Ancestor.var(); - dontRemoveAncestor.setBit(ancestorVar); - toClearDontRemoveAcestor.push(ancestorVar); - } - dontRemoveAncestor.removeThese(toClearDontRemoveAcestor); - toClearDontRemoveAcestor.clear(); - } - uselessBin.clear(); - #ifdef DEBUG_USELESS_LEARNT_BIN_REMOVAL - dontRemoveAncestor.isZero(); - uint64_t backupProps; - #endif - - assert(solver.decisionLevel() > 0); - int32_t difference = propagatedVars.size() - (solver.trail.size()-solver.trail_lim[0]); - #ifdef DEBUG_USELESS_LEARNT_BIN_REMOVAL - uint32_t propagated = solver.trail.size()-solver.trail_lim[0]; - #endif - assert(difference >= 0); - if (difference == 0) { - solver.cancelUntilLight(); - goto end; - } - for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { - Lit x = solver.trail[c]; - unPropagatedBin.clearBit(x.var()); - toVisit.push(x); - needToVisit.setBit(x.var()); - } - std::sort(toVisit.getData(), toVisit.getDataEnd(), LitOrder2(solver.binPropData)); - solver.cancelUntilLight(); - - #ifdef DEBUG_USELESS_LEARNT_BIN_REMOVAL - backupProps = solver.propagations; - if (solver.conf.doRemUselessLBins) { - solver.newDecisionLevel(); - solver.uncheckedEnqueueLight2(lit, 0, lit_Undef, false); - failed = (!solver.propagateBin(uselessBin).isNULL()); - uselessBin.clear(); - for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { - Lit x = solver.trail[c]; - } - assert(!failed); - assert(propagated == solver.trail.size()-solver.trail_lim[0]); - solver.cancelUntilLight(); - } - solver.propagations = backupProps; - #endif - - /************************* - //To check that the ordering is the right way - // --> i.e. to avoid mistake present in Glucose's ordering*/ - /*std::cout << "--------------------" << std::endl; - for (uint32_t i = 0; i < toVisit.size(); i++) { - std::cout << "i:" << std::setw(8) << i - << " level:" << std::setw(3) << solver.binPropData[toVisit[i].var()].lev - << " lit : " << toVisit[i] - << std::endl; - } - std::cout << "difference: " << difference << std::endl; - std::cout << "--------------------" << std::endl;*/ - /***************************/ - - //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); - //addMyImpliesSetAsBins(*l, difference); - 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--; - } - - - assert(difference >= 0); - myImpliesSet.clear(); - - if (difference == 0) { - needToVisit.removeTheseLit(toVisit); - break; - } - } - #ifdef DEBUG_HYPERBIN - assert(unPropagatedBin.isZero()); - assert(needToVisit.isZero()); - #endif //DEBUG_HYPERBIN - - end: - hyperbinProps += solver.propagations - oldProps + extraTime; -} - -/** -@brief Fills myimplies and myimpliesSet by propagating lit at a binary level - -Used to check which variables are propagated by a certain literal when -propagating it only at the binary level -@p[in] the literal to be propagated at the binary level -*/ -void FailedLitSearcher::fillImplies(const Lit lit) -{ - solver.newDecisionLevel(); - solver.uncheckedEnqueueLight(lit); - failed = (!solver.propagate<false>(false).isNULL()); - assert(!failed); - - assert(solver.decisionLevel() > 0); - for (int sublevel = solver.trail.size()-1; sublevel >= (int)solver.trail_lim[0]; sublevel--) { - Var x = solver.trail[sublevel].var(); - needToVisit.clearBit(x); - if (unPropagatedBin[x]) { - myImpliesSet.push(x); - } - } - solver.cancelUntilLight(); -} - -/*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; - } - - uint64_t backupProps = solver.propagations; - vector<BinAddData> 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<BinAddData>::iterator it2 = litsAddedEach.begin(); it2 != litsAddedEach.end(); it2++) { - if (it2->lit == alsoAddedLit) { - litsAddedEach.erase(it2); - break; - } - } - } - } - } - assert(litsAddedEach.empty()); - solver.propagations = backupProps; -}*/ - - -/** -@brief Adds a learnt binary clause to the solver - -Used by hyperBinResolution() to add the newly discovered clauses -*/ -void FailedLitSearcher::addBin(const Lit lit1, const Lit lit2) -{ - #ifdef VERBOSE_DEBUG - std::cout << "Adding extra bin: " << lit1 << " " << lit2 << std::endl; - #endif //VERBOSE_DEBUG - - assert(solver.value(lit1) == l_Undef); - assert(solver.value(lit2) == l_Undef); - tmpPs[0] = lit1; - tmpPs[1] = lit2; - - solver.addClauseInt(tmpPs, true); - tmpPs.clear(); - tmpPs.growTo(2); - assert(solver.ok); - addedBin++; -} |