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