From 5c4be04e77c9eb40331eaf0722bbd5c732cbedfc Mon Sep 17 00:00:00 2001 From: msoos Date: Fri, 4 Jun 2010 18:11:26 +0000 Subject: [PATCH] Last commit was wrong. Importing again CryptoMiniSat-'Cluster56' git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@813 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/BitArray.h | 193 +++ src/sat/cryptominisat2/BoundedQueue.h | 88 ++ src/sat/cryptominisat2/CSet.h | 136 ++ src/sat/cryptominisat2/Clause.cpp | 15 + src/sat/cryptominisat2/Clause.h | 496 ++++++++ src/sat/cryptominisat2/ClauseCleaner.cpp | 421 +++++++ src/sat/cryptominisat2/ClauseCleaner.h | 81 ++ src/sat/cryptominisat2/Conglomerate.cpp | 526 ++++++++ src/sat/cryptominisat2/Conglomerate.h | 125 ++ src/sat/cryptominisat2/DoublePackedRow.h | 173 +++ src/sat/cryptominisat2/FailedVarSearcher.cpp | 1045 ++++++++++++++++ src/sat/cryptominisat2/FailedVarSearcher.h | 169 +++ src/sat/cryptominisat2/FindUndef.cpp | 177 +++ src/sat/cryptominisat2/FindUndef.h | 59 + src/sat/cryptominisat2/Gaussian.cpp | 1161 ++++++++++++++++++ src/sat/cryptominisat2/Gaussian.h | 242 ++++ src/sat/cryptominisat2/GaussianConfig.h | 62 + src/sat/cryptominisat2/Logger.cpp | 909 ++++++++++++++ src/sat/cryptominisat2/Logger.h | 190 +++ src/sat/cryptominisat2/Makefile | 32 + src/sat/cryptominisat2/MatrixFinder.cpp | 249 ++++ src/sat/cryptominisat2/MatrixFinder.h | 72 ++ src/sat/cryptominisat2/MersenneTwister.h | 427 +++++++ src/sat/cryptominisat2/constants.h | 46 + 24 files changed, 7094 insertions(+) diff --git a/src/sat/cryptominisat2/BitArray.h b/src/sat/cryptominisat2/BitArray.h index e69de29..aa58b62 100644 --- a/src/sat/cryptominisat2/BitArray.h +++ b/src/sat/cryptominisat2/BitArray.h @@ -0,0 +1,193 @@ +/*********************************************************************************** +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 +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +namespace MINISAT +{ +using namespace MINISAT; + +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; + } + + BitArray& operator&=(const BitArray& b) + { + assert(size == b.size); + uint64_t* t1 = mp; + uint64_t* t2 = b.mp; + for (uint64_t i = 0; i < size; i++) { + *t1 &= *t2; + t1++; + t2++; + } + + return *this; + } + + const bool nothingInCommon(const BitArray& b) const + { + assert(size == b.size); + const uint64_t* t1 = mp; + const uint64_t* t2 = b.mp; + for (uint64_t i = 0; i < size; i++) { + if ((*t1)&(*t2)) return false; + t1++; + t2++; + } + + return true; + } + + BitArray& removeThese(const BitArray& b) + { + assert(size == b.size); + uint64_t* t1 = mp; + uint64_t* t2 = b.mp; + for (uint64_t i = 0; i < size; i++) { + *t1 &= ~(*t2); + t1++; + t2++; + } + + return *this; + } + + template + BitArray& removeThese(const T& rem) + { + for (uint32_t i = 0; i < rem.size(); i++) { + clearBit(rem[i]); + } + + return *this; + } + + void resize(uint _size, const bool fill) + { + _size = _size/64 + (bool)(_size%64); + if (size != _size) { + delete[] mp; + size = _size; + mp = new uint64_t[size]; + } + if (fill) setOne(); + else setZero(); + } + + ~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 setOne() + { + 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; +}; + +}; //NAMESPACE MINISAT + +#endif //BITARRAY_H + diff --git a/src/sat/cryptominisat2/BoundedQueue.h b/src/sat/cryptominisat2/BoundedQueue.h index e69de29..a705a6d 100644 --- a/src/sat/cryptominisat2/BoundedQueue.h +++ b/src/sat/cryptominisat2/BoundedQueue.h @@ -0,0 +1,88 @@ +/*****************************************************************************************[Queue.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + 2008 - Gilles Audemard, Laurent Simon + +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 BoundedQueue_h +#define BoundedQueue_h + +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "Vec.h" + +//================================================================================================= + +namespace MINISAT +{ +using namespace MINISAT; + +template +class bqueue { + vec elems; + int first; + int last; + uint64_t sumofqueue; + int maxsize; + int queuesize; // Number of current elements (must be < maxsize !) + +public: + bqueue(void) : first(0), last(0), sumofqueue(0), maxsize(0), queuesize(0) { } + + void initSize(int size) {growTo(size);} // Init size of bounded size queue + + void push(T x) { + if (queuesize==maxsize) { + assert(last==first); // The queue is full, next value to enter will replace oldest one + sumofqueue -= elems[last]; + if ((++last) == maxsize) last = 0; + } else + queuesize++; + sumofqueue += x; + elems[first] = x; + if ((++first) == maxsize) first = 0; + } + + T peek() { assert(queuesize>0); return elems[last]; } + void pop() {sumofqueue-=elems[last]; queuesize--; if ((++last) == maxsize) last = 0;} + + uint64_t getsum() const {return sumofqueue;} + uint32_t getavg() const {return (uint64_t)sumofqueue/(uint64_t)queuesize;} + int isvalid() const {return (queuesize==maxsize);} + + void growTo(int size) { + elems.growTo(size); + first=0; maxsize=size; queuesize = 0; + for(int i=0;i +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +namespace MINISAT +{ +using namespace MINISAT; + +class Clause; + +template +uint32_t calcAbstraction(const T& ps) { + uint32_t abstraction = 0; + for (uint32_t i = 0; i != ps.size(); i++) + abstraction |= 1 << (ps[i].toInt() & 31); + return abstraction; +} + +//#pragma pack(push) +//#pragma pack(1) +class ClauseSimp +{ + public: + ClauseSimp(Clause* c, const uint32_t _index) : + clause(c) + , index(_index) + {} + + Clause* clause; + uint32_t index; +}; +//#pragma pack(pop) + +class CSet { + vec where; // Map clause ID to position in 'which'. + vec which; // List of clauses (for fast iteration). May contain 'Clause_NULL'. + vec free; // List of positions holding 'Clause_NULL'. + + public: + //ClauseSimp& operator [] (uint32_t index) { return which[index]; } + void reserve(uint32_t size) { where.reserve(size);} + uint32_t size(void) const { return which.size(); } + uint32_t nElems(void) const { return which.size() - free.size(); } + + bool add(const ClauseSimp& c) { + assert(c.clause != NULL); + where.growTo(c.index+1, std::numeric_limits::max()); + if (where[c.index] != std::numeric_limits::max()) { + return true; + } + if (free.size() > 0){ + where[c.index] = free.last(); + which[free.last()] = c; + free.pop(); + }else{ + where[c.index] = which.size(); + which.push(c); + } + return false; + } + + bool exclude(const ClauseSimp& c) { + assert(c.clause != NULL); + if (c.index >= where.size() || where[c.index] == std::numeric_limits::max()) { + //not inside + return false; + } + free.push(where[c.index]); + which[where[c.index]].clause = NULL; + where[c.index] = std::numeric_limits::max(); + return true; + } + + void clear(void) { + for (uint32_t i = 0; i < which.size(); i++) { + if (which[i].clause != NULL) { + where[which[i].index] = std::numeric_limits::max(); + } + } + which.clear(); + free.clear(); + } + + class iterator + { + public: + iterator(ClauseSimp* _it) : + it(_it) + {} + + void operator++() + { + it++; + } + + const bool operator!=(const iterator& iter) const + { + return (it != iter.it);; + } + + ClauseSimp& operator*() { + return *it; + } + + ClauseSimp*& operator->() { + return it; + } + private: + ClauseSimp* it; + }; + + iterator begin() + { + return iterator(which.getData()); + } + + iterator end() + { + return iterator(which.getData() + which.size()); + } +}; + +}; //NAMESPACE MINISAT + +#endif //CSET_H \ No newline at end of file diff --git a/src/sat/cryptominisat2/Clause.cpp b/src/sat/cryptominisat2/Clause.cpp index e69de29..b81d636 100644 --- a/src/sat/cryptominisat2/Clause.cpp +++ b/src/sat/cryptominisat2/Clause.cpp @@ -0,0 +1,15 @@ +#include "Clause.h" + +namespace MINISAT +{ +using namespace MINISAT; + +#ifdef USE_POOLS +#ifdef USE_4POOLS +boost::pool<> clausePoolQuad(sizeof(Clause) + 5*sizeof(Lit)); +#endif //USE_4POOLS +boost::pool<> clausePoolTri(sizeof(Clause) + 3*sizeof(Lit)); +boost::pool<> clausePoolBin(sizeof(Clause) + 2*sizeof(Lit)); +#endif //USE_POOLS + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index e69de29..fab2159 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -0,0 +1,496 @@ +/***********************************************************************************[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 + +#ifdef _MSC_VER +#include +#else +#include "SmallPtr.h" +#include +#endif //_MSC_VER +#include +#include +#include +#include "Vec.h" +#include "SolverTypes.h" +#include "PackedRow.h" +#include "constants.h" +#include "SmallPtr.h" +#ifdef USE_POOLS +#include "pool.hpp" +#endif //USE_POOLS +#ifndef uint +#define uint unsigned int +#endif + +//#define USE_4POOLS + +using std::vector; + +namespace MINISAT +{ +using namespace MINISAT; + +//================================================================================================= +// Clause -- a simple class for representing a clause: + +class MatrixFinder; + +class Clause +{ +protected: + + #ifdef STATS_NEEDED + uint group; + #endif + + uint32_t isLearnt:1; + uint32_t strenghtened:1; + uint32_t varChanged:1; + uint32_t sorted:1; + uint32_t invertedXor:1; + uint32_t isXorClause:1; + uint32_t subsume0Done:1; + uint32_t isRemoved:1; + #ifdef USE_POOLS + uint32_t wasTriOriginallyInt:1; + uint32_t wasBinOriginallyInt:1; + #ifdef USE_4POOLS + uint32_t wasQuadOriginallyInt:1; + #endif //USE_4POOLS + #endif //USE_POOLS + uint32_t mySize:20; + + union {uint32_t act; uint32_t abst;} extra; + float oldActivityInter; + #ifdef _MSC_VER + Lit data[1]; + #else + Lit data[0]; + #endif //_MSC_VER + +#ifdef _MSC_VER +public: +#endif //_MSC_VER + template + Clause(const V& ps, const uint _group, const bool learnt) + { + isXorClause = false; + strenghtened = false; + sorted = false; + varChanged = true; + subsume0Done = false; + mySize = ps.size(); + isLearnt = learnt; + isRemoved = false; + setGroup(_group); + #ifdef USE_POOLS + setAllocSize(); + #endif //USE_POOLS + + for (uint i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) { + extra.act = 0; + oldActivityInter = 0; + } else + calcAbstraction(); + } + +public: + #ifndef _MSC_VER + // -- use this function instead: + template + friend Clause* Clause_new(const T& ps, const uint group, const bool learnt = false); + friend Clause* Clause_new(Clause& c); + #endif //_MSC_VER + + const uint size () const { + return mySize; + } + void resize (const uint size) { + mySize = size; + } + void shrink (const uint i) { + assert(i <= size()); + mySize -= i; + } + void pop () { + shrink(1); + } + const bool isXor () { + return isXorClause; + } + const bool learnt () const { + return isLearnt; + } + float& oldActivity () { + return oldActivityInter; + } + + const float& oldActivity () const { + return oldActivityInter; + } + + + const bool getStrenghtened() const { + return strenghtened; + } + void setStrenghtened() { + strenghtened = true; + sorted = false; + subsume0Done = false; + } + void unsetStrenghtened() { + strenghtened = false; + } + const bool getVarChanged() const { + return varChanged; + } + void setVarChanged() { + varChanged = true; + sorted = false; + subsume0Done = false; + } + void unsetVarChanged() { + varChanged = false; + } + const bool getSorted() const { + return sorted; + } + void setSorted() { + sorted = true; + } + void setUnsorted() { + sorted = false; + } + void subsume0Finished() { + subsume0Done = 1; + } + const bool subsume0IsFinished() { + return subsume0Done; + } + + Lit& operator [] (uint32_t i) { + return data[i]; + } + const Lit& operator [] (uint32_t i) const { + return data[i]; + } + + void setActivity(uint32_t i) { + extra.act = i; + } + + const uint32_t& activity () const { + return extra.act; + } + + void makeNonLearnt() { + assert(isLearnt); + isLearnt = false; + calcAbstraction(); + } + + void makeLearnt(const uint32_t newActivity) { + extra.act = newActivity; + oldActivityInter = 0; + isLearnt = true; + } + + inline void strengthen(const Lit p) + { + remove(*this, p); + sorted = false; + calcAbstraction(); + } + + void calcAbstraction() { + assert(!learnt()); + extra.abst = 0; + for (uint32_t i = 0; i != size(); i++) + extra.abst |= 1 << (data[i].toInt() & 31); + } + + uint32_t getAbst() + { + return extra.abst; + } + + const Lit* getData () const { + return data; + } + Lit* getData () { + return data; + } + const Lit* getDataEnd () const { + return data+size(); + } + Lit* getDataEnd () { + return data+size(); + } + void print(FILE* to = stdout) { + plainPrint(to); + fprintf(to, "c clause learnt %s group %d act %d oldAct %f\n", (learnt() ? "yes" : "no"), getGroup(), activity(), oldActivity()); + } + void plainPrint(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"); + } + #ifdef STATS_NEEDED + const uint32_t getGroup() const + { + return group; + } + void setGroup(const uint32_t _group) + { + group = _group; + } + #else + const uint getGroup() const + { + return 0; + } + void setGroup(const uint32_t _group) + { + return; + } + #endif //STATS_NEEDED + void setRemoved() { + isRemoved = true; + } + + const bool removed() const { + return isRemoved; + } + #ifdef USE_POOLS + const bool wasTriOriginally() const + { + return wasTriOriginallyInt; + } + const bool wasBinOriginally() const + { + return wasBinOriginallyInt; + } + #ifdef USE_4POOLS + const bool wasQuadOriginally() const + { + return wasQuadOriginallyInt; + } + #endif //USE_4POOLS + void setAllocSize() + { + wasTriOriginallyInt = false; + wasBinOriginallyInt = false; + #ifdef USE_4POOLS + wasQuadOriginallyInt = false; + #endif //USE_4POOLS + switch(size()) { + case 2: + wasBinOriginallyInt = true; + break; + case 3: + wasTriOriginallyInt = true; + break; + #ifdef USE_4POOLS + case 4: + wasQuadOriginallyInt = true; + break; + case 5: + wasQuadOriginallyInt = true; + break; + #endif //USE_4POOLS + } + } + #endif //USE_POOLS +}; + +class XorClause : public Clause +{ + +#ifdef _MSC_VER +public: +#else //_MSC_VER +protected: +#endif //_MSC_VER + + // 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) + { + invertedXor = inverted; + isXorClause = true; + calcXorAbstraction(); + } + +public: + #ifndef _MSC_VER + // -- use this function instead: + template + friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group); + #endif //_MSC_VER + + inline bool xor_clause_inverted() const + { + return invertedXor; + } + inline void invert(bool b) + { + invertedXor ^= b; + } + void calcXorAbstraction() { + extra.abst = 0; + for (uint32_t i = 0; i != size(); i++) + extra.abst |= 1 << (data[i].var() & 31); + } + + void print() { + printf("XOR Clause group: %d, size: %d, learnt:%d, lits:\"", getGroup(), size(), learnt()); + plainPrint(); + } + + void plainPrint(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; +}; + +#ifdef USE_POOLS +extern boost::pool<> clausePoolTri; +extern boost::pool<> clausePoolBin; +#ifdef USE_4POOLS +extern boost::pool<> clausePoolQuad; +#endif //USE_4POOLS +#endif //USE_POOLS + +template +inline void* allocEnough(const T& ps) +{ + void* mem; + switch(ps.size()) { + #ifdef USE_POOLS + case 2: + mem = clausePoolBin.malloc(); + break; + case 3: + mem = clausePoolTri.malloc(); + break; + #ifdef USE_4POOLS + case 4: + mem = clausePoolQuad.malloc(); + break; + case 5: + mem = clausePoolQuad.malloc(); + break; + #endif //USE_4POOLS + #endif //USE_POOLS + default: + mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + break; + } + + return mem; +} + +template +Clause* Clause_new(const T& ps, const uint group, const bool learnt = false) +{ + void* mem = allocEnough(ps); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} + +template +XorClause* XorClause_new(const T& ps, const bool inverted, const uint group) +{ + void* mem = allocEnough(ps); + XorClause* real= new (mem) XorClause(ps, inverted, group); + return real; +} + +inline Clause* Clause_new(Clause& c) +{ + void* mem = allocEnough(c); + //Clause* real= new (mem) Clause(ps, group, learnt); + memcpy(mem, &c, sizeof(Clause)+sizeof(Lit)*c.size()); + Clause& c2 = *(Clause*)mem; + #ifdef USE_POOLS + c2.setAllocSize(); + #endif //USE_POOLS + + return &c2; +} + +inline void clauseFree(Clause* c) +{ + #ifdef USE_POOLS + if (c->wasTriOriginally()) + clausePoolTri.free(c); + else if (c->wasBinOriginally()) + clausePoolBin.free(c); + #ifdef USE_4POOLS + else if (c->wasQuadOriginally()) + clausePoolQuad.free(c); + #endif //USE_4POOLS + else + #endif //USE_POOLS + free(c); +} + +#ifdef _MSC_VER +typedef Clause* ClausePtr; +typedef XorClause* XorClausePtr; +#else +typedef sptr ClausePtr; +typedef sptr XorClausePtr; +#endif //_MSC_VER + +#pragma pack(push) +#pragma pack(1) +class WatchedBin { + public: + WatchedBin(Clause *_clause, Lit _impliedLit) : clause(_clause), impliedLit(_impliedLit) {}; + ClausePtr clause; + Lit impliedLit; +}; + +class Watched { + public: + Watched(Clause *_clause, Lit _blockedLit) : clause(_clause), blockedLit(_blockedLit) {}; + ClausePtr clause; + Lit blockedLit; +}; +#pragma pack(pop) + +}; //NAMESPACE MINISAT + +#endif //CLAUSE_H diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index e69de29..42ff1a6 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -0,0 +1,421 @@ +/*********************************************************************************** +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 "ClauseCleaner.h" +#include "VarReplacer.h" + +#ifdef _MSC_VER +#define __builtin_prefetch(a,b,c) +#endif //_MSC_VER + +//#define DEBUG_CLEAN +//#define VERBOSE_DEBUG + +namespace MINISAT +{ +using namespace MINISAT; + +ClauseCleaner::ClauseCleaner(Solver& _solver) : + solver(_solver) +{ + for (uint i = 0; i < 6; i++) { + lastNumUnitarySat[i] = solver.get_unitary_learnts_num(); + lastNumUnitaryClean[i] = solver.get_unitary_learnts_num(); + } +} + +void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, const uint limit) +{ + #ifdef DEBUG_CLEAN + assert(solver.decisionLevel() == 0); + #endif + + if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num()) + return; + + uint32_t i,j; + for (i = j = 0; i < cs.size(); i++) { + if (satisfied(*cs[i])) + solver.removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); + + lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); +} + +void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, const uint limit) +{ + #ifdef DEBUG_CLEAN + assert(solver.decisionLevel() == 0); + #endif + + if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num()) + return; + + Clause **i,**j, **end; + for (i = j = cs.getData(), end = i + cs.size(); i != end; i++) { + if (i+1 != end) + __builtin_prefetch(*(i+1), 0, 0); + if (satisfied(**i)) + solver.removeClause(**i); + else + *j++ = *i; + } + cs.shrink(i - j); + + lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); +} + +void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type, const uint limit) +{ + assert(solver.decisionLevel() == 0); + assert(solver.qhead == solver.trail.size()); + + if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num()) + return; + + #ifdef VERBOSE_DEBUG + std::cout << "Cleaning " << (type==binaryClauses ? "binaryClauses" : "normal clauses" ) << std::endl; + #endif //VERBOSE_DEBUG + + Clause **s, **ss, **end; + for (s = ss = cs.getData(), end = s + cs.size(); s != end;) { + if (s+1 != end) + __builtin_prefetch(*(s+1), 1, 0); + if (cleanClause(*s)) { + clauseFree(*s); + s++; + } else if (type != ClauseCleaner::binaryClauses && (*s)->size() == 2) { + solver.binaryClauses.push(*s); + solver.becameBinary++; + s++; + } else { + *ss++ = *s++; + } + } + cs.shrink(s-ss); + + lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); + + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(Clause) useful ?? Removed: " << s-ss << endl; + #endif +} + +inline const bool ClauseCleaner::cleanClause(Clause*& cc) +{ + Clause& c = *cc; + + Lit origLit1 = c[0]; + Lit origLit2 = c[1]; + uint32_t origSize = c.size(); + + Lit *i, *j, *end; + for (i = j = c.getData(), end = i + c.size(); i != end; i++) { + lbool val = solver.value(*i); + if (val == l_Undef) { + *j++ = *i; + continue; + } + + if (val == l_True) { + solver.detachModifiedClause(origLit1, origLit2, origSize, &c); + return true; + } + } + c.shrink(i-j); + + if (i != j) { + c.setStrenghtened(); + if (c.size() == 2) { + solver.detachModifiedClause(origLit1, origLit2, origSize, &c); + Clause *c2 = Clause_new(c); + clauseFree(&c); + cc = c2; + solver.attachClause(*c2); + /*} else if (c.size() == 3) { + solver.detachModifiedClause(origLit1, origLit2, origSize, &c); + Clause *c2 = Clause_new(c); + clauseFree(&c); + cc = c2; + solver.attachClause(*c2);*/ + } else { + if (c.learnt()) + solver.learnts_literals -= i-j; + else + solver.clauses_literals -= i-j; + } + } + + return false; +} + +void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type, const uint limit) +{ + assert(solver.decisionLevel() == 0); + assert(solver.qhead == solver.trail.size()); + + if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num()) + return; + + XorClause **s, **ss, **end; + for (s = ss = cs.getData(), end = s + cs.size(); s != end; s++) { + if (s+1 != end) + __builtin_prefetch(*(s+1), 1, 0); + + #ifdef DEBUG_ATTACH + assert(find(solver.xorwatches[(**s)[0].var()], *s)); + assert(find(solver.xorwatches[(**s)[1].var()], *s)); + if (solver.assigns[(**s)[0].var()]!=l_Undef || solver.assigns[(**s)[1].var()]!=l_Undef) { + satisfied(**s); + } + #endif //DEBUG_ATTACH + + if (cleanClause(**s)) { + solver.freeLater.push(*s); + (*s)->setRemoved(); + } else { + #ifdef DEBUG_ATTACH + assert(find(solver.xorwatches[(**s)[0].var()], *s)); + assert(find(solver.xorwatches[(**s)[1].var()], *s)); + #endif //DEBUG_ATTACH + *ss++ = *s; + } + } + cs.shrink(s-ss); + + lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); + + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(XorClause) useful: ?? Removed: " << s-ss << endl; + #endif +} + +inline const bool ClauseCleaner::cleanClause(XorClause& c) +{ + Lit *i, *j, *end; + Var origVar1 = c[0].var(); + Var origVar2 = c[1].var(); + uint32_t origSize = c.size(); + for (i = j = c.getData(), end = i + c.size(); i != end; i++) { + const lbool& val = solver.assigns[i->var()]; + if (val.isUndef()) { + *j = *i; + j++; + } else c.invert(val.getBool()); + } + c.shrink(i-j); + + assert(c.size() != 1); + switch (c.size()) { + case 0: { + solver.detachModifiedClause(origVar1, origVar2, origSize, &c); + return true; + } + case 2: { + c[0] = c[0].unsign(); + c[1] = c[1].unsign(); + solver.varReplacer->replace(c, c.xor_clause_inverted(), c.getGroup()); + solver.detachModifiedClause(origVar1, origVar2, origSize, &c); + return true; + } + default: { + if (i-j > 0) { + c.setStrenghtened(); + solver.clauses_literals -= i-j; + } + return false; + } + } + + assert(false); + return false; +} + +void ClauseCleaner::cleanClausesBewareNULL(vec& cs, ClauseCleaner::ClauseSetType type, Subsumer& subs, const uint limit) +{ + assert(solver.decisionLevel() == 0); + assert(solver.qhead == solver.trail.size()); + + if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num()) + return; + + ClauseSimp *s, *end; + for (s = cs.getData(), end = s + cs.size(); s != end; s++) { + if (s+1 != end) + __builtin_prefetch((s+1)->clause, 1, 0); + if (s->clause == NULL) + continue; + + if (cleanClauseBewareNULL(*s, subs)) { + continue; + } else if (s->clause->size() == 2) + solver.becameBinary++; + } + + lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); +} + +inline const bool ClauseCleaner::cleanClauseBewareNULL(ClauseSimp cc, Subsumer& subs) +{ + Clause& c = *cc.clause; + vec origClause(c.size()); + memcpy(origClause.getData(), c.getData(), sizeof(Lit)*c.size()); + + Lit *i, *j, *end; + for (i = j = c.getData(), end = i + c.size(); i != end; i++) { + lbool val = solver.value(*i); + if (val == l_Undef) { + *j++ = *i; + continue; + } + + if (val == l_True) { + subs.unlinkModifiedClause(origClause, cc); + clauseFree(cc.clause); + return true; + } + } + + if (i != j) { + c.setStrenghtened(); + if (origClause.size() > 2 && origClause.size()-(i-j) == 2) { + subs.unlinkModifiedClause(origClause, cc); + subs.clauses[cc.index] = cc; + c.shrink(i-j); + solver.attachClause(c); + subs.linkInAlreadyClause(cc); + } else { + c.shrink(i-j); + subs.unlinkModifiedClauseNoDetachNoNULL(origClause, cc); + subs.linkInAlreadyClause(cc); + if (c.learnt()) + solver.learnts_literals -= i-j; + else + solver.clauses_literals -= i-j; + } + c.calcAbstraction(); + subs.updateClause(cc); + } + + return false; +} + +void ClauseCleaner::cleanXorClausesBewareNULL(vec& cs, ClauseCleaner::ClauseSetType type, XorSubsumer& subs, const uint limit) +{ + assert(solver.decisionLevel() == 0); + assert(solver.qhead == solver.trail.size()); + + if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num()) + return; + + XorClauseSimp *s, *end; + for (s = cs.getData(), end = s + cs.size(); s != end; s++) { + if (s+1 != end) + __builtin_prefetch((s+1)->clause, 1, 0); + if (s->clause == NULL) + continue; + + cleanXorClauseBewareNULL(*s, subs); + } + + lastNumUnitaryClean[type] = solver.get_unitary_learnts_num(); +} + +inline const bool ClauseCleaner::cleanXorClauseBewareNULL(XorClauseSimp cc, XorSubsumer& subs) +{ + XorClause& c = *cc.clause; + vec origClause(c.size()); + memcpy(origClause.getData(), c.getData(), sizeof(Lit)*c.size()); + + Lit *i, *j, *end; + for (i = j = c.getData(), end = i + c.size(); i != end; i++) { + const lbool& val = solver.assigns[i->var()]; + if (val.isUndef()) { + *j = *i; + j++; + } else c.invert(val.getBool()); + } + c.shrink(i-j); + + switch(c.size()) { + case 0: { + subs.unlinkModifiedClause(origClause, cc); + clauseFree(cc.clause); + return true; + } + case 2: { + vec ps(2); + ps[0] = c[0].unsign(); + ps[1] = c[1].unsign(); + solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.getGroup()); + subs.unlinkModifiedClause(origClause, cc); + clauseFree(cc.clause); + return true; + } + default: + if (i-j > 0) { + subs.unlinkModifiedClauseNoDetachNoNULL(origClause, cc); + subs.linkInAlreadyClause(cc); + c.calcXorAbstraction(); + } + } + + return false; +} + +bool ClauseCleaner::satisfied(const Clause& c) const +{ + for (uint i = 0; i != c.size(); i++) + if (solver.value(c[i]) == l_True) + return true; + return false; +} + +bool ClauseCleaner::satisfied(const XorClause& c) const +{ + bool final = c.xor_clause_inverted(); + for (uint k = 0; k != c.size(); k++ ) { + const lbool& val = solver.assigns[c[k].var()]; + if (val.isUndef()) return false; + final ^= val.getBool(); + } + return final; +} + +void ClauseCleaner::moveBinClausesToBinClauses() +{ + assert(solver.decisionLevel() == 0); + assert(solver.qhead == solver.trail.size()); + + vec& cs = solver.clauses; + Clause **s, **ss, **end; + for (s = ss = cs.getData(), end = s + cs.size(); s != end; s++) { + if (s+1 != end) + __builtin_prefetch(*(s+1), 1, 0); + + if ((**s).size() == 2) + solver.binaryClauses.push(*s); + else + *ss++ = *s; + } + cs.shrink(s-ss); +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/ClauseCleaner.h b/src/sat/cryptominisat2/ClauseCleaner.h index e69de29..d4c2adf 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.h +++ b/src/sat/cryptominisat2/ClauseCleaner.h @@ -0,0 +1,81 @@ +/*********************************************************************************** +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 CLAUSECLEANER_H +#define CLAUSECLEANER_H + +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "Solver.h" +#include "Subsumer.h" +#include "XorSubsumer.h" + +namespace MINISAT +{ +using namespace MINISAT; + +class ClauseCleaner +{ + public: + ClauseCleaner(Solver& solver); + + enum ClauseSetType {clauses, xorclauses, learnts, binaryClauses, simpClauses, xorSimpClauses}; + + void cleanClauses(vec& cs, ClauseSetType type, const uint limit = 0); + void cleanClausesBewareNULL(vec& cs, ClauseSetType type, Subsumer& subs, const uint limit = 0); + void cleanXorClausesBewareNULL(vec& cs, ClauseSetType type, XorSubsumer& subs, const uint limit = 0); + const bool cleanClauseBewareNULL(ClauseSimp c, Subsumer& subs); + const bool cleanXorClauseBewareNULL(XorClauseSimp c, XorSubsumer& subs); + + void cleanClauses(vec& cs, ClauseSetType type, const uint limit = 0); + void removeSatisfied(vec& cs, ClauseSetType type, const uint limit = 0); + void removeSatisfied(vec& cs, ClauseSetType type, const uint limit = 0); + void removeAndCleanAll(const bool nolimit = false); + bool satisfied(const Clause& c) const; + bool satisfied(const XorClause& c) const; + + void moveBinClausesToBinClauses(); + + private: + const bool cleanClause(XorClause& c); + const bool cleanClause(Clause*& c); + + uint lastNumUnitarySat[6]; + uint lastNumUnitaryClean[6]; + + Solver& solver; +}; + +inline void ClauseCleaner::removeAndCleanAll(const bool nolimit) +{ + //uint limit = std::min((uint)((double)solver.order_heap.size() * PERCENTAGECLEANCLAUSES), FIXCLEANREPLACE); + uint limit = (double)solver.order_heap.size() * PERCENTAGECLEANCLAUSES; + if (nolimit) limit = 0; + + removeSatisfied(solver.binaryClauses, ClauseCleaner::binaryClauses, limit); + cleanClauses(solver.clauses, ClauseCleaner::clauses, limit); + cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses, limit); + cleanClauses(solver.learnts, ClauseCleaner::learnts, limit); +} + +}; //NAMESPACE MINISAT + +#endif //CLAUSECLEANER_H diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index e69de29..96855d7 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -0,0 +1,526 @@ +/*********************************************************************************** +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 "Conglomerate.h" +#include "VarReplacer.h" +#include "ClauseCleaner.h" + +#include +#include +#include +#include "time_mem.h" +#include +using std::make_pair; + +//#define VERBOSE_DEBUG + +#ifdef VERBOSE_DEBUG +#include +using std::cout; +using std::endl; +#endif + +namespace MINISAT +{ +using namespace MINISAT; + +Conglomerate::Conglomerate(Solver& _solver) : + found(0) + , solver(_solver) +{} + +Conglomerate::~Conglomerate() +{ + for(uint i = 0; i < calcAtFinish.size(); i++) + free(calcAtFinish[i]); +} + +void Conglomerate::blockVars() +{ + for (Clause *const*it = solver.clauses.getData(), *const*end = it + solver.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 (Clause *const*it = solver.binaryClauses.getData(), *const*end = it + solver.binaryClauses.size(); it != end; it++) { + const Clause& c = **it; + blocked[c[0].var()] = true; + blocked[c[1].var()] = true; + } + + for (Lit* it = &(solver.trail[0]), *end = it + solver.trail.size(); it != end; it++) + blocked[it->var()] = true; + + const vec& clauses = solver.varReplacer->getClauses(); + for (Clause *const*it = clauses.getData(), *const*end = it + 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; + } + } +} + +void Conglomerate::fillVarToXor() +{ + varToXor.clear(); + + uint i = 0; + for (XorClause* const* it = solver.xorclauses.getData(), *const*end = it + solver.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::removeVar(const Var var) +{ + solver.activity[var] = 0.0; + solver.order_heap.update(var); + removedVars[var] = true; + if (solver.decision_var[var]) { + madeVarNonDecision.push(var); + solver.setDecisionVar(var, false); + } + found++; +} + +void Conglomerate::processClause(XorClause& x, uint32_t num, Var remove_var) +{ + for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) { + Var var = a->var(); + if (var != remove_var) { + varToXorMap::iterator finder = varToXor.find(var); + if (finder != varToXor.end()) { + vector >::iterator it = + std::find(finder->second.begin(), finder->second.end(), make_pair(&x, num)); + finder->second.erase(it); + } + } + } +} + +const bool Conglomerate::heuleProcessFull() +{ + #ifdef VERBOSE_DEBUG + cout << "Heule XOR-ing started" << endl; + #endif + + double time = cpuTime(); + found = 0; + uint oldToReplaceVars = solver.varReplacer->getNewToReplaceVars(); + solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); + if (solver.ok == false) + return false; + + toRemove.clear(); + toRemove.resize(solver.xorclauses.size(), false); + blocked.clear(); + blocked.resize(solver.nVars(), false); + fillVarToXor(); + if (!heuleProcess()) + goto end; + + if (solver.verbosity >=1) { + std::cout << "c | Heule-processings XORs:" << std::setw(8) << std::setprecision(2) << std::fixed << cpuTime()-time + << " Found smaller XOR-s: " << std::setw(6) << found + << " New bin anti/eq-s: " << std::setw(3) << solver.varReplacer->getNewToReplaceVars() - oldToReplaceVars + << std::setw(0) << " |" << std::endl; + } + +end: + + clearToRemove(); + + return solver.ok; +} + +const bool Conglomerate::conglomerateXorsFull() +{ + #ifdef VERBOSE_DEBUG + cout << "Finding conglomerate xors started" << endl; + #endif + + double time = cpuTime(); + found = 0; + uint32_t origNumClauses = solver.xorclauses.size(); + + solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); + if (solver.ok == false) + return false; + + toRemove.clear(); + toRemove.resize(solver.xorclauses.size(), false); + blocked.clear(); + blocked.resize(solver.nVars(), false); + blockVars(); + fillVarToXor(); + if (conglomerateXors() == false) + goto end; + +end: + + clearToRemove(); + assert(origNumClauses >= solver.xorclauses.size()); + if (solver.verbosity >=1) { + std::cout << "c | Conglomerating XORs:" << std::setw(8) << std::setprecision(2) << std::fixed << cpuTime()-time << " s " + << " removed " << std::setw(8) << found << " vars" + << " removed " << std::setw(8) << origNumClauses-solver.xorclauses.size() << " clauses" + << std::setw(0) << " |" << std::endl; + } + + clearLearntsFromToRemove(); + solver.order_heap.filter(Solver::VarFilter(solver)); + + return solver.ok; +} + +void Conglomerate::fillNewSet(vector >& newSet, vector >& clauseSet) const +{ + newSet.clear(); + newSet.resize(clauseSet.size()); + + XorClause& firstXorClause = *(clauseSet[0].first); + newSet[0].resize(firstXorClause.size()); + memcpy(&newSet[0][0], firstXorClause.getData(), sizeof(Lit)*firstXorClause.size()); + + for (uint i = 1; i < clauseSet.size(); i++) { + XorClause& thisXorClause = *clauseSet[i].first; + newSet[i] = newSet[0]; + newSet[i].resize(firstXorClause.size()+thisXorClause.size()); + memcpy(&newSet[i][firstXorClause.size()], thisXorClause.getData(), sizeof(Lit)*thisXorClause.size()); + clearDouble(newSet[i]); + } +} + +const bool Conglomerate::heuleProcess() +{ + vector > newSet; + while(varToXor.begin() != varToXor.end()) { + varToXorMap::iterator it = varToXor.begin(); + vector >& clauseSet = it->second; + const Var var = it->first; + + if (blocked[var] || clauseSet.size() == 1) { + varToXor.erase(it); + blocked[var] = true; + continue; + } + blocked[var] = true; + + std::sort(clauseSet.begin(), clauseSet.end(), ClauseSetSorter()); + fillNewSet(newSet, clauseSet); + + for (uint i = 1; i < newSet.size(); i++) if (newSet[i].size() <= 2) { + found++; + XorClause& thisXorClause = *clauseSet[i].first; + const bool inverted = !clauseSet[0].first->xor_clause_inverted() ^ thisXorClause.xor_clause_inverted(); + const uint old_group = thisXorClause.getGroup(); + + #ifdef VERBOSE_DEBUG + cout << "- XOR1:"; + clauseSet[0].first->plainPrint(); + cout << "- XOR2:"; + thisXorClause.plainPrint(); + #endif + + if (!dealWithNewClause(newSet[i], inverted, old_group)) + return false; + assert(newSet.size() == clauseSet.size()); + } + + varToXor.erase(it); + } + + return (solver.ok = (solver.propagate() == NULL)); +} + +const bool Conglomerate::conglomerateXors() +{ + vector > newSet; + while(varToXor.begin() != varToXor.end()) { + varToXorMap::iterator it = varToXor.begin(); + vector >& clauseSet = it->second; + const Var var = it->first; + + //We blocked the var during dealWithNewClause (it was in a 2-long xor-clause) + if (blocked[var]) { + varToXor.erase(it); + continue; + } + + if (clauseSet.size() == 0) { + removeVar(var); + varToXor.erase(it); + continue; + } + + std::sort(clauseSet.begin(), clauseSet.end(), ClauseSetSorter()); + fillNewSet(newSet, clauseSet); + + int diff = 0; + for (size_t i = 1; i < newSet.size(); i++) + diff += (int)newSet[i].size()-(int)clauseSet[i].first->size(); + + if (newSet.size() > 2) { + blocked[var] = true; + varToXor.erase(it); + continue; + } + + XorClause& firstXorClause = *(clauseSet[0].first); + bool first_inverted = !firstXorClause.xor_clause_inverted(); + removeVar(var); + + #ifdef VERBOSE_DEBUG + cout << "--- New conglomerate set ---" << endl; + cout << "- Removing: "; + firstXorClause.plainPrint(); + cout << "Adding var " << var+1 << " to calcAtFinish" << endl; + #endif + + assert(!toRemove[clauseSet[0].second]); + toRemove[clauseSet[0].second] = true; + processClause(firstXorClause, clauseSet[0].second, var); + solver.detachClause(firstXorClause); + calcAtFinish.push(&firstXorClause); + + for (uint i = 1; i < clauseSet.size(); i++) { + XorClause& thisXorClause = *clauseSet[i].first; + #ifdef VERBOSE_DEBUG + cout << "- Removing: "; + thisXorClause.plainPrint(); + #endif + + const uint old_group = thisXorClause.getGroup(); + const bool inverted = first_inverted ^ thisXorClause.xor_clause_inverted(); + assert(!toRemove[clauseSet[i].second]); + toRemove[clauseSet[i].second] = true; + processClause(thisXorClause, clauseSet[i].second, var); + solver.removeClause(thisXorClause); + + if (!dealWithNewClause(newSet[i], inverted, old_group)) + return false; + assert(newSet.size() == clauseSet.size()); + } + + varToXor.erase(it); + } + + return (solver.ok = (solver.propagate() == NULL)); +} + +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) { + solver.ok = false; + return false; + } + break; + } + case 1: { + #ifdef VERBOSE_DEBUG + cout << "--> xor is 1-long, attempting to set variable " << ps[0].var()+1 << endl; + #endif + + if (solver.assigns[ps[0].var()] == l_Undef) { + assert(solver.decisionLevel() == 0); + blocked[ps[0].var()] = true; + solver.uncheckedEnqueue(Lit(ps[0].var(), inverted)); + } else if (solver.assigns[ps[0].var()] != boolToLBool(!inverted)) { + #ifdef VERBOSE_DEBUG + cout << "Conflict. Aborting."; + #endif + solver.ok = false; + return false; + } else { + #ifdef VERBOSE_DEBUG + cout << "Variable already set to correct value"; + #endif + } + break; + } + + case 2: { + #ifdef VERBOSE_DEBUG + cout << "--> xor is 2-long, must later replace variable" << endl; + XorClause* newX = XorClause_new(ps, inverted, old_group); + newX->plainPrint(); + free(newX); + #endif + + vec tmpPS(2); + tmpPS[0] = ps[0]; + tmpPS[1] = ps[1]; + if (solver.varReplacer->replace(tmpPS, inverted, old_group) == false) + return false; + blocked[ps[0].var()] = true; + blocked[ps[1].var()] = true; + break; + } + + default: { + XorClause* newX = XorClause_new(ps, inverted, old_group); + + #ifdef VERBOSE_DEBUG + cout << "- Adding: "; + newX->plainPrint(); + #endif + + solver.xorclauses.push(newX); + toRemove.push_back(false); + solver.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, (uint32_t)(toRemove.size()-1))); + } + break; + } + } + + return true; +} + +void Conglomerate::clearDouble(vector& ps) const +{ + std::sort(ps.begin(), ps.end()); + Lit p; + uint32_t i, j; + for (i = j = 0, p = lit_Undef; i != ps.size(); i++) { + ps[i] = ps[i].unsign(); + if (ps[i] == p) { + //added, but easily removed + j--; + p = lit_Undef; + } else + ps[j++] = p = ps[i]; + } + ps.resize(ps.size() - (i - j)); +} + +void Conglomerate::clearToRemove() +{ + assert(toRemove.size() == solver.xorclauses.size()); + + XorClause **a = solver.xorclauses.getData(); + XorClause **r = a; + XorClause **end = a + solver.xorclauses.size(); + for (uint i = 0; r != end; i++) { + if (!toRemove[i]) + *a++ = *r++; + else { + r++; + } + } + solver.xorclauses.shrink(r-a); +} + +void Conglomerate::clearLearntsFromToRemove() +{ + Clause **a = solver.learnts.getData(); + Clause **r = a; + Clause **end = a + solver.learnts.size(); + for (; r != end;) { + const Clause& c = **r; + bool inside = false; + if (!solver.locked(c)) { + for (uint i = 0; i < c.size(); i++) { + if (removedVars[c[i].var()]) { + inside = true; + break; + } + } + } + if (!inside) + *a++ = *r++; + else { + solver.removeClause(**r); + r++; + } + } + solver.learnts.shrink(r-a); +} + +void Conglomerate::extendModel(Solver& solver2) +{ + #ifdef VERBOSE_DEBUG + cout << "Executing doCalcAtFinish" << endl; + #endif + + vec ps; + for (int i = (int)(calcAtFinish.size())-1; i >= 0; i--) { + XorClause& c = *calcAtFinish[i]; + assert(c.size() > 2); + + ps.clear(); + for (Lit *l = c.getData(), *end = c.getDataEnd(); l != end; l++) { + ps.push(l->unsign()); + } + + solver2.addXorClause(ps, c.xor_clause_inverted(), c.getGroup()); + assert(solver2.ok); + } +} + +const bool Conglomerate::addRemovedClauses() +{ + #ifdef VERBOSE_DEBUG + cout << "Executing addRemovedClauses" << endl; + #endif + + for(XorClause **it = calcAtFinish.getData(), **end = calcAtFinish.getDataEnd(); it != end; it++) + { + XorClause& c = **it; + #ifdef VERBOSE_DEBUG + cout << "readding already removed (conglomerated) clause: "; + c.plainPrint(); + #endif + + for(Lit *l = c.getData(), *end2 = c.getDataEnd(); l != end2 ; l++) + *l = l->unsign(); + + FILE* backup_libraryCNFfile = solver.libraryCNFFile; + solver.libraryCNFFile = NULL; + if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) { + for (;it != end; it++) free(*it); + calcAtFinish.clear(); + return false; + } + solver.libraryCNFFile = backup_libraryCNFfile; + free(&c); + } + calcAtFinish.clear(); + + std::fill(removedVars.getData(), removedVars.getDataEnd(), false); + for (Var *v = madeVarNonDecision.getData(), *end = madeVarNonDecision.getDataEnd(); v != end; v++) { + solver.setDecisionVar(*v, true); + } + madeVarNonDecision.clear(); + + return true; +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h index e69de29..50972d4 100644 --- a/src/sat/cryptominisat2/Conglomerate.h +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -0,0 +1,125 @@ +/*********************************************************************************** +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 CONGLOMERATE_H +#define CONGLOMERATE_H + +#include +#include +#include +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "Clause.h" +#include "VarReplacer.h" +#include "Solver.h" + +using std::vector; +using std::pair; +using std::map; +using std::set; + +namespace MINISAT +{ +using namespace MINISAT; + +class Solver; + +class Conglomerate +{ +public: + Conglomerate(Solver& solver); + ~Conglomerate(); + const bool conglomerateXorsFull(); + const bool heuleProcessFull(); + const bool addRemovedClauses(); ///& getCalcAtFinish() const; + vec& getCalcAtFinish(); + const vec& getRemovedVars() const; + const bool needCalcAtFinish() const; + + void newVar(); + +private: + + struct ClauseSetSorter { + bool operator () (const pair& a, const pair& b) { + return a.first->size() < b.first->size(); + } + }; + + const bool conglomerateXors(); + const bool heuleProcess(); + + void fillNewSet(vector >& newSet, vector >& clauseSet) const; + + void removeVar(const Var var); + void processClause(XorClause& x, uint32_t num, Var remove_var); + void blockVars(); + void fillVarToXor(); + void clearDouble(vector& ps) const; + void clearToRemove(); + void clearLearntsFromToRemove(); + bool dealWithNewClause(vector& ps, const bool inverted, const uint old_group); + + typedef map > > varToXorMap; + varToXorMap varToXor; + vector blocked; + vector toRemove; + + vec removedVars; + vec madeVarNonDecision; + + vec calcAtFinish; + uint found; + + Solver& solver; +}; + +inline void Conglomerate::newVar() +{ + removedVars.push(false); +} + +inline const vec& Conglomerate::getRemovedVars() const +{ + return removedVars; +} + +inline const vec& Conglomerate::getCalcAtFinish() const +{ + return calcAtFinish; +} + +inline vec& Conglomerate::getCalcAtFinish() +{ + return calcAtFinish; +} + +inline const bool Conglomerate::needCalcAtFinish() const +{ + return calcAtFinish.size(); +} + +}; //NAMESPACE MINISAT + +#endif //CONGLOMERATE_H diff --git a/src/sat/cryptominisat2/DoublePackedRow.h b/src/sat/cryptominisat2/DoublePackedRow.h index e69de29..50cfd8a 100644 --- a/src/sat/cryptominisat2/DoublePackedRow.h +++ b/src/sat/cryptominisat2/DoublePackedRow.h @@ -0,0 +1,173 @@ +/*********************************************************************************** +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 DOUBLEPACKEDROW_H +#define DOUBLEPACKEDROW_H + +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include + +#include "SolverTypes.h" + +namespace MINISAT +{ +using namespace MINISAT; + +class DoublePackedRow +{ + private: + class BitIter { + public: + inline void operator=(const lbool toSet) + { + val &= ~((unsigned char)3 << offset); + val |= toSet.value << offset; + } + + inline operator lbool() const + { + return lbool((val >> offset) & 3); + } + + inline const bool isUndef() const { + return ((lbool)*this).isUndef(); + } + inline const bool isDef() const { + return ((lbool)*this).isDef(); + } + inline const bool getBool() const { + return ((lbool)*this).getBool(); + } + inline const bool operator==(lbool b) const { + return ((lbool)*this) == b; + } + inline const bool operator!=(lbool b) const { + return ((lbool)*this) != b; + } + const lbool operator^(const bool b) const { + return ((lbool)*this) ^ b; + } + + private: + friend class DoublePackedRow; + inline BitIter(unsigned char& mp, const uint32_t _offset) : + val(mp) + , offset(_offset) + {} + + unsigned char& val; + const uint32_t offset; + }; + + class BitIterConst { + public: + inline operator lbool() const + { + return lbool((val >> offset) & 3); + } + + inline const bool isUndef() const { + return ((lbool)*this).isUndef(); + } + inline const bool isDef() const { + return ((lbool)*this).isDef(); + } + inline const bool getBool() const { + return ((lbool)*this).getBool(); + } + inline const bool operator==(lbool b) const { + return ((lbool)*this) == b; + } + inline const bool operator!=(lbool b) const { + return ((lbool)*this) != b; + } + const lbool operator^(const bool b) const { + return ((lbool)*this) ^ b; + } + + + private: + friend class DoublePackedRow; + inline BitIterConst(unsigned char& mp, const uint32_t _offset) : + val(mp) + , offset(_offset) + {} + + const unsigned char& val; + const uint32_t offset; + }; + + public: + DoublePackedRow() : + numElems(0) + , mp(NULL) + {} + + uint32_t size() const + { + return numElems; + } + + void growTo(const uint32_t newNumElems) + { + uint32_t oldSize = numElems/4 + (bool)(numElems % 4); + uint32_t newSize = newNumElems/4 + (bool)(newNumElems % 4); + + if (oldSize >= newSize) { + numElems = std::max(newNumElems, numElems); + return; + } + + mp = (unsigned char*)realloc(mp, newSize*sizeof(unsigned char)); + numElems = newNumElems; + } + + inline BitIter operator[](const uint32_t at) + { + return BitIter(mp[at/4], (at%4)*2); + } + + inline const BitIterConst operator[](const uint32_t at) const + { + return BitIterConst(mp[at/4], (at%4)*2); + } + + inline void push(const lbool val) + { + growTo(numElems+1); + (*this)[numElems-1] = val; + } + + /*void clear(const uint32_t at) + { + mp[at/32] &= ~((uint64_t)3 << ((at%32)*2)); + }*/ + + private: + + Var numElems; + unsigned char *mp; +}; + +}; //NAMESPACE MINISAT + +#endif //DOUBLEPACKEDROW_H diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp index e69de29..4b273f7 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.cpp +++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp @@ -0,0 +1,1045 @@ +/*********************************************************************************** +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 "FailedVarSearcher.h" + +#include +#include +#include +using std::make_pair; +using std::set; + +#include "Solver.h" +#include "ClauseCleaner.h" +#include "time_mem.h" +#include "VarReplacer.h" +#include "ClauseCleaner.h" +#include "StateSaver.h" + +#ifdef _MSC_VER +#define __builtin_prefetch(a,b,c) +#endif //_MSC_VER + +//#define VERBOSE_DEUBUG + +namespace MINISAT +{ +using namespace MINISAT; + +FailedVarSearcher::FailedVarSearcher(Solver& _solver): + solver(_solver) + , tmpPs(2) + , finishedLastTimeVar(true) + , lastTimeWentUntilVar(0) + , finishedLastTimeBin(true) + , lastTimeWentUntilBin(0) + , numPropsMultiplier(1.0) + , lastTimeFoundTruths(0) + , numCalls(0) +{ +} + +void FailedVarSearcher::addFromSolver(const vec< XorClause* >& cs) +{ + xorClauseSizes.clear(); + xorClauseSizes.growTo(cs.size()); + occur.resize(solver.nVars()); + for (Var var = 0; var < solver.nVars(); var++) { + occur[var].clear(); + } + + uint32_t i = 0; + for (XorClause * const*it = cs.getData(), * const*end = it + cs.size(); it != end; it++, i++) { + if (it+1 != end) + __builtin_prefetch(*(it+1), 0, 0); + + const XorClause& cl = **it; + xorClauseSizes[i] = cl.size(); + for (const Lit *l = cl.getData(), *end2 = l + cl.size(); l != end2; l++) { + occur[l->var()].push_back(i); + } + } +} + +inline void FailedVarSearcher::removeVarFromXors(const Var var) +{ + vector& occ = occur[var]; + if (occ.empty()) return; + + for (uint32_t *it = &occ[0], *end = it + occ.size(); it != end; it++) { + xorClauseSizes[*it]--; + if (!xorClauseTouched[*it]) { + xorClauseTouched.setBit(*it); + investigateXor.push(*it); + } + } +} + +inline void FailedVarSearcher::addVarFromXors(const Var var) +{ + vector& occ = occur[var]; + if (occ.empty()) return; + + for (uint32_t *it = &occ[0], *end = it + occ.size(); it != end; it++) { + xorClauseSizes[*it]++; + } +} + +const TwoLongXor FailedVarSearcher::getTwoLongXor(const XorClause& c) +{ + TwoLongXor tmp; + uint32_t num = 0; + tmp.inverted = c.xor_clause_inverted(); + + for(const Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + if (solver.assigns[l->var()] == l_Undef) { + assert(num < 2); + tmp.var[num] = l->var(); + num++; + } else { + tmp.inverted ^= (solver.assigns[l->var()] == l_True); + } + } + + #ifdef VERBOSE_DEUBUG + if (num != 2) { + std::cout << "Num:" << num << std::endl; + c.plainPrint(); + } + #endif + + std::sort(&tmp.var[0], &tmp.var[0]+2); + assert(num == 2); + return tmp; +} + +const bool FailedVarSearcher::search(uint64_t numProps) +{ + assert(solver.decisionLevel() == 0); + solver.testAllClauseAttach(); + double myTime = cpuTime(); + uint32_t origHeapSize = solver.order_heap.size(); + StateSaver savedState(solver); + Heap order_heap_copy(solver.order_heap); //for hyperbin + uint64_t origBinClauses = solver.binaryClauses.size(); + + if (solver.readdOldLearnts && !readdRemovedLearnts()) goto end; + + //General Stats + numFailed = 0; + goodBothSame = 0; + numCalls++; + + //If failed var searching is going good, do successively more and more of it + if (lastTimeFoundTruths > 500 || (double)lastTimeFoundTruths > (double)solver.order_heap.size() * 0.03) std::max(numPropsMultiplier*1.7, 5.0); + else numPropsMultiplier = 1.0; + numProps = (uint64_t) ((double)numProps * numPropsMultiplier *3); + + //For BothSame + propagated.resize(solver.nVars(), 0); + propValue.resize(solver.nVars(), 0); + + //For calculating how many variables have really been set + origTrailSize = solver.trail.size(); + + //For 2-long xor (rule 6 of Equivalent literal propagation in the DLL procedure by Chu-Min Li) + toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); + lastTrailSize = solver.trail.size(); + binXorFind = true; + twoLongXors.clear(); + if (solver.xorclauses.size() < 5 || + solver.xorclauses.size() > 30000 || + solver.order_heap.size() > 30000 || + solver.nClauses() > 100000) + binXorFind = false; + if (binXorFind) { + solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); + addFromSolver(solver.xorclauses); + } + xorClauseTouched.resize(solver.xorclauses.size(), 0); + newBinXor = 0; + + //For 2-long xor through Le Berre paper + bothInvert = 0; + + //For HyperBin + unPropagatedBin.resize(solver.nVars(), 0); + myimplies.resize(solver.nVars(), 0); + hyperbinProps = 0; + if (solver.addExtraBins && !orderLits()) return false; + maxHyperBinProps = numProps/8; + + //uint32_t fromBin; + uint32_t fromVar; + if (finishedLastTimeVar || lastTimeWentUntilVar >= solver.nVars()) + fromVar = 0; + else + fromVar = lastTimeWentUntilVar; + finishedLastTimeVar = true; + lastTimeWentUntilVar = solver.nVars(); + origProps = solver.propagations; + for (Var var = fromVar; var < solver.nVars(); var++) { + if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) + continue; + if (solver.propagations - origProps >= numProps) { + finishedLastTimeVar = false; + lastTimeWentUntilVar = var; + break; + } + if (!tryBoth(Lit(var, false), Lit(var, true))) + goto end; + } + + numProps = (double)numProps * 1.2; + hyperbinProps = 0; + while (!order_heap_copy.empty()) { + Var var = order_heap_copy.removeMin(); + if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) + continue; + if (solver.propagations - origProps >= numProps) { + finishedLastTimeVar = false; + lastTimeWentUntilVar = var; + break; + } + if (!tryBoth(Lit(var, false), Lit(var, true))) + goto end; + } + + /*if (solver.verbosity >= 1) printResults(myTime); + if (finishedLastTimeBin || lastTimeWentUntilBin >= solver.binaryClauses.size()) + fromBin = 0; + else + fromBin = lastTimeWentUntilBin; + finishedLastTimeBin = true; + lastTimeWentUntilBin = solver.nVars(); + for (uint32_t binCl = 0; binCl < solver.binaryClauses.size(); binCl++) { + if ((double)(solver.propagations - origProps) >= 1.1*(double)numProps) { + finishedLastTimeBin = false; + lastTimeWentUntilBin = binCl; + break; + } + + Clause& cl = *solver.binaryClauses[binCl]; + if (solver.value(cl[0]) == l_Undef && solver.value(cl[1]) == l_Undef) { + if (!tryBoth(cl[0], cl[1])) + goto end; + } + }*/ + + /*for (Clause **it = solver.clauses.getData(), **end = solver.clauses.getDataEnd(); it != end; it++) { + Clause& c = **it; + for (uint i = 0; i < c.size(); i++) { + if (solver.value(c[i]) != l_Undef) goto next; + } + if (!tryAll(c.getData(), c.getDataEnd())) + goto end; + + next:; + } + + for (Clause **it = solver.learnts.getData(), **end = solver.learnts.getDataEnd(); it != end; it++) { + Clause& c = **it; + for (uint i = 0; i < c.size(); i++) { + if (solver.value(c[i]) != l_Undef) goto next2; + } + if (!tryAll(c.getData(), c.getDataEnd())) + goto end; + + next2:; + }*/ + +end: + bool removedOldLearnts = false; + binClauseAdded = solver.binaryClauses.size() - origBinClauses; + //Print results + if (solver.verbosity >= 1) printResults(myTime); + + solver.order_heap.filter(Solver::VarFilter(solver)); + + if (solver.ok && (numFailed || goodBothSame)) { + double time = cpuTime(); + if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) { + completelyDetachAndReattach(); + removedOldLearnts = true; + } else { + solver.clauseCleaner->removeAndCleanAll(); + } + if (solver.verbosity >= 1 && numFailed + goodBothSame > 100) { + std::cout << "c | Cleaning up after failed var search: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime() - time << " s " + << std::setw(33) << " | " << std::endl; + } + } + + if (solver.ok && solver.readdOldLearnts && !removedOldLearnts) { + if (solver.removedLearnts.size() < 100000) { + removeOldLearnts(); + } else { + completelyDetachAndReattach(); + } + } + + lastTimeFoundTruths = solver.trail.size() - origTrailSize; + + savedState.restore(); + + solver.testAllClauseAttach(); + return solver.ok; +} + +void FailedVarSearcher::completelyDetachAndReattach() +{ + solver.clauses_literals = 0; + solver.learnts_literals = 0; + for (uint32_t i = 0; i < solver.nVars(); i++) { + solver.binwatches[i*2].clear(); + solver.binwatches[i*2+1].clear(); + solver.watches[i*2].clear(); + solver.watches[i*2+1].clear(); + solver.xorwatches[i].clear(); + } + solver.varReplacer->reattachInternalClauses(); + cleanAndAttachClauses(solver.binaryClauses); + cleanAndAttachClauses(solver.clauses); + cleanAndAttachClauses(solver.learnts); + cleanAndAttachClauses(solver.xorclauses); +} + +void FailedVarSearcher::printResults(const double myTime) const +{ + std::cout << "c | Flit: "<< std::setw(5) << numFailed << + " Blit: " << std::setw(6) << goodBothSame << + " bXBeca: " << std::setw(4) << newBinXor << + " bXProp: " << std::setw(4) << bothInvert << + " Bins:" << std::setw(7) << binClauseAdded << + " P: " << std::setw(4) << std::fixed << std::setprecision(1) << (double)(solver.propagations - origProps)/1000000.0 << "M" + " T: " << std::setw(5) << std::fixed << std::setprecision(2) << cpuTime() - myTime << + std::setw(5) << " |" << std::endl; +} + +const bool FailedVarSearcher::orderLits() +{ + uint64_t oldProps = solver.propagations; + double myTime = cpuTime(); + uint32_t numChecked = 0; + litDegrees.clear(); + litDegrees.resize(solver.nVars()*2, 0); + BitArray alreadyTested; + alreadyTested.resize(solver.nVars()*2, 0); + uint32_t i; + + for (i = 0; i < 3*solver.order_heap.size(); i++) { + if (solver.propagations - oldProps > 1500000) break; + Var var = solver.order_heap[solver.mtrand.randInt(solver.order_heap.size()-1)]; + if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue; + + Lit randLit(var, solver.mtrand.randInt(1)); + if (alreadyTested[randLit.toInt()]) continue; + alreadyTested.setBit(randLit.toInt()); + + numChecked++; + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(randLit); + failed = (solver.propagateBin() != NULL); + if (failed) { + solver.cancelUntil(0); + solver.uncheckedEnqueue(~randLit); + solver.ok = (solver.propagate() == NULL); + if (!solver.ok) return false; + continue; + } + assert(solver.decisionLevel() > 0); + for (int c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) { + Lit x = solver.trail[c]; + litDegrees[x.toInt()]++; + } + solver.cancelUntil(0); + } + std::cout << "c binary Degree finding time: " << cpuTime() - myTime << " s num checked: " << numChecked << " i: " << i << " props: " << (solver.propagations - oldProps) << std::endl; + solver.propagations = oldProps; + + return true; +} + +void FailedVarSearcher::removeOldLearnts() +{ + for (Clause **it = solver.removedLearnts.getData(), **end = solver.removedLearnts.getDataEnd(); it != end; it++) { + solver.detachClause(**it); + } +} + +struct reduceDB_ltOldLearnt +{ + bool operator () (const Clause* x, const Clause* y) { + return x->size() > y->size(); + } +}; + +const bool FailedVarSearcher::readdRemovedLearnts() +{ + uint32_t toRemove = (solver.removedLearnts.size() > MAX_OLD_LEARNTS) ? (solver.removedLearnts.size() - MAX_OLD_LEARNTS/4) : 0; + if (toRemove > 0) + std::sort(solver.removedLearnts.getData(), solver.removedLearnts.getDataEnd(), reduceDB_ltOldLearnt()); + + Clause **it1, **it2; + it1 = it2 = solver.removedLearnts.getData(); + for (Clause **end = solver.removedLearnts.getDataEnd(); it1 != end; it1++) { + if (toRemove > 0) { + clauseFree(*it1); + toRemove--; + continue; + } + + Clause* c = solver.addClauseInt(**it1, (**it1).getGroup()); + clauseFree(*it1); + if (c != NULL) { + *it2 = c; + it2++; + } + if (!solver.ok) { + it1++; + for (; it1 != end; it1++) clauseFree(*it1); + } + } + solver.removedLearnts.shrink(it1-it2); + //std::cout << "Readded old learnts. New facts:" << (int)origHeapSize - (int)solver.order_heap.size() << std::endl; + + return solver.ok; +} + +#define MAX_REMOVE_BIN_FULL_PROPS 20000000 +#define EXTRATIME_DIVIDER 3 + +template +const bool FailedVarSearcher::removeUslessBinFull() +{ + if (!solver.performReplace) return true; + while (solver.performReplace && solver.varReplacer->getClauses().size() > 0) { + if (!solver.varReplacer->performReplace(true)) return false; + solver.clauseCleaner->removeAndCleanAll(true); + } + assert(solver.varReplacer->getClauses().size() == 0); + solver.testAllClauseAttach(); + if (startUp) { + solver.clauseCleaner->moveBinClausesToBinClauses(); + } + + double myTime = cpuTime(); + toDeleteSet.clear(); + toDeleteSet.growTo(solver.nVars()*2, 0); + uint32_t origHeapSize = solver.order_heap.size(); + uint64_t origProps = solver.propagations; + bool fixed = false; + uint32_t extraTime = solver.binaryClauses.size() / EXTRATIME_DIVIDER; + + uint32_t startFrom = solver.mtrand.randInt(solver.order_heap.size()); + for (uint32_t i = 0; i != solver.order_heap.size(); i++) { + Var var = solver.order_heap[(i+startFrom)%solver.order_heap.size()]; + if (solver.propagations - origProps + extraTime > MAX_REMOVE_BIN_FULL_PROPS) break; + if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue; + + Lit lit(var, true); + if (!removeUselessBinaries(lit)) { + fixed = true; + solver.cancelUntil(0); + solver.uncheckedEnqueue(~lit); + solver.ok = (solver.propagate() == NULL); + if (!solver.ok) return false; + continue; + } + + lit = ~lit; + if (!removeUselessBinaries(lit)) { + fixed = true; + solver.cancelUntil(0); + solver.uncheckedEnqueue(~lit); + solver.ok = (solver.propagate() == NULL); + if (!solver.ok) return false; + continue; + } + } + + Clause **i, **j; + i = j = solver.binaryClauses.getData(); + uint32_t num = 0; + for (Clause **end = solver.binaryClauses.getDataEnd(); i != end; i++, num++) { + if (!(*i)->removed()) { + *j++ = *i; + } else { + clauseFree(*i); + } + } + uint32_t removedUselessBin = i - j; + solver.binaryClauses.shrink(i - j); + + if (fixed) solver.order_heap.filter(Solver::VarFilter(solver)); + + if (solver.verbosity >= 1) { + std::cout + << "c Removed useless bin:" << std::setw(8) << removedUselessBin + << " fixed: " << std::setw(4) << (origHeapSize - solver.order_heap.size()) + << " props: " << std::fixed << std::setprecision(2) << std::setw(4) << (double)(solver.propagations - origProps)/1000000.0 << "M" + << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << std::endl; + } + + return true; +} + +const bool FailedVarSearcher::tryBoth(const Lit lit1, const Lit lit2) +{ + if (binXorFind) { + if (lastTrailSize < solver.trail.size()) { + for (uint32_t i = lastTrailSize; i != solver.trail.size(); i++) { + removeVarFromXors(solver.trail[i].var()); + } + } + lastTrailSize = solver.trail.size(); + xorClauseTouched.setZero(); + investigateXor.clear(); + } + + propagated.setZero(); + twoLongXors.clear(); + propagatedVars.clear(); + unPropagatedBin.setZero(); + bothSame.clear(); + + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(lit1); + failed = (solver.propagateLight() != NULL); + if (failed) { + solver.cancelUntil(0); + numFailed++; + solver.uncheckedEnqueue(~lit1); + solver.ok = (solver.propagate(false) == NULL); + if (!solver.ok) return false; + return true; + } else { + assert(solver.decisionLevel() > 0); + for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { + Var x = solver.trail[c].var(); + propagated.setBit(x); + if (solver.addExtraBins) { + unPropagatedBin.setBit(x); + propagatedVars.push(x); + } + if (solver.assigns[x].getBool()) propValue.setBit(x); + else propValue.clearBit(x); + + if (binXorFind) removeVarFromXors(x); + } + + if (binXorFind) { + for (uint32_t *it = investigateXor.getData(), *end = investigateXor.getDataEnd(); it != end; it++) { + if (xorClauseSizes[*it] == 2) + twoLongXors.insert(getTwoLongXor(*solver.xorclauses[*it])); + } + for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { + addVarFromXors(solver.trail[c].var()); + } + xorClauseTouched.setZero(); + investigateXor.clear(); + } + + solver.cancelUntil(0); + } + + if (solver.addExtraBins && hyperbinProps < maxHyperBinProps) addBinClauses(lit1); + propagatedVars.clear(); + unPropagatedBin.setZero(); + + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(lit2); + failed = (solver.propagateLight() != NULL); + if (failed) { + solver.cancelUntil(0); + numFailed++; + solver.uncheckedEnqueue(~lit2); + solver.ok = (solver.propagate(false) == NULL); + if (!solver.ok) return false; + return true; + } else { + assert(solver.decisionLevel() > 0); + for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { + Var x = solver.trail[c].var(); + if (propagated[x]) { + if (solver.addExtraBins) { + unPropagatedBin.setBit(x); + propagatedVars.push(x); + } + if (propValue[x] == solver.assigns[x].getBool()) { + //they both imply the same + bothSame.push(Lit(x, !propValue[x])); + } else if (c != (int)solver.trail_lim[0]) { + bool invert; + if (lit1.var() == lit2.var()) { + assert(lit1.sign() == false && lit2.sign() == true); + tmpPs[0] = Lit(lit1.var(), false); + tmpPs[1] = Lit(x, false); + invert = propValue[x]; + } else { + tmpPs[0] = Lit(lit1.var(), false); + tmpPs[1] = Lit(lit2.var(), false); + invert = lit1.sign() ^ lit2.sign(); + } + if (!solver.varReplacer->replace(tmpPs, invert, 0)) + return false; + bothInvert += solver.varReplacer->getNewToReplaceVars() - toReplaceBefore; + toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); + } + } + if (solver.assigns[x].getBool()) propValue.setBit(x); + else propValue.clearBit(x); + if (binXorFind) removeVarFromXors(x); + } + + if (binXorFind) { + if (twoLongXors.size() > 0) { + for (uint32_t *it = investigateXor.getData(), *end = it + investigateXor.size(); it != end; it++) { + if (xorClauseSizes[*it] == 2) { + TwoLongXor tmp = getTwoLongXor(*solver.xorclauses[*it]); + if (twoLongXors.find(tmp) != twoLongXors.end()) { + tmpPs[0] = Lit(tmp.var[0], false); + tmpPs[1] = Lit(tmp.var[1], false); + if (!solver.varReplacer->replace(tmpPs, tmp.inverted, solver.xorclauses[*it]->getGroup())) + return false; + newBinXor += solver.varReplacer->getNewToReplaceVars() - toReplaceBefore; + toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); + } + } + } + } + for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { + addVarFromXors(solver.trail[c].var()); + } + } + + solver.cancelUntil(0); + } + + if (solver.addExtraBins && hyperbinProps < maxHyperBinProps) addBinClauses(lit2); + + for(uint32_t i = 0; i != bothSame.size(); i++) { + solver.uncheckedEnqueue(bothSame[i]); + } + goodBothSame += bothSame.size(); + solver.ok = (solver.propagate(false) == NULL); + if (!solver.ok) return false; + + return true; +} + +struct litOrder +{ + litOrder(const vector& _litDegrees) : + litDegrees(_litDegrees) + {} + + bool operator () (const Lit& x, const Lit& y) { + return litDegrees[x.toInt()] > litDegrees[y.toInt()]; + } + + const vector& litDegrees; +}; + +void FailedVarSearcher::addBinClauses(const Lit& lit) +{ + uint64_t oldProps = solver.propagations; + #ifdef VERBOSE_DEBUG + std::cout << "Checking one BTC vs UP" << std::endl; + #endif //VERBOSE_DEBUG + vec toVisit; + + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(lit); + failed = (solver.propagateBin() != NULL); + assert(!failed); + + assert(solver.decisionLevel() > 0); + if (propagatedVars.size() - (solver.trail.size()-solver.trail_lim[0]) == 0) { + solver.cancelUntil(0); + goto end; + } + for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { + Lit x = solver.trail[c]; + unPropagatedBin.clearBit(x.var()); + toVisit.push(x); + } + solver.cancelUntil(0); + + std::sort(toVisit.getData(), toVisit.getDataEnd(), litOrder(litDegrees)); + /************************* + //To check that the ordering is the right way + // --> i.e. to avoid mistake present in Glucose's ordering + for (uint32_t i = 0; i < toVisit.size(); i++) { + std::cout << "i:" << std::setw(8) << i << " degree:" << litDegrees[toVisit[i].toInt()] << std::endl; + } + std::cout << std::endl; + ***************************/ + + //difference between UP and BTC is in unPropagatedBin + for (Lit *l = toVisit.getData(), *end = toVisit.getDataEnd(); l != end; l++) { + #ifdef VERBOSE_DEBUG + std::cout << "Checking visit level " << end-l-1 << std::endl; + uint32_t thisLevel = 0; + #endif //VERBOSE_DEBUG + fillImplies(*l); + if (unPropagatedBin.nothingInCommon(myimplies)) goto next; + for (const Var *var = propagatedVars.getData(), *end2 = propagatedVars.getDataEnd(); var != end2; var++) { + if (unPropagatedBin[*var] && myimplies[*var]) { + #ifdef VERBOSE_DEBUG + thisLevel++; + #endif //VERBOSE_DEBUG + addBin(~*l, Lit(*var, !propValue[*var])); + unPropagatedBin.removeThese(myImpliesSet); + if (unPropagatedBin.isZero()) { + myimplies.removeThese(myImpliesSet); + myImpliesSet.clear(); + goto end; + } + } + } + next: + myimplies.removeThese(myImpliesSet); + myImpliesSet.clear(); + #ifdef VERBOSE_DEBUG + if (thisLevel > 0) { + std::cout << "Added " << thisLevel << " level diff:" << end-l-1 << std::endl; + } + #endif //VERBOSE_DEBUG + } + assert(unPropagatedBin.isZero()); + + end: + hyperbinProps += solver.propagations - oldProps; +} + +void FailedVarSearcher::fillImplies(const Lit& lit) +{ + solver.newDecisionLevel(); + solver.uncheckedEnqueue(lit); + failed = (solver.propagateLight() != NULL); + assert(!failed); + + assert(solver.decisionLevel() > 0); + for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { + Lit x = solver.trail[c]; + myimplies.setBit(x.var()); + myImpliesSet.push(x.var()); + } + solver.cancelUntil(0); +} + +template +const bool FailedVarSearcher::fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec& wrong) +{ + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(lit); + //if it's a cycle, it doesn't work, so don't propagate origLit + failed = (solver.propagateBinExcept(origLit) != NULL); + if (failed) return false; + + assert(solver.decisionLevel() > 0); + int c; + extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER; + for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) { + Lit x = solver.trail[c]; + if (toDeleteSet[x.toInt()]) { + wrong.push(x); + toDeleteSet[x.toInt()] = false; + }; + solver.assigns[x.var()] = l_Undef; + } + solver.assigns[solver.trail[c].var()] = l_Undef; + + solver.qhead = solver.trail_lim[0]; + solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]); + solver.trail_lim.clear(); + //solver.cancelUntil(0); + + return true; +} + +void FailedVarSearcher::addBin(const Lit& lit1, const Lit& lit2) +{ + #ifdef VERBOSE_DEBUG + std::cout << "Adding extra bin: "; + lit1.print(); std::cout << " "; lit2.printFull(); + #endif //VERBOSE_DEBUG + + tmpPs[0] = lit1; + tmpPs[1] = lit2; + solver.addLearntClause(tmpPs, 0, 0); + tmpPs.growTo(2); + assert(solver.ok); +} + +template +const bool FailedVarSearcher::removeUselessBinaries(const Lit& lit) +{ + //Nothing can be learnt at this point! + //Otherwise, it might happen that the path to X has learnts, + //but binary clause to X is not learnt. + //So we remove X , then we might remove + //the path (since it's learnt) -- removing a FACT!! + //[note:removal can be through variable elimination + //, and removeWrong() will happily remove it + assert(!startUp || solver.learnts.size() == 0); + + solver.newDecisionLevel(); + solver.uncheckedEnqueueLight(lit); + failed = (solver.propagateBinOneLevel() != NULL); + if (failed) return false; + bool ret = true; + + oneHopAway.clear(); + assert(solver.decisionLevel() > 0); + int c; + if (solver.trail.size()-solver.trail_lim[0] == 0) { + solver.cancelUntil(0); + goto end; + } + extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER; + for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) { + Lit x = solver.trail[c]; + toDeleteSet[x.toInt()] = true; + oneHopAway.push(x); + solver.assigns[x.var()] = l_Undef; + } + solver.assigns[solver.trail[c].var()] = l_Undef; + + solver.qhead = solver.trail_lim[0]; + solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]); + solver.trail_lim.clear(); + //solver.cancelUntil(0); + + wrong.clear(); + for(uint32_t i = 0; i < oneHopAway.size(); i++) { + //no need to visit it if it already queued for removal + //basically, we check if it's in 'wrong' + if (toDeleteSet[oneHopAway[i].toInt()]) { + if (!fillBinImpliesMinusLast(lit, oneHopAway[i], wrong)) { + ret = false; + goto end; + } + } + } + + for (uint32_t i = 0; i < wrong.size(); i++) { + removeBin(~lit, wrong[i]); + } + + end: + for(uint32_t i = 0; i < oneHopAway.size(); i++) { + toDeleteSet[oneHopAway[i].toInt()] = false; + } + + return ret; +} +template const bool FailedVarSearcher::removeUselessBinaries (const Lit& lit); +template const bool FailedVarSearcher::removeUselessBinaries (const Lit& lit); +template const bool FailedVarSearcher::fillBinImpliesMinusLast (const Lit& origLit, const Lit& lit, vec& wrong); +template const bool FailedVarSearcher::fillBinImpliesMinusLast (const Lit& origLit, const Lit& lit, vec& wrong); +template const bool FailedVarSearcher::removeUslessBinFull (); +template const bool FailedVarSearcher::removeUslessBinFull (); + +void FailedVarSearcher::removeBin(const Lit& lit1, const Lit& lit2) +{ + /******************* + Lit litFind1 = lit_Undef; + Lit litFind2 = lit_Undef; + + if (solver.binwatches[(~lit1).toInt()].size() < solver.binwatches[(~lit2).toInt()].size()) { + litFind1 = lit1; + litFind2 = lit2; + } else { + litFind1 = lit2; + litFind2 = lit1; + } + ********************/ + + //Find AND remove from watches + vec& bwin = solver.binwatches[(~lit1).toInt()]; + extraTime += bwin.size() / EXTRATIME_DIVIDER; + Clause *cl = NULL; + WatchedBin *i, *j; + i = j = bwin.getData(); + for (const WatchedBin *end = bwin.getDataEnd(); i != end; i++) { + if (i->impliedLit == lit2 && cl == NULL) { + cl = i->clause; + } else { + *j++ = *i; + } + } + bwin.shrink(1); + assert(cl != NULL); + + bool found = false; + vec& bwin2 = solver.binwatches[(~lit2).toInt()]; + extraTime += bwin2.size() / EXTRATIME_DIVIDER; + i = j = bwin2.getData(); + for (const WatchedBin *end = bwin2.getDataEnd(); i != end; i++) { + if (i->clause == cl) { + found = true; + } else { + *j++ = *i; + } + } + bwin2.shrink(1); + assert(found); + + #ifdef VERBOSE_DEBUG + std::cout << "Removing useless bin: "; + cl->plainPrint(); + #endif //VERBOSE_DEBUG + + cl->setRemoved(); + solver.clauses_literals -= 2; +} + +template +inline void FailedVarSearcher::cleanAndAttachClauses(vec& cs) +{ + T **i = cs.getData(); + T **j = i; + for (T **end = cs.getDataEnd(); i != end; i++) { + if (cleanClause(**i)) { + solver.attachClause(**i); + *j++ = *i; + } else { + clauseFree(*i); + } + } + cs.shrink(i-j); +} + +inline const bool FailedVarSearcher::cleanClause(Clause& ps) +{ + uint32_t origSize = ps.size(); + + Lit *i = ps.getData(); + Lit *j = i; + for (Lit *end = ps.getDataEnd(); i != end; i++) { + if (solver.value(*i) == l_True) return false; + if (solver.value(*i) == l_Undef) { + *j++ = *i; + } + } + ps.shrink(i-j); + assert(ps.size() > 1); + + if (ps.size() != origSize) ps.setStrenghtened(); + if (origSize != 2 && ps.size() == 2) + solver.becameBinary++; + + return true; +} + +inline const bool FailedVarSearcher::cleanClause(XorClause& ps) +{ + uint32_t origSize = ps.size(); + + Lit *i = ps.getData(), *j = i; + for (Lit *end = ps.getDataEnd(); i != end; i++) { + if (solver.assigns[i->var()] == l_True) ps.invert(true); + if (solver.assigns[i->var()] == l_Undef) { + *j++ = *i; + } + } + ps.shrink(i-j); + + if (ps.size() == 0) return false; + assert(ps.size() > 1); + + if (ps.size() != origSize) ps.setStrenghtened(); + if (ps.size() == 2) { + ps[0] = ps[0].unsign(); + ps[1] = ps[1].unsign(); + solver.varReplacer->replace(ps, ps.xor_clause_inverted(), ps.getGroup()); + return false; + } + + return true; +} + +/*************** +UNTESTED CODE +***************** +const bool FailedVarSearcher::tryAll(const Lit* begin, const Lit* end) +{ + propagated.setZero(); + BitArray propagated2; + propagated2.resize(solver.nVars(), 0); + propValue.resize(solver.nVars(), 0); + bool first = true; + bool last = false; + + for (const Lit *it = begin; it != end; it++, first = false) { + if (it+1 == end) last = true; + + if (!first && !last) propagated2.setZero(); + solver.newDecisionLevel(); + solver.uncheckedEnqueue(*it); + failed = (solver.propagate(false) != NULL); + if (failed) { + solver.cancelUntil(0); + numFailed++; + solver.uncheckedEnqueue(~(*it)); + solver.ok = (solver.propagate(false) == NULL); + if (!solver.ok) return false; + return true; + } else { + assert(solver.decisionLevel() > 0); + for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) { + Var x = solver.trail[c].var(); + if (last) { + if (propagated[x] && propValue[x] == solver.assigns[x].getBool()) + bothSame.push_back(make_pair(x, !propValue[x])); + } else { + if (first) { + propagated.setBit(x); + if (solver.assigns[x].getBool()) + propValue.setBit(x); + else + propValue.clearBit(x); + } else if (propValue[x] == solver.assigns[x].getBool()) { + propagated2.setBit(x); + } + } + } + solver.cancelUntil(0); + } + if (!last && !first) { + propagated &= propagated2; + if (propagated.isZero()) return true; + } + } + + for(uint32_t i = 0; i != bothSame.size(); i++) { + solver.uncheckedEnqueue(Lit(bothSame[i].first, bothSame[i].second)); + } + goodBothSame += bothSame.size(); + bothSame.clear(); + solver.ok = (solver.propagate(false) == NULL); + if (!solver.ok) return false; + + return true; +} +************** +Untested code end +**************/ + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/FailedVarSearcher.h b/src/sat/cryptominisat2/FailedVarSearcher.h index e69de29..9f714ea 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.h +++ b/src/sat/cryptominisat2/FailedVarSearcher.h @@ -0,0 +1,169 @@ +/*********************************************************************************** +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 FAILEDVARSEARCHER_H +#define FAILEDVARSEARCHER_H + +#include +#include +using std::map; + +#include "SolverTypes.h" +#include "Clause.h" +#include "BitArray.h" + +namespace MINISAT +{ +using namespace MINISAT; + +class Solver; + +class TwoLongXor +{ + public: + const bool operator==(const TwoLongXor& other) const + { + if (var[0] == other.var[0] && var[1] == other.var[1] && inverted == other.inverted) + return true; + return false; + } + const bool operator<(const TwoLongXor& other) const + { + if (var[0] < other.var[0]) return true; + if (var[0] > other.var[0]) return false; + + if (var[1] < other.var[1]) return true; + if (var[1] > other.var[1]) return false; + + if (inverted < other.inverted) return true; + if (inverted > other.inverted) return false; + + return false; + } + + Var var[2]; + bool inverted; +}; + +class FailedVarSearcher { + public: + FailedVarSearcher(Solver& _solver); + + const bool search(uint64_t numProps); + template + const bool removeUslessBinFull(); + + private: + //For 2-long xor + const TwoLongXor getTwoLongXor(const XorClause& c); + void addFromSolver(const vec& cs); + uint32_t newBinXor; + + //For detach&re-attach (when lots of vars found) + template + void cleanAndAttachClauses(vec& cs); + const bool cleanClause(Clause& ps); + const bool cleanClause(XorClause& ps); + void completelyDetachAndReattach(); + + //For re-adding old removed learnt clauses + const bool readdRemovedLearnts(); + void removeOldLearnts(); + + //Main + const bool tryBoth(const Lit lit1, const Lit lit2); + const bool tryAll(const Lit* begin, const Lit* end); + void printResults(const double myTime) const; + + Solver& solver; + + //Time + uint32_t extraTime; + + //For failure + bool failed; + + //bothprop finding + BitArray propagated; + BitArray propValue; + vec bothSame; + + //2-long xor-finding + vec xorClauseSizes; + vector > occur; + void removeVarFromXors(const Var var); + void addVarFromXors(const Var var); + BitArray xorClauseTouched; + vec investigateXor; + std::set twoLongXors; + bool binXorFind; + uint32_t lastTrailSize; + + //2-long xor-finding no.2 through + // 1) (a->b, ~a->~b) -> a=b + // 2) binary clause (a,c): (a->g, c->~g) -> a = ~c + uint32_t bothInvert; + + //finding HyperBins + void addBinClauses(const Lit& lit); + BitArray unPropagatedBin; + vec propagatedVars; + void addBin(const Lit& lit1, const Lit& lit2); + void fillImplies(const Lit& lit); + BitArray myimplies; + vec myImpliesSet; + uint64_t hyperbinProps; + vector litDegrees; + const bool orderLits(); + uint64_t maxHyperBinProps; + uint64_t binClauseAdded; + + //Remove useless binaries + template + const bool fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec& wrong); + template + const bool removeUselessBinaries(const Lit& lit); + void removeBin(const Lit& lit1, const Lit& lit2); + vec toDeleteSet; + vec oneHopAway; + vec wrong; + + //Temporaries + vec tmpPs; + + //State for this run + uint32_t toReplaceBefore; + uint32_t origTrailSize; + uint64_t origProps; + uint32_t numFailed; + uint32_t goodBothSame; + + //State between runs + bool finishedLastTimeVar; + uint32_t lastTimeWentUntilVar; + bool finishedLastTimeBin; + uint32_t lastTimeWentUntilBin; + + double numPropsMultiplier; + uint32_t lastTimeFoundTruths; + + uint32_t numCalls; +}; + +}; //NAMESPACE MINISAT + +#endif //FAILEDVARSEARCHER_H \ No newline at end of file diff --git a/src/sat/cryptominisat2/FindUndef.cpp b/src/sat/cryptominisat2/FindUndef.cpp index e69de29..84d8a6c 100644 --- a/src/sat/cryptominisat2/FindUndef.cpp +++ b/src/sat/cryptominisat2/FindUndef.cpp @@ -0,0 +1,177 @@ +/*********************************************************************************** +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 "FindUndef.h" + +#include "Solver.h" +#include "VarReplacer.h" +#include + +namespace MINISAT +{ +using namespace MINISAT; + +FindUndef::FindUndef(Solver& _solver) : + solver(_solver) + , isPotentialSum(0) +{ +} + +void FindUndef::fillPotential() +{ + int trail = solver.decisionLevel()-1; + + while(trail > 0) { + assert(trail < (int)solver.trail_lim.size()); + uint at = solver.trail_lim[trail]; + + assert(at > 0); + Var v = solver.trail[at].var(); + if (solver.assigns[v] != l_Undef) { + isPotential[v] = true; + isPotentialSum++; + } + + trail--; + } + + for (XorClause** it = solver.xorclauses.getData(), **end = it + solver.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(!solver.value(*l).isUndef()); + } + } + + vector replacingVars = solver.varReplacer->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]) + solver.assigns[i] = l_Undef; +} + +void FindUndef::moveBinToNormal() +{ + binPosition = solver.clauses.size(); + for (uint i = 0; i != solver.binaryClauses.size(); i++) + solver.clauses.push(solver.binaryClauses[i]); + solver.binaryClauses.clear(); +} + +void FindUndef::moveBinFromNormal() +{ + for (uint i = binPosition; i != solver.clauses.size(); i++) + solver.binaryClauses.push(solver.clauses[i]); + solver.clauses.shrink(solver.clauses.size() - binPosition); +} + +const uint FindUndef::unRoll() +{ + if (solver.decisionLevel() == 0) return 0; + + moveBinToNormal(); + + dontLookAtClause.resize(solver.clauses.size(), false); + isPotential.resize(solver.nVars(), false); + fillPotential(); + satisfies.resize(solver.nVars(), 0); + + while(!updateTables()) { + assert(isPotentialSum > 0); + + uint32_t maximum = 0; + Var v = var_Undef; + for (uint i = 0; i < isPotential.size(); i++) { + if (isPotential[i] && satisfies[i] >= maximum) { + maximum = satisfies[i]; + v = i; + } + } + assert(v != var_Undef); + + isPotential[v] = false; + isPotentialSum--; + + std::fill(satisfies.begin(), satisfies.end(), 0); + } + + unboundIsPotentials(); + moveBinFromNormal(); + + return isPotentialSum; +} + +bool FindUndef::updateTables() +{ + bool allSat = true; + + uint i = 0; + for (Clause** it = solver.clauses.getData(), **end = it + solver.clauses.size(); it != end; it++, i++) { + if (dontLookAtClause[i]) + continue; + + Clause& c = **it; + bool definitelyOK = false; + Var v = var_Undef; + uint numTrue = 0; + for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + if (solver.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) { + assert(v != var_Undef); + isPotential[v] = false; + isPotentialSum--; + dontLookAtClause[i] = true; + continue; + } + + //numTrue > 1 + allSat = false; + for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) { + if (solver.value(*l) == l_True) + satisfies[l->var()]++; + } + } + + return allSat; +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/FindUndef.h b/src/sat/cryptominisat2/FindUndef.h index e69de29..d3612ac 100644 --- a/src/sat/cryptominisat2/FindUndef.h +++ b/src/sat/cryptominisat2/FindUndef.h @@ -0,0 +1,59 @@ +/*********************************************************************************** +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 FINDUNDEF_H +#define FINDUNDEF_H + +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER +#include +using std::vector; + +#include "Solver.h" + +namespace MINISAT +{ +using namespace MINISAT; + +class FindUndef { + public: + FindUndef(Solver& _solver); + const uint unRoll(); + + private: + Solver& solver; + + void moveBinToNormal(); + void moveBinFromNormal(); + 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; + uint32_t binPosition; + +}; + +}; //NAMESPACE MINISAT + +#endif // \ No newline at end of file diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index e69de29..4b7b905 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -0,0 +1,1161 @@ +/*********************************************************************************** +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 +#include "ClauseCleaner.h" + +using std::ostream; +using std::cout; +using std::endl; + +#ifdef VERBOSE_DEBUG +#include +#endif + +namespace MINISAT +{ +using namespace MINISAT; +static const uint16_t unassigned_col = std::numeric_limits::max(); +static const Var unassigned_var = std::numeric_limits::max(); + +ostream& operator << (ostream& os, const vec& v) +{ + for (uint32_t 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, const vector& _xorclauses) : + solver(_solver) + , config(_config) + , matrix_no(_matrix_no) + , xorclauses(_xorclauses) + , messed_matrix_vars_since_reversal(true) + , gauss_last_level(0) + , disabled(false) + , useful_prop(0) + , useful_confl(0) + , called(0) + , unit_truths(0) +{ +} + +Gaussian::~Gaussian() +{ + for (uint i = 0; i < clauses_toclear.size(); i++) + clauseFree(clauses_toclear[i].first); +} + +inline void Gaussian::set_matrixset_to_cur() +{ + uint level = solver.decisionLevel() / config.only_nth_gauss_save; + assert(level <= matrix_sets.size()); + + if (level == matrix_sets.size()) + matrix_sets.push_back(cur_matrixset); + else + matrix_sets[level] = cur_matrixset; +} + +const bool Gaussian::full_init() +{ + assert(solver.ok); + + if (!should_init()) return true; + reset_stats(); + uint32_t last_trail_size = solver.trail.size(); + + bool do_again_gauss = true; + while (do_again_gauss) { + do_again_gauss = false; + solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); + if (!solver.ok) return false; + init(); + Clause* confl; + gaussian_ret g = gaussian(confl); + switch (g) { + case unit_conflict: + case conflict: + solver.ok = false; + return false; + case unit_propagation: + case propagation: + unit_truths += last_trail_size - solver.trail.size(); + do_again_gauss = true; + solver.ok = (solver.propagate() == NULL); + if (!solver.ok) return false; + break; + case nothing: + break; + } + } + + return true; +} + +void Gaussian::init() +{ + assert(solver.decisionLevel() == 0); + + fill_matrix(cur_matrixset); + if (!cur_matrixset.num_rows || !cur_matrixset.num_cols) { + disabled = true; + badlevel = 0; + return; + } + + matrix_sets.clear(); + matrix_sets.push_back(cur_matrixset); + gauss_last_level = solver.trail.size(); + messed_matrix_vars_since_reversal = false; + badlevel = UINT_MAX; + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Gaussian init finished." << endl; + #endif +} + +uint Gaussian::select_columnorder(vector& var_to_col, matrixset& origMat) +{ + var_to_col.resize(solver.nVars(), unassigned_col); + + uint num_xorclauses = 0; + for (uint32_t i = 0; i != xorclauses.size(); i++) { + XorClause& c = *xorclauses[i]; + if (c.removed()) continue; + num_xorclauses++; + + for (uint i2 = 0; i2 < c.size(); i2++) { + assert(solver.assigns[c[i2].var()].isUndef()); + var_to_col[c[i2].var()] = unassigned_col - 1; + } + } + + uint largest_used_var = 0; + for (uint i = 0; i < var_to_col.size(); i++) + if (var_to_col[i] != unassigned_col) + largest_used_var = i; + var_to_col.resize(largest_used_var + 1); + + var_is_in.resize(var_to_col.size(), 0); + origMat.var_is_set.resize(var_to_col.size(), 0); + + origMat.col_to_var.clear(); + vector vars(solver.nVars()); + if (!config.orderCols) { + for (uint32_t i = 0; i < solver.nVars(); i++) { + vars.push_back(i); + } + std::random_shuffle(vars.begin(), vars.end()); + } + + Heap order_heap(solver.order_heap); + uint32_t iterReduceIt = 0; + while ((config.orderCols && !order_heap.empty()) || (!config.orderCols && iterReduceIt < vars.size())) + { + Var v; + if (config.orderCols) v = order_heap.removeMin(); + else v = vars[iterReduceIt++]; + 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] = origMat.col_to_var.size()-1; + var_is_in.setBit(v); + } + } + + //for the ones that were not in the order_heap, but are marked in var_to_col + for (uint v = 0; v != var_to_col.size(); v++) { + if (var_to_col[v] == unassigned_col - 1) { + origMat.col_to_var.push_back(v); + var_to_col[v] = origMat.col_to_var.size() -1; + var_is_in.setBit(v); + } + } + + #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; + #endif + + return num_xorclauses; +} + +void Gaussian::fill_matrix(matrixset& origMat) +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Filling matrix" << endl; + #endif + + vector var_to_col; + origMat.num_rows = select_columnorder(var_to_col, origMat); + origMat.num_cols = origMat.col_to_var.size(); + col_to_var_original = origMat.col_to_var; + changed_rows.resize(origMat.num_rows); + memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size()); + + 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.first_one_in_row.resize(origMat.num_rows); + + origMat.removeable_cols = 0; + origMat.least_column_changed = -1; + origMat.matrix.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 (uint32_t i = 0; i != xorclauses.size(); i++) { + const XorClause& c = *xorclauses[i]; + if (c.removed()) continue; + + origMat.matrix.getVarsetAt(matrix_row).set(c, var_to_col, origMat.num_cols); + origMat.matrix.getMatrixAt(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.beginMatrix(); + uint row_num = 0; + + if (solver.assigns[var].getBool()) { + for (uint end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) { + if ((*this_row)[col]) { + changed_rows[row_num] = true; + (*this_row).invert_is_true(); + (*this_row).clearBit(col); + } + } + } else { + for (uint end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) { + if ((*this_row)[col]) { + changed_rows[row_num] = true; + (*this_row).clearBit(col); + } + } + } + + #ifdef DEBUG_GAUSS + bool c = false; + for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = r + m.matrix.getSize(); 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(nothing_to_propagate(cur_matrixset)); + assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m)); + #endif + + memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size()); + + uint last = 0; + uint col = 0; + for (const 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; + + #ifdef DEBUG_GAUSS + check_matrix_against_varset(m.matrix, m); + #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;*/ +} + +inline void Gaussian::update_last_one_in_col(matrixset& m) +{ + for (uint16_t* i = &m.last_one_in_col[0]+m.last_one_in_col.size()-1, *end = &m.last_one_in_col[0]-1; i != end && *i >= m.num_rows; i--) + *i = m.num_rows; +} + +Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl) +{ + if (solver.decisionLevel() >= badlevel) + return nothing; + + if (messed_matrix_vars_since_reversal) { + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix needs copy before update" << endl; + #endif + + const uint level = solver.decisionLevel() / config.only_nth_gauss_save; + assert(level < matrix_sets.size()); + cur_matrixset = matrix_sets[level]; + } + update_last_one_in_col(cur_matrixset); + update_matrix_by_col_all(cur_matrixset); + + messed_matrix_vars_since_reversal = false; + gauss_last_level = solver.trail.size(); + badlevel = UINT_MAX; + + 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); + #endif + + gaussian_ret ret; + //There is no early abort, so this is unneeded + /*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); + //} + #ifdef DEBUG_GAUSS + assert(ret == conflict || nothing_to_propagate(cur_matrixset)); + #endif + + if (!cur_matrixset.num_cols || !cur_matrixset.num_rows) { + badlevel = solver.decisionLevel(); + return nothing; + } + + if (ret == nothing && + solver.decisionLevel() % 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(solver.decisionLevel() == 0 || check_last_one_in_cols(m)); + #endif + + uint i = 0; + uint j = (config.iterativeReduce) ? m.least_column_changed + 1 : 0; + PackedMatrix::iterator beginIt = m.matrix.beginMatrix(); + PackedMatrix::iterator rowIt = m.matrix.beginMatrix(); + + #ifdef DEBUG_GAUSS + check_first_one_in_row(m, j); + #endif + + if (j) { + uint16_t until = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows); + if (j-1 > m.first_one_in_row[m.num_rows-1]) + until = m.num_rows; + for (;i != until; i++, ++rowIt) if (changed_rows[i] && (*rowIt).popcnt_is_one(m.first_one_in_row[i])) + propagatable_rows.push(i); + } + + #ifdef VERBOSE_DEBUG + cout << "At while() start: i,j = " << i << ", " << j << endl; + cout << "num_rows:" << m.num_rows << " num_cols:" << m.num_cols << endl; + #endif + + if (j > m.num_cols) { + #ifdef VERBOSE_DEBUG + cout << "Going straight to finish" << endl; + #endif + goto finish; + } + + #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; + } + + PackedMatrix::iterator this_matrix_row = rowIt; + PackedMatrix::iterator end = beginIt + m.last_one_in_col[j]; + for (; this_matrix_row != end; ++this_matrix_row) { + if ((*this_matrix_row)[j]) + break; + } + + if (this_matrix_row != end) { + + //swap rows i and maxi, but do not change the value of i; + if (this_matrix_row != rowIt) { + #ifdef VERBOSE_DEBUG + no_exchanged++; + #endif + + //Would early abort, but would not find the best conflict (and would be expensive) + //if (matrix_row_i.is_true() && matrix_row_i.isZero()) { + // conflict_row = i; + // return 0; + //} + (*rowIt).swapBoth(*this_matrix_row); + } + #ifdef DEBUG_GAUSS + assert(m.matrix.getMatrixAt(i).popcnt(j) == m.matrix.getMatrixAt(i).popcnt()); + assert(m.matrix.getMatrixAt(i)[j]); + #endif + + if ((*rowIt).popcnt_is_one(j)) + propagatable_rows.push(i); + + //Now A[i,j] will contain the old value of A[maxi,j]; + ++this_matrix_row; + for (; this_matrix_row != end; ++this_matrix_row) if ((*this_matrix_row)[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 + + (*this_matrix_row).xorBoth(*rowIt); + //Would early abort, but would not find the best conflict (and would be expensive) + //if (it->is_true() &&it->isZero()) { + // conflict_row = i2; + // return 0; + //} + } + m.first_one_in_row[i] = j; + i++; + ++rowIt; + m.last_one_in_col[j] = i; + } else { + m.first_one_in_row[i] = j; + m.last_one_in_col[j] = i + 1; + } + 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++) { + assert(m.matrix.getMatrixAt(row).popcnt() == m.matrix.getMatrixAt(row).popcnt(col)); + assert(!(m.col_to_var[col] == unassigned_var && m.matrix.getMatrixAt(row)[col])); + if (m.col_to_var[col] == unassigned_var || !m.matrix.getMatrixAt(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.col_to_var[col] == unassigned_var || std::min((uint16_t)(m.last_one_in_col[col]-1), m.num_rows) == 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); + + m.matrix.getVarsetAt(best_row).fill(tmp_clause, solver.assigns, col_to_var_original); + confl = (Clause*)XorClause_new(tmp_clause, false, solver.learnt_clause_group++); + Clause& cla = *confl; + #ifdef STATS_NEEDED + if (solver.dynamic_behaviour_analysis) + solver.logger.set_group_name(confl->getGroup(), "learnt gauss clause"); + #endif + + if (cla.size() <= 1) { + solver.ok = false; + return unit_conflict; + } + + assert(cla.size() >= 2); + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Found conflict:"; + cla.plainPrint(); + #endif + + if (maxlevel != solver.decisionLevel()) { + #ifdef STATS_NEEDED + if (solver.dynamic_behaviour_analysis) + solver.logger.conflict(Logger::gauss_confl_type, maxlevel, confl->getGroup(), *confl); + #endif + 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()] == (int32_t)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) +{ + int32_t maxlevel = std::numeric_limits::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.getMatrixAt(row).isZero()); + #endif + if (m.matrix.getMatrixAt(row).is_true()) + analyse_confl(m, row, maxlevel, size, best_row); + } + + if (maxlevel != std::numeric_limits::max()) + return handle_matrix_confl(confl, m, size, maxlevel, best_row); + + #ifdef DEBUG_GAUSS + assert(check_no_conflict(m)); + assert(last_row == 0 || !m.matrix.getMatrixAt(last_row-1).isZero()); + #endif + + #ifdef VERBOSE_DEBUG + cout << "Resizing matrix to num_rows = " << last_row << endl; + #endif + m.num_rows = last_row; + m.matrix.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 until_sublevel) +{ + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Canceling until sublevel " << until_sublevel << endl; + #endif + + for (vector::iterator gauss = solver.gauss_matrixes.begin(), end= solver.gauss_matrixes.end(); gauss != end; gauss++) + if (*gauss != this) (*gauss)->canceling(until_sublevel); + + for (int sublevel = solver.trail.size()-1; sublevel >= (int)until_sublevel; sublevel--) { + Var var = solver.trail[sublevel].var(); + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Canceling var " << var+1 << endl; + #endif + + #ifdef USE_OLD_POLARITIES + solver.polarity[var] = solver.oldPolarity[var]; + #endif //USE_OLD_POLARITIES + solver.assigns[var] = l_Undef; + solver.insertVarOrder(var); + } + solver.trail.shrink(solver.trail.size() - until_sublevel); + + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")Canceling sublevel finished." << endl; + #endif +} + +void Gaussian::analyse_confl(const matrixset& m, const uint row, int32_t& 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.matrix.getVarsetAt(row)); + cout << endl; + + cout << "(" << matrix_no << ")corresponding matrix's row (should be empty): "; + print_matrix_row(m.matrix.getMatrixAt(row)); + cout << endl; + #endif + + int32_t this_maxlevel = 0; + unsigned long int var = 0; + uint this_size = 0; + while (true) { + var = m.matrix.getVarsetAt(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 != std::numeric_limits::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 != std::numeric_limits::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.getMatrixAt(row) << endl; + cout << "(" << matrix_no << ")matrix row:"; + print_matrix_row(m.matrix.getMatrixAt(row)); + cout << endl; + #endif + + m.matrix.getVarsetAt(row).fill(tmp_clause, solver.assigns, col_to_var_original); + Clause& cla = *(Clause*)XorClause_new(tmp_clause, false, solver.learnt_clause_group++); + #ifdef VERBOSE_DEBUG + cout << "(" << matrix_no << ")matrix prop clause: "; + cla.plainPrint(); + cout << endl; + #endif + + assert(m.matrix.getMatrixAt(row).is_true() == !cla[0].sign()); + assert(solver.assigns[cla[0].var()].isUndef()); + if (cla.size() == 1) { + solver.cancelUntil(0); + solver.uncheckedEnqueue(cla[0]); + clauseFree(&cla); + return unit_propagation; + } + + clauses_toclear.push_back(std::make_pair(&cla, solver.trail.size()-1)); + #ifdef STATS_NEEDED + if (solver.dynamic_behaviour_analysis) + solver.logger.set_group_name(cla.getGroup(), "gauss prop clause"); + #endif + solver.uncheckedEnqueue(cla[0], &cla); + + return propagation; +} + +void Gaussian::disable_if_necessary() +{ + if (//nof_conflicts >= 0 + //&& conflictC >= nof_conflicts/8 + !config.dontDisable + && called > 50 + && useful_confl*2+useful_prop < (uint)((double)called*0.05) ) + 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, true); + clauseFree(confl); + + if (ret != l_Nothing) return ret; + return l_Continue; + } + case unit_propagation: + unit_truths++; + case propagation: + useful_prop++; + return l_Continue; + case unit_conflict: { + unit_truths++; + useful_confl++; + if (confl->size() == 0) { + clauseFree(confl); + return l_False; + } + + Lit lit = (*confl)[0]; + #ifdef STATS_NEEDED + if (solver.dynamic_behaviour_analysis) + solver.logger.conflict(Logger::gauss_confl_type, 0, confl->getGroup(), *confl); + #endif + + solver.cancelUntil(0); + + if (solver.assigns[lit.var()].isDef()) { + clauseFree(confl); + return l_False; + } + + solver.uncheckedEnqueue(lit); + + clauseFree(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++; + } + cout << "final:" << row.is_true() << endl;; +} + +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.is_true()) 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::print_matrix_stats() const +{ + cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl; +} + + +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.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r, ++row) { + if ((*r).is_true() && (*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.beginMatrix(); it != m.matrix.endMatrix(); ++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; + } +} + +const bool Gaussian::nothing_to_propagate(matrixset& m) const +{ + for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); 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.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r) { + if ((*r).isZero() && (*r).is_true()) + 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 = std::min(m.last_one_in_col[i] - 1, (int)m.num_rows); + uint real_last = 0; + uint i2 = 0; + for (PackedMatrix::iterator it = m.matrix.beginMatrix(); it != m.matrix.endMatrix(); ++it, i2++) { + if ((*it)[i]) + real_last = i2; + } + if (real_last > last) + return false; + } + + return true; +} + +void Gaussian::check_matrix_against_varset(PackedMatrix& matrix, const matrixset& m) const +{ + for (uint i = 0; i < matrix.getSize(); i++) { + const PackedRow mat_row = matrix.getMatrixAt(i); + const PackedRow var_row = matrix.getVarsetAt(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]); + assert(m.col_to_var[col] == unassigned_var); + assert(m.var_is_set[var]); + final = !final; + } else if (solver.assigns[var] == l_False) { + assert(!mat_row[col]); + assert(m.col_to_var[col] == unassigned_var); + assert(m.var_is_set[var]); + } else if (solver.assigns[var] == l_Undef) { + assert(m.col_to_var[col] != unassigned_var); + assert(!m.var_is_set[var]); + assert(mat_row[col]); + } else assert(false); + + col++; + } + if ((final^!mat_row.is_true()) != !var_row.is_true()) { + cout << "problem with row:"; print_matrix_row_with_assigns(var_row); cout << endl; + assert(false); + } + } +} + +const void Gaussian::check_first_one_in_row(matrixset& m, const uint j) +{ + if (j) { + uint16_t until2 = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows); + if (j-1 > m.first_one_in_row[m.num_rows-1]) { + until2 = m.num_rows; + #ifdef VERBOSE_DEBUG + cout << "j-1 > m.first_one_in_row[m.num_rows-1]" << "j:" << j << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl; + #endif + } + for (uint i2 = 0; i2 != until2; i2++) { + #ifdef VERBOSE_DEBUG + cout << endl << "row " << i2 << " (num rows:" << m.num_rows << ")" << endl; + cout << m.matrix.getMatrixAt(i2) << endl; + cout << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl; + cout << "first_one_in_row:" << m.first_one_in_row[i2] << endl; + cout << "num_cols:" << m.num_cols << endl; + cout << "popcnt:" << m.matrix.getMatrixAt(i2).popcnt() << endl; + cout << "popcnt_is_one():" << m.matrix.getMatrixAt(i2).popcnt_is_one() << endl; + cout << "popcnt_is_one("<< m.first_one_in_row[i2] <<"): " << m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]) << endl; + #endif + + for (uint i3 = 0; i3 < m.first_one_in_row[i2]; i3++) { + assert(m.matrix.getMatrixAt(i2)[i3] == 0); + } + assert(m.matrix.getMatrixAt(i2)[m.first_one_in_row[i2]]); + assert(m.matrix.getMatrixAt(i2).popcnt_is_one() == + m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2])); + } + } +} + +//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_is_true(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 +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "SolverTypes.h" +#include "Solver.h" +#include "GaussianConfig.h" +#include "PackedMatrix.h" +#include "BitArray.h" + +//#define VERBOSE_DEBUG +//#define DEBUG_GAUSS + +#ifdef VERBOSE_DEBUG +using std::vector; +using std::cout; +using std::endl; +#endif + +namespace MINISAT +{ +using namespace MINISAT; + +class Clause; + +class Gaussian +{ +public: + Gaussian(Solver& solver, const GaussianConfig& config, const uint matrix_no, const vector& xorclauses); + ~Gaussian(); + + const bool full_init(); + llbool find_truths(vec& learnt_clause, int& conflictC); + + //statistics + void print_stats() const; + 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; + const uint32_t get_unit_truths() const; + void set_disabled(const bool toset); + + //functions used throughout the Solver + void canceling(const uint sublevel); + +protected: + Solver& solver; + + //Gauss high-level configuration + const GaussianConfig& config; + const uint matrix_no; + vector xorclauses; + + enum gaussian_ret {conflict, unit_conflict, propagation, unit_propagation, nothing}; + gaussian_ret gaussian(Clause*& confl); + + vector col_to_var_original; //Matches columns to variables + BitArray var_is_in; //variable is part of the the matrix. var_is_in's size is _minimal_ so you should check whether var_is_in.getSize() < var before issuing var_is_in[var] + uint badlevel; + + class matrixset + { + public: + PackedMatrix matrix; // The matrix, updated to reflect variable assignements + BitArray var_is_set; + vector col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives unassigned_var 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) + vector last_one_in_col; //last_one_in_col[COL] tells the last row+1 that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row) + vector first_one_in_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 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 > clauses_toclear; + bool disabled; // Gauss is disabled + + //State of current elimnation + vec propagatable_rows; //used to store which rows were deemed propagatable during elimination + vector 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 + uint32_t unit_truths; //how many unitary (i.e. decisionLevel 0) truths have been found + + //gauss init functions + void init(); // Initalise gauss state + void fill_matrix(matrixset& origMat); // Fills the origMat matrix + uint select_columnorder(vector& var_to_col, matrixset& origMat); // 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, int32_t& 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' + vec tmp_clause; + + //propagation&conflict handling + void cancel_until_sublevel(const uint until_sublevel); // cancels until sublevel 'until_sublevel'. The var 'until_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(); + void reset_stats(); + void update_last_one_in_col(matrixset& m); + +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; + void check_matrix_against_varset(PackedMatrix& matrix,const matrixset& m) const; + const bool check_last_one_in_cols(matrixset& m) const; + const void check_first_one_in_row(matrixset& m, const uint j); + 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 bool Gaussian::should_init() const +{ + return (config.decision_until > 0); +} + +inline bool Gaussian::should_check_gauss(const uint decisionlevel, const uint starts) const +{ + return (!disabled + && decisionlevel < config.decision_until); +} + +inline void Gaussian::canceling(const uint sublevel) +{ + if (disabled) + return; + uint a = 0; + for (int i = clauses_toclear.size()-1; i >= 0 && clauses_toclear[i].second > sublevel; i--) { + clauseFree(clauses_toclear[i].first); + a++; + } + clauses_toclear.resize(clauses_toclear.size()-a); + + if (messed_matrix_vars_since_reversal) + return; + int c = std::min((int)gauss_last_level, (int)(solver.trail.size())-1); + for (; c >= (int)sublevel; c--) { + Var var = solver.trail[c].var(); + if (var < var_is_in.getSize() + && var_is_in[var] + && cur_matrixset.var_is_set[var]) { + messed_matrix_vars_since_reversal = true; + return; + } + } +} + +inline const uint32_t Gaussian::get_unit_truths() const +{ + return unit_truths; +} + +inline const uint Gaussian::get_called() const +{ + return called; +} + +inline const uint Gaussian::get_useful_prop() const +{ + return useful_prop; +} + +inline const uint Gaussian::get_useful_confl() const +{ + return useful_confl; +} + +inline const bool Gaussian::get_disabled() const +{ + return disabled; +} + +inline void Gaussian::set_disabled(const bool toset) +{ + disabled = toset; +} + +std::ostream& operator << (std::ostream& os, const vec& v); + +}; //NAMESPACE MINISAT + +#endif //GAUSSIAN_H diff --git a/src/sat/cryptominisat2/GaussianConfig.h b/src/sat/cryptominisat2/GaussianConfig.h index e69de29..0806f83 100644 --- a/src/sat/cryptominisat2/GaussianConfig.h +++ b/src/sat/cryptominisat2/GaussianConfig.h @@ -0,0 +1,62 @@ +/*********************************************************************************** +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 + +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "PackedRow.h" + +namespace MINISAT +{ +using namespace MINISAT; + +class GaussianConfig +{ + public: + + GaussianConfig() : + only_nth_gauss_save(2) + , decision_until(0) + , dontDisable(false) + , noMatrixFind(false) + , orderCols(true) + , iterativeReduce(true) + , maxMatrixRows(1000) + , minMatrixRows(20) + { + } + + //tuneable gauss parameters + uint only_nth_gauss_save; //save only every n-th gauss matrix + uint decision_until; //do Gauss until this level + bool dontDisable; //If activated, gauss elimination is never disabled + bool noMatrixFind; //Put all xor-s into one matrix, don't find matrixes + bool orderCols; //Order columns according to activity + bool iterativeReduce; //Don't minimise matrix work + uint32_t maxMatrixRows; //The maximum matrix size -- no. of rows + uint32_t minMatrixRows; //The minimum matrix size -- no. of rows +}; + +}; //NAMESPACE MINISAT + +#endif //GAUSSIANCONFIG_H diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index e69de29..59013e5 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -0,0 +1,909 @@ +/*********************************************************************************** +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 +#include +using std::cout; +using std::endl; +using std::ofstream; + +#include "Logger.h" +#include "SolverTypes.h" +#include "Solver.h" +#include "Gaussian.h" + +#define FST_WIDTH 10 +#define SND_WIDTH 35 +#define TRD_WIDTH 10 + +namespace MINISAT +{ +using namespace MINISAT; + +Logger::Logger(int& _verbosity) : + proof_graph_on(false) + , mini_proof(false) + , statistics_on(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) + , proofStarts(0) +{ + runid /= 10; + runid = time(NULL) % 10000; + if (verbosity >= 1) printf("c 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, "Noname"); + times_var_propagated.resize(var+1, 0); + times_var_guessed.resize(var+1, 0); + depths_of_assigns_for_var.resize(var+1); + depths_of_assigns_unit.resize(var+1, false); + } +} + +// 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_propagations_unit.resize(group+1, false); + depths_of_conflicts_for_group.resize(group+1); + } +} + +string Logger::cut_name_to_size(const string& name) const +{ + string ret = name; + uint len = name.length(); + while(len > 0 && (name[len-1] == ' ' || name[len-1] == 0x0A || name[len-1] == 0x0D)) { + ret.resize(len-1); + len--; + } + + if (len > SND_WIDTH-3) { + ret[SND_WIDTH-3] = '\0'; + ret[SND_WIDTH-4] = '.'; + ret[SND_WIDTH-5] = '.'; + } + + return ret; +} + +// Adds the new clause group's name to the information stored +void Logger::set_group_name(const uint group, const char* name_tmp) +{ + if (!statistics_on && !proof_graph_on) + return; + + string name; + if (name_tmp == NULL) return; + else name = name_tmp; + + set_group_name(group, name); +} + +void Logger::set_group_name(const uint group, string& name) +{ + new_group(group); + + if (name == "Noname") return; + + if (groupnames[group] == "Noname") { + groupnames[group] = name; + } else if (groupnames[group] != name) { + std::cout << "Error! Group no. " << group << "has been named twice. First, as '" << groupnames[group] << "', then second as '" << name << "'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line" << std::endl; + exit(-1); + } +} + +string Logger::get_group_name(const uint group) const +{ + assert(group < groupnames.size()); + return groupnames[group]; +} + +string Logger::get_var_name(const Var var) const +{ + if (var >= varnames.size()) return "unknown"; + return varnames[var]; +} + +// sets the variable's name +void Logger::set_variable_name(const uint var, char* name_tmp) +{ + if (!statistics_on && !proof_graph_on) + return; + + new_var(var); + + string name; + if (name_tmp == NULL) + name = ""; + else + name = name_tmp; + + if (varnames[var] == "Noname") { + 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(); +} + +void Logger::begin() +{ + begin_called = true; + if (proof_graph_on) { + std::stringstream filename; + filename << "proofs/" << runid << "-proof" << proofStarts++ << "-" << S->starts << ".dot"; + + 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.str().c_str(),"w"); + if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename.str().c_str()), 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 (uint32_t i = 0; i != learnt_clause.size(); i++) { + if (learnt_clause[i].sign()) fprintf(proof,"-"); + int myvar = learnt_clause[i].var(); + if (varnames[myvar] != "Noname") + fprintf(proof,"%s\\n",varnames[myvar].c_str()); + else + fprintf(proof,"Var: %d\\n",myvar); + } + } + 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].sum += S->decisionLevel(); + depths_of_conflicts_for_group[group].num ++; + + no_conflicts++; + sum_conflict_depths += S->trail.size() - S->trail_lim[0]; + sum_decisions_on_branches += S->decisionLevel(); + sum_propagations_on_branches += S->trail.size() - S->trail_lim[0] - S->decisionLevel(); + + if (branch_depth_distrib.size() <= S->decisionLevel()) + branch_depth_distrib.resize(S->decisionLevel()+1, 0); + branch_depth_distrib[S->decisionLevel()]++; + } +} + +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); + +// 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, Clause* c) +{ + first_begin(); + assert(!(proof == NULL && proof_graph_on)); + + uint group; + prop_type type; + if (c == NULL) { + if (S->decisionLevel() == 0) + type = add_clause_type; + else + type = guess_type; + group = std::numeric_limits::max(); + } else { + type = simple_propagation_type; + group = c->getGroup(); + } + + //graph + if (proof_graph_on && (!mini_proof || type == guess_type)) { + uniqueid++; + + fprintf(proof,"node%d [shape=box, label=\"",uniqueid);; + if (lit.sign()) + fprintf(proof,"-"); + if (varnames[lit.var()] != "Noname") + fprintf(proof,"%s\"];\n",varnames[lit.var()].c_str()); + else + fprintf(proof,"Var: %d\"];\n",lit.var()); + + fprintf(proof,"node%d -> node%d [label=\"",history[history.size()-1],uniqueid); + + switch (type) { + case simple_propagation_type: + fprintf(proof,"%s\"];\n", groupnames[group].c_str()); + break; + + case add_clause_type: + fprintf(proof,"red. from clause\"];\n"); + break; + + case guess_type: + fprintf(proof,"guess\",style=bold];\n"); + break; + } + history.push_back(uniqueid); + } + + if (statistics_on) { + switch (type) { + case simple_propagation_type: + depths_of_propagations_for_group[group].sum += S->decisionLevel(); + depths_of_propagations_for_group[group].num ++; + if (S->decisionLevel() == 0) depths_of_propagations_unit[group] = true; + times_group_caused_propagation[group]++; + case add_clause_type: + no_propagations++; + times_var_propagated[lit.var()]++; + depths_of_assigns_for_var[lit.var()].sum += S->decisionLevel(); + depths_of_assigns_for_var[lit.var()].num ++; + if (S->decisionLevel() == 0) depths_of_assigns_unit[lit.var()] = true; + break; + case guess_type: + no_decisions++; + times_var_guessed[lit.var()]++; + + depths_of_assigns_for_var[lit.var()].sum += S->decisionLevel(); + depths_of_assigns_for_var[lit.var()].num ++; + break; + } + } +} + +// Ending of a restart iteration +void Logger::end(const finish_type finish) +{ + first_begin(); + 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 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(); + } + + if (model_found || unsat_model_found) + begin_called = false; +} + +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 = (double)depths_of_assigns_for_var[i].sum + /(double)depths_of_assigns_for_var[i].num; + if (depths_of_assigns_for_var[i].num > 0 && !depths_of_assigns_unit[i]) + 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 = (double)depths_of_propagations_for_group[i].sum + /(double)depths_of_propagations_for_group[i].num; + if (depths_of_propagations_for_group[i].num > 0 && !depths_of_propagations_unit[i]) + 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 = (double)depths_of_conflicts_for_group[i].sum + /(double)depths_of_conflicts_for_group[i].num; + if (depths_of_conflicts_for_group[i].num > 0) + 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 (uint32_t 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, cut_name_to_size(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, cut_name_to_size(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, cut_name_to_size(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, cut_name_to_size(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; + + uint i = 0; + for (vector::const_iterator it = branch_depth_distrib.begin(); it != branch_depth_distrib.end(); it++, i++) { + range_stat[i/range] += *it; + } + + 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()); + i = 0; + + for (map::iterator it = range_stat.begin(); it != range_stat.end(); it++, i++) { + std::stringstream ss2; + ss2 << it->first*range << " - " << it->first*range + range-1; + 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; + } + } + 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_num(); + + uint slice = (maximum+1)/max_print_lines + (bool)((maximum+1)%max_print_lines); + + print_footer(); + print_simple_line(" Learnt clause length distribution"); + print_line("Length between", "no. cl."); + print_footer(); + + uint until = slice; + uint from = 0; + while(until < maximum+1) { + std::stringstream ss2; + ss2 << from << " - " << until-1; + + uint sum = 0; + for (; from < until; from++) { + map::const_iterator it = learnt_sizes.find(from); + if (it != learnt_sizes.end()) + sum += it->second; + } + + print_line(ss2.str(), sum); + + until += slice; + } + + print_footer(); + + print_leearnt_clause_graph_distrib(maximum, learnt_sizes); +} + +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 >= (uint)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->get_unitary_learnts_num()); + print_footer(); +} + +void Logger::print_learnt_unitaries(const uint from, const string display) const +{ + print_footer(); + print_simple_line(display); + print_header("var", "name", "value"); + uint32_t until; + if (S->decisionLevel() > 0) + until = S->trail_lim[0]; + else + until = S->trail.size(); + for (uint i = from; i < until; i++) { + Var var = S->trail[i].var(); + bool value = !(S->trail[i].sign()); + print_line(var+1, cut_name_to_size(varnames[var]), value); + } + 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(2); + 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(); + #ifdef USE_GAUSS + print_matrix_stats(); + #endif //USE_GAUSS + print_learnt_unitaries(0," Unitary clauses learnt until now"); + print_learnt_unitaries(last_unitary_learnt_clauses, " Unitary clauses during this restart"); + print_advanced_stats(); + print_general_stats(); +} + +#ifdef USE_GAUSS +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(); +} +#endif //USE_GAUSS + +void Logger::print_advanced_stats() const +{ + print_footer(); + print_simple_line(" Advanced statistics - for only this restart"); + print_footer(); + print_line("Unitary learnts", S->get_unitary_learnts_num() - last_unitary_learnt_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 avgIt; + + for (avgIt it = depths_of_propagations_for_group.begin(); it != depths_of_propagations_for_group.end(); it++) { + it->sum = 0; + it->num = 0; + } + + for (avgIt it = depths_of_conflicts_for_group.begin(); it != depths_of_conflicts_for_group.end(); it++) { + it->sum = 0; + it->num = 0; + } + + for (avgIt it = depths_of_assigns_for_var.begin(); it != depths_of_assigns_for_var.end(); it++) { + it->sum = 0; + it->num = 0; + } + for (uint i = 0; i < depths_of_assigns_unit.size(); i++) + depths_of_assigns_unit[i] = false; + + for (uint i = 0; i < depths_of_propagations_unit.size(); i++) + depths_of_propagations_unit[i] = false; + + sum_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(); + last_unitary_learnt_clauses = S->get_unitary_learnts_num(); +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h index e69de29..7567c7a 100644 --- a/src/sat/cryptominisat2/Logger.h +++ b/src/sat/cryptominisat2/Logger.h @@ -0,0 +1,190 @@ +/*********************************************************************************** +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 +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "Vec.h" +#include "Heap.h" +#include "Alg.h" +#include "SolverTypes.h" +#include "limits.h" +#include "Clause.h" + +using std::vector; +using std::pair; +using std::string; +using std::map; + +namespace MINISAT +{ +using namespace MINISAT; + +class Solver; + +class MyAvg { +public: + MyAvg() : + sum(0) + , num(0) + {} + + uint sum; + uint num; +}; + +class Logger +{ +public: + Logger(int& vebosity); + void setSolver(const Solver* S); + + //types of props, confl, and finish + enum prop_type { add_clause_type, guess_type, simple_propagation_type}; + enum confl_type { simple_confl_type, gauss_confl_type }; + enum finish_type { model_found, unsat_model_found, restarting}; + + //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, Clause* c); + + //functions to add/name variables + void new_var(const Var var); + void set_variable_name(const uint var, char* name_tmp); + + //function to name clause groups + void set_group_name(const uint group, const char* name_tmp); + void set_group_name(const uint group, string& name); + string get_group_name(const uint group) const; + string get_var_name(const Var var) const; + + 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); + string cut_name_to_size(const string& name) const; + + void print_groups(const vector >& to_print) const; + void print_groups(const vector >& to_print) const; + void print_vars(const vector >& to_print) const; + 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; + void print_learnt_unitaries(const uint from, const string display) 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_propagations_unit; + vector depths_of_conflicts_for_group; + vector depths_of_assigns_for_var; + vector depths_of_assigns_unit; + + //the distribution of branch depths. first = depth, second = number of occurances + vector branch_depth_distrib; + + uint64_t sum_conflict_depths; + uint64_t no_conflicts; + uint64_t no_decisions; + uint64_t no_propagations; + uint64_t sum_decisions_on_branches; + uint64_t sum_propagations_on_branches; + uint64_t last_unitary_learnt_clauses; + + //message display properties + const int& verbosity; + + const Solver* S; + + void first_begin(); + bool begin_called; + uint proofStarts; +}; + +}; //NAMESPACE MINISAT + +#endif //LOGGER_H diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index e69de29..b5b64e5 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -0,0 +1,32 @@ +TOP = ../../.. +include $(TOP)/scripts/Makefile.common + +MTL = mtl +MTRAND = MTRand +SOURCES = Logger.cpp Solver.cpp PackedRow.cpp \ + XorFinder.cpp Conglomerate.cpp VarReplacer.cpp \ + FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp \ + Clause.cpp FailedVarSearcher.cpp PartFinder.cpp \ + Subsumer.cpp PartHandler.cpp XorSubsumer.cpp SmallPtr.cpp \ + Gaussian.cpp MatrixFinder.cpp StateSaver.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) + ranlib $@ + cp $(LIB) ../ + cp $(OBJECTS) ../ + +clean: + rm -f $(OBJECTS) $(LIB) + +.cpp.o: + $(CC) $(CFLAGS) $< -o $@ diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp index e69de29..35443a7 100644 --- a/src/sat/cryptominisat2/MatrixFinder.cpp +++ b/src/sat/cryptominisat2/MatrixFinder.cpp @@ -0,0 +1,249 @@ +/*********************************************************************************** +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 "ClauseCleaner.h" +#include "time_mem.h" + +#include +#include +#include +#include +using std::set; +using std::map; + +//#define VERBOSE_DEBUG + +using std::cout; +using std::endl; + +namespace MINISAT +{ +using namespace MINISAT; + +//#define PART_FINDING + +MatrixFinder::MatrixFinder(Solver& _solver) : + solver(_solver) +{ +} + +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 bool MatrixFinder::findMatrixes() +{ + table.clear(); + table.resize(solver.nVars(), var_Undef); + reverseTable.clear(); + matrix_no = 0; + double myTime = cpuTime(); + + if (solver.xorclauses.size() < MIN_GAUSS_XOR_CLAUSES || + solver.gaussconfig.decision_until <= 0 || + solver.xorclauses.size() > MAX_GAUSS_XOR_CLAUSES + ) + return true; + + solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); + if (!solver.ok) return false; + + if (solver.gaussconfig.noMatrixFind) { + if (solver.verbosity >=1) + cout << "c | Matrix finding disabled through switch. Putting all xors into matrix." << endl; + vector xorclauses; + xorclauses.reserve(solver.xorclauses.size()); + for (uint32_t i = 0; i < solver.xorclauses.size(); i++) + xorclauses.push_back(solver.xorclauses[i]); + solver.gauss_matrixes.push_back(new Gaussian(solver, solver.gaussconfig, 0, xorclauses)); + return true; + } + + for (XorClause** c = solver.xorclauses.getData(), **end = c + solver.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()] != var_Undef) + 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 + + uint32_t numMatrixes = setMatrixes(); + + if (solver.verbosity >=1) + std::cout << "c | Finding matrixes : " << cpuTime() - myTime << " s (found " << numMatrixes << ") |" << endl; + + for (vector::iterator gauss = solver.gauss_matrixes.begin(), end = solver.gauss_matrixes.end(); gauss != end; gauss++) { + if (!(*gauss)->full_init()) return false; + } + + return true; +} + +const uint MatrixFinder::setMatrixes() +{ + vector > numXorInMatrix; + for (uint i = 0; i < matrix_no; i++) + numXorInMatrix.push_back(std::make_pair(i, 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 = solver.xorclauses.getData(), **end = c + solver.xorclauses.size(); c != end; c++) { + XorClause& x = **c; + const uint matrix = table[x[0].var()]; + assert(matrix < matrix_no); + + //for stats + numXorInMatrix[matrix].second++; + 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 + } + + std::sort(numXorInMatrix.begin(), numXorInMatrix.end(), mysorter()); + + #ifdef PART_FINDING + for (uint i = 0; i < matrix_no; i++) + findParts(xorFingerprintInMatrix[i], xorsInMatrix[i]); + #endif //PART_FINDING + + uint realMatrixNum = 0; + for (int a = matrix_no-1; a != -1; a--) { + uint i = numXorInMatrix[a].first; + + if (numXorInMatrix[a].second < 3) + continue; + + const uint totalSize = reverseTable[i].size()*numXorInMatrix[a].second; + const double density = (double)sumXorSizeInMatrix[i]/(double)totalSize*100.0; + double avg = (double)sumXorSizeInMatrix[i]/(double)numXorInMatrix[a].second; + double variance = 0.0; + for (uint i2 = 0; i2 < xorSizesInMatrix[i].size(); i2++) + variance += pow((double)xorSizesInMatrix[i][i2]-avg, 2); + variance /= (double)xorSizesInMatrix.size(); + const double stdDeviation = sqrt(variance); + + if (numXorInMatrix[a].second >= solver.gaussconfig.minMatrixRows + && numXorInMatrix[a].second <= solver.gaussconfig.maxMatrixRows + && realMatrixNum < 3) + { + if (solver.verbosity >=1) + cout << "c | Matrix no " << std::setw(2) << realMatrixNum; + solver.gauss_matrixes.push_back(new Gaussian(solver, solver.gaussconfig, realMatrixNum, xorsInMatrix[i])); + realMatrixNum++; + + } else { + if (solver.verbosity >=1 /*&& numXorInMatrix[a].second >= 20*/) + cout << "c | Unused Matrix "; + } + if (solver.verbosity >=1 /*&& numXorInMatrix[a].second >= 20*/) { + cout << std::setw(7) << numXorInMatrix[a].second << " 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; + } + } + + 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)->plainPrint(); + (*a2)->plainPrint(); + cout << "END" << endl; + } + } + } +} + +}; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/MatrixFinder.h b/src/sat/cryptominisat2/MatrixFinder.h index e69de29..293630b 100644 --- a/src/sat/cryptominisat2/MatrixFinder.h +++ b/src/sat/cryptominisat2/MatrixFinder.h @@ -0,0 +1,72 @@ +/*********************************************************************************** +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 +#ifdef _MSC_VER +#include +#else +#include +#endif //_MSC_VER + +#include "Clause.h" +#include "Solver.h" + +namespace MINISAT +{ +using namespace MINISAT; + +class Solver; + +using std::map; +using std::vector; +using std::pair; + +class MatrixFinder { + + public: + MatrixFinder(Solver& solver); + const bool findMatrixes(); + + private: + const uint setMatrixes(); + + struct mysorter + { + bool operator () (const pair& left, const pair& right) + { + return left.second < right.second; + } + }; + + 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; + + Solver& solver; +}; + +}; //NAMESPACE MINISAT + +#endif //MATRIXFINDER_H diff --git a/src/sat/cryptominisat2/MersenneTwister.h b/src/sat/cryptominisat2/MersenneTwister.h index e69de29..964ecc7 100644 --- a/src/sat/cryptominisat2/MersenneTwister.h +++ b/src/sat/cryptominisat2/MersenneTwister.h @@ -0,0 +1,427 @@ +// MersenneTwister.h +// Mersenne Twister random number generator -- a C++ class MTRand +// Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus +// Richard J. Wagner v1.0 15 May 2003 rjwagner@writeme.com + +// The Mersenne Twister is an algorithm for generating random numbers. It +// was designed with consideration of the flaws in various other generators. +// The period, 2^19937-1, and the order of equidistribution, 623 dimensions, +// are far greater. The generator is also fast; it avoids multiplication and +// division, and it benefits from caches and pipelines. For more information +// see the inventors' web page at http://www.math.keio.ac.jp/~matumoto/emt.html + +// Reference +// M. Matsumoto and T. Nishimura, "Mersenne Twister: A 623-Dimensionally +// Equidistributed Uniform Pseudo-Random Number Generator", ACM Transactions on +// Modeling and Computer Simulation, Vol. 8, No. 1, January 1998, pp 3-30. + +// Copyright (C) 1997 - 2002, Makoto Matsumoto and Takuji Nishimura, +// Copyright (C) 2000 - 2003, Richard J. Wagner +// All rights reserved. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions +// are met: +// +// 1. Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// +// 3. The names of its contributors may not be used to endorse or promote +// products derived from this software without specific prior written +// permission. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +// CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +// The original code included the following notice: +// +// When you use this, send an email to: matumoto@math.keio.ac.jp +// with an appropriate reference to your work. +// +// It would be nice to CC: rjwagner@writeme.com and Cokus@math.washington.edu +// when you write. + +#ifndef MERSENNETWISTER_H +#define MERSENNETWISTER_H + +#include +#include +#include +#include +#include + +namespace MINISAT +{ + +// Not thread safe (unless auto-initialization is avoided and each thread has +// its own MTRand object) + +class MTRand { +// Data +public: + typedef unsigned long uint32; // unsigned integer type, at least 32 bits + + enum { N = 624 }; // length of state vector + enum { SAVE = N + 1 }; // length of array for save() + +protected: + enum { M = 397 }; // period parameter + + uint32 state[N]; // internal state + uint32 *pNext; // next value to get from state + int left; // number of values left before reload needed + + +//Methods +public: + MTRand( const uint32& oneSeed ); // initialize with a simple uint32 + MTRand( uint32 *const bigSeed, uint32 const seedLength = N ); // or an array + MTRand(); // auto-initialize with /dev/urandom or time() and clock() + + // Do NOT use for CRYPTOGRAPHY without securely hashing several returned + // values together, otherwise the generator state can be learned after + // reading 624 consecutive values. + + // Access to 32-bit random numbers + double rand(); // real number in [0,1] + double rand( const double& n ); // real number in [0,n] + double randExc(); // real number in [0,1) + double randExc( const double& n ); // real number in [0,n) + double randDblExc(); // real number in (0,1) + double randDblExc( const double& n ); // real number in (0,n) + uint32 randInt(); // integer in [0,2^32-1] + uint32 randInt( const uint32& n ); // integer in [0,n] for n < 2^32 + double operator()() { return rand(); } // same as rand() + + // Access to 53-bit random numbers (capacity of IEEE double precision) + double rand53(); // real number in [0,1) + + // Access to nonuniform random number distributions + double randNorm( const double& mean = 0.0, const double& variance = 0.0 ); + + // Re-seeding functions with same behavior as initializers + void seed( const uint32 oneSeed ); + void seed( uint32 *const bigSeed, const uint32 seedLength = N ); + void seed(); + + // Saving and loading generator state + void save( uint32* saveArray ) const; // to array of size SAVE + void load( uint32 *const loadArray ); // from such array + friend std::ostream& operator<<( std::ostream& os, const MTRand& mtrand ); + friend std::istream& operator>>( std::istream& is, MTRand& mtrand ); + +protected: + void initialize( const uint32 oneSeed ); + void reload(); + uint32 hiBit( const uint32& u ) const { return u & 0x80000000UL; } + uint32 loBit( const uint32& u ) const { return u & 0x00000001UL; } + uint32 loBits( const uint32& u ) const { return u & 0x7fffffffUL; } + uint32 mixBits( const uint32& u, const uint32& v ) const + { return hiBit(u) | loBits(v); } + uint32 twist( const uint32& m, const uint32& s0, const uint32& s1 ) const + { return m ^ (mixBits(s0,s1)>>1) ^ (-loBit(s1) & 0x9908b0dfUL); } + static uint32 hash( time_t t, clock_t c ); +}; + + +inline MTRand::MTRand( const uint32& oneSeed ) + { seed(oneSeed); } + +inline MTRand::MTRand( uint32 *const bigSeed, const uint32 seedLength ) + { seed(bigSeed,seedLength); } + +inline MTRand::MTRand() + { seed(); } + +inline double MTRand::rand() + { return double(randInt()) * (1.0/4294967295.0); } + +inline double MTRand::rand( const double& n ) + { return rand() * n; } + +inline double MTRand::randExc() + { return double(randInt()) * (1.0/4294967296.0); } + +inline double MTRand::randExc( const double& n ) + { return randExc() * n; } + +inline double MTRand::randDblExc() + { return ( double(randInt()) + 0.5 ) * (1.0/4294967296.0); } + +inline double MTRand::randDblExc( const double& n ) + { return randDblExc() * n; } + +inline double MTRand::rand53() +{ + uint32 a = randInt() >> 5, b = randInt() >> 6; + return ( a * 67108864.0 + b ) * (1.0/9007199254740992.0); // by Isaku Wada +} + +inline double MTRand::randNorm( const double& mean, const double& variance ) +{ + // Return a real number from a normal (Gaussian) distribution with given + // mean and variance by Box-Muller method + double r = sqrt( -2.0 * log( 1.0-randDblExc()) ) * variance; + double phi = 2.0 * 3.14159265358979323846264338328 * randExc(); + return mean + r * cos(phi); +} + +inline MTRand::uint32 MTRand::randInt() +{ + // Pull a 32-bit integer from the generator state + // Every other access function simply transforms the numbers extracted here + + if( left == 0 ) reload(); + --left; + + register uint32 s1; + s1 = *pNext++; + s1 ^= (s1 >> 11); + s1 ^= (s1 << 7) & 0x9d2c5680UL; + s1 ^= (s1 << 15) & 0xefc60000UL; + return ( s1 ^ (s1 >> 18) ); +} + +inline MTRand::uint32 MTRand::randInt( const uint32& n ) +{ + // Find which bits are used in n + // Optimized by Magnus Jonsson (magnus@smartelectronix.com) + uint32 used = n; + used |= used >> 1; + used |= used >> 2; + used |= used >> 4; + used |= used >> 8; + used |= used >> 16; + + // Draw numbers until one is found in [0,n] + uint32 i; + do + i = randInt() & used; // toss unused bits to shorten search + while( i > n ); + return i; +} + + +inline void MTRand::seed( const uint32 oneSeed ) +{ + // Seed the generator with a simple uint32 + initialize(oneSeed); + reload(); +} + + +inline void MTRand::seed( uint32 *const bigSeed, const uint32 seedLength ) +{ + // Seed the generator with an array of uint32's + // There are 2^19937-1 possible initial states. This function allows + // all of those to be accessed by providing at least 19937 bits (with a + // default seed length of N = 624 uint32's). Any bits above the lower 32 + // in each element are discarded. + // Just call seed() if you want to get array from /dev/urandom + initialize(19650218UL); + register int i = 1; + register uint32 j = 0; + register int k = ( N > seedLength ? N : seedLength ); + for( ; k; --k ) + { + state[i] = + state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1664525UL ); + state[i] += ( bigSeed[j] & 0xffffffffUL ) + j; + state[i] &= 0xffffffffUL; + ++i; ++j; + if( i >= N ) { state[0] = state[N-1]; i = 1; } + if( j >= seedLength ) j = 0; + } + for( k = N - 1; k; --k ) + { + state[i] = + state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1566083941UL ); + state[i] -= i; + state[i] &= 0xffffffffUL; + ++i; + if( i >= N ) { state[0] = state[N-1]; i = 1; } + } + state[0] = 0x80000000UL; // MSB is 1, assuring non-zero initial array + reload(); +} + + +inline void MTRand::seed() +{ + // Seed the generator with an array from /dev/urandom if available + // Otherwise use a hash of time() and clock() values + + // First try getting an array from /dev/urandom + FILE* urandom = fopen( "/dev/urandom", "rb" ); + if( urandom ) + { + uint32 bigSeed[N]; + register uint32 *s = bigSeed; + register int i = N; + register bool success = true; + while( success && i-- ) + success = fread( s++, sizeof(uint32), 1, urandom ); + fclose(urandom); + if( success ) { seed( bigSeed, N ); return; } + } + + // Was not successful, so use time() and clock() instead + seed( hash( time(NULL), clock() ) ); +} + + +inline void MTRand::initialize( const uint32 seed ) +{ + // Initialize generator state with seed + // See Knuth TAOCP Vol 2, 3rd Ed, p.106 for multiplier. + // In previous versions, most significant bits (MSBs) of the seed affect + // only MSBs of the state array. Modified 9 Jan 2002 by Makoto Matsumoto. + register uint32 *s = state; + register uint32 *r = state; + register int i = 1; + *s++ = seed & 0xffffffffUL; + for( ; i < N; ++i ) + { + *s++ = ( 1812433253UL * ( *r ^ (*r >> 30) ) + i ) & 0xffffffffUL; + r++; + } +} + + +inline void MTRand::reload() +{ + // Generate N new values in state + // Made clearer and faster by Matthew Bellew (matthew.bellew@home.com) + register uint32 *p = state; + register int i; + for( i = N - M; i--; ++p ) + *p = twist( p[M], p[0], p[1] ); + for( i = M; --i; ++p ) + *p = twist( p[M-N], p[0], p[1] ); + *p = twist( p[M-N], p[0], state[0] ); + + left = N, pNext = state; +} + + +inline MTRand::uint32 MTRand::hash( time_t t, clock_t c ) +{ + // Get a uint32 from t and c + // Better than uint32(x) in case x is floating point in [0,1] + // Based on code by Lawrence Kirby (fred@genesis.demon.co.uk) + + static uint32 differ = 0; // guarantee time-based seeds will change + + uint32 h1 = 0; + unsigned char *p = (unsigned char *) &t; + for( size_t i = 0; i < sizeof(t); ++i ) + { + h1 *= UCHAR_MAX + 2U; + h1 += p[i]; + } + uint32 h2 = 0; + p = (unsigned char *) &c; + for( size_t j = 0; j < sizeof(c); ++j ) + { + h2 *= UCHAR_MAX + 2U; + h2 += p[j]; + } + return ( h1 + differ++ ) ^ h2; +} + + +inline void MTRand::save( uint32* saveArray ) const +{ + register uint32 *sa = saveArray; + register const uint32 *s = state; + register int i = N; + for( ; i--; *sa++ = *s++ ) {} + *sa = left; +} + + +inline void MTRand::load( uint32 *const loadArray ) +{ + register uint32 *s = state; + register uint32 *la = loadArray; + register int i = N; + for( ; i--; *s++ = *la++ ) {} + left = *la; + pNext = &state[N-left]; +} + + +inline std::ostream& operator<<( std::ostream& os, const MTRand& mtrand ) +{ + register const MTRand::uint32 *s = mtrand.state; + register int i = mtrand.N; + for( ; i--; os << *s++ << "\t" ) {} + return os << mtrand.left; +} + + +inline std::istream& operator>>( std::istream& is, MTRand& mtrand ) +{ + register MTRand::uint32 *s = mtrand.state; + register int i = mtrand.N; + for( ; i--; is >> *s++ ) {} + is >> mtrand.left; + mtrand.pNext = &mtrand.state[mtrand.N-mtrand.left]; + return is; +} +}; + +#endif // MERSENNETWISTER_H + +// Change log: +// +// v0.1 - First release on 15 May 2000 +// - Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus +// - Translated from C to C++ +// - Made completely ANSI compliant +// - Designed convenient interface for initialization, seeding, and +// obtaining numbers in default or user-defined ranges +// - Added automatic seeding from /dev/urandom or time() and clock() +// - Provided functions for saving and loading generator state +// +// v0.2 - Fixed bug which reloaded generator one step too late +// +// v0.3 - Switched to clearer, faster reload() code from Matthew Bellew +// +// v0.4 - Removed trailing newline in saved generator format to be consistent +// with output format of built-in types +// +// v0.5 - Improved portability by replacing static const int's with enum's and +// clarifying return values in seed(); suggested by Eric Heimburg +// - Removed MAXINT constant; use 0xffffffffUL instead +// +// v0.6 - Eliminated seed overflow when uint32 is larger than 32 bits +// - Changed integer [0,n] generator to give better uniformity +// +// v0.7 - Fixed operator precedence ambiguity in reload() +// - Added access for real numbers in (0,1) and (0,n) +// +// v0.8 - Included time.h header to properly support time_t and clock_t +// +// v1.0 - Revised seeding to match 26 Jan 2002 update of Nishimura and Matsumoto +// - Allowed for seeding with arrays of any length +// - Added access for real numbers in [0,1) with 53-bit resolution +// - Added access for real numbers from normal (Gaussian) distributions +// - Increased overall speed by optimizing twist() +// - Doubled speed of integer [0,n] generation +// - Fixed out-of-range number generation on 64-bit machines +// - Improved portability by substituting literal constants for long enum's +// - Changed license from GNU LGPL to BSD diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h index e69de29..02d5766 100644 --- a/src/sat/cryptominisat2/constants.h +++ b/src/sat/cryptominisat2/constants.h @@ -0,0 +1,46 @@ +/****************************************************************************************[Solver.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +glucose -- Gilles Audemard, Laurent Simon (2008) + +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. +**************************************************************************************************/ + +#define RATIOREMOVECLAUSES 3 +#define NBCLAUSESBEFOREREDUCE 20000 +#define DYNAMICNBLEVEL +#define UPDATEVARACTIVITY +#define FIXCLEANREPLACE 30U +#define PERCENTAGEPERFORMREPLACE 0.01 +#define PERCENTAGECLEANCLAUSES 0.01 +#define MAX_CLAUSENUM_XORFIND 5000000 +#define BINARY_TO_XOR_APPROX 4.0 +#define FULLRESTART_MULTIPLIER 250 +#define SIMPLIFY_MULTIPLIER 300 +#define FULLRESTART_MULTIPLIER_MULTIPLIER 3.5 +#define RESTART_TYPE_DECIDER_FROM 2 +#define RESTART_TYPE_DECIDER_UNTIL 7 +//#define VERBOSE_DEBUG_XOR +//#define VERBOSE_DEBUG +#define USE_GAUSS +#define MIN_GAUSS_XOR_CLAUSES 5 +#define MAX_GAUSS_XOR_CLAUSES 30000 +#define MAX_OLD_LEARNTS 2000000 +//#define DEBUG_ATTACH +#define RANDOM_LOOKAROUND_SEARCHSPACE +//#define USE_OLD_POLARITIES +//#define DEBUG_VARELIM +#define BURST_SEARCH +#define USE_POOLS -- 2.47.3