From 43f89dc2ccfbb24f2f13f394595abfd3e29b50bd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 22 Sep 2018 12:01:24 -0700 Subject: [PATCH 1/3] changes in column_info of lar_solver Signed-off-by: Lev Nachmanson --- src/util/lp/column_info.h | 10 ---------- src/util/lp/lar_solver.cpp | 9 ++------- src/util/lp/lar_solver.h | 2 +- src/util/lp/lp_primal_core_solver_def.h | 1 + src/util/lp/lp_solver_def.h | 2 +- 5 files changed, 5 insertions(+), 19 deletions(-) diff --git a/src/util/lp/column_info.h b/src/util/lp/column_info.h index 407f40dfc..2a38900c1 100644 --- a/src/util/lp/column_info.h +++ b/src/util/lp/column_info.h @@ -69,16 +69,6 @@ public: m_column_index(static_cast(-1)) {} - column_info(unsigned column_index) : - m_lower_bound_is_set(false), - m_lower_bound_is_strict(false), - m_upper_bound_is_set (false), - m_upper_bound_is_strict (false), - m_is_fixed(false), - m_cost(numeric_traits::zero()), - m_column_index(column_index) { - } - column_info(const column_info & ci) { m_name = ci.m_name; m_lower_bound_is_set = ci.m_lower_bound_is_set; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 30494aa1c..c83268602 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -909,13 +909,8 @@ bool lar_solver::try_to_set_fixed(column_info & ci) { return false; } -column_type lar_solver::get_column_type(const column_info & ci) { - auto ret = ci.get_column_type_no_flipping(); - if (ret == column_type::boxed) { // changing boxed to fixed because of the no span - if (ci.get_lower_bound() == ci.get_upper_bound()) - ret = column_type::fixed; - } - return ret; +column_type lar_solver::get_column_type(unsigned j) const{ + return m_mpq_lar_core_solver.m_column_types[j]; } std::string lar_solver::get_column_name(unsigned j) const { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index f3aa4f23b..cfe581ba3 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -395,7 +395,7 @@ public: bool try_to_set_fixed(column_info & ci); - column_type get_column_type(const column_info & ci); + column_type get_column_type(unsigned j) const; std::string get_column_name(unsigned j) const; diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h index 1e9edbd31..872922f60 100644 --- a/src/util/lp/lp_primal_core_solver_def.h +++ b/src/util/lp/lp_primal_core_solver_def.h @@ -1238,6 +1238,7 @@ template void lp_primal_core_solver::print_column break; case column_type::free_column: out << "( _" << this->m_x[j] << "_)" << std::endl; + break; default: lp_unreachable(); } diff --git a/src/util/lp/lp_solver_def.h b/src/util/lp/lp_solver_def.h index 10c7a6feb..9b385dee6 100644 --- a/src/util/lp/lp_solver_def.h +++ b/src/util/lp/lp_solver_def.h @@ -24,7 +24,7 @@ Revision History: namespace lp { template column_info * lp_solver::get_or_create_column_info(unsigned column) { auto it = m_map_from_var_index_to_column_info.find(column); - return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info(static_cast(-1))) : it->second; + return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info()) : it->second; } template From 9a09689dfab27059332092bf329db0c4abc258b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Sep 2018 19:19:05 -0700 Subject: [PATCH 2/3] add documentation on the cuber Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 11 ++++++++++- src/sat/sat_lookahead.cpp | 2 ++ src/sat/sat_params.pyg | 28 +++++++++++++++++++++++++--- 3 files changed, 37 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b9e15d329..a6b05904c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6605,7 +6605,12 @@ class Solver(Z3PPObject): _handle_parse_error(e, self.ctx) def cube(self, vars = None): - """Get set of cubes""" + """Get set of cubes + The method takes an optional set of variables that restrict which + variables may be used as a starting point for cubing. + If vars is not None, then the first case split is based on a variable in + this set. + """ self.cube_vs = AstVector(None, self.ctx) if vars is not None: for v in vars: @@ -6621,6 +6626,10 @@ class Solver(Z3PPObject): return def cube_vars(self): + """Access the set of variables that were touched by the most recently generated cube. + This set of variables can be used as a starting point for additional cubes. + The idea is that variables that appear in clauses that are reduced by the most recent + cube are likely more useful to cube on.""" return self.cube_vs def proof(self): diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 3833e2a52..4ca2c5f84 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -16,6 +16,8 @@ Author: Notes: + + --*/ #include diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 89776c479..113a8133e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -50,17 +50,39 @@ def_module_params('sat', ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'), ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'), ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth. + # So if the value is 10, at most 1024 cubes will be generated of length 10. + # - freevars: cutoff based on a variable fraction of lookahead.cube.freevars. + # Cut if the number of current unassigned variables drops below a fraction of number of initial variables. + # - psat: Let psat_heur := (Sum_{clause C} (psat.clause_base ^ {-|C|+1})) / |freevars|^psat.var_exp + # Cut if the value of psat_heur exceeds psat.trigger + # - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables + # at the time of the last conflict. The fraction is increased every time the a cutoff is created. + # - adative_psat: Cut based on psat_heur in an adaptive way. ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), - ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free variable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), - ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), - ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) + ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')) + # reward function used to determine which literal to cube on. + # - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March. + # - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018 + # The score of a literal lit is: + # Sum_{C in Clauses | lit in C} 2 ^ (- |C|+1) + # * Sum_{lit' in C | lit' != lit} lit_occs(~lit') + # / | C | + # where lit_occs(lit) is the number of clauses containing lit. + # - heuleu: The score of a literal lit is: Sum_{C in Clauses | lit in C} 2 ^ (-|C| + 1) + # - unit: heule_schur + also counts number of unit clauses. + # - march_cu: default reward function used in a version of March + # Each reward function also comes with its own variant of "mix_diff", which + # is the function for combining reward metrics for the positive and negative variant of a literal. + ) From 066b5334ad5882dff635abd354928f14b9a3c4d2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 22 Sep 2018 20:57:59 -0700 Subject: [PATCH 3/3] refactor some parameters into fields in Gomory cuts Signed-off-by: Lev Nachmanson --- src/util/lp/gomory.cpp | 119 +++++++++++++++++++++-------------------- 1 file changed, 62 insertions(+), 57 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 96b3ab395..ad1c02625 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -27,11 +27,15 @@ class gomory::imp { lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut explanation& m_ex; // the conflict explanation - unsigned m_inf_col; // a basis column which has to be an integer but has a not integral value + unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value const row_strip& m_row; - const int_solver& m_int_solver; - - + const int_solver& m_int_solver; + mpq m_lcm_den; + mpq m_f; + mpq m_one_minus_f; + mpq m_fj; + mpq m_one_minus_fj; + const impq & get_value(unsigned j) const { return m_int_solver.get_value(j); } bool is_real(unsigned j) const { return m_int_solver.is_real(j); } bool at_lower(unsigned j) const { return m_int_solver.at_lower(j); } @@ -42,66 +46,60 @@ class gomory::imp { constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); } bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); } - void int_case_in_gomory_cut(const mpq & a, unsigned j, - mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) { - lp_assert(is_int(j) && !a.is_int()); - mpq fj = fractional_part(a); + void int_case_in_gomory_cut(unsigned j) { + lp_assert(is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", - tout << a << " j=" << j << " k = " << m_k; - tout << ", fj: " << fj << ", "; - tout << "a - fj = " << a - fj << ", "; + tout << " k = " << m_k; + tout << ", fj: " << m_fj << ", "; tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl; ); - lp_assert(fj.is_pos() && (a - fj).is_int()); mpq new_a; if (at_lower(j)) { - new_a = fj <= one_minus_f0 ? fj / one_minus_f0 : ((1 - fj) / f0); + new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); lp_assert(new_a.is_pos()); m_k.addmul(new_a, lower_bound(j).x); - m_ex.push_justification(column_lower_bound_constraint(j), new_a); + m_ex.push_justification(column_lower_bound_constraint(j)); } else { lp_assert(at_upper(j)); // the upper terms are inverted: therefore we have the minus - new_a = - (fj <= f0 ? fj / f0 : ((1 - fj) / one_minus_f0)); + new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); lp_assert(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); - m_ex.push_justification(column_upper_bound_constraint(j), new_a); + m_ex.push_justification(column_upper_bound_constraint(j)); } m_t.add_monomial(new_a, j); - lcm_den = lcm(lcm_den, denominator(new_a)); - TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";); + m_lcm_den = lcm(m_lcm_den, denominator(new_a)); + TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", m_lcm_den = " << m_lcm_den << "\n";); } - void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) { + void real_case_in_gomory_cut(const mpq & a, unsigned j) { TRACE("gomory_cut_detail_real", tout << "real\n";); mpq new_a; - if (at_lower(x_j)) { + if (at_lower(j)) { if (a.is_pos()) { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } else { - new_a = a / f0; - new_a.neg(); + new_a = - a / m_f; } - m_k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than - // k += lower_bound(x_j).x * new_a; - m_ex.push_justification(column_lower_bound_constraint(x_j), new_a); + m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than + // k += lower_bound(j).x * new_a; + m_ex.push_justification(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(x_j)); + lp_assert(at_upper(j)); if (a.is_pos()) { - new_a = a / f0; - new_a.neg(); // the upper terms are inverted. + new_a = - a / m_f; } else { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } - m_k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a; - m_ex.push_justification(column_upper_bound_constraint(x_j), new_a); + m_k.addmul(new_a, upper_bound(j).x); // k += upper_bound(j).x * new_a; + m_ex.push_justification(column_upper_bound_constraint(j)); } - TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << m_k << "\n";); - m_t.add_monomial(new_a, x_j); + TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";); + m_t.add_monomial(new_a, j); } lia_move report_conflict_from_gomory_cut() { @@ -111,7 +109,7 @@ class gomory::imp { return lia_move::conflict; } - void adjust_term_and_k_for_some_ints_case_gomory(mpq &lcm_den) { + void adjust_term_and_k_for_some_ints_case_gomory() { lp_assert(!m_t.is_empty()); // k = 1 + sum of m_t at bounds auto pol = m_t.coeffs_as_vector(); @@ -134,16 +132,16 @@ class gomory::imp { m_t.add_monomial(mpq(1), v); } } else { - lcm_den = lcm(lcm_den, denominator(m_k)); - lp_assert(lcm_den.is_pos()); - TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << lcm_den << std::endl;); - if (!lcm_den.is_one()) { + m_lcm_den = lcm(m_lcm_den, denominator(m_k)); + lp_assert(m_lcm_den.is_pos()); + TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;); + if (!m_lcm_den.is_one()) { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { - pi.first *= lcm_den; + pi.first *= m_lcm_den; SASSERT(!is_int(pi.second) || pi.first.is_int()); } - m_k *= lcm_den; + m_k *= m_lcm_den; } // negate everything to return -pol <= -m_k for (const auto & pi: pol) { @@ -275,14 +273,14 @@ public: // gomory will be t <= k and the current solution has a property t > k m_k = 1; m_t.clear(); - mpq lcm_den(1); + mpq m_lcm_den(1); bool some_int_columns = false; - mpq f0 = fractional_part(get_value(m_inf_col)); - TRACE("gomory_cut_detail", tout << "f0: " << f0 << ", "; - tout << "1 - f0: " << 1 - f0 << ", get_value(m_inf_col).x - f0 = " << get_value(m_inf_col).x - f0;); - lp_assert(f0.is_pos() && (get_value(m_inf_col).x - f0).is_int()); + mpq m_f = fractional_part(get_value(m_inf_col)); + TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; + tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f;); + lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); - mpq one_min_f0 = 1 - f0; + mpq one_min_m_f = 1 - m_f; for (const auto & p : m_row) { unsigned j = p.var(); if (j == m_inf_col) { @@ -290,20 +288,26 @@ public: TRACE("gomory_cut_detail", tout << "seeing basic var";); continue; } - // make the format compatible with the format used in: Integrating Simplex with DPLL(T) - mpq a = - p.coeff(); - if (is_real(j)) - real_case_in_gomory_cut(a, j, f0, one_min_f0); - else if (!a.is_int()) { // fj will be zero and no monomial will be added + + // use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T) + if (is_real(j)) { + real_case_in_gomory_cut(- p.coeff(), j); + } else { + if (p.coeff().is_int()) { + // m_fj will be zero and no monomial will be added + continue; + } some_int_columns = true; - int_case_in_gomory_cut(a, j, lcm_den, f0, one_min_f0); + m_fj = fractional_part(-p.coeff()); + m_one_minus_fj = 1 - m_fj; + int_case_in_gomory_cut(j); } } if (m_t.is_empty()) return report_conflict_from_gomory_cut(); if (some_int_columns) - adjust_term_and_k_for_some_ints_case_gomory(lcm_den); + adjust_term_and_k_for_some_ints_case_gomory(); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); m_int_solver.m_lar_solver->subs_term_columns(m_t); @@ -317,9 +321,10 @@ public: m_ex(ex), m_inf_col(basic_inf_int_j), m_row(row), - m_int_solver(int_slv) - { - } + m_int_solver(int_slv), + m_lcm_den(1), + m_f(fractional_part(get_value(basic_inf_int_j).x)), + m_one_minus_f(1 - m_f) {} };