From 32b5dc31d16eaa3bd78387a4baa7c31fc3124773 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Thu, 8 Dec 2022 11:14:47 +0100 Subject: [PATCH] Added missing functions for backtracking --- src/sat/sat_config.cpp | 2 + src/sat/sat_config.h | 2 + src/sat/sat_params.pyg | 8 ++-- src/sat/smt/xor_gaussian.cpp | 77 +++++++++++++++++++----------------- src/sat/smt/xor_gaussian.h | 20 +++++----- src/sat/smt/xor_solver.cpp | 38 +++++++++++++++++- src/sat/smt/xor_solver.h | 4 ++ 7 files changed, 100 insertions(+), 51 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 646299567..9eb25d956 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -266,6 +266,8 @@ namespace sat { m_xor_gauss_max_num_matrices = p.xor_gauss_max_num_matrices(); m_xor_gauss_force_use_all_matrices = p.xor_gauss_force_use_all_matrices(); m_xor_gauss_min_usefulness_cutoff = p.xor_gauss_min_usefulness_cutoff(); + m_xor_gauss_autodisable = p.xor_gauss_autodisable(); + m_xor_gauss_detach_reattach = p.xor_gauss_detach_reattach(); sat_simplifier_params ssp(_p); m_elim_vars = ssp.elim_vars(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 13e9a08d7..7ec074b05 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -209,6 +209,8 @@ namespace sat { unsigned m_xor_gauss_max_num_matrices; bool m_xor_gauss_force_use_all_matrices; double m_xor_gauss_min_usefulness_cutoff; + bool m_xor_gauss_autodisable; + bool m_xor_gauss_detach_reattach; const bool m_xor_gauss_doMatrixFind = true; const unsigned m_xor_gauss_min_clauses = 2; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 9ee8889ab..c2db71745 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -133,15 +133,15 @@ def_module_params('sat', # ('xor.max_to_find_slow', UINT, 'tbd'), # ('xor.max_xor_matrix, UINT64, 'tbd'), # ('xor.allow_elim_vars', BOOL, 'tbd'), - # ('xor.var_per_cut', UINT, 'tbd'), # ('xor.force_preserve_xors', BOOL, 'tbd'), ('xor.gauss.max_matrix_columns', UINT, 1000, 'tbd'), ('xor.gauss.max_matrix_rows', UINT, 2000, 'The maximum matrix size -- no. of rows'), ('xor.gauss.min_matrix_rows', UINT, 3, 'The minimum matrix size -- no. of rows'), ('xor.gauss.max_num_matrices', UINT, 5, 'Maximum number of matrices'), - ('xor.gauss.force_use_all_matrices', BOOL, True, 'tbd'), - # ('xor.gauss.autodisable', BOOL, False, 'tbd'), - ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0.2, 'tbd'), + ('xor.gauss.force_use_all_matrices', BOOL, False, 'Force using all matrices'), + ('xor.gauss.autodisable', BOOL, True, 'Automatically disable gauss when performing badly'), + ('xor.gauss.detach_reattach', BOOL, False, 'Detach and reattach XORs'), + ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0.2, 'Turn off Gauss if less than this many usefulenss ratio is recorded'), # ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'), # ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'), # ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd') diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp index 0c6720ff2..a078b9af0 100644 --- a/src/sat/smt/xor_gaussian.cpp +++ b/src/sat/smt/xor_gaussian.cpp @@ -162,14 +162,14 @@ EGaussian::EGaussian(xr::solver& _solver, unsigned _matrix_no, const vectorrhs() = 0; }; - add_packed_row(cols_unset); - add_packed_row(cols_vals); - add_packed_row(tmp_col); - add_packed_row(tmp_col2); + add_packed_row(m_cols_unset); + add_packed_row(m_cols_vals); + add_packed_row(m_tmp_col); + add_packed_row(m_tmp_col2); initialized = true; update_cols_vals_set(true); @@ -446,8 +446,8 @@ literal_vector& EGaussian::get_reason(unsigned row, int& out_ID) { m_mat[row].get_reason( to_fill, m_column_to_var, - *cols_vals, - *tmp_col2, + *m_cols_vals, + *m_tmp_col2, xor_reasons[row].m_propagated); xor_reasons[row].m_must_recalc = false; @@ -638,10 +638,10 @@ bool EGaussian::find_truths( m_column_to_var, var_has_resp_row, new_resp_var, - *tmp_col, - *tmp_col2, - *cols_vals, - *cols_unset, + *m_tmp_col, + *m_tmp_col2, + *m_cols_vals, + *m_cols_unset, ret_lit_prop); find_truth_called_propgause++; @@ -754,28 +754,30 @@ bool EGaussian::find_truths( } inline void EGaussian::update_cols_vals_set(literal lit) { - cols_unset->clearBit(m_var_to_column[lit.var()]); + m_cols_unset->clearBit(m_var_to_column[lit.var()]); if (!lit.sign()) - cols_vals->setBit(m_var_to_column[lit.var()]); + m_cols_vals->setBit(m_var_to_column[lit.var()]); } +// Updates the auxiliary row that determines which variables of the matrix are unassigned and which values they have +// In case the argument is false it only updates the recently added variables. If true, it recalculates all void EGaussian::update_cols_vals_set(bool force) { SASSERT(initialized); - if (cancelled_since_val_update || force) { - cols_vals->setZero(); - cols_unset->setOne(); + if (recalculate_values || force) { + m_cols_vals->setZero(); + m_cols_unset->setOne(); for (unsigned col = 0; col < m_column_to_var.size(); col++) { unsigned var = m_column_to_var[col]; if (m_solver.s().value(var) != l_undef) { - cols_unset->clearBit(col); + m_cols_unset->clearBit(col); if (m_solver.s().value(var) == l_true) - cols_vals->setBit(col); + m_cols_vals->setBit(col); } } last_val_update = m_solver.s().trail_size(); - cancelled_since_val_update = false; + recalculate_values = false; TRACE("xor", tout << "last val update set to " << last_val_update << "\n"); return; } @@ -789,21 +791,21 @@ void EGaussian::update_cols_vals_set(bool force) { unsigned col = m_var_to_column[var]; if (col != UINT32_MAX) { SASSERT(m_solver.s().value(var) != l_undef); - cols_unset->clearBit(col); + m_cols_unset->clearBit(col); if (m_solver.s().value(var) == l_true) - cols_vals->setBit(col); + m_cols_vals->setBit(col); } } last_val_update = m_solver.s().trail_size(); std::cout << "Col-Unassigned: "; - for (int i = 0; i < 64 * cols_unset->size; ++i) { - std::cout << (*cols_unset)[i]; + for (int i = 0; i < 64 * m_cols_unset->size; ++i) { + std::cout << (*m_cols_unset)[i]; } std::cout << "\n"; std::cout << "Col-Values: "; - for (int i = 0; i < 64 * cols_vals->size; ++i) { - std::cout << (*cols_vals)[i]; + for (int i = 0; i < 64 * m_cols_vals->size; ++i) { + std::cout << (*m_cols_vals)[i]; } std::cout << std::endl; } @@ -873,10 +875,10 @@ void EGaussian::eliminate_column(unsigned p, gauss_data& gqd) { m_column_to_var, var_has_resp_row, new_non_resp_var, - *tmp_col, - *tmp_col2, - *cols_vals, - *cols_unset, + *m_tmp_col, + *m_tmp_col2, + *m_cols_vals, + *m_cols_unset, ret_lit_prop ); elim_called_propgause++; @@ -1082,6 +1084,7 @@ bool EGaussian::check_row_satisfied(unsigned row) { return !fin; } +// determines if the current matrix must be disabled because it performs badly bool EGaussian::must_disable(gauss_data& gqd) { SASSERT(initialized); gqd.disable_checks++; diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h index 7db7478e4..bacb5bc54 100644 --- a/src/sat/smt/xor_gaussian.h +++ b/src/sat/smt/xor_gaussian.h @@ -585,7 +585,7 @@ namespace xr { unsigned p, gauss_data& gqd ); - void canceling(); + void enforce_recalculate(); bool full_init(bool& created); void update_cols_vals_set(bool force); bool must_disable(gauss_data& gqd); @@ -668,7 +668,7 @@ namespace xr { /////////////// unsigned matrix_no; bool initialized = false; - bool cancelled_since_val_update = true; + bool recalculate_values = true; unsigned last_val_update = 0; vector m_xorclauses; @@ -699,20 +699,22 @@ namespace xr { unsigned m_num_cols = 0; //quick lookup - PackedRow* cols_vals = nullptr; // the current model for the variable in the respective column. Only correct if the respective element in cols_unset is 0 (lazily -> update_cols_vals_set) - PackedRow* cols_unset = nullptr; // initially a sequence of 1. If the variable at the respective colum in the matrix is assigned it is set to 0 (lazily -> update_cols_vals_set) - PackedRow* tmp_col = nullptr; - PackedRow* tmp_col2 = nullptr; + PackedRow* m_cols_vals = nullptr; // the current model for the variable in the respective column. Only correct if the respective element in cols_unset is 0 (lazily -> update_cols_vals_set) + PackedRow* m_cols_unset = nullptr; // initially a sequence of 1. If the variable at the respective colum in the matrix is assigned it is set to 0 (lazily -> update_cols_vals_set) + PackedRow* m_tmp_col = nullptr; + PackedRow* m_tmp_col2 = nullptr; void update_cols_vals_set(literal lit); //Data to free (with delete[] x) // TODO: This are always 4 equally sized elements; merge them into one block - svector tofree; + svector m_tofree; }; - inline void EGaussian::canceling() { - cancelled_since_val_update = true; + // enforces to recalculate the auxiliary rows that determine which variables of the matrix are unassigned/assigned to true + // necessary after backtracking + inline void EGaussian::enforce_recalculate() { + recalculate_values = true; memset(satisfied_xors.data(), false, satisfied_xors.size()); } diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index 26f42d75d..3b09c9edb 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -281,6 +281,12 @@ namespace xr { m_justifications_lim.shrink(old_sz); m_justifications.shrink(old_sz);*/ + for (unsigned i = 0; i < m_gmatrices.size(); i++) + if (m_gmatrices[i] && !m_gqueuedata[i].disabled) + m_gmatrices[i]->enforce_recalculate(); + + check_need_gauss_jordan_disable(); + if (m_region) m_region->pop_scope(num_scopes); } @@ -296,6 +302,17 @@ namespace xr { if (n > 0) pop_core(n); } + + bool solver::check_model(sat::model const& m) const { + for (const auto& clause : m_xorclauses) { + bool eval = false; + for (bool_var v : clause) + eval ^= m[v]; + if (eval != clause.m_rhs) + return false; + } + return true; + } // inprocessing // pre_simplify: decompile all xor constraints to allow other in-processing. @@ -391,6 +408,25 @@ namespace xr { } } + // disables matrixes if applicable + void solver::check_need_gauss_jordan_disable() { + for (unsigned i = 0; i < m_gqueuedata.size(); i++) { + auto& gqd = m_gqueuedata[i]; + if (gqd.disabled) + continue; + + // TODO: Without having the xors also as clauses, this is unsound + /*if (s().get_config().m_xor_gauss_autodisable && + !s().get_config().m_xor_gauss_detach_reattach && + m_gmatrices[i]->must_disable(gqd)) { + gqd.disabled = true; + }*/ + + gqd.reset(); + m_gmatrices[i]->update_cols_vals_set(false); + } + } + // throw away all assigned clash-variables and simplify xor-clause with respect to current assignment // may add conflict or propagate bool solver::clean_one_xor(xor_clause& x) { @@ -461,7 +497,7 @@ namespace xr { bool ret_no_irred_nonxor_contains_clash_vars; if (can_detach && s().get_config().m_xor_gauss_detach_reattach && - !s().get_config().autodisable && + !s().get_config().m_xor_gauss_autodisable && (ret_no_irred_nonxor_contains_clash_vars = no_irred_nonxor_contains_clash_vars())) { detach_xor_clauses(mfinder.clash_vars_unused); unset_clash_decision_vars(xorclauses); diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index c7a988485..64956fac2 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -88,6 +88,8 @@ namespace xr { bool add_simple_xor_constraint(const xor_clause& constraint); + void check_need_gauss_jordan_disable(); + bool inconsistent() const { return s().inconsistent(); } public: @@ -136,5 +138,7 @@ namespace xr { std::ostream& display(std::ostream& out) const override; std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; + + bool check_model(sat::model const& m) const override; }; }