From: msoos Date: Fri, 27 Nov 2009 10:26:02 +0000 (+0000) Subject: Adding Cryptominisat Version 2 X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3e0022f2f1ef85e8202c5ea26f146e518416614e;p=francis%2Fstp.git Adding Cryptominisat Version 2 git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@429 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index c1504c3..5272713 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -19,6 +19,10 @@ CFLAGS_BASE = $(OPTIMIZE) CRYPTOMINISAT = true CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT +# OPTION to compile CRYPTOMiniSAT version 2.x +#CRYPTOMINISAT2 = true +#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT + # OPTION to compile MiniSAT #CORE = true #CFLAGS_BASE = $(OPTIMIZE) -DCORE diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 1f89b09..f19b67a 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -21,6 +21,9 @@ all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interfa ifdef CRYPTOMINISAT $(MAKE) -C $(SRC)/sat cryptominisat endif +ifdef CRYPTOMINISAT2 + $(MAKE) -C $(SRC)/sat cryptominisat2 +endif ifdef CORE $(MAKE) -C $(SRC)/sat core endif diff --git a/src/sat/cryptominisat2/BitArray.h b/src/sat/cryptominisat2/BitArray.h new file mode 100644 index 0000000..74b3b8e --- /dev/null +++ b/src/sat/cryptominisat2/BitArray.h @@ -0,0 +1,128 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef BITARRAY_H +#define BITARRAY_H + +//#define DEBUG_BITARRAY + +#include +#include +#include + +#ifndef uint +#define uint unsigned int +#endif + +class BitArray +{ +public: + BitArray() : + size(0) + , mp(NULL) + { + } + + BitArray(const BitArray& b) : + size(b.size) + { + mp = new uint64_t[size]; + memcpy(mp, b.mp, sizeof(uint64_t)*size); + } + + BitArray& operator=(const BitArray& b) + { + if (size != b.size) { + delete[] mp; + size = b.size; + mp = new uint64_t[size]; + } + memcpy(mp, b.mp, sizeof(uint64_t)*size); + + return *this; + } + + void resize(uint _size) + { + _size = _size/64 + (bool)(_size%64); + if (size != _size) { + delete[] mp; + size = _size; + mp = new uint64_t[size]; + } + } + + ~BitArray() + { + delete[] mp; + } + + inline const bool isZero() const + { + const uint64_t* mp2 = (const uint64_t*)mp; + + for (uint i = 0; i < size; i++) { + if (mp2[i]) return false; + } + return true; + } + + inline void setZero() + { + memset(mp, 0, size*sizeof(uint64_t)); + } + + inline void clearBit(const uint i) + { + #ifdef DEBUG_BITARRAY + assert(size*64 > i); + #endif + + mp[i/64] &= ~((uint64_t)1 << (i%64)); + } + + inline void setBit(const uint i) + { + #ifdef DEBUG_BITARRAY + assert(size*64 > i); + #endif + + mp[i/64] |= ((uint64_t)1 << (i%64)); + } + + inline const bool operator[](const uint& i) const + { + #ifdef DEBUG_BITARRAY + assert(size*64 > i); + #endif + + return (mp[i/64] >> (i%64)) & 1; + } + + inline const uint getSize() const + { + return size*64; + } + +private: + + uint size; + uint64_t* mp; +}; + +#endif //BITARRAY_H + diff --git a/src/sat/cryptominisat2/Clause.cpp b/src/sat/cryptominisat2/Clause.cpp new file mode 100644 index 0000000..2566be1 --- /dev/null +++ b/src/sat/cryptominisat2/Clause.cpp @@ -0,0 +1,47 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include "Clause.h" + +namespace MINISAT +{ + +Clause* Clause_new(const vec& ps, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} + +Clause* Clause_new(const vector& ps, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} + +Clause* Clause_new(const PackedRow& row, const vec& assigns, const vector& col_to_var_original, const uint group) +{ + const uint size = row.popcnt(); + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*size); + Clause* real= new (mem) Clause(row, size, assigns, col_to_var_original, group); + return real; +} + +}; diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h new file mode 100644 index 0000000..c8ab10e --- /dev/null +++ b/src/sat/cryptominisat2/Clause.h @@ -0,0 +1,212 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef CLAUSE_H +#define CLAUSE_H + +#include +#include +#include +#include +#include "Vec.h" +#include "SolverTypes.h" +#include "PackedRow.h" + +namespace MINISAT +{ + +#ifndef uint +#define uint unsigned int +#endif + +using std::vector; + + +//================================================================================================= +// Clause -- a simple class for representing a clause: + +class MatrixFinder; + +class Clause +{ +public: + const uint group; +protected: + /** + bit-layout of size_etc: + + range type meaning + -------------------------------------------- + 0th bit bool learnt clause + 1st - 2nd bit 2bit int marking + 3rd bit bool inverted xor + 4th-15th bit 12bit int matrix number + 16th -31st bit 16bit int size + */ + uint32_t size_etc; + float act; + Lit data[0]; + +public: + Clause(const PackedRow& row, const uint size, const vec& assigns, const vector& col_to_var_original, const uint _group) : + group(_group) + { + size_etc = 0; + setSize(size); + setLearnt(false); + row.fill(data, assigns, col_to_var_original); + } + + template + Clause(const V& ps, const uint _group, const bool learnt) : + group(_group) + { + size_etc = 0; + setSize(ps.size()); + setLearnt(learnt); + for (uint i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) act = 0; + } + + // -- use this function instead: + friend Clause* Clause_new(const vec& ps, const uint group, const bool learnt = false); + friend Clause* Clause_new(const vector& ps, const uint group, const bool learnt = false); + + uint size () const { + return size_etc >> 16; + } + void shrink (uint i) { + assert(i <= size()); + size_etc = (((size_etc >> 16) - i) << 16) | (size_etc & ((1 << 16)-1)); + } + void pop () { + shrink(1); + } + bool learnt () const { + return size_etc & 1; + } + uint32_t mark () const { + return (size_etc >> 1) & 3; + } + void mark (uint32_t m) { + size_etc = (size_etc & ~6) | ((m & 3) << 1); + } + + Lit& operator [] (uint32_t i) { + return data[i]; + } + const Lit& operator [] (uint32_t i) const { + return data[i]; + } + + float& activity () { + return act; + } + + Lit* getData () { + return data; + } + void print() { + printf("Clause group: %d, size: %d, learnt:%d, lits: ", group, size(), learnt()); + plain_print(); + } + void plain_print(FILE* to = stdout) const { + for (uint i = 0; i < size(); i++) { + if (data[i].sign()) fprintf(to, "-"); + fprintf(to, "%d ", data[i].var() + 1); + } + fprintf(to, "0\n"); + } +protected: + void setSize(uint32_t size) { + size_etc = (size_etc & ((1 << 16)-1)) + (size << 16); + } + void setLearnt(bool learnt) { + size_etc = (size_etc & ~1) + learnt; + } +}; + +class XorClause : public Clause +{ +public: + // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). + template + XorClause(const V& ps, const bool inverted, const uint _group) : + Clause(ps, _group, false) + { + setInverted(inverted); + } + + // -- use this function instead: + template + friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group) { + void* mem = malloc(sizeof(XorClause) + sizeof(Lit)*(ps.size())); + XorClause* real= new (mem) XorClause(ps, inverted, group); + return real; + } + + inline bool xor_clause_inverted() const + { + return size_etc & 8; + } + inline void invert(bool b) + { + size_etc ^= (uint32_t)b << 3; + } + + inline uint32_t getMatrix() const + { + return ((size_etc >> 4) & ((1 << 12)-1)); + } + + void print() { + printf("XOR Clause group: %d, size: %d, learnt:%d, lits:\"", group, size(), learnt()); + plain_print(); + } + + void plain_print(FILE* to = stdout) const { + fprintf(to, "x"); + if (xor_clause_inverted()) + printf("-"); + for (uint i = 0; i < size(); i++) { + fprintf(to, "%d ", data[i].var() + 1); + } + fprintf(to, "0\n"); + } + + friend class MatrixFinder; + +protected: + inline void setMatrix (uint32_t toset) { + assert(toset < (1 << 12)); + size_etc = (size_etc & 15) + (toset << 4) + (size_etc & ~((1 << 16)-1)); + } + inline void setInverted(bool inverted) + { + size_etc = (size_etc & 7) + ((uint32_t)inverted << 3) + (size_etc & ~15); + } +}; + +Clause* Clause_new(const vec& ps, const uint group, const bool learnt); +Clause* Clause_new(const vector& ps, const uint group, const bool learnt); +Clause* Clause_new(const PackedRow& ps, const vec& assigns, const vector& col_to_var_original, const uint group); +}; + +#endif //CLAUSE_H diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp new file mode 100644 index 0000000..4ae5dd2 --- /dev/null +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -0,0 +1,300 @@ +#include "Conglomerate.h" +#include "Solver.h" +#include "VarReplacer.h" + +#include +#include + +//#define VERBOSE_DEBUG + +#ifdef VERBOSE_DEBUG +#include +using std::cout; +using std::endl; +#endif + +using std::make_pair; + +namespace MINISAT +{ +using namespace MINISAT; + +Conglomerate::Conglomerate(Solver *_S) : + S(_S) +{} + +const vec& Conglomerate::getCalcAtFinish() const +{ + return calcAtFinish; +} + +vec& Conglomerate::getCalcAtFinish() +{ + return calcAtFinish; +} + +void Conglomerate::fillVarToXor() +{ + blocked.clear(); + varToXor.clear(); + + blocked.resize(S->nVars(), false); + for (Clause *const*it = S->clauses.getData(), *const*end = it + S->clauses.size(); it != end; it++) { + const Clause& c = **it; + for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) { + blocked[a->var()] = true; + } + } + + for (Lit* it = &(S->trail[0]), *end = it + S->trail.size(); it != end; it++) + blocked[it->var()] = true; + + uint i = 0; + for (XorClause* const* it = S->xorclauses.getData(), *const*end = it + S->xorclauses.size(); it != end; it++, i++) { + const XorClause& c = **it; + for (const Lit * a = &c[0], *end = a + c.size(); a != end; a++) { + if (!blocked[a->var()]) + varToXor[a->var()].push_back(make_pair(*it, i)); + } + } +} + +void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vector& vars) { + for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) { + if (a->var() != var) { + vars.push_back(*a); + varToXorMap::iterator finder = varToXor.find(a->var()); + if (finder != varToXor.end()) { + vector >::iterator it = + std::find(finder->second.begin(), finder->second.end(), make_pair(&x, num)); + finder->second.erase(it); + } + } + } +} + +uint Conglomerate::conglomerateXors() +{ + if (S->xorclauses.size() == 0) + return 0; + toRemove.resize(S->xorclauses.size(), false); + + #ifdef VERBOSE_DEBUG + cout << "Finding conglomerate xors started" << endl; + #endif + + fillVarToXor(); + + uint found = 0; + while(varToXor.begin() != varToXor.end()) { + varToXorMap::iterator it = varToXor.begin(); + const vector >& c = it->second; + const uint& var = it->first; + S->setDecisionVar(var, false); + + if (c.size() == 0) { + varToXor.erase(it); + continue; + } + + #ifdef VERBOSE_DEBUG + cout << "--- New conglomerate set ---" << endl; + #endif + + XorClause& x = *(c[0].first); + bool first_inverted = !x.xor_clause_inverted(); + vector first_vars; + process_clause(x, c[0].second, var, first_vars); + + #ifdef VERBOSE_DEBUG + cout << "- Removing: "; + x.plain_print(); + cout << "Adding var " << var+1 << " to calcAtFinish" << endl; + #endif + + assert(!toRemove[c[0].second]); + toRemove[c[0].second] = true; + S->detachClause(x); + calcAtFinish.push(&x); + found++; + + vector ps; + for (uint i = 1; i < c.size(); i++) { + ps = first_vars; + XorClause& x = *c[i].first; + process_clause(x, c[i].second, var, ps); + + #ifdef VERBOSE_DEBUG + cout << "- Removing: "; + x.plain_print(); + #endif + + const uint old_group = x.group; + bool inverted = first_inverted ^ x.xor_clause_inverted(); + assert(!toRemove[c[i].second]); + toRemove[c[i].second] = true; + S->removeClause(x); + found++; + clearDouble(ps); + + if (!dealWithNewClause(ps, inverted, old_group)) { + clearToRemove(); + S->ok = false; + return found; + } + } + + varToXor.erase(it); + } + + clearToRemove(); + + S->toReplace->performReplace(); + if (S->ok == false) return found; + S->ok = (S->propagate() == NULL); + + return found; +} + +bool Conglomerate::dealWithNewClause(vector& ps, const bool inverted, const uint old_group) +{ + switch(ps.size()) { + case 0: { + #ifdef VERBOSE_DEBUG + cout << "--> xor is 0-long" << endl; + #endif + + if (!inverted) + return false; + break; + } + case 1: { + #ifdef VERBOSE_DEBUG + cout << "--> xor is 1-long, attempting to set variable " << ps[0].var()+1 << endl; + #endif + + if (S->assigns[ps[0].var()] == l_Undef) { + assert(S->decisionLevel() == 0); + S->uncheckedEnqueue(Lit(ps[0].var(), inverted)); + ps[0] = Lit(ps[0].var(), inverted); + Clause* newC = Clause_new(ps, old_group); + S->unitary_learnts.push(newC); + } else if (S->assigns[ps[0].var()] != boolToLBool(!inverted)) { + #ifdef VERBOSE_DEBUG + cout << "Conflict. Aborting."; + #endif + return false; + } + break; + } + + case 2: { + #ifdef VERBOSE_DEBUG + cout << "--> xor is 2-long, must later replace variable, adding var " << ps[0].var() + 1 << " to calcAtFinish:" << endl; + XorClause* newX = XorClause_new(ps, inverted, old_group); + newX->plain_print(); + free(newX); + #endif + + S->toReplace->replace(ps[0].var(), Lit(ps[1].var(), !inverted)); + break; + } + + default: { + XorClause* newX = XorClause_new(ps, inverted, old_group); + + #ifdef VERBOSE_DEBUG + cout << "- Adding: "; + newX->plain_print(); + #endif + + S->xorclauses.push(newX); + toRemove.push_back(false); + S->attachClause(*newX); + for (const Lit * a = &((*newX)[0]), *end = a + newX->size(); a != end; a++) { + if (!blocked[a->var()]) + varToXor[a->var()].push_back(make_pair(newX, toRemove.size()-1)); + } + break; + } + } + + return true; +} + +void Conglomerate::clearDouble(vector& ps) const +{ + std::sort(ps.begin(), ps.end()); + Lit p; + uint i, j; + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { + if (ps[i] == p) { + //added, but easily removed + j--; + p = lit_Undef; + } else //just add + ps[j++] = p = ps[i]; + } + ps.resize(ps.size()-(i - j)); +} + +void Conglomerate::clearToRemove() +{ + XorClause **a = S->xorclauses.getData(); + XorClause **r = a; + XorClause **end = a + S->xorclauses.size(); + for (uint i = 0; r != end; i++) { + if (!toRemove[i]) + *a++ = *r++; + else + r++; + } + S->xorclauses.shrink(r-a); +} + +void Conglomerate::doCalcAtFinish() +{ + #ifdef VERBOSE_DEBUG + cout << "Executing doCalcAtFinish" << endl; + #endif + + vector toAssign; + for (XorClause** it = calcAtFinish.getData() + calcAtFinish.size()-1; it != calcAtFinish.getData()-1; it--) { + toAssign.clear(); + XorClause& c = **it; + assert(c.size() > 2); + + #ifdef VERBOSE_DEBUG + cout << "doCalcFinish for xor-clause:"; + S->printClause(c); cout << endl; + #endif + + bool final = c.xor_clause_inverted(); + for (int k = 0, size = c.size(); k < size; k++ ) { + const lbool& val = S->assigns[c[k].var()]; + if (val == l_Undef) + toAssign.push_back(c[k].var()); + else + final ^= val.getBool(); + } + #ifdef VERBOSE_DEBUG + if (toAssign.size() == 0) { + cout << "ERROR: toAssign.size() == 0 !!" << endl; + for (int k = 0, size = c.size(); k < size; k++ ) { + cout << "Var: " << c[k].var() + 1 << " Level: " << S->level[c[k].var()] << endl; + } + } + if (toAssign.size() > 1) { + cout << "Double assign!" << endl; + } + #endif + assert(toAssign.size() > 0); + + for (uint i = 1; i < toAssign.size(); i++) { + S->uncheckedEnqueue(Lit(toAssign[i], false), &c); + } + S->uncheckedEnqueue(Lit(toAssign[0], final), &c); + } +} + +}; diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h new file mode 100644 index 0000000..1927571 --- /dev/null +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -0,0 +1,47 @@ +#ifndef CONGLOMERATE_H +#define CONGLOMERATE_H + +#include +#include +#include "Clause.h" +#include "VarReplacer.h" + +using std::vector; +using std::pair; +using std::map; + +class Solver; + +namespace MINISAT +{ +using namespace MINISAT; + +class Conglomerate +{ +public: + Conglomerate(Solver *S); + uint conglomerateXors(); ///& getCalcAtFinish() const; + vec& getCalcAtFinish(); + +private: + + void process_clause(XorClause& x, const uint num, uint var, vector& vars); + void fillVarToXor(); + void clearDouble(vector& ps) const; + void clearToRemove(); + bool dealWithNewClause(vector& ps, const bool inverted, const uint old_group); + + typedef map > > varToXorMap; + varToXorMap varToXor; + vector blocked; + vector toRemove; + + vec calcAtFinish; + + Solver* S; +}; +}; + +#endif //CONGLOMERATE_H diff --git a/src/sat/cryptominisat2/FindUndef.cpp b/src/sat/cryptominisat2/FindUndef.cpp new file mode 100644 index 0000000..1fdff06 --- /dev/null +++ b/src/sat/cryptominisat2/FindUndef.cpp @@ -0,0 +1,131 @@ +#include "FindUndef.h" + +#include "Solver.h" +#include + +namespace MINISAT +{ + +FindUndef::FindUndef(Solver& _S) : + S(_S) + , isPotentialSum(0) +{ + dontLookAtClause.resize(S.clauses.size(), false); + isPotential.resize(S.nVars(), false); + fillPotential(); + satisfies.resize(S.nVars(), 0); +} + +void FindUndef::fillPotential() +{ + int trail = S.decisionLevel()-1; + + while(trail > 0) { + assert(trail < S.trail_lim.size()); + uint at = S.trail_lim[trail]; + + assert(at > 0); + Var v = S.trail[at].var(); + isPotential[v] = true; + isPotentialSum++; + + trail--; + } + + for (XorClause** it = S.xorclauses.getData(), **end = it + S.xorclauses.size(); it != end; it++) { + XorClause& c = **it; + for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + if (isPotential[l->var()]) { + isPotential[l->var()] = false; + isPotentialSum--; + } + assert(!S.value(*l).isUndef()); + } + } + + vector replacingVars = S.toReplace->getReplacingVars(); + for (Var *it = &replacingVars[0], *end = it + replacingVars.size(); it != end; it++) { + if (isPotential[*it]) { + isPotential[*it] = false; + isPotentialSum--; + } + } +} + +void FindUndef::unboundIsPotentials() +{ + for (uint i = 0; i < isPotential.size(); i++) + if (isPotential[i]) + S.assigns[i] = l_Undef; +} + +const uint FindUndef::unRoll() +{ + while(!updateTables()) { + assert(isPotentialSum > 0); + + uint32_t maximum = 0; + Var v; + for (uint i = 0; i < isPotential.size(); i++) { + if (isPotential[i] && satisfies[i] >= maximum) { + maximum = satisfies[i]; + v = i; + } + } + + isPotential[v] = false; + isPotentialSum--; + + std::fill(satisfies.begin(), satisfies.end(), 0); + } + + unboundIsPotentials(); + + return isPotentialSum; +} + +bool FindUndef::updateTables() +{ + bool allSat = true; + + uint i = 0; + for (Clause** it = S.clauses.getData(), **end = it + S.clauses.size(); it != end; it++, i++) { + if (dontLookAtClause[i]) + continue; + + Clause& c = **it; + bool definitelyOK = false; + Var v; + uint numTrue = 0; + for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + if (S.value(*l) == l_True) { + if (!isPotential[l->var()]) { + dontLookAtClause[i] = true; + definitelyOK = true; + break; + } else { + numTrue ++; + v = l->var(); + } + } + } + if (definitelyOK) + continue; + + if (numTrue == 1) { + isPotential[v] = false; + isPotentialSum--; + dontLookAtClause[i] = true; + continue; + } + + allSat = false; + for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + if (S.value(*l) == l_True) + satisfies[l->var()]++; + } + } + + return allSat; +} +}; diff --git a/src/sat/cryptominisat2/FindUndef.h b/src/sat/cryptominisat2/FindUndef.h new file mode 100644 index 0000000..e47a904 --- /dev/null +++ b/src/sat/cryptominisat2/FindUndef.h @@ -0,0 +1,33 @@ +#ifndef FINDUNDEF_H +#define FINDUNDEF_H + +#include +using std::vector; + +#include "Solver.h" + +namespace MINISAT +{ + +class FindUndef { + public: + FindUndef(Solver& S); + const uint unRoll(); + + private: + Solver& S; + + bool updateTables(); + void fillPotential(); + void unboundIsPotentials(); + + vector dontLookAtClause; //If set to TRUE, then that clause already has only 1 lit that is true, so it can be skipped during updateFixNeed() + vector satisfies; + vector isPotential; + uint32_t isPotentialSum; + +}; +}; + +#endif // + diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp new file mode 100644 index 0000000..e35d667 --- /dev/null +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -0,0 +1,1124 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#include "Gaussian.h" + +#include +#include +#include "Clause.h" +#include + +#ifdef VERBOSE_DEBUG +#include +#endif + +namespace MINISAT +{ +using namespace MINISAT; + +using std::ostream; +using std::cout; +using std::endl; + +uint64_t* PackedRow::tmp_row; + +ostream& operator << (ostream& os, const vec& v) +{ + for (int i = 0; i < v.size(); i++) { + if (v[i].sign()) os << "-"; + os << v[i].var()+1 << " "; + } + + return os; +} + +Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _matrix_no) : + solver(_solver) + , config(_config) + , matrix_no(_matrix_no) + , messed_matrix_vars_since_reversal(true) + , gauss_last_level(0) + , disabled(false) + , useful_prop(0) + , useful_confl(0) + , called(0) +{ + PackedRow::tmp_row = new uint64_t[1000]; +} + +Gaussian::~Gaussian() +{ + clear_clauses(); +} + +void Gaussian::clear_clauses() +{ + std::for_each(matrix_clauses_toclear.begin(), matrix_clauses_toclear.end(), std::ptr_fun(free)); + matrix_clauses_toclear.clear(); +} + +llbool Gaussian::full_init() +{ + assert(config.every_nth_gauss > 0); + assert(config.only_nth_gauss_save >= config.every_nth_gauss); + assert(config.only_nth_gauss_save % config.every_nth_gauss == 0); + assert(config.decision_from % config.every_nth_gauss == 0); + assert(config.decision_from % config.only_nth_gauss_save == 0); + + if (!should_init()) return l_Nothing; + + bool do_again_gauss = true; + while (do_again_gauss) { + do_again_gauss = false; + solver.removeSatisfied(solver.xorclauses); + solver.cleanClauses(solver.xorclauses); + init(); + Clause* confl; + gaussian_ret g = gaussian(confl); + switch (g) { + case unit_conflict: + case conflict: + return l_False; + case unit_propagation: + case propagation: + do_again_gauss=true; + if (solver.propagate() != NULL) return l_False; + break; + case nothing: + break; + } + } + + return l_Nothing; +} + +void Gaussian::init(void) +{ + assert(solver.decisionLevel() == 0); + + matrix_sets.clear(); + fill_matrix(); + if (origMat.num_rows == 0) return; + + cur_matrixset = origMat; + + gauss_last_level = solver.trail.size(); + messed_matrix_vars_since_reversal = false; + if (config.decision_from > 0) went_below_decision_from = true; + else went_below_decision_from = true; + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Gaussian init finished." << endl; + #endif +} + +uint Gaussian::select_columnorder(vector& var_to_col) +{ + var_to_col.resize(solver.nVars(), unassigned_col); + + uint largest_used_var = 0; + uint num_xorclauses = 0; + for (int i = 0; i < solver.xorclauses.size(); i++) { + #ifdef DEBUG_GAUSS + assert(!solver.satisfied(*solver.xorclauses[i])); + #endif + if (solver.xorclauses[i]->getMatrix() == matrix_no) { + num_xorclauses++; + XorClause& c = *solver.xorclauses[i]; + for (uint i2 = 0; i2 < c.size(); i2++) { + assert(solver.assigns[c[i2].var()].isUndef()); + var_to_col[c[i2].var()] = 1; + largest_used_var = std::max(largest_used_var, c[i2].var()); + } + } + } + var_to_col.resize(largest_used_var + 1); + + origMat.col_to_var.clear(); + for (int i = solver.order_heap.size()-1; i >= 0 ; i--) + //for inverse order: + //for (int i = 0; i < order_heap.size() ; i++) + { + Var v = solver.order_heap[i]; + + if (var_to_col[v] == 1) { + #ifdef DEBUG_GAUSS + vector::iterator it = + std::find(origMat.col_to_var.begin(), origMat.col_to_var.end(), v); + assert(it == origMat.col_to_var.end()); + #endif + + origMat.col_to_var.push_back(v); + var_to_col[v] = 2; + } + } + + //for the ones that were not in the order_heap, but are marked in var_to_col + for (uint i = 0; i < var_to_col.size(); i++) { + if (var_to_col[i] == 1) + origMat.col_to_var.push_back(i); + } + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")col_to_var:"; + std::copy(origMat.col_to_var.begin(), origMat.col_to_var.end(), std::ostream_iterator(cout, ",")); + cout << endl; + + cout << "(" << matrix_no << ")var_to_col:" << endl; + #endif + + var_is_in.resize(var_to_col.size()); + var_is_in.setZero(); + origMat.var_is_set.resize(var_to_col.size()); + origMat.var_is_set.setZero(); + for (uint i = 0; i < var_to_col.size(); i++) { + if (var_to_col[i] != unassigned_col) { + vector::iterator it = std::find(origMat.col_to_var.begin(), origMat.col_to_var.end(), i); + assert(it != origMat.col_to_var.end()); + var_to_col[i] = &(*it) - &origMat.col_to_var[0]; + var_is_in.setBit(i); + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")var_to_col[" << i << "]:" << var_to_col[i] << endl; + #endif + } + } + + return num_xorclauses; +} + +void Gaussian::fill_matrix() +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Filling matrix" << endl; + #endif + + vector var_to_col; + origMat.num_rows = select_columnorder(var_to_col); + origMat.num_cols = origMat.col_to_var.size(); + col_to_var_original = origMat.col_to_var; + changed_rows.resize(origMat.num_rows); + changed_rows.setZero(); + if (origMat.num_rows == 0) return; + + origMat.last_one_in_col.resize(origMat.num_cols); + std::fill(origMat.last_one_in_col.begin(), origMat.last_one_in_col.end(), origMat.num_rows); + origMat.past_the_end_last_one_in_col = origMat.num_cols; + + origMat.removeable_cols = 0; + origMat.least_column_changed = -1; + origMat.matrix.resize(origMat.num_rows, origMat.num_cols); + origMat.varset.resize(origMat.num_rows, origMat.num_cols); + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix size:" << origMat.num_rows << "," << origMat.num_cols << endl; + #endif + + uint matrix_row = 0; + for (int i = 0; i < solver.xorclauses.size(); i++) { + const XorClause& c = *solver.xorclauses[i]; + + if (c.getMatrix() == matrix_no) { + origMat.varset[matrix_row].set(c, var_to_col, origMat.num_cols); + origMat.matrix[matrix_row].set(c, var_to_col, origMat.num_cols); + matrix_row++; + } + } + assert(origMat.num_rows == matrix_row); +} + +void Gaussian::update_matrix_col(matrixset& m, const Var var, const uint col) +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Updating matrix var " << var+1 << " (col " << col << ", m.last_one_in_col[col]: " << m.last_one_in_col[col] << ")" << endl; + cout << "m.num_rows:" << m.num_rows << endl; + #endif + + #ifdef DEBUG_GAUSS + assert(col < m.num_cols); + #endif + + m.least_column_changed = std::min(m.least_column_changed, (int)col); + PackedMatrix::iterator this_row = m.matrix.begin(); + uint row_num = 0; + + if (solver.assigns[var].getBool()) { + for (PackedMatrix::iterator end = this_row + std::min(m.last_one_in_col[col], m.num_rows); this_row != end; ++this_row, row_num++) { + PackedRow r = *this_row; + if (r[col]) { + changed_rows.setBit(row_num); + r.invert_xor_clause_inverted(); + r.clearBit(col); + } + } + } else { + for (PackedMatrix::iterator end = this_row + std::min(m.last_one_in_col[col], m.num_rows); this_row != end; ++this_row, row_num++) { + PackedRow r = *this_row; + if (r[col]) { + changed_rows.setBit(row_num); + r.clearBit(col); + } + } + } + + #ifdef DEBUG_GAUSS + bool c = false; + for(PackedMatrix::iterator r = m.matrix.begin(), end = r + m.matrix.size(); r != end; ++r) + c |= (*r)[col]; + assert(!c); + #endif + + m.removeable_cols++; + m.col_to_var[col] = unassigned_var; + m.var_is_set.setBit(var); +} + +void Gaussian::update_matrix_by_col_all(matrixset& m) +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Updating matrix." << endl; + print_matrix(m); + uint num_updated = 0; + #endif + + #ifdef DEBUG_GAUSS + assert(config.every_nth_gauss != 1 || nothing_to_propagate(cur_matrixset)); + assert(check_last_one_in_cols(m)); + #endif + + changed_rows.setZero(); + + uint last = 0; + uint col = 0; + for (Var *it = &m.col_to_var[0], *end = it + m.num_cols; it != end; col++, it++) { + if (*it != unassigned_var && solver.assigns[*it].isDef()) { + update_matrix_col(m, *it, col); + last++; + #ifdef VERBOSE_DEBUG + num_updated++; + #endif + } else + last = 0; + } + m.num_cols -= last; + m.past_the_end_last_one_in_col -= last; + + #ifdef DEBUG_GAUSS + check_matrix_against_varset(m.matrix, m.varset); + #endif + + #ifdef VERBOSE_DEBUG + cout << "Matrix update finished, updated " << num_updated << " cols" << endl; + print_matrix(m); + #endif + + /*cout << "num_rows:" << m.num_rows; + cout << " num_rows diff:" << origMat.num_rows - m.num_rows << endl; + cout << "num_cols:" << col_to_var_original.size(); + cout << " num_cols diff:" << col_to_var_original.size() - m.col_to_var.size() << endl; + cout << "removeable cols:" << m.removeable_cols << endl;*/ +} + +Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl) +{ + if (origMat.num_rows == 0) return nothing; + + if (!messed_matrix_vars_since_reversal) { + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix needs only update" << endl; + #endif + + update_matrix_by_col_all(cur_matrixset); + } else { + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix needs copy&update" << endl; + #endif + + if (went_below_decision_from) + cur_matrixset = origMat; + else + cur_matrixset = matrix_sets[((solver.decisionLevel() - config.decision_from) / config.only_nth_gauss_save)]; + + update_matrix_by_col_all(cur_matrixset); + } + if (!cur_matrixset.num_cols || !cur_matrixset.num_cols) + return nothing; + + messed_matrix_vars_since_reversal = false; + gauss_last_level = solver.trail.size(); + + propagatable_rows.clear(); + + uint conflict_row = UINT_MAX; + uint last_row = eliminate(cur_matrixset, conflict_row); + #ifdef DEBUG_GAUSS + check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset.varset); + #endif + + gaussian_ret ret; + if (conflict_row != UINT_MAX) { + uint maxlevel = UINT_MAX; + uint size = UINT_MAX; + uint best_row = UINT_MAX; + analyse_confl(cur_matrixset, conflict_row, maxlevel, size, best_row); + ret = handle_matrix_confl(confl, cur_matrixset, size, maxlevel, best_row); + + } else { + ret = handle_matrix_prop_and_confl(cur_matrixset, last_row, confl); + } + + if (ret == nothing + && (solver.decisionLevel() == 0 || ((solver.decisionLevel() - config.decision_from) % config.only_nth_gauss_save == 0)) + ) + set_matrixset_to_cur(); + + #ifdef VERBOSE_DEBUG + if (ret == nothing) + cout << "(" << matrix_no << ")Useless. "; + else + cout << "(" << matrix_no << ")Useful. "; + cout << "(" << matrix_no << ")Useful prop in " << ((double)useful_prop/(double)called)*100.0 << "%" << endl; + cout << "(" << matrix_no << ")Useful confl in " << ((double)useful_confl/(double)called)*100.0 << "%" << endl; + #endif + + return ret; +} + +uint Gaussian::eliminate(matrixset& m, uint& conflict_row) +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")"; + cout << "Starting elimination" << endl; + cout << "m.least_column_changed:" << m.least_column_changed << endl; + print_last_one_in_cols(m); + + uint number_of_row_additions = 0; + uint no_exchanged = 0; + #endif + + if (m.least_column_changed == INT_MAX) { + #ifdef VERBOSE_DEBUG + cout << "Nothing to eliminate" << endl; + #endif + + return m.num_rows; + } + + + #ifdef DEBUG_GAUSS + assert(check_last_one_in_cols(m)); + #endif + + uint i = 0; + uint j = m.least_column_changed + 1; + + if (j) { + uint16_t until = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows); + if (j > m.past_the_end_last_one_in_col) + until = m.num_rows; + for (;i != until; i++) if (changed_rows[i] && m.matrix[i].popcnt_is_one()) + propagatable_rows.push(i); + } + + if (j > m.past_the_end_last_one_in_col) { + #ifdef VERBOSE_DEBUG + cout << "Going straight to finish" << endl; + #endif + goto finish; + } + + #ifdef VERBOSE_DEBUG + cout << "At while() start: i,j = " << i << ", " << j << endl; + #endif + + #ifdef DEBUG_GAUSS + assert(i <= m.num_rows && j <= m.num_cols); + #endif + + while (i != m.num_rows && j != m.num_cols) { + //Find pivot in column j, starting in row i: + + if (m.col_to_var[j] == unassigned_var) { + j++; + continue; + } + + uint best_row = i; + PackedMatrix::iterator this_matrix_row = m.matrix.begin() + i; + PackedMatrix::iterator end = m.matrix.begin() + std::min(m.last_one_in_col[j], m.num_rows); + for (; this_matrix_row != end; ++this_matrix_row, best_row++) { + if ((*this_matrix_row)[j]) + break; + } + + if (this_matrix_row != end) { + PackedRow matrix_row_i = m.matrix[i]; + PackedRow varset_row_i = m.varset[i]; + + //swap rows i and maxi, but do not change the value of i; + if (i != best_row) { + #ifdef VERBOSE_DEBUG + no_exchanged++; + #endif + + if (!matrix_row_i.get_xor_clause_inverted() && matrix_row_i.isZero()) { + conflict_row = i; + return 0; + } + matrix_row_i.swap(*this_matrix_row); + varset_row_i.swap(m.varset[best_row]); + } + #ifdef DEBUG_GAUSS + assert(m.matrix[i].popcnt(j) == m.matrix[i].popcnt()); + assert(m.matrix[i][j]); + #endif + + if (matrix_row_i.popcnt_is_one(j)) + propagatable_rows.push(i); + + //Now A[i,j] will contain the old value of A[maxi,j]; + uint i2 = best_row+1; + for (PackedMatrix::iterator it = this_matrix_row+1, it2 = m.varset.begin() + i2; it != end; ++it, ++it2, i2++) if ((*it)[j]) { + //subtract row i from row u; + //Now A[u,j] will be 0, since A[u,j] - A[i,j] = A[u,j] -1 = 0. + #ifdef VERBOSE_DEBUG + number_of_row_additions++; + #endif + + *it ^= matrix_row_i; + *it2 ^= varset_row_i; + //Would early abort, but would not find the best conflict: + //if (!it->get_xor_clause_inverted() &&it->isZero()) { + // conflict_row = i2; + // return 0; + //} + } + i++; + m.last_one_in_col[j] = i; + } else + m.last_one_in_col[j] = i + 1; + j++; + } + + m.past_the_end_last_one_in_col = j; + + finish: + + m.least_column_changed = INT_MAX; + + #ifdef VERBOSE_DEBUG + cout << "Finished elimination" << endl; + cout << "Returning with i,j:" << i << ", " << j << "(" << m.num_rows << ", " << m.num_cols << ")" << endl; + print_matrix(m); + print_last_one_in_cols(m); + cout << "(" << matrix_no << ")Exchanged:" << no_exchanged << " row additions:" << number_of_row_additions << endl; + #endif + + #ifdef DEBUG_GAUSS + assert(check_last_one_in_cols(m)); + uint row = 0; + uint col = 0; + for (; col < m.num_cols && row < m.num_rows && row < i && col < m.past_the_end_last_one_in_col; col++) { + assert(m.matrix[row].popcnt() == m.matrix[row].popcnt(col)); + assert(!(m.col_to_var[col] == unassigned_var && m.matrix[row][col])); + if (m.col_to_var[col] == unassigned_var || !m.matrix[row][col]) { + #ifdef VERBOSE_DEBUG + cout << "row:" << row << " col:" << col << " m.last_one_in_col[col]-1: " << m.last_one_in_col[col]-1 << endl; + #endif + assert(m.last_one_in_col[col]-1 == row); + continue; + } + row++; + } + #endif + + return i; +} + +Gaussian::gaussian_ret Gaussian::handle_matrix_confl(Clause*& confl, const matrixset& m, const uint size, const uint maxlevel, const uint best_row) +{ + assert(best_row != UINT_MAX); + + confl = Clause_new(m.varset[best_row], solver.assigns, col_to_var_original, solver.learnt_clause_group++); + Clause& cla = *confl; + if (solver.dynamic_behaviour_analysis) + solver.logger.set_group_name(confl->group, "learnt gauss clause"); + + if (cla.size() <= 1) + return unit_conflict; + + assert(cla.size() >= 2); + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Found conflict:"; + solver.printClause(cla); + #endif + + if (maxlevel != solver.decisionLevel()) { + if (solver.dynamic_behaviour_analysis) + solver.logger.conflict(Logger::gauss_confl_type, maxlevel, confl->group, *confl); + solver.cancelUntil(maxlevel); + } + const uint curr_dec_level = solver.decisionLevel(); + assert(maxlevel == curr_dec_level); + + uint maxsublevel = 0; + uint maxsublevel_at = UINT_MAX; + for (uint i = 0, size = cla.size(); i < size; i++) if (solver.level[cla[i].var()] == curr_dec_level) { + uint tmp = find_sublevel(cla[i].var()); + if (tmp >= maxsublevel) { + maxsublevel = tmp; + maxsublevel_at = i; + } + } + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ") || Sublevel of confl: " << maxsublevel << " (due to var:" << cla[maxsublevel_at].var()-1 << ")" << endl; + #endif + + Lit tmp(cla[maxsublevel_at]); + cla[maxsublevel_at] = cla[1]; + cla[1] = tmp; + + cancel_until_sublevel(maxsublevel+1); + messed_matrix_vars_since_reversal = true; + return conflict; +} + +Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint last_row, Clause*& confl) +{ + uint maxlevel = UINT_MAX; + uint size = UINT_MAX; + uint best_row = UINT_MAX; + + for (uint row = last_row; row != m.num_rows; row++) { + #ifdef DEBUG_GAUSS + assert(m.matrix[row].isZero()); + #endif + if (!m.matrix[row].get_xor_clause_inverted()) + analyse_confl(m, row, maxlevel, size, best_row); + } + + if (maxlevel != UINT_MAX) + return handle_matrix_confl(confl, m, size, maxlevel, best_row); + + #ifdef DEBUG_GAUSS + assert(check_no_conflict(m)); + #endif + m.num_rows = last_row; + m.matrix.resizeNumRows(m.num_rows); + m.varset.resizeNumRows(m.num_rows); + + gaussian_ret ret = nothing; + + uint num_props = 0; + for (const uint* prop_row = propagatable_rows.getData(), *end = prop_row + propagatable_rows.size(); prop_row != end; prop_row++ ) { + //this is a "000..1..0000000X" row. I.e. it indicates a propagation + ret = handle_matrix_prop(m, *prop_row); + num_props++; + if (ret == unit_propagation) { + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Unit prop! Breaking from prop examination" << endl; + #endif + return unit_propagation; + } + } + #ifdef VERBOSE_DEBUG + if (num_props > 0) cout << "(" << matrix_no << ")Number of props during gauss:" << num_props << endl; + #endif + + return ret; +} + +uint Gaussian::find_sublevel(const Var v) const +{ + for (int i = solver.trail.size()-1; i >= 0; i --) + if (solver.trail[i].var() == v) return i; + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Oooops! Var " << v+1 << " does not have a sublevel!! (so it must be undefined)" << endl; + #endif + + assert(false); + return 0; +} + +void Gaussian::cancel_until_sublevel(const uint sublevel) +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Canceling until sublevel " << sublevel << endl; + #endif + + for (int level = solver.trail.size()-1; level >= sublevel; level--) { + Var var = solver.trail[level].var(); + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Canceling var " << var+1 << endl; + #endif + + solver.assigns[var] = l_Undef; + solver.insertVarOrder(var); + for (Gaussian **gauss = &(solver.gauss_matrixes[0]), **end= gauss + solver.gauss_matrixes.size(); gauss != end; gauss++) + if (*gauss != this) (*gauss)->canceling(level, var); + } + solver.trail.shrink(solver.trail.size() - sublevel); + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Canceling sublevel finished." << endl; + #endif +} + +void Gaussian::analyse_confl(const matrixset& m, const uint row, uint& maxlevel, uint& size, uint& best_row) const +{ + assert(row < m.num_rows); + + //this is a "000...00000001" row. I.e. it indicates we are on the wrong branch + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix conflict found!" << endl; + cout << "(" << matrix_no << ")conflict clause's vars: "; + print_matrix_row_with_assigns(m.varset[row]); + cout << endl; + + cout << "(" << matrix_no << ")corresponding matrix's row (should be empty): "; + print_matrix_row(m.matrix[row]); + cout << endl; + #endif + + uint this_maxlevel = 0; + unsigned long int var = 0; + uint this_size = 0; + while (true) { + var = m.varset[row].scan(var); + if (var == ULONG_MAX) break; + + const Var real_var = col_to_var_original[var]; + assert(real_var < solver.nVars()); + + if (solver.level[real_var] > this_maxlevel) + this_maxlevel = solver.level[real_var]; + var++; + this_size++; + } + + //the maximum of all lit's level must be lower than the max. level of the current best clause (or this clause must be either empty or unit clause) + if (!( + (this_maxlevel < maxlevel) + || (this_maxlevel == maxlevel && this_size < size) + || (this_size <= 1) + )) { + assert(maxlevel != UINT_MAX); + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Other found conflict just as good or better."; + cout << "(" << matrix_no << ") || Old maxlevel:" << maxlevel << " new maxlevel:" << this_maxlevel; + cout << "(" << matrix_no << ") || Old size:" << size << " new size:" << this_size << endl; + //assert(!(maxlevel != UINT_MAX && maxlevel != this_maxlevel)); //NOTE: only holds if gauss is executed at each level + #endif + + return; + } + + + #ifdef VERBOSE_DEBUG + if (maxlevel != UINT_MAX) + cout << "(" << matrix_no << ")Better conflict found."; + else + cout << "(" << matrix_no << ")Found a possible conflict."; + + cout << "(" << matrix_no << ") || Old maxlevel:" << maxlevel << " new maxlevel:" << this_maxlevel; + cout << "(" << matrix_no << ") || Old size:" << size << " new size:" << this_size << endl; + #endif + + maxlevel = this_maxlevel; + size = this_size; + best_row = row; +} + +Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row) +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix prop found!" << endl; + cout << m.matrix[row] << endl; + cout << "(" << matrix_no << ")matrix row:"; + print_matrix_row(m.matrix[row]); + cout << endl; + #endif + + Clause& cla = *Clause_new(m.varset[row], solver.assigns, col_to_var_original, solver.learnt_clause_group++); + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix prop clause: "; + solver.printClause(cla); + cout << endl; + #endif + + assert(!m.matrix[row].get_xor_clause_inverted() == !cla[0].sign()); + assert(solver.assigns[cla[0].var()].isUndef()); + if (cla.size() == 1) { + const Lit lit = cla[0]; + if (solver.dynamic_behaviour_analysis) { + solver.logger.set_group_name(cla.group, "unitary learnt clause"); + solver.logger.conflict(Logger::gauss_confl_type, 0, cla.group, cla); + } + + solver.cancelUntil(0); + solver.uncheckedEnqueue(lit); + solver.unitary_learnts.push(&cla); + if (solver.dynamic_behaviour_analysis) + solver.logger.propagation(cla[0], Logger::gauss_propagation_type, cla.group); + return unit_propagation; + } + + matrix_clauses_toclear.push_back(&cla); + solver.uncheckedEnqueue(cla[0], &cla); + if (solver.dynamic_behaviour_analysis) { + solver.logger.set_group_name(cla.group, "gauss prop clause"); + solver.logger.propagation(cla[0], Logger::gauss_propagation_type, cla.group); + } + + return propagation; +} + +void Gaussian::disable_if_necessary() +{ + if (//nof_conflicts >= 0 + //&& conflictC >= nof_conflicts/8 + /*&&*/ called > 100 + && (double)useful_confl/(double)called < 0.1 + && (double)useful_prop/(double)called < 0.3 ) + disabled = true; +} + +llbool Gaussian::find_truths(vec& learnt_clause, int& conflictC) +{ + Clause* confl; + + disable_if_necessary(); + if (should_check_gauss(solver.decisionLevel(), solver.starts)) { + called++; + gaussian_ret g = gaussian(confl); + + switch (g) { + case conflict: { + useful_confl++; + llbool ret = solver.handle_conflict(learnt_clause, confl, conflictC); + free(confl); + + if (ret != l_Nothing) return ret; + return l_Continue; + } + case propagation: + case unit_propagation: + useful_prop++; + return l_Continue; + case unit_conflict: { + useful_confl++; + if (confl->size() == 0) { + free(confl); + return l_False; + } + + Lit lit = (*confl)[0]; + if (solver.dynamic_behaviour_analysis) + solver.logger.conflict(Logger::gauss_confl_type, 0, confl->group, *confl); + + solver.cancelUntil(0); + + if (solver.assigns[lit.var()].isDef()) { + if (solver.dynamic_behaviour_analysis) + solver.logger.empty_clause(confl->group); + + free(confl); + return l_False; + } + + solver.uncheckedEnqueue(lit); + if (solver.dynamic_behaviour_analysis) + solver.logger.propagation(lit, Logger::gauss_propagation_type, confl->group); + + free(confl); + return l_Continue; + } + case nothing: + break; + } + } + + return l_Nothing; +} + +template +void Gaussian::print_matrix_row(const T& row) const +{ + unsigned long int var = 0; + while (true) { + var = row.scan(var); + if (var == ULONG_MAX) break; + + else cout << col_to_var_original[var]+1 << ", "; + var++; + } + if (row.get_xor_clause_inverted()) cout << "xor_clause_inverted"; +} + +template +void Gaussian::print_matrix_row_with_assigns(const T& row) const +{ + unsigned long int col = 0; + while (true) { + col = row.scan(col); + if (col == ULONG_MAX) break; + + else { + Var var = col_to_var_original[col]; + cout << var+1 << "(" << lbool_to_string(solver.assigns[var]) << ")"; + cout << ", "; + } + col++; + } + if (row.get_xor_clause_inverted()) cout << "xor_clause_inverted"; +} + +const string Gaussian::lbool_to_string(const lbool toprint) +{ + if (toprint == l_True) + return "true"; + if (toprint == l_False) + return "false"; + if (toprint == l_Undef) + return "undef"; + + assert(false); + return ""; +} + + +void Gaussian::print_stats() const +{ + if (called > 0) { + cout.setf(std::ios::fixed); + std::cout << " Gauss(" << matrix_no << ") useful"; + cout << " prop: " << std::setprecision(2) << std::setw(5) << ((double)useful_prop/(double)called)*100.0 << "% "; + cout << " confl: " << std::setprecision(2) << std::setw(5) << ((double)useful_confl/(double)called)*100.0 << "% "; + if (disabled) std::cout << "disabled"; + } else + std::cout << " Gauss(" << matrix_no << ") not called."; +} + +void Gaussian::reset_stats() +{ + useful_prop = 0; + useful_confl = 0; + called = 0; + disabled = false; +} + +bool Gaussian::check_no_conflict(matrixset& m) const +{ + uint row = 0; + for(PackedMatrix::iterator r = m.matrix.begin(), end = m.matrix.end(); r != end; ++r, ++row) { + if (!(*r).get_xor_clause_inverted() && (*r).isZero()) { + cout << "Conflict at row " << row << endl; + return false; + } + } + return true; +} + +void Gaussian::print_matrix(matrixset& m) const +{ + uint row = 0; + for (PackedMatrix::iterator it = m.matrix.begin(); it != m.matrix.end(); ++it, row++) { + cout << *it << " -- row:" << row; + if (row >= m.num_rows) + cout << " (considered past the end)"; + cout << endl; + } +} + +void Gaussian::print_last_one_in_cols(matrixset& m) const +{ + for (uint i = 0; i < m.num_cols; i++) { + cout << "last_one_in_col[" << i << "]-1 = " << m.last_one_in_col[i]-1 << endl; + } + cout << "m.past_the_end_last_one_in_col:" << m.past_the_end_last_one_in_col << endl; +} + +const bool Gaussian::nothing_to_propagate(matrixset& m) const +{ + for(PackedMatrix::iterator r = m.matrix.begin(), end = m.matrix.end(); r != end; ++r) { + if ((*r).popcnt_is_one() + && solver.assigns[m.col_to_var[(*r).scan(0)]].isUndef()) + return false; + } + for(PackedMatrix::iterator r = m.matrix.begin(), end = m.matrix.end(); r != end; ++r) { + if ((*r).isZero() && !(*r).get_xor_clause_inverted()) + return false; + } + return true; +} + +const bool Gaussian::check_last_one_in_cols(matrixset& m) const +{ + for(uint i = 0; i < m.num_cols; i++) { + const uint last = m.last_one_in_col[i] - 1; + uint real_last = 0; + uint i2; + for (PackedMatrix::iterator it = m.matrix.begin(); it != m.matrix.end(); ++it, i2++) { + if ((*it)[i]) + real_last = i2; + } + if (real_last > last) return false; + } + + return true; +} + +const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset) const +{ + assert(matrix.size() == varset.size()); + + for (uint i = 0; i < matrix.size(); i++) { + const PackedRow mat_row = matrix[i]; + const PackedRow var_row = varset[i]; + + unsigned long int col = 0; + bool final = false; + while (true) { + col = var_row.scan(col); + if (col == ULONG_MAX) break; + + const Var var = col_to_var_original[col]; + assert(var < solver.nVars()); + + if (solver.assigns[var] == l_True) { + assert(!mat_row[col]); + final = !final; + } else if (solver.assigns[var] == l_False) { + assert(!mat_row[col]); + } else if (solver.assigns[var] == l_Undef) { + assert(mat_row[col]); + } else assert(false); + + col++; + } + if ((final^mat_row.get_xor_clause_inverted()) != var_row.get_xor_clause_inverted()) { + cout << "problem with row:"; print_matrix_row_with_assigns(var_row); cout << endl; + assert(false); + } + } +} + +const uint Gaussian::get_called() const +{ + return called; +} + +const uint Gaussian::get_useful_prop() const +{ + return useful_prop; +} + +const uint Gaussian::get_useful_confl() const +{ + return useful_confl; +} + +const bool Gaussian::get_disabled() const +{ + return disabled; +} + +void Gaussian::set_disabled(const bool toset) +{ + disabled = toset; +} + +//old functions + +/*void Gaussian::update_matrix_by_row(matrixset& m) const +{ +#ifdef VERBOSE_DEBUG + cout << "Updating matrix." << endl; + uint num_updated = 0; +#endif +#ifdef DEBUG_GAUSS + assert(nothing_to_propagate(cur_matrixset)); +#endif + + mpz_class toclear, tocount; + uint last_col = 0; + + for (uint col = 0; col < m.num_cols; col ++) { + Var var = m.col_to_var[col]; + + if (var != UINT_MAX && !solver.assigns[var].isUndef()) { + toclear.setBit(col); + if (solver.assigns[var].getBool()) tocount.setBit(col); + +#ifdef DEBUG_GAUSS + assert(m.var_to_col[var] < UINT_MAX-1); +#endif + last_col = col; + m.least_column_changed = std::min(m.least_column_changed, (int)col); + + m.removeable_cols++; + m.col_to_var[col] = UINT_MAX; + m.var_to_col[var] = UINT_MAX-1; +#ifdef VERBOSE_DEBUG + num_updated++; +#endif + } + } + + toclear.invert(); + mpz_class tmp; + mpz_class* this_row = &m.matrix[0]; + for(uint i = 0, until = std::min(m.num_rows, m.last_one_in_col[last_col]+1); i < until; i++, this_row++) { + mpz_class& r = *this_row; + mpz_and(tmp.get_mp(), tocount.get_mp(), r.get_mp()); + r.invert_xor_clause_inverted(tmp.popcnt() % 2); + r &= toclear; +} + +#ifdef VERBOSE_DEBUG + cout << "Updated " << num_updated << " matrix cols. Could remove " << m.removeable_cols << " cols " <= last_level; level--){ + Var var = solver.trail[level].var(); + const uint col = m.var_to_col[var]; + if ( col < UINT_MAX-1) { + update_matrix_col(m, var, col); +#ifdef VERBOSE_DEBUG + num_updated++; +#endif + } + } + +#ifdef VERBOSE_DEBUG + cout << "Updated " << num_updated << " matrix cols. Could remove " << m.removeable_cols << " cols (out of " << m.num_cols << " )" <. +**************************************************************************************************/ + +#ifndef GAUSSIAN_H +#define GAUSSIAN_H + +#include +#include "SolverTypes.h" +#include "Solver.h" +#include "GaussianConfig.h" +#include "PackedMatrix.h" +#include "BitArray.h" + +namespace MINISAT +{ +using namespace MINISAT; + +using std::vector; +using std::cout; +using std::endl; + +class Clause; + +static const uint16_t unassigned_col = -1; +static const Var unassigned_var = -1; + +//#define VERBOSE_DEBUG +//#define DEBUG_GAUSS +class Gaussian +{ +public: + Gaussian(Solver& solver, const GaussianConfig& config, const uint matrix_no); + ~Gaussian(); + + llbool full_init(); + llbool find_truths(vec& learnt_clause, int& conflictC); + + //statistics + void print_stats() const; + void reset_stats(); + void print_matrix_stats() const; + const uint get_called() const; + const uint get_useful_prop() const; + const uint get_useful_confl() const; + const bool get_disabled() const; + void set_disabled(const bool toset); + + //functions used throughout the Solver + void back_to_level(const uint level); + void canceling(const uint level, const Var var); + void clear_clauses(); + +protected: + Solver& solver; + + //Gauss high-level configuration + const GaussianConfig& config; + const uint matrix_no; + + enum gaussian_ret {conflict, unit_conflict, propagation, unit_propagation, nothing}; + gaussian_ret gaussian(Clause*& confl); + + vector col_to_var_original; + BitArray var_is_in; + + class matrixset + { + public: + PackedMatrix matrix; // The matrix, updated to reflect variable assignements + PackedMatrix varset; // The matrix, without variable assignements. The xor-clause is read from here. This matrix only follows the 'matrix' with its row-swap, row-xor, and row-delete operations. + BitArray var_is_set; + vector col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives UINT_MAX if the COL has been zeroed (i.e. the variable assigned) + uint16_t num_rows; // number of active rows in the matrix. Unactive rows are rows that contain only zeros (and if they are conflicting, then the conflict has been treated) + uint num_cols; // number of active columns in the matrix. The columns at the end that have all be zeroed are no longer active + int least_column_changed; // when updating the matrix, this value contains the smallest column number that has been updated (Gauss elim. can start from here instead of from column 0) + uint16_t past_the_end_last_one_in_col; + vector last_one_in_col; //last_one_in_col[COL] tells the last row that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row) + uint removeable_cols; // the number of columns that have been zeroed out (i.e. assigned) + }; + + //Saved states + vector matrix_sets; // The matrixsets for depths 'decision_from' + 0, 'decision_from' + only_nth_gaussian_save, 'decision_from' + 2*only_nth_gaussian_save, ... 'decision_from' + 'decision_until'. + matrixset origMat; // The matrixset at depth 0 of the search tree + matrixset cur_matrixset; // The current matrixset, i.e. the one we are working on, or the last one we worked on + + //Varibales to keep Gauss state + bool messed_matrix_vars_since_reversal; + int gauss_last_level; + vector matrix_clauses_toclear; + bool went_below_decision_from; + bool disabled; // Gauss is disabled + + //State of current elimnation + vec propagatable_rows; //used to store which rows were deemed propagatable during elimination + BitArray changed_rows; //used to store which rows were deemed propagatable during elimination + + //Statistics + uint useful_prop; //how many times Gauss gave propagation as a result + uint useful_confl; //how many times Gauss gave conflict as a result + uint called; //how many times called the Gauss + + //gauss init functions + void init(); // Initalise gauss state + void fill_matrix(); // Fills the origMat matrix + uint select_columnorder(vector& var_to_col); // Fills var_to_col and col_to_var of the origMat matrix. + + //Main function + uint eliminate(matrixset& matrix, uint& conflict_row); //does the actual gaussian elimination + + //matrix update functions + void update_matrix_col(matrixset& matrix, const Var x, const uint col); // Update one matrix column + void update_matrix_by_col_all(matrixset& m); // Update all columns, column-by-column (and not row-by-row) + void set_matrixset_to_cur(); // Save the current matrixset, the cur_matrixset to matrix_sets + //void update_matrix_by_row(matrixset& matrix) const; + //void update_matrix_by_col(matrixset& matrix, const uint last_level) const; + + //conflict&propagation handling + gaussian_ret handle_matrix_prop_and_confl(matrixset& m, uint row, Clause*& confl); + void analyse_confl(const matrixset& m, const uint row, uint& maxlevel, uint& size, uint& 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(Clause*& confl, const matrixset& m, const uint size, const uint maxlevel, const uint best_row); + gaussian_ret handle_matrix_prop(matrixset& m, const uint row); // Handle matrix propagation at row 'row' + + //propagation&conflict handling + void cancel_until_sublevel(const uint sublevel); // cancels until sublevel 'sublevel'. The var 'sublevel' must NOT go over the current level. I.e. this function is ONLY for moving inside the current level + uint find_sublevel(const Var v) const; // find the sublevel (i.e. trail[X]) of a given variable + + //helper functions + bool at_first_init() const; + bool should_init() const; + bool should_check_gauss(const uint decisionlevel, const uint starts) const; + void disable_if_necessary(); + +private: + + //debug functions + bool check_no_conflict(matrixset& m) const; // Are there any conflicts that the matrixset 'm' causes? + const bool nothing_to_propagate(matrixset& m) const; // Are there any conflicts of propagations that matrixset 'm' clauses? + template + void print_matrix_row(const T& row) const; // Print matrix row 'row' + template + void print_matrix_row_with_assigns(const T& row) const; + const bool check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset) const; + const bool check_last_one_in_cols(matrixset& m) const; + void print_matrix(matrixset& m) const; + void print_last_one_in_cols(matrixset& m) const; + static const string lbool_to_string(const lbool toprint); +}; + +inline void Gaussian::back_to_level(const uint level) +{ + if (level <= config.decision_from) went_below_decision_from = true; +} + +inline bool Gaussian::should_init() const +{ + return (solver.starts >= config.starts_from && config.decision_until > 0); +} + +inline bool Gaussian::should_check_gauss(const uint decisionlevel, const uint starts) const +{ + return (!disabled + && starts >= config.starts_from + && decisionlevel < config.decision_until + && decisionlevel >= config.decision_from + && decisionlevel % config.every_nth_gauss == 0); +} + +inline void Gaussian::canceling(const uint level, const Var var) +{ + if (!messed_matrix_vars_since_reversal + && level <= gauss_last_level + && var < var_is_in.getSize() + && var_is_in[var] + && cur_matrixset.var_is_set[var] + ) + messed_matrix_vars_since_reversal = true; +} + +inline void Gaussian::print_matrix_stats() const +{ + cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl; +} + +inline void Gaussian::set_matrixset_to_cur() +{ + /*cout << solver.decisionLevel() << endl; + cout << decision_from << endl; + cout << matrix_sets.size() << endl;*/ + + if (solver.decisionLevel() == 0) { + origMat = cur_matrixset; + } + + if (solver.decisionLevel() >= config.decision_from) { + uint level = ((solver.decisionLevel() - config.decision_from) / config.only_nth_gauss_save); + + assert(level <= matrix_sets.size()); //TODO check if we need this, or HOW we need this in a multi-matrix setting + if (level == matrix_sets.size()) + matrix_sets.push_back(cur_matrixset); + else + matrix_sets[level] = cur_matrixset; + } +} + +std::ostream& operator << (std::ostream& os, const vec& v); +}; + +#endif //GAUSSIAN_H diff --git a/src/sat/cryptominisat2/GaussianConfig.h b/src/sat/cryptominisat2/GaussianConfig.h new file mode 100644 index 0000000..449b03e --- /dev/null +++ b/src/sat/cryptominisat2/GaussianConfig.h @@ -0,0 +1,44 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef GAUSSIANCONFIG_H +#define GAUSSIANCONFIG_H + +#include + +class GaussianConfig +{ + public: + + GaussianConfig() : + only_nth_gauss_save(2) + , decision_from(0) + , decision_until(0) + , every_nth_gauss(1) + , starts_from(3) + { + } + + //tuneable gauss parameters + uint only_nth_gauss_save; //save only every n-th gauss matrix + uint decision_from; //start from this decision level + uint decision_until; //do Gauss until this level + uint every_nth_gauss; //do Gauss every nth level + uint starts_from; //Gauss elimination starts from this restart number +}; + +#endif //GAUSSIANCONFIG_H \ No newline at end of file diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp new file mode 100644 index 0000000..bb15f2d --- /dev/null +++ b/src/sat/cryptominisat2/Logger.cpp @@ -0,0 +1,871 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include +#include +#include +#include +#include +#include +#include +#include +using std::cout; +using std::endl; +using std::ofstream; + +#include "Logger.h" +#include "SolverTypes.h" +#include "Solver.h" +#include "Gaussian.h" + +namespace MINISAT +{ + +#define FST_WIDTH 10 +#define SND_WIDTH 35 +#define TRD_WIDTH 10 + +Logger::Logger(int& _verbosity) : + proof_graph_on(false) + , statistics_on(false) + , mini_proof(false) + + , max_print_lines(20) + , uniqueid(1) + + , proof(NULL) + + , sum_conflict_depths(0) + , no_conflicts(0) + , no_decisions(0) + , no_propagations(0) + , sum_decisions_on_branches(0) + , sum_propagations_on_branches(0) + + , verbosity(_verbosity) + , begin_called(false) +{ + runid /= 10; + runid = time(NULL) % 10000; + if (verbosity >= 1) printf("RunID is: #%d\n",runid); +} + +void Logger::setSolver(const Solver* _S) +{ + S = _S; +} + +// Adds a new variable to the knowledge of the logger +void Logger::new_var(const Var var) +{ + if (!statistics_on && !proof_graph_on) + return; + + if (varnames.size() <= var) { + varnames.resize(var+1); + times_var_propagated.resize(var+1, 0); + times_var_guessed.resize(var+1, 0); + depths_of_assigns_for_var.resize(var+1); + } + std::stringstream ss; + ss << var + 1; + varnames[var] = ss.str(); +} + +// Resizes the groupnames and other, related vectors to accomodate for a new group +void Logger::new_group(const uint group) +{ + if (groupnames.size() <= group) { + groupnames.resize(group+1, "Noname"); + times_group_caused_conflict.resize(group+1, 0); + times_group_caused_propagation.resize(group+1, 0); + depths_of_propagations_for_group.resize(group+1); + depths_of_conflicts_for_group.resize(group+1); + } +} + +void Logger::cut_name_to_size(string& name) const +{ + uint len = name.length(); + if (len > 0 && name[len-1] == '\r') { + name[len-1] = '\0'; + len--; + } + + if (len > SND_WIDTH-2) { + name[SND_WIDTH-2] = '\0'; + name[SND_WIDTH-3] = '.'; + name[SND_WIDTH-4] = '.'; + } +} + +// Adds the new clause group's name to the information stored +void Logger::set_group_name(const uint group, string name) +{ + if (!statistics_on && !proof_graph_on) + return; + + new_group(group); + cut_name_to_size(name); + + if (name.length() == 0) return; + + if (groupnames[group] == "Noname") { + groupnames[group] = name; + } else if (groupnames[group] != name) { + printf("Error! Group no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", group, groupnames[group].c_str(), name.c_str()); + exit(-1); + } +} + +// sets the variable's name +void Logger::set_variable_name(const uint var, string name) +{ + if (!statistics_on && !proof_graph_on) + return; + + new_var(var); + cut_name_to_size(name); + + std::stringstream ss; + ss << var + 1; + if (varnames[var] == ss.str()) { + varnames[var] = name; + } else if (varnames[var] != name) { + printf("Error! Variable no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", var+1, varnames[var].c_str(), name.c_str()); + exit(-1); + } +} + +void Logger::first_begin() +{ + if (begin_called) + return; + + begin_called = true; + begin(); +} + +void Logger::begin() +{ + if (proof_graph_on) { + char filename[80]; + sprintf(filename, "proofs/%d-proof%d.dot", runid, S->starts); + + if (S->starts == 0) + history.push_back(uniqueid); + else { + if (mini_proof) + history.resize(S->decisionLevel()+1); + else + history.resize(S->trail.size()+1); + } + + proof = fopen(filename,"w"); + if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename), exit(-1); + fprintf(proof, "digraph G {\n"); + fprintf(proof,"node%d [shape=circle, label=\"BEGIN\", root];\n", history[history.size()-1]); + } + + if (statistics_on) + reset_statistics(); +} + +// For noting conflicts. Updates the proof graph and the statistics. +template +void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const T& learnt_clause) +{ + 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 (int i = 0; i < learnt_clause.size(); i++) { + if (learnt_clause[i].sign()) fprintf(proof,"-"); + int myvar = learnt_clause[i].var(); + fprintf(proof,"%s\\n",varnames[myvar].c_str()); + } + } + fprintf(proof,"\"];\n"); + + fprintf(proof,"node%d -> node%d [label=\"",history[history.size()-1],uniqueid); + if (type == gauss_confl_type) + fprintf(proof,"Gauss\",style=bold"); + else + fprintf(proof,"%s\"", groupnames[group].c_str()); + fprintf(proof,"];\n"); + + if (!mini_proof) + history.resize(goback_sublevel+1); + else + history.resize(goback_level+1); + fprintf(proof,"node%d -> node%d [style=dotted];\n",uniqueid,history[history.size()-1]); + } + + if (statistics_on) { + times_group_caused_conflict[group]++; + depths_of_conflicts_for_group[group].push_back(S->decisionLevel()); + + 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(); + + map::iterator it = branch_depth_distrib.find(S->decisionLevel()); + if (it == branch_depth_distrib.end()) + branch_depth_distrib[S->decisionLevel()] = 1; + else + it->second++; + } +} + +template void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const Clause& learnt_clause); + +template void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const vec& learnt_clause); + +// For the really strange event that the solver is given an empty clause +void Logger::empty_clause(const uint group) +{ + first_begin(); + assert(!(proof == NULL && proof_graph_on)); + + if (proof_graph_on) { + uniqueid++; + fprintf(proof,"node%d -> node%d [label=\"emtpy clause:",history[history.size()-1],uniqueid); + fprintf(proof,"%s\"];\n", groupnames[group].c_str()); + history.push_back(uniqueid); + } +} + +// Propagating a literal. Type of literal and the (learned clause's)/(propagating clause's)/(etc) group must be given. Updates the proof graph and the statistics. note: the meaning of the variable 'group' depends on the type +void Logger::propagation(const Lit lit, const prop_type type, const uint group) +{ + first_begin(); + assert(!(proof == NULL && proof_graph_on)); + + //graph + if (proof_graph_on && (!mini_proof || type == guess_type || type == assumption_type)) { + uniqueid++; + + fprintf(proof,"node%d [shape=box, label=\"",uniqueid);; + if (lit.sign()) + fprintf(proof,"-"); + fprintf(proof,"%s\"];\n",varnames[lit.var()].c_str()); + + 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 gauss_propagation_type: + fprintf(proof,"Gauss propagation\",style=bold];\n"); + break; + + case add_clause_type: + fprintf(proof,"red. from %s\"];\n",groupnames[group].c_str()); + break; + + case unit_clause_type: + fprintf(proof,"unit clause %s,style=bold\"];\n",groupnames[group].c_str()); + break; + + case assumption_type: + fprintf(proof,"assumption\"];\n"); + break; + + case guess_type: + fprintf(proof,"guess\",style=bold];\n"); + break; + } + history.push_back(uniqueid); + } + + if (statistics_on) { + switch (type) { + case unit_clause_type: + learnt_unitary_clauses++; + case add_clause_type: + case gauss_propagation_type: + case simple_propagation_type: + no_propagations++; + times_var_propagated[lit.var()]++; + + depths_of_propagations_for_group[group].push_back(S->decisionLevel()); + times_group_caused_propagation[group]++; + depths_of_assigns_for_var[lit.var()].push_back(S->decisionLevel()); + break; + + case assumption_type: + case guess_type: + no_decisions++; + times_var_guessed[lit.var()]++; + + depths_of_assigns_for_var[lit.var()].push_back(S->decisionLevel()); + break; + } + } +} + +// Ending of a restart iteration +void Logger::end(const finish_type finish) +{ + assert(!(proof == NULL && proof_graph_on)); + + if (proof_graph_on) { + uniqueid++; + switch (finish) { + case model_found: + fprintf(proof,"node%d [shape=doublecircle, label=\"MODEL\"];\n",uniqueid); + break; + case unsat_model_found: + fprintf(proof,"node%d [shape=doublecircle, label=\"UNSAT\"];\n",uniqueid); + break; + case done_adding_clauses: + fprintf(proof,"node%d [shape=doublecircle, label=\"Done adding\\nclauses\"];\n",uniqueid); + break; + case restarting: + fprintf(proof,"node%d [shape=doublecircle, label=\"Re-starting\\nsearch\"];\n",uniqueid); + break; + } + + fprintf(proof,"node%d -> node%d;\n",history[history.size()-1],uniqueid); + fprintf(proof,"}\n"); + history.push_back(uniqueid); + + proof = (FILE*)fclose(proof); + assert(proof == NULL); + } + + if (statistics_on) { + printstats(); + if (finish == restarting) + reset_statistics(); + } +} + +void Logger::print_footer() const +{ + cout << "+" << std::setfill('-') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "-" << std::setfill(' ') << "+" << endl; +} + +void Logger::print_assign_var_order() const +{ + vector > prop_ordered; + for (uint i = 0; i < depths_of_assigns_for_var.size(); i++) { + double avg = 0.0; + bool was_unit = false; + for (vector::const_iterator it = depths_of_assigns_for_var[i].begin(); it != depths_of_assigns_for_var[i].end(); it++) { + avg += *it; + if (*it == 0) was_unit = true; + } + if (depths_of_assigns_for_var[i].size() > 0 && !was_unit) { + avg /= (double) depths_of_assigns_for_var[i].size(); + prop_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!prop_ordered.empty()) { + print_footer(); + print_simple_line(" Variables are assigned in the following order"); + print_simple_line(" (unitary clauses not shown)"); + print_header("var", "var name", "avg order"); + std::sort(prop_ordered.begin(), prop_ordered.end()); + print_vars(prop_ordered); + } +} + +void Logger::print_prop_order() const +{ + vector > prop_ordered; + for (uint i = 0; i < depths_of_propagations_for_group.size(); i++) { + double avg = 0.0; + bool was_unit = false; + for (vector::const_iterator it = depths_of_propagations_for_group[i].begin(); it != depths_of_propagations_for_group[i].end(); it++) { + avg += *it; + if (*it == 0) was_unit = true; + } + if (depths_of_propagations_for_group[i].size() > 0 && !was_unit) { + avg /= (double) depths_of_propagations_for_group[i].size(); + prop_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!prop_ordered.empty()) { + print_footer(); + print_simple_line(" Propagation depth order of clause groups"); + print_simple_line(" (unitary clauses not shown)"); + print_header("group", "group name", "avg order"); + std::sort(prop_ordered.begin(), prop_ordered.end()); + print_groups(prop_ordered); + } +} + +void Logger::print_confl_order() const +{ + vector > confl_ordered; + for (uint i = 0; i < depths_of_conflicts_for_group.size(); i++) { + double avg = 0.0; + for (vector::const_iterator it = depths_of_conflicts_for_group[i].begin(); it != depths_of_conflicts_for_group[i].end(); it++) + avg += *it; + if (depths_of_conflicts_for_group[i].size() > 0) { + avg /= (double) depths_of_conflicts_for_group[i].size(); + confl_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!confl_ordered.empty()) { + print_footer(); + print_simple_line(" Avg. conflict depth order of clause groups"); + print_header("groupno", "group name", "avg. depth"); + std::sort(confl_ordered.begin(), confl_ordered.end()); + print_groups(confl_ordered); + } +} + + +void Logger::print_times_var_guessed() const +{ + vector > times_var_ordered; + for (int i = 0; i < varnames.size(); i++) if (times_var_guessed[i] > 0) + times_var_ordered.push_back(std::make_pair(times_var_guessed[i], i)); + + if (!times_var_ordered.empty()) { + print_footer(); + print_simple_line(" No. times variable branched on"); + print_header("var", "var name", "no. times"); + std::sort(times_var_ordered.rbegin(), times_var_ordered.rend()); + print_vars(times_var_ordered); + } +} + +void Logger::print_times_group_caused_propagation() const +{ + vector > props_group_ordered; + for (uint i = 0; i < times_group_caused_propagation.size(); i++) + if (times_group_caused_propagation[i] > 0) + props_group_ordered.push_back(std::make_pair(times_group_caused_propagation[i], i)); + + if (!props_group_ordered.empty()) { + print_footer(); + print_simple_line(" No. propagations made by clause groups"); + print_header("group", "group name", "no. props"); + std::sort(props_group_ordered.rbegin(),props_group_ordered.rend()); + print_groups(props_group_ordered); + } +} + +void Logger::print_times_group_caused_conflict() const +{ + vector > confls_group_ordered; + for (uint i = 0; i < times_group_caused_conflict.size(); i++) + if (times_group_caused_conflict[i] > 0) + confls_group_ordered.push_back(std::make_pair(times_group_caused_conflict[i], i)); + + if (!confls_group_ordered.empty()) { + print_footer(); + print_simple_line(" No. conflicts made by clause groups"); + print_header("group", "group name", "no. confl"); + std::sort(confls_group_ordered.rbegin(), confls_group_ordered.rend()); + print_groups(confls_group_ordered); + } +} + +template +void Logger::print_line(const uint& number, const string& name, const T& value) const +{ + cout << "|" << std::setw(FST_WIDTH) << number << " " << std::setw(SND_WIDTH) << name << " " << std::setw(TRD_WIDTH) << value << "|" << endl; +} + +void Logger::print_header(const string& first, const string& second, const string& third) const +{ + cout << "|" << std::setw(FST_WIDTH) << first << " " << std::setw(SND_WIDTH) << second << " " << std::setw(TRD_WIDTH) << third << "|" << endl; + print_footer(); +} + +void Logger::print_groups(const vector >& to_print) const +{ + uint i = 0; + typedef vector >::const_iterator myiterator; + for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + print_line(it->second+1, groupnames[it->second], it->first); + } + print_footer(); +} + +void Logger::print_groups(const vector >& to_print) const +{ + uint i = 0; + typedef vector >::const_iterator myiterator; + for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + print_line(it->second+1, groupnames[it->second], it->first); + } + print_footer(); +} + +void Logger::print_vars(const vector >& to_print) const +{ + uint i = 0; + for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) + print_line(it->second+1, varnames[it->second], it->first); + + print_footer(); +} + +void Logger::print_vars(const vector >& to_print) const +{ + uint i = 0; + for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + print_line(it->second+1, varnames[it->second], it->first); + } + + print_footer(); +} + +template +void Logger::print_line(const string& str, const T& num) const +{ + cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+4) << str << std::setw(TRD_WIDTH) << num << "|" << endl; +} + +void Logger::print_simple_line(const string& str) const +{ + cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << str << "|" << endl; +} + +void Logger::print_center_line(const string& str) const +{ + uint middle = (FST_WIDTH+SND_WIDTH+TRD_WIDTH+4-str.size())/2; + int rest = FST_WIDTH+SND_WIDTH+TRD_WIDTH+4-middle*2-str.size(); + cout << "|" << std::setw(middle) << " " << str << std::setw(middle + rest) << " " << "|" << endl; +} + +void Logger::print_branch_depth_distrib() const +{ + //cout << "--- Branch depth stats ---" << endl; + + const uint range = 20; + map range_stat; + + for (map::const_iterator it = branch_depth_distrib.begin(); it != branch_depth_distrib.end(); it++) { + //cout << it->first << " : " << it->second << endl; + range_stat[it->first/range] += it->second; + } + //cout << endl; + + print_footer(); + print_simple_line(" No. search branches with branch depth between"); + print_line("Branch depth between", "no. br.-s"); + print_footer(); + + std::stringstream ss; + ss << "branch_depths/branch_depth_file" << runid << "-" << S->starts << ".txt"; + ofstream branch_depth_file; + branch_depth_file.open(ss.str().c_str()); + uint i = 0; + + for (map::iterator it = range_stat.begin(); it != range_stat.end(); it++) { + std::stringstream ss2; + ss2 << it->first*range << " - " << it->first*range + range-1; + print_line(ss2.str(), it->second); + + if (branch_depth_file.is_open()) { + branch_depth_file << i << "\t" << it->second << "\t"; + if (i % 5 == 0) + branch_depth_file << "\"" << it->first*range << "\""; + else + branch_depth_file << "\"\""; + branch_depth_file << endl; + } + i++; + } + if (branch_depth_file.is_open()) + branch_depth_file.close(); + print_footer(); + +} + +void Logger::print_learnt_clause_distrib() const +{ + map learnt_sizes; + const vec& learnts = S->get_learnts(); + + uint maximum = 0; + + for (uint i = 0; i < learnts.size(); i++) + { + uint size = learnts[i]->size(); + maximum = std::max(maximum, size); + + map::iterator it = learnt_sizes.find(size); + if (it == learnt_sizes.end()) + learnt_sizes[size] = 1; + else + it->second++; + } + + learnt_sizes[0] = S->get_unitary_learnts().size(); + + uint slice = (maximum+1)/max_print_lines + (bool)((maximum+1)%max_print_lines); + + print_footer(); + print_simple_line(" Learnt clause length distribution"); + print_line("Length between", "no. cl."); + print_footer(); + + uint until = slice; + uint from = 0; + while(until < maximum+1) { + std::stringstream ss2; + ss2 << from << " - " << until-1; + + uint sum = 0; + for (; from < until; from++) { + map::const_iterator it = learnt_sizes.find(from); + if (it != learnt_sizes.end()) + sum += it->second; + } + + print_line(ss2.str(), sum); + + until += slice; + } + + print_footer(); + + print_leearnt_clause_graph_distrib(maximum, learnt_sizes); +} + +void Logger::print_leearnt_clause_graph_distrib(const uint maximum, const map& learnt_sizes) const +{ + uint no_slices = FST_WIDTH + SND_WIDTH + TRD_WIDTH + 4-3; + uint slice = (maximum+1)/no_slices + (bool)((maximum+1)%no_slices); + uint until = slice; + uint from = 0; + vector slices; + uint hmax = 0; + while(until < maximum+1) { + uint sum = 0; + for (; from < until; from++) { + map::const_iterator it = learnt_sizes.find(from); + if (it != learnt_sizes.end()) + sum += it->second; + } + slices.push_back(sum); + until += slice; + 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()) + cout << yaxis[height-1-i-middle] << " "; + else + cout << " "; + for (uint i2 = 0; i2 < no_slices; i2++) { + if (slices[i2]/hslice >= i) cout << "+"; + else cout << " "; + } + cout << "|" << endl; + } + print_center_line(" Learnt clause size"); + print_footer(); +} + +void Logger::print_general_stats() const +{ + print_footer(); + print_simple_line(" Standard MiniSat stats -- for all restarts until now"); + print_footer(); + print_line("Restart number", S->starts); + print_line("Number of conflicts", S->conflicts); + print_line("Number of decisions", S->decisions); + print_line("Number of variables", S->order_heap.size()); + print_line("Number of clauses", S->nClauses()); + print_line("Number of literals in clauses",S->clauses_literals); + print_line("Avg. literals per learnt clause",(double)S->learnts_literals/(double)S->nLearnts()); + print_line("Progress estimate (%):", S->progress_estimate*100.0); + print_line("All unitary learnts until now", S->unitary_learnts.size()); + + print_footer(); +} + + +// Prints statistics on the console +void Logger::printstats() const +{ + assert(statistics_on); + assert(varnames.size() == times_var_guessed.size()); + assert(varnames.size() == times_var_propagated.size()); + + const uint fullwidth = FST_WIDTH+SND_WIDTH+TRD_WIDTH+4; + cout << endl; + cout << "+" << std::setfill('=') << std::setw(fullwidth) << "=" << "+" << endl; + std::stringstream tmp; + tmp << " STATS FOR RESTART NO. " << std::setw(3) << S->starts << " BEGIN "; + uint len = (fullwidth-2)/2-tmp.str().length()/2; + 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(4); + print_statistics_note(); + print_times_var_guessed(); + print_times_group_caused_propagation(); + print_times_group_caused_conflict(); + print_prop_order(); + print_confl_order(); + print_assign_var_order(); + print_branch_depth_distrib(); + print_learnt_clause_distrib(); + print_matrix_stats(); + print_advanced_stats(); + print_general_stats(); +} + +void Logger::print_matrix_stats() const +{ + print_footer(); + print_simple_line(" Matrix statistics"); + print_footer(); + + uint i = 0; + for (vector::const_iterator it = S->gauss_matrixes.begin(), end = S->gauss_matrixes.end(); it != end; it++, i++) { + std::stringstream s; + s << "Matrix " << i << " enabled"; + 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(); +} + +void Logger::print_advanced_stats() const +{ + print_footer(); + print_simple_line(" Advanced statistics - for only this restart"); + print_footer(); + print_line("Unitary learnts", learnt_unitary_clauses); + print_line("No. branches visited", no_conflicts); + 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(); +} + +void Logger::print_statistics_note() const +{ + print_footer(); + print_simple_line("Statistics note: If you used CryptoMiniSat as"); + print_simple_line("a library then vars are all shifted by 1 here"); + print_simple_line("and in every printed output of the solver."); + print_simple_line("This does not apply when you use CryptoMiniSat"); + print_simple_line("as a stand-alone program."); + print_footer(); +} + +// resets all stored statistics. Might be useful, to generate statistics for each restart and not for the whole search in general +void Logger::reset_statistics() +{ + assert(S->decisionLevel() == 0); + assert(times_var_guessed.size() == times_var_propagated.size()); + assert(times_group_caused_conflict.size() == times_group_caused_propagation.size()); + + typedef vector::iterator vecit; + for (vecit it = times_var_guessed.begin(); it != times_var_guessed.end(); it++) + *it = 0; + + for (vecit it = times_var_propagated.begin(); it != times_var_propagated.end(); it++) + *it = 0; + + for (vecit it = times_group_caused_conflict.begin(); it != times_group_caused_conflict.end(); it++) + *it = 0; + + for (vecit it = times_group_caused_propagation.begin(); it != times_group_caused_propagation.end(); it++) + *it = 0; + + for (vecit it = confls_by_group.begin(); it != confls_by_group.end(); it++) + *it = 0; + + for (vecit it = props_by_group.begin(); it != props_by_group.end(); it++) + *it = 0; + + typedef vector >::iterator vecvecit; + + for (vecvecit it = depths_of_propagations_for_group.begin(); it != depths_of_propagations_for_group.end(); it++) + it->clear(); + + for (vecvecit it = depths_of_conflicts_for_group.begin(); it != depths_of_conflicts_for_group.end(); it++) + it->clear(); + + for (vecvecit it = depths_of_assigns_for_var.begin(); it != depths_of_assigns_for_var.end(); it++) + it->clear(); + + sum_conflict_depths = 0; + no_conflicts = 0; + no_decisions = 0; + no_propagations = 0; + sum_decisions_on_branches = 0; + sum_propagations_on_branches = 0; + branch_depth_distrib.clear(); + learnt_unitary_clauses = 0; +} +}; diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h new file mode 100644 index 0000000..2917b98 --- /dev/null +++ b/src/sat/cryptominisat2/Logger.h @@ -0,0 +1,172 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef LOGGER_H +#define LOGGER_H + +#include +#include +#include +#include +#include +#include + +#include "Vec.h" +#include "Heap.h" +#include "Alg.h" +#include "SolverTypes.h" +#include "stdint.h" +#include "limits.h" +#include "Clause.h" + +#ifndef uint +#define uint unsigned int +#endif + +namespace MINISAT +{ + +using std::vector; +using std::pair; +using std::string; +using std::map; + +class Solver; + +class Logger +{ +public: + Logger(int& vebosity); + void setSolver(const Solver* S); + + //types of props, confl, and finish + enum prop_type { revert_guess_type, unit_clause_type, add_clause_type, assumption_type, guess_type, simple_propagation_type, gauss_propagation_type }; + enum confl_type { simple_confl_type, gauss_confl_type }; + enum finish_type { model_found, unsat_model_found, restarting, done_adding_clauses }; + + //Conflict and propagation(guess is also a proapgation...) + template + void conflict(const confl_type type, const uint goback_level, const uint group, const T& learnt_clause); + void propagation(const Lit lit, const prop_type type, const uint group = UINT_MAX); + void empty_clause(const uint group); + + //functions to add/name variables + void new_var(const Var var); + void set_variable_name(const uint var, string name); + + //function to name clause groups + void set_group_name(const uint group, string name); + + void begin(); + void end(const finish_type finish); + + void newclause(const vec& ps, const bool xor_clause, const uint group); + + bool proof_graph_on; + bool mini_proof; + bool statistics_on; + +private: + void new_group(const uint group); + void cut_name_to_size(string& name) const; + + void print_groups(const vector >& to_print) const; + void print_groups(const vector >& to_print) const; + void print_vars(const vector >& to_print) const; + void print_vars(const vector >& to_print) const; + void print_times_var_guessed() const; + void print_times_group_caused_propagation() const; + void print_times_group_caused_conflict() const; + void print_branch_depth_distrib() const; + void print_learnt_clause_distrib() const; + void print_leearnt_clause_graph_distrib(const uint maximum, const map& learnt_sizes) const; + void print_advanced_stats() const; + void print_statistics_note() const; + void print_matrix_stats() const; + void print_general_stats() const; + + uint max_print_lines; + template + void print_line(const uint& number, const string& name, const T& value) const; + void print_header(const string& first, const string& second, const string& third) const; + void print_footer() const; + template + 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; + void printstats() const; + void reset_statistics(); + + //internal data structures + uint uniqueid; //used to store the last unique ID given to a node + vector history; //stores the node uniqueIDs + + //graph drawing + FILE* proof; //The file to store the proof + uint runid; + + //--------------------- + //statistics collection + //--------------------- + + //group and var names + vector groupnames; + vector varnames; + + //confls and props grouped by clause groups + vector confls_by_group; + vector props_by_group; + + //props and guesses grouped by vars + vector times_var_guessed; + vector times_var_propagated; + + vector times_group_caused_conflict; + vector times_group_caused_propagation; + + vector > depths_of_propagations_for_group; + vector > depths_of_conflicts_for_group; + vector > depths_of_assigns_for_var; + + //the distribution of branch depths. first = depth, second = number of occurances + map branch_depth_distrib; + + uint sum_conflict_depths; + uint no_conflicts; + uint no_decisions; + uint no_propagations; + uint sum_decisions_on_branches; + uint sum_propagations_on_branches; + uint learnt_unitary_clauses; + + //message display properties + const int& verbosity; + + const Solver* S; + + void first_begin(); + bool begin_called; +}; + +}; +#endif //LOGGER_H diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile new file mode 100644 index 0000000..4a5f742 --- /dev/null +++ b/src/sat/cryptominisat2/Makefile @@ -0,0 +1,24 @@ +include ../../../scripts/Makefile.common + +MTL = ../cryptominisat/mtl +MTRAND = ../cryptominisat/MTRand +SOURCES = Clause.cpp Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp +OBJECTS = $(SOURCES:.cpp=.o) +LIB = libminisat.a +CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c +EXEC = minisat +LFLAGS = -lz + +all: $(LIB) #$(EXEC) +lib: $(LIB) + +$(LIB): $(OBJECTS) + rm -f $@ + ar cq $@ $(OBJECTS) + cp $(LIB) ../ + +clean: + rm -f $(OBJECTS) $(LIB) ../$(LIB) + +.cpp.o: + $(CC) $(CFLAGS) $< -o $@ diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp new file mode 100644 index 0000000..bc36445 --- /dev/null +++ b/src/sat/cryptominisat2/MatrixFinder.cpp @@ -0,0 +1,218 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#include "MatrixFinder.h" + +#include "Solver.h" +#include "Gaussian.h" +#include "GaussianConfig.h" + +#include +#include +#include +#include +namespace MINISAT +{ + +using std::set; +using std::map; + +//#define VERBOSE_DEBUG + +#ifdef VERBOSE_DEBUG +using std::cout; +using std::endl; +#endif + +//#define PART_FINDING + +MatrixFinder::MatrixFinder(Solver *_S) : + S(_S) + , unAssigned(_S->nVars() + 1) +{ + table.resize(S->nVars(), unAssigned); + matrix_no = 0; +} + +inline const Var MatrixFinder::fingerprint(const XorClause& c) const +{ + Var fingerprint = 0; + + for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) + fingerprint |= a->var(); + + return fingerprint; +} + +inline const bool MatrixFinder::firstPartOfSecond(const XorClause& c1, const XorClause& c2) const +{ + uint i1, i2; + for (i1 = 0, i2 = 0; i1 < c1.size() && i2 < c2.size();) { + if (c1[i1].var() != c2[i2].var()) + i2++; + else { + i1++; + i2++; + } + } + + return (i1 == c1.size()); +} + +const uint MatrixFinder::findMatrixes() +{ + if (S->xorclauses.size() == 0) + return 0; + + for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) { + set tomerge; + vector newSet; + for (Lit *l = &(**c)[0], *end2 = l + (**c).size(); l != end2; l++) { + if (table[l->var()] != unAssigned) + tomerge.insert(table[l->var()]); + else + newSet.push_back(l->var()); + } + if (tomerge.size() == 1) { + const uint into = *tomerge.begin(); + map >::iterator intoReverse = reverseTable.find(into); + for (uint i = 0; i < newSet.size(); i++) { + intoReverse->second.push_back(newSet[i]); + table[newSet[i]] = into; + } + continue; + } + + for (set::iterator it = tomerge.begin(); it != tomerge.end(); it++) { + newSet.insert(newSet.end(), reverseTable[*it].begin(), reverseTable[*it].end()); + reverseTable.erase(*it); + } + for (uint i = 0; i < newSet.size(); i++) + table[newSet[i]] = matrix_no; + reverseTable[matrix_no] = newSet; + matrix_no++; + } + + #ifdef VERBOSE_DEBUG + for (map >::iterator it = reverseTable.begin(), end = reverseTable.end(); it != end; it++) { + cout << "-- set begin --" << endl; + for (vector::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) { + cout << *it2 << ", "; + } + cout << "-------" << endl; + } + #endif + + return setMatrixes(); +} + +const uint MatrixFinder::setMatrixes() +{ + vector numXorInMatrix(matrix_no, 0); + vector sumXorSizeInMatrix(matrix_no, 0); + vector > xorSizesInMatrix(matrix_no); + vector > xorsInMatrix(matrix_no); + + #ifdef PART_FINDING + vector > xorFingerprintInMatrix(matrix_no); + #endif + + for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) { + XorClause& x = **c; + const uint matrix = table[x[0].var()]; + + //for stats + numXorInMatrix[matrix]++; + sumXorSizeInMatrix[matrix] += x.size(); + xorSizesInMatrix[matrix].push_back(x.size()); + xorsInMatrix[matrix].push_back(&x); + + #ifdef PART_FINDING + xorFingerprintInMatrix[matrix].push_back(fingerprint(x)); + #endif //PART_FINDING + } + + #ifdef PART_FINDING + for (uint i = 0; i < matrix_no; i++) + findParts(xorFingerprintInMatrix[i], xorsInMatrix[i]); + #endif //PART_FINDING + + uint realMatrixNum = 0; + vector remapMatrixes(matrix_no, UINT_MAX); + for (uint i = 0; i < matrix_no; i++) { + if (numXorInMatrix[i] < 3) + continue; + + const uint totalSize = reverseTable[i].size()*numXorInMatrix[i]; + const double density = (double)sumXorSizeInMatrix[i]/(double)totalSize*100.0; + double avg = (double)sumXorSizeInMatrix[i]/(double)numXorInMatrix[i]; + double variance = 0.0; + for (uint i2 = 0; i2 < xorSizesInMatrix[i].size(); i2++) + variance += pow((double)xorSizesInMatrix[i][i2]-avg, 2); + variance /= xorSizesInMatrix.size(); + const double stdDeviation = sqrt(variance); + + if (numXorInMatrix[i] >= 20 + && numXorInMatrix[i] <= 1000 + && realMatrixNum < (1 << 12)) + { + cout << "| Matrix no " << std::setw(4) << realMatrixNum; + remapMatrixes[i] = realMatrixNum; + realMatrixNum++; + } else { + cout << "| Unused Matrix "; + } + cout << std::setw(5) << numXorInMatrix[i] << " x" << std::setw(5) << reverseTable[i].size(); + cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%"; + cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg; + cout << " stdev:" << std::setw(6) << std::fixed << std::setprecision(2) << stdDeviation << " |" << endl; + } + + for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) { + XorClause& x = **c; + const uint toSet = remapMatrixes[table[x[0].var()]]; + if (toSet != UINT_MAX) + x.setMatrix(toSet); + else + x.setMatrix((1 << 12)-1); + } + + for (uint i = 0; i < realMatrixNum; i++) + S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, i)); + + return realMatrixNum; +} + +void MatrixFinder::findParts(vector& xorFingerprintInMatrix, vector& xorsInMatrix) +{ + uint ai = 0; + for (XorClause **a = &xorsInMatrix[0], **end = a + xorsInMatrix.size(); a != end; a++, ai++) { + const Var fingerprint = xorFingerprintInMatrix[ai]; + uint ai2 = 0; + for (XorClause **a2 = &xorsInMatrix[0]; a2 != end; a2++, ai2++) { + if (ai == ai2) continue; + const Var fingerprint2 = xorFingerprintInMatrix[ai2]; + if (((fingerprint & fingerprint2) == fingerprint) && firstPartOfSecond(**a, **a2)) { + cout << "First part of second:" << endl; + (*a)->plain_print(); + (*a2)->plain_print(); + cout << "END" << endl; + } + } + } +} +}; diff --git a/src/sat/cryptominisat2/MatrixFinder.h b/src/sat/cryptominisat2/MatrixFinder.h new file mode 100644 index 0000000..1d3e4bc --- /dev/null +++ b/src/sat/cryptominisat2/MatrixFinder.h @@ -0,0 +1,56 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef MATRIXFINDER_H +#define MATRIXFINDER_H + +#include +#include "Clause.h" +#include +#include + +namespace MINISAT +{ + +class Solver; + +using std::map; +using std::vector; + +class MatrixFinder { + + public: + MatrixFinder(Solver* S); + const uint findMatrixes(); + + private: + const uint setMatrixes(); + + void findParts(vector& xorFingerprintInMatrix, vector& xorsInMatrix); + inline const Var fingerprint(const XorClause& c) const; + inline const bool firstPartOfSecond(const XorClause& c1, const XorClause& c2) const; + + map > reverseTable; //matrix -> vars + vector table; //var -> matrix + uint matrix_no; + const uint unAssigned; + + Solver* S; +}; +}; + +#endif //MATRIXFINDER_H diff --git a/src/sat/cryptominisat2/PackedMatrix.h b/src/sat/cryptominisat2/PackedMatrix.h new file mode 100644 index 0000000..9f4178e --- /dev/null +++ b/src/sat/cryptominisat2/PackedMatrix.h @@ -0,0 +1,233 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef PACKEDMATRIX_H +#define PACKEDMATRIX_H + +#include "PackedRow.h" +#include + +//#define DEBUG_MATRIX + +#ifndef uint +#define uint unsigned int +#endif + +namespace MINISAT +{ + +class PackedMatrix +{ +public: + PackedMatrix() : + numRows(0) + , numCols(0) + , mp(NULL) + { + } + + PackedMatrix(const PackedMatrix& b) : + numRows(b.numRows) + , numCols(b.numCols) + { + mp = new uint64_t[numRows*(numCols+1)]; + std::copy(b.mp, b.mp+numRows*(numCols+1), mp); + } + + ~PackedMatrix() + { + delete[] mp; + } + + void resize(const uint num_rows, uint num_cols) + { + num_cols = num_cols / 64 + (bool)(num_cols % 64); + if (numRows*(numCols+1) < num_rows*(num_cols+1)) { + delete[] mp; + mp = new uint64_t[num_rows*(num_cols+1)]; + } + numRows = num_rows; + numCols = num_cols; + } + + void resizeNumRows(const uint num_rows) + { + numRows = num_rows; + } + + PackedMatrix& operator=(const PackedMatrix& b) + { + if (b.numRows*(b.numCols+1) > numRows*(numCols+1)) { + delete[] mp; + mp = new uint64_t[b.numRows*(b.numCols+1)]; + } + + numRows = b.numRows; + numCols = b.numCols; + std::copy(b.mp, b.mp+numRows*(numCols+1), mp); + + return *this; + } + + inline PackedRow operator[](const uint i) + { + #ifdef DEBUG_MATRIX + assert(i <= numRows); + #endif + + return PackedRow(numCols, *(mp+i*(numCols+1)), mp+i*(numCols+1)+1); + } + + inline const PackedRow operator[](const uint i) const + { + #ifdef DEBUG_MATRIX + assert(i <= numRows); + #endif + + return PackedRow(numCols, *(mp+i*(numCols+1)), mp+i*(numCols+1)+1); + } + + class iterator + { + public: + PackedRow operator*() + { + return PackedRow(numCols, *mp, mp+1); + } + + iterator& operator++() + { + mp += numCols+1; + return *this; + } + + iterator operator+(const uint num) const + { + iterator ret(*this); + ret.mp += (numCols+1)*num; + return ret; + } + + void operator+=(const uint num) + { + mp += (numCols+1)*num; + } + + const bool operator!=(const iterator& it) const + { + return mp != it.mp; + } + + const bool operator==(const iterator& it) const + { + return mp == it.mp; + } + + private: + friend class PackedMatrix; + + iterator(uint64_t* _mp, const uint _numCols) : + mp(_mp) + , numCols(_numCols) + {} + + uint64_t* mp; + const uint numCols; + }; + + inline iterator begin() + { + return iterator(mp, numCols); + } + + inline iterator end() + { + return iterator(mp+numRows*(numCols+1), numCols); + } + + /*class const_iterator + { + public: + const PackedRow operator*() + { + return PackedRow(numCols, *mp, mp+1); + } + + const_iterator& operator++() + { + mp += numCols+1; + return *this; + } + + const_iterator operator+(const uint num) const + { + const_iterator ret(*this); + ret.mp += (numCols+1)*num; + return ret; + } + + void operator+=(const uint num) + { + mp += (numCols+1)*num; + } + + const bool operator!=(const const_iterator& it) const + { + return mp != it.mp; + } + + const bool operator==(const const_iterator& it) const + { + return mp == it.mp; + } + + private: + friend class PackedMatrix; + + const_iterator(uint64_t* _mp, const uint _numCols) : + mp(_mp) + , numCols(_numCols) + {} + + const uint64_t* mp; + const uint numCols; + }; + inline const_iterator begin() const + { + return const_iterator(mp, numCols); + } + + inline const_iterator end() const + { + return const_iterator(mp+numRows*(numCols+1), numCols); + }*/ + + inline const uint size() const + { + return numRows; + } + +private: + + uint numRows; + uint numCols; + uint64_t* mp; +}; +}; + +#endif //PACKEDMATRIX_H + diff --git a/src/sat/cryptominisat2/PackedRow.cpp b/src/sat/cryptominisat2/PackedRow.cpp new file mode 100644 index 0000000..8bdd638 --- /dev/null +++ b/src/sat/cryptominisat2/PackedRow.cpp @@ -0,0 +1,161 @@ +#include "PackedRow.h" +namespace MINISAT +{ + +std::ostream& operator << (std::ostream& os, const PackedRow& m) +{ + for(uint i = 0; i < m.size*64; i++) { + os << m[i]; + } + os << " -- xor: " << m.get_xor_clause_inverted(); + return os; +} + +bool PackedRow::operator ==(const PackedRow& b) const +{ + #ifdef DEBUG_ROW + assert(size > 0); + assert(b.size > 0); + assert(size == b.size); + #endif + + return (std::equal(b.mp-1, b.mp+size, mp-1)); +} + +bool PackedRow::operator !=(const PackedRow& b) const +{ + #ifdef DEBUG_ROW + assert(size > 0); + assert(b.size > 0); + assert(size == b.size); + #endif + + return (std::equal(b.mp-1, b.mp+size, mp-1)); +} + +bool PackedRow::popcnt_is_one() const +{ + char popcount = 0; + for (uint i = 0; i < size; i++) if (mp[i]) { + uint64_t tmp = mp[i]; + for (uint i2 = 0; i2 < 64; i2++) { + popcount += tmp & 1; + if (popcount > 1) return false; + tmp >>= 1; + } + } + return popcount; +} + +bool PackedRow::popcnt_is_one(uint from) const +{ + from++; + for (uint i = from/64; i < size; i++) if (mp[i]) { + uint64_t tmp = mp[i]; + uint i2; + if (i == from/64) { + i2 = from%64; + tmp >>= i2; + } else + i2 = 0; + for (; i2 < 64; i2++) { + if (tmp & 1) return false; + tmp >>= 1; + } + } + return true; +} + +uint PackedRow::popcnt() const +{ + uint popcnt = 0; + for (uint i = 0; i < size; i++) if (mp[i]) { + uint64_t tmp = mp[i]; + for (uint i2 = 0; i2 < 64; i2++) { + popcnt += (tmp & 1); + tmp >>= 1; + } + } + return popcnt; +} + +uint PackedRow::popcnt(const uint from) const +{ + uint popcnt = 0; + for (uint i = from/64; i < size; i++) if (mp[i]) { + uint64_t tmp = mp[i]; + uint i2; + if (i == from/64) { + i2 = from%64; + tmp >>= i2; + } else + i2 = 0; + for (; i2 < 64; i2++) { + popcnt += (tmp & 1); + tmp >>= 1; + } + } + return popcnt; +} + +PackedRow& PackedRow::operator=(const PackedRow& b) +{ + #ifdef DEBUG_ROW + assert(size > 0); + assert(b.size > 0); + assert(size == b.size); + #endif + + memcpy(mp-1, b.mp-1, size+1); + return *this; +} + +PackedRow& PackedRow::operator^=(const PackedRow& b) +{ + #ifdef DEBUG_ROW + assert(size > 0); + assert(b.size > 0); + assert(b.size == size); + #endif + + for (uint i = 0; i < size; i++) { + mp[i] ^= b.mp[i]; + } + xor_clause_inverted ^= !b.xor_clause_inverted; + return *this; +} + +void PackedRow::fill(Lit* ps, const vec& assigns, const vector& col_to_var_original) const +{ + bool final = xor_clause_inverted; + + Lit* ps_first = ps; + uint col = 0; + bool wasundef = false; + for (uint i = 0; i < size; i++) for (uint i2 = 0; i2 < 64; i2++) { + if ((mp[i] >> i2) &1) { + const uint& var = col_to_var_original[col]; + assert(var != UINT_MAX); + + const lbool val = assigns[var]; + const bool val_bool = val.getBool(); + *ps = Lit(var, val_bool); + final ^= val_bool; + if (val.isUndef()) { + assert(!wasundef); + Lit tmp(*ps_first); + *ps_first = *ps; + *ps = tmp; + wasundef = true; + } + ps++; + } + col++; + } + if (wasundef) { + *ps_first ^= final; + //assert(ps != ps_first+1); + } else + assert(!final); +} +}; diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h new file mode 100644 index 0000000..2ea84fd --- /dev/null +++ b/src/sat/cryptominisat2/PackedRow.h @@ -0,0 +1,163 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef PACKEDROW_H +#define PACKEDROW_H + +//#define DEBUG_ROW + +#include +#include +#include "SolverTypes.h" +#include "Vec.h" +#include +#include +#include + +#ifndef uint +#define uint unsigned int +#endif + +namespace MINISAT +{ + +using std::vector; + + +class PackedMatrix; + +class PackedRow +{ +public: + bool operator ==(const PackedRow& b) const; + bool operator !=(const PackedRow& b) const; + PackedRow& operator=(const PackedRow& b); + uint popcnt() const; + uint popcnt(uint from) const; + bool popcnt_is_one() const; + bool popcnt_is_one(uint from) const; + + inline const uint64_t& get_xor_clause_inverted() const + { + return xor_clause_inverted; + } + + inline const bool isZero() const + { + const uint64_t* mp2 = (const uint64_t*)mp; + + for (uint i = 0; i < size; i++) { + if (mp2[i]) return false; + } + return true; + } + + inline void setZero() + { + memset(mp, 0, sizeof(uint64_t)*size); + } + + inline void clearBit(const uint i) + { + mp[i/64] &= ~((uint64_t)1 << (i%64)); + } + + inline void invert_xor_clause_inverted(const bool b = true) + { + xor_clause_inverted ^= b; + } + + inline void setBit(const uint i) + { + mp[i/64] |= ((uint64_t)1 << (i%64)); + } + + void swap(PackedRow b) + { + #ifdef DEBUG_ROW + assert(size > 0); + assert(b.size > 0); + assert(b.size == size); + #endif + + memcpy(tmp_row, b.mp-1, sizeof(uint64_t)*(size+1)); + memcpy(b.mp-1, mp-1, sizeof(uint64_t)*(size+1)); + memcpy(mp-1, tmp_row, sizeof(uint64_t)*(size+1)); + } + + PackedRow& operator^=(const PackedRow& b); + + inline const bool operator[](const uint& i) const + { + #ifdef DEBUG_ROW + assert(size*64 > i); + #endif + + return (mp[i/64] >> (i%64)) & 1; + } + + template + void set(const T& v, const vector& var_to_col, const uint matrix_size) + { + assert(size == (matrix_size/64) + ((bool)(matrix_size % 64))); + //mp = new uint64_t[size]; + setZero(); + for (uint i = 0; i < v.size(); i++) { + const uint toset_var = var_to_col[v[i].var()]; + assert(toset_var != UINT_MAX); + + setBit(toset_var); + } + + xor_clause_inverted = v.xor_clause_inverted(); + } + + void fill(Lit* ps, const vec& assigns, const vector& col_to_var_original) const; + + inline unsigned long int scan(const unsigned long int var) const + { + #ifdef DEBUG_ROW + assert(size > 0); + #endif + + for(uint i = var; i < size*64; i++) + if (this->operator[](i)) return i; + return ULONG_MAX; + } + + friend std::ostream& operator << (std::ostream& os, const PackedRow& m); + + static uint64_t *tmp_row; + +private: + friend class PackedMatrix; + PackedRow(const uint _size, uint64_t& _xor_clause_inverted, uint64_t* const _mp) : + size(_size) + , xor_clause_inverted(_xor_clause_inverted) + , mp(_mp) + {} + + const uint size; + uint64_t* const mp; + uint64_t& xor_clause_inverted; +}; + +std::ostream& operator << (std::ostream& os, const PackedRow& m); +}; + +#endif //PACKEDROW_H + diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp new file mode 100644 index 0000000..dc62f77 --- /dev/null +++ b/src/sat/cryptominisat2/Solver.cpp @@ -0,0 +1,1475 @@ +/****************************************************************************************[Solver.C] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include "Solver.h" +#include "Sort.h" +#include +#include +#include +#include +#include + +#include "Clause.h" +#include "time_mem.h" + +#include "VarReplacer.h" +#include "FindUndef.h" +#include "Gaussian.h" +#include "MatrixFinder.h" +#include "Conglomerate.h" +#include "XorFinder.h" + +namespace MINISAT +{ +using namespace MINISAT; + +//================================================================================================= +// Constructor/Destructor: + + +Solver::Solver() : + // Parameters: (formerly in 'SearchParams') + var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) + , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + + // More parameters: + // + , expensive_ccmin (true) + , polarity_mode (polarity_user) + , verbosity (0) + , restrictedPickBranch(0) + , useRealUnknowns(false) + , xorFinder (true) + + // Statistics: (formerly in 'SolverStats') + // + , starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) + , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) + + , ok (true) + , cla_inc (1) + , var_inc (1) + , qhead (0) + , simpDB_assigns (-1) + , simpDB_props (0) + , order_heap (VarOrderLt(activity)) + , progress_estimate(0) + , remove_satisfied (true) + , mtrand((unsigned long int)0) + , logger(verbosity) + , dynamic_behaviour_analysis(false) //do not document the proof as default + , maxRestarts(UINT_MAX) + , learnt_clause_group(0) + , greedyUnbound(false) +{ + toReplace = new VarReplacer(this); + conglomerate = new Conglomerate(this); + logger.setSolver(this); +} + + +Solver::~Solver() +{ + for (int i = 0; i < learnts.size(); i++) free(learnts[i]); + for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_learnts[i]); + for (int i = 0; i < clauses.size(); i++) free(clauses[i]); + for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]); + for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; + gauss_matrixes.clear(); + delete toReplace; + delete conglomerate; +} + +//================================================================================================= +// Minor methods: + + +// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be +// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). +Var Solver::newVar(bool sign, bool dvar) +{ + int v = nVars(); + watches .push(); // (list for positive literal) + watches .push(); // (list for negative literal) + xorwatches.push(); // (list for variables in xors) + reason .push(NULL); + assigns .push(l_Undef); + level .push(-1); + activity .push(0); + seen .push(0); + polarity .push_back((char)sign); + + decision_var.push_back(dvar); + toReplace->newVar(); + + insertVarOrder(v); + if (dynamic_behaviour_analysis) + logger.new_var(v); + + return v; +} + +bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint group, char* group_name) +{ + + assert(decisionLevel() == 0); + + if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); + + if (!ok) + return false; + + // Check if clause is satisfied and remove false/duplicate literals: + sort(ps); + Lit p; + int i, j; + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { + while (ps[i].var() >= nVars()) newVar(); + xor_clause_inverted ^= ps[i].sign(); + ps[i] ^= ps[i].sign(); + + if (ps[i] == p) { + //added, but easily removed + j--; + p = lit_Undef; + if (!assigns[ps[i].var()].isUndef()) + xor_clause_inverted ^= assigns[ps[i].var()].getBool(); + } else if (value(ps[i]) == l_Undef) //just add + ps[j++] = p = ps[i]; + else xor_clause_inverted ^= (value(ps[i]) == l_True); //modify xor_clause_inverted instead of adding + } + ps.shrink(i - j); + + switch(ps.size()) { + case 0: { + if (xor_clause_inverted) + return true; + + if (dynamic_behaviour_analysis) logger.empty_clause(group); + return ok = false; + } + case 1: { + assert(value(ps[0]) == l_Undef); + uncheckedEnqueue( (xor_clause_inverted) ? ~ps[0] : ps[0]); + if (dynamic_behaviour_analysis) + logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::add_clause_type, group); + return ok = (propagate() == NULL); + } + case 2: { + #ifdef VERBOSE_DEBUG + cout << "--> xor is 2-long, replacing var " << ps[0].var()+1 << " with " << (!xor_clause_inverted ? "-" : "") << ps[1].var()+1 << endl; + #endif + + learnt_clause_group = std::max(group+1, learnt_clause_group); + toReplace->replace(ps[0].var(), Lit(ps[1].var(), !xor_clause_inverted)); + break; + } + default: { + learnt_clause_group = std::max(group+1, learnt_clause_group); + XorClause* c = XorClause_new(ps, xor_clause_inverted, group); + + xorclauses.push(c); + attachClause(*c); + break; + } + } + + return true; +} + +bool Solver::addClause(vec& ps, const uint group, char* group_name) +{ + assert(decisionLevel() == 0); + + if (dynamic_behaviour_analysis) + logger.set_group_name(group, group_name); + + if (!ok) + return false; + + // Check if clause is satisfied and remove false/duplicate literals: + sort(ps); + Lit p; + int i, j; + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { + while (ps[i].var() >= nVars()) newVar(); + + if (value(ps[i]) == l_True || ps[i] == ~p) + return true; + else if (value(ps[i]) != l_False && ps[i] != p) + ps[j++] = p = ps[i]; + } + ps.shrink(i - j); + + if (ps.size() == 0) { + if (dynamic_behaviour_analysis) logger.empty_clause(group); + return ok = false; + } else if (ps.size() == 1) { + assert(value(ps[0]) == l_Undef); + uncheckedEnqueue(ps[0]); + if (dynamic_behaviour_analysis) + logger.propagation(ps[0], Logger::add_clause_type, group); + return ok = (propagate() == NULL); + } else { + learnt_clause_group = std::max(group+1, learnt_clause_group); + + Clause* c = Clause_new(ps, group); + + clauses.push(c); + attachClause(*c); + } + + return true; +} + +void Solver::attachClause(XorClause& c) +{ + assert(c.size() > 1); + + xorwatches[c[0].var()].push(&c); + xorwatches[c[1].var()].push(&c); + + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); +} + +void Solver::attachClause(Clause& c) +{ + assert(c.size() > 1); + + watches[(~c[0]).toInt()].push(&c); + watches[(~c[1]).toInt()].push(&c); + + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); +} + + +void Solver::detachClause(const XorClause& c) +{ + assert(c.size() > 1); + assert(find(xorwatches[c[0].var()], &c)); + assert(find(xorwatches[c[1].var()], &c)); + remove(xorwatches[c[0].var()], &c); + remove(xorwatches[c[1].var()], &c); + + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); +} + +void Solver::detachClause(const Clause& c) +{ + assert(c.size() > 1); + assert(find(watches[(~c[0]).toInt()], &c)); + assert(find(watches[(~c[1]).toInt()], &c)); + remove(watches[(~c[0]).toInt()], &c); + remove(watches[(~c[1]).toInt()], &c); + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); +} + +void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint origSize, const Clause* address) +{ + assert(origSize > 1); + assert(find(watches[(~lit1).toInt()], address)); + assert(find(watches[(~lit2).toInt()], address)); + remove(watches[(~lit1).toInt()], address); + remove(watches[(~lit2).toInt()], address); + if (address->learnt()) learnts_literals -= origSize; + else clauses_literals -= origSize; +} + + +bool Solver::satisfied(const Clause& c) const +{ + for (uint i = 0; i < c.size(); i++) + if (value(c[i]) == l_True) + return true; + return false; +} + +bool Solver::satisfied(const XorClause& c) const +{ + bool final = c.xor_clause_inverted(); + for (uint k = 0; k < c.size(); k++ ) { + const lbool& val = assigns[c[k].var()]; + if (val.isUndef()) return false; + final ^= val.getBool(); + } + return final; +} + + +// Revert to the state at given level (keeping all assignment at 'level' but not beyond). +// +void Solver::cancelUntil(int level) +{ + #ifdef VERBOSE_DEBUG + cout << "Canceling until level " << level; + if (level > 0) cout << " sublevel: " << trail_lim[level]; + cout << endl; + #endif + + if (decisionLevel() > level) { + for (int c = trail.size()-1; c >= trail_lim[level]; c--) { + Var x = trail[c].var(); + #ifdef VERBOSE_DEBUG + cout << "Canceling var " << x+1 << " sublevel:" << c << endl; + #endif + for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++) + (*gauss)->canceling(c, x); + assigns[x] = l_Undef; + insertVarOrder(x); + } + qhead = trail_lim[level]; + trail.shrink(trail.size() - trail_lim[level]); + trail_lim.shrink(trail_lim.size() - level); + for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++) + (*gauss)->back_to_level(decisionLevel()); + } + + #ifdef VERBOSE_DEBUG + cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel:" << trail.size()-1 << ")" << endl; + #endif +} + +//Permutates the clauses in the solver. Very useful to calcuate the average time it takes the solver to solve the prolbem +void Solver::permutateClauses() +{ + for (int i = 0; i < clauses.size(); i++) { + int j = mtrand.randInt(i); + Clause* tmp = clauses[i]; + clauses[i] = clauses[j]; + clauses[j] = tmp; + } + + for (int i = 0; i < xorclauses.size(); i++) { + int j = mtrand.randInt(i); + XorClause* tmp = xorclauses[i]; + xorclauses[i] = xorclauses[j]; + xorclauses[j] = tmp; + } +} + +void Solver::setRealUnknown(const uint var) +{ + if (realUnknowns.size() < var+1) + realUnknowns.resize(var+1, false); + realUnknowns[var] = true; +} + +void Solver::printLit(const Lit l) const +{ + printf("%s%d:%c", l.sign() ? "-" : "", l.var()+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X')); +} + + +void Solver::printClause(const Clause& c) const +{ + printf("(group: %d) ", c.group); + for (uint i = 0; i < c.size();) { + printLit(c[i]); + i++; + if (i < c.size()) printf(" "); + } +} + +void Solver::printClause(const XorClause& c) const +{ + printf("(group: %d) ", c.group); + if (c.xor_clause_inverted()) printf(" /inverted/ "); + for (uint i = 0; i < c.size();) { + printLit(c[i].unsign()); + i++; + if (i < c.size()) printf(" + "); + } +} + +void Solver::set_gaussian_decision_until(const uint to) +{ + gaussconfig.decision_until = to; +} + +void Solver::set_gaussian_decision_from(const uint from) +{ + gaussconfig.decision_from = from; +} + +//================================================================================================= +// Major methods: + + +Lit Solver::pickBranchLit(int polarity_mode) +{ + #ifdef VERBOSE_DEBUG + cout << "decision level:" << decisionLevel() << " "; + #endif + + Var next = var_Undef; + + // Random decision: + if (mtrand.randDblExc() < random_var_freq && !order_heap.empty()) { + if (restrictedPickBranch == 0) next = order_heap[mtrand.randInt(order_heap.size()-1)]; + else next = order_heap[mtrand.randInt(std::min((uint32_t)order_heap.size()-1, restrictedPickBranch))]; + + if (assigns[next] == l_Undef && decision_var[next]) + rnd_decisions++; + } + + // Activity based decision: + //bool dont_do_bad_decision = false; + //if (restrictedPickBranch != 0) dont_do_bad_decision = (mtrand.randInt(100) != 0); + while (next == var_Undef || assigns[next] != l_Undef || !decision_var[next]) + if (order_heap.empty()) { + next = var_Undef; + break; + } else { + next = order_heap.removeMin(); + } + + bool sign = false; + switch (polarity_mode) { + case polarity_true: + sign = false; + break; + case polarity_false: + sign = true; + break; + case polarity_user: + if (next != var_Undef) + sign = polarity[next]; + break; + case polarity_rnd: + sign = mtrand.randInt(1); + break; + default: + assert(false); + } + + assert(next == var_Undef || value(next) == l_Undef); + + if (next == var_Undef) { + #ifdef VERBOSE_DEBUG + cout << "SAT!" << endl; + #endif + return lit_Undef; + } else { + Lit lit(next,sign); + #ifdef VERBOSE_DEBUG + cout << "decided on: " << lit.var()+1 << " to set:" << !lit.sign() << endl; + #endif + return lit; + } +} + + +/*_________________________________________________________________________________________________ +| +| analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] +| +| Description: +| Analyze conflict and produce a reason clause. +| +| Pre-conditions: +| * 'out_learnt' is assumed to be cleared. +| * Current decision level must be greater than root level. +| +| Post-conditions: +| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +| +| Effect: +| Will undo part of the trail, upto but not beyond the assumption of the current decision level. +|________________________________________________________________________________________________@*/ +void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) +{ + int pathC = 0; + Lit p = lit_Undef; + + // Generate conflict clause: + // + out_learnt.push(); // (leave room for the asserting literal) + int index = trail.size() - 1; + out_btlevel = 0; + + do { + assert(confl != NULL); // (otherwise should be UIP) + Clause& c = *confl; + + if (c.learnt()) + claBumpActivity(c); + + for (uint j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) { + const Lit& q = c[j]; + const uint my_var = q.var(); + + if (!seen[my_var] && level[my_var] > 0) { + if (!useRealUnknowns || (my_var < realUnknowns.size() && realUnknowns[my_var])) + varBumpActivity(my_var); + seen[my_var] = 1; + if (level[my_var] >= decisionLevel()) + pathC++; + else { + out_learnt.push(q); + if (level[my_var] > out_btlevel) + out_btlevel = level[my_var]; + } + } + } + + // Select next clause to look at: + while (!seen[trail[index--].var()]); + p = trail[index+1]; + confl = reason[p.var()]; + seen[p.var()] = 0; + pathC--; + + } while (pathC > 0); + out_learnt[0] = ~p; + + // Simplify conflict clause: + // + int i, j; + if (expensive_ccmin) { + uint32_t abstract_level = 0; + for (i = 1; i < out_learnt.size(); i++) + abstract_level |= abstractLevel(out_learnt[i].var()); // (maintain an abstraction of levels involved in conflict) + + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++) + if (reason[out_learnt[i].var()] == NULL || !litRedundant(out_learnt[i], abstract_level)) + out_learnt[j++] = out_learnt[i]; + } else { + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++) { + const Clause& c = *reason[out_learnt[i].var()]; + for (uint k = 1; k < c.size(); k++) + if (!seen[c[k].var()] && level[c[k].var()] > 0) { + out_learnt[j++] = out_learnt[i]; + break; + } + } + } + max_literals += out_learnt.size(); + out_learnt.shrink(i - j); + tot_literals += out_learnt.size(); + + // Find correct backtrack level: + // + if (out_learnt.size() == 1) + out_btlevel = 0; + else { + int max_i = 1; + for (int i = 2; i < out_learnt.size(); i++) + if (level[out_learnt[i].var()] > level[out_learnt[max_i].var()]) + max_i = i; + Lit p = out_learnt[max_i]; + out_learnt[max_i] = out_learnt[1]; + out_learnt[1] = p; + out_btlevel = level[p.var()]; + } + + + for (int j = 0; j < analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared) +} + + +// Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is +// visiting literals at levels that cannot be removed later. +bool Solver::litRedundant(Lit p, uint32_t abstract_levels) +{ + analyze_stack.clear(); + analyze_stack.push(p); + int top = analyze_toclear.size(); + while (analyze_stack.size() > 0) { + assert(reason[analyze_stack.last().var()] != NULL); + const Clause& c = *reason[analyze_stack.last().var()]; + analyze_stack.pop(); + + for (uint i = 1; i < c.size(); i++) { + Lit p = c[i]; + if (!seen[p.var()] && level[p.var()] > 0) { + if (reason[p.var()] != NULL && (abstractLevel(p.var()) & abstract_levels) != 0) { + seen[p.var()] = 1; + analyze_stack.push(p); + analyze_toclear.push(p); + } else { + for (int j = top; j < analyze_toclear.size(); j++) + seen[analyze_toclear[j].var()] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; + } + } + } + } + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +void Solver::analyzeFinal(Lit p, vec& out_conflict) +{ + out_conflict.clear(); + out_conflict.push(p); + + if (decisionLevel() == 0) + return; + + seen[p.var()] = 1; + + for (int i = trail.size()-1; i >= trail_lim[0]; i--) { + Var x = trail[i].var(); + if (seen[x]) { + if (reason[x] == NULL) { + assert(level[x] > 0); + out_conflict.push(~trail[i]); + } else { + const Clause& c = *reason[x]; + for (uint j = 1; j < c.size(); j++) + if (level[c[j].var()] > 0) + seen[c[j].var()] = 1; + } + seen[x] = 0; + } + } + + seen[p.var()] = 0; +} + + +void Solver::uncheckedEnqueue(Lit p, Clause* from) +{ + #ifdef VERBOSE_DEBUG + cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel:" << trail.size() << endl; + #endif + + assert(value(p) == l_Undef); + const Var v = p.var(); + assigns [v] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient + level [v] = decisionLevel(); + reason [v] = from; + polarity[p.var()] = p.sign(); + trail.push(p); +} + + +/*_________________________________________________________________________________________________ +| +| 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. +|________________________________________________________________________________________________@*/ +Clause* Solver::propagate(const bool xor_as_well) +{ + Clause* confl = NULL; + int num_props = 0; + + #ifdef VERBOSE_DEBUG + cout << "Propagation started" << endl; + #endif + + while (qhead < trail.size()) { + Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. + vec& ws = watches[p.toInt()]; + Clause **i, **j, **end; + num_props++; + + #ifdef VERBOSE_DEBUG + cout << "Propagating lit " << (p.sign() ? '-' : ' ') << p.var()+1 << endl; + #endif + + for (i = j = ws.getData(), end = i + ws.size(); i != end;) { + Clause& c = **i++; + + // Make sure the false literal is data[1]: + const Lit false_lit(~p); + if (c[0] == false_lit) + c[0] = c[1], c[1] = false_lit; + + assert(c[1] == false_lit); + + // If 0th watch is true, then clause is already satisfied. + const Lit& first = c[0]; + if (value(first) == l_True) { + *j++ = &c; + } else { + // Look for new watch: + for (uint k = 2; k < c.size(); k++) + if (value(c[k]) != l_False) { + c[1] = c[k]; + c[k] = false_lit; + watches[(~c[1]).toInt()].push(&c); + goto FoundWatch; + } + + // Did not find watch -- clause is unit under assignment: + *j++ = &c; + if (value(first) == l_False) { + confl = &c; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } else { + uncheckedEnqueue(first, &c); + if (dynamic_behaviour_analysis) + logger.propagation(first,Logger::simple_propagation_type,c.group); + } + } +FoundWatch: + ; + } + ws.shrink(i - j); + + if (xor_as_well && !confl) confl = propagate_xors(p); + } + propagations += num_props; + simpDB_props -= num_props; + + #ifdef VERBOSE_DEBUG + cout << "Propagation ended." << endl; + #endif + + return confl; +} + +Clause* Solver::propagate_xors(const Lit& p) +{ + #ifdef VERBOSE_DEBUG_XOR + cout << "Xor-Propagating variable " << p.var()+1 << endl; + #endif + + Clause* confl = NULL; + + vec& ws = xorwatches[p.var()]; + XorClause **i, **j, **end; + for (i = j = ws.getData(), end = i + ws.size(); i != end;) { + XorClause& c = **i++; + + // Make sure the false literal is data[1]: + if (c[0].var() == p.var()) { + Lit tmp(c[0]); + c[0] = c[1]; + c[1] = tmp; + } + assert(c[1].var() == p.var()); + + #ifdef VERBOSE_DEBUG_XOR + cout << "--> xor thing -- " << endl; + printClause(c); + cout << endl; + #endif + bool final = c.xor_clause_inverted(); + for (int k = 0, size = c.size(); k < size; k++ ) { + const lbool& val = assigns[c[k].var()]; + if (val.isUndef() && k >= 2) { + Lit tmp(c[1]); + c[1] = c[k]; + c[k] = tmp; + #ifdef VERBOSE_DEBUG_XOR + cout << "new watch set" << endl << endl; + #endif + xorwatches[c[1].var()].push(&c); + goto FoundWatch; + } + + c[k] = c[k].unsign() ^ val.getBool(); + final ^= val.getBool(); + } + + + { + // Did not find watch -- clause is unit under assignment: + *j++ = &c; + + #ifdef VERBOSE_DEBUG_XOR + cout << "final: " << std::boolalpha << final << " - "; + #endif + if (assigns[c[0].var()].isUndef()) { + c[0] = c[0].unsign()^final; + + #ifdef VERBOSE_DEBUG_XOR + cout << "propagating "; + printLit(c[0]); + cout << endl; + cout << "propagation clause -- "; + printClause(*(Clause*)&c); + cout << endl << endl; + #endif + + uncheckedEnqueue(c[0], (Clause*)&c); + if (dynamic_behaviour_analysis) + logger.propagation(c[0], Logger::simple_propagation_type, c.group); + } else if (!final) { + + #ifdef VERBOSE_DEBUG_XOR + printf("conflict clause -- "); + printClause(*(Clause*)&c); + cout << endl << endl; + #endif + + confl = (Clause*)&c; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } else { + #ifdef VERBOSE_DEBUG_XOR + printf("xor satisfied\n"); + #endif + + Lit tmp(c[0]); + c[0] = c[1]; + c[1] = tmp; + } + } +FoundWatch: + ; + } + ws.shrink(i - j); + + return confl; +} + + +/*_________________________________________________________________________________________________ +| +| reduceDB : () -> [void] +| +| Description: +| 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. +|________________________________________________________________________________________________@*/ +struct reduceDB_lt { + bool operator () (Clause* x, Clause* y) { + return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); + } +}; +void Solver::reduceDB() +{ + int i, j; + double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + + sort(learnts, reduceDB_lt()); + for (i = j = 0; i < learnts.size() / 2; i++) { + if (learnts[i]->size() > 2 && !locked(*learnts[i])) + removeClause(*learnts[i]); + else + learnts[j++] = learnts[i]; + } + for (; i < learnts.size(); i++) { + if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim) + removeClause(*learnts[i]); + else + learnts[j++] = learnts[i]; + } + learnts.shrink(i - j); +} + +const vec& Solver::get_learnts() const +{ + return learnts; +} + +const vec& Solver::get_sorted_learnts() +{ + sort(learnts, reduceDB_lt()); + return learnts; +} + +const vec& Solver::get_unitary_learnts() const +{ + return unitary_learnts; +} + +void Solver::dump_sorted_learnts(const char* file) +{ + FILE* outfile = fopen(file, "w"); + if (!outfile) { + printf("Error: Cannot open file '%s' to write learnt clauses!\n", file); + exit(-1); + } + + for (uint i = 0; i < unitary_learnts.size(); i++) + unitary_learnts[i]->plain_print(outfile); + + sort(learnts, reduceDB_lt()); + for (int i = learnts.size()-1; i >= 0 ; i--) { + learnts[i]->plain_print(outfile); + } + fclose(outfile); +} + +void Solver::setMaxRestarts(const uint num) +{ + maxRestarts = num; +} + +bool Solver::cleanClause(Clause& c) const +{ + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + if (value(*i) == l_Undef) { + *j = *i; + j++; + } else assert(at > 1); + assert(value(*i) != l_True); + } + c.shrink(i-j); + return (i-j > 0); +} + +void Solver::cleanClauses(vec& cs) +{ + uint useful = 0; + for (int s = 0; s < cs.size(); s++) + useful += cleanClause(*cs[s]); + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(Clause) useful:" << useful << endl; + #endif +} + +void Solver::cleanClauses(vec& cs) +{ + uint useful = 0; + for (int s = 0; s < cs.size(); s++) { + XorClause& c = *cs[s]; + #ifdef VERBOSE_DEBUG + std::cout << "Cleaning clause:"; + c.plain_print(); + printClause(c);std::cout << std::endl; + #endif + + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + const lbool& val = assigns[i->var()]; + if (val.isUndef()) { + *j = *i; + j++; + } else /*assert(at>1),*/ c.invert(val.getBool()); + } + c.shrink(i-j); + if (i-j > 0) useful++; + + #ifdef VERBOSE_DEBUG + std::cout << "Cleaned clause:"; + c.plain_print(); + printClause(c);std::cout << std::endl; + #endif + assert(c.size() > 1); + } + + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(XorClause) useful:" << useful << endl; + #endif +} + +/*_________________________________________________________________________________________________ +| +| simplify : [void] -> [bool] +| +| Description: +| Simplify the clause database according to the current top-level assigment. Currently, the only +| thing done here is the removal of satisfied clauses, but more things can be put here. +|________________________________________________________________________________________________@*/ +lbool Solver::simplify() +{ + assert(decisionLevel() == 0); + + if (!ok || propagate() != NULL) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + } + ok = false; + return l_False; + } + + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) { + return l_Undef; + } + + // Remove satisfied clauses: + removeSatisfied(learnts); + if (remove_satisfied) { // Can be turned off. + removeSatisfied(clauses); + removeSatisfied(xorclauses); + } + + // Remove fixed variables from the variable heap: + order_heap.filter(VarFilter(*this)); + + simpDB_assigns = nAssigns(); + simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) + + //cleanClauses(clauses); + //cleanClauses(xorclauses); + //cleanClauses(learnts); + + return l_Undef; +} + + +/*_________________________________________________________________________________________________ +| +| search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] +| +| Description: +| Search for a model the specified number of conflicts, keeping the number of learnt clauses +| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to +| indicate infinity. +| +| Output: +| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If +| all variables are decision variables, this means that the clause set is satisfiable. 'l_False' +| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. +|________________________________________________________________________________________________@*/ +lbool Solver::search(int nof_conflicts, int nof_learnts) +{ + assert(ok); + int conflictC = 0; + vec learnt_clause; + llbool ret; + + starts++; + for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++) { + ret = (*gauss)->full_init(); + if (ret != l_Nothing) return ret; + } + + if (dynamic_behaviour_analysis) logger.begin(); + + for (;;) { + Clause* confl = propagate(); + + if (confl != NULL) { + ret = handle_conflict(learnt_clause, confl, conflictC); + if (ret != l_Nothing) return ret; + } else { + bool at_least_one_continue = false; + for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++) { + ret = (*gauss)->find_truths(learnt_clause, conflictC); + if (ret == l_Continue) at_least_one_continue = true; + else if (ret != l_Nothing) return ret; + } + if (at_least_one_continue) continue; + ret = new_decision(nof_conflicts, nof_learnts, conflictC); + if (ret != l_Nothing) return ret; + } + } +} + +llbool Solver::new_decision(int& nof_conflicts, int& nof_learnts, int& conflictC) +{ + if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + if (dynamic_behaviour_analysis) { + logger.end(Logger::restarting); + } + return l_Undef; + } + + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && simplify() == l_False) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + } + return l_False; + } + + if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) + // Reduce the set of learnt clauses: + reduceDB(); + + Lit next = lit_Undef; + while (decisionLevel() < assumptions.size()) { + // Perform user provided assumption: + Lit p = assumptions[decisionLevel()]; + if (value(p) == l_True) { + // Dummy decision level: + newDecisionLevel(); + if (dynamic_behaviour_analysis) logger.propagation(p, Logger::assumption_type); + } else if (value(p) == l_False) { + analyzeFinal(~p, conflict); + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + } + return l_False; + } else { + next = p; + break; + } + } + + if (next == lit_Undef) { + // New variable decision: + decisions++; + next = pickBranchLit(polarity_mode); + + if (next == lit_Undef) { + // Model found: + if (dynamic_behaviour_analysis) { + logger.end(Logger::model_found); + } + return l_True; + } + } + + // Increase decision level and enqueue 'next' + assert(value(next) == l_Undef); + newDecisionLevel(); + uncheckedEnqueue(next); + if (dynamic_behaviour_analysis) logger.propagation(next, Logger::guess_type); + + return l_Nothing; +} + +llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conflictC) +{ + #ifdef VERBOSE_DEBUG + cout << "Handling conflict: "; + for (uint i = 0; i < learnt_clause.size(); i++) + cout << learnt_clause[i].var()+1 << ","; + cout << endl; + #endif + + int backtrack_level; + + conflicts++; + conflictC++; + if (decisionLevel() == 0) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + } + return l_False; + } + learnt_clause.clear(); + analyze(confl, learnt_clause, backtrack_level); + if (dynamic_behaviour_analysis) + logger.conflict(Logger::simple_confl_type, backtrack_level, confl->group, learnt_clause); + cancelUntil(backtrack_level); + + #ifdef VERBOSE_DEBUG + cout << "Learning:"; + for (uint i = 0; i < learnt_clause.size(); i++) printLit(learnt_clause[i]), cout << " "; + cout << endl; + cout << "reverting var " << learnt_clause[0].var()+1 << " to " << !learnt_clause[0].sign() << endl; + #endif + + assert(value(learnt_clause[0]) == l_Undef); + //Unitary learnt + if (learnt_clause.size() == 1) { + Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true); + unitary_learnts.push(c); + uncheckedEnqueue(learnt_clause[0]); + if (dynamic_behaviour_analysis) { + logger.set_group_name(c->group, "unitary learnt clause"); + logger.propagation(learnt_clause[0], Logger::unit_clause_type, c->group); + } + assert(backtrack_level == 0 && "Unit clause learnt, so must cancel until level 0, right?"); + + #ifdef VERBOSE_DEBUG + cout << "Unit clause learnt." << endl; + #endif + //Normal learnt + } else { + Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true); + learnts.push(c); + attachClause(*c); + claBumpActivity(*c); + uncheckedEnqueue(learnt_clause[0], c); + + if (dynamic_behaviour_analysis) { + logger.set_group_name(c->group, "learnt clause"); + logger.propagation(learnt_clause[0], Logger::simple_propagation_type, c->group); + } + } + + varDecayActivity(); + claDecayActivity(); + + return l_Nothing; +} + +double Solver::progressEstimate() const +{ + double progress = 0; + double F = 1.0 / nVars(); + + for (int i = 0; i <= decisionLevel(); i++) { + int beg = i == 0 ? 0 : trail_lim[i - 1]; + int end = i == decisionLevel() ? trail.size() : trail_lim[i]; + progress += pow(F, i) * (end - beg); + } + + return progress / nVars(); +} + +void Solver::print_gauss_sum_stats() const +{ + if (gauss_matrixes.size() == 0) { + printf(" no matrixes found |\n"); + return; + } + + uint called = 0; + uint useful_prop = 0; + uint useful_confl = 0; + uint disabled = 0; + for (Gaussian *const*gauss = &gauss_matrixes[0], *const*end= gauss + gauss_matrixes.size(); gauss != end; gauss++) { + disabled += (*gauss)->get_disabled(); + called += (*gauss)->get_called(); + useful_prop += (*gauss)->get_useful_prop(); + useful_confl += (*gauss)->get_useful_confl(); + //gauss->print_stats(); + //gauss->print_matrix_stats(); + } + + if (called == 0) { + printf(" disabled |\n"); + } else { + printf(" %3.0lf%% |", (double)useful_prop/(double)called*100.0); + printf(" %3.0lf%% |", (double)useful_confl/(double)called*100.0); + printf(" %3.0lf%% |\n", 100.0-(double)disabled/(double)gauss_matrixes.size()*100.0); + } +} + +lbool Solver::solve(const vec& assumps) +{ + if (dynamic_behaviour_analysis) + logger.end(Logger::done_adding_clauses); + + model.clear(); + conflict.clear(); + + if (!ok) return l_False; + + assumps.copyTo(assumptions); + + double nof_conflicts = restart_first; + double nof_learnts = nClauses() * learntsize_factor; + lbool status = l_Undef; + + toReplace->performReplace(); + if (!ok) return l_False; + + if (xorFinder) { + double time; + if (clauses.size() < 400000) { + time = cpuTime(); + removeSatisfied(clauses); + cleanClauses(clauses); + uint sumLengths = 0; + XorFinder xorFinder(this, clauses, xorclauses); + uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10); + + printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); + if (!ok) return l_False; + } + + if (xorclauses.size() > 1) { + uint orig_total = 0; + uint orig_num_cls = xorclauses.size(); + for (uint i = 0; i < xorclauses.size(); i++) { + orig_total += xorclauses[i]->size(); + } + + time = cpuTime(); + removeSatisfied(xorclauses); + cleanClauses(xorclauses); + uint foundCong = conglomerate->conglomerateXors(); + printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong); + if (!ok) return l_False; + + uint new_total = 0; + uint new_num_cls = xorclauses.size(); + for (uint i = 0; i < xorclauses.size(); i++) { + new_total += xorclauses[i]->size(); + } + printf("| Sum xclauses before: %8d, after: %12d |\n", orig_num_cls, new_num_cls); + printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total); + } + } + + if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) { + removeSatisfied(xorclauses); + cleanClauses(xorclauses); + double time = cpuTime(); + MatrixFinder m(this); + const uint numMatrixes = m.findMatrixes(); + printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes); + } + + + if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { + printf("============================[ Search Statistics ]========================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | GAUSS |\n"); + printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | Prop Confl On |\n"); + printf("=========================================================================================\n"); + } + + // Search: + while (status == l_Undef && starts < maxRestarts) { + removeSatisfied(clauses); + removeSatisfied(xorclauses); + removeSatisfied(learnts); + + cleanClauses(clauses); + cleanClauses(xorclauses); + cleanClauses(learnts); + + if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts()); + print_gauss_sum_stats(); + } + for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++) + (*gauss)->reset_stats(); + + status = search((int)nof_conflicts, (int)nof_learnts); + nof_conflicts *= restart_inc; + nof_learnts *= learntsize_inc; + + for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++) + (*gauss)->clear_clauses(); + } + + if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { + printf("===================================================================="); + print_gauss_sum_stats(); + } + + if (status == l_True) { + conglomerate->doCalcAtFinish(); + toReplace->extendModel(); + // Extend & copy model: + model.growTo(nVars()); + for (int i = 0; i < nVars(); i++) model[i] = value(i); +#ifndef NDEBUG + verifyModel(); +#endif + if (greedyUnbound) { + double time = cpuTime(); + FindUndef finder(*this); + const uint unbounded = finder.unRoll(); + printf("Greedy unbounding :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded); + } + } if (status == l_False) { + if (conflict.size() == 0) + ok = false; + } + + cancelUntil(0); + return status; +} + +//================================================================================================= +// Debug methods: + +bool Solver::verifyXorClauses(const vec& cs) const +{ + #ifdef VERBOSE_DEBUG + cout << "Checking xor-clauses whether they have been properly satisfied." << endl;; + #endif + + bool failed = false; + + for (int i = 0; i < xorclauses.size(); i++) { + XorClause& c = *xorclauses[i]; + bool final = c.xor_clause_inverted(); + + #ifdef VERBOSE_DEBUG + std::sort(&c[0], &c[0] + c.size()); + c.plain_print(); + #endif + + for (uint j = 0; j < c.size(); j++) { + assert(modelValue(c[j].unsign()) != l_Undef); + final ^= (modelValue(c[j].unsign()) == l_True); + } + if (!final) { + printf("unsatisfied clause: "); + printClause(*xorclauses[i]); + printf("\n"); + failed = true; + } + } + + return failed; +} + +void Solver::verifyModel() +{ + bool failed = false; + for (int i = 0; i < clauses.size(); i++) { + Clause& c = *clauses[i]; + for (uint j = 0; j < c.size(); j++) + if (modelValue(c[j]) == l_True) + goto next; + + printf("unsatisfied clause: "); + printClause(*clauses[i]); + printf("\n"); + failed = true; +next: + ; + } + + failed |= verifyXorClauses(xorclauses); + failed |= verifyXorClauses(conglomerate->getCalcAtFinish()); + + assert(!failed); + + printf("Verified %d clauses.\n", clauses.size() + xorclauses.size() + conglomerate->getCalcAtFinish().size()); +} + + +void Solver::checkLiteralCount() +{ + // Check that sizes are calculated correctly: + int cnt = 0; + for (int i = 0; i < clauses.size(); i++) + cnt += clauses[i]->size(); + + for (int i = 0; i < xorclauses.size(); i++) + cnt += xorclauses[i]->size(); + + if ((int)clauses_literals != cnt) { + fprintf(stderr, "literal count: %d, real value = %d\n", (int)clauses_literals, cnt); + assert((int)clauses_literals == cnt); + } +} + +}; diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h new file mode 100644 index 0000000..f0596a5 --- /dev/null +++ b/src/sat/cryptominisat2/Solver.h @@ -0,0 +1,474 @@ +/****************************************************************************************[Solver.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef SOLVER_H +#define SOLVER_H + +#include +#include + +#include "Vec.h" +#include "Heap.h" +#include "Alg.h" +#include "MersenneTwister.h" +#include "SolverTypes.h" +#include "Clause.h" +#include "VarReplacer.h" +#include "GaussianConfig.h" +#include "Logger.h" + +namespace MINISAT +{ +using namespace MINISAT; + +class Gaussian; +class MatrixFinder; +class Conglomerate; +class VarReplacer; +class XorFinder; +class FindUndef; + +//#define VERBOSE_DEBUG_XOR +//#define VERBOSE_DEBUG + +#ifdef VERBOSE_DEBUG +using std::cout; +using std::endl; +#endif + + +//================================================================================================= +// Solver -- the main class: + +class Solver +{ +public: + + // Constructor/Destructor: + // + Solver(); + ~Solver(); + + // Problem specification: + // + Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + bool addClause (vec& ps, const uint group, char* group_name); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + bool addXorClause (vec& ps, bool xor_clause_inverted, const uint group, char* group_name); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! + + // Solving: + // + lbool simplify (); // Removes already satisfied clauses. + lbool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. + lbool solve (); // Search without assumptions. + bool okay () const; // FALSE means solver is in a conflicting state + + // Variable mode: + // + void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. + void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. + void setSeed (const uint32_t seed); // Sets the seed to be the given number + void permutateClauses(); // Permutates the clauses using the seed. It updates the seed in mtrand + void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown + void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on) + void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value + + // 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. + int nAssigns () const; // The current number of assigned literals. + int nClauses () const; // The current number of original clauses. + int nLearnts () const; // The current number of learnt clauses. + int nVars () const; // The current number of variables. + + // Extra results: (read-only member variable) + // + vec model; // If problem is satisfiable, this vector contains the model (if any). + vec conflict; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + + // Mode of operation: + // + double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95) + double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999) + double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) + 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) + bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE) + int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) + int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0) + uint restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all]) + bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true + vector realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable + bool xorFinder; // Automatically find xor-clauses and convert them + void set_gaussian_decision_until(const uint to); + void set_gaussian_decision_from(const uint from); + + + enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 }; + + // Statistics: (read-only member variable) + // + uint64_t starts, decisions, rnd_decisions, propagations, conflicts; + uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; + + //Logging + void needStats(); // Prepares the solver to output statistics + void needProofGraph(); // Prepares the solver to output proof graphs during solving + void setVariableName(int var, char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger') + const vec& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses + const vec& get_learnts() const; //Get all learnt clauses + const vec& get_unitary_learnts() const; //return the set of unitary learned clauses + void dump_sorted_learnts(const char* file); + friend class FindUndef; + bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef) + +protected: + vector gauss_matrixes; + GaussianConfig gaussconfig; + void print_gauss_sum_stats() const; + friend class Gaussian; + + + // Helper structures: + // + struct VarOrderLt { + const vec& activity; + bool operator () (Var x, Var y) const { + return activity[x] > activity[y]; + } + VarOrderLt(const vec& act) : activity(act) { } + }; + + friend class VarFilter; + struct VarFilter { + const Solver& s; + VarFilter(const Solver& _s) : s(_s) {} + bool operator()(Var v) const { + return s.assigns[v].isUndef() && s.decision_var[v]; + } + }; + + // Solver state: + // + bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! + vec clauses; // List of problem clauses. + vec xorclauses; // List of problem xor-clauses. + vec learnts; // List of learnt clauses. + vec unitary_learnts; // List of learnt clauses. + double cla_inc; // Amount to bump next clause with. + vec activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. + vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. + vec assigns; // The current assignments + vector polarity; // The preferred polarity of each variable. + vector decision_var; // Declares if a variable is eligible for selection in the decision heuristic. + vec trail; // Assignment stack; stores all assigments made in the order they were made. + vec trail_lim; // Separator indices for different decision levels in 'trail'. + vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + vec level; // 'level[var]' contains the level at which the assignment was made. + int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). + int 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()'. + vec assumptions; // Current set of assumptions provided to solve by the user. + Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. + double progress_estimate;// Set by 'search()'. + bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. + MTRand mtrand; // random number generator + Logger logger; // dynamic logging, statistics + friend class Logger; + bool dynamic_behaviour_analysis; //should 'logger' be called whenever a propagation/conflict/decision is made? + uint maxRestarts; // More than this number of restarts will not be performed + + // 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. + // + vec seen; + vec analyze_stack; + vec analyze_toclear; + vec add_tmp; + + //Logging + uint learnt_clause_group; //the group number of learnt clauses. Incremented at each added learnt clause + + // Main internal methods: + // + void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. + Lit pickBranchLit (int polarity_mode); // Return the next decision variable. + void newDecisionLevel (); // Begins a new decision level. + void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. + bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. + Clause* propagate (const bool xor_as_well = true); // Perform unit propagation. Returns possibly conflicting clause. + Clause* propagate_xors (const Lit& p); + void cancelUntil (int level); // Backtrack until a certain level. + void analyze (Clause* confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) + void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? + bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') + lbool search (int nof_conflicts, int nof_learnts); // Search for a given number of conflicts. + void reduceDB (); // Reduce the set of learnt clauses. + template + void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. + void cleanClauses (vec& cs); + bool cleanClause (Clause& c) const; + void cleanClauses (vec& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses + llbool handle_conflict (vec& learnt_clause, Clause* confl, int& conflictC);// Handles the conflict clause + llbool new_decision (int& nof_conflicts, int& nof_learnts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made + + // Maintaining Variable/Clause activity: + // + 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. + void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value. + + // Operations on clauses: + // + void attachClause (XorClause& c); + void attachClause (Clause& c); // Attach a clause to watcher lists. + void detachClause (const XorClause& c); + void detachClause (const Clause& c); // Detach a clause to watcher lists. + void detachModifiedClause(const Lit lit1, const Lit lit2, const uint size, const Clause* address); + template + void removeClause(T& c); // Detach and free a clause. + bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. + bool satisfied (const XorClause& c) const; // Returns TRUE if the clause is satisfied in the current state + bool satisfied (const Clause& c) const; // Returns TRUE if the clause is satisfied in the current state. + + // Misc: + // + int decisionLevel () const; // Gives the current decisionlevel. + uint32_t abstractLevel (const Var& x) const; // Used to represent an abstraction of sets of decision levels. + double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... + + //Xor-finding related stuff + friend class XorFinder; + friend class Conglomerate; + friend class MatrixFinder; + friend class VarReplacer; + Conglomerate* conglomerate; + VarReplacer* toReplace; + + // Debug: + void printLit (const Lit l) const; + void printClause (const Clause& c) const; + void printClause (const XorClause& c) const; + void verifyModel (); + bool verifyXorClauses (const vec& cs) const; + void checkLiteralCount(); +}; + + +//================================================================================================= +// Implementation of inline methods: + + +inline void Solver::insertVarOrder(Var x) +{ + if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); +} + +inline void Solver::varDecayActivity() +{ + var_inc *= var_decay; +} +inline void Solver::varBumpActivity(Var v) +{ + if ( (activity[v] += var_inc) > 1e100 ) { + // Rescale: + for (int i = 0; i < nVars(); i++) + activity[i] *= 1e-100; + var_inc *= 1e-100; + } + + // Update order_heap with respect to new activity: + if (order_heap.inHeap(v)) + order_heap.decrease(v); +} + +inline void Solver::claDecayActivity() +{ + cla_inc *= clause_decay; +} +inline void Solver::claBumpActivity (Clause& c) +{ + if ( (c.activity() += cla_inc) > 1e20 ) { + // Rescale: + for (int i = 0; i < learnts.size(); i++) + learnts[i]->activity() *= 1e-20; + cla_inc *= 1e-20; + } +} + +inline bool Solver::enqueue (Lit p, Clause* from) +{ + return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); +} +inline bool Solver::locked (const Clause& c) const +{ + return reason[c[0].var()] == &c && value(c[0]) == l_True; +} +inline void Solver::newDecisionLevel() +{ + trail_lim.push(trail.size()); + #ifdef VERBOSE_DEBUG + cout << "New decision level:" << trail_lim.size() << endl; + #endif +} +inline int Solver::decisionLevel () const +{ + return trail_lim.size(); +} +inline uint32_t Solver::abstractLevel (const Var& x) const +{ + return 1 << (level[x] & 31); +} +inline lbool Solver::value (const Var& x) const +{ + return assigns[x]; +} +inline lbool Solver::value (const Lit& p) const +{ + return assigns[p.var()] ^ p.sign(); +} +inline lbool Solver::modelValue (const Lit& p) const +{ + return model[p.var()] ^ p.sign(); +} +inline int Solver::nAssigns () const +{ + return trail.size(); +} +inline int Solver::nClauses () const +{ + return clauses.size() + xorclauses.size(); +} +inline int Solver::nLearnts () const +{ + return learnts.size(); +} +inline int Solver::nVars () const +{ + return assigns.size(); +} +inline void Solver::setPolarity (Var v, bool b) +{ + polarity [v] = (char)b; +} +inline void Solver::setDecisionVar(Var v, bool b) +{ + decision_var[v] = b; + if (b) { + insertVarOrder(v); + } +} +inline lbool Solver::solve () +{ + vec tmp; + return solve(tmp); +} +inline bool Solver::okay () const +{ + return ok; +} +inline void Solver::setSeed (const uint32_t seed) +{ + mtrand.seed(seed); // Set seed of the variable-selection and clause-permutation(if applicable) +} +inline void Solver::needStats() +{ + dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate statistics + logger.statistics_on = true; +} +inline void Solver::needProofGraph() +{ + dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate proof graphs during solving + logger.proof_graph_on = true; +} +inline void Solver::setVariableName(int var, char* 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 +inline void Solver::needRealUnknowns() +{ + useRealUnknowns = true; +} +template +void Solver::removeSatisfied(vec& cs) +{ + int i,j; + for (i = j = 0; i < cs.size(); i++) { + if (satisfied(*cs[i])) + removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); +} +template +void Solver::removeClause(T& c) +{ + detachClause(c); + free(&c); +} + + +//================================================================================================= +// Debug + etc: + +static inline void logLit(FILE* f, Lit l) +{ + fprintf(f, "%sx%d", l.sign() ? "~" : "", l.var()+1); +} + +static inline void logLits(FILE* f, const vec& ls) +{ + fprintf(f, "[ "); + if (ls.size() > 0) { + logLit(f, ls[0]); + for (int i = 1; i < ls.size(); i++) { + fprintf(f, ", "); + logLit(f, ls[i]); + } + } + fprintf(f, "] "); +} + +static inline const char* showBool(bool b) +{ + return b ? "true" : "false"; +} + + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(bool expr) +{ + assert(expr); +} + +//================================================================================================= +}; + +#endif //SOLVER_H diff --git a/src/sat/cryptominisat2/SolverTypes.h b/src/sat/cryptominisat2/SolverTypes.h new file mode 100644 index 0000000..7499c56 --- /dev/null +++ b/src/sat/cryptominisat2/SolverTypes.h @@ -0,0 +1,169 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + + +#ifndef SOLVERTYPES_H +#define SOLVERTYPES_H + +#include +#include +#include "Alg.h" + +namespace MINISAT +{ +using namespace MINISAT; + +//================================================================================================= +// Variables, literals, lifted booleans, clauses: + + +// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, +// so that they can be used as array indices. + +typedef uint32_t Var; +#define var_Undef (0xffffffffU >>1) + +class Lit +{ + uint32_t x; + explicit Lit(uint32_t i) : x(i) { }; +public: + Lit() : x(2*var_Undef) {} // (lit_Undef) + explicit Lit(Var var, bool sign) : x((var+var) + (int)sign) { } + + const uint32_t& toInt() const { // Guarantees small, positive integers suitable for array indexing. + return x; + } + Lit operator~() const { + return Lit(x ^ 1); + } + Lit operator^(const bool b) const { + return Lit(x ^ b); + } + Lit& operator^=(const bool b) { + x ^= b; + return *this; + } + bool sign() const { + return x & 1; + } + Var var() const { + return x >> 1; + } + Lit unsign() const { + return Lit(x & ~1); + } + bool operator==(const Lit& p) const { + return x == p.x; + } + bool operator!= (const Lit& p) const { + return x != p.x; + } + bool operator < (const Lit& p) const { + return x < p.x; // '<' guarantees that p, ~p are adjacent in the ordering. + } +}; + +const Lit lit_Undef(var_Undef, false); // }- Useful special constants. +const Lit lit_Error(var_Undef, true ); // } + +//================================================================================================= +// Lifted booleans: + +class llbool; + +class lbool +{ + char value; + explicit lbool(char v) : value(v) { } + +public: + lbool() : value(0) { }; + inline char getchar() const { + return value; + } + inline lbool(llbool b); + + inline const bool isUndef() const { + return !value; + } + inline const bool isDef() const { + return value; + } + inline const bool getBool() const { + return (value+1) >> 1; + } + inline const bool operator==(lbool b) const { + return value == b.value; + } + inline const bool operator!=(lbool b) const { + return value != b.value; + } + lbool operator^(const bool b) const { + return lbool(value - value*2*b); + } + //lbool operator ^ (const bool b) const { return b ? lbool(-value) : lbool(value); } + + friend lbool toLbool(const char v); + friend lbool boolToLBool(const bool b); + friend class llbool; +}; +inline lbool toLbool(const char v) +{ + return lbool(v); +} +inline lbool boolToLBool(const bool b) +{ + return lbool(2*b-1); +} + +const lbool l_True = toLbool( 1); +const lbool l_False = toLbool(-1); +const lbool l_Undef = toLbool( 0); + + +class llbool +{ + char value; + +public: + llbool(): value(0) {}; + llbool(lbool v) : + value(v.value) {}; + llbool(char a) : + value(a) {} + + inline const bool operator!=(const llbool& v) const { + return (v.value != value); + } + + inline const bool operator==(const llbool& v) const { + return (v.value == value); + } + + friend class lbool; +}; +const llbool l_Nothing = toLbool(2); +const llbool l_Continue = toLbool(3); + +lbool::lbool(llbool b) : value(b.value) {}; +}; + +#endif //SOLVERTYPES_H diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION new file mode 100644 index 0000000..270c744 --- /dev/null +++ b/src/sat/cryptominisat2/VERSION @@ -0,0 +1 @@ +CryptoMiniSat SVN revision: r454 , GIT revision: 91b7fc803564cfd5e5af363c81c1c68bdced162b diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp new file mode 100644 index 0000000..c3b31c6 --- /dev/null +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -0,0 +1,338 @@ +#include "VarReplacer.h" + +#include "Solver.h" +#include "Conglomerate.h" + +//#define VERBOSE_DEBUG + +#ifdef VERBOSE_DEBUG +#include +using std::cout; +using std::endl; +#endif + +namespace MINISAT +{ + +VarReplacer::VarReplacer(Solver *_S) : + replacedLits(0) + , replacedVars(0) + , S(_S) +{ +} + +void VarReplacer::performReplace() +{ + #ifdef VERBOSE_DEBUG + cout << "Replacer started." << endl; + uint i = 0; + for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { + if (it->var() == i) continue; + cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") << it->var()+1 << endl; + } + #endif + + if (replacedVars == 0) return; + + replace_set(S->clauses); + replace_set(S->learnts); + + replace_set(S->xorclauses, true); + replace_set(S->conglomerate->getCalcAtFinish(), false); + + printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits); + + replacedVars = 0; + replacedLits = 0; + + if (S->ok) + S->ok = (S->propagate() == NULL); + + S->order_heap.filter(Solver::VarFilter(*S)); +} + +void VarReplacer::replace_set(vec& cs, const bool need_reattach) +{ + XorClause **a = cs.getData(); + XorClause **r = a; + for (XorClause **end = a + cs.size(); r != end;) { + XorClause& c = **r; + + bool needReattach = false; + for (Lit *l = &c[0], *lend = l + c.size(); l != lend; l++) { + Lit newlit = table[l->var()]; + if (newlit.var() != l->var()) { + if (need_reattach && !needReattach) + S->detachClause(c); + needReattach = true; + *l = Lit(newlit.var(), false); + c.invert(newlit.sign()); + replacedLits++; + } + } + + if (need_reattach && needReattach) { + std::sort(c.getData(), c.getData() + c.size()); + Lit p; + int i, j; + for (i = j = 0, p = lit_Undef; i < c.size(); i++) { + c[i] = c[i].unsign(); + if (c[i] == p) { + //added, but easily removed + j--; + p = lit_Undef; + if (!S->assigns[c[i].var()].isUndef()) + c.invert(S->assigns[c[i].var()].getBool()); + } else if (S->value(c[i]) == l_Undef) //just add + c[j++] = p = c[i]; + else c.invert(S->value(c[i]) == l_True); //modify xor_clause_inverted instead of adding + } + c.shrink(i - j); + + switch (c.size()) { + case 0: { + if (!c.xor_clause_inverted()) + S->ok = false; + free(&c); + r++; + break; + } + case 1: { + S->uncheckedEnqueue(Lit(c[0].var(), !c.xor_clause_inverted())); + free(&c); + r++; + break; + } + default: { + S->attachClause(c); + *a++ = *r++; + break; + } + } + } else { + *a++ = *r++; + } + } + cs.shrink(r-a); +} + +void VarReplacer::replace_set(vec& cs) +{ + Clause **a = cs.getData(); + Clause **r = a; + for (Clause **end = a + cs.size(); r != end; ) { + Clause& c = **r; + bool changed = false; + Lit origLit1 = c[0]; + Lit origLit2 = c[1]; + for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + if (table[l->var()].var() != l->var()) { + changed = true; + *l = table[l->var()] ^ l->sign(); + replacedLits++; + } + } + + if (changed && handleUpdatedClause(c, origLit1, origLit2)) { + free(&c); + r++; + } else { + *a++ = *r++; + } + } + cs.shrink(r-a); +} + +bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2) +{ + bool satisfied = false; + std::sort(c.getData(), c.getData() + c.size()); + Lit p; + int i, j; + const uint origSize = c.size(); + for (i = j = 0, p = lit_Undef; i < origSize; i++) { + if (S->value(c[i]) == l_True || c[i] == ~p) { + satisfied = true; + break; + } + else if (S->value(c[i]) != l_False && c[i] != p) + c[j++] = p = c[i]; + } + c.shrink(i - j); + + if (satisfied) { + S->detachModifiedClause(origLit1, origLit2, origSize, &c); + return true; + } + + switch(c.size()) { + case 0: + S->detachModifiedClause(origLit1, origLit2, origSize, &c); + S->ok = false; + return true; + case 1 : + S->uncheckedEnqueue(c[0]); + S->detachModifiedClause(origLit1, origLit2, origSize, &c); + return true; + default: + if (origLit1 != c[0] || origLit2 != c[1]) { + S->detachModifiedClause(origLit1, origLit2, origSize, &c); + S->attachClause(c); + } + return false; + } +} + +const uint VarReplacer::getNumReplacedLits() const +{ + return replacedLits; +} + +const uint VarReplacer::getNumReplacedVars() const +{ + return replacedVars; +} + +const vector VarReplacer::getReplacingVars() const +{ + vector replacingVars; + + for(map >::const_iterator it = reverseTable.begin(), end = reverseTable.end(); it != end; it++) { + replacingVars.push_back(it->first); + } + + return replacingVars; +} + +void VarReplacer::extendModel() const +{ + uint i = 0; + for (vector::const_iterator it = table.begin(); it != table.end(); it++, i++) { + if (it->var() == i) continue; + + #ifdef VERBOSE_DEBUG + cout << "Extending model: var "; S->printLit(Lit(i, false)); + cout << " to "; S->printLit(*it); + cout << endl; + #endif + + assert(S->assigns[i] == l_Undef); + assert(S->assigns[it->var()] != l_Undef); + + bool val = (S->assigns[it->var()] == l_False); + S->uncheckedEnqueue(Lit(i, val ^ it->sign())); + } +} + +void VarReplacer::replace(Var var, Lit lit) +{ + assert(var != lit.var()); + + //Detect circle + if (alreadyIn(var, lit)) return; + replacedVars++; + + Lit lit1 = table[var]; + bool inverted = false; + + //This pointer is already set, try to invert + if (lit1.var() != var) { + Var tmp_var = var; + + var = lit.var(); + lit = Lit(tmp_var, lit.sign()); + inverted = true; + } + + if (inverted) { + //Inversion is also set + Lit lit2 = table[var]; + + //triangular cycle + if (lit1.var() == lit2.var()) { + if (lit1.sign() ^ lit2.sign() != lit.sign()) { + #ifdef VERBOSE_DEBUG + cout << "Inverted cycle in var-replacement -> UNSAT" << endl; + #endif + S->ok = false; + } + return; + } + + if (lit2.var() != var) { + setAllThatPointsHereTo(lit1.var(), Lit(lit.var(), lit1.sign())); + table[lit1.var()] = Lit(lit.var(), lit1.sign()); + reverseTable[lit.var()].push_back(lit1.var()); + S->setDecisionVar(lit1.var(), false); + + setAllThatPointsHereTo(lit2.var(), lit ^ lit2.sign()); + table[lit2.var()] = lit ^ lit2.sign(); + reverseTable[lit.var()].push_back(lit2.var()); + S->setDecisionVar(lit2.var(), false); + + table[lit.var()] = Lit(lit.var(), false); + S->setDecisionVar(lit.var(), true); + return; + } + } + + //Follow forwards + Lit lit2 = table[lit.var()]; + if (lit2.var() != lit.var()) + lit = lit2 ^ lit.sign(); + + //Follow backwards + setAllThatPointsHereTo(var, lit); + + table[var] = lit; + reverseTable[lit.var()].push_back(var); + S->setDecisionVar(var, false); +} + +bool VarReplacer::alreadyIn(const Var var, const Lit lit) +{ + Lit lit2 = table[var]; + if (lit2.var() == lit.var()) { + if (lit2.sign() != lit.sign()) { + #ifdef VERBOSE_DEBUG + cout << "Inverted cycle in var-replacement -> UNSAT" << endl; + #endif + S->ok = false; + } + return true; + } + + lit2 = table[lit.var()]; + if (lit2.var() == var) { + if (lit2.sign() != lit.sign()) { + #ifdef VERBOSE_DEBUG + cout << "Inverted cycle in var-replacement -> UNSAT" << endl; + #endif + S->ok = false; + } + return true; + } + + return false; +} + +void VarReplacer::setAllThatPointsHereTo(const Var var, const Lit lit) +{ + map >::iterator it = reverseTable.find(var); + if (it == reverseTable.end()) + return; + + for(vector::const_iterator it2 = it->second.begin(), end = it->second.end(); it2 != end; it2++) { + assert(table[*it2].var() == var); + table[*it2] = lit ^ table[*it2].sign(); + if (lit.var() != *it2) + reverseTable[lit.var()].push_back(*it2); + } + reverseTable.erase(it); +} + +void VarReplacer::newVar() +{ + table.push_back(Lit(table.size(), false)); +} +}; diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h new file mode 100644 index 0000000..3d11ff0 --- /dev/null +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -0,0 +1,48 @@ +#ifndef VARREPLACER_H +#define VARREPLACER_H + +#include "SolverTypes.h" +#include "Clause.h" +#include "Vec.h" + +#include +#include +#include + +namespace MINISAT +{ + +using std::map; +using std::vector; + +class Solver; + +class VarReplacer +{ + public: + VarReplacer(Solver* S); + void replace(const Var var, Lit lit); + void extendModel() const; + void performReplace(); + const uint getNumReplacedLits() const; + const uint getNumReplacedVars() const; + const vector getReplacingVars() const; + void newVar(); + + private: + void replace_set(vec& set); + void replace_set(vec& cs, const bool need_reattach); + bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2); + + void setAllThatPointsHereTo(const Var var, const Lit lit); + bool alreadyIn(const Var var, const Lit lit); + + vector table; + map > reverseTable; + + uint replacedLits; + uint replacedVars; + Solver* S; +}; +}; +#endif //VARREPLACER_H diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp new file mode 100644 index 0000000..d3c0a11 --- /dev/null +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -0,0 +1,321 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#include "XorFinder.h" + +#include +#include +#include +#include "Solver.h" +#include "VarReplacer.h" + +namespace MINISAT +{ + + +//#define VERBOSE_DEBUG + +#ifdef VERBOSE_DEBUG +#include +using std::cout; +using std::endl; +#endif + +using std::make_pair; + +XorFinder::XorFinder(Solver* _S, vec& _cls, vec& _xorcls) : + cls(_cls) + , xorcls(_xorcls) + , S(_S) +{ +} + +uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSize) +{ + toRemove.clear(); + toRemove.resize(cls.size(), false); + + table.clear(); + table.reserve(cls.size()/2); + uint i = 0; + for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++, i++) { + const uint size = (*it)->size(); + if ( size > maxSize || size < minSize) continue; + table.push_back(make_pair(*it, i)); + } + + uint found = findXors(sumLengths); + if (found > 0) { + clearToRemove(); + + S->toReplace->performReplace(); + if (S->ok == false) return found; + S->ok = (S->propagate() == NULL); + } + + return found; +} + +uint XorFinder::doByPart(uint& sumLengths, const uint minSize, const uint maxSize) +{ + toRemove.clear(); + toRemove.resize(cls.size(), false); + + uint sumUsage = 0; + vector varUsage(S->nVars(), 0); + for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++) { + const uint size = (*it)->size(); + if ( size > maxSize || size < minSize) continue; + + for (const Lit *l = &(**it)[0], *end = l + size; l != end; l++) { + varUsage[l->var()]++; + sumUsage++; + } + } + + uint found = 0; + #ifdef VERBOSE_DEBUG + uint sumNumClauses = 0; + #endif + + const uint limit = 800000; + uint from = 0; + uint until = 0; + while (until < varUsage.size()) { + uint estimate = 0; + for (; until < varUsage.size(); until++) { + estimate += varUsage[until]; + if (estimate >= limit) break; + } + #ifdef VERBOSE_DEBUG + printf("Xor-finding: Vars from: %d, until: %d\n", from, until); + uint numClauses = 0; + #endif + + table.clear(); + table.reserve(estimate/2); + uint i = 0; + for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++, i++) { + if (toRemove[i]) continue; + const uint size = (*it)->size(); + if ( size > maxSize || size < minSize) continue; + + for (Lit *l = &(**it)[0], *end = l + size; l != end; l++) { + if (l->var() >= from && l->var() <= until) { + table.push_back(make_pair(*it, i)); + #ifdef VERBOSE_DEBUG + numClauses++; + #endif + break; + } + } + } + #ifdef VERBOSE_DEBUG + printf("numClauses in range: %d\n", numClauses); + sumNumClauses += numClauses; + #endif + + uint lengths; + found += findXors(lengths); + sumLengths += lengths; + #ifdef VERBOSE_DEBUG + printf("Found in this range: %d\n", found); + #endif + + from = until+1; + } + + clearToRemove(); + + S->toReplace->performReplace(); + if (S->ok == false) return found; + S->ok = (S->propagate() == NULL); + + #ifdef VERBOSE_DEBUG + cout << "Overdone work due to partitioning:" << (double)sumNumClauses/(double)cls.size() << "x" << endl; + #endif + + return found; +} + +uint XorFinder::findXors(uint& sumLengths) +{ + #ifdef VERBOSE_DEBUG + cout << "Finding Xors started" << endl; + #endif + + uint foundXors = 0; + sumLengths = 0; + std::sort(table.begin(), table.end(), clause_sorter_primary()); + + ClauseTable::iterator begin = table.begin(); + ClauseTable::iterator end = table.begin(); + vector lits; + bool impair; + while (getNextXor(begin, end, impair)) { + const Clause& c = *(begin->first); + lits.clear(); + for (const Lit *it = &c[0], *cend = it+c.size() ; it != cend; it++) { + lits.push_back(Lit(it->var(), false)); + } + uint old_group = c.group; + + #ifdef VERBOSE_DEBUG + cout << "- Found clauses:" << endl; + #endif + + for (ClauseTable::iterator it = begin; it != end; it++) { + #ifdef VERBOSE_DEBUG + it->first->plain_print(); + #endif + toRemove[it->second] = true; + S->removeClause(*it->first); + } + + switch(lits.size()) { + case 2: { + S->toReplace->replace(lits[0].var(), Lit(lits[1].var(), !impair)); + + #ifdef VERBOSE_DEBUG + XorClause* x = XorClause_new(lits, impair, old_group); + cout << "- Final 2-long xor-clause: "; + x->plain_print(); + free(x); + #endif + break; + } + default: { + XorClause* x = XorClause_new(lits, impair, old_group); + xorcls.push(x); + S->attachClause(*x); + + #ifdef VERBOSE_DEBUG + cout << "- Final xor-clause: "; + x->plain_print(); + #endif + } + } + + foundXors++; + sumLengths += lits.size(); + } + + return foundXors; +} + +void XorFinder::clearToRemove() +{ + Clause **a = cls.getData(); + Clause **r = cls.getData(); + Clause **cend = cls.getData() + cls.size(); + for (uint i = 0; r != cend; i++) { + if (!toRemove[i]) + *a++ = *r++; + else + r++; + } + cls.shrink(r-a); +} + +bool XorFinder::getNextXor(ClauseTable::iterator& begin, ClauseTable::iterator& end, bool& impair) +{ + ClauseTable::iterator tableEnd = table.end(); + + while(begin != tableEnd && end != tableEnd) { + begin = end; + end++; + while(end != tableEnd && clause_vareq(begin->first, end->first)) + end++; + if (isXor(begin, end, impair)) + return true; + } + + return false; +} + +bool XorFinder::clauseEqual(const Clause& c1, const Clause& c2) const +{ + assert(c1.size() == c2.size()); + for (uint i = 0, size = c1.size(); i < size; i++) + if (c1[i].sign() != c2[i].sign()) return false; + + return true; +} + +bool XorFinder::impairSigns(const Clause& c) const +{ + uint num = 0; + for (const Lit *it = &c[0], *end = it + c.size(); it != end; it++) + num += it->sign(); + + return num % 2; +} + +bool XorFinder::isXor(const ClauseTable::iterator& begin, const ClauseTable::iterator& end, bool& impair) +{ + uint size = &(*begin) - &(*end); + assert(size > 0); + const uint requiredSize = 1 << (begin->first->size()-1); + + if (size < requiredSize) + return false; + + std::sort(begin, end, clause_sorter_secondary()); + + uint numPair = 0; + uint numImpair = 0; + countImpairs(begin, end, numImpair, numPair); + + if (numImpair == requiredSize) { + impair = true; + + return true; + } + + if (numPair == requiredSize) { + impair = false; + + return true; + } + + return false; +} + +void XorFinder::countImpairs(const ClauseTable::iterator& begin, const ClauseTable::iterator& end, uint& numImpair, uint& numPair) const +{ + numImpair = 0; + numPair = 0; + + ClauseTable::const_iterator it = begin; + ClauseTable::const_iterator it2 = begin; + it2++; + + bool impair = impairSigns(*it->first); + numImpair += impair; + numPair += !impair; + + for (; it2 != end;) { + if (!clauseEqual(*it->first, *it2->first)) { + bool impair = impairSigns(*it2->first); + numImpair += impair; + numPair += !impair; + } + it++; + it2++; + } +} +}; diff --git a/src/sat/cryptominisat2/XorFinder.h b/src/sat/cryptominisat2/XorFinder.h new file mode 100644 index 0000000..a6c480a --- /dev/null +++ b/src/sat/cryptominisat2/XorFinder.h @@ -0,0 +1,120 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + +#ifndef XORFINDER_H +#define XORFINDER_H + +#include "Clause.h" +#include +#include "VarReplacer.h" + +namespace MINISAT +{ + +class Solver; + +using std::pair; + +class XorFinder +{ + public: + + XorFinder(Solver* S, vec& cls, vec& xorcls); + uint doByPart(uint& sumLengths, const uint minSize, const uint maxSize); + uint doNoPart(uint& sumLengths, const uint minSize, const uint maxSize); + + private: + typedef vector > ClauseTable; + + uint findXors(uint& sumLengths); + bool getNextXor(ClauseTable::iterator& begin, ClauseTable::iterator& end, bool& impair); + + struct clause_hasher { + size_t operator()(const Clause* c) const + { + size_t hash = 5381; + hash = ((hash << 5) + hash) ^ c->size(); + for (uint i = 0, size = c->size(); i < size; i++) + hash = ((hash << 5) + hash) ^ (*c)[i].var(); + + return hash; + } + }; + + struct clause_sorter_primary { + bool operator()(const pair& c11, const pair& c22) + { + if (c11.first->size() != c22.first->size()) + return (c11.first->size() < c22.first->size()); + + for (a = c11.first->getData(), b = c22.first->getData(), end = a + c11.first->size(); a != end; a++, b++) { + if (a->var() != b->var()) + return (a->var() < b->var()); + } + + return false; + } + + Lit const *a; + Lit const *b; + Lit const *end; + }; + + struct clause_sorter_secondary { + bool operator()(const pair& c11, const pair& c22) const + { + const Clause& c1 = *(c11.first); + const Clause& c2 = *(c22.first); + + for (uint i = 0, size = c1.size(); i < size; i++) { + if (c1[i].sign() != c2[i].sign()) + return c2[i].sign(); + } + + return false; + } + }; + + bool clause_vareq(const Clause* c1, const Clause* c2) const + { + if (c1->size() != c2->size()) + return false; + + for (uint i = 0, size = c1->size(); i < size; i++) + if ((*c1)[i].var() != (*c2)[i].var()) + return false; + + return true; + } + + ClauseTable table; + vector toRemove; + void clearToRemove(); + + vec& cls; + vec& xorcls; + + bool clauseEqual(const Clause& c1, const Clause& c2) const; + bool impairSigns(const Clause& c) const; + void countImpairs(const ClauseTable::iterator& begin, const ClauseTable::iterator& end, uint& numImpair, uint& numPair) const; + bool isXor(const ClauseTable::iterator& begin, const ClauseTable::iterator& end, bool& impair); + + Solver* S; +}; +}; + +#endif //XORFINDER_H diff --git a/src/sat/cryptominisat2/time_mem.h b/src/sat/cryptominisat2/time_mem.h new file mode 100644 index 0000000..1e09812 --- /dev/null +++ b/src/sat/cryptominisat2/time_mem.h @@ -0,0 +1,75 @@ +#ifndef TIME_MEM_H +#define TIME_MEM_H + +namespace MINISAT +{ + +#ifdef _MSC_VER +#include + +static inline double cpuTime(void) +{ + return (double)clock() / CLOCKS_PER_SEC; +} +#else +#ifdef CROSS_COMPILE +#include + +static inline double cpuTime(void) +{ + return (double)clock() / CLOCKS_PER_SEC; +} +#else +#include +#include +#include + +static inline double cpuTime(void) +{ + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; +} +#endif +#endif + + +#if defined(__linux__) +static inline int memReadStat(int field) +{ + char name[256]; + pid_t pid = getpid(); + sprintf(name, "/proc/%d/statm", pid); + FILE* in = fopen(name, "rb"); + if (in == NULL) return 0; + int value; + for (; field >= 0; field--) + fscanf(in, "%d", &value); + fclose(in); + return value; +} +static inline uint64_t memUsed() +{ + return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); +} + + +#elif defined(__FreeBSD__) +static inline uint64_t memUsed(void) +{ + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return ru.ru_maxrss*1024; +} + + +#else +static inline uint64_t memUsed() +{ + return 0; +} +#endif + +}; + +#endif //TIME_MEM_H