From 38751430df4078e14feda6d8e50f9bf5ae1b1419 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 5 Dec 2017 17:53:48 -0800 Subject: [PATCH] adaptive psat cutoff Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 19 +++++++++++-------- src/sat/sat_config.h | 9 +++++---- src/sat/sat_lookahead.cpp | 15 ++++++++++----- src/sat/sat_lookahead.h | 4 +++- src/sat/sat_params.pyg | 10 +++++----- 5 files changed, 34 insertions(+), 23 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 87d84f133..660337071 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -109,20 +109,23 @@ namespace sat { throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'"); } - if (p.lookahead_cube_cutoff() == symbol("adaptive")) { - m_lookahead_cube_cutoff = adaptive_cutoff; + if (p.lookahead_cube_cutoff() == symbol("depth")) { + m_lookahead_cube_cutoff = depth_cutoff; } - else if (p.lookahead_cube_cutoff() == symbol("fixed_depth")) { - m_lookahead_cube_cutoff = fixed_depth_cutoff; - } - else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) { - m_lookahead_cube_cutoff = fixed_freevars_cutoff; + else if (p.lookahead_cube_cutoff() == symbol("freevars")) { + m_lookahead_cube_cutoff = freevars_cutoff; } else if (p.lookahead_cube_cutoff() == symbol("psat")) { m_lookahead_cube_cutoff = psat_cutoff; } + else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars")) { + m_lookahead_cube_cutoff = adaptive_freevars_cutoff; + } + else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat")) { + m_lookahead_cube_cutoff = adaptive_psat_cutoff; + } else { - throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'adaptive', 'fixed_depth', 'fixed_freevars'"); + throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'depth', 'freevars', 'psat', 'adaptive_freevars' and 'adaptive_psat'"); } m_lookahead_cube_fraction = p.lookahead_cube_fraction(); m_lookahead_cube_depth = p.lookahead_cube_depth(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index ed7802cef..f66c0dbdf 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -66,10 +66,11 @@ namespace sat { }; enum cutoff_t { - adaptive_cutoff, - fixed_depth_cutoff, - fixed_freevars_cutoff, - psat_cutoff + depth_cutoff, + freevars_cutoff, + psat_cutoff, + adaptive_freevars_cutoff, + adaptive_psat_cutoff }; struct config { diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index a9ae3b641..ec1bf23f2 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2092,11 +2092,14 @@ namespace sat { } backtrack_level = UINT_MAX; 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_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)); + if ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) || + (m_config.m_cube_cutoff == 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_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || + (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) { + double dec = (1.0 - pow(m_config.m_cube_fraction, depth)); + m_cube_state.m_freevars_threshold *= dec; + m_cube_state.m_psat_threshold *= dec; set_conflict(); m_cube_state.inc_cutoff(); #if 0 @@ -2109,10 +2112,12 @@ namespace sat { return l_undef; } int prev_nfreevars = m_freevars.size(); + double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX; // MN. only compute PSAT if enabled literal lit = choose(); if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); m_cube_state.m_freevars_threshold = prev_nfreevars; + m_cube_state.m_psat_threshold = prev_psat; m_cube_state.inc_conflict(); if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 254dd614f..6a7bb7449 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -101,7 +101,7 @@ namespace sat { m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; - m_cube_cutoff = adaptive_cutoff; + m_cube_cutoff = adaptive_freevars_cutoff; m_cube_depth = 10; m_cube_fraction = 0.4; m_cube_freevars = 0.8; @@ -177,6 +177,7 @@ namespace sat { svector m_is_decision; literal_vector m_cube; double m_freevars_threshold; + double m_psat_threshold; unsigned m_conflicts; unsigned m_cutoffs; cube_state() { reset(); } @@ -185,6 +186,7 @@ namespace sat { m_is_decision.reset(); m_cube.reset(); m_freevars_threshold = 0; + m_psat_threshold = DBL_MAX; reset_stats(); } void reset_stats() { m_conflicts = 0; m_cutoffs = 0; } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 0e6823030..4432c0b16 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -37,13 +37,13 @@ def_module_params('sat', ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), - ('lookahead.cube.cutoff', SYMBOL, 'adaptive', 'cutoff type used to create lookahead cubes: adaptive, fixed_depth, fixed_freevars, psat'), - ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive'), - ('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.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + ('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, 10, '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.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'), + ('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'),