mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fixed freevars and psat cube cutoffs

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-04 14:33:48 -08:00
parent 2e042a8bea
commit e0dfbd6d1c
5 changed files with 56 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_config.cpp
View file

@ -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

6
src/sat/sat_config.h
View file

@ -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;

38
src/sat/sat_lookahead.cpp
View file

@ -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 {

8
src/sat/sat_lookahead.h
View file

@ -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),

4
src/sat/sat_params.pyg
View file

@ -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'),