mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-09-19 08:31:56 -07:00
commit d03e3765b9
8 changed files with 214 additions and 91 deletions
Download patch file Download diff file Expand all files Collapse all files

55
src/sat/ba_solver.cpp
View file

@ -1820,6 +1820,10 @@ namespace sat {
} }
} }
++j;
if (j < p.num_watch()) {
j = p.num_watch();
}
CTRACE("sat", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); CTRACE("sat", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true););
if (_debug_conflict) { if (_debug_conflict) {
@ -1845,6 +1849,25 @@ namespace sat {
SASSERT(validate_unit_propagation(p, r, l)); SASSERT(validate_unit_propagation(p, r, l));
} }
bool ba_solver::is_extended_binary(ext_justification_idx idx, literal_vector & r) {
constraint const& c = index2constraint(idx);
switch (c.tag()) {
case card_t: {
card const& ca = c.to_card();
if (ca.size() == ca.k() + 1 && ca.lit() == null_literal) {
r.reset();
for (literal l : ca) r.push_back(l);
return true;
}
else {
return false;
}
}
default:
return false;
}
}
void ba_solver::simplify(xor& x) { void ba_solver::simplify(xor& x) {
// no-op // no-op
} }
@ -2110,18 +2133,40 @@ namespace sat {
/** /**
\brief Lex on (glue, size) \brief Lex on (glue, size)
*/ */
struct constraint_glue_lt { struct constraint_glue_psm_lt {
bool operator()(ba_solver::constraint const * c1, ba_solver::constraint const * c2) const { bool operator()(ba_solver::constraint const * c1, ba_solver::constraint const * c2) const {
return return
(c1->glue() < c2->glue()) || (c1->glue() < c2->glue()) ||
(c1->glue() == c2->glue() && c1->size() < c2->size()); (c1->glue() == c2->glue() &&
(c1->psm() < c2->psm() ||
(c1->psm() == c2->psm() && c1->size() < c2->size())));
} }
}; };
void ba_solver::update_psm(constraint& c) const {
unsigned r = 0;
switch (c.tag()) {
case card_t:
for (literal l : c.to_card()) {
if (s().m_phase[l.var()] == (l.sign() ? NEG_PHASE : POS_PHASE)) ++r;
}
break;
case pb_t:
for (wliteral l : c.to_pb()) {
if (s().m_phase[l.second.var()] == (l.second.sign() ? NEG_PHASE : POS_PHASE)) ++r;
}
break;
default:
break;
}
c.set_psm(r);
}
void ba_solver::gc() { void ba_solver::gc() {
if (m_learned.size() >= 2 * m_constraints.size()) { if (m_learned.size() >= 2 * m_constraints.size()) {
std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_lt()); for (auto & c : m_learned) update_psm(*c);
gc_half("glue"); std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_psm_lt());
gc_half("glue-psm");
cleanup_constraints(m_learned, true); cleanup_constraints(m_learned, true);
} }
} }
@ -3056,7 +3101,7 @@ namespace sat {
} }
for (wliteral l : p1) { for (wliteral l : p1) {
SASSERT(m_weights[l.second.index()] == 0); SASSERT(m_weights[l.second.index()] == 0);
m_weights[l.second.index()] = l.first; m_weights.setx(l.second.index(), l.first, 0);
mark_visited(l.second); mark_visited(l.second);
} }
for (unsigned i = 0; i < p1.num_watch(); ++i) { for (unsigned i = 0; i < p1.num_watch(); ++i) {

7
src/sat/ba_solver.h
View file

@ -64,12 +64,13 @@ namespace sat {
bool m_removed; bool m_removed;
literal m_lit; literal m_lit;
unsigned m_glue; unsigned m_glue;
unsigned m_psm;
unsigned m_size; unsigned m_size;
size_t m_obj_size; size_t m_obj_size;
bool m_learned; bool m_learned;
unsigned m_id; unsigned m_id;
public: public:
constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz): m_tag(t), m_removed(false), m_lit(l), m_glue(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {} constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz): m_tag(t), m_removed(false), m_lit(l), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); } ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
unsigned id() const { return m_id; } unsigned id() const { return m_id; }
tag_t tag() const { return m_tag; } tag_t tag() const { return m_tag; }
@ -82,6 +83,8 @@ namespace sat {
void nullify_literal() { m_lit = null_literal; } void nullify_literal() { m_lit = null_literal; }
unsigned glue() const { return m_glue; } unsigned glue() const { return m_glue; }
void set_glue(unsigned g) { m_glue = g; } void set_glue(unsigned g) { m_glue = g; }
unsigned psm() const { return m_psm; }
void set_psm(unsigned p) { m_psm = p; }
void set_learned(bool f) { m_learned = f; } void set_learned(bool f) { m_learned = f; }
bool learned() const { return m_learned; } bool learned() const { return m_learned; }
@ -269,6 +272,7 @@ namespace sat {
void subsumption(constraint& c1); void subsumption(constraint& c1);
void subsumption(card& c1); void subsumption(card& c1);
void gc_half(char const* _method); void gc_half(char const* _method);
void update_psm(constraint& c) const;
void mutex_reduction(); void mutex_reduction();
typedef vector<std::pair<rational, lp::var_index>> lhs_t; typedef vector<std::pair<rational, lp::var_index>> lhs_t;
@ -446,6 +450,7 @@ namespace sat {
virtual void pop_reinit(); virtual void pop_reinit();
virtual void gc(); virtual void gc();
virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const; virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const;
virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r);
virtual void init_use_list(ext_use_list& ul); virtual void init_use_list(ext_use_list& ul);
virtual bool is_blocked(literal l, ext_constraint_idx idx); virtual bool is_blocked(literal l, ext_constraint_idx idx);

181
src/sat/sat_ccc.cpp
View file

@ -36,39 +36,48 @@ using namespace sat;
// ------------ // ------------
// cuber // cuber
ccc::cuber::cuber(ccc& c): m_ccc(c), lh(c.m_s), m_branch_id(0) {} ccc::cuber::cuber(ccc& c): m_ccc(c), m_lh(alloc(lookahead, c.m_s)), m_branch_id(0) {}
lbool ccc::cuber::search() { lbool ccc::cuber::search() {
m_branch_id = 0; while (true) {
m_last_closure_level = 1000; m_branch_id = 0;
m_last_closure_level = 1000;
lh.init_search(); m_lh->init_search();
lh.m_model.reset(); m_lh->m_model.reset();
lookahead::scoped_level _sl(lh, lh.c_fixed_truth); lookahead::scoped_level _sl(*m_lh.get(), m_lh->c_fixed_truth);
lh.m_search_mode = lookahead_mode::searching; m_lh->m_search_mode = lookahead_mode::searching;
lbool r = research(); lbool r = research();
if (r == l_true) { if (r == l_true) {
m_ccc.m_model = lh.get_model(); m_ccc.m_model = m_lh->get_model();
}
if (false && r == l_undef) {
continue;
}
m_lh->collect_statistics(m_ccc.m_lh_stats);
return r;
} }
lh.collect_statistics(m_ccc.m_lh_stats);
return r;
} }
lbool ccc::cuber::research() { lbool ccc::cuber::research() {
m_ccc.m_s.checkpoint(); m_ccc.m_s.checkpoint();
if (lh.inconsistent()) { if (m_lh->inconsistent()) {
return l_false; return l_false;
} }
if (pop_lookahead()) {
return l_undef;
}
if (get_solved()) { if (get_solved()) {
return l_false; return l_false;
} }
lh.inc_istamp(); m_lh->inc_istamp();
literal l = lh.choose(); literal l = m_lh->choose();
if (lh.inconsistent()) { if (m_lh->inconsistent()) {
return l_false; return l_false;
} }
@ -76,34 +85,35 @@ lbool ccc::cuber::research() {
return l_true; return l_true;
} }
if (!decisions.empty()) { if (!m_decisions.empty()) {
m_ccc.put_decision(decisions.back()); m_ccc.put_decision(m_decisions.back());
} }
// update trail and decisions
++lh.m_stats.m_decisions; // update trail and m_decisions
unsigned parent_id = decisions.empty() ? 0 : decisions.back().m_id;
++m_lh->m_stats.m_decisions;
unsigned parent_id = m_decisions.empty() ? 0 : m_decisions.back().m_id;
unsigned spawn_id = spawn_conquer(); unsigned spawn_id = spawn_conquer();
unsigned branch1 = m_branch_id++; unsigned branch1 = m_branch_id++;
unsigned branch2 = m_branch_id++; unsigned branch2 = m_branch_id++;
decision d(branch1, decisions.size() + 1, l, parent_id, spawn_id); decision d(branch1, m_decisions.size() + 1, l, parent_id, spawn_id);
decisions.push_back(d); m_decisions.push_back(d);
IF_VERBOSE(1, d.pp(verbose_stream() << "select " << m_last_closure_level << " ") << "\n";); IF_VERBOSE(2, d.pp(verbose_stream() << "select " << m_last_closure_level << " ") << "\n";);
IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";); IF_VERBOSE(2, verbose_stream() << "select " << pp_prefix(m_lh->m_prefix, m_lh->m_trail_lim.size()) << ": " << l << " " << m_lh->m_trail.size() << "\n";);
IF_VERBOSE(2, pp(verbose_stream(), decisions) << "\n"; ); IF_VERBOSE(3, pp(verbose_stream(), m_decisions) << "\n"; );
TRACE("sat", tout << "choose: " << l << "\n";); TRACE("sat", tout << "choose: " << l << "\n";);
lh.push(l, lh.c_fixed_truth); m_lh->push(l, m_lh->c_fixed_truth);
lbool r = research(); lbool r = research();
if (r == l_false) { if (r == l_false) {
lh.pop(); m_lh->pop();
if (decisions.back().is_closed()) { if (m_decisions.back().is_closed()) {
// branch was solved by a spawned conquer process // branch was solved by a spawned conquer process
IF_VERBOSE(1, decisions.back().pp(verbose_stream() << "closed ") << "\n";); IF_VERBOSE(1, m_decisions.back().pp(verbose_stream() << "closed ") << "\n";);
r = l_false; r = l_false;
decisions.pop_back(); m_decisions.pop_back();
} }
else { else {
if (spawn_id > 0) { if (spawn_id > 0) {
@ -111,22 +121,41 @@ lbool ccc::cuber::research() {
m_last_closure_level *= 3; m_last_closure_level *= 3;
m_last_closure_level /= 4; m_last_closure_level /= 4;
} }
lh.inc_istamp(); m_lh->inc_istamp();
lh.flip_prefix(); m_lh->flip_prefix();
lh.push(~l, lh.c_fixed_truth); m_lh->push(~l, m_lh->c_fixed_truth);
decisions.back().negate(); m_decisions.back().negate();
decisions.back().m_id = branch2; m_decisions.back().m_id = branch2;
decisions.back().m_spawn_id = 0; m_decisions.back().m_spawn_id = 0;
r = research(); r = research();
if (r == l_false) { if (r == l_false) {
lh.pop(); m_lh->pop();
decisions.pop_back(); m_decisions.pop_back();
} }
} }
} }
return r; return r;
} }
bool ccc::cuber::pop_lookahead() {
return false;
scoped_ptr<lookahead> new_lh;
bool result = false;
#pragma omp critical (ccc_new_lh)
{
if (m_ccc.m_new_lh) {
new_lh = m_ccc.m_new_lh.detach();
result = true;
}
}
if (new_lh) {
m_lh->collect_statistics(m_ccc.m_lh_stats);
m_lh = new_lh.detach();
}
return result;
}
void ccc::cuber::update_closure_level(decision const& d, int offset) { void ccc::cuber::update_closure_level(decision const& d, int offset) {
m_last_closure_level = (d.m_depth + 3*m_last_closure_level) / 4; m_last_closure_level = (d.m_depth + 3*m_last_closure_level) / 4;
if (m_last_closure_level >= static_cast<unsigned>(abs(offset))) { if (m_last_closure_level >= static_cast<unsigned>(abs(offset))) {
@ -140,13 +169,13 @@ unsigned ccc::cuber::spawn_conquer() {
// decisions must have been solved at a higher level by a conquer thread // decisions must have been solved at a higher level by a conquer thread
// //
if (!m_free_threads.empty()) { if (!m_free_threads.empty()) {
if (m_last_closure_level <= decisions.size()) { if (m_last_closure_level <= m_decisions.size()) {
result = m_free_threads.back(); result = m_free_threads.back();
++m_ccc.m_ccc_stats.m_spawn_opened; ++m_ccc.m_ccc_stats.m_spawn_opened;
m_free_threads.pop_back(); m_free_threads.pop_back();
} }
else { else {
IF_VERBOSE(1, verbose_stream() << m_last_closure_level << " " << decisions.size() << "\n";); IF_VERBOSE(1, verbose_stream() << m_last_closure_level << " " << m_decisions.size() << "\n";);
} }
} }
return result; return result;
@ -181,13 +210,13 @@ bool ccc::cuber::get_solved() {
unsigned branch_id = sol.m_branch_id; unsigned branch_id = sol.m_branch_id;
unsigned thread_id = sol.m_thread_id; unsigned thread_id = sol.m_thread_id;
bool found = false; bool found = false;
for (unsigned i = decisions.size(); i > 0; ) { for (unsigned i = m_decisions.size(); i > 0; ) {
--i; --i;
decision& d = decisions[i]; decision& d = m_decisions[i];
if (branch_id == d.m_id) { if (branch_id == d.m_id) {
if (d.m_spawn_id == thread_id && thread_id != 0) { if (d.m_spawn_id == thread_id && thread_id != 0) {
SASSERT(d.m_spawn_id > 0); SASSERT(d.m_spawn_id > 0);
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": spawn close ") << "\n";); IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": spawn close ") << "\n";);
++m_ccc.m_ccc_stats.m_spawn_closed; ++m_ccc.m_ccc_stats.m_spawn_closed;
d.close(); d.close();
free_conquer(thread_id); free_conquer(thread_id);
@ -195,7 +224,7 @@ bool ccc::cuber::get_solved() {
break; break;
} }
else { else {
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": conquer ") << "\n";); IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": conquer ") << "\n";);
++m_ccc.m_ccc_stats.m_cdcl_closed; ++m_ccc.m_ccc_stats.m_cdcl_closed;
update_closure_level(d, 1); update_closure_level(d, 1);
return true; return true;
@ -236,6 +265,7 @@ lbool ccc::conquer::search() {
s.simplify_problem(); s.simplify_problem();
if (s.check_inconsistent()) return l_false; if (s.check_inconsistent()) return l_false;
s.gc(); s.gc();
push_lookahead();
} }
} }
catch (solver::abort_solver) { catch (solver::abort_solver) {
@ -245,16 +275,16 @@ lbool ccc::conquer::search() {
void ccc::conquer::replay_decisions() { void ccc::conquer::replay_decisions() {
s.propagate(true); s.propagate(true);
for (unsigned i = s.scope_lvl(); !s.inconsistent() && i < decisions.size(); ++i) { for (unsigned i = s.scope_lvl(); !s.inconsistent() && i < m_decisions.size(); ++i) {
decision const& d = decisions[i]; decision const& d = m_decisions[i];
IF_VERBOSE(2, verbose_stream() << thread_id << ": replay " << d.get_literal(thread_id) << " " << s.value(d.get_literal(thread_id)) << "\n";); IF_VERBOSE(2, verbose_stream() << thread_id << ": replay " << d.get_literal(thread_id) << " " << s.value(d.get_literal(thread_id)) << "\n";);
if (!push_decision(d)) { if (!push_decision(d)) {
// negation of decision is implied. // negation of decision is implied.
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": backjump to level " << i << " ") << "\n";); IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": backjump to level " << i << " ") << "\n";);
while (decisions.size() > i) { while (m_decisions.size() > i) {
pop_decision(decisions.back()); pop_decision(m_decisions.back());
decisions.pop_back(); m_decisions.pop_back();
} }
break; break;
} }
@ -280,6 +310,19 @@ void ccc::conquer::pop_decision(decision const& d) {
} }
} }
void ccc::conquer::push_lookahead() {
return;
#pragma omp critical (ccc_new_lh)
{
if (!m_ccc.m_new_lh && m_ccc.m_num_clauses > s.num_clauses()) {
std::cout << "push " << s.num_clauses() << "\n";
m_ccc.m_new_lh = alloc(lookahead, s);
m_ccc.m_num_clauses = s.num_clauses();
}
}
}
bool ccc::conquer::push_decision(decision const& d) { bool ccc::conquer::push_decision(decision const& d) {
literal lit = d.get_literal(thread_id); literal lit = d.get_literal(thread_id);
switch (s.value(lit)) { switch (s.value(lit)) {
@ -313,7 +356,7 @@ bool ccc::conquer::cube_decision() {
if (d.is_spawned(thread_id)) IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << " ") << "\n";); if (d.is_spawned(thread_id)) IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << " ") << "\n";);
if (!decisions.empty() && decisions.back().m_depth + 1 < d.m_depth) { if (!m_decisions.empty() && m_decisions.back().m_depth + 1 < d.m_depth) {
if (d.is_spawned(thread_id)) { if (d.is_spawned(thread_id)) {
pop_decision(d); pop_decision(d);
} }
@ -322,43 +365,43 @@ bool ccc::conquer::cube_decision() {
break; break;
} }
} }
SASSERT(decisions.empty() || decisions.back().m_depth + 1 >= d.m_depth); SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 >= d.m_depth);
if (!decisions.empty() && decisions.back().is_spawned(thread_id) && decisions.back().m_depth == d.m_depth) { if (!m_decisions.empty() && m_decisions.back().is_spawned(thread_id) && m_decisions.back().m_depth == d.m_depth) {
SASSERT(d.m_spawn_id == 0); SASSERT(d.m_spawn_id == 0);
SASSERT(decisions.back().is_left()); SASSERT(m_decisions.back().is_left());
SASSERT(!d.is_left()); SASSERT(!d.is_left());
IF_VERBOSE(1, verbose_stream() << thread_id << " inherit spawn\n";); IF_VERBOSE(1, verbose_stream() << thread_id << " inherit spawn\n";);
decisions.back().m_spawn_id = 0; m_decisions.back().m_spawn_id = 0;
m_spawned = false; m_spawned = false;
} }
SASSERT(decisions.empty() || decisions.back().m_depth + 1 >= d.m_depth); SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 >= d.m_depth);
while (!decisions.empty() && decisions.back().m_depth >= d.m_depth) { while (!m_decisions.empty() && m_decisions.back().m_depth >= d.m_depth) {
// check_non_model("cube decision", decisions); // check_non_model("cube decision", m_decisions);
if (decisions.back().is_spawned(thread_id)) { if (m_decisions.back().is_spawned(thread_id)) {
pop_decision(decisions.back()); pop_decision(m_decisions.back());
} }
decisions.pop_back(); m_decisions.pop_back();
} }
SASSERT(decisions.empty() || decisions.back().m_depth + 1 == d.m_depth); SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 == d.m_depth);
SASSERT(decisions.empty() || decisions.back().m_id == d.m_parent); SASSERT(m_decisions.empty() || m_decisions.back().m_id == d.m_parent);
if (m_spawned) { if (m_spawned) {
decisions.push_back(d); m_decisions.push_back(d);
return true; return true;
} }
s.pop_reinit(s.scope_lvl() - decisions.size()); s.pop_reinit(s.scope_lvl() - m_decisions.size());
SASSERT(s.m_qhead == s.m_trail.size()); SASSERT(s.m_qhead == s.m_trail.size());
SASSERT(s.scope_lvl() == decisions.size()); SASSERT(s.scope_lvl() == m_decisions.size());
literal lit = d.get_literal(thread_id); literal lit = d.get_literal(thread_id);
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": cube ") << "\n";); IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": cube ") << "\n";);
IF_VERBOSE(2, pp(verbose_stream() << thread_id << ": push ", decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n"; IF_VERBOSE(3, pp(verbose_stream() << thread_id << ": push ", m_decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n";
if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";); if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";);
if (push_decision(d)) { if (push_decision(d)) {
decisions.push_back(d); m_decisions.push_back(d);
} }
else { else {
pop_decision(d); pop_decision(d);

20
src/sat/sat_ccc.h
View file

@ -74,7 +74,7 @@ namespace sat {
reslimit m_limit; reslimit m_limit;
ccc& m_ccc; ccc& m_ccc;
solver s; solver s;
svector<decision> decisions; svector<decision> m_decisions;
unsigned thread_id; unsigned thread_id;
bool m_spawned; bool m_spawned;
conquer(ccc& super, params_ref const& p, unsigned tid): m_ccc(super), s(p, m_limit), thread_id(tid), m_spawned(false) {} conquer(ccc& super, params_ref const& p, unsigned tid): m_ccc(super), s(p, m_limit), thread_id(tid), m_spawned(false) {}
@ -84,16 +84,17 @@ namespace sat {
lbool bounded_search(); lbool bounded_search();
bool push_decision(decision const& d); bool push_decision(decision const& d);
void pop_decision(decision const& d); void pop_decision(decision const& d);
void push_lookahead();
void replay_decisions(); void replay_decisions();
}; };
struct cuber { struct cuber {
ccc& m_ccc; ccc& m_ccc;
lookahead lh; scoped_ptr<lookahead> m_lh;
unsigned m_branch_id; unsigned m_branch_id;
unsigned m_last_closure_level; unsigned m_last_closure_level;
unsigned_vector m_free_threads; unsigned_vector m_free_threads;
svector<decision> decisions; svector<decision> m_decisions;
cuber(ccc& c); cuber(ccc& c);
lbool search(); lbool search();
@ -102,11 +103,14 @@ namespace sat {
void update_closure_level(decision const& d, int offset); void update_closure_level(decision const& d, int offset);
unsigned spawn_conquer(); unsigned spawn_conquer();
void free_conquer(unsigned thread_id); void free_conquer(unsigned thread_id);
bool pop_lookahead();
}; };
solver& m_s; solver& m_s;
queue<solution> m_solved; queue<solution> m_solved;
vector<queue<decision> > m_decisions; vector<queue<decision> > m_decisions;
scoped_ptr<lookahead> m_new_lh;
unsigned m_num_clauses;
unsigned m_num_conquer; unsigned m_num_conquer;
model m_model; model m_model;
volatile bool m_cancel; volatile bool m_cancel;
@ -127,7 +131,7 @@ namespace sat {
public: public:
ccc(solver& s): m_s(s) {} ccc(solver& s): m_s(s), m_num_clauses(s.num_clauses()) {}
lbool search(); lbool search();

1
src/sat/sat_extension.h
View file

@ -55,6 +55,7 @@ namespace sat {
virtual bool propagate(literal l, ext_constraint_idx idx) = 0; virtual bool propagate(literal l, ext_constraint_idx idx) = 0;
virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0; virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0;
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0; virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) = 0;
virtual void asserted(literal l) = 0; virtual void asserted(literal l) = 0;
virtual check_result check() = 0; virtual check_result check() = 0;
virtual lbool resolve_conflict() { return l_undef; } // stores result in sat::solver::m_lemma virtual lbool resolve_conflict() { return l_undef; } // stores result in sat::solver::m_lemma

22
src/sat/sat_lookahead.cpp
View file

@ -503,6 +503,7 @@ namespace sat {
// arcs are added in the opposite direction of implications. // arcs are added in the opposite direction of implications.
// So for implications l => u we add arcs u -> l // So for implications l => u we add arcs u -> l
void lookahead::init_arcs(literal l) { void lookahead::init_arcs(literal l) {
literal_vector lits;
literal_vector const& succ = m_binary[l.index()]; literal_vector const& succ = m_binary[l.index()];
for (unsigned i = 0; i < succ.size(); ++i) { for (unsigned i = 0; i < succ.size(); ++i) {
literal u = succ[i]; literal u = succ[i];
@ -512,6 +513,16 @@ namespace sat {
add_arc( u, l); add_arc( u, l);
} }
} }
for (auto w : m_watches[l.index()]) {
if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) {
for (literal u : lits) {
if (u.index() > l.index() && is_stamped(u)) {
add_arc(~l, ~u);
add_arc( u, l);
}
}
}
}
} }
void lookahead::get_scc(literal v) { void lookahead::get_scc(literal v) {
@ -852,7 +863,7 @@ namespace sat {
copy_clauses(m_s.m_clauses); copy_clauses(m_s.m_clauses);
copy_clauses(m_s.m_learned); copy_clauses(m_s.m_learned);
m_config.m_use_ternary_reward &= !m_s.m_ext; // m_config.m_use_ternary_reward &= !m_s.m_ext;
// copy units // copy units
unsigned trail_sz = m_s.init_trail_size(); unsigned trail_sz = m_s.init_trail_size();
@ -887,7 +898,7 @@ namespace sat {
if (c.was_removed()) continue; if (c.was_removed()) continue;
// enable when there is a non-ternary reward system. // enable when there is a non-ternary reward system.
if (c.size() > 3) { if (c.size() > 3) {
m_config.m_use_ternary_reward = false; // m_config.m_use_ternary_reward = false;
} }
bool was_eliminated = false; bool was_eliminated = false;
for (unsigned i = 0; !was_eliminated && i < c.size(); ++i) { for (unsigned i = 0; !was_eliminated && i < c.size(); ++i) {
@ -1245,7 +1256,12 @@ namespace sat {
double lookahead::literal_occs(literal l) { double lookahead::literal_occs(literal l) {
double result = m_binary[l.index()].size(); double result = m_binary[l.index()].size();
for (clause const* c : m_full_watches[l.index()]) { for (clause const* c : m_full_watches[l.index()]) {
if (!is_true((*c)[0]) && !is_true((*c)[1])) { bool has_true = false;
for (literal l : *c) {
has_true = is_true(l);
if (has_true) break;
}
if (!has_true) {
result += 1.0 / c->size(); result += 1.0 / c->size();
} }
} }

6
src/sat/sat_scc.cpp
View file

@ -33,10 +33,11 @@ namespace sat {
struct frame { struct frame {
unsigned m_lidx; unsigned m_lidx;
unsigned m_succ_idx;
bool m_first; bool m_first;
watched * m_it; watched * m_it;
watched * m_end; watched * m_end;
frame(unsigned lidx, watched * it, watched * end):m_lidx(lidx), m_first(true), m_it(it), m_end(end) {} frame(unsigned lidx, watched * it, watched * end, unsigned sidx = 0):m_lidx(lidx), m_succ_idx(sidx), m_first(true), m_it(it), m_end(end) {}
}; };
typedef svector<frame> frames; typedef svector<frame> frames;
@ -75,7 +76,7 @@ namespace sat {
index.resize(num_lits, UINT_MAX); index.resize(num_lits, UINT_MAX);
lowlink.resize(num_lits, UINT_MAX); lowlink.resize(num_lits, UINT_MAX);
in_s.resize(num_lits, false); in_s.resize(num_lits, false);
literal_vector roots; literal_vector roots, lits;
roots.resize(m_solver.num_vars(), null_literal); roots.resize(m_solver.num_vars(), null_literal);
unsigned next_index = 0; unsigned next_index = 0;
svector<frame> frames; svector<frame> frames;
@ -106,6 +107,7 @@ namespace sat {
frame & fr = frames.back(); frame & fr = frames.back();
unsigned l_idx = fr.m_lidx; unsigned l_idx = fr.m_lidx;
if (!fr.m_first) { if (!fr.m_first) {
SASSERT(fr.m_it->is_binary_clause());
// after visiting child // after visiting child
literal l2 = fr.m_it->get_literal(); literal l2 = fr.m_it->get_literal();
unsigned l2_idx = l2.index(); unsigned l2_idx = l2.index();

7
src/sat/sat_solver.cpp
View file

@ -913,6 +913,13 @@ namespace sat {
if (check_inconsistent()) return l_false; if (check_inconsistent()) return l_false;
gc(); gc();
#if 0
if (m_clauses.size() < 65000) {
return do_ccc();
return lookahead_search();
}
#endif
if (m_config.m_restart_max <= m_restarts) { if (m_config.m_restart_max <= m_restarts) {
m_reason_unknown = "sat.max.restarts"; m_reason_unknown = "sat.max.restarts";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);