From e0dfbd6d1cf7341da84a315bb1e715d3767c9126 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Mon, 4 Dec 2017 14:33:48 -0800 Subject: [PATCH] fixed freevars and psat cube cutoffs Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 6 ++++++ src/sat/sat_config.h | 6 +++++- src/sat/sat_lookahead.cpp | 38 +++++++++++++++++++++++++++++++++++--- src/sat/sat_lookahead.h | 8 ++++++++ src/sat/sat_params.pyg | 4 ++-- 5 files changed, 56 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index bd2a48ff2..b0797dae9 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -121,12 +121,18 @@ namespace sat { else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) { m_lookahead_cube_cutoff = fixed_freevars_cutoff; } + else if (p.lookahead_cube_cutoff() == symbol("psat")) { + m_lookahead_cube_cutoff = psat_cutoff; + } else { throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'adaptive', 'fixed_depth', 'fixed_freevars'"); } m_lookahead_cube_fraction = p.lookahead_cube_fraction(); m_lookahead_cube_depth = p.lookahead_cube_depth(); m_lookahead_cube_freevars = p.lookahead_cube_freevars(); + m_lookahead_cube_psat_var_exp = p.lookahead_cube_psat_var_exp(); + m_lookahead_cube_psat_clause_base = p.lookahead_cube_psat_clause_base(); + m_lookahead_cube_psat_trigger = p.lookahead_cube_psat_trigger(); m_lookahead_global_autarky = p.lookahead_global_autarky(); // These parameters are not exposed diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index f6f6774fc..1529466ee 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -68,7 +68,8 @@ namespace sat { enum cutoff_t { adaptive_cutoff, fixed_depth_cutoff, - fixed_freevars_cutoff + fixed_freevars_cutoff, + psat_cutoff }; struct config { @@ -95,6 +96,9 @@ namespace sat { double m_lookahead_cube_fraction; unsigned m_lookahead_cube_depth; double m_lookahead_cube_freevars; + double m_lookahead_cube_psat_var_exp; + double m_lookahead_cube_psat_clause_base; + double m_lookahead_cube_psat_trigger; reward_t m_lookahead_reward; bool m_lookahead_global_autarky; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 6aae5738e..3feb9455d 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2019,6 +2019,35 @@ namespace sat { st.update("lh cube conflicts", m_cube_state.m_conflicts); } + double lookahead::psat_heur() { + double h = 0.0; + for (bool_var x : m_freevars) { + literal l(x, false); + for (literal lit : m_binary[l.index()]) { + h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0; + } + for (literal lit : m_binary[(~l).index()]) { + h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0; + } + for (binary b : m_ternary[l.index()]) { + h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ? + 1.0 / pow(m_config.m_cube_psat_clause_base, 2) : + 0.0; + } + for (binary b : m_ternary[(~l).index()]) { + h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ? + 1.0 / pow(m_config.m_cube_psat_clause_base, 2) : + 0.0; + } + } + for (nary * n : m_nary_clauses) { + h += 1.0 / pow(m_config.m_cube_psat_clause_base, n->size() - 1); + } + h /= pow(m_freevars.size(), m_config.m_cube_psat_var_exp); + IF_VERBOSE(10, verbose_stream() << "(sat-cube-psat :val " << h << ")\n";); + return h; + } + lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { scoped_ext _scoped_ext(*this); lits.reset(); @@ -2065,9 +2094,8 @@ namespace sat { depth = m_cube_state.m_cube.size(); if ((m_config.m_cube_cutoff == fixed_depth_cutoff && depth == m_config.m_cube_depth) || (m_config.m_cube_cutoff == adaptive_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || - /* m_cube_cutoff is fixed_freevars */ m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) { - /*if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || - (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {*/ + (m_config.m_cube_cutoff == fixed_freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || + (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger)) { m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); set_conflict(); m_cube_state.inc_cutoff(); @@ -2085,6 +2113,7 @@ namespace sat { if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); m_cube_state.m_freevars_threshold = prev_nfreevars; + m_cube_state.inc_conflict(); if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; } @@ -2503,6 +2532,9 @@ namespace sat { m_config.m_cube_fraction = m_s.m_config.m_lookahead_cube_fraction; m_config.m_cube_depth = m_s.m_config.m_lookahead_cube_depth; m_config.m_cube_freevars = m_s.m_config.m_lookahead_cube_freevars; + m_config.m_cube_psat_var_exp = m_s.m_config.m_lookahead_cube_psat_var_exp; + m_config.m_cube_psat_clause_base = m_s.m_config.m_lookahead_cube_psat_clause_base; + m_config.m_cube_psat_trigger = m_s.m_config.m_lookahead_cube_psat_trigger; } void lookahead::collect_statistics(statistics& st) const { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index bd4198dcd..254dd614f 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -84,6 +84,9 @@ namespace sat { unsigned m_cube_depth; double m_cube_fraction; double m_cube_freevars; + double m_cube_psat_var_exp; + double m_cube_psat_clause_base; + double m_cube_psat_trigger; config() { memset(this, sizeof(*this), 0); @@ -102,6 +105,9 @@ namespace sat { m_cube_depth = 10; m_cube_fraction = 0.4; m_cube_freevars = 0.8; + m_cube_psat_var_exp = 1.0; + m_cube_psat_clause_base = 2.0; + m_cube_psat_trigger = 5.0; } }; @@ -547,6 +553,8 @@ namespace sat { void add_hyper_binary(); + double psat_heur(); + public: lookahead(solver& s) : m_s(s), diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 085f0c067..565c6dbcc 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -42,8 +42,8 @@ def_module_params('sat', ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is fixed_depth.'), ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is fixed_freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), - ('lookahead.cube.psat.clause_base', DOUBLE, 1, 'clause base for PSAT cutoff') - ('lookahead.cube.psat.probability', DOUBLE' 0.5, 'probability to create lookahead cubes 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'), ('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'),