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-15 22:49:21 -07:00
parent ddb9e6e8d4
commit 33f74b9c9f
4 changed files with 110 additions and 71 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/opt/maxres.cpp
View file

@ -219,27 +219,50 @@ public:
}
lbool mss_solver() {
NOT_IMPLEMENTED_YET();
init();
init_local();
enable_sls(m_asms);
set_mus(false);
ptr_vector<expr> mcs;
while (m_lower < m_upper) {
lbool is_sat = s().check_sat(0, 0);
// is_sat = get_mcs(mcs);
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
lbool is_sat = s().check_sat(0, 0);
if (is_sat == l_true) {
vector<ptr_vector<expr> > cores;
ptr_vector<expr> mss;
model_ref mdl;
expr_ref tmp(m);
mcs.reset();
s().get_model(mdl);
update_assignment(mdl.get());
for (unsigned i = 0; i < m_asms.size(); ++i) {
VERIFY(mdl->eval(m_asms[i].get(), tmp));
if (m.is_true(tmp)) {
mss.push_back(m_asms[i].get());
}
}
is_sat = m_mss(cores, mss, mcs);
std::cout << mcs.size() << " " << is_sat << "\n";
}
switch (is_sat) {
case l_undef:
return l_undef;
case l_false:
m_lower = m_upper;
break;
case l_true:
//
case l_true: {
is_sat = process_sat(mcs);
if (is_sat != l_true) {
return is_sat;
}
model_ref mdl;
m_mss.get_model(mdl);
update_assignment(mdl.get());
break;
}
}
}
m_lower = m_upper;
return l_true;
@ -496,8 +519,9 @@ public:
lbool is_sat = s().check_sat(sz, asms.c_ptr());
switch (is_sat) {
case l_true: {
s().get_model(m_model); // last model is best way to reduce search space.
update_assignment();
model_ref mdl;
s().get_model(mdl); // last model is best way to reduce search space.
update_assignment(mdl.get());
ptr_vector<expr> mss;
mss.append(asms.size(), asms.c_ptr());
set_mus(false);
@ -506,8 +530,8 @@ public:
if (is_sat != l_true) {
return is_sat;
}
m_mss.get_model(m_model); // last model is best way to reduce search space.
update_assignment();
m_mss.get_model(mdl); // last model is best way to reduce search space.
update_assignment(mdl.get());
if (!cores.empty() && mcs.size() > cores.back().size()) {
mcs.reset();
}
@ -550,12 +574,12 @@ public:
}
void update_assignment() {
void update_assignment(model* mdl) {
rational upper(0);
expr_ref tmp(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr* n = m_soft[i].get();
VERIFY(m_model->eval(n, tmp));
VERIFY(mdl->eval(n, tmp));
if (!m.is_true(tmp)) {
upper += m_weights[i];
}
@ -565,6 +589,7 @@ public:
if (upper >= m_upper) {
return;
}
m_model = mdl;
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr* n = m_soft[i].get();

11
src/opt/maxsmt.cpp
View file

@ -28,15 +28,7 @@ Notes:
#include "wmax.h"
#include "maxsls.h"
#include "ast_pp.h"
#include "pb_decl_plugin.h"
#include "pb_sls.h"
#include "tactical.h"
#include "tactic.h"
#include "tactic2solver.h"
#include "qfbv_tactic.h"
#include "card2bv_tactic.h"
#include "uint_set.h"
#include "pb_preprocess_tactic.h"
#include "opt_context.h"
@ -133,6 +125,9 @@ namespace opt {
else if (maxsat_engine == symbol("mus-mss-maxres")) {
m_msolver = mk_mus_mss_maxres(m_c, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("mss-maxres")) {
m_msolver = mk_mss_maxres(m_c, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("pbmax")) {
m_msolver = mk_pbmax(m_c, m_weights, m_soft_constraints);
}

116
src/sat/sat_sls.cpp
View file

@ -51,7 +51,6 @@ namespace sat {
}
sls::sls(solver& s): s(s), m_cancel(false) {
m_max_tries = 1000000;
m_prob_choose_min_var = 43;
m_clause_generation = 0;
}
@ -88,6 +87,9 @@ namespace sat {
}
init_tabu(sz, tabu);
m_clause_generation = s.m_stats.m_non_learned_generation;
m_max_tries = 10*(s.num_vars() + m_clauses.size());
}
void sls::init_clauses() {
@ -363,7 +365,6 @@ namespace sat {
m_clause_weights.resize(m_clauses.size(), 1);
m_sscore.resize(s.num_vars(), 0.0);
m_hscore.resize(s.num_vars(), 0);
m_marked.resize(s.num_vars(), false);
unsigned num_violated = 0;
for (unsigned i = 0; i < m_soft.size(); ++i) {
literal lit = m_soft[i];
@ -372,7 +373,7 @@ namespace sat {
m_sscore[lit.var()] = -m_sscore[lit.var()];
}
}
for (unsigned i = 0; i < s.num_vars(); ++i) {
for (bool_var i = 0; i < s.num_vars(); ++i) {
m_hscore[i] = compute_hscore(i);
refresh_scores(i);
}
@ -380,6 +381,16 @@ namespace sat {
unsigned i = 0;
for (; !m_cancel && m_best_value > 0 && i < m_max_tries; ++i) {
wflip();
if (m_false.empty()) {
double val = evaluate_model();
if (val < m_best_value || m_best_value < 0.0) {
m_best_value = val;
m_best_model.reset();
m_best_model.append(m_model);
IF_VERBOSE(0, verbose_stream() << "new value: " << val << " @ " << i << "\n";);
m_max_tries *= 2;
}
}
}
TRACE("sat", display(tout););
IF_VERBOSE(0, verbose_stream() << "tries " << i << "\n";);
@ -394,15 +405,6 @@ namespace sat {
}
bool wsls::pick_wflip(literal & lit) {
if (m_false.empty()) {
double val = evaluate_model();
if (val < m_best_value || m_best_value < 0.0) {
m_best_value = val;
m_best_model.reset();
m_best_model.append(m_model);
IF_VERBOSE(0, verbose_stream() << "new value:" << val << "\n";);
}
}
unsigned idx;
if (!m_H.empty()) {
idx = m_H.choose(m_rand);
@ -468,7 +470,7 @@ namespace sat {
m_sscore[v] = -m_sscore[v];
m_hscore[v] = compute_hscore(v);
refresh_scores(v);
recompute_hscores(v);
recompute_hscores(lit);
}
void wsls::update_hard_weights() {
@ -550,53 +552,71 @@ namespace sat {
return hs;
}
void wsls::recompute_hscores(bool_var v) {
literal lit(v, false);
if (value_at(lit, m_model) == l_false) {
lit.neg();
}
m_marked[v] = true;
unsigned_vector const& use1 = get_use(~lit);
void wsls::recompute_hscores(literal lit) {
SASSERT(value_at(lit, m_model) == l_true);
bool_var v = lit.var();
TRACE("sat", tout << v << " := " << m_hscore[v] << "\n";);
unsigned_vector const& use1 = get_use(lit);
unsigned sz = use1.size();
unsigned csz;
for (unsigned i = 0; i < sz; ++i) {
unsigned cl = use1[i];
if (m_num_true[cl] > 2) continue;
clause const& c = *m_clauses[cl];
csz = c.size();
for (unsigned j = 0; j < csz; ++j) {
add_refresh(c[j].var());
unsigned cl = use1[i];
TRACE("sat", tout << *m_clauses[cl] << " " << m_num_true[cl] << "\n";);
SASSERT(m_num_true[cl] > 0);
if (m_num_true[cl] == 1) {
// num_true 0 -> 1
// other literals don't have upside any more.
// subtract one from all other literals
adjust_all_values(lit, cl, -static_cast<int>(m_clause_weights[cl]));
}
else if (m_num_true[cl] == 2) {
// num_true 1 -> 2, previous critical literal is no longer critical
adjust_pivot_value(lit, cl, +m_clause_weights[cl]);
}
}
unsigned_vector const& use2 = get_use(lit);
unsigned_vector const& use2 = get_use(~lit);
sz = use2.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned cl = use2[i];
if (m_num_true[cl] > 2) continue;
clause const& c = *m_clauses[cl];
csz = c.size();
for (unsigned j = 0; j < csz; ++j) {
add_refresh(c[j].var());
TRACE("sat", tout << *m_clauses[cl] << " " << m_num_true[cl] << "\n";);
if (m_num_true[cl] == 0) {
// num_true 1 -> 0
// all variables became critical.
adjust_all_values(~lit, cl, +m_clause_weights[cl]);
}
}
m_marked[v] = false;
for (unsigned i = 0; i < m_to_refresh.size(); ++i) {
v = m_to_refresh[i];
int hs = compute_hscore(v);
if (hs != m_hscore[v]) {
TRACE("sat_verbose", tout << "refresh: " << v << " from " << m_hscore[v] << " to " << hs << "\n";);
m_hscore[v] = hs;
refresh_scores(v);
else if (m_num_true[cl] == 1) {
adjust_pivot_value(~lit, cl, -static_cast<int>(m_clause_weights[cl]));
}
m_marked[v] = false;
// else n+1 -> n >= 2
}
m_to_refresh.reset();
}
void wsls::add_refresh(bool_var v) {
if (!m_marked[v]) {
m_to_refresh.push_back(v);
m_marked[v] = true;
void wsls::adjust_all_values(literal lit, unsigned cl, int delta) {
clause const& c = *m_clauses[cl];
unsigned sz = c.size();
TRACE("sat", tout << lit << " " << c << " delta: " << delta << " nt: " << m_num_true[cl] << "\n";);
for (unsigned i = 0; i < sz; ++i) {
literal lit2 = c[i];
if (lit2 != lit) {
TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";);
m_hscore[lit2.var()] += delta;
TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";);
refresh_scores(lit2.var());
}
}
}
void wsls::adjust_pivot_value(literal lit, unsigned cl, int delta) {
clause const& c = *m_clauses[cl];
unsigned csz = c.size();
for (unsigned j = 0; j < csz; ++j) {
literal lit2 = c[j];
if (lit2 != lit && value_at(lit2, m_model) == l_true) {
TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";);
m_hscore[lit2.var()] += delta;
TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";);
refresh_scores(lit2.var());
break;
}
}
}

7
src/sat/sat_sls.h
View file

@ -91,8 +91,6 @@ namespace sat {
model m_best_model;
index_set m_H, m_S;
unsigned m_smoothing_probability;
svector<bool> m_marked;
unsigned_vector m_to_refresh;
public:
wsls(solver& s);
virtual ~wsls();
@ -110,8 +108,9 @@ namespace sat {
virtual void check_invariant();
void refresh_scores(bool_var v);
int compute_hscore(bool_var v);
void recompute_hscores(bool_var v);
void add_refresh(bool_var v);
void recompute_hscores(literal lit);
void adjust_all_values(literal lit, unsigned cl, int delta);
void adjust_pivot_value(literal lit, unsigned cl, int delta);
};
};