return *this;
}
+ template<class T>
+ 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);
--- /dev/null
+/***************************************************************************
+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 <http://www.gnu.org/licenses/>.
+*****************************************************************************/
+
+#include "BothCache.h"
+#include "time_mem.h"
+#include <iomanip>
+#include "VarReplacer.h"
+#include "Subsumer.h"
+#include "XorSubsumer.h"
+#include "PartHandler.h"
+
+BothCache::BothCache(Solver& _solver) :
+ solver(_solver)
+{};
+
+const bool BothCache::tryBoth(const vector<TransCache>& cache)
+{
+ vec<bool> seen(solver.nVars(), 0);
+ vec<bool> val(solver.nVars(), 0);
+ vec<Lit> 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<LitExtra> const* cache1;
+ vector<LitExtra> 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<LitExtra>::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<LitExtra>::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<LitExtra>::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
--- /dev/null
+#ifndef BOTHCACHE_H
+#define BOTHCACHE_H
+
+#include "Solver.h"
+
+class BothCache
+{
+ public:
+ BothCache(Solver& solver);
+ const bool tryBoth(const vector<TransCache>& cache);
+
+ private:
+ Solver& solver;
+};
+
+#endif //BOTHCACHE_H
\ No newline at end of file
class ClauseSimp
{
public:
+ ClauseSimp() {};
ClauseSimp(Clause* c, const uint32_t _index) :
clause(c)
, index(_index)
uint32_t isRemoved:1; ///<Is this clause queued for removal because of usless binary removal?
uint32_t isFreed:1; ///<Has this clause been marked as freed by the ClauseAllocator ?
uint32_t glue:MAX_GLUE_BITS; ///<Clause glue -- clause activity according to GLUCOSE
- uint32_t mySize:19; ///<The current size of the clause
-
- float miniSatAct; ///<Clause activity according to MiniSat
+ uint32_t mySize:18; ///<The current size of the clause
uint32_t abst; //Abstraction of clause
uint32_t group;
#endif
- #ifdef _MSC_VER
- Lit data[1];
- #else
/**
@brief Stores the literals in the clause
glue, etc. We allocate therefore the clause manually, taking care that
there is enough space for data[] to hold the literals
*/
+ #ifdef __GNUC__
Lit data[0];
- #endif //_MSC_VER
+ #else
+ //NOTE: Dangerous packing. We love C++. More info: stackoverflow.com/questions/688471/variable-sized-struct-c
+ Lit data[1];
+ #endif //__GNUC__
#ifdef _MSC_VER
public:
setGroup(_group);
memcpy(data, ps.getData(), ps.size()*sizeof(Lit));
- miniSatAct = 0;
+ glue = MAX_THEORETICAL_GLUE;
setStrenghtened();
}
return isLearnt;
}
- float& getMiniSatAct()
- {
- return miniSatAct;
- }
-
- void setMiniSatAct(const float newMiniSatAct)
- {
- miniSatAct = newMiniSatAct;
- }
-
- const float& getMiniSatAct() const
- {
- return miniSatAct;
- }
-
const bool getStrenghtened() const
{
return strenghtened;
isLearnt = false;
}
- void makeLearnt(const uint32_t newGlue, const float newMiniSatAct)
+ void makeLearnt(const uint32_t newGlue)
{
glue = newGlue;
- miniSatAct = newMiniSatAct;
isLearnt = true;
}
setStrenghtened();
}
+ inline void add(const Lit p)
+ {
+ mySize++;
+ data[mySize-1] = p;
+ setStrenghtened();
+ }
+
void calcAbstractionClause()
{
abst = calcAbstraction(*this);
}
- uint32_t getAbst()
+ const uint32_t getAbst() const
{
return abst;
}
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
{
for (uint32_t i = 0; i < size(); i++) {
- if (data[i].sign()) fprintf(to, "-");
- fprintf(to, "%d ", data[i].var() + 1);
+ data[i].print(to);
}
fprintf(to, "0\n");
}
{
if (other.getGlue() < getGlue())
setGlue(other.getGlue());
- if (other.getMiniSatAct() > getMiniSatAct())
- setMiniSatAct(other.getMiniSatAct());
}
};
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
//#include "VarReplacer.h"
#include "PartHandler.h"
#include "Gaussian.h"
+#include <sys/mman.h>
//For mild debug info:
//#define DEBUG_CLAUSEALLOCATOR
ClauseAllocator::ClauseAllocator()
{
assert(MIN_LIST_SIZE < MAXSIZE);
- assert(sizeof(Clause) + 2*sizeof(Lit) > sizeof(NewPointerAndOffset));
+ assert(sizeof(Clause) + 2*sizeof(Lit) >= sizeof(NewPointerAndOffset));
}
/**
ClauseAllocator::~ClauseAllocator()
{
for (uint32_t i = 0; i < dataStarts.size(); i++) {
- delete [] dataStarts[i];
+ free(dataStarts[i]);
}
}
template<class T>
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;
}
<< ")" << 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);
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);
}
updateAllOffsetsAndPointers(solver);
for (uint32_t i = 0; i < dataStarts.size(); i++)
- delete [] dataStarts[i];
+ free(dataStarts[i]);
dataStarts.clear();
maxSizes.clear();
__builtin_prefetch(*(s+1), 1, 0);
if (cleanClause(*s)) {
solver.clauseAllocator.clauseFree(*s);
+ if (type == learnts) solver.nbCompensateSubsumer++;
} else {
*ss++ = *s;
}
} 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;
, 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.)
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;
}
}
done += i2;
- failed = (!solver.propagate(false).isNULL());
- if (numCalls > 3 && failed) break;
+ failed = (!solver.propagate<false>(false).isNULL());
+ if (failed) break;
}
solver.cancelUntilLight();
assert(solver.ok);
}
-const bool ClauseVivifier::vivifyClauses2(vec<Clause*>& clauses)
+const bool ClauseVivifier::vivifyClausesCache(vec<Clause*>& clauses)
{
assert(solver.ok);
vec<Lit> lits;
bool needToFinish = false;
double myTime = cpuTime();
-
- if (numCalls < 3) return true;
+ const vector<TransCache>& cache = solver.transOTFCache;
Clause** i = clauses.getData();
Clause** j = i;
if (seen[l->toInt()] == 0) continue;
Lit lit = *l;
- countTime += solver.transOTFCache[l->toInt()].lits.size();
- for (vector<Lit>::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<LitExtra>::const_iterator it2 = cache[l->toInt()].lits.begin()
+ , end2 = cache[l->toInt()].lits.end(); it2 != end2; it2++) {
+ seen[(~(it2->getLit())).toInt()] = 0;
}
}
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;
class ClauseVivifier {
public:
ClauseVivifier(Solver& solver);
- const bool vivifyClauses();
- const bool vivifyClauses2(vec<Clause*>& clauses);
+ const bool vivify();
+ const bool vivifyClausesCache(vec<Clause*>& clauses);
private:
+ //Actual algorithms used
+ const bool vivifyClausesNormal();
+
/**
@brief Records data for asymmBranch()
cleanAndAttachClauses(solver.xorclauses);
solver.clauseCleaner->removeSatisfiedBins();
- if (solver.ok) solver.ok = (solver.propagate().isNULL());
+ if (solver.ok) solver.ok = (solver.propagate<true>().isNULL());
return solver.ok;
}
#include "Subsumer.h"
#include "VarReplacer.h"
#include "XorSubsumer.h"
+#include "PartHandler.h"
#include <iomanip>
+#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;
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()
|| solver.value(lit1.var()) != l_Undef
) continue;
- vector<Lit>& bins = shared.bins[wsLit];
- vec<Watched>& ws = solver.watches[wsLit];
+ vector<BinClause>& 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();
}
template <class T>
-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<Lit>& 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<Lit>& ps);
+template<class T>
+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<Lit>& ps, const bool learnt);
-const bool DataSync::syncBinFromOthers(const Lit lit, const vector<Lit>& bins, uint32_t& finished, vec<Watched>& 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<TriClause>& 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<TriClause>& 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<Lit> 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<Watched>& 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<Watched>& 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<TriClause>::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<TriClause>& tris = sharedData->tris[(~lit1).toInt()];
+ for (vector<TriClause>::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<BinClause>& 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<Lit> addedToSeen;
- for (Watched *it = ws.getData(), *end = ws.getDataEnd(); it != end; it++) {
+ const vec<Watched>& 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<LitExtra>& cache = solver.transOTFCache[(~lit).toInt()].lits;
+ for (vector<LitExtra>::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) {
+ addedToSeen.push(it->getLit());
+ seen[it->getLit().toInt()] = true;
+ }
vec<Lit> 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;
void DataSync::syncBinToOthers()
{
- for(vector<std::pair<Lit, Lit> >::const_iterator it = newBinClauses.begin(), end = newBinClauses.end(); it != end; it++) {
- addOneBinToOthers(it->first, it->second);
+ for(vector<BinClause>::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<Lit>& bins = sharedData->bins[(~lit1).toInt()];
- for (vector<Lit>::const_iterator it = bins.begin(), end = bins.end(); it != end; it++) {
- if (*it == lit2) return;
+ vector<BinClause>& bins = sharedData->bins[(~lit1).toInt()];
+ for (vector<BinClause>::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()
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<true>().isNULL();
if (!solver.ok) return false;
thisGotUnitData++;
continue;
void newVar();
const bool syncData();
+ //New clause signalation
+ template <class T> void signalNewBinClause(const T& ps, const bool learnt = true);
+ void signalNewBinClause(Lit lit1, Lit lit2, const bool learnt = true);
+ template <class T> 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 <class T> 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<Lit>& bins, uint32_t& finished, vec<Watched>& ws);
- void syncBinToOthers();
- void addOneBinToOthers(const Lit lit1, const Lit lit2);
- const bool shareBinData();
+ uint32_t sentUnitData;
+ uint32_t recvUnitData;
- //stuff to sync
- vector<std::pair<Lit, Lit> > newBinClauses;
+ //bin sharing functions
+ const bool shareBinData();
+ vector<BinClause> newBinClauses;
+ const bool syncBinFromOthers(const Lit lit, const vector<BinClause>& bins, uint32_t& finished);
+ void syncBinToOthers();
+ void addOneBinToOthers(const Lit lit1, const Lit lit2, const bool leanrt);
+ vec<uint32_t> syncFinish;
+ uint32_t sentBinData;
+ uint32_t recvBinData;
+
+ //tri sharing functions
+ const bool shareTriData();
+ vector<TriClause> newTriClauses;
+ const bool syncTriFromOthers(const Lit lit1, const vector<TriClause>& tris, uint32_t& finished);
+ void syncTriToOthers();
+ void addOneTriToOthers(const Lit lit1, const Lit lit2, const Lit lit3);
+ vec<uint32_t> syncFinishTri;
+ uint32_t sentTriData;
+ uint32_t recvTriData;
+
+ //ER sharing
+ void syncERVarsToHere();
+ void syncERVarsFromHere();
//stats
uint64_t lastSyncConf;
- vec<uint32_t> syncFinish;
- uint32_t sentUnitData;
- uint32_t recvUnitData;
- uint32_t sentBinData;
- uint32_t recvBinData;
+ uint32_t numCalls;
//misc
vec<char> seen;
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;
+}
#include <iostream>
#include <iomanip>
-#include "Solver.h"
+#include "MTSolver.h"
#ifdef VERBOSE_DEBUG
#define DEBUG_COMMENT_PARSING
//#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)
{}
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;
}
/**
@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;
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;
{
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;
++in;
parseString(in, str);
if (str == "clause") {
- parseClauseParameters(in, learnt, glue, miniSatAct);
+ parseClauseParameters(in, learnt, glue);
} else {
needToParseComments = true;
}
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());
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, "
#include "Logger.h"
#endif //STATS_NEEDED
-class Solver;
+class MTSolver;
/**
@brief Parses up a DIMACS file that my be zipped
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 <class T>
void parse_DIMACS(T input_stream);
float parseFloat(StreamBuffer& in);
void parseString(StreamBuffer& in, std::string& str);
void readClause(StreamBuffer& in, vec<Lit>& 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);
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; ///<printing partial solutions to debugLibPart1..N.output when "debugLib" is set to TRUE
uint32_t groupId;
#include "ClauseCleaner.h"
#include "StateSaver.h"
#include "CompleteDetachReattacher.h"
+#include "PartHandler.h"
+#include "BothCache.h"
#ifdef _MSC_VER
#define __builtin_prefetch(a,b,c)
{
assert(solver.decisionLevel() == 0);
if (solver.nVars() == 0) return solver.ok;
+ if (solver.conf.doCacheOTFSSR && numCalls > 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();
//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;
}
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])
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));
reattacher.detachNonBinsNonTris(true);
const bool ret = reattacher.reattachNonBins();
release_assert(ret == true);
- removedOldLearnts = true;
} else {
solver.clauseCleaner->removeAndCleanAll();
}
" 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;
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();
solver.newDecisionLevel();
solver.uncheckedEnqueueLight(lit1);
- failed = (!solver.propagate(false).isNULL());
+ failed = (!solver.propagate<false>(false).isNULL());
if (failed) {
solver.cancelUntilLight();
numFailed++;
solver.uncheckedEnqueue(~lit1);
- solver.ok = (solver.propagate(false).isNULL());
+ solver.ok = (solver.propagate<true>().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<Lit> oldCache;
+ vector<LitExtra> 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);
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++) {
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>(false).isNULL());
if (failed) {
solver.cancelUntilLight();
numFailed++;
solver.uncheckedEnqueue(~lit2);
- solver.ok = (solver.propagate(false).isNULL());
+ solver.ok = (solver.propagate<true>().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<LitExtra> lit2OTFCache;
for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
Var x = solver.trail[c].var();
if (propagated[x]) {
//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();
}
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
}
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<true>().isNULL());
if (!solver.ok) return false;
for (uint32_t i = 0; i < binXorToAdd.size(); i++) {
return true;
}
+const bool FailedLitSearcher::performAddBinLaters()
+{
+ assert(solver.ok);
+ for (vector<std::pair<Lit, Lit> >::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<Lit>& oldCache*/)
+{
+ /*if (solver.conf.doAddBinCache) {
+ //Not forgetting stuff already known at one point from cache
+ for (vector<Lit>::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
continue;
}
- Var ancestorVar = solver.binPropData[it->var()].lev2Ancestor.var();
+ Var ancestorVar = solver.binPropData[it->var()].lev1Ancestor.var();
dontRemoveAncestor.setBit(ancestorVar);
toClearDontRemoveAcestor.push(ancestorVar);
}
//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
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<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());
+}
+
/**
@brief Fills myimplies and myimpliesSet by propagating lit at a binary level
{
solver.newDecisionLevel();
solver.uncheckedEnqueueLight(lit);
- failed = (!solver.propagate(false).isNULL());
+ failed = (!solver.propagate<false>(false).isNULL());
assert(!failed);
assert(solver.decisionLevel() > 0);
assert(solver.ok);
addedBin++;
}
+
+void FailedLitSearcher::fillToTry(vec<Var>& 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<std::pair<uint64_t, uint64_t> >::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<Var> 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<Var>& vars, uint32_t& enqueued, uint32_t& finished, uint32_t& numFailed)
+{
+ assert(solver.ok);
+
+ vec<Lit> 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>(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<true>().isNULL();
+ //exit(-1);
+
+ return solver.ok;
+}
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; ///<The solver we are updating&working with
bool failed; ///<For checking that a specific propagation failed (=conflict). It is used in many places
//bothprop finding
+ vector<uint32_t> propagatedBitSet;
BitArray propagated; ///<These lits have been propagated by propagating the lit picked
+ BitArray propagated2; ///<These lits have been propagated by propagating the lit picked
BitArray propValue; ///<The value (0 or 1) of the lits propagated set in "propagated"
/**
@brief Lits that have been propagated to the same value both by "var" and "~var"
const vec<BinPropData>& binPropData;
};
+ struct BinAddData
+ {
+ vector<Lit> 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<Lit>& oldCache*/);
void hyperBinResolution(const Lit lit);
BitArray unPropagatedBin;
BitArray needToVisit;
void fillImplies(const Lit lit);
vec<Var> myImpliesSet; ///<variables set in myimplies
uint64_t hyperbinProps; ///<Number of bogoprops done by the hyper-binary resolution function hyperBinResolution()
+ void addMyImpliesSetAsBins(Lit lit, int32_t& difference);
+
+ //Cache equivalence within hyperbin
+ const bool performAddBinLaters();
+ vector<std::pair<Lit, Lit> > addBinLater;
+ uint32_t addedCacheBin;
//bin-removal within hyper-bin-res
vec<Lit> uselessBin;
*/
uint64_t maxHyperBinProps;
+ //Multi-level
+ void calcNegPosDist();
+ const bool tryMultiLevel(const vec<Var>& vars, uint32_t& enqueued, uint32_t& finished, uint32_t& numFailed);
+ const bool tryMultiLevelAll();
+ void fillToTry(vec<Var>& toTry);
+
//Temporaries
vec<Lit> tmpPs;
case propagation:
unit_truths += last_trail_size - solver.trail.size();
do_again_gauss = true;
- solver.ok = (solver.propagate().isNULL());
+ solver.ok = (solver.propagate<true>().isNULL());
if (!solver.ok) return false;
break;
case nothing:
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:"
#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;
Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint32_t last_row, PropBy& confl)
{
- int32_t maxlevel = std::numeric_limits<int32_t>::max();
+ uint32_t maxlevel = std::numeric_limits<uint32_t>::max();
uint32_t size = UINT_MAX;
uint32_t best_row = UINT_MAX;
analyse_confl(m, row, maxlevel, size, best_row);
}
- if (maxlevel != std::numeric_limits<int32_t>::max())
+ if (maxlevel != std::numeric_limits<uint32_t>::max())
return handle_matrix_confl(confl, m, size, maxlevel, best_row);
#ifdef DEBUG_GAUSS
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);
}
#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);
#endif
#endif
- int32_t this_maxlevel = 0;
+ uint32_t this_maxlevel = 0;
unsigned long int var = 0;
uint32_t this_size = 0;
while (true) {
|| (this_maxlevel == maxlevel && this_size < size)
|| (this_size <= 1)
)) {
- assert(maxlevel != std::numeric_limits<int32_t>::max());
+ assert(maxlevel != std::numeric_limits<uint32_t>::max());
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")Other found conflict just as good or better.";
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
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;
}
//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<Lit> tmp_clause;
ret.resize(len-1);
len--;
}
-
+
if (len > SND_WIDTH-3) {
ret[SND_WIDTH-3] = '\0';
ret[SND_WIDTH-4] = '.';
{
if (!statistics_on && !proof_graph_on)
return;
-
+
string name;
if (name_tmp == NULL) return;
else name = name_tmp;
}
// 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) {
{
if (begin_called)
return;
-
+
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 {
{
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,"-");
else
fprintf(proof,"%s\"", groupnames[group].c_str());
fprintf(proof,"];\n");
-
+
if (!mini_proof)
history.resize(goback_sublevel+1);
else
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()]++;
{
first_begin();
assert(!(proof == NULL && proof_graph_on));
-
+
uint group;
prop_type type;
if (c == NULL) {
//graph
if (proof_graph_on && (!mini_proof || type == guess_type)) {
uniqueid++;
-
+
fprintf(proof,"node%d [shape=box, label=\"",uniqueid);;
if (lit.sign())
fprintf(proof,"-");
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;
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;
{
first_begin();
assert(!(proof == NULL && proof_graph_on));
-
+
if (proof_graph_on) {
uniqueid++;
switch (finish) {
if (finish == restarting)
reset_statistics();
}
-
+
if (model_found || unsat_model_found)
begin_called = false;
}
uint i = 0;
for (vector<pair<double, uint> >::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();
}
for (vector<pair<uint, uint> >::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();
}
ofstream branch_depth_file;
branch_depth_file.open(ss.str().c_str());
i = 0;
-
+
for (map<uint, uint>::iterator it = range_stat.begin(); it != range_stat.end(); it++, i++) {
std::stringstream ss2;
ss2 << it->first*range << " - " << it->first*range + range-1;
{
map<uint, uint> learnt_sizes;
const vec<Clause*>& 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<uint, uint>::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<uint, uint>::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);
}
hmax = std::max(hmax, sum);
}
slices.resize(no_slices, 0);
-
+
uint height = max_print_lines;
uint hslice = (hmax+1)/height + (bool)((hmax+1)%height);
if (hslice == 0) return;
-
+
print_simple_line(" Learnt clause distribution in graph form");
print_footer();
string yaxis = "Number";
uint middle = (height-yaxis.size())/2;
-
+
for (int i = height-1; i > 0; i--) {
cout << "| ";
if (height-1-i >= middle && height-1-i-middle < yaxis.size())
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();
print_footer();
print_simple_line(" Matrix statistics");
print_footer();
-
+
uint i = 0;
for (vector<Gaussian*>::const_iterator it = S->gauss_matrixes.begin(), end = S->gauss_matrixes.end(); it != end; it++, i++) {
std::stringstream s;
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
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();
}
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<uint>::iterator vecit;
for (vecit it = times_var_guessed.begin(); it != times_var_guessed.end(); it++)
*it = 0;
}
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;
sum(0)
, num(0)
{}
-
+
uint sum;
uint num;
};
//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);
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<pair<uint, uint> >& to_print) const;
void print_groups(const vector<pair<double, uint> >& to_print) const;
void print_vars(const vector<pair<uint, uint> >& to_print) const;
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;
//message display properties
const int& verbosity;
-
+
const Solver* S;
-
+
void first_begin();
bool begin_called;
uint proofStarts;
--- /dev/null
+/***************************************************************************
+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 <http://www.gnu.org/licenses/>.
+*****************************************************************************/
+
+#include "MTSolver.h"
+
+#include <set>
+#include <omp.h>
+#include <time.h>
+#include <algorithm>
+
+#if defined( _WIN32 ) || defined( _WIN64 )
+#include <windows.h>
+#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<Lit>& assumps)
+{
+ std::set<uint32_t> 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<Lit> 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<class T> 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<Lit> 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<Lit>& ps, const uint32_t group, const char* group_name);
+template bool MTSolver::addClause(Clause& ps, const uint32_t group, const char* group_name);
+
+template<class T> 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<Lit> 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<Lit>& 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<class T> 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<Lit> 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<Lit>& 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.
+
--- /dev/null
+/***************************************************************************
+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 <http://www.gnu.org/licenses/>.
+*****************************************************************************/
+
+#include "Solver.h"
+#include "SharedData.h"
+#include <string>
+
+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<class T>
+ 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<class T>
+ bool addLearntClause(T& ps, const uint32_t group = 0, const char* group_name = NULL, const uint32_t glue = 10);
+ template<class T>
+ 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<Lit>& assumps); ///<Search for a model that respects a given set of assumptions.
+ const lbool solve (); ///<Search without assumptions.
+ const bool okay () const; ///<FALSE means solver is in a conflicting state
+
+ // Variable mode:
+ //
+ void setDecisionVar (Var v, bool b); ///<Declare if a variable should be eligible for selection in the decision heuristic.
+
+ // Read state:
+ //
+ const lbool modelValue (const Lit p) const; ///<The value of a literal in the last model. The last call to solve must have been satisfiable.
+ const uint32_t nAssigns () const; ///<The current number of assigned literals.
+ const uint32_t nClauses () const; ///<The current number of original clauses.
+ const uint32_t nLiterals () const; ///<The current number of total literals.
+ const uint32_t nLearnts () const; ///<The current number of learnt clauses.
+ const uint32_t nVars () const; ///<The current number of variables.
+
+ // Extra results: (read-only member variable)
+ //
+ vec<lbool> model; ///<If problem is satisfiable, this vector contains the model (if any).
+ vec<Lit> conflict; ///<If problem is unsatisfiable (possibly under assumptions), this vector represent the final conflict clause expressed in the assumptions.
+
+ //Logging
+ void needStats(); // Prepares the solver to output statistics
+ void needProofGraph(); // Prepares the solver to output proof graphs during solving
+ void setVariableName(const Var var, const std::string& name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger')
+ const vec<Clause*>& 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<Clause*>& get_learnts() const; //Get all learnt clauses that are >1 long
+ const vector<Lit> 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; ///<Get number of variables eliminated
+ const uint32_t getNumElimXorSubsume() const; ///<Get number of variables eliminated with xor-magic
+ const uint32_t getNumXorTrees() const; ///<Get the number of trees built from 2-long XOR-s. This is effectively the number of variables that replace other variables
+ const uint32_t getNumXorTreesCrownSize() const; ///<Get the number of variables being replaced by other variables
+ /**
+ @brief Get total time spent in Subsumer.
+
+ This includes: subsumption, self-subsuming resolution, variable elimination,
+ blocked clause elimination, subsumption and self-subsuming resolution
+ using non-existent binary clauses.
+ */
+ const double getTotalTimeSubsumer() const;
+ const double getTotalTimeFailedLitSearcher() const;
+ const double getTotalTimeSCC() const;
+
+ /**
+ @brief Get total time spent in XorSubsumer.
+
+ This included subsumption, variable elimination through XOR,
+ and local&global substitution (see Heule's Thesis)
+ */
+ const double getTotalTimeXorSubsumer() const;
+ const uint32_t getVerbosity() const;
+ void setNeedToInterrupt();
+ const bool getNeedToDumpLearnts() const;
+ const bool getNeedToDumpOrig() const;
+
+ void printNumThreads() const;
+
+ private:
+ void setUpFinish(const lbool retVal, const int threadNum);
+
+ SolverConf conf;
+ GaussConf gaussConfig;
+
+
+ int numThreads;
+ void setupOneSolver(const int num);
+ std::vector<Solver*> 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<Lit> 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();
+}
#include <sstream>
#include <iostream>
#include <iomanip>
-#include <omp.h>
#ifdef _MSC_VER
#include <msvc/stdint.h>
#else
{
}
-std::map<uint32_t, Solver*> solversToInterrupt;
+MTSolver* solversToInterrupt;
std::set<uint32_t> finished;
/**
*/
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;
}
#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
-void Main::parseInAllFiles(Solver& solver)
+void Main::parseInAllFiles(MTSolver& solver)
{
double myTime = cpuTime();
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;
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");
}
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) {
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) {
}
}
-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);
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);
signal(SIGINT, SIGINT_handler);
//signal(SIGHUP,SIGINT_handler);
- if (main.numThreads == 1)
- return main.singleThreadSolve();
- else
- return main.multiThreadSolve();
+ return main.solve();
}
#include <zlib.h>
#endif // DISABLE_ZLIB
-#include "Solver.h"
+#include "MTSolver.h"
#include "SharedData.h"
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);
SolverConf conf;
GaussConf gaussconfig;
+ int numThreads;
bool grouping;
bool debugLib;
bool twoFileNamesPresent;
std::vector<std::string> filesToRead;
- SharedData sharedData;
-
int argc;
char** argv;
};
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
if (!solver.ok) return false;
}
+ removeVarsOnlyInLearnts();
addToPart(solver.clauses);
addToPartBins();
addToPart(solver.xorclauses);
+ //checkLearntBinAdded();
+
const uint32_t parts = setParts();
#ifndef NDEBUG
return true;
}
+void PartFinder::checkLearntBinAdded()
+{
+ uint32_t wsLit = 0;
+ for (vec<Watched> *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) {
+ Lit lit = ~Lit::toLit(wsLit);
+ vec<Watched>& 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<uint32_t>::max()
+ || table[i->getOtherLit().var()] == std::numeric_limits<uint32_t>::max()
+ ) {
+ std::cout << " max: " << lit << " , " << i->getOtherLit() << std::endl;
+ }
+ }
+ }
+ }
+}
+
+void PartFinder::removeVarsOnlyInLearnts()
+{
+ vec<char> usedVar(solver.nVars(), false);
+
+ addClausesToUsed(solver.clauses, usedVar);
+ addClausesToUsed(solver.xorclauses, usedVar);
+ addBinsToUsed(usedVar);
+
+ removeLearntClausesNotInVars(usedVar);
+ removeBinClausesNotInVars(usedVar);
+}
+
+void PartFinder::removeLearntClausesNotInVars(vec<char>& 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<char>& usedVar)
+{
+ uint64_t removedHalfLearnt = 0;
+
+ uint32_t wsLit = 0;
+ for (vec<Watched> *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) {
+ Lit lit = ~Lit::toLit(wsLit);
+ vec<Watched>& 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<class T>
+void PartFinder::addClausesToUsed(const vec<T*>& cs, vec<char>& 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<char>& usedVar)
+{
+ uint32_t wsLit = 0;
+ for (const vec<Watched> *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) {
+ Lit lit = ~Lit::toLit(wsLit);
+ const vec<Watched>& 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<class T>
void PartFinder::addToPart(const vec<T*>& cs)
{
lits[0] = lit;
const vec<Watched>& 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);
}
}
template<class T>
-void PartFinder::addToPartClause(T& cl)
+void PartFinder::addToPartClause(const T& cl)
{
set<uint32_t> tomerge;
vector<Var> newSet;
const vector<Var>& getPartVars(const uint32_t part);
private:
+ //removing learnt clauses that contain vars that are no longer in any clauses
+ void removeVarsOnlyInLearnts();
+ template<class T>
+ void addClausesToUsed(const vec<T*>& cs, vec<char>& usedVar);
+ void addBinsToUsed(vec<char>& usedVar);
+ void removeLearntClausesNotInVars(vec<char>& usedVar);
+ void removeBinClausesNotInVars(vec<char>& usedVar);
+ void checkLearntBinAdded();
+
const uint32_t setParts();
void addToPartBins();
- template<class T> void addToPartClause(T& cl);
+ template<class T> void addToPartClause(const T& cl);
template<class T> void addToPart(const vec<T*>& cs);
struct mysorter
inline const uint32_t PartFinder::getVarPart(const Var var) const
{
+ if (var >= table.size()) return false;
return table[var];
}
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();
//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);
}
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<true>().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());
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;
}
/**
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;
}
}
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);
}
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 {
The variables that form part of the part will determine if the clause is in the
part or not
*/
-void PartHandler::moveClauses(vec<XorClause*>& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder)
+void PartHandler::moveXorClauses(vec<XorClause*>& 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++) {
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<Clause*>& 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
//For moving clauses
void moveBinClauses(Solver& newSolver, const uint32_t part, PartFinder& partFinder);
- void moveClauses(vec<XorClause*>& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder);
+ void moveXorClauses(vec<XorClause*>& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder);
void moveClauses(vec<Clause*>& cs, Solver& newSolver, const uint32_t part, PartFinder& partFinder);
- void moveLearntClauses(vec<Clause*>& 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;
RestartTypeChooser::RestartTypeChooser(const Solver& s) :
solver(s)
- , topX(100)
- , limit(40)
+ , topXPerc(0.01)
+ , limitPerc(0.0018)
{
}
*/
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;
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) <<std::endl;
+ std::cout << "c Avg same vars in first&second: " << avg() << " standard Deviation:" << stdDeviation(sameIns) <<std::endl;
#endif
}
*/
const RestartType RestartTypeChooser::choose()
{
- pair<double, double> 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<double, double> 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;
+ }
}
/**
void RestartTypeChooser::calcHeap()
{
firstVars.clear();
- firstVars.reserve(topX);
#ifdef PRINT_VARS
std::cout << "First vars:" << std::endl;
#endif
#endif
}
-const std::pair<double, double> RestartTypeChooser::countVarsDegreeStDev() const
+/*const std::pair<double, double> RestartTypeChooser::countVarsDegreeStDev() const
{
vector<uint32_t> degrees;
degrees.resize(solver.nVars(), 0);
}
}
}
-}
+}*/
private:
void calcHeap();
const double avg() const;
- const std::pair<double, double> countVarsDegreeStDev() const;
const double stdDeviation(vector<uint32_t>& measure) const;
+ /*const std::pair<double, double> countVarsDegreeStDev() const;
template<class T>
void addDegrees(const vec<T*>& cs, vector<uint32_t>& degrees) const;
- void addDegreesBin(vector<uint32_t>& degrees) const;
+ void addDegreesBin(vector<uint32_t>& degrees) const;*/
const Solver& solver;
- const uint32_t topX; ///<The how many is the top X? 100 is default
- const uint32_t limit; ///<If top x contains on average this many common varables, we select MiniSat-type
+ const double topXPerc; ///<The how many is the top X? 100 is default
+ const double limitPerc; ///<If top x contains on average this many common varables, we select MiniSat-type
+
vector<Var> sameIns;
+ uint32_t topX;
+ uint32_t limit;
vector<Var> firstVars; ///<The top x variables (in terms of var activity)
vector<Var> firstVarsOld; ///<The previous top x variables (in terms of var activity)
inline void RestartTypeChooser::reset()
{
+ firstVarsOld.clear();
sameIns.clear();
+ topX = 0;
+ limit = 0;
}
#endif //RESTARTTYPECHOOSER_H
#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)
{}
doit(lit, vertex);
}
- if (solver.conf.doExtendedSCC) {
+ if (solver.conf.doExtendedSCC && solver.conf.doCacheOTFSSR) {
Lit vertLit = Lit::toLit(vertex);
- vector<Lit>& transCache = solver.transOTFCache[(~Lit::toLit(vertex)).toInt()].lits;
- vector<Lit>::iterator it = transCache.begin();
- vector<Lit>::iterator it2 = it;
+ vector<LitExtra>& transCache = solver.transOTFCache[(~vertLit).toInt()].lits;
+ vector<LitExtra>::iterator it = transCache.begin();
+ vector<LitExtra>::iterator it2 = it;
uint32_t newSize = 0;
- for (vector<Lit>::iterator end = transCache.end(); it != end; it++) {
- Lit lit = *it;
+ for (vector<LitExtra>::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);
}
Solver& solver;
const vec<char>& varElimed1;
const vec<char>& varElimed2;
+ const vec<lbool>& varPartHandled;
const vector<Lit>& replaceTable;
double totalTime;
};
#include "SolverTypes.h"
#include <vector>
+#include <set>
+
+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<lbool> value;
- std::vector<std::vector<Lit> > bins;
+ std::vector<std::vector<BinClause> > bins;
+ std::vector<std::vector<TriClause> > tris;
+
+ int threadAddingVars;
+ bool EREnded;
+ std::set<int> othersSyncedER;
+ uint32_t numNewERVars;
+ uint32_t lastNewERVars;
};
#endif //SHARED_DATA_H
#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
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)
, moreRecurMinLDo(0)
, updateTransCache(0)
, nbClOverMaxGlue(0)
+ , OTFGateRemLits(0)
+ , OTFGateRemSucc(0)
, ok (true)
, numBins (0)
- , cla_inc (1)
, qhead (0)
, mtrand ((unsigned long int)0)
, 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)
{
watches .push(); // (list for negative literal)
reason .push(PropBy());
assigns .push(l_Undef);
- level .push(-1);
+ level .push(std::numeric_limits<uint32_t>::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);
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();
}
case 1: {
uncheckedEnqueue(Lit(ps[0].var(), xorEqualFalse));
- ok = (propagate().isNULL());
+ ok = (propagate<true>().isNULL());
return NULL;
}
case 2: {
*/
template <class T>
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);
return NULL;
} else if (ps.size() == 1) {
uncheckedEnqueue(ps[0]);
- ok = (propagate().isNULL());
+ ok = (propagate<true>().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<Lit>& 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<Lit>& ps, const uint32_t group, const bool learnt, const uint32_t glue, const bool inOriginalInput, const bool attach);
template<class T> const bool Solver::addClauseHelper(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;
template<class T>
-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<Lit>& 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<Lit>& 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);
/**
{
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()]);
}
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)
{
#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) {
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<Lit>& cache = transOTFCache[(~lit).toInt()].lits;
+ vector<LitExtra>& cache = transOTFCache[(~lit).toInt()].lits;
uint32_t cacheSize = cache.size();
- for (vector<Lit>::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) {
+ for (vector<LitExtra>::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 </*=*/ cacheSize
+ ) {
+ //if (litReachable[it->toInt()].numInCache == cacheSize && mtrand.randInt(1) == 0) continue;
+ litReachable[it->getLit().toInt()].lit = lit;
+ litReachable[it->getLit().toInt()].numInCache = cacheSize;
}
}
}
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<LitExtra> 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);
}
//=================================================================================================
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);
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];
@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<Lit>& out_learnt, int& out_btlevel, uint32_t &glue, const bool update)
+Clause* Solver::analyze(PropBy conflHalf, vec<Lit>& out_learnt, uint32_t& out_btlevel, uint32_t &glue, const bool update)
{
int pathC = 0;
Lit p = lit_Undef;
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();
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())
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)
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
*/
void Solver::minimiseLeartFurther(vec<Lit>& 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
//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<Lit> oldCl = cl;
+ while (true) {
+ for (Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) {
+ const vector<OrGate*>& gates = subsumer->getGateOcc(*l);
+ if (gates.empty()) continue;
+
+ for (vector<OrGate*>::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]) <<std::endl;
+ }
+ std::cout << "New clause: " << cl << std::endl;
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ std::cout << "-> Lit " << cl[i] << " lev: " << level[cl[i].var()] << " val: " << value(cl[i]) << std::endl;
+ }
+ #endif
+
+ if (firstInside) {
+ uint32_t swapWith = std::numeric_limits<uint32_t>::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<uint64_t>::max()
- && (transOTFCache[l->toInt()].conflictLastUpdated + thisUpdateTransOTFSSCache >= conflicts))) {
- for (vector<Lit>::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<LitExtra>::const_iterator it = cache1.lits.begin(), end2 = cache1.lits.end(); it != end2; it++) {
+ seen[(~(it->getLit())).toInt()] = 0;
}
} else {
updateTransCache++;
//watches are mostly sorted, so it's more-or-less OK to break
// if non-bi or non-tri is encountered
- break;
+ //break;
}
}
void Solver::transMinimAndUpdateCache(const Lit lit, uint32_t& moreRecurProp)
{
- vector<Lit>& allAddedToSeen2 = transOTFCache[lit.toInt()].lits;
- allAddedToSeen2.clear();
+ assert(conf.doCacheOTFSSR);
+ vector<LitExtra> 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<Watched>& ws = watches[(~thisLit).toInt()];
+ vec<Watched>& 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<Lit>::const_iterator it = allAddedToSeen2.begin(), end = allAddedToSeen2.end(); it != end; it++) {
- seen[(~(*it)).toInt()] = 0;
- seen2[it->toInt()] = 0;
+ for (vector<LitExtra>::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;
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)
}
#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)
#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
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<bool full>
+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();
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<bool full>
+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();
}
/**
-@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<bool full>
inline const bool Solver::propNormalClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl, const bool update)
{
if (value(i->getBlockedLit()).getBool()) {
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);
}
/**
-@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
\todo maybe not worth it, and a variable-based watchlist should be used
*/
+template<bool full>
inline const bool Solver::propXorClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl)
{
ClauseOffset offset = i->getXorOffset();
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();
Basically, it goes through the watchlists recursively, and calls the appropirate
propagaton function
*/
+template<bool full>
PropBy Solver::propagate(const bool update)
{
PropBy confl;
Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
vec<Watched>& 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;
#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;
<< " 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<full>(i, end, p, confl)) break;
else continue;
} //end BINARY
if (i->isTriClause()) {
- if (!propTriClause(i, j, end, p, confl)) break;
+ *j++ = *i;
+ if (!propTriClause<full>(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<full>(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;
if (i->isXorClause()) {
num_props += 10;
- if (!propXorClause(i, j, end, p, confl)) break;
+ if (!propXorClause<full>(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);
return confl;
}
+template PropBy Solver::propagate <true>(const bool update);
+template PropBy Solver::propagate <false>(const bool update);
/**
@brief Only propagates binary clauses
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<Watched> & 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 {
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);
}
}
/**
-@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()
{
| 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();
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;
#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();
totalGlueOfNonRemoved += learnts[i]->getGlue();
totalSizeOfNonRemoved += learnts[i]->size();
totalNumNonRemoved++;
+ numThreeLongLearnt += (learnts[i]->size()==3);
+ removeNum++;
learnts[j++] = learnts[i];
}
}
totalGlueOfNonRemoved += learnts[i]->getGlue();
totalSizeOfNonRemoved += learnts[i]->size();
totalNumNonRemoved++;
+ numThreeLongLearnt += (learnts[i]->size()==3);
learnts[j++] = learnts[i];
}
learnts.shrink_(i - j);
<< 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;
}
testAllClauseAttach();
assert(decisionLevel() == 0);
- if (!ok || !propagate().isNULL()) {
+ if (!ok || !propagate<true>().isNULL()) {
ok = false;
return false;
}
totalSimplifyTime += cpuTime() - myTime;
testAllClauseAttach();
+ checkNoWrongAttach();
return true;
}
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;
else dynStarts++;
}
glueHistory.fastclear();
+ agility = 0.0;
+ numAgilityTooHigh = 0;
+ lastConflAgilityTooHigh = std::numeric_limits<uint64_t>::max();
#ifdef USE_GAUSS
for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end = gauss_matrixes.end(); gauss != end; gauss++) {
#endif //VERBOSE_DEBUG
for (;;) {
assert(ok);
- PropBy confl = propagate(update);
+ PropBy confl = propagate<true>(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 {
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;
}
}
@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();
}
// 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()) {
if (dynamic_behaviour_analysis)
progress_estimate = progressEstimate();
#endif
+
cancelUntil(0);
return l_Undef;
}
cout << endl;
#endif
- int backtrack_level;
+ uint32_t backtrack_level;
uint32_t glue;
conflicts++;
#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());
}
#endif
//Normal learnt
} else {
+ bumpUIPPolCount(learnt_clause);
if (learnt_clause.size() == 2) {
attachBinClause(learnt_clause[0], learnt_clause[1], true);
numNewBin++;
}
varDecayActivity();
- if (update && restartType == static_restart) claDecayActivity();
return l_Nothing;
}
+void Solver::bumpUIPPolCount(const vec<Lit>& 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
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();
}
}
conflSizeHist.clear();
conflSizeHist.initSize(1000);
- lastSelectedRestartType = restartType;
+ subRestartType = restartType;
}
/**
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<uint64_t>::max(), false);
}
+ if (needToInterrupt) return l_Undef;
printRestartStat("S");
if (status != l_Undef) goto end;
#endif //BURST_SEARCH
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) {
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<LitExtra> tmp1;
+ transOTFCache[Lit(var, false).toInt()].lits.swap(tmp1);
+ vector<LitExtra> tmp2;
+ transOTFCache[Lit(var, true).toInt()].lits.swap(tmp2);
+ }
+ }
+
end:
#ifdef BURST_SEARCH
if (conf.verbosity >= 3)
status = l_False;
testAllClauseAttach();
+ checkNoWrongAttach();
+ numSimplifyRounds++;
if (!ok) return l_False;
return status;
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;
if (conf.doReplace && !varReplacer->performReplace()) return;
if (conf.doClausVivif && !conf.libraryUsage
- && !clauseVivifier->vivifyClauses()) return;
+ && !clauseVivifier->vivify()) return;
bool saveDoHyperBin = conf.doHyperBinRes;
conf.doHyperBinRes = false;
found solution with all the intermediary simplifications (e.g. variable
elimination, etc.) and output the solution.
*/
-lbool Solver::solve(const vec<Lit>& assumps)
+const lbool Solver::solve(const vec<Lit>& assumps, const int _numThreads , const int _threadNum)
{
+ numThreads = _numThreads;
+ threadNum = _threadNum;
#ifdef VERBOSE_DEBUG
std::cout << "Solver::solve() called" << std::endl;
#endif
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
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) {
}
#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();
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<true>().isNULL());
release_assert(ok && "c ERROR! Extension of model failed!");
}
checkSolution();
#include "GaussianConfig.h"
#include "ClauseAllocator.h"
#include "SolverConf.h"
+#include "TransCache.h"
#define release_assert(a) \
do { \
} \
} while (0)
+#ifndef __GNUC__
+#define __builtin_prefetch(a,b,c)
+#endif //__GNUC__
+
class Gaussian;
class MatrixFinder;
class Conglomerate;
class ClauseVivifier;
class SharedData;
class DataSync;
+class BothCache;
namespace BEEV
{
class CryptoMinisat;
}
+
#ifdef VERBOSE_DEBUG
#define DEBUG_UNCHECKEDENQUEUE_LEVEL0
using std::cout;
//=================================================================================================
// 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);
+ }
};
/**
// 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:
template<class T>
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<class T>
- 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<class T>
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<Lit>& assumps); ///<Search for a model that respects a given set of assumptions.
- lbool solve (); ///<Search without assumptions.
- void handleSATSolution(); ///<Extends model, if needed, and fills "model"
- void handleUNSATSolution(); ///<If conflict really was zero-length, sets OK to false
- bool okay () const; ///<FALSE means solver is in a conflicting state
+ const lbool solve (const vec<Lit>& assumps, const int numThreads = 1, const int threadNum = 0); ///<Search for a model that respects a given set of assumptions.
+ const lbool solve (const int numThreads = 1, const int threadNum = 0); ///<Search without assumptions.
+ const bool okay () const; ///<FALSE means solver is in a conflicting state
// Variable mode:
//
// Read state:
//
- lbool value (const Var x) const; ///<The current value of a variable.
- lbool value (const Lit p) const; ///<The current value of a literal.
- lbool modelValue (const Lit p) const; ///<The value of a literal in the last model. The last call to solve must have been satisfiable.
- uint32_t nAssigns () const; ///<The current number of assigned literals.
- uint32_t nClauses () const; ///<The current number of original clauses.
- uint32_t nLiterals () const; ///<The current number of total literals.
- uint32_t nLearnts () const; ///<The current number of learnt clauses.
- uint32_t nVars () const; ///<The current number of variables.
+ const lbool value (const Var x) const; ///<The current value of a variable.
+ const lbool value (const Lit p) const; ///<The current value of a literal.
+ const lbool modelValue (const Lit p) const; ///<The value of a literal in the last model. The last call to solve must have been satisfiable.
+ const uint32_t nAssigns () const; ///<The current number of assigned literals.
+ const uint32_t nClauses () const; ///<The current number of original clauses.
+ const uint32_t nLiterals () const; ///<The current number of total literals.
+ const uint32_t nLearnts () const; ///<The current number of learnt clauses.
+ const uint32_t nVars () const; ///<The current number of variables.
// Extra results: (read-only member variable)
//
vec<lbool> model; ///<If problem is satisfiable, this vector contains the model (if any).
vec<Lit> conflict; ///<If problem is unsatisfiable (possibly under assumptions), this vector represent the final conflict clause expressed in the assumptions.
- // Mode of operation:
- //
- SolverConf conf;
- GaussConf gaussconfig; ///<Configuration for the gaussian elimination can be set here
- bool needToInterrupt; ///<Used internally mostly. If set to TRUE, we will interrupt cleanly ASAP. The important thing is "cleanly", since we need to wait until a point when all datastructures are in a sane state (i.e. not in the middle of some algorithm)
-
//Logging
void needStats(); // Prepares the solver to output statistics
void needProofGraph(); // Prepares the solver to output proof graphs during solving
- void setVariableName(const Var var, const char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger')
+ void setVariableName(const Var var, const std::string& name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger')
const vec<Clause*>& 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<Clause*>& get_learnts() const; //Get all learnt clauses that are >1 long
const vector<Lit> get_unitary_learnts() const; //return the set of unitary learnt clauses
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; ///<Get number of variables eliminated
const uint32_t getNumElimXorSubsume() const; ///<Get number of variables eliminated with xor-magic
const uint32_t getNumXorTrees() const; ///<Get the number of trees built from 2-long XOR-s. This is effectively the number of variables that replace other variables
*/
const double getTotalTimeXorSubsumer() const;
+ const uint32_t getVerbosity() const;
+ void setNeedToInterrupt(const bool value = true);
+ const bool getNeedToInterrupt() const;
+ const bool getNeedToDumpLearnts() const;
+ const bool getNeedToDumpOrig() const;
+
protected:
- //gauss
+ // Mode of operation:
+ //
+ SolverConf conf;
+ /**
+ @brief If set to TRUE, we will interrupt cleanly ASAP.
+
+ The important thing is "cleanly", since we need to wait until a point when
+ all datastructures are in a sane state (i.e. not in the middle of some
+ algorithm)
+ */
+ bool needToInterrupt;
+ int numThreads;
+ int threadNum;
+
+ //Gauss
+ //
+ GaussConf gaussconfig; ///<Configuration for the gaussian elimination can be set here
const bool clearGaussMatrixes();
vector<Gaussian*> gauss_matrixes;
#ifdef USE_GAUSS
uint64_t moreRecurMinLDo; ///<Decided to carry out transitive on-the-fly self-subsuming resolution on this many clauses
uint64_t updateTransCache; ///<Number of times the transitive OTF-reduction cache has been updated
uint64_t nbClOverMaxGlue; ///<Number or clauses over maximum glue defined in maxGlue
+ uint64_t OTFGateRemLits;
+ uint64_t OTFGateRemSucc;
//Multi-threading
DataSync* dataSync;
vec<Clause*> learnts; ///< List of learnt clauses.
uint32_t numBins;
vec<XorClause*> 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<vec<Watched> > watches; ///< 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<lbool> assigns; ///< The current assignments
vector<bool> decision_var; ///< Declares if a variable is eligible for selection in the decision heuristic.
vec<Lit> trail; ///< Assignment stack; stores all assigments made in the order they were made.
vec<uint32_t> trail_lim; ///< Separator indices for different decision levels in 'trail'.
vec<PropBy> reason; ///< 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
- vec<int32_t> level; ///< 'level[var]' contains the level at which the assignment was made.
+ vec<uint32_t> level; ///< 'level[var]' contains the level at which the assignment was made.
vec<BinPropData> 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
Heap<VarOrderLt> 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<uint32_t> activity; ///< A heuristic measurement of the activity of a variable.
uint32_t var_inc; ///< Amount to bump next variable with.
+ vector<std::pair<uint64_t, uint64_t> > lTPolCount;
+ void bumpUIPPolCount(const vec<Lit>& lit);
+ vector<UIPNegPosDist> negPosDist;
/////////////////
// Learnt clause cleaning
bqueue<uint32_t> glueHistory; ///< Set of last decision levels in (glue of) conflict clauses. Used for dynamic restarting
vec<Clause*> 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.
//
////////////
// Transitive on-the-fly self-subsuming resolution
///////////
- class TransCache {
- public:
- TransCache() :
- conflictLastUpdated(std::numeric_limits<uint64_t>::max())
- {};
-
- vector<Lit> lits;
- uint64_t conflictLastUpdated;
- };
class LitReachData {
public:
LitReachData() :
void saveOTFData();
vector<LitReachData>litReachable;
void calcReachability();
+ const bool cacheContainsBinCl(const Lit lit1, const Lit lit2, const bool learnt) const;
////////////
//Logging
////////////////
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<Lit>& uselessBin);
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<bool full>
+ PropBy propagate(const bool update = true); // Perform unit propagation. Returns possibly conflicting clause.
+ template<bool full>
+ const bool propTriClause (Watched* i, Watched *end, const Lit p, PropBy& confl);
+ template<bool full>
+ const bool propBinaryClause(Watched* i, Watched *end, const Lit p, PropBy& confl);
+ vec<uint32_t> popularity;
+ template<bool full>
const bool propNormalClause(Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl, const bool update);
+ template<bool full>
const bool propXorClause (Watched* &i, Watched* &j, Watched *end, const Lit p, PropBy& confl);
void sortWatched();
///////////////
void cancelUntil (int level); // Backtrack until a certain level.
void cancelUntilLight();
- Clause* analyze (PropBy confl, vec<Lit>& out_learnt, int& out_btlevel, uint32_t &nblevels, const bool update);
+ Clause* analyze (PropBy confl, vec<Lit>& out_learnt, uint32_t& out_btlevel, uint32_t &nblevels, const bool update);
void analyzeFinal (Lit p, vec<Lit>& 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.
/////////////////
// 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<Lit>& 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(); ///<Extends model, if needed, and fills "model"
+ void handleUNSATSolution(); ///<If conflict really was zero-length, sets OK to false
/////////////////
// Maintaining Variable/Clause activity:
/////////////////
- void claBumpActivity (Clause& c);
void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
- void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
/////////////////
// Operations on clauses:
/////////////////
template<class T> const bool addClauseHelper(T& ps, const uint32_t group, const char* group_name);
template <class T>
- 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<class T>
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);
// 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
friend class SCCFinder;
friend class ClauseVivifier;
friend class DataSync;
+ friend class BothCache;
Conglomerate* conglomerate;
VarReplacer* varReplacer;
ClauseCleaner* clauseCleaner;
/////////////////////////
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; ///<Used internally to determine which restart strategy is currently in use
- RestartType lastSelectedRestartType; ///<The last selected restart type. Used when we are just after a full restart, and need to know how to really act
+ RestartType subRestartType;
//////////////////////////
// Problem simplification
const bool simplify(); // Removes satisfied clauses and finds binary xors
bool simplifying; ///<We are currently doing burst search
double totalSimplifyTime;
+ uint32_t numSimplifyRounds;
uint32_t simpDB_assigns; ///< Number of top-level assignments since last execution of 'simplify()'.
int64_t simpDB_props; ///< Remaining number of propagations that must be made before next execution of 'simplify()'.
void printEndSearchStat();
void addSymmBreakClauses();
void initialiseSolver();
+ void checkNoWrongAttach() const;
//Misc related binary clauses
void dumpBinClauses(const bool alsoLearnt, const bool alsoNonLearnt, FILE* outfile) const;
void tallyVotes(const vec<XorClause*>& cs, vec<double>& votes) const;
void setPolarity(Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
vector<bool> polarity; // The preferred polarity of each variable.
- #ifdef USE_OLD_POLARITIES
- vector<bool> 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)
{
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
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();
}
insertVarOrder(v);
}
}
-inline lbool Solver::solve ()
+inline const lbool Solver::solve (const int _numThreads, const int _threadNum)
{
vec<Lit> tmp;
- return solve(tmp);
+ return solve(tmp, numThreads, threadNum);
}
-inline bool Solver::okay () const
+inline const bool Solver::okay () const
{
return ok;
}
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
{
return;
}
+inline void Solver::checkNoWrongAttach() const
+{
+ return;
+}
inline void Solver::findAllAttach() const
{
return;
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;
}
//=================================================================================================
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)
, doMaxGlueDel (false)
, doPrintAvgBranch (false)
, doCacheOTFSSR (true)
+ , doCacheNLBins (true)
, doExtendedSCC (true)
+ , doGateFind (true)
+ , doAlwaysFMinim (true)
+ , doER (true)
, doCalcReach (true)
, maxRestarts (std::numeric_limits<uint32_t>::max())
SolverConf();
double random_var_freq; ///<The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) NOTE: This is really strange. If the number of variables set is large, then the random chance is in fact _far_ lower than this value. This is because the algorithm tries to set one variable randomly, but if that variable is already set, then it _silently_ fails, and moves on (doing non-random flip)!
- double clause_decay; ///<Inverse of the clause activity decay factor. Only applies if using MiniSat-style clause activities (default: 1 / 0.999)
int restart_first; ///<The initial restart limit. (default 100)
double restart_inc; ///<The factor with which the restart limit is multiplied in each restart. (default 1.5)
double learntsize_factor; ///<The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)
- double learntsize_inc; ///<The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
+ double agilityG;
+ double agilityLimit;
bool expensive_ccmin; ///<Should clause minimisation by Sorensson&Biere be used? (default TRUE)
int polarity_mode; ///<Controls which polarity the decision heuristic chooses. Auto means Jeroslow-Wang (default: polarity_auto)
int verbosity; ///<Verbosity level. 0=silent, 1=some progress report, 2=lots of report, 3 = all report (default 2)
bool doMaxGlueDel;
bool doPrintAvgBranch;
bool doCacheOTFSSR;
+ bool doCacheNLBins;
bool doExtendedSCC;
+ bool doGateFind;
+ bool doAlwaysFMinim;
+ bool doER;
bool doCalcReach; ///<Calculate reachability, and influence variable decisions with that
//interrupting & dumping
}
}
+
+#ifdef DEBUG_ATTACH_FULL
+void Solver::checkNoWrongAttach() const
+{
+ for (Clause *const*i = learnts.getData(), *const*end = learnts.getDataEnd(); i != end; i++) {
+
+ const Clause& cl = **i;
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ if (i > 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++) {
}
}
-}
\ No newline at end of file
+}
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);
Lit lit = ~Lit::toLit(wsLit);
const vec<Watched>& 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;
const vec<Clause*>& 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;
}
<< 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;
}
}
<< 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) {
}
- DimacsParser parser(this, false, false, false, true);
+ /*
+ DimacsParser parser(this, false, false, false);
#ifdef DISABLE_ZLIB
FILE * in = fopen("output", "rb");
#else
gzclose(in);
#endif // DISABLE_ZLIB
+ */
std::cout << "c Finished saucy, time: " << (cpuTime() - myTime) << std::endl;
}
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)
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");
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
printStatsLine("c CPU time", cpu_time, " s");
}
}
+
+const bool Solver::cacheContainsBinCl(const Lit lit1, const Lit lit2, const bool learnt) const
+{
+ const vector<LitExtra>& cache = transOTFCache[(~lit1).toInt()].lits;
+ for (vector<LitExtra>::const_iterator it = cache.begin(), end = cache.end(); it != end; it++) {
+ if (it->getLit() == lit2 && (!learnt || it->getOnlyNLBin())) return true;
+ }
+
+ return false;
+}
#include <stdio.h>
#include <vector>
#include "constants.h"
+#include <iomanip>
+#include <sstream>
//=================================================================================================
// Variables, literals, lifted booleans, clauses:
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);
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<Lit>& lits)
struct BinPropData {
uint32_t lev;
- Lit lev2Ancestor;
+ Lit lev1Ancestor;
bool learntLeadHere;
+ bool hasChildren;
};
**************************************************************************************************/
#include "StateSaver.h"
+#include "PartHandler.h"
StateSaver::StateSaver(Solver& _solver) :
solver(_solver)
//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);
+ }
}
#include "OnlyNonLearntBins.h"
#include "UselessBinRemover.h"
#include "DataSync.h"
+#include "BothCache.h"
+#include <set>
+#include "PartHandler.h"
#ifdef _MSC_VER
#define __builtin_prefetch(a,b,c)
//#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;
solver(s)
, totalTime(0.0)
, numElimed(0)
- , numCalls(1)
+ , numERVars(0)
+ , finishedAddingVars(false)
+ , numCalls(0)
, alsoLearnt(false)
{
};
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();
subsume0Happened ret;
ret.subsumedNonLearnt = false;
ret.glue = std::numeric_limits<uint32_t>::max();
- ret.act = std::numeric_limits< float >::min();
vec<ClauseSimp> subs;
findSubsumed(ps, abs, subs);
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;
}
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<char>& lits, const uint32_t abst)
-{
- vec<ClauseSimp> subs;
- vec<ClauseSimp> subs2;
- vec<Lit> subs2Lit;
-
- vec<ClauseSimp>& 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
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;
return retval;
}
-const bool Subsumer::cleanClause(vec<Lit>& 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
#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()) {
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());
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()
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
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;
*/
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;
}
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);
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<Watched>& 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;
return true;
}
-const bool Subsumer::subsWNonExitsBinsFullFull()
-{
- double myTime = cpuTime();
- clauses_subsumed = 0;
- literals_removed = 0;
- for (vec<Watched> *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);
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<Watched> *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) {
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<true>().isNULL();
if (!solver.ok) return false;
continue;
}
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<true>().isNULL();
if (!solver.ok) return false;
continue;
}
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;
}
@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;
else
failed = !onlyNonLearntBins->propagate();
if (failed) return false;
- uint32_t abst = 0;
+ vector<LitExtra> 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;
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;
}
/**
}
clauses.clear();
cl_touched.clear();
+ defOfOrGate.clear();
addedClauseLits = 0;
+ numLearntBinVarRemAdded = 0;
}
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<Var> order;
if (first) {
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
|| 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();
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);
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)
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) {
} 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);
<< " 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;
}
}
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;
if (alsoLearnt) {
numMaxElim = 0;
numMaxElimVars = 0;
- numMaxSubsume0 /= 2;
- numMaxSubsume1 /= 2;
+ numMaxSubsume0 /= 3;
+ numMaxSubsume1 /= 5;
numMaxBlockVars = 0;
- } else {
- numCalls++;
}
//For debugging
*/
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;
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;
// 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<ClAndBin> posAll, negAll;
fillClAndBin(posAll, poss, lit);
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;
}
}
numMaxElim -= posSize * negSize + before_literals;
poss.clear();
negs.clear();
+ if (numCalls >= 4) addLearntBinaries(var);
removeClauses(posAll, negAll, var);
#ifndef NDEBUG
}
#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<Lit> tmp;
+ Lit lit = Lit(var, false);
+ const vec<Watched>& ws = solver.watches[lit.toInt()];
+ const vec<Watched>& 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
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++;
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<Var, uint32_t> p1, const std::pair<Var, uint32_t> p2)
+ {
+ return p1.second > p2.second;
+ }
+};
+
+void Subsumer::createNewVar()
+{
+ double myTime = cpuTime();
+ vector<NewGateData> newGates;
+ vec<Lit> lits;
+ vec<ClauseSimp> 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<OrGate> backupOrGates = orGates;
+ if (!carryOutER()) return false;
+ for (vector<OrGate>::const_iterator it = backupOrGates.begin(), end = backupOrGates.end(); it != end; it++) {
+ orGates.push_back(*it);
+ }
+ }
+
+ for (vector<OrGate>::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<OrGate>::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<Lit> 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<LitExtra>& 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<LitExtra>& cache = solver.transOTFCache[(~otherLit).toInt()].lits;
+
+ bool OK = false;
+ for (vector<LitExtra>::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<ClauseSimp> 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<Lit>::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<LitExtra>& cache = solver.transOTFCache[l->toInt()].lits;
+ for (vector<LitExtra>::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<Lit> lits;
+ andGateTotalSize = 0;
+ uint32_t foundPotential;
+ //double myTime = cpuTime();
+ uint64_t numOp = 0;
+
+ for (vector<OrGate>::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<uint32_t> 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<ClauseSimp>& 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<ClauseSimp>& 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<uint32_t>::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<Lit> 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<ClauseSimp>& sizeSortedOcc, const Lit lit, const uint32_t abst2, ClauseSimp& other)
+{
+ for (vector<ClauseSimp>::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<Watched> *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) {
+ Lit lit = ~Lit::toLit(wsLit);
+ vec<Watched>& 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;
+}
#include <map>
#include <vector>
#include <list>
+#include <set>
#include <queue>
+#include <set>
+#include <iomanip>
+
using std::vector;
using std::list;
using std::map;
class ClauseCleaner;
class OnlyNonLearntBins;
+class OrGate {
+ public:
+ Lit eqLit;
+ vector<Lit> 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
const double getTotalTime() const;
const map<Var, vector<vector<Lit> > >& getElimedOutVar() const;
const map<Var, vector<std::pair<Lit, Lit> > >& 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<OrGate*>& getGateOcc(const Lit lit) const;
private:
vec<CSet* > iter_sets; ///<Sets currently used in iterations.
vec<char> cannot_eliminate;///<Variables that cannot be eliminated due to, e.g. XOR-clauses
vec<char> seen_tmp; ///<Used in various places to help perform algorithms
+ vec<char> seen_tmp2; ///<Used in various places to help perform algorithms
//Global stats
Solver& solver; ///<The solver this simplifier is connected to
//Used by cleaner
void unlinkClause(ClauseSimp cc, const Var elim = var_Undef);
ClauseSimp linkInClause(Clause& cl);
+ const bool handleUpdatedClause(ClauseSimp& c);
//Findsubsumed
template<class T>
struct subsume0Happened {
bool subsumedNonLearnt;
uint32_t glue;
- float act;
};
/**
@brief Sort clauses according to size
const bool subsume1(vec<Lit>& ps, const bool wasLearnt);
void strenghten(ClauseSimp& c, const Lit toRemoveLit);
const bool cleanClause(Clause& ps);
- const bool cleanClause(vec<Lit>& ps) const;
- void handleSize1Clause(const Lit lit);
//Variable elimination
/**
Lit lit2;
bool isBin;
};
+ uint32_t numLearntBinVarRemAdded;
void orderVarsForElim(vec<Var>& order);
const uint32_t numNonLearntBins(const Lit lit) const;
bool maybeEliminate(Var x);
+ void addLearntBinaries(const Var var);
void removeClauses(vec<ClAndBin>& posAll, vec<ClAndBin>& negAll, const Var var);
void removeClausesHelper(vec<ClAndBin>& todo, const Var var, std::pair<uint32_t, uint32_t>& removed);
bool merge(const ClAndBin& ps, const ClAndBin& qs, const Lit without_p, const Lit without_q, vec<Lit>& out_clause);
const bool eliminateVars();
void fillClAndBin(vec<ClAndBin>& all, vec<ClauseSimp>& cs, const Lit lit);
+ void removeBinsAndTris(const Var var);
+ const uint32_t removeBinAndTrisHelper(const Lit lit, vec<Watched>& ws);
+
//Subsume with Nonexistent Bins
struct BinSorter2 {
const bool operator()(const Watched& first, const Watched& second)
return false;
};
};
- const bool subsWNonExitsBinsFullFull();
- const bool subsWNonExistBinsFull();
- const bool subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* OnlyNonLearntBins);
- void subsume0BIN(const Lit lit, const vec<char>& 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<Lit> toVisit; ///<Literals that we have visited from a given literal during subsumption w/ non-existent binaries (list)
- vec<char> toVisitAll; ///<Literals that we have visited from a given literal during subsumption w/ non-existent binaries (contains '1' for literal.toInt() that we visited)
//Blocked clause elimination
class VarOcc {
void touchBlockedVar(const Var x);
void blockedClauseElimAll(const Lit lit);
+ //Gate extraction
+ struct OrGateSorter {
+ const bool operator() (const OrGate& gate1, const OrGate& gate2) {
+ return (gate1.lits.size() > 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<OrGate> orGates;
+ vector<vector<OrGate*> > gateOcc;
+ uint32_t numOrGateReplaced;
+ const bool findEqOrGates();
+ vec<char> defOfOrGate;
+ const bool carryOutER();
+ void createNewVar();
+ const bool doAllOptimisationWithGates();
+ uint32_t andGateNumFound;
+ uint32_t andGateTotalSize;
+ vec<char> 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<ClauseSimp>& sizeSortedOcc, const Lit lit, const uint32_t abst2, ClauseSimp& other);
+ vector<vector<ClauseSimp> > sizeSortedOcc;
//validity checking
const bool verifyIntegrity();
uint32_t clauses_subsumed; ///<Number of clauses subsumed in this run
uint32_t literals_removed; ///<Number of literals removed from clauses through self-subsuming resolution in this run
uint32_t numCalls; ///<Number of times simplifyBySubsumption() has been called
- uint32_t clauseID; ///<We need to have clauseIDs since clauses don't natively have them. The ClauseID is stored by ClauseSimp, which also stores a pointer to the clause
bool alsoLearnt;
};
occur .push();
seen_tmp .push(0); // (one for each polarity)
seen_tmp .push(0);
+ seen_tmp2 .push(0); // (one for each polarity)
+ seen_tmp2 .push(0);
touchedVars .push(0);
var_elimed .push(0);
touchedBlockedVarsBool.push(0);
ol_seenNeg.push(1);
ol_seenNeg.push(1);
touch(solver.nVars()-1);
+ dontElim.push(0);
+ gateOcc.push_back(vector<OrGate*>());
+ gateOcc.push_back(vector<OrGate*>());
}
inline const map<Var, vector<vector<Lit> > >& Subsumer::getElimedOutVar() 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<OrGate*>& Subsumer::getGateOcc(const Lit lit) const
+{
+ return gateOcc[lit.toInt()];
+}
+
#endif //SIMPLIFIER_H
--- /dev/null
+#ifndef TRANSCACHE_H
+#define TRANSCACHE_H
+
+#include <vector>
+#include <limits>
+#include <algorithm>
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#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<uint64_t>::max())
+ {};
+
+ void merge(std::vector<LitExtra>& 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<LitExtra> oldLits(lits);
+ std::vector<LitExtra> newLits;
+ newLits.swap(lits);
+ newLits.clear();
+
+ std::vector<LitExtra>::iterator it = oldLits.begin();
+ std::vector<LitExtra>::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<LitExtra> lits;
+ uint64_t conflictLastUpdated;
+};
+
+#endif //TRANSCACHE_H
\ No newline at end of file
fixed = true;
solver.cancelUntilLight();
solver.uncheckedEnqueue(~lit);
- solver.ok = (solver.propagate().isNULL());
+ solver.ok = (solver.propagate<true>().isNULL());
if (!solver.ok) return false;
continue;
}
fixed = true;
solver.cancelUntilLight();
solver.uncheckedEnqueue(~lit);
- solver.ok = (solver.propagate().isNULL());
+ solver.ok = (solver.propagate<true>().isNULL());
if (!solver.ok) return false;
continue;
}
CryptoMiniSat
-GIT revision: 588152bb03adf98ffd581c4579e1d6c5eec92f8f
+GIT revision: d28c9b8ba7b189113cdf9c8147a14ae2a9b546bd
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);
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<true>().isNULL());
return true;
case 2: {
solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
solver.clauses_literals -= removedNonLearnt;
solver.numBins -= (removedLearnt + removedNonLearnt)/2;
- if (solver.ok) solver.ok = (solver.propagate().isNULL());
+ if (solver.ok) solver.ok = (solver.propagate<true>().isNULL());
return solver.ok;
}
}
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
return true;
case 1 :
solver.uncheckedEnqueue(c[0]);
- solver.ok = (solver.propagate().isNULL());
+ solver.ok = (solver.propagate<true>().isNULL());
return true;
case 2:
solver.attachBinClause(c[0], c[1], c.learnt());
solver.dataSync->signalNewBinClause(c);
return true;
default:
+ if (c.size() == 3) solver.dataSync->signalNewTriClause(c);
solver.attachClause(c);
return false;
}
assert(solver.assigns[i].getBool() == (solver.assigns[it->var()].getBool() ^ it->sign()));
}
}
- solver.ok = (solver.propagate().isNULL());
+ solver.ok = (solver.propagate<true>().isNULL());
assert(solver.ok);
}
}
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());
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)) {
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<true>().isNULL());
return solver.ok;
}
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());
\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);
}
-/***********************************************************************************
+/***************************************************************************
CryptoMiniSat -- Copyright (c) 2009 Mate Soos
This program is free software: you can redistribute it and/or modify
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
-**************************************************************************************************/
+*****************************************************************************/
#ifndef VARREPLACER_H
#define VARREPLACER_H
const bool replace_set(vec<XorClause*>& 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);
std::sort(table.begin(), table.end(), clause_sorter_primary());
if (!findXors(sumLengths)) goto end;
- solver.ok = (solver.propagate().isNULL());
+ solver.ok = (solver.propagate<true>().isNULL());
end:
}
propagated = (solver.qhead != solver.trail.size());
- solver.ok = (solver.propagate().isNULL());
+ solver.ok = (solver.propagate<true>().isNULL());
if (!solver.ok) {
return false;
}
///////////////////
//Parameters for learnt-clause cleaning
-#define RATIOREMOVECLAUSES 1.0/2.0
+#define RATIOREMOVECLAUSES (1.0/2.0)
#define NBCLAUSESBEFOREREDUCE 20000
#define FIXCLEANREPLACE 30U
#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
#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
#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
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++;
if (sz == cap) {
cap = imax(2, (cap*3+1)>>1);
data = (T*)realloc(data, cap * sizeof(T));
+ assert(data != NULL);
}
data[sz++] = elem;
}
projects / francis / stp.git / commitdiff