mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 09:35:32 +00:00
testing double lookahead
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c0188a7ec0
commit
b70096a97f
6 changed files with 75 additions and 16 deletions
|
|
@ -449,6 +449,23 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
void drat::add(literal_vector const& c) {
|
||||
for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
|
||||
if (m_out) dump(c.size(), c.begin(), status::learned);
|
||||
if (s.m_config.m_drat_check) {
|
||||
switch (c.size()) {
|
||||
case 0: add(); break;
|
||||
case 1: append(c[0], status::learned); break;
|
||||
default: {
|
||||
verify(c.size(), c.begin());
|
||||
clause* cl = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), true);
|
||||
append(*cl, status::external);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void drat::del(literal l) {
|
||||
if (m_out) dump(1, &l, status::deleted);
|
||||
if (s.m_config.m_drat_check) append(l, status::deleted);
|
||||
|
|
|
|||
|
|
@ -57,6 +57,7 @@ namespace sat {
|
|||
void append(literal l, status st);
|
||||
void append(literal l1, literal l2, status st);
|
||||
void append(clause& c, status st);
|
||||
|
||||
friend std::ostream& operator<<(std::ostream & out, status st);
|
||||
status get_status(bool learned) const;
|
||||
|
||||
|
|
@ -82,6 +83,7 @@ namespace sat {
|
|||
void add(literal l1, literal l2, bool learned);
|
||||
void add(clause& c, bool learned);
|
||||
void add(literal_vector const& c, svector<premise> const& premises);
|
||||
void add(literal_vector const& c); // add learned clause
|
||||
|
||||
bool is_cleaned(clause& c) const;
|
||||
void del(literal l);
|
||||
|
|
|
|||
|
|
@ -142,11 +142,11 @@ namespace sat {
|
|||
// the current best noise is below 1000
|
||||
if (best_unsat_rate >= last_best_unsat_rate) {
|
||||
// worse
|
||||
noise = noise - noise * 2 * noise_delta;
|
||||
m_noise -= m_noise * 2 * m_noise_delta;
|
||||
}
|
||||
else {
|
||||
// better
|
||||
noise = noise + (10000 - noise) * noise_delta;
|
||||
m_noise += (10000 - m_noise) * m_noise_delta;
|
||||
}
|
||||
for (unsigned i = 0; i < m_constraints.size(); ++i) {
|
||||
constraint& c = m_constraints[i];
|
||||
|
|
@ -381,7 +381,7 @@ namespace sat {
|
|||
if (tries % 10 == 0 || m_unsat_stack.empty()) { \
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \
|
||||
<< " :flips " << flips \
|
||||
<< " :noise " << noise \
|
||||
<< " :noise " << m_noise \
|
||||
<< " :unsat " << /*m_unsat_stack.size()*/ best_unsat \
|
||||
<< " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \
|
||||
}
|
||||
|
|
@ -506,7 +506,7 @@ namespace sat {
|
|||
SASSERT(c.m_k < constraint_value(c));
|
||||
// TBD: dynamic noise strategy
|
||||
//if (m_rand() % 100 < 98) {
|
||||
if (m_rand() % 10000 >= noise) {
|
||||
if (m_rand() % 10000 >= m_noise) {
|
||||
// take this branch with 98% probability.
|
||||
// find the first one, to fast break the rest
|
||||
unsigned best_bsb = 0;
|
||||
|
|
|
|||
|
|
@ -176,8 +176,8 @@ namespace sat {
|
|||
unsigned m_max_steps = (1 << 30);
|
||||
|
||||
// dynamic noise
|
||||
unsigned noise = 400; // normalized by 10000
|
||||
double noise_delta = 0.05;
|
||||
double m_noise = 400; // normalized by 10000
|
||||
double m_noise_delta = 0.05;
|
||||
|
||||
// for tuning
|
||||
int s_id = 0; // strategy id
|
||||
|
|
|
|||
|
|
@ -113,6 +113,9 @@ namespace sat {
|
|||
config m_config;
|
||||
double m_delta_trigger;
|
||||
|
||||
drat m_drat;
|
||||
literal_vector m_assumptions;
|
||||
|
||||
literal_vector m_trail; // trail of units
|
||||
unsigned_vector m_trail_lim;
|
||||
vector<literal_vector> m_binary; // literal: binary clauses
|
||||
|
|
@ -229,6 +232,7 @@ namespace sat {
|
|||
m_binary[(~l2).index()].push_back(l1);
|
||||
m_binary_trail.push_back((~l1).index());
|
||||
++m_stats.m_add_binary;
|
||||
if (s.m_config.m_drat) validate_binary(l1, l2);
|
||||
}
|
||||
|
||||
void del_binary(unsigned idx) {
|
||||
|
|
@ -240,6 +244,17 @@ namespace sat {
|
|||
++m_stats.m_del_binary;
|
||||
}
|
||||
|
||||
|
||||
void validate_binary(literal l1, literal l2) {
|
||||
if (m_search_mode == lookahead_mode::searching) {
|
||||
m_assumptions.push_back(l1);
|
||||
m_assumptions.push_back(l2);
|
||||
m_drat.add(m_assumptions);
|
||||
m_assumptions.pop_back();
|
||||
m_assumptions.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
// -------------------------------------
|
||||
// track consequences of binary clauses
|
||||
// see also 72 - 79 in sat11.w
|
||||
|
|
@ -1034,14 +1049,18 @@ namespace sat {
|
|||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
m_full_watches[(~c[i]).index()].push_back(c1);
|
||||
}
|
||||
if (s.m_config.m_drat) m_drat.add(c, false);
|
||||
}
|
||||
|
||||
// copy units
|
||||
unsigned trail_sz = s.init_trail_size();
|
||||
for (unsigned i = 0; i < trail_sz; ++i) {
|
||||
literal l = s.m_trail[i];
|
||||
if (s.m_config.m_drat) m_drat.add(l, false);
|
||||
assign(l);
|
||||
}
|
||||
propagate();
|
||||
m_qhead = m_trail.size();
|
||||
TRACE("sat", s.display(tout); display(tout););
|
||||
}
|
||||
|
||||
|
|
@ -1056,11 +1075,13 @@ namespace sat {
|
|||
m_retired_ternary_lim.push_back(m_retired_ternary.size());
|
||||
m_qhead_lim.push_back(m_qhead);
|
||||
scoped_level _sl(*this, level);
|
||||
m_assumptions.push_back(~lit);
|
||||
assign(lit);
|
||||
propagate();
|
||||
}
|
||||
|
||||
void pop() {
|
||||
m_assumptions.pop_back();
|
||||
m_inconsistent = false;
|
||||
SASSERT(m_search_mode == lookahead_mode::searching);
|
||||
|
||||
|
|
@ -1319,7 +1340,7 @@ namespace sat {
|
|||
for (; m_qhead < m_trail.size(); ++m_qhead) {
|
||||
if (inconsistent()) break;
|
||||
literal l = m_trail[m_qhead];
|
||||
TRACE("sat", tout << "propagate " << l << "\n";);
|
||||
TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
|
||||
propagate_binary(l);
|
||||
propagate_clauses(l);
|
||||
}
|
||||
|
|
@ -1360,7 +1381,7 @@ namespace sat {
|
|||
TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";);
|
||||
reset_wnb(lit);
|
||||
push_lookahead1(lit, level);
|
||||
//do_double(lit, base);
|
||||
do_double(lit, base);
|
||||
bool unsat = inconsistent();
|
||||
pop_lookahead1(lit);
|
||||
if (unsat) {
|
||||
|
|
@ -1386,12 +1407,14 @@ namespace sat {
|
|||
}
|
||||
|
||||
void init_wnb() {
|
||||
TRACE("sat", tout << "init_wnb: " << m_qhead << "\n";);
|
||||
m_qhead_lim.push_back(m_qhead);
|
||||
m_trail_lim.push_back(m_trail.size());
|
||||
}
|
||||
|
||||
void reset_wnb() {
|
||||
m_qhead = m_qhead_lim.back();
|
||||
TRACE("sat", tout << "reset_wnb: " << m_qhead << "\n";);
|
||||
unsigned old_sz = m_trail_lim.back();
|
||||
for (unsigned i = old_sz; i < m_trail.size(); ++i) {
|
||||
set_undef(m_trail[i]);
|
||||
|
|
@ -1541,14 +1564,15 @@ namespace sat {
|
|||
SASSERT(dl_no_overflow(base));
|
||||
unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1);
|
||||
scoped_level _sl(*this, dl_truth);
|
||||
init_wnb();
|
||||
assign(l);
|
||||
propagate();
|
||||
bool change = true;
|
||||
unsigned num_iterations = 0;
|
||||
init_wnb();
|
||||
while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) {
|
||||
change = false;
|
||||
num_iterations++;
|
||||
base += 2*m_lookahead.size();
|
||||
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
|
||||
literal lit = m_lookahead[i].m_lit;
|
||||
if (is_fixed_at(lit, dl_truth)) continue;
|
||||
|
|
@ -1564,7 +1588,6 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
SASSERT(dl_truth - 2 * m_lookahead.size() > base);
|
||||
base += 2*m_lookahead.size();
|
||||
}
|
||||
reset_wnb();
|
||||
SASSERT(m_level == dl_truth);
|
||||
|
|
@ -1576,6 +1599,14 @@ namespace sat {
|
|||
|
||||
unsigned scope_lvl() const { return m_trail_lim.size(); }
|
||||
|
||||
void validate_assign(literal l) {
|
||||
if (s.m_config.m_drat && m_search_mode == lookahead_mode::searching) {
|
||||
m_assumptions.push_back(l);
|
||||
m_drat.add(m_assumptions);
|
||||
m_assumptions.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
void assign(literal l) {
|
||||
SASSERT(m_level > 0);
|
||||
if (is_undef(l)) {
|
||||
|
|
@ -1586,11 +1617,13 @@ namespace sat {
|
|||
m_stats.m_propagations++;
|
||||
TRACE("sat", tout << "removing free var v" << l.var() << "\n";);
|
||||
m_freevars.remove(l.var());
|
||||
validate_assign(l);
|
||||
}
|
||||
}
|
||||
else if (is_false(l)) {
|
||||
TRACE("sat", tout << "conflict: " << l << " @ " << m_level << " " << m_search_mode << "\n";);
|
||||
SASSERT(!is_true(l));
|
||||
validate_assign(l);
|
||||
set_conflict();
|
||||
}
|
||||
}
|
||||
|
|
@ -1709,6 +1742,7 @@ namespace sat {
|
|||
public:
|
||||
lookahead(solver& s) :
|
||||
s(s),
|
||||
m_drat(s),
|
||||
m_level(2),
|
||||
m_prefix(0) {
|
||||
m_search_mode = lookahead_mode::searching;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue