mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

freevars cube 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-01 11:02:29 -08:00
parent 427b5ef002
commit 1b7cb110d3
5 changed files with 46 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/sat/sat_config.cpp
View file

@ -112,8 +112,21 @@ 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;
}
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 {
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_cutoff = p.lookahead_cube_cutoff();
m_lookahead_cube_depth = p.lookahead_cube_depth();
m_lookahead_cube_freevars = p.lookahead_cube_freevars();
m_lookahead_global_autarky = p.lookahead_global_autarky();
// These parameters are not exposed

10
src/sat/sat_config.h
View file

@ -65,6 +65,12 @@ namespace sat {
march_cu_reward
};
enum cutoff_t {
adaptive_cutoff,
fixed_depth_cutoff,
fixed_freevars_cutoff
};
struct config {
unsigned long long m_max_memory;
phase_selection m_phase;
@ -85,8 +91,10 @@ namespace sat {
bool m_lookahead_search;
bool m_lookahead_simplify;
bool m_lookahead_simplify_bca;
unsigned m_lookahead_cube_cutoff;
cutoff_t m_lookahead_cube_cutoff;
double m_lookahead_cube_fraction;
unsigned m_lookahead_cube_depth;
double m_lookahead_cube_freevars;
reward_t m_lookahead_reward;
bool m_lookahead_global_autarky;

10
src/sat/sat_lookahead.cpp
View file

@ -1032,6 +1032,7 @@ namespace sat {
}
propagate();
m_qhead = m_trail.size();
m_init_freevars = m_freevars.size();
TRACE("sat", m_s.display(tout); display(tout););
}
@ -2054,8 +2055,11 @@ namespace sat {
}
backtrack_level = UINT_MAX;
depth = m_cube_state.m_cube.size();
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)) {
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_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
set_conflict();
#if 0
@ -2413,6 +2417,8 @@ namespace sat {
m_config.m_reward_type = m_s.m_config.m_lookahead_reward;
m_config.m_cube_cutoff = m_s.m_config.m_lookahead_cube_cutoff;
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;
}
void lookahead::collect_statistics(statistics& st) const {

11
src/sat/sat_lookahead.h
View file

@ -80,8 +80,10 @@ namespace sat {
unsigned m_dl_max_iterations;
unsigned m_tc1_limit;
reward_t m_reward_type;
unsigned m_cube_cutoff;
cutoff_t m_cube_cutoff;
unsigned m_cube_depth;
double m_cube_fraction;
double m_cube_freevars;
config() {
memset(this, sizeof(*this), 0);
@ -96,8 +98,10 @@ namespace sat {
m_dl_max_iterations = 2;
m_tc1_limit = 10000000;
m_reward_type = ternary_reward;
m_cube_cutoff = 0;
m_cube_cutoff = adaptive_cutoff;
m_cube_depth = 10;
m_cube_fraction = 0.4;
m_cube_freevars = 0.8;
}
};
@ -222,11 +226,12 @@ namespace sat {
svector<prefix> m_vprefix; // var: prefix where variable participates in propagation
unsigned m_rating_throttle; // throttle to recompute rating
indexed_uint_set m_freevars;
unsigned m_init_freevars;
lookahead_mode m_search_mode; // mode of search
stats m_stats;
model m_model;
cube_state m_cube_state;
scoped_ptr<extension> m_ext;
scoped_ptr<extension> m_ext;
// ---------------------------------------
// truth values

9
src/sat/sat_params.pyg
View file

@ -37,8 +37,13 @@ def_module_params('sat',
('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search', BOOL, False, 'use local search instead of CDCL'),
('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
('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.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_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'),