mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

adaptive psat cutoff

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-05 17:53:48 -08:00
parent d8a62dff73
commit 38751430df
5 changed files with 34 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/sat/sat_config.cpp
View file

@ -109,20 +109,23 @@ namespace sat {
throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'"); throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
} }
if (p.lookahead_cube_cutoff() == symbol("adaptive")) { if (p.lookahead_cube_cutoff() == symbol("depth")) {
m_lookahead_cube_cutoff = adaptive_cutoff; m_lookahead_cube_cutoff = depth_cutoff;
} }
else if (p.lookahead_cube_cutoff() == symbol("fixed_depth")) { else if (p.lookahead_cube_cutoff() == symbol("freevars")) {
m_lookahead_cube_cutoff = fixed_depth_cutoff; m_lookahead_cube_cutoff = freevars_cutoff;
}
else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) {
m_lookahead_cube_cutoff = fixed_freevars_cutoff;
} }
else if (p.lookahead_cube_cutoff() == symbol("psat")) { else if (p.lookahead_cube_cutoff() == symbol("psat")) {
m_lookahead_cube_cutoff = psat_cutoff; 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 { 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_fraction = p.lookahead_cube_fraction();
m_lookahead_cube_depth = p.lookahead_cube_depth(); m_lookahead_cube_depth = p.lookahead_cube_depth();

9
src/sat/sat_config.h
View file

@ -66,10 +66,11 @@ namespace sat {
}; };
enum cutoff_t { enum cutoff_t {
adaptive_cutoff, depth_cutoff,
fixed_depth_cutoff, freevars_cutoff,
fixed_freevars_cutoff, psat_cutoff,
psat_cutoff adaptive_freevars_cutoff,
adaptive_psat_cutoff
}; };
struct config { struct config {

15
src/sat/sat_lookahead.cpp
View file

@ -2092,11 +2092,14 @@ namespace sat {
} }
backtrack_level = UINT_MAX; backtrack_level = UINT_MAX;
depth = m_cube_state.m_cube.size(); depth = m_cube_state.m_cube.size();
if ((m_config.m_cube_cutoff == fixed_depth_cutoff && depth == m_config.m_cube_depth) || if ((m_config.m_cube_cutoff == 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 == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) ||
(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_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_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); (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(); set_conflict();
m_cube_state.inc_cutoff(); m_cube_state.inc_cutoff();
#if 0 #if 0
@ -2109,10 +2112,12 @@ namespace sat {
return l_undef; return l_undef;
} }
int prev_nfreevars = m_freevars.size(); 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(); literal lit = choose();
if (inconsistent()) { if (inconsistent()) {
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
m_cube_state.m_freevars_threshold = prev_nfreevars; m_cube_state.m_freevars_threshold = prev_nfreevars;
m_cube_state.m_psat_threshold = prev_psat;
m_cube_state.inc_conflict(); m_cube_state.inc_conflict();
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
continue; continue;

4
src/sat/sat_lookahead.h
View file

@ -101,7 +101,7 @@ namespace sat {
m_dl_max_iterations = 2; m_dl_max_iterations = 2;
m_tc1_limit = 10000000; m_tc1_limit = 10000000;
m_reward_type = ternary_reward; m_reward_type = ternary_reward;
m_cube_cutoff = adaptive_cutoff; m_cube_cutoff = adaptive_freevars_cutoff;
m_cube_depth = 10; m_cube_depth = 10;
m_cube_fraction = 0.4; m_cube_fraction = 0.4;
m_cube_freevars = 0.8; m_cube_freevars = 0.8;
@ -177,6 +177,7 @@ namespace sat {
svector<bool> m_is_decision; svector<bool> m_is_decision;
literal_vector m_cube; literal_vector m_cube;
double m_freevars_threshold; double m_freevars_threshold;
double m_psat_threshold;
unsigned m_conflicts; unsigned m_conflicts;
unsigned m_cutoffs; unsigned m_cutoffs;
cube_state() { reset(); } cube_state() { reset(); }
@ -185,6 +186,7 @@ namespace sat {
m_is_decision.reset(); m_is_decision.reset();
m_cube.reset(); m_cube.reset();
m_freevars_threshold = 0; m_freevars_threshold = 0;
m_psat_threshold = DBL_MAX;
reset_stats(); reset_stats();
} }
void reset_stats() { m_conflicts = 0; m_cutoffs = 0; } void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }

10
src/sat/sat_params.pyg
View file

@ -37,13 +37,13 @@ def_module_params('sat',
('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('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', BOOL, False, 'use local search instead of CDCL'),
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('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.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'), ('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 fixed_depth.'), ('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 fixed_freevars'), ('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.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.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_search', BOOL, False, 'use lookahead solver'),
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),