diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/Gaussian.cpp')
-rw-r--r-- | src/prop/cryptominisat/Solver/Gaussian.cpp | 1147 |
1 files changed, 0 insertions, 1147 deletions
diff --git a/src/prop/cryptominisat/Solver/Gaussian.cpp b/src/prop/cryptominisat/Solver/Gaussian.cpp deleted file mode 100644 index e186d5849..000000000 --- a/src/prop/cryptominisat/Solver/Gaussian.cpp +++ /dev/null @@ -1,1147 +0,0 @@ -/*************************************************************************** -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> -#include "ClauseCleaner.h" -#include "VarReplacer.h" -#include "DataSync.h" - -//#define VERBOSE_DEBUG -//#define DEBUG_GAUSS - -#ifdef VERBOSE_DEBUG -#include <iterator> -#endif - -using namespace CMSat; -using std::ostream; -using std::cout; -using std::endl; - -static const uint16_t unassigned_col = std::numeric_limits<uint16_t>::max(); -static const Var unassigned_var = std::numeric_limits<Var>::max(); - -Gaussian::Gaussian(Solver& _solver, const GaussConf& _config, const uint32_t _matrix_no, const vector<XorClause*>& _xorclauses) : - solver(_solver) - , config(_config) - , matrix_no(_matrix_no) - , xorclauses(_xorclauses) - , messed_matrix_vars_since_reversal(true) - , gauss_last_level(0) - , disabled(false) - , useful_prop(0) - , useful_confl(0) - , called(0) - , unit_truths(0) -{ -} - -Gaussian::~Gaussian() -{ - for (uint32_t i = 0; i < clauses_toclear.size(); i++) - solver.clauseAllocator.clauseFree(clauses_toclear[i].first); -} - -inline void Gaussian::set_matrixset_to_cur() -{ - uint32_t 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; -} - -bool Gaussian::full_init() -{ - assert(solver.ok); - assert(solver.decisionLevel() == 0); - - if (!should_init()) return true; - reset_stats(); - uint32_t last_trail_size = solver.trail.size(); - - bool do_again_gauss = true; - while (do_again_gauss) { - do_again_gauss = false; - solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses); - if (!solver.ok) return false; - init(); - PropBy confl; - gaussian_ret g = gaussian(confl); - switch (g) { - case unit_conflict: - case conflict: - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")conflict at level 0" << std::endl; - #endif - solver.ok = false; - return false; - case unit_propagation: - case propagation: - unit_truths += last_trail_size - solver.trail.size(); - do_again_gauss = true; - solver.ok = (solver.propagate<true>().isNULL()); - if (!solver.ok) return false; - break; - case nothing: - break; - } - } - - return true; -} - -void Gaussian::init() -{ - assert(solver.decisionLevel() == 0); - - fill_matrix(cur_matrixset); - if (!cur_matrixset.num_rows || !cur_matrixset.num_cols) { - disabled = true; - badlevel = 0; - return; - } - - matrix_sets.clear(); - matrix_sets.push_back(cur_matrixset); - gauss_last_level = solver.trail.size(); - messed_matrix_vars_since_reversal = false; - badlevel = UINT_MAX; - - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")Gaussian init finished." << endl; - #endif -} - -uint32_t Gaussian::select_columnorder(vector<uint16_t>& var_to_col, matrixset& origMat) -{ - var_to_col.resize(solver.nVars(), unassigned_col); - - uint32_t num_xorclauses = 0; - for (uint32_t i = 0; i != xorclauses.size(); i++) { - XorClause& c = *xorclauses[i]; - if (c.getRemoved()) continue; - num_xorclauses++; - - for (uint32_t i2 = 0; i2 < c.size(); i2++) { - assert(solver.assigns[c[i2].var()].isUndef()); - var_to_col[c[i2].var()] = unassigned_col - 1; - } - } - - uint32_t largest_used_var = 0; - for (uint32_t i = 0; i < var_to_col.size(); i++) - if (var_to_col[i] != unassigned_col) - largest_used_var = i; - var_to_col.resize(largest_used_var + 1); - - var_is_in.resize(var_to_col.size(), 0); - origMat.var_is_set.resize(var_to_col.size(), 0); - - origMat.col_to_var.clear(); - vector<Var> vars(solver.nVars()); - if (!config.orderCols) { - for (uint32_t i = 0; i < solver.nVars(); i++) { - vars.push_back(i); - } - std::random_shuffle(vars.begin(), vars.end()); - } - - Heap<Solver::VarOrderLt> order_heap(solver.order_heap); - uint32_t iterReduceIt = 0; - while ((config.orderCols && !order_heap.empty()) || (!config.orderCols && iterReduceIt < vars.size())) - { - Var v; - if (config.orderCols) v = order_heap.removeMin(); - else v = vars[iterReduceIt++]; - if (var_to_col[v] == 1) { - #ifdef DEBUG_GAUSS - vector<uint32_t>::iterator it = - std::find(origMat.col_to_var.begin(), origMat.col_to_var.end(), v); - assert(it == origMat.col_to_var.end()); - #endif - - origMat.col_to_var.push_back(v); - var_to_col[v] = origMat.col_to_var.size()-1; - var_is_in.setBit(v); - } - } - - //for the ones that were not in the order_heap, but are marked in var_to_col - for (uint32_t 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_MORE - cout << "(" << matrix_no << ")col_to_var:"; - std::copy(origMat.col_to_var.begin(), origMat.col_to_var.end(), std::ostream_iterator<uint32_t>(cout, ",")); - cout << endl; - #endif - - return num_xorclauses; -} - -void Gaussian::fill_matrix(matrixset& origMat) -{ - #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); - origMat.num_cols = origMat.col_to_var.size(); - col_to_var_original = origMat.col_to_var; - changed_rows.resize(origMat.num_rows); - memset(&changed_rows[0], 0, sizeof(unsigned char)*changed_rows.size()); - - origMat.last_one_in_col.resize(origMat.num_cols); - std::fill(origMat.last_one_in_col.begin(), origMat.last_one_in_col.end(), origMat.num_rows); - origMat.first_one_in_row.resize(origMat.num_rows); - - origMat.removeable_cols = 0; - origMat.least_column_changed = -1; - origMat.matrix.resize(origMat.num_rows, origMat.num_cols); - - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")matrix size:" << origMat.num_rows << "," << origMat.num_cols << endl; - #endif - - uint32_t matrix_row = 0; - for (uint32_t i = 0; i != xorclauses.size(); i++) { - const XorClause& c = *xorclauses[i]; - if (c.getRemoved()) continue; - - origMat.matrix.getVarsetAt(matrix_row).set(c, var_to_col, origMat.num_cols); - origMat.matrix.getMatrixAt(matrix_row).set(c, var_to_col, origMat.num_cols); - matrix_row++; - } - assert(origMat.num_rows == matrix_row); -} - -void Gaussian::update_matrix_col(matrixset& m, const Var var, const uint32_t col) -{ - #ifdef VERBOSE_DEBUG_MORE - cout << "(" << matrix_no << ")Updating matrix var " << var+1 << " (col " << col << ", m.last_one_in_col[col]: " << m.last_one_in_col[col] << ")" << endl; - cout << "m.num_rows:" << m.num_rows << endl; - #endif - - #ifdef DEBUG_GAUSS - assert(col < m.num_cols); - #endif - - m.least_column_changed = std::min(m.least_column_changed, (int)col); - PackedMatrix::iterator this_row = m.matrix.beginMatrix(); - uint32_t row_num = 0; - - if (solver.assigns[var].getBool()) { - for (uint32_t end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) { - if ((*this_row)[col]) { - changed_rows[row_num] = true; - (*this_row).invert_is_true(); - (*this_row).clearBit(col); - } - } - } else { - for (uint32_t end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) { - if ((*this_row)[col]) { - changed_rows[row_num] = true; - (*this_row).clearBit(col); - } - } - } - - #ifdef DEBUG_GAUSS - bool c = false; - for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = r + m.matrix.getSize(); r != end; ++r) - c |= (*r)[col]; - assert(!c); - #endif - - m.removeable_cols++; - m.col_to_var[col] = unassigned_var; - m.var_is_set.setBit(var); -} - -void Gaussian::update_matrix_by_col_all(matrixset& m) -{ - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")Updating matrix." << endl; - #ifdef VERBOSE_DEBUG_MORE - print_matrix(m); - #endif - uint32_t num_updated = 0; - #endif - - #ifdef DEBUG_GAUSS - assert(nothing_to_propagate(cur_matrixset)); - assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m)); - #endif - - memset(&changed_rows[0], 0, sizeof(unsigned char)*changed_rows.size()); - - uint32_t last = 0; - uint32_t col = 0; - for (const Var *it = &m.col_to_var[0], *end = it + m.num_cols; it != end; col++, it++) { - if (*it != unassigned_var && solver.assigns[*it].isDef()) { - update_matrix_col(m, *it, col); - last++; - #ifdef VERBOSE_DEBUG - num_updated++; - #endif - } else - last = 0; - } - m.num_cols -= last; - - #ifdef DEBUG_GAUSS - check_matrix_against_varset(m.matrix, m); - #endif - - #ifdef VERBOSE_DEBUG - cout << "Matrix update finished, updated " << num_updated << " cols" << endl; - #ifdef VERBOSE_DEBUG_MORE - print_matrix(m); - #endif - #endif - - /*cout << "num_rows:" << m.num_rows; - cout << " num_rows diff:" << origMat.num_rows - m.num_rows << endl; - cout << "num_cols:" << col_to_var_original.size(); - cout << " num_cols diff:" << col_to_var_original.size() - m.col_to_var.size() << endl; - cout << "removeable cols:" << m.removeable_cols << endl;*/ -} - -inline void Gaussian::update_last_one_in_col(matrixset& m) -{ - for (uint16_t* i = &m.last_one_in_col[0]+m.last_one_in_col.size()-1, *end = &m.last_one_in_col[0]-1; i != end && *i >= m.num_rows; i--) - *i = m.num_rows; -} - -Gaussian::gaussian_ret Gaussian::gaussian(PropBy& confl) -{ - if (solver.decisionLevel() >= badlevel) - return nothing; - - if (messed_matrix_vars_since_reversal) { - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")matrix needs copy before update" << endl; - #endif - - const uint32_t level = solver.decisionLevel() / config.only_nth_gauss_save; - assert(level < matrix_sets.size()); - cur_matrixset = matrix_sets[level]; - } - update_last_one_in_col(cur_matrixset); - update_matrix_by_col_all(cur_matrixset); - - messed_matrix_vars_since_reversal = false; - gauss_last_level = solver.trail.size(); - badlevel = UINT_MAX; - - propagatable_rows.clear(); - uint32_t last_row = eliminate(cur_matrixset); - #ifdef DEBUG_GAUSS - check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset); - #endif - - gaussian_ret ret; - //There is no early abort, so this is unneeded - /*if (conflict_row != UINT_MAX) { - uint32_t maxlevel = UINT_MAX; - uint32_t size = UINT_MAX; - uint32_t best_row = UINT_MAX; - analyse_confl(cur_matrixset, conflict_row, maxlevel, size, best_row); - ret = handle_matrix_confl(confl, cur_matrixset, size, maxlevel, best_row); - } else {*/ - ret = handle_matrix_prop_and_confl(cur_matrixset, last_row, confl); - //} - #ifdef DEBUG_GAUSS - assert(ret == conflict || ret == unit_conflict || nothing_to_propagate(cur_matrixset)); - #endif - - if (!cur_matrixset.num_cols || !cur_matrixset.num_rows) { - badlevel = solver.decisionLevel(); - return ret; - } - - if (ret == nothing && - solver.decisionLevel() % config.only_nth_gauss_save == 0) - set_matrixset_to_cur(); - - #ifdef VERBOSE_DEBUG - if (ret == nothing) - cout << "(" << matrix_no << ")Useless. "; - else - cout << "(" << matrix_no << ")Useful. "; - cout << "(" << matrix_no << ")Useful prop in " << ((double)useful_prop/(double)called)*100.0 << "%" << endl; - cout << "(" << matrix_no << ")Useful confl in " << ((double)useful_confl/(double)called)*100.0 << "%" << endl; - #endif - - return ret; -} - -uint32_t Gaussian::eliminate(matrixset& m) -{ - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")"; - cout << "Starting elimination" << endl; - cout << "m.least_column_changed:" << m.least_column_changed << endl; - #ifdef VERBOSE_DEBUG_MORE - print_last_one_in_cols(m); - #endif - - uint32_t number_of_row_additions = 0; - uint32_t no_exchanged = 0; - #endif - - if (m.least_column_changed == INT_MAX) { - #ifdef VERBOSE_DEBUG - cout << "Nothing to eliminate" << endl; - #endif - - return m.num_rows; - } - - - #ifdef DEBUG_GAUSS - assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m)); - #endif - - uint32_t i = 0; - uint32_t j = (config.iterativeReduce) ? m.least_column_changed + 1 : 0; - PackedMatrix::iterator beginIt = m.matrix.beginMatrix(); - PackedMatrix::iterator rowIt = m.matrix.beginMatrix(); - - #ifdef DEBUG_GAUSS - check_first_one_in_row(m, j); - #endif - - if (j) { - uint16_t until = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows); - if (j-1 > m.first_one_in_row[m.num_rows-1]) - until = m.num_rows; - for (;i != until; i++, ++rowIt) if (changed_rows[i] && (*rowIt).popcnt_is_one(m.first_one_in_row[i])) - propagatable_rows.push(i); - } - - #ifdef VERBOSE_DEBUG - cout << "At while() start: i,j = " << i << ", " << j << endl; - cout << "num_rows:" << m.num_rows << " num_cols:" << m.num_cols << endl; - #endif - - if (j > m.num_cols) { - #ifdef VERBOSE_DEBUG - cout << "Going straight to finish" << endl; - #endif - goto finish; - } - - #ifdef DEBUG_GAUSS - assert(i <= m.num_rows && j <= m.num_cols); - #endif - - while (i != m.num_rows && j != m.num_cols) { - //Find pivot in column j, starting in row i: - - if (m.col_to_var[j] == unassigned_var) { - j++; - continue; - } - - PackedMatrix::iterator this_matrix_row = rowIt; - PackedMatrix::iterator end = beginIt + m.last_one_in_col[j]; - for (; this_matrix_row != end; ++this_matrix_row) { - if ((*this_matrix_row)[j]) - break; - } - - if (this_matrix_row != end) { - - //swap rows i and maxi, but do not change the value of i; - if (this_matrix_row != rowIt) { - #ifdef VERBOSE_DEBUG - no_exchanged++; - #endif - - //Would early abort, but would not find the best conflict (and would be expensive) - //if (matrix_row_i.is_true() && matrix_row_i.isZero()) { - // conflict_row = i; - // return 0; - //} - (*rowIt).swapBoth(*this_matrix_row); - } - #ifdef DEBUG_GAUSS - assert(m.matrix.getMatrixAt(i).popcnt(j) == m.matrix.getMatrixAt(i).popcnt()); - assert(m.matrix.getMatrixAt(i)[j]); - #endif - - if ((*rowIt).popcnt_is_one(j)) - propagatable_rows.push(i); - - //Now A[i,j] will contain the old value of A[maxi,j]; - ++this_matrix_row; - for (; this_matrix_row != end; ++this_matrix_row) if ((*this_matrix_row)[j]) { - //subtract row i from row u; - //Now A[u,j] will be 0, since A[u,j] - A[i,j] = A[u,j] -1 = 0. - #ifdef VERBOSE_DEBUG - number_of_row_additions++; - #endif - - (*this_matrix_row).xorBoth(*rowIt); - //Would early abort, but would not find the best conflict (and would be expensive) - //if (it->is_true() &&it->isZero()) { - // conflict_row = i2; - // return 0; - //} - } - m.first_one_in_row[i] = j; - i++; - ++rowIt; - m.last_one_in_col[j] = i; - } else { - m.first_one_in_row[i] = j; - m.last_one_in_col[j] = i + 1; - } - j++; - } - - finish: - - m.least_column_changed = INT_MAX; - - #ifdef VERBOSE_DEBUG - cout << "Finished elimination" << endl; - cout << "Returning with i,j:" << i << ", " << j << "(" << m.num_rows << ", " << m.num_cols << ")" << endl; - #ifdef VERBOSE_DEBUG_MORE - print_matrix(m); - print_last_one_in_cols(m); - #endif - cout << "(" << matrix_no << ")Exchanged:" << no_exchanged << " row additions:" << number_of_row_additions << endl; - #endif - - #ifdef DEBUG_GAUSS - assert(check_last_one_in_cols(m)); - uint32_t row = 0; - uint32_t col = 0; - for (; col < m.num_cols && row < m.num_rows && row < i ; col++) { - assert(m.matrix.getMatrixAt(row).popcnt() == m.matrix.getMatrixAt(row).popcnt(col)); - assert(!(m.col_to_var[col] == unassigned_var && m.matrix.getMatrixAt(row)[col])); - if (m.col_to_var[col] == unassigned_var || !m.matrix.getMatrixAt(row)[col]) { - #ifdef VERBOSE_DEBUG_MORE - cout << "row:" << row << " col:" << col << " m.last_one_in_col[col]-1: " << m.last_one_in_col[col]-1 << endl; - #endif - assert(m.col_to_var[col] == unassigned_var || std::min((uint16_t)(m.last_one_in_col[col]-1), m.num_rows) == row); - continue; - } - row++; - } - #endif - - return i; -} - -Gaussian::gaussian_ret Gaussian::handle_matrix_confl(PropBy& confl, const matrixset& m, const uint32_t maxlevel, const uint32_t best_row) -{ - assert(best_row != UINT_MAX); - - const bool xorEqualFalse = !m.matrix.getVarsetAt(best_row).is_true(); - const bool wasUndef = m.matrix.getVarsetAt(best_row).fill(tmp_clause, solver.assigns, col_to_var_original); - release_assert(!wasUndef); - - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")matrix confl clause:" - << tmp_clause << " , " - << "xorEqualFalse:" << xorEqualFalse << std::endl; - #endif - - if (tmp_clause.size() <= 1) { - if (!tmp_clause.empty()) { - confl = PropBy(tmp_clause[0]); - } else { - confl = PropBy(); - solver.ok = false; - } - return unit_conflict; - } - - if (maxlevel != solver.decisionLevel()) { - solver.cancelUntil(maxlevel); - } - const uint32_t curr_dec_level = solver.decisionLevel(); - assert(maxlevel == curr_dec_level); - - uint32_t maxsublevel = 0; - if (tmp_clause.size() == 2) { - Lit lit1 = tmp_clause[0]; - Lit lit2 = tmp_clause[1]; - - solver.watches[(~lit1).toInt()].push(Watched(lit2, true)); - solver.watches[(~lit2).toInt()].push(Watched(lit1, true)); - solver.numBins++; - solver.learnts_literals += 2; - solver.dataSync->signalNewBinClause(lit1, lit2); - - lit1 = ~lit1; - lit2 = ~lit2; - solver.watches[(~lit2).toInt()].push(Watched(lit1, true)); - solver.watches[(~lit1).toInt()].push(Watched(lit2, true)); - solver.numBins++; - solver.learnts_literals += 2; - solver.dataSync->signalNewBinClause(lit1, lit2); - - lit1 = ~lit1; - lit2 = ~lit2; - uint32_t sublevel1 = find_sublevel(lit1.var()); - uint32_t sublevel2 = find_sublevel(lit2.var()); - if (sublevel1 > sublevel2) { - maxsublevel = sublevel1; - std::swap(lit1, lit2); - } else { - maxsublevel = sublevel2; - } - - confl = PropBy(lit1); - solver.failBinLit = lit2; - } else { - Clause* conflPtr = (Clause*)solver.clauseAllocator.XorClause_new(tmp_clause, xorEqualFalse); - confl = solver.clauseAllocator.getOffset(conflPtr); - Clause& cla = *conflPtr; - - uint32_t maxsublevel_at = UINT_MAX; - for (uint32_t i = 0, size = cla.size(); i != size; i++) if (solver.level[cla[i].var()] == (int32_t)curr_dec_level) { - uint32_t 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, uint32_t last_row, PropBy& confl) -{ - int32_t maxlevel = std::numeric_limits<int32_t>::max(); - uint32_t size = UINT_MAX; - uint32_t best_row = UINT_MAX; - - for (uint32_t row = last_row; row != m.num_rows; row++) { - #ifdef DEBUG_GAUSS - assert(m.matrix.getMatrixAt(row).isZero()); - #endif - if (m.matrix.getMatrixAt(row).is_true()) - analyse_confl(m, row, maxlevel, size, best_row); - } - - if (maxlevel != std::numeric_limits<int32_t>::max()) - return handle_matrix_confl(confl, m, maxlevel, best_row); - - #ifdef DEBUG_GAUSS - assert(check_no_conflict(m)); - assert(last_row == 0 || !m.matrix.getMatrixAt(last_row-1).isZero()); - #endif - - #ifdef VERBOSE_DEBUG - cout << "Resizing matrix to num_rows = " << last_row << endl; - #endif - m.num_rows = last_row; - m.matrix.resizeNumRows(m.num_rows); - - gaussian_ret ret = nothing; - - uint32_t num_props = 0; - for (const uint32_t* 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; -} - -uint32_t 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 uint32_t until_sublevel) -{ - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")Canceling until sublevel " << until_sublevel << endl; - #endif - - for (vector<Gaussian*>::iterator gauss = solver.gauss_matrixes.begin(), end= solver.gauss_matrixes.end(); gauss != end; gauss++) - if (*gauss != this) (*gauss)->canceling(until_sublevel); - - for (int sublevel = solver.trail.size()-1; sublevel >= (int)until_sublevel; sublevel--) { - Var var = solver.trail[sublevel].var(); - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")Canceling var " << var+1 << endl; - #endif - - solver.assigns[var] = l_Undef; - solver.insertVarOrder(var); - } - solver.trail.shrink(solver.trail.size() - until_sublevel); - - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")Canceling sublevel finished." << endl; - #endif -} - -void Gaussian::analyse_confl(const matrixset& m, const uint32_t row, int32_t& maxlevel, uint32_t& size, uint32_t& 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: "; - #ifdef VERBOSE_DEBUG_MORE - print_matrix_row_with_assigns(m.matrix.getVarsetAt(row)); - cout << endl; - - cout << "(" << matrix_no << ")corresponding matrix's row (should be empty): "; - print_matrix_row(m.matrix.getMatrixAt(row)); - cout << endl; - #endif - #endif - - int32_t this_maxlevel = 0; - unsigned long int var = 0; - uint32_t this_size = 0; - while (true) { - var = m.matrix.getVarsetAt(row).scan(var); - if (var == ULONG_MAX) break; - - const Var real_var = col_to_var_original[var]; - assert(real_var < solver.nVars()); - - if (solver.level[real_var] > this_maxlevel) - this_maxlevel = solver.level[real_var]; - var++; - this_size++; - } - - //the maximum of all lit's level must be lower than the max. level of the current best clause (or this clause must be either empty or unit clause) - if (!( - (this_maxlevel < maxlevel) - || (this_maxlevel == maxlevel && this_size < size) - || (this_size <= 1) - )) { - assert(maxlevel != std::numeric_limits<int32_t>::max()); - - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")Other found conflict just as good or better."; - cout << "(" << matrix_no << ") || Old maxlevel:" << maxlevel << " new maxlevel:" << this_maxlevel; - cout << "(" << matrix_no << ") || Old size:" << size << " new size:" << this_size << endl; - //assert(!(maxlevel != UINT_MAX && maxlevel != this_maxlevel)); //NOTE: only holds if gauss is executed at each level - #endif - - return; - } - - - #ifdef VERBOSE_DEBUG - if (maxlevel != std::numeric_limits<int32_t>::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 uint32_t row) -{ - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")matrix prop" << endl; - #ifdef VERBOSE_DEBUG_MORE - cout << "(" << matrix_no << ")matrix row:" << m.matrix.getMatrixAt(row) << endl; - #endif - #endif - - bool xorEqualFalse = !m.matrix.getVarsetAt(row).is_true(); - m.matrix.getVarsetAt(row).fill(tmp_clause, solver.assigns, col_to_var_original); - #ifdef VERBOSE_DEBUG - cout << "(" << matrix_no << ")matrix prop clause: " << tmp_clause << std::endl; - cout << endl; - #endif - - switch(tmp_clause.size()) { - case 0: - //This would mean nothing, empty = true, always true in xors - assert(false); - break; - case 1: - solver.cancelUntil(0); - solver.uncheckedEnqueue(tmp_clause[0]); - return unit_propagation; - case 2: { - solver.cancelUntil(0); - tmp_clause[0] = tmp_clause[0].unsign(); - tmp_clause[1] = tmp_clause[1].unsign(); - XorClause* cl = solver.addXorClauseInt(tmp_clause, xorEqualFalse); - release_assert(cl == NULL); - release_assert(solver.ok); - return unit_propagation; - } - default: - if (solver.decisionLevel() == 0) { - solver.uncheckedEnqueue(tmp_clause[0]); - return unit_propagation; - } - Clause& cla = *(Clause*)solver.clauseAllocator.XorClause_new(tmp_clause, xorEqualFalse); - assert(m.matrix.getMatrixAt(row).is_true() == !cla[0].sign()); - assert(solver.assigns[cla[0].var()].isUndef()); - - clauses_toclear.push_back(std::make_pair(&cla, solver.trail.size()-1)); - solver.uncheckedEnqueue(cla[0], solver.clauseAllocator.getOffset(&cla)); - return propagation; - } - - return propagation; -} - -void Gaussian::disable_if_necessary() -{ - if (//nof_conflicts >= 0 - //&& conflictC >= nof_conflicts/8 - !config.dontDisable - && called > 50 - && useful_confl*2+useful_prop < (uint32_t)((double)called*0.05) ) - disabled = true; -} - -llbool Gaussian::find_truths(vec<Lit>& learnt_clause, uint64_t& conflictC) -{ - PropBy confl; - - disable_if_necessary(); - if (should_check_gauss(solver.decisionLevel())) { - called++; - gaussian_ret g = gaussian(confl); - - switch (g) { - case conflict: { - useful_confl++; - llbool ret = solver.handle_conflict(learnt_clause, confl, conflictC, true); - if (confl.isClause()) - solver.clauseAllocator.clauseFree(solver.clauseAllocator.getPointer(confl.getClause())); - - if (ret != l_Nothing) return ret; - return l_Continue; - } - case unit_propagation: - unit_truths++; - case propagation: - useful_prop++; - return l_Continue; - case unit_conflict: { - unit_truths++; - useful_confl++; - if (confl.isNULL()) { - #ifdef VERBOSE_DEBUG - std::cout << "(" << matrix_no << ")zero-length conflict. UNSAT" << std::endl; - #endif - solver.ok = false; - return l_False; - } - - Lit lit = confl.getOtherLit(); - solver.cancelUntil(0); - - #ifdef VERBOSE_DEBUG - std::cout << "(" << matrix_no << ")one-length conflict" << std::endl; - #endif - if (solver.value(lit) != l_Undef) { - assert(solver.value(lit) == l_False); - #ifdef VERBOSE_DEBUG - std::cout << "(" << matrix_no << ") -> UNSAT" << std::endl; - #endif - solver.ok = false; - return l_False; - } - #ifdef VERBOSE_DEBUG - std::cout << "(" << matrix_no << ") -> setting to correct value" << std::endl; - #endif - solver.uncheckedEnqueue(lit); - 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++; - } - cout << "final:" << row.is_true() << endl;; -} - -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.is_true()) cout << "xorEqualFalse"; -} - -string Gaussian::lbool_to_string(const lbool toprint) -{ - if (toprint == l_True) - return "true"; - if (toprint == l_False) - return "false"; - if (toprint == l_Undef) - return "undef"; - - assert(false); - return ""; -} - - -void Gaussian::print_stats() const -{ - if (called > 0) { - cout.setf(std::ios::fixed); - std::cout << " Gauss(" << matrix_no << ") useful"; - cout << " prop: " << std::setprecision(2) << std::setw(5) << ((double)useful_prop/(double)called)*100.0 << "% "; - cout << " confl: " << std::setprecision(2) << std::setw(5) << ((double)useful_confl/(double)called)*100.0 << "% "; - if (disabled) std::cout << "disabled"; - } else - std::cout << " Gauss(" << matrix_no << ") not called."; -} - -void Gaussian::print_matrix_stats() const -{ - cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl; -} - - -void Gaussian::reset_stats() -{ - useful_prop = 0; - useful_confl = 0; - called = 0; - disabled = false; -} - -bool Gaussian::check_no_conflict(matrixset& m) const -{ - uint32_t row = 0; - for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r, ++row) { - if ((*r).is_true() && (*r).isZero()) { - cout << "Conflict at row " << row << endl; - return false; - } - } - return true; -} - -void Gaussian::print_matrix(matrixset& m) const -{ - uint32_t row = 0; - for (PackedMatrix::iterator it = m.matrix.beginMatrix(); it != m.matrix.endMatrix(); ++it, row++) { - cout << *it << " -- row:" << row; - if (row >= m.num_rows) - cout << " (considered past the end)"; - cout << endl; - } -} - -void Gaussian::print_last_one_in_cols(matrixset& m) const -{ - for (uint32_t i = 0; i < m.num_cols; i++) { - cout << "last_one_in_col[" << i << "]-1 = " << m.last_one_in_col[i]-1 << endl; - } -} - -bool Gaussian::nothing_to_propagate(matrixset& m) const -{ - for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r) { - if ((*r).popcnt_is_one() - && solver.assigns[m.col_to_var[(*r).scan(0)]].isUndef()) { - #ifdef VERBOSE_DEBUG - std::cout << "row " << (*r) << " is a propagation, but we didn't catch it" << std::endl; - #endif - return false; - } - } - for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r) { - if ((*r).isZero() && (*r).is_true()) { - #ifdef VERBOSE_DEBUG - std::cout << "row " << (*r) << " is a conflict, but we didn't catch it" << std::endl; - #endif - return false; - } - } - return true; -} - -bool Gaussian::check_last_one_in_cols(matrixset& m) const -{ - for(uint32_t i = 0; i < m.num_cols; i++) { - const uint32_t last = std::min(m.last_one_in_col[i] - 1, (int)m.num_rows); - uint32_t real_last = 0; - uint32_t i2 = 0; - for (PackedMatrix::iterator it = m.matrix.beginMatrix(); it != m.matrix.endMatrix(); ++it, i2++) { - if ((*it)[i]) - real_last = i2; - } - if (real_last > last) - return false; - } - - return true; -} - -void Gaussian::check_matrix_against_varset(PackedMatrix& matrix, const matrixset& m) const -{ - for (uint32_t i = 0; i < matrix.getSize(); i++) { - const PackedRow mat_row = matrix.getMatrixAt(i); - const PackedRow var_row = matrix.getVarsetAt(i); - - unsigned long int col = 0; - bool final = false; - while (true) { - col = var_row.scan(col); - if (col == ULONG_MAX) break; - - const Var var = col_to_var_original[col]; - assert(var < solver.nVars()); - - if (solver.assigns[var] == l_True) { - assert(!mat_row[col]); - assert(m.col_to_var[col] == unassigned_var); - assert(m.var_is_set[var]); - final = !final; - } else if (solver.assigns[var] == l_False) { - assert(!mat_row[col]); - assert(m.col_to_var[col] == unassigned_var); - assert(m.var_is_set[var]); - } else if (solver.assigns[var] == l_Undef) { - assert(m.col_to_var[col] != unassigned_var); - assert(!m.var_is_set[var]); - assert(mat_row[col]); - } else assert(false); - - col++; - } - if ((final^!mat_row.is_true()) != !var_row.is_true()) { - cout << "problem with row:"; print_matrix_row_with_assigns(var_row); cout << endl; - assert(false); - } - } -} - -void Gaussian::check_first_one_in_row(matrixset& m, const uint32_t j) -{ - if (j) { - uint16_t until2 = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows); - if (j-1 > m.first_one_in_row[m.num_rows-1]) { - until2 = m.num_rows; - #ifdef VERBOSE_DEBUG - cout << "j-1 > m.first_one_in_row[m.num_rows-1]" << "j:" << j << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl; - #endif - } - for (uint32_t i2 = 0; i2 != until2; i2++) { - #ifdef VERBOSE_DEBUG - cout << endl << "row " << i2 << " (num rows:" << m.num_rows << ")" << endl; - cout << m.matrix.getMatrixAt(i2) << endl; - cout << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl; - cout << "first_one_in_row:" << m.first_one_in_row[i2] << endl; - cout << "num_cols:" << m.num_cols << endl; - cout << "popcnt:" << m.matrix.getMatrixAt(i2).popcnt() << endl; - cout << "popcnt_is_one():" << m.matrix.getMatrixAt(i2).popcnt_is_one() << endl; - cout << "popcnt_is_one("<< m.first_one_in_row[i2] <<"): " << m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]) << endl; - #endif - - for (uint32_t i3 = 0; i3 < m.first_one_in_row[i2]; i3++) { - assert(m.matrix.getMatrixAt(i2)[i3] == 0); - } - assert(m.matrix.getMatrixAt(i2)[m.first_one_in_row[i2]]); - assert(m.matrix.getMatrixAt(i2).popcnt_is_one() == - m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2])); - } - } -} |