From: msoos Date: Mon, 30 Nov 2009 18:47:08 +0000 (+0000) Subject: Updating cryptominsat2 to revision r483. Multiple performance bugs fixed, glucose... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=71410d2e246e7229a9aad8cc140a4136608d8a23;p=francis%2Fstp.git Updating cryptominsat2 to revision r483. Multiple performance bugs fixed, glucose solver has been partially imported, and a memory leak has been fixed -- approx. 600 lines changed git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@432 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/Clause.cpp b/src/sat/cryptominisat2/Clause.cpp deleted file mode 100644 index 2566be1..0000000 --- a/src/sat/cryptominisat2/Clause.cpp +++ /dev/null @@ -1,47 +0,0 @@ -/***********************************************************************************[SolverTypes.h] -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#include "Clause.h" - -namespace MINISAT -{ - -Clause* Clause_new(const vec& ps, const uint group, const bool learnt) -{ - void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); - Clause* real= new (mem) Clause(ps, group, learnt); - return real; -} - -Clause* Clause_new(const vector& ps, const uint group, const bool learnt) -{ - void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); - Clause* real= new (mem) Clause(ps, group, learnt); - return real; -} - -Clause* Clause_new(const PackedRow& row, const vec& assigns, const vector& col_to_var_original, const uint group) -{ - const uint size = row.popcnt(); - void* mem = malloc(sizeof(Clause) + sizeof(Lit)*size); - Clause* real= new (mem) Clause(row, size, assigns, col_to_var_original, group); - return real; -} - -}; diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index c8ab10e..a6768f9 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -61,18 +61,10 @@ protected: 16th -31st bit 16bit int size */ uint32_t size_etc; - float act; + union { int act; uint32_t abst; } extra; Lit data[0]; public: - Clause(const PackedRow& row, const uint size, const vec& assigns, const vector& col_to_var_original, const uint _group) : - group(_group) - { - size_etc = 0; - setSize(size); - setLearnt(false); - row.fill(data, assigns, col_to_var_original); - } template Clause(const V& ps, const uint _group, const bool learnt) : @@ -82,7 +74,8 @@ public: setSize(ps.size()); setLearnt(learnt); for (uint i = 0; i < ps.size(); i++) data[i] = ps[i]; - if (learnt) act = 0; + if (learnt) extra.act = 0; + else calcAbstraction(); } // -- use this function instead: @@ -116,11 +109,33 @@ public: return data[i]; } - float& activity () { - return act; + void setActivity(int i) { + extra.act = i; + } + + const int& activity () const { + return extra.act; + } + + Lit subsumes (const Clause& other) const; + + inline void strengthen(const Lit p) + { + remove(*this, p); + calcAbstraction(); + } + + void calcAbstraction() { + uint32_t abstraction = 0; + for (int i = 0; i < size(); i++) + abstraction |= 1 << (data[i].var() & 31); + extra.abst = abstraction; } - Lit* getData () { + const Lit* getData () const { + return data; + } + Lit* getData () { return data; } void print() { @@ -204,9 +219,62 @@ protected: } }; -Clause* Clause_new(const vec& ps, const uint group, const bool learnt); -Clause* Clause_new(const vector& ps, const uint group, const bool learnt); -Clause* Clause_new(const PackedRow& ps, const vec& assigns, const vector& col_to_var_original, const uint group); +template +Clause* Clause_new(const T& ps, const uint group, const bool learnt = false) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} +//Clause* Clause_new(const vector& ps, const uint group, const bool learnt); + +/*_________________________________________________________________________________________________ +| +| subsumes : (other : const Clause&) -> Lit +| +| Description: +| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other' +| by subsumption resolution. +| +| Result: +| lit_Error - No subsumption or simplification +| lit_Undef - Clause subsumes 'other' +| p - The literal p can be deleted from 'other' +|________________________________________________________________________________________________@*/ +inline Lit Clause::subsumes(const Clause& other) const +{ + if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) + return lit_Error; + + Lit ret = lit_Undef; + const Lit* c = this->getData(); + const Lit* d = other.getData(); + + for (int i = 0; i < size(); i++) { + // search for c[i] or ~c[i] + for (int j = 0; j < other.size(); j++) + if (c[i] == d[j]) + goto ok; + else if (ret == lit_Undef && c[i] == ~d[j]){ + ret = c[i]; + goto ok; + } + + // did not find it + return lit_Error; + ok:; + } + + return ret; +} + + +class WatchedBin { + public: + WatchedBin(Clause *_clause, Lit _impliedLit) : impliedLit(_impliedLit), clause(_clause) {}; + Lit impliedLit; + Clause *clause; +}; }; #endif //CLAUSE_H diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index 4ae5dd2..0d7696c 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -209,6 +209,7 @@ bool Conglomerate::dealWithNewClause(vector& ps, const bool inverted, const #endif S->xorclauses.push(newX); + S->xorclauses_tofree.push(newX); toRemove.push_back(false); S->attachClause(*newX); for (const Lit * a = &((*newX)[0]), *end = a + newX->size(); a != end; a++) { diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index e35d667..c1b0d1b 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -34,8 +34,6 @@ using std::ostream; using std::cout; using std::endl; -uint64_t* PackedRow::tmp_row; - ostream& operator << (ostream& os, const vec& v) { for (int i = 0; i < v.size(); i++) { @@ -46,10 +44,11 @@ ostream& operator << (ostream& os, const vec& v) return os; } -Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _matrix_no) : +Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _matrix_no, const vector& _xorclauses) : solver(_solver) , config(_config) , matrix_no(_matrix_no) + , xorclauses(_xorclauses) , messed_matrix_vars_since_reversal(true) , gauss_last_level(0) , disabled(false) @@ -57,7 +56,6 @@ Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _m , useful_confl(0) , called(0) { - PackedRow::tmp_row = new uint64_t[1000]; } Gaussian::~Gaussian() @@ -65,6 +63,17 @@ Gaussian::~Gaussian() clear_clauses(); } +inline void Gaussian::set_matrixset_to_cur() +{ + uint level = solver.decisionLevel() / config.only_nth_gauss_save; + assert(level <= matrix_sets.size()); + + if (level == matrix_sets.size()) + matrix_sets.push_back(cur_matrixset); + else + matrix_sets[level] = cur_matrixset; +} + void Gaussian::clear_clauses() { std::for_each(matrix_clauses_toclear.begin(), matrix_clauses_toclear.end(), std::ptr_fun(free)); @@ -73,12 +82,6 @@ void Gaussian::clear_clauses() 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; @@ -106,47 +109,57 @@ llbool Gaussian::full_init() return l_Nothing; } -void Gaussian::init(void) +void Gaussian::init() { assert(solver.decisionLevel() == 0); - matrix_sets.clear(); - fill_matrix(); - if (origMat.num_rows == 0) return; + fill_matrix(cur_matrixset); + if (!cur_matrixset.num_rows || !cur_matrixset.num_cols) { + disabled = true; + badlevel = 0; + return; + } - cur_matrixset = origMat; - + matrix_sets.clear(); + matrix_sets.push_back(cur_matrixset); 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; + badlevel = UINT_MAX; #ifdef VERBOSE_DEBUG cout << "(" << matrix_no << ")Gaussian init finished." << endl; #endif } -uint Gaussian::select_columnorder(vector& var_to_col) +uint Gaussian::select_columnorder(vector& var_to_col, matrixset& origMat) { 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++) { + for (int i = 0; i != xorclauses.size(); i++) { #ifdef DEBUG_GAUSS - assert(!solver.satisfied(*solver.xorclauses[i])); + assert(xorclauses[i]->mark() || !solver.satisfied(*xorclauses[i])); #endif - if (solver.xorclauses[i]->getMatrix() == matrix_no) { + if (!xorclauses[i]->mark()) { num_xorclauses++; - XorClause& c = *solver.xorclauses[i]; + XorClause& c = *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[c[i2].var()] = unassigned_col - 1; } } } + + uint largest_used_var = 0; + for (uint i = 0; i < var_to_col.size(); i++) + if (var_to_col[i] != unassigned_col) + largest_used_var = i; var_to_col.resize(largest_used_var + 1); + + var_is_in.resize(var_to_col.size()); + var_is_in.setZero(); + origMat.var_is_set.resize(var_to_col.size()); + origMat.var_is_set.setZero(); origMat.col_to_var.clear(); for (int i = solver.order_heap.size()-1; i >= 0 ; i--) @@ -163,56 +176,41 @@ uint Gaussian::select_columnorder(vector& var_to_col) #endif origMat.col_to_var.push_back(v); - var_to_col[v] = 2; + var_to_col[v] = origMat.col_to_var.size()-1; + var_is_in.setBit(v); } } //for the ones that were not in the order_heap, but are marked in var_to_col - for (uint i = 0; i < var_to_col.size(); i++) { - if (var_to_col[i] == 1) - origMat.col_to_var.push_back(i); + for (uint v = 0; v != var_to_col.size(); v++) { + if (var_to_col[v] == unassigned_col - 1) { + origMat.col_to_var.push_back(v); + var_to_col[v] = origMat.col_to_var.size() -1; + var_is_in.setBit(v); + } } #ifdef VERBOSE_DEBUG cout << "(" << matrix_no << ")col_to_var:"; std::copy(origMat.col_to_var.begin(), origMat.col_to_var.end(), std::ostream_iterator(cout, ",")); cout << endl; - - cout << "(" << matrix_no << ")var_to_col:" << endl; #endif - var_is_in.resize(var_to_col.size()); - var_is_in.setZero(); - origMat.var_is_set.resize(var_to_col.size()); - origMat.var_is_set.setZero(); - for (uint i = 0; i < var_to_col.size(); i++) { - if (var_to_col[i] != unassigned_col) { - vector::iterator it = std::find(origMat.col_to_var.begin(), origMat.col_to_var.end(), i); - assert(it != origMat.col_to_var.end()); - var_to_col[i] = &(*it) - &origMat.col_to_var[0]; - var_is_in.setBit(i); - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")var_to_col[" << i << "]:" << var_to_col[i] << endl; - #endif - } - } - return num_xorclauses; } -void Gaussian::fill_matrix() +void Gaussian::fill_matrix(matrixset& origMat) { #ifdef VERBOSE_DEBUG cout << "(" << matrix_no << ")Filling matrix" << endl; #endif vector var_to_col; - origMat.num_rows = select_columnorder(var_to_col); + origMat.num_rows = select_columnorder(var_to_col, origMat); origMat.num_cols = origMat.col_to_var.size(); col_to_var_original = origMat.col_to_var; changed_rows.resize(origMat.num_rows); 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); @@ -228,10 +226,10 @@ void Gaussian::fill_matrix() #endif uint matrix_row = 0; - for (int i = 0; i < solver.xorclauses.size(); i++) { - const XorClause& c = *solver.xorclauses[i]; + for (int i = 0; i < xorclauses.size(); i++) { + const XorClause& c = *xorclauses[i]; - if (c.getMatrix() == matrix_no) { + if (!c.mark()) { 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++; @@ -276,7 +274,7 @@ void Gaussian::update_matrix_col(matrixset& m, const Var var, const uint col) #ifdef DEBUG_GAUSS bool c = false; - for(PackedMatrix::iterator r = m.matrix.begin(), end = r + m.matrix.size(); r != end; ++r) + for(PackedMatrix::iterator r = m.matrix.begin(), end = r + m.matrix.getSize(); r != end; ++r) c |= (*r)[col]; assert(!c); #endif @@ -295,15 +293,15 @@ void Gaussian::update_matrix_by_col_all(matrixset& m) #endif #ifdef DEBUG_GAUSS - assert(config.every_nth_gauss != 1 || nothing_to_propagate(cur_matrixset)); - assert(check_last_one_in_cols(m)); + assert(nothing_to_propagate(cur_matrixset)); + assert(solver.decisionLevel() == 0 || 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++) { + for (const Var *it = &m.col_to_var[0], *end = it + m.num_cols; it != end; col++, it++) { if (*it != unassigned_var && solver.assigns[*it].isDef()) { update_matrix_col(m, *it, col); last++; @@ -314,10 +312,10 @@ void Gaussian::update_matrix_by_col_all(matrixset& m) last = 0; } m.num_cols -= last; - m.past_the_end_last_one_in_col -= last; + m.past_the_end_last_one_in_col = std::min(m.past_the_end_last_one_in_col, (uint16_t)m.num_cols); #ifdef DEBUG_GAUSS - check_matrix_against_varset(m.matrix, m.varset); + check_matrix_against_varset(m.matrix, m.varset, m); #endif #ifdef VERBOSE_DEBUG @@ -334,55 +332,50 @@ void Gaussian::update_matrix_by_col_all(matrixset& m) Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl) { - if (origMat.num_rows == 0) return nothing; + if (solver.decisionLevel() >= badlevel) + return nothing; - if (!messed_matrix_vars_since_reversal) { + if (messed_matrix_vars_since_reversal) { #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")matrix needs only update" << endl; + cout << "(" << matrix_no << ")matrix needs copy before 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); + const uint level = solver.decisionLevel() / config.only_nth_gauss_save; + assert(level < matrix_sets.size()); + cur_matrixset = matrix_sets[level]; } - if (!cur_matrixset.num_cols || !cur_matrixset.num_cols) - return nothing; + update_matrix_by_col_all(cur_matrixset); messed_matrix_vars_since_reversal = false; gauss_last_level = solver.trail.size(); + badlevel = UINT_MAX; propagatable_rows.clear(); - uint conflict_row = UINT_MAX; uint last_row = eliminate(cur_matrixset, conflict_row); #ifdef DEBUG_GAUSS - check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset.varset); + check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset.varset, cur_matrixset); #endif gaussian_ret ret; - if (conflict_row != UINT_MAX) { + //There is no early abort, so this is unneeded + /*if (conflict_row != UINT_MAX) { uint maxlevel = UINT_MAX; uint size = UINT_MAX; uint best_row = UINT_MAX; analyse_confl(cur_matrixset, conflict_row, maxlevel, size, best_row); ret = handle_matrix_confl(confl, cur_matrixset, size, maxlevel, best_row); - - } else { + } else {*/ ret = handle_matrix_prop_and_confl(cur_matrixset, last_row, confl); + //} + + if (!cur_matrixset.num_cols || !cur_matrixset.num_rows) { + badlevel = solver.decisionLevel(); + return nothing; } - if (ret == nothing - && (solver.decisionLevel() == 0 || ((solver.decisionLevel() - config.decision_from) % config.only_nth_gauss_save == 0)) - ) + if (ret == nothing && + solver.decisionLevel() % config.only_nth_gauss_save == 0) set_matrixset_to_cur(); #ifdef VERBOSE_DEBUG @@ -419,7 +412,7 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) #ifdef DEBUG_GAUSS - assert(check_last_one_in_cols(m)); + assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m)); #endif uint i = 0; @@ -467,6 +460,7 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) if (this_matrix_row != end) { PackedRow matrix_row_i = m.matrix[i]; PackedRow varset_row_i = m.varset[i]; + PackedMatrix::iterator this_varset_row = m.varset.begin() + best_row; //swap rows i and maxi, but do not change the value of i; if (i != best_row) { @@ -474,12 +468,13 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) no_exchanged++; #endif - if (!matrix_row_i.get_xor_clause_inverted() && matrix_row_i.isZero()) { - conflict_row = i; - return 0; - } + //Would early abort, but would not find the best conflict (and would be expensive) + //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]); + varset_row_i.swap(*this_varset_row); } #ifdef DEBUG_GAUSS assert(m.matrix[i].popcnt(j) == m.matrix[i].popcnt()); @@ -490,17 +485,18 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) 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]) { + ++this_matrix_row; + ++this_varset_row; + for (; this_matrix_row != end; ++this_matrix_row, ++this_varset_row) if ((*this_matrix_row)[j]) { //subtract row i from row u; //Now A[u,j] will be 0, since A[u,j] - A[i,j] = A[u,j] -1 = 0. #ifdef VERBOSE_DEBUG number_of_row_additions++; #endif - *it ^= matrix_row_i; - *it2 ^= varset_row_i; - //Would early abort, but would not find the best conflict: + *this_matrix_row ^= matrix_row_i; + *this_varset_row ^= varset_row_i; + //Would early abort, but would not find the best conflict (and would be expensive) //if (!it->get_xor_clause_inverted() &&it->isZero()) { // conflict_row = i2; // return 0; @@ -538,7 +534,7 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) #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); + assert(m.col_to_var[col] == unassigned_var || std::min(m.last_one_in_col[col]-1, (int)m.num_rows) == row); continue; } row++; @@ -552,7 +548,8 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(Clause*& confl, const matri { assert(best_row != UINT_MAX); - confl = Clause_new(m.varset[best_row], solver.assigns, col_to_var_original, solver.learnt_clause_group++); + m.varset[best_row].fill(tmp_clause, solver.assigns, col_to_var_original); + confl = Clause_new(tmp_clause, solver.learnt_clause_group++, false); Clause& cla = *confl; if (solver.dynamic_behaviour_analysis) solver.logger.set_group_name(confl->group, "learnt gauss clause"); @@ -754,7 +751,8 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row cout << endl; #endif - Clause& cla = *Clause_new(m.varset[row], solver.assigns, col_to_var_original, solver.learnt_clause_group++); + m.varset[row].fill(tmp_clause, solver.assigns, col_to_var_original); + Clause& cla = *Clause_new(tmp_clause, solver.learnt_clause_group++, false); #ifdef VERBOSE_DEBUG cout << "(" << matrix_no << ")matrix prop clause: "; solver.printClause(cla); @@ -970,24 +968,25 @@ const bool Gaussian::nothing_to_propagate(matrixset& m) const 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; + const uint last = std::min(m.last_one_in_col[i] - 1, (int)m.num_rows); uint real_last = 0; - uint i2; + uint i2 = 0; 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; + if (real_last > last) + return false; } return true; } -const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset) const +const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset, const matrixset& m) const { - assert(matrix.size() == varset.size()); + assert(matrix.getSize() == varset.getSize()); - for (uint i = 0; i < matrix.size(); i++) { + for (uint i = 0; i < matrix.getSize(); i++) { const PackedRow mat_row = matrix[i]; const PackedRow var_row = varset[i]; @@ -1002,10 +1001,16 @@ const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMat if (solver.assigns[var] == l_True) { assert(!mat_row[col]); + assert(m.col_to_var[col] == unassigned_var); + assert(m.var_is_set[var]); final = !final; } else if (solver.assigns[var] == l_False) { assert(!mat_row[col]); + assert(m.col_to_var[col] == unassigned_var); + assert(m.var_is_set[var]); } else if (solver.assigns[var] == l_Undef) { + assert(m.col_to_var[col] != unassigned_var); + assert(!m.var_is_set[var]); assert(mat_row[col]); } else assert(false); diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h index 6f5461e..4730adf 100644 --- a/src/sat/cryptominisat2/Gaussian.h +++ b/src/sat/cryptominisat2/Gaussian.h @@ -43,7 +43,7 @@ static const Var unassigned_var = -1; class Gaussian { public: - Gaussian(Solver& solver, const GaussianConfig& config, const uint matrix_no); + Gaussian(Solver& solver, const GaussianConfig& config, const uint matrix_no, const vector& xorclauses); ~Gaussian(); llbool full_init(); @@ -70,12 +70,14 @@ protected: //Gauss high-level configuration const GaussianConfig& config; const uint matrix_no; + vector xorclauses; enum gaussian_ret {conflict, unit_conflict, propagation, unit_propagation, nothing}; gaussian_ret gaussian(Clause*& confl); - vector col_to_var_original; - BitArray var_is_in; + vector col_to_var_original; //Matches columns to variables + BitArray var_is_in; //variable is part of the the matrix. var_is_in's size is _minimal_ so you should check whether var_is_in.getSize() < var before issuing var_is_in[var] + uint badlevel; class matrixset { @@ -83,25 +85,23 @@ protected: PackedMatrix matrix; // The matrix, updated to reflect variable assignements PackedMatrix varset; // The matrix, without variable assignements. The xor-clause is read from here. This matrix only follows the 'matrix' with its row-swap, row-xor, and row-delete operations. BitArray var_is_set; - vector col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives UINT_MAX if the COL has been zeroed (i.e. the variable assigned) + vector col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives unassigned_var if the COL has been zeroed (i.e. the variable assigned) uint16_t num_rows; // number of active rows in the matrix. Unactive rows are rows that contain only zeros (and if they are conflicting, then the conflict has been treated) uint num_cols; // number of active columns in the matrix. The columns at the end that have all be zeroed are no longer active int least_column_changed; // when updating the matrix, this value contains the smallest column number that has been updated (Gauss elim. can start from here instead of from column 0) uint16_t past_the_end_last_one_in_col; - vector last_one_in_col; //last_one_in_col[COL] tells the last row that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row) + vector last_one_in_col; //last_one_in_col[COL] tells the last row+1 that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row) uint removeable_cols; // the number of columns that have been zeroed out (i.e. assigned) }; //Saved states vector matrix_sets; // The matrixsets for depths 'decision_from' + 0, 'decision_from' + only_nth_gaussian_save, 'decision_from' + 2*only_nth_gaussian_save, ... 'decision_from' + 'decision_until'. - matrixset origMat; // The matrixset at depth 0 of the search tree matrixset cur_matrixset; // The current matrixset, i.e. the one we are working on, or the last one we worked on //Varibales to keep Gauss state bool messed_matrix_vars_since_reversal; int gauss_last_level; vector matrix_clauses_toclear; - bool went_below_decision_from; bool disabled; // Gauss is disabled //State of current elimnation @@ -115,8 +115,8 @@ protected: //gauss init functions void init(); // Initalise gauss state - void fill_matrix(); // Fills the origMat matrix - uint select_columnorder(vector& var_to_col); // Fills var_to_col and col_to_var of the origMat matrix. + void fill_matrix(matrixset& origMat); // Fills the origMat matrix + uint select_columnorder(vector& var_to_col, matrixset& origMat); // Fills var_to_col and col_to_var of the origMat matrix. //Main function uint eliminate(matrixset& matrix, uint& conflict_row); //does the actual gaussian elimination @@ -133,6 +133,7 @@ protected: 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' + vec tmp_clause; //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 @@ -153,18 +154,13 @@ private: void print_matrix_row(const T& row) const; // Print matrix row 'row' template void print_matrix_row_with_assigns(const T& row) const; - const bool check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset) const; + const bool check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset, const matrixset& m) 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); @@ -174,9 +170,7 @@ inline bool Gaussian::should_check_gauss(const uint decisionlevel, const uint st { return (!disabled && starts >= config.starts_from - && decisionlevel < config.decision_until - && decisionlevel >= config.decision_from - && decisionlevel % config.every_nth_gauss == 0); + && decisionlevel < config.decision_until); } inline void Gaussian::canceling(const uint level, const Var var) @@ -195,27 +189,6 @@ inline void Gaussian::print_matrix_stats() const cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl; } -inline void Gaussian::set_matrixset_to_cur() -{ - /*cout << solver.decisionLevel() << endl; - cout << decision_from << endl; - cout << matrix_sets.size() << endl;*/ - - if (solver.decisionLevel() == 0) { - origMat = cur_matrixset; - } - - if (solver.decisionLevel() >= config.decision_from) { - uint level = ((solver.decisionLevel() - config.decision_from) / config.only_nth_gauss_save); - - assert(level <= matrix_sets.size()); //TODO check if we need this, or HOW we need this in a multi-matrix setting - if (level == matrix_sets.size()) - matrix_sets.push_back(cur_matrixset); - else - matrix_sets[level] = cur_matrixset; - } -} - std::ostream& operator << (std::ostream& os, const vec& v); }; diff --git a/src/sat/cryptominisat2/GaussianConfig.h b/src/sat/cryptominisat2/GaussianConfig.h index 449b03e..cc60c80 100644 --- a/src/sat/cryptominisat2/GaussianConfig.h +++ b/src/sat/cryptominisat2/GaussianConfig.h @@ -19,6 +19,11 @@ along with this program. If not, see . #define GAUSSIANCONFIG_H #include +#include "PackedRow.h" + +namespace MINISAT +{ +using namespace MINISAT; class GaussianConfig { @@ -26,19 +31,22 @@ class GaussianConfig GaussianConfig() : only_nth_gauss_save(2) - , decision_from(0) , decision_until(0) - , every_nth_gauss(1) , starts_from(3) { + if (PackedRow::tmp_row == NULL) + PackedRow::tmp_row = new uint64_t[1000]; + } + + ~GaussianConfig() + { + delete[] PackedRow::tmp_row; } //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 +}; +#endif //GAUSSIANCONFIG_H diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index bb15f2d..dd7b23b 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -43,8 +43,8 @@ namespace MINISAT Logger::Logger(int& _verbosity) : proof_graph_on(false) - , statistics_on(false) , mini_proof(false) + , statistics_on(false) , max_print_lines(20) , uniqueid(1) @@ -165,8 +165,8 @@ void Logger::first_begin() void Logger::begin() { if (proof_graph_on) { - char filename[80]; - sprintf(filename, "proofs/%d-proof%d.dot", runid, S->starts); + std::stringstream filename; + filename << "proofs/" << runid << "-proof" << S->starts << ".dot"; if (S->starts == 0) history.push_back(uniqueid); @@ -177,8 +177,8 @@ void Logger::begin() 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); + proof = fopen(filename.str().c_str(),"w"); + if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename.str().c_str()), exit(-1); fprintf(proof, "digraph G {\n"); fprintf(proof,"node%d [shape=circle, label=\"BEGIN\", root];\n", history[history.size()-1]); } diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h index 2917b98..2564303 100644 --- a/src/sat/cryptominisat2/Logger.h +++ b/src/sat/cryptominisat2/Logger.h @@ -56,7 +56,7 @@ public: 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 prop_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 }; diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index 67c8931..b375538 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -2,7 +2,7 @@ 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 +SOURCES = 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 diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp index bc36445..ba1e552 100644 --- a/src/sat/cryptominisat2/MatrixFinder.cpp +++ b/src/sat/cryptominisat2/MatrixFinder.cpp @@ -41,8 +41,8 @@ using std::endl; //#define PART_FINDING MatrixFinder::MatrixFinder(Solver *_S) : - S(_S) - , unAssigned(_S->nVars() + 1) + unAssigned(_S->nVars() + 1) + , S(_S) { table.resize(S->nVars(), unAssigned); matrix_no = 0; @@ -122,7 +122,10 @@ const uint MatrixFinder::findMatrixes() const uint MatrixFinder::setMatrixes() { - vector numXorInMatrix(matrix_no, 0); + vector > numXorInMatrix; + for (uint i = 0; i < matrix_no; i++) + numXorInMatrix.push_back(std::make_pair(i, 0)); + vector sumXorSizeInMatrix(matrix_no, 0); vector > xorSizesInMatrix(matrix_no); vector > xorsInMatrix(matrix_no); @@ -134,9 +137,10 @@ const uint MatrixFinder::setMatrixes() for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) { XorClause& x = **c; const uint matrix = table[x[0].var()]; + assert(matrix < matrix_no); //for stats - numXorInMatrix[matrix]++; + numXorInMatrix[matrix].second++; sumXorSizeInMatrix[matrix] += x.size(); xorSizesInMatrix[matrix].push_back(x.size()); xorsInMatrix[matrix].push_back(&x); @@ -146,54 +150,46 @@ const uint MatrixFinder::setMatrixes() #endif //PART_FINDING } + std::sort(numXorInMatrix.begin(), numXorInMatrix.end(), mysorter()); + #ifdef PART_FINDING for (uint i = 0; i < matrix_no; i++) findParts(xorFingerprintInMatrix[i], xorsInMatrix[i]); #endif //PART_FINDING uint realMatrixNum = 0; - vector remapMatrixes(matrix_no, UINT_MAX); - for (uint i = 0; i < matrix_no; i++) { - if (numXorInMatrix[i] < 3) + for (int a = matrix_no-1; a != -1; a--) { + uint i = numXorInMatrix[a].first; + + if (numXorInMatrix[a].second < 3) continue; - const uint totalSize = reverseTable[i].size()*numXorInMatrix[i]; + const uint totalSize = reverseTable[i].size()*numXorInMatrix[a].second; const double density = (double)sumXorSizeInMatrix[i]/(double)totalSize*100.0; - double avg = (double)sumXorSizeInMatrix[i]/(double)numXorInMatrix[i]; + double avg = (double)sumXorSizeInMatrix[i]/(double)numXorInMatrix[a].second; double variance = 0.0; for (uint i2 = 0; i2 < xorSizesInMatrix[i].size(); i2++) variance += pow((double)xorSizesInMatrix[i][i2]-avg, 2); variance /= xorSizesInMatrix.size(); const double stdDeviation = sqrt(variance); - if (numXorInMatrix[i] >= 20 - && numXorInMatrix[i] <= 1000 - && realMatrixNum < (1 << 12)) + if (numXorInMatrix[a].second >= 20 + && numXorInMatrix[a].second <= 1000 + && realMatrixNum < 3) { cout << "| Matrix no " << std::setw(4) << realMatrixNum; - remapMatrixes[i] = realMatrixNum; + S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, realMatrixNum, xorsInMatrix[i])); realMatrixNum++; + } else { cout << "| Unused Matrix "; } - cout << std::setw(5) << numXorInMatrix[i] << " x" << std::setw(5) << reverseTable[i].size(); + cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size(); cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%"; cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg; cout << " stdev:" << std::setw(6) << std::fixed << std::setprecision(2) << stdDeviation << " |" << endl; } - 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; } diff --git a/src/sat/cryptominisat2/MatrixFinder.h b/src/sat/cryptominisat2/MatrixFinder.h index 1d3e4bc..f4b6aaf 100644 --- a/src/sat/cryptominisat2/MatrixFinder.h +++ b/src/sat/cryptominisat2/MatrixFinder.h @@ -30,6 +30,7 @@ class Solver; using std::map; using std::vector; +using std::pair; class MatrixFinder { @@ -40,6 +41,14 @@ class MatrixFinder { private: const uint setMatrixes(); + struct mysorter + { + bool operator () (const pair& left, const pair& right) + { + return left.second < right.second; + } + }; + void findParts(vector& xorFingerprintInMatrix, vector& xorsInMatrix); inline const Var fingerprint(const XorClause& c) const; inline const bool firstPartOfSecond(const XorClause& c1, const XorClause& c2) const; diff --git a/src/sat/cryptominisat2/PackedMatrix.h b/src/sat/cryptominisat2/PackedMatrix.h index 9f4178e..602f54e 100644 --- a/src/sat/cryptominisat2/PackedMatrix.h +++ b/src/sat/cryptominisat2/PackedMatrix.h @@ -44,8 +44,12 @@ public: numRows(b.numRows) , numCols(b.numCols) { + #ifdef DEBUG_MATRIX + assert(b.numRows > 0 && b.numCols > 0); + #endif + mp = new uint64_t[numRows*(numCols+1)]; - std::copy(b.mp, b.mp+numRows*(numCols+1), mp); + memcpy(mp, b.mp, sizeof(uint64_t)*numRows*(numCols+1)); } ~PackedMatrix() @@ -66,19 +70,27 @@ public: void resizeNumRows(const uint num_rows) { + #ifdef DEBUG_MATRIX + assert(num_rows <= numRows); + #endif + numRows = num_rows; } PackedMatrix& operator=(const PackedMatrix& b) { - if (b.numRows*(b.numCols+1) > numRows*(numCols+1)) { + #ifdef DEBUG_MATRIX + //assert(b.numRows > 0 && b.numCols > 0); + #endif + + if (numRows*(numCols+1) < b.numRows*(b.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); + memcpy(mp, b.mp, sizeof(uint64_t)*numRows*(numCols+1)); return *this; } @@ -216,7 +228,7 @@ public: return const_iterator(mp+numRows*(numCols+1), numCols); }*/ - inline const uint size() const + inline const uint getSize() const { return numRows; } diff --git a/src/sat/cryptominisat2/PackedRow.cpp b/src/sat/cryptominisat2/PackedRow.cpp index 8bdd638..b4f10a4 100644 --- a/src/sat/cryptominisat2/PackedRow.cpp +++ b/src/sat/cryptominisat2/PackedRow.cpp @@ -2,6 +2,8 @@ namespace MINISAT { +__thread uint64_t* PackedRow::tmp_row = NULL; + std::ostream& operator << (std::ostream& os, const PackedRow& m) { for(uint i = 0; i < m.size*64; i++) { @@ -125,11 +127,11 @@ PackedRow& PackedRow::operator^=(const PackedRow& b) return *this; } -void PackedRow::fill(Lit* ps, const vec& assigns, const vector& col_to_var_original) const +void PackedRow::fill(vec& tmp_clause, const vec& assigns, const vector& col_to_var_original) const { bool final = xor_clause_inverted; - Lit* ps_first = ps; + tmp_clause.clear(); uint col = 0; bool wasundef = false; for (uint i = 0; i < size; i++) for (uint i2 = 0; i2 < 64; i2++) { @@ -137,23 +139,22 @@ void PackedRow::fill(Lit* ps, const vec& assigns, const vector& col_ const uint& var = col_to_var_original[col]; assert(var != UINT_MAX); - const lbool val = assigns[var]; + const lbool& val = assigns[var]; const bool val_bool = val.getBool(); - *ps = Lit(var, val_bool); + tmp_clause.push(Lit(var, val_bool)); final ^= val_bool; if (val.isUndef()) { assert(!wasundef); - Lit tmp(*ps_first); - *ps_first = *ps; - *ps = tmp; + Lit tmp(tmp_clause[0]); + tmp_clause[0] = tmp_clause.last(); + tmp_clause.last() = tmp; wasundef = true; } - ps++; } col++; } if (wasundef) { - *ps_first ^= final; + tmp_clause[0] ^= final; //assert(ps != ps_first+1); } else assert(!final); diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h index 2ea84fd..795f0c1 100644 --- a/src/sat/cryptominisat2/PackedRow.h +++ b/src/sat/cryptominisat2/PackedRow.h @@ -126,7 +126,7 @@ public: xor_clause_inverted = v.xor_clause_inverted(); } - void fill(Lit* ps, const vec& assigns, const vector& col_to_var_original) const; + void fill(vec& tmp_clause, const vec& assigns, const vector& col_to_var_original) const; inline unsigned long int scan(const unsigned long int var) const { @@ -141,14 +141,14 @@ public: friend std::ostream& operator << (std::ostream& os, const PackedRow& m); - static uint64_t *tmp_row; + static __thread 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) + , xor_clause_inverted(_xor_clause_inverted) {} const uint size; diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index dc62f77..73607d7 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -1,6 +1,7 @@ /****************************************************************************************[Solver.C] MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson CryptoMiniSat -- Copyright (c) 2009 Mate Soos +glucose -- Gilles Audemard, Laurent Simon (2008) Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, @@ -46,8 +47,8 @@ using namespace MINISAT; 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) + var_decay(1 / 0.95), random_var_freq(0.02) + , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1) // More parameters: // @@ -55,17 +56,24 @@ Solver::Solver() : , polarity_mode (polarity_user) , verbosity (0) , restrictedPickBranch(0) - , useRealUnknowns(false) + , useRealUnknowns (false) , xorFinder (true) + , greedyUnbound (false) // Statistics: (formerly in 'SolverStats') // + , nbDL2(0), nbBin(0), nbReduceDB(0) , 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) + + , curRestart (1) + , conf4Stats (0) + , nbclausesbeforereduce (NBCLAUSESBEFOREREDUCE) + , qhead (0) , simpDB_assigns (-1) , simpDB_props (0) @@ -76,8 +84,8 @@ Solver::Solver() : , logger(verbosity) , dynamic_behaviour_analysis(false) //do not document the proof as default , maxRestarts(UINT_MAX) + , MYFLAG (0) , learnt_clause_group(0) - , greedyUnbound(false) { toReplace = new VarReplacer(this); conglomerate = new Conglomerate(this); @@ -90,7 +98,7 @@ 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 (int i = 0; i < xorclauses_tofree.size(); i++) free(xorclauses_tofree[i]); for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; gauss_matrixes.clear(); delete toReplace; @@ -105,15 +113,18 @@ Solver::~Solver() // 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(); + Var v = nVars(); watches .push(); // (list for positive literal) watches .push(); // (list for negative literal) + binwatches.push(); // (list for positive literal) + binwatches.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); + permDiff .push(0); polarity .push_back((char)sign); decision_var.push_back(dvar); @@ -141,7 +152,6 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro 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(); @@ -186,6 +196,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro XorClause* c = XorClause_new(ps, xor_clause_inverted, group); xorclauses.push(c); + xorclauses_tofree.push(c); attachClause(*c); break; } @@ -209,8 +220,6 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) 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) @@ -219,7 +228,8 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) ps.shrink(i - j); if (ps.size() == 0) { - if (dynamic_behaviour_analysis) logger.empty_clause(group); + if (dynamic_behaviour_analysis) + logger.empty_clause(group); return ok = false; } else if (ps.size() == 1) { assert(value(ps[0]) == l_Undef); @@ -241,7 +251,7 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) void Solver::attachClause(XorClause& c) { - assert(c.size() > 1); + assert(c.size() > 2); xorwatches[c[0].var()].push(&c); xorwatches[c[1].var()].push(&c); @@ -253,9 +263,16 @@ void Solver::attachClause(XorClause& c) void Solver::attachClause(Clause& c) { assert(c.size() > 1); - - watches[(~c[0]).toInt()].push(&c); - watches[(~c[1]).toInt()].push(&c); + int index0 = (~c[0]).toInt(); + int index1 = (~c[1]).toInt(); + + if (c.size() == 2) { + binwatches[index0].push(WatchedBin(&c, c[1])); + binwatches[index1].push(WatchedBin(&c, c[0])); + } else { + watches[index0].push(&c); + watches[index1].push(&c); + } if (c.learnt()) learnts_literals += c.size(); else clauses_literals += c.size(); @@ -277,10 +294,20 @@ void Solver::detachClause(const XorClause& c) 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.size() == 2) { + assert(findWatchedBinCl(binwatches[(~c[0]).toInt()], &c)); + assert(findWatchedBinCl(binwatches[(~c[1]).toInt()], &c)); + + removeWatchedBinCl(binwatches[(~c[0]).toInt()], &c); + removeWatchedBinCl(binwatches[(~c[1]).toInt()], &c); + } else { + assert(findWatchedCl(watches[(~c[0]).toInt()], &c)); + assert(findWatchedCl(watches[(~c[1]).toInt()], &c)); + + removeWatchedCl(watches[(~c[0]).toInt()], &c); + removeWatchedCl(watches[(~c[1]).toInt()], &c); + } + if (c.learnt()) learnts_literals -= c.size(); else clauses_literals -= c.size(); } @@ -288,10 +315,18 @@ void Solver::detachClause(const Clause& c) 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 (origSize == 2) { + assert(findWatchedBinCl(binwatches[(~lit1).toInt()], address)); + assert(findWatchedBinCl(binwatches[(~lit2).toInt()], address)); + removeWatchedBinCl(binwatches[(~lit1).toInt()], address); + removeWatchedBinCl(binwatches[(~lit2).toInt()], address); + } else { + 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; } @@ -341,8 +376,6 @@ void Solver::cancelUntil(int level) 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 @@ -407,11 +440,6 @@ 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: @@ -497,7 +525,7 @@ Lit Solver::pickBranchLit(int polarity_mode) | Effect: | Will undo part of the trail, upto but not beyond the assumption of the current decision level. |________________________________________________________________________________________________@*/ -void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) +void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int &nbLevels/*, int &merged*/) { int pathC = 0; Lit p = lit_Undef; @@ -511,9 +539,8 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) do { assert(confl != NULL); // (otherwise should be UIP) Clause& c = *confl; - - if (c.learnt()) - claBumpActivity(c); + if (p != lit_Undef) + reverse_binary_clause(c); for (uint j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) { const Lit& q = c[j]; @@ -523,9 +550,13 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) if (!useRealUnknowns || (my_var < realUnknowns.size() && realUnknowns[my_var])) varBumpActivity(my_var); seen[my_var] = 1; - if (level[my_var] >= decisionLevel()) + if (level[my_var] >= decisionLevel()) { pathC++; - else { + #ifdef UPDATEVARACTIVITY + if ( reason[q.var()] != NULL && reason[q.var()]->learnt() ) + lastDecisionLevel.push(q); + #endif + } else { out_learnt.push(q); if (level[my_var] > out_btlevel) out_btlevel = level[my_var]; @@ -558,7 +589,9 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) } else { out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++) { - const Clause& c = *reason[out_learnt[i].var()]; + Clause& c = *reason[out_learnt[i].var()]; + reverse_binary_clause(c); + for (uint k = 1; k < c.size(); k++) if (!seen[c[k].var()] && level[c[k].var()] > 0) { out_learnt[j++] = out_learnt[i]; @@ -585,6 +618,26 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) out_btlevel = level[p.var()]; } + nbLevels = 0; + MYFLAG++; + for(int i = 0; i < out_learnt.size(); i++) { + int lev = level[out_learnt[i].var()]; + if (permDiff[lev] != MYFLAG) { + permDiff[lev] = MYFLAG; + nbLevels++; + //merged += nbPropagated(lev); + } + } + + #ifdef UPDATEVARACTIVITY + if (lastDecisionLevel.size() > 0) { + for(int i = 0; iactivity() < nbLevels) + varBumpActivity(lastDecisionLevel[i].var()); + } + lastDecisionLevel.clear(); + } + #endif for (int j = 0; j < analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared) } @@ -599,7 +652,9 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) 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()]; + Clause& c = *reason[analyze_stack.last().var()]; + reverse_binary_clause(c); + analyze_stack.pop(); for (uint i = 1; i < c.size(); i++) { @@ -704,6 +759,22 @@ Clause* Solver::propagate(const bool xor_as_well) Clause **i, **j, **end; num_props++; + //First propagate binary clauses + vec & wbin = binwatches[p.toInt()]; + for(WatchedBin *k = wbin.getData(), *end = k + wbin.size(); k != end; k++) { + Lit imp = k->impliedLit; + lbool val = value(imp); + if (val == l_False) + return k->clause; + if (val == l_Undef) { + uncheckedEnqueue(imp, k->clause); + if (dynamic_behaviour_analysis) + logger.propagation(imp, Logger::simple_propagation_type, k->clause->group); + } + } + + //Next, propagate normal clauses + #ifdef VERBOSE_DEBUG cout << "Propagating lit " << (p.sign() ? '-' : ' ') << p.var()+1 << endl; #endif @@ -724,7 +795,7 @@ Clause* Solver::propagate(const bool xor_as_well) *j++ = &c; } else { // Look for new watch: - for (uint k = 2; k < c.size(); k++) + for (uint k = 2; k != c.size(); k++) if (value(c[k]) != l_False) { c[1] = c[k]; c[k] = false_lit; @@ -744,6 +815,22 @@ Clause* Solver::propagate(const bool xor_as_well) uncheckedEnqueue(first, &c); if (dynamic_behaviour_analysis) logger.propagation(first,Logger::simple_propagation_type,c.group); + #ifdef DYNAMICNBLEVEL + if (c.learnt() && c.activity() > 2) { // GA + MYFLAG++; + int nbLevels =0; + for(Lit *i = c.getData(), *end = i+c.size(); i != end; i++) { + int l = level[i->var()]; + if (permDiff[l] != MYFLAG) { + permDiff[l] = MYFLAG; + nbLevels++; + } + + } + if(nbLevels+1 < c.activity()) + c.setActivity(nbLevels); + } + #endif } } FoundWatch: @@ -751,6 +838,7 @@ FoundWatch: } ws.shrink(i - j); + //Finally, propagate XOR-clauses if (xor_as_well && !confl) confl = propagate_xors(p); } propagations += num_props; @@ -790,7 +878,7 @@ Clause* Solver::propagate_xors(const Lit& p) cout << endl; #endif bool final = c.xor_clause_inverted(); - for (int k = 0, size = c.size(); k < size; k++ ) { + 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]); @@ -871,27 +959,38 @@ FoundWatch: | 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()); + bool operator () (const Clause* x, const Clause* y) { + const uint xsize = x->size(); + const uint ysize = y->size(); + + // First criteria + if (xsize > 2 && ysize == 2) return 1; + if (ysize > 2 && xsize == 2) return 0; + if (xsize == 2 && ysize == 2) return 0; + + // Second criteria + if (x->activity() > y->activity()) return 1; + if (x->activity() < y->activity()) return 0; + + //return x->oldActivity() < y->oldActivity(); + return xsize < ysize; } }; + void Solver::reduceDB() { int i, j; - double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + nbReduceDB++; sort(learnts, reduceDB_lt()); - for (i = j = 0; i < learnts.size() / 2; i++) { - if (learnts[i]->size() > 2 && !locked(*learnts[i])) + for (i = j = 0; i < learnts.size() / RATIOREMOVECLAUSES; i++){ + if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() > 2) 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[j++] = learnts[i]; } learnts.shrink(i - j); } @@ -935,8 +1034,12 @@ void Solver::setMaxRestarts(const uint num) maxRestarts = num; } -bool Solver::cleanClause(Clause& c) const +bool Solver::cleanClause(Clause& c) { + assert(c.size() >= 2); + Lit first = c[0]; + Lit second = c[1]; + Lit *i, *j, *end; uint at = 0; for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { @@ -946,7 +1049,12 @@ bool Solver::cleanClause(Clause& c) const } else assert(at > 1); assert(value(*i) != l_True); } - c.shrink(i-j); + if ((c.size() > 2) && (c.size() - (i-j) == 2)) { + detachModifiedClause(first, second, c.size(), &c); + c.shrink(i-j); + attachClause(c); + } else + c.shrink(i-j); return (i-j > 0); } @@ -963,8 +1071,9 @@ void Solver::cleanClauses(vec& cs) void Solver::cleanClauses(vec& cs) { uint useful = 0; - for (int s = 0; s < cs.size(); s++) { - XorClause& c = *cs[s]; + XorClause **s, **ss, **end; + for (s = ss = cs.getData(), end = s + cs.size(); s != end;) { + XorClause& c = **s; #ifdef VERBOSE_DEBUG std::cout << "Cleaning clause:"; c.plain_print(); @@ -983,6 +1092,16 @@ void Solver::cleanClauses(vec& cs) c.shrink(i-j); if (i-j > 0) useful++; + if (c.size() == 2) { + vec ps; + ps.push(c[0]); + ps.push(c[1]); + addBinaryXorClause(ps, c.xor_clause_inverted(), c.group); + removeClause(c); + s++; + } else + *ss++ = *s++; + #ifdef VERBOSE_DEBUG std::cout << "Cleaned clause:"; c.plain_print(); @@ -990,6 +1109,7 @@ void Solver::cleanClauses(vec& cs) #endif assert(c.size() > 1); } + cs.shrink(s-ss); #ifdef VERBOSE_DEBUG cout << "cleanClauses(XorClause) useful:" << useful << endl; @@ -1055,7 +1175,7 @@ lbool Solver::simplify() | 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) +lbool Solver::search(int nof_conflicts) { assert(ok); int conflictC = 0; @@ -1084,13 +1204,13 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) else if (ret != l_Nothing) return ret; } if (at_least_one_continue) continue; - ret = new_decision(nof_conflicts, nof_learnts, conflictC); + ret = new_decision(nof_conflicts, conflictC); if (ret != l_Nothing) return ret; } } } -llbool Solver::new_decision(int& nof_conflicts, int& nof_learnts, int& conflictC) +llbool Solver::new_decision(int& nof_conflicts, int& conflictC) { if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { // Reached bound on number of conflicts: @@ -1110,9 +1230,12 @@ llbool Solver::new_decision(int& nof_conflicts, int& nof_learnts, int& conflictC return l_False; } - if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) - // Reduce the set of learnt clauses: + // Reduce the set of learnt clauses: + if (conflicts >= curRestart * nbclausesbeforereduce) { + curRestart ++; reduceDB(); + nbclausesbeforereduce += 500; + } Lit next = lit_Undef; while (decisionLevel() < assumptions.size()) { @@ -1152,7 +1275,8 @@ llbool Solver::new_decision(int& nof_conflicts, int& nof_learnts, int& conflictC assert(value(next) == l_Undef); newDecisionLevel(); uncheckedEnqueue(next); - if (dynamic_behaviour_analysis) logger.propagation(next, Logger::guess_type); + if (dynamic_behaviour_analysis) + logger.propagation(next, Logger::guess_type); return l_Nothing; } @@ -1167,6 +1291,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf #endif int backtrack_level; + int nbLevels; conflicts++; conflictC++; @@ -1177,7 +1302,9 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf return l_False; } learnt_clause.clear(); - analyze(confl, learnt_clause, backtrack_level); + analyze(confl, learnt_clause, backtrack_level, nbLevels); + conf4Stats++; + if (dynamic_behaviour_analysis) logger.conflict(Logger::simple_confl_type, backtrack_level, confl->group, learnt_clause); cancelUntil(backtrack_level); @@ -1208,8 +1335,9 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf } else { Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true); learnts.push(c); + c->setActivity(nbLevels); // LS + if (nbLevels <= 2) nbDL2++; attachClause(*c); - claBumpActivity(*c); uncheckedEnqueue(learnt_clause[0], c); if (dynamic_behaviour_analysis) { @@ -1219,7 +1347,6 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf } varDecayActivity(); - claDecayActivity(); return l_Nothing; } @@ -1274,15 +1401,22 @@ lbool Solver::solve(const vec& assumps) model.clear(); conflict.clear(); + curRestart = 1; if (!ok) return l_False; assumps.copyTo(assumptions); double nof_conflicts = restart_first; - double nof_learnts = nClauses() * learntsize_factor; lbool status = l_Undef; + if (nClauses() * learntsize_factor < nbclausesbeforereduce) { + if (nClauses() * learntsize_factor < nbclausesbeforereduce/2) + nbclausesbeforereduce = nbclausesbeforereduce/4; + else + nbclausesbeforereduce = (nClauses() * learntsize_factor)/2; + } + toReplace->performReplace(); if (!ok) return l_False; @@ -1293,7 +1427,7 @@ lbool Solver::solve(const vec& assumps) removeSatisfied(clauses); cleanClauses(clauses); uint sumLengths = 0; - XorFinder xorFinder(this, clauses, xorclauses); + XorFinder xorFinder(this, clauses); 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); @@ -1352,15 +1486,14 @@ lbool Solver::solve(const vec& assumps) 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()); + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nbclausesbeforereduce*curRestart, 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); + status = search((int)nof_conflicts); 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(); @@ -1390,6 +1523,12 @@ lbool Solver::solve(const vec& assumps) if (conflict.size() == 0) ok = false; } + + #ifdef LS_STATS_NBBUMP + for(int i=0;isize(),learnts[i]->activity(), + (unsigned int)learnts[i]->nbBump()); + #endif cancelUntil(0); return status; diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index f0596a5..37686d1 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -1,6 +1,7 @@ /****************************************************************************************[Solver.h] MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson CryptoMiniSat -- Copyright (c) 2009 Mate Soos +glucose -- Gilles Audemard, Laurent Simon (2008) Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, @@ -33,6 +34,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "VarReplacer.h" #include "GaussianConfig.h" #include "Logger.h" +#include "constants.h" namespace MINISAT { @@ -88,6 +90,14 @@ public: 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 + template + void removeWatchedCl(vec &ws, const Clause *c); + template + bool findWatchedCl(vec& ws, const Clause *c); + template + void removeWatchedBinCl(vec &ws, const Clause *c); + template + bool findWatchedBinCl(vec& ws, const Clause *c); // Read state: // @@ -108,7 +118,6 @@ public: // 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) @@ -121,6 +130,8 @@ public: bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true vector realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable bool xorFinder; // Automatically find xor-clauses and convert them + friend class FindUndef; + bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef) void set_gaussian_decision_until(const uint to); void set_gaussian_decision_from(const uint from); @@ -131,6 +142,7 @@ public: // uint64_t starts, decisions, rnd_decisions, propagations, conflicts; uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; + uint64_t nbDL2, nbBin, nbReduceDB; //Logging void needStats(); // Prepares the solver to output statistics @@ -140,8 +152,6 @@ public: const vec& get_learnts() const; //Get all learnt clauses const vec& get_unitary_learnts() const; //return the set of unitary learned clauses void dump_sorted_learnts(const char* file); - friend class FindUndef; - bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef) protected: vector gauss_matrixes; @@ -173,14 +183,15 @@ protected: // bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! vec clauses; // List of problem clauses. - vec xorclauses; // List of problem xor-clauses. + vec xorclauses; // List of problem xor-clauses. Will not be freed + vec xorclauses_tofree;// List of problem xor-clauses. Will be freed vec learnts; // List of learnt clauses. vec unitary_learnts; // List of learnt clauses. - double cla_inc; // Amount to bump next clause with. vec activity; // A heuristic measurement of the activity of a variable. double var_inc; // Amount to bump next variable with. vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. + vec > binwatches; vec assigns; // The current assignments vector polarity; // The preferred polarity of each variable. vector decision_var; // Declares if a variable is eligible for selection in the decision heuristic. @@ -188,6 +199,13 @@ protected: vec trail_lim; // Separator indices for different decision levels in 'trail'. vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. vec level; // 'level[var]' contains the level at which the assignment was made. + vec permDiff; // LS: permDiff[var] contains the current conflict number... Used to count the number of different decision level variables in learnt clause + #ifdef UPDATEVARACTIVITY + vec lastDecisionLevel; + #endif + int64_t curRestart; + int64_t conf4Stats; + int nbclausesbeforereduce; 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()'. @@ -208,12 +226,14 @@ protected: vec analyze_stack; vec analyze_toclear; vec add_tmp; + unsigned long int MYFLAG; //Logging uint learnt_clause_group; //the group number of learnt clauses. Incremented at each added learnt clause // Main internal methods: // + //int nbPropagated (int level); 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. @@ -222,18 +242,18 @@ protected: Clause* propagate (const bool xor_as_well = true); // Perform unit propagation. Returns possibly conflicting clause. Clause* propagate_xors (const Lit& p); void cancelUntil (int level); // Backtrack until a certain level. - void analyze (Clause* confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) + void analyze (Clause* confl, vec& out_learnt, int& out_btlevel, int &nblevels); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - lbool search (int nof_conflicts, int nof_learnts); // Search for a given number of conflicts. + lbool search (int nof_conflicts); // Search for a given number of conflicts. void reduceDB (); // Reduce the set of learnt clauses. template void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. void cleanClauses (vec& cs); - bool cleanClause (Clause& c) const; + bool cleanClause (Clause& c); void cleanClauses (vec& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses llbool handle_conflict (vec& learnt_clause, Clause* confl, int& conflictC);// Handles the conflict clause - llbool new_decision (int& nof_conflicts, int& nof_learnts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made + llbool new_decision (int& nof_conflicts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made // Maintaining Variable/Clause activity: // @@ -249,11 +269,14 @@ protected: void detachClause (const XorClause& c); void detachClause (const Clause& c); // Detach a clause to watcher lists. void detachModifiedClause(const Lit lit1, const Lit lit2, const uint size, const Clause* address); - template - void removeClause(T& c); // Detach and free a clause. + void removeClause(Clause& c); // Detach and free a clause. + void removeClause(XorClause& 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. + void reverse_binary_clause(Clause& c) const; // Binary clauses --- the first Lit has to be true + template + inline void addBinaryXorClause(T& ps, const bool xor_clause_inverted, const uint group); //Adds Binary XOR clause as two normal clauses // Misc: // @@ -306,20 +329,6 @@ inline void Solver::varBumpActivity(Var 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); @@ -335,6 +344,11 @@ inline void Solver::newDecisionLevel() cout << "New decision level:" << trail_lim.size() << endl; #endif } +/*inline int Solver::nbPropagated(int level) { + if (level == decisionLevel()) + return trail.size() - trail_lim[level-1] - 1; + return trail_lim[level] - trail_lim[level-1] - 1; +}*/ inline int Solver::decisionLevel () const { return trail_lim.size(); @@ -427,12 +441,70 @@ void Solver::removeSatisfied(vec& cs) } cs.shrink(i - j); } +template +inline void Solver::removeWatchedCl(vec &ws, const Clause *c) { + int j = 0; + for (; j < ws.size() && ws[j] != c; j++); + assert(j < ws.size()); + for (; j < ws.size()-1; j++) ws[j] = ws[j+1]; + ws.pop(); +} +template +inline void Solver::removeWatchedBinCl(vec &ws, const Clause *c) { + int j = 0; + for (; j < ws.size() && ws[j].clause != c; j++); + assert(j < ws.size()); + for (; j < ws.size()-1; j++) ws[j] = ws[j+1]; + ws.pop(); +} template -void Solver::removeClause(T& c) +inline bool Solver::findWatchedCl(vec& ws, const Clause *c) +{ + int j = 0; + for (; j < ws.size() && ws[j] != c; j++); + return j < ws.size(); +} +template +inline bool Solver::findWatchedBinCl(vec& ws, const Clause *c) +{ + int j = 0; + for (; j < ws.size() && ws[j].clause != c; j++); + return j < ws.size(); +} +inline void Solver::reverse_binary_clause(Clause& c) const { + if (c.size() == 2 && value(c[0]) == l_False) { + assert(value(c[1]) == l_True); + Lit tmp = c[0]; + c[0] = c[1], c[1] = tmp; + } +} +template +inline void Solver::addBinaryXorClause(T& ps, const bool xor_clause_inverted, const uint group) { + Clause* c; + ps[0] = ps[0].unsign(); + ps[1] = ps[1].unsign(); + ps[0] ^= xor_clause_inverted; + + c = Clause_new(ps, group, false); + clauses.push(c); + attachClause(*c); + + ps[0] ^= true; + ps[1] ^= true; + c = Clause_new(ps, group, false); + clauses.push(c); + attachClause(*c); +} +inline void Solver::removeClause(Clause& c) { detachClause(c); free(&c); } +inline void Solver::removeClause(XorClause& c) +{ + detachClause(c); + c.mark(1); +} //================================================================================================= diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 270c744..ef1835c 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1 +1,4 @@ -CryptoMiniSat SVN revision: r454 , GIT revision: 91b7fc803564cfd5e5af363c81c1c68bdced162b +CryptoMiniSat +SVN revision: r484 +GIT revision: 36a94d9b25be76b24dd26a413928a3ae559c3983 + diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index c3b31c6..fde63c6 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -93,19 +93,23 @@ void VarReplacer::replace_set(vec& cs, const bool need_reattach) 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++; + if (c.size() == 2) { + S->addBinaryXorClause(c, c.xor_clause_inverted(), c.group); + c.mark(1); + r++; + } else { + S->attachClause(c); + *a++ = *r++; + } break; } } @@ -250,7 +254,7 @@ void VarReplacer::replace(Var var, Lit lit) //triangular cycle if (lit1.var() == lit2.var()) { - if (lit1.sign() ^ lit2.sign() != lit.sign()) { + if ((lit1.sign() ^ lit2.sign()) != lit.sign()) { #ifdef VERBOSE_DEBUG cout << "Inverted cycle in var-replacement -> UNSAT" << endl; #endif diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index d3c0a11..3808c85 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -37,9 +37,8 @@ using std::endl; using std::make_pair; -XorFinder::XorFinder(Solver* _S, vec& _cls, vec& _xorcls) : +XorFinder::XorFinder(Solver* _S, vec& _cls) : cls(_cls) - , xorcls(_xorcls) , S(_S) { } @@ -200,7 +199,8 @@ uint XorFinder::findXors(uint& sumLengths) } default: { XorClause* x = XorClause_new(lits, impair, old_group); - xorcls.push(x); + S->xorclauses.push(x); + S->xorclauses_tofree.push(x); S->attachClause(*x); #ifdef VERBOSE_DEBUG diff --git a/src/sat/cryptominisat2/XorFinder.h b/src/sat/cryptominisat2/XorFinder.h index a6c480a..11d2624 100644 --- a/src/sat/cryptominisat2/XorFinder.h +++ b/src/sat/cryptominisat2/XorFinder.h @@ -33,7 +33,7 @@ class XorFinder { public: - XorFinder(Solver* S, vec& cls, vec& xorcls); + XorFinder(Solver* S, vec& cls); uint doByPart(uint& sumLengths, const uint minSize, const uint maxSize); uint doNoPart(uint& sumLengths, const uint minSize, const uint maxSize); @@ -106,7 +106,6 @@ class XorFinder void clearToRemove(); vec& cls; - vec& xorcls; bool clauseEqual(const Clause& c1, const Clause& c2) const; bool impairSigns(const Clause& c) const; diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h new file mode 100644 index 0000000..f429650 --- /dev/null +++ b/src/sat/cryptominisat2/constants.h @@ -0,0 +1,6 @@ +#define RATIOREMOVECLAUSES 2 +#define NBCLAUSESBEFOREREDUCE 20000 +#define DYNAMICNBLEVEL +#define CONSTANTREMOVECLAUSE +#define UPDATEVARACTIVITY +#define BLOCK