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

Merge pull request #11 from TheRealNebus/opt

Browse source 
Opt
This commit is contained in:
Nikolaj Bjorner 2017-12-05 18:03:24 -08:00 committed by GitHub
parent fc3cbcbe02 38751430df
commit 9ff724ec6d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
5 changed files with 108 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/sat/sat_config.cpp
View file

@ -109,8 +109,30 @@ 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("depth")) {
m_lookahead_cube_cutoff = depth_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 'depth', 'freevars', 'psat', 'adaptive_freevars' and 'adaptive_psat'");
}
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_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

15
src/sat/sat_config.h
View file

@ -65,6 +65,14 @@ namespace sat {
march_cu_reward
};
enum cutoff_t {
depth_cutoff,
freevars_cutoff,
psat_cutoff,
adaptive_freevars_cutoff,
adaptive_psat_cutoff
};
struct config {
unsigned long long m_max_memory;
phase_selection m_phase;
@ -84,8 +92,13 @@ namespace sat {
bool m_local_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;
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;

48
src/sat/sat_lookahead.cpp
View file

@ -1033,6 +1033,7 @@ namespace sat {
}
propagate();
m_qhead = m_trail.size();
m_init_freevars = m_freevars.size();
TRACE("sat", m_s.display(tout); display(tout););
}
@ -2018,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();
@ -2062,9 +2092,14 @@ 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)) {
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
@ -2077,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;
@ -2500,6 +2537,11 @@ 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;
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 {

21
src/sat/sat_lookahead.h
View file

@ -80,8 +80,13 @@ 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;
double m_cube_psat_var_exp;
double m_cube_psat_clause_base;
double m_cube_psat_trigger;
config() {
memset(this, sizeof(*this), 0);
@ -96,8 +101,13 @@ namespace sat {
m_dl_max_iterations = 2;
m_tc1_limit = 10000000;
m_reward_type = ternary_reward;
m_cube_cutoff = 0;
m_cube_cutoff = adaptive_freevars_cutoff;
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;
}
};
@ -167,6 +177,7 @@ namespace sat {
svector<bool> m_is_decision;
literal_vector m_cube;
double m_freevars_threshold;
double m_psat_threshold;
unsigned m_conflicts;
unsigned m_cutoffs;
cube_state() { reset(); }
@ -175,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; }
@ -228,11 +240,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
@ -542,6 +555,8 @@ namespace sat {
void add_hyper_binary();
double psat_heur();
public:
lookahead(solver& s) :
m_s(s),

10
src/sat/sat_params.pyg
View file

@ -37,8 +37,14 @@ 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.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_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. 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'),
('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),