3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 05:37:00 +00:00

testing lookahead

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-12 11:49:07 -08:00
parent 690689424d
commit 42deeb3498
13 changed files with 456 additions and 15 deletions

394
src/sat/sat_lookahead.h Normal file
View file

@ -0,0 +1,394 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
sat_lookahead.h
Abstract:
Lookahead SAT solver in the style of March.
Author:
Nikolaj Bjorner (nbjorner) 2017-2-11
Notes:
--*/
#ifndef _SAT_LOOKAHEAD_H_
#define _SAT_LOOKAHEAD_H_
namespace sat {
class lookahead {
solver& s;
struct config {
double m_dl_success;
};
config m_config;
double m_delta_trigger;
literal_vector m_trail;
literal_vector m_units;
unsigned_vector m_units_lim;
unsigned_vector m_learned_lim;
void init() {
m_delta_trigger = s.num_vars()/10;
m_config.m_dl_success = 0.8;
}
void push(literal lit) {
m_learned_lim.push_back(s.m_learned.size());
m_units_lim.push_back(m_units.size());
m_trail.push_back(lit);
s.push();
assign(lit);
}
void pop() {
s.pop(1);
unsigned old_sz = m_learned_lim.back();
m_learned_lim.pop_back();
for (unsigned i = old_sz; i < s.m_learned.size(); ++i) {
clause* r = s.m_learned[i];
s.dettach_clause(*r);
s.m_cls_allocator.del_clause(r);
}
s.m_learned.shrink(old_sz);
literal lits[2] = { m_trail.back(), null_literal };
unsigned new_unit_sz = m_units_lim.back();
for (unsigned i = m_units.size(); i > new_unit_sz; ) {
--i;
lits[1] = m_units[i];
clause * r = s.m_cls_allocator.mk_clause(2, lits, true);
s.m_learned.push_back(r);
}
m_units.shrink(new_unit_sz);
m_units_lim.pop_back();
m_trail.pop_back();
}
unsigned diff(unsigned value0) const {
unsigned value1 = get_state_value();
SASSERT(value1 >= value0);
return value1 - value0;
}
unsigned mix_diff(unsigned l, unsigned r) const {
return l + r + (1 << 10) * l * r;
}
void get_resolvent_units(literal lit) {
if (inconsistent()) return;
for (unsigned i = s.m_trail.size(); i > 0; ) {
--i;
literal l = s.m_trail[i];
if (l == lit) break;
SASSERT(s.lvl(l) == s.scope_lvl());
watch_list& wlist = s.m_watches[(~l).index()];
watch_list::iterator it = wlist.begin(), end = wlist.end();
for (; it != end; ++it) {
switch (it->get_kind()) {
case watched::TERNARY:
if (s.value(it->get_literal1()) == l_false &&
s.value(it->get_literal()) == l_false) {
m_units.push_back(l);
goto done_watch_list;
}
break;
case watched::CLAUSE: {
clause_offset cls_off = it->get_clause_offset();
clause & c = *(s.m_cls_allocator.get_clause(cls_off));
if (c.size() == 2) break;
SASSERT(c.size() > 2);
if (c[0] == l && s.value(c[1]) == l_false) {
DEBUG_CODE(for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
m_units.push_back(l);
goto done_watch_list;
}
if (c[1] == l && s.value(c[0]) == l_false) {
DEBUG_CODE(for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
m_units.push_back(l);
goto done_watch_list;
}
break;
}
default:
break;
}
}
done_watch_list:
continue;
}
}
literal choose() {
literal l;
while (!choose1(l)) {};
return l;
}
unsigned get_state_value() const {
return s.m_learned.size();
}
bool choose1(literal& l) {
literal_vector P;
pre_select(P);
l = null_literal;
if (P.empty()) {
return true;
}
unsigned value0 = get_state_value();
unsigned h = 0, count = 1;
literal_vector& units = m_units;;
for (unsigned i = 0; i < P.size(); ++i) {
literal lit = P[i];
push(lit);
if (do_double(value0)) double_look();
if (inconsistent()) {
pop();
assign(~lit);
if (do_double(value0)) double_look();
if (inconsistent()) return true;
continue;
}
unsigned diff1 = diff(value0);
pop();
push(~lit);
if (do_double(value0)) double_look();
bool unsat2 = inconsistent();
unsigned diff2 = diff(value0);
pop();
if (unsat2) {
assign(lit);
continue;
}
unsigned mixd = mix_diff(diff1, diff2);
if (mixd > h || (mixd == h && s.m_rand(count) == 0)) {
h = mixd;
l = diff1 < diff2 ? lit : ~lit;
++count;
}
}
return l != null_literal;
}
void double_look() {
literal_vector P;
pre_select(P);
for (unsigned i = 0; !inconsistent() && i < P.size(); ++i) {
literal lit = P[i];
push(lit);
bool unsat = inconsistent();
pop();
if (unsat) {
assign(~lit);
continue;
}
push(~lit);
unsat = inconsistent();
pop();
if (unsat) {
assign(lit);
}
}
update_delta_trigger();
}
void assign(literal l) {
s.assign(l, justification());
s.propagate(false);
get_resolvent_units(l);
}
bool inconsistent() { return s.inconsistent(); }
void pre_select(literal_vector& P) {
select_variables(P);
order_by_implication_trees(P);
}
void order_by_implication_trees(literal_vector& P) {
literal_set roots;
literal_vector nodes, parent;
//
// Extract binary clauses in watch list.
// Produce implication graph between literals in P.
//
for (unsigned i = 0; i < P.size(); ++i) {
literal lit1 = P[i], lit2;
//
// lit2 => lit1, where lit2 is a root.
// make lit1 a root instead of lit2
//
watch_list& wlist = s.m_watches[(~lit1).index()];
watch_list::iterator it = wlist.begin(), end = wlist.end();
lit2 = null_literal;
for (; it != end; ++it) {
switch (it->get_kind()) {
case watched::BINARY:
lit2 = it->get_literal();
break;
case watched::CLAUSE: {
clause_offset cls_off = it->get_clause_offset();
clause & c = *(s.m_cls_allocator.get_clause(cls_off));
if (c.size() == 2) {
if (c[0] == ~lit1) {
lit2 = c[1];
}
else {
SASSERT(c[1] == ~lit1);
lit2 = c[0];
}
}
break;
}
default:
break;
}
if (lit2 != null_literal && roots.contains(lit2)) {
// lit2 => lit1
// if lit2 is a root, put it under lit2
parent.setx(lit2.index(), lit1, null_literal);
roots.remove(lit2);
roots.insert(lit1);
goto found;
}
}
//
// lit1 => lit2.
// if lit2 is a node, put lit1 above lit2
//
it = s.m_watches[lit1.index()].begin();
end = s.m_watches[lit1.index()].end();
for (; it != end; ++it) {
lit2 = null_literal;
switch (it->get_kind()) {
case watched::BINARY:
lit2 = it->get_literal();
break;
case watched::CLAUSE: {
clause_offset cls_off = it->get_clause_offset();
clause & c = *(s.m_cls_allocator.get_clause(cls_off));
if (c.size() == 2) {
if (c[0] == lit1) {
lit2 = c[1];
}
else {
SASSERT(c[1] == lit1);
lit2 = c[0];
}
}
break;
}
default:
break;
}
if (lit2 != null_literal && nodes.contains(lit2)) {
// lit1 => lit2
parent.setx(lit1.index(), lit2, null_literal);
nodes.insert(lit1);
goto found;
}
}
std::cout << "no parents or children of literal " << lit1 << "\n";
nodes.push_back(lit1);
roots.insert(lit1);
found:
;
}
std::cout << "implication trees\n";
for (unsigned i = 0; i < parent.size(); ++i) {
literal p = parent[i];
if (p != null_literal) {
std::cout << to_literal(i) << " |-> " << p << "\n";
}
}
}
void select_variables(literal_vector& P) {
for (unsigned i = 0; i < s.num_vars(); ++i) {
if (s.value(i) == l_undef) {
P.push_back(literal(i, false));
}
}
}
bool do_double(unsigned value0) {
unsigned value1 = get_state_value();
return !inconsistent() && value1 - value0 > m_delta_trigger;
}
void update_delta_trigger() {
if (inconsistent()) {
m_delta_trigger -= (1 - m_config.m_dl_success) / m_config.m_dl_success;
}
else {
m_delta_trigger += 1;
}
if (m_delta_trigger >= s.num_vars()) {
// reset it.
}
}
lbool search() {
literal_vector trail;
#define BACKTRACK \
if (inconsistent()) { \
if (trail.empty()) return l_false; \
pop(); \
assign(~trail.back()); \
trail.pop_back(); \
continue; \
} \
while (true) {
s.checkpoint();
BACKTRACK;
literal l = choose();
TRACE("sat", tout << l << "\n";);
BACKTRACK;
if (l == null_literal) {
return l_true;
}
push(l);
trail.push_back(l);
}
}
public:
lookahead(solver& s) : s(s) {
init();
}
lbool check() {
return search();
}
};
}
#endif