mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

sls

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-13 01:22:45 -07:00
parent cafb31ff94
commit 999db1e280
6 changed files with 92 additions and 168 deletions
Download patch file Download diff file Expand all files Collapse all files

151
src/sat/sat_mus.cpp
View file

@ -37,7 +37,6 @@ namespace sat {
m_core.append(m_mus);
s.m_core.reset();
s.m_core.append(m_core);
m_model.reset();
}
lbool mus::operator()() {
@ -47,8 +46,7 @@ namespace sat {
reset();
literal_vector& core = m_core;
literal_vector& mus = m_mus;
core.append(s.get_core());
core.append(s.get_core());
while (!core.empty()) {
TRACE("sat",
@ -74,14 +72,9 @@ namespace sat {
case l_true: {
SASSERT(value_at(lit, s.get_model()) == l_false);
mus.push_back(lit);
if (core.empty()) {
break;
if (!core.empty()) {
// mr(); // TBD: measure
}
// sz = core.size();
// measure_mr();
// core.append(mus);
// rmr();
// core.resize(sz);
break;
}
case l_false:
@ -105,141 +98,27 @@ namespace sat {
return l_true;
}
void mus::measure_mr() {
model const& m2 = s.get_model();
if (!m_model.empty()) {
unsigned n = 0;
for (unsigned i = 0; i < m_model.size(); ++i) {
if (m2[i] != m_model[i]) ++n;
}
std::cout << "model diff: " << n << " out of " << m_model.size() << "\n";
}
m_model.reset();
m_model.append(m2);
void mus::mr() {
sls sls(s);
literal_vector tabu;
tabu.append(m_mus);
tabu.append(m_core);
bool reuse_model = false;
for (unsigned i = m_mus.size(); i < tabu.size(); ++i) {
tabu[i] = ~tabu[i];
lbool is_sat = sls(tabu.size(), tabu.c_ptr());
lbool is_sat = sls(tabu.size(), tabu.c_ptr(), reuse_model);
tabu[i] = ~tabu[i];
switch (is_sat) {
case l_true:
//m_mus.push_back(tabu[i]);
//m_core.erase(tabu[i]);
std::cout << "in core " << tabu[i] << "\n";
break;
default:
break;
if (is_sat == l_true) {
m_mus.push_back(tabu[i]);
m_core.erase(tabu[i]);
IF_VERBOSE(2, verbose_stream() << "in core " << tabu[i] << "\n";);
reuse_model = true;
}
else {
IF_VERBOSE(2, verbose_stream() << "NOT in core " << tabu[i] << "\n";);
reuse_model = false;
}
}
}
//
// TBD: eager model rotation allows rotating the same clause
// several times with respect to different models.
//
void mus::rmr() {
return;
#if 0
model& model = s.m_model;
literal lit = m_mus.back();
literal assumption_lit;
SASSERT(value_at(lit, model) == l_false);
// literal is false in current model.
unsigned sz = m_toswap.size();
find_swappable(lit);
unsigned sz1 = m_toswap.size();
for (unsigned i = sz; i < sz1; ++i) {
lit = m_toswap[i];
SASSERT(value_at(lit, model) == l_false);
model[lit.var()] = ~model[lit.var()]; // swap assignment
if (has_single_unsat(assumption_lit) && !m_mus.contains(assumption_lit)) {
m_mus.push_back(assumption_lit);
rmr();
}
model[lit.var()] = ~model[lit.var()]; // swap assignment back
}
m_toswap.resize(sz);
#endif
}
bool mus::has_single_unsat(literal& assumption_lit) {
model const& model = s.get_model();
return false;
}
//
// lit is false in model.
// find clauses where ~lit occurs, and all other literals
// are false in model.
// for each of the probed literals, determine if swapping the
// assignment falsifies a hard clause, if not, add to m_toswap.
//
void mus::find_swappable(literal lit) {
IF_VERBOSE(3, verbose_stream() << "(sat.mus swap " << lit << ")\n";);
unsigned sz = m_toswap.size();
literal lit2, lit3;
model const& model = s.get_model();
SASSERT(value_at(lit, model) == l_false);
watch_list const& wlist = s.get_wlist(lit);
watch_list::const_iterator it = wlist.begin();
watch_list::const_iterator end = wlist.end();
unsigned num_cand = 0;
for (; it != end && num_cand <= 1; ++it) {
switch (it->get_kind()) {
case watched::BINARY:
if (it->is_learned()) {
break;
}
lit2 = it->get_literal();
if (value_at(lit2, model) == l_true) {
break;
}
IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << ") ";);
TRACE("sat", tout << ~lit << " " << lit2 << "\n";);
++num_cand;
break;
case watched::TERNARY:
lit2 = it->get_literal1();
lit3 = it->get_literal2();
if (value_at(lit2, model) == l_true) {
break;
}
if (value_at(lit3, model) == l_true) {
break;
}
IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << " " << lit3 << ") ";);
++num_cand;
break;
case watched::CLAUSE: {
clause_offset cls_off = it->get_clause_offset();
clause& c = *(s.m_cls_allocator.get_clause(cls_off));
if (c.is_learned()) {
break;
}
++num_cand;
IF_VERBOSE(1, verbose_stream() << c << " ";);
TRACE("sat", tout << c << "\n";);
break;
}
case watched::EXT_CONSTRAINT:
TRACE("sat", tout << "external constraint - should avoid rmr\n";);
return;
}
}
if (num_cand > 1) {
m_toswap.resize(sz);
}
else {
IF_VERBOSE(1, verbose_stream() << "wlist size: " << num_cand << " " << m_core.size() << "\n";);
}
}
}

7
src/sat/sat_mus.h
View file

@ -23,8 +23,6 @@ namespace sat {
class mus {
literal_vector m_core;
literal_vector m_mus;
literal_vector m_toswap;
model m_model;
solver& s;
public:
@ -33,10 +31,7 @@ namespace sat {
lbool operator()();
private:
lbool mus2();
void rmr();
void measure_mr();
bool has_single_unsat(literal& assumption_lit);
void find_swappable(literal lit);
void mr();
void reset();
void set_core();
};

79
src/sat/sat_sls.cpp
View file

@ -53,6 +53,7 @@ namespace sat {
sls::sls(solver& s): s(s) {
m_max_tries = 10000;
m_prob_choose_min_var = 43;
m_clause_generation = 0;
}
sls::~sls() {
@ -61,12 +62,13 @@ namespace sat {
}
}
lbool sls::operator()(unsigned sz, literal const* tabu) {
init(sz, tabu);
for (unsigned i = 0; !m_false.empty() && i < m_max_tries; ++i) {
lbool sls::operator()(unsigned sz, literal const* tabu, bool reuse_model) {
init(sz, tabu, reuse_model);
unsigned i;
for (i = 0; !m_false.empty() && i < m_max_tries; ++i) {
flip();
}
IF_VERBOSE(2, verbose_stream() << "tries " << i << "\n";);
if (m_false.empty()) {
SASSERT(s.check_model(m_model));
return l_true;
@ -74,10 +76,18 @@ namespace sat {
return l_undef;
}
void sls::init(unsigned sz, literal const* tabu) {
init_clauses();
init_model(sz, tabu);
init_use();
void sls::init(unsigned sz, literal const* tabu, bool reuse_model) {
bool same_generation = (m_clause_generation == s.m_stats.m_non_learned_generation);
if (!same_generation) {
init_clauses();
init_use();
IF_VERBOSE(0, verbose_stream() << s.m_stats.m_non_learned_generation << " " << m_clause_generation << "\n";);
}
if (!reuse_model) {
init_model();
}
init_tabu(sz, tabu);
m_clause_generation = s.m_stats.m_non_learned_generation;
}
void sls::init_clauses() {
@ -97,22 +107,17 @@ namespace sat {
for (unsigned i = 0; i < bincs.size(); ++i) {
lits[0] = bincs[i].first;
lits[1] = bincs[i].second;
m_clauses.push_back(m_alloc.mk_clause(2, lits, false));
clause* cl = m_alloc.mk_clause(2, lits, false);
m_clauses.push_back(cl);
m_bin_clauses.push_back(cl);
}
}
void sls::init_model(unsigned sz, literal const* tabu) {
void sls::init_model() {
m_num_true.reset();
m_model.reset();
m_model.append(s.get_model());
m_tabu.reset();
m_tabu.resize(s.num_vars(), false);
for (unsigned i = 0; i < sz; ++i) {
m_model[tabu[i].var()] = tabu[i].sign()?l_false:l_true;
SASSERT(value_at(tabu[i], m_model) == l_true);
}
sz = m_clauses.size();
unsigned sz = m_clauses.size();
for (unsigned i = 0; i < sz; ++i) {
clause const& c = *m_clauses[i];
unsigned n = 0;
@ -136,7 +141,32 @@ namespace sat {
if (n == 0) {
m_false.insert(i);
}
}
}
}
void sls::init_tabu(unsigned sz, literal const* tabu) {
// our main use is where m_model satisfies all the hard constraints.
// SASSERT(s.check_model(m_model));
// SASSERT(m_false.empty());
// ASSERT: m_num_true is correct count.
m_tabu.reset();
m_tabu.resize(s.num_vars(), false);
for (unsigned i = 0; i < sz; ++i) {
literal lit = tabu[i];
if (s.m_level[lit.var()] == 0) continue;
if (value_at(lit, m_model) == l_false) {
flip(lit);
}
m_tabu[lit.var()] = true;
}
for (unsigned i = 0; i < s.m_trail.size(); ++i) {
literal lit = s.m_trail[i];
if (s.m_level[lit.var()] > 0) break;
if (value_at(lit, m_model) != l_true) {
flip(lit);
}
m_tabu[lit.var()] = true;
}
}
void sls::init_use() {
@ -191,7 +221,7 @@ namespace sat {
m_min_vars.push_back(lit);
}
}
if (min_break == 0 || (m_min_vars.empty() && m_rand(100) >= m_prob_choose_min_var)) {
if (min_break == 0 || (!m_min_vars.empty() && m_rand(100) >= m_prob_choose_min_var)) {
lit = m_min_vars[m_rand(m_min_vars.size())];
return true;
}
@ -206,8 +236,15 @@ namespace sat {
void sls::flip() {
literal lit;
if (!pick_flip(lit)) return;
if (pick_flip(lit)) {
flip(lit);
}
}
void sls::flip(literal lit) {
// IF_VERBOSE(0, verbose_stream() << lit << " ";);
SASSERT(value_at(lit, m_model) == l_false);
SASSERT(!m_tabu[lit.var()]);
m_model[lit.var()] = lit.sign()?l_false:l_true;
SASSERT(value_at(lit, m_model) == l_true);
unsigned_vector const& use1 = get_use(lit);

9
src/sat/sat_sls.h
View file

@ -42,6 +42,7 @@ namespace sat {
random_gen m_rand;
unsigned m_max_tries;
unsigned m_prob_choose_min_var; // number between 0 and 99.
unsigned m_clause_generation;
ptr_vector<clause const> m_clauses; // vector of all clauses.
index_set m_false; // clauses currently false
vector<unsigned_vector> m_use_list; // use lists for literals
@ -54,15 +55,17 @@ namespace sat {
public:
sls(solver& s);
~sls();
lbool operator()(unsigned sz, literal const* tabu);
lbool operator()(unsigned sz, literal const* tabu, bool reuse_model);
private:
bool local_search();
void init(unsigned sz, literal const* tabu);
void init_model(unsigned sz, literal const* tabu);
void init(unsigned sz, literal const* tabu, bool reuse_model);
void init_tabu(unsigned sz, literal const* tabu);
void init_model();
void init_use();
void init_clauses();
bool pick_flip(literal& lit);
void flip();
void flip(literal lit);
unsigned get_break_count(literal lit, unsigned min_break);
unsigned_vector const& get_use(literal lit);
};

11
src/sat/sat_solver.cpp
View file

@ -61,6 +61,7 @@ namespace sat {
for (clause * const * it = begin; it != end; ++it) {
m_cls_allocator.del_clause(*it);
}
++m_stats.m_non_learned_generation;
}
void solver::copy(solver const & src) {
@ -165,6 +166,12 @@ namespace sat {
mk_clause(3, ls);
}
void solver::del_clause(clause& c) {
m_cls_allocator.del_clause(&c);
m_stats.m_del_clause++;
if (!c.is_learned()) m_stats.m_non_learned_generation++;
}
clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) {
TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << "\n";);
if (!learned) {
@ -173,7 +180,8 @@ namespace sat {
if (!keep) {
return 0; // clause is equivalent to true.
}
}
++m_stats.m_non_learned_generation;
}
switch (num_lits) {
case 0:
@ -2690,6 +2698,7 @@ namespace sat {
m_del_clause = 0;
m_minimized_lits = 0;
m_dyn_sub_res = 0;
m_non_learned_generation = 0;
}
void mk_stat::display(std::ostream & out) const {

3
src/sat/sat_solver.h
View file

@ -58,6 +58,7 @@ namespace sat {
unsigned m_del_clause;
unsigned m_minimized_lits;
unsigned m_dyn_sub_res;
unsigned m_non_learned_generation;
stats() { reset(); }
void reset();
void collect_statistics(statistics & st) const;
@ -173,7 +174,7 @@ namespace sat {
void mk_clause(literal l1, literal l2, literal l3);
protected:
void del_clause(clause & c) { m_cls_allocator.del_clause(&c); m_stats.m_del_clause++; }
void del_clause(clause & c);
clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
void mk_bin_clause(literal l1, literal l2, bool learned);
bool propagate_bin_clause(literal l1, literal l2);