mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

disable uhle from lookahead solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-01 19:56:01 -08:00
parent 75bf942237
commit eca250933d
12 changed files with 213 additions and 96 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/sat/sat_asymm_branch.cpp
View file

@ -150,27 +150,6 @@ namespace sat {
}
}
void asymm_branch::operator()(big& big) {
s.propagate(false);
if (s.m_inconsistent)
return;
report rpt(*this);
for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) {
unsigned elim = m_elim_literals;
big.reinit();
process(&big, s.m_clauses);
process(&big, s.m_learned);
process_bin(big);
unsigned num_elim = m_elim_literals - elim;
IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
if (num_elim == 0)
break;
if (num_elim > 1000)
i = 0;
}
s.propagate(false);
}
void asymm_branch::operator()(bool force) {
++m_calls;
@ -196,11 +175,11 @@ namespace sat {
++counter;
change = false;
if (m_asymm_branch_sampled) {
big big(s.m_rand, true);
big big(s.m_rand);
if (process(big, true)) change = true;
}
if (m_asymm_branch_sampled) {
big big(s.m_rand, false);
big big(s.m_rand);
if (process(big, false)) change = true;
}
if (m_asymm_branch) {
@ -431,11 +410,10 @@ namespace sat {
bool asymm_branch::process_sampled(big& big, clause & c) {
scoped_detach scoped_d(s, c);
sort(big, c);
if (!big.learned() && !c.is_learned() && uhte(big, c)) {
// TBD: mark clause as learned.
++m_hidden_tautologies;
scoped_d.del_clause();
return false;
if (uhte(big, c)) {
// don't touch hidden tautologies.
// ATE takes care of them.
return true;
}
return uhle(scoped_d, big, c);
}

2
src/sat/sat_asymm_branch.h
View file

@ -91,8 +91,6 @@ namespace sat {
void operator()(bool force);
void operator()(big& big);
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);

4
src/sat/sat_big.cpp
View file

@ -21,9 +21,8 @@ Revision History:
namespace sat {
big::big(random_gen& rand, bool binary):
big::big(random_gen& rand):
m_rand(rand) {
m_binary = binary;
}
void big::init(solver& s, bool learned) {
@ -141,7 +140,6 @@ namespace sat {
}
unsigned big::reduce_tr(solver& s) {
if (!m_binary && learned()) return 0;
unsigned num_lits = s.num_vars() * 2;
unsigned idx = 0;
unsigned elim = 0;

2
src/sat/sat_big.h
View file

@ -41,7 +41,7 @@ namespace sat {
public:
big(random_gen& rand, bool binary);
big(random_gen& rand);
/**
\brief initialize a BIG from a solver.
*/

1
src/sat/sat_config.cpp
View file

@ -76,7 +76,6 @@ namespace sat {
m_unit_walk_threads = p.unit_walk_threads();
m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_simplify_bca = p.lookahead_simplify_bca();
m_lookahead_simplify_asymm_branch = p.lookahead_simplify_asymm_branch();
if (p.lookahead_reward() == symbol("heule_schur"))
m_lookahead_reward = heule_schur_reward;
else if (p.lookahead_reward() == symbol("heuleu"))

1
src/sat/sat_config.h
View file

@ -94,7 +94,6 @@ namespace sat {
bool m_unit_walk;
bool m_lookahead_simplify;
bool m_lookahead_simplify_bca;
bool m_lookahead_simplify_asymm_branch;
cutoff_t m_lookahead_cube_cutoff;
double m_lookahead_cube_fraction;
unsigned m_lookahead_cube_depth;

29
src/sat/sat_lookahead.cpp
View file

@ -2306,16 +2306,12 @@ namespace sat {
roots[v] = p;
VERIFY(get_parent(p) == p);
VERIFY(get_parent(~p) == ~p);
IF_VERBOSE(0, verbose_stream() << p << " " << q << "\n";);
}
}
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :equivalences " << to_elim.size() << ")\n";);
elim_eqs elim(m_s);
elim(roots, to_elim);
if (get_config().m_lookahead_simplify_asymm_branch) {
big_asymm_branch(learned);
}
if (learned && get_config().m_lookahead_simplify_bca) {
add_hyper_binary();
}
@ -2324,29 +2320,6 @@ namespace sat {
m_lookahead.reset();
}
/**
\brief extract binary implication graph from learned binary clauses and use it
for strengthening clauses.
*/
void lookahead::big_asymm_branch(bool learned) {
unsigned num_lits = m_s.num_vars() * 2;
unsigned idx = 0;
big big(m_s.m_rand, false);
big.init_adding_edges(m_s.num_vars(), learned);
for (auto const& lits : m_binary) {
literal u = get_parent(to_literal(idx++));
if (u == null_literal) continue;
for (literal v : lits) {
v = get_parent(v);
if (v != null_literal)
big.add_edge(u, v);
}
}
big.done_adding_edges();
asymm_branch ab(m_s, m_s.m_params);
ab(big);
}
/**
\brief reduction based on binary implication graph
@ -2372,7 +2345,7 @@ namespace sat {
}
}
big big(m_s.m_rand, false);
big big(m_s.m_rand);
big.init(m_s, true);
svector<std::pair<literal, literal>> candidates;

2
src/sat/sat_lookahead.h
View file

@ -555,8 +555,6 @@ namespace sat {
void add_hyper_binary();
void big_asymm_branch(bool learned);
double psat_heur();
public:

1
src/sat/sat_params.pyg
View file

@ -51,7 +51,6 @@ def_module_params('sat',
('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, True, 'add learned binary clauses as part of lookahead simplification'),
('lookahead_simplify.asymm_branch', BOOL, True, 'apply asymmetric branch simplification with lookahead simplifier'),
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))

2
src/sat/sat_scc.cpp
View file

@ -27,7 +27,7 @@ namespace sat {
scc::scc(solver & s, params_ref const & p):
m_solver(s),
m_big(s.m_rand, true) {
m_big(s.m_rand) {
reset_statistics();
updt_params(p);
}

2
src/sat/sat_simplifier.cpp
View file

@ -214,7 +214,7 @@ namespace sat {
}
register_clauses(s.m_clauses);
if (bce_enabled() || bca_enabled() || ate_enabled()) {
if (!learned && (bce_enabled() || bca_enabled() || ate_enabled())) {
elim_blocked_clauses();
}