mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

remove unused features related to weighted check-sat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-13 20:53:22 -08:00
parent 9f49905582
commit bc6b3007de
16 changed files with 58 additions and 1656 deletions
Download patch file Download diff file Expand all files Collapse all files

2
contrib/cmake/src/sat/CMakeLists.txt
View file

@ -2,7 +2,6 @@ z3_add_component(sat
SOURCES SOURCES
dimacs.cpp dimacs.cpp
sat_asymm_branch.cpp sat_asymm_branch.cpp
sat_bceq.cpp
sat_clause.cpp sat_clause.cpp
sat_clause_set.cpp sat_clause_set.cpp
sat_clause_use_list.cpp sat_clause_use_list.cpp
@ -16,7 +15,6 @@ z3_add_component(sat
sat_probing.cpp sat_probing.cpp
sat_scc.cpp sat_scc.cpp
sat_simplifier.cpp sat_simplifier.cpp
sat_sls.cpp
sat_solver.cpp sat_solver.cpp
sat_watched.cpp sat_watched.cpp
COMPONENT_DEPENDENCIES COMPONENT_DEPENDENCIES

12
src/opt/maxres.cpp
View file

@ -302,17 +302,7 @@ public:
} }
lbool check_sat(unsigned sz, expr* const* asms) { lbool check_sat(unsigned sz, expr* const* asms) {
if (m_st == s_primal_dual && m_c.sat_enabled()) { return s().check_sat(sz, asms);
rational max_weight = m_upper;
vector<rational> weights;
for (unsigned i = 0; i < sz; ++i) {
weights.push_back(get_weight(asms[i]));
}
return inc_sat_check_sat(s(), sz, asms, weights.c_ptr(), max_weight);
}
else {
return s().check_sat(sz, asms);
}
} }
void found_optimum() { void found_optimum() {

46
src/opt/pb_sls.cpp
View file

@ -20,9 +20,49 @@ Notes:
#include "smt_literal.h" #include "smt_literal.h"
#include "ast_pp.h" #include "ast_pp.h"
#include "th_rewriter.h" #include "th_rewriter.h"
#include "sat_sls.h" #include "sat_types.h"
namespace smt { namespace smt {
class index_set {
unsigned_vector m_elems;
unsigned_vector m_index;
public:
unsigned num_elems() const { return m_elems.size(); }
unsigned operator[](unsigned idx) const { return m_elems[idx]; }
void reset() { m_elems.reset(); m_index.reset(); }
bool empty() const { return m_elems.empty(); }
bool contains(unsigned idx) const {
return
(idx < m_index.size()) &&
(m_index[idx] < m_elems.size()) &&
(m_elems[m_index[idx]] == idx);
}
void insert(unsigned idx) {
m_index.reserve(idx+1);
if (!contains(idx)) {
m_index[idx] = m_elems.size();
m_elems.push_back(idx);
}
}
void remove(unsigned idx) {
if (!contains(idx)) return;
unsigned pos = m_index[idx];
m_elems[pos] = m_elems.back();
m_index[m_elems[pos]] = pos;
m_elems.pop_back();
}
unsigned choose(random_gen& rnd) const {
SASSERT(!empty());
return m_elems[rnd(num_elems())];
}
};
struct pb_sls::imp { struct pb_sls::imp {
struct clause { struct clause {
@ -73,8 +113,8 @@ namespace smt {
expr_ref_vector m_trail; expr_ref_vector m_trail;
obj_map<expr, unsigned> m_decl2var; // map declarations to Boolean variables. obj_map<expr, unsigned> m_decl2var; // map declarations to Boolean variables.
ptr_vector<expr> m_var2decl; // reverse map ptr_vector<expr> m_var2decl; // reverse map
sat::index_set m_hard_false; // list of hard clauses that are false. index_set m_hard_false; // list of hard clauses that are false.
sat::index_set m_soft_false; // list of soft clauses that are false. index_set m_soft_false; // list of soft clauses that are false.
unsigned m_max_flips; // maximal number of flips unsigned m_max_flips; // maximal number of flips
unsigned m_non_greedy_percent; // percent of moves to do non-greedy style unsigned m_non_greedy_percent; // percent of moves to do non-greedy style
random_gen m_rng; random_gen m_rng;

530
src/sat/sat_bceq.cpp
View file

@ -1,530 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sat_bceq.cpp
Abstract:
Find equivalent literals based on blocked clause decomposition.
Author:
Nikolaj Bjorner (nbjorner) 2014-09-27.
Revision History:
--*/
#include"sat_bceq.h"
#include"sat_solver.h"
#include"trace.h"
#include"bit_vector.h"
#include"map.h"
#include"sat_elim_eqs.h"
namespace sat {
void bceq::use_list::init(unsigned num_vars) {
m_clauses.reset();
m_clauses.resize(2*num_vars);
}
void bceq::use_list::insert(clause& c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
m_clauses[c[i].index()].push_back(&c);
}
}
void bceq::use_list::erase(clause& c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
m_clauses[c[i].index()].erase(&c);
}
}
ptr_vector<clause>& bceq::use_list::get(literal lit) {
return m_clauses[lit.index()];
}
bceq::bceq(solver & s):
m_solver(s) {
}
void bceq::register_clause(clause* cls) {
m_clauses.setx(cls->id(), cls, 0);
}
void bceq::unregister_clause(clause* cls) {
m_clauses.setx(cls->id(), 0, 0);
}
void bceq::init() {
m_clauses.reset();
m_bin_clauses.reset();
m_L.reset();
m_R.reset();
m_L_blits.reset();
m_R_blits.reset();
m_bce_use_list.reset();
clause * const* it = m_solver.begin_clauses();
clause * const* end = m_solver.end_clauses();
for (; it != end; ++it) {
clause* cls = *it;
if (!cls->was_removed()) {
m_use_list->insert(*cls);
register_clause(cls);
}
}
bin_clauses bc;
m_solver.collect_bin_clauses(bc, false); // exclude roots.
literal lits[2];
for (unsigned i = 0; i < bc.size(); ++i) {
lits[0] = bc[i].first;
lits[1] = bc[i].second;
clause* cls = m_solver.m_cls_allocator.mk_clause(2, lits, false);
m_use_list->insert(*cls);
m_bin_clauses.push_back(cls);
register_clause(cls);
}
TRACE("sat",
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const* cls = m_clauses[i];
if (cls) tout << *cls << "\n";
});
}
void bceq::pure_decompose() {
// while F != empty
// pick a clause and variable x in clause.
// get use list U1 of x and U2 of ~x
// assume |U1| >= |U2|
// add U1 to clause set.
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause* cls = m_clauses[i];
if (cls) {
SASSERT(i == cls->id());
pure_decompose((*cls)[0]);
SASSERT(!m_clauses[i]);
}
}
m_L.reverse();
m_L_blits.reverse();
}
void bceq::pure_decompose(literal lit) {
clause_use_list& pos = m_use_list->get(lit);
clause_use_list& neg = m_use_list->get(~lit);
unsigned sz1 = m_L.size();
unsigned sz2 = m_R.size();
pure_decompose(pos, m_L);
pure_decompose(neg, m_R);
unsigned delta1 = m_L.size() - sz1;
unsigned delta2 = m_R.size() - sz2;
if (delta1 < delta2) {
m_L_blits.resize(sz1+delta2, ~lit);
m_R_blits.resize(sz2+delta1, lit);
for (unsigned i = 0; i < delta1; ++i) {
std::swap(m_L[sz1 + i], m_R[sz2 + i]);
}
for (unsigned i = delta1; i < delta2; ++i) {
m_L.push_back(m_R[sz2 + i]);
}
m_R.resize(sz2 + delta1);
std::swap(delta1, delta2);
}
else {
m_L_blits.resize(sz1+delta1, lit);
m_R_blits.resize(sz2+delta2, ~lit);
}
TRACE("bceq", tout << lit << " " << "pos: " << delta1 << " " << "neg: " << delta2 << "\n";);
}
void bceq::pure_decompose(clause_use_list& uses, svector<clause*>& clauses) {
unsigned sz = uses.size();
for (unsigned i = 0; i < sz; ++i) {
clause& cls = *uses[i];
if (!cls.was_removed() && m_clauses[cls.id()]) {
clauses.push_back(&cls);
m_clauses[cls.id()] = 0;
}
}
}
void bceq::post_decompose() {
m_marked.reset();
m_marked.resize(2*m_solver.num_vars(), false);
use_list ul;
use_list* save = m_use_list;
m_use_list = &ul;
ul.init(m_solver.num_vars());
for (unsigned i = 0; i < m_L.size(); ++i) {
ul.insert(*m_L[i]);
}
// cheap pass: add clauses from R in order
// such that they are blocked with respect to
// predecessors.
m_removed.reset();
for (unsigned i = 0; i < m_R.size(); ++i) {
literal lit = find_blocked(*m_R[i]);
if (lit != null_literal) {
m_L.push_back(m_R[i]);
m_L_blits.push_back(lit);
ul.insert(*m_R[i]);
m_R[i] = m_R.back();
m_R_blits[i] = m_R_blits.back();
m_R.pop_back();
m_R_blits.pop_back();
--i;
}
}
// expensive pass: add clauses from R as long
// as BCE produces the empty set of clauses.
m_bce_use_list.init(m_solver.num_vars());
for (unsigned i = 0; i < m_L.size(); ++i) {
m_bce_use_list.insert(*m_L[i]);
}
for (unsigned i = 0; i < m_R.size(); ++i) {
if (bce(*m_R[i])) {
m_R[i] = m_R.back();
m_R_blits[i] = m_R_blits.back();
m_R.pop_back();
m_R_blits.pop_back();
--i;
}
}
m_use_list = save;
}
// Note: replay blocked clause elimination:
// Suppose C u { c1 } is blocked.
// annotate each clause by blocking literal.
// for new clause c2, check if C u { c2 } is blocked.
// For each c in C record which literal it is blocked.
// (Order the clauses in C by block ordering)
// l | c is blocked,
// -> c2 contains ~l => check if c c2 is blocked
//
bool bceq::bce(clause& cls0) {
IF_VERBOSE(1, verbose_stream() << "bce " << m_L.size() << " " << m_R.size() << " " << cls0 << "\n";);
unsigned_vector& live_clauses = m_live_clauses;
live_clauses.reset();
m_use_list = &m_bce_use_list;
m_bce_use_list.insert(cls0);
svector<clause*>& clauses = m_L;
literal_vector& blits = m_L_blits;
clauses.push_back(&cls0);
blits.push_back(null_literal);
bool removed = false;
m_removed.reset();
for (unsigned i = 0; i < clauses.size(); ++i) {
clause& cls1 = *clauses[i];
literal lit = find_blocked(cls1);
if (lit == null_literal) {
live_clauses.push_back(i);
}
else {
m_removed.setx(cls1.id(), true, false);
removed = true;
}
}
while (removed) {
removed = false;
//std::cout << live_clauses.size() << " ";
for (unsigned i = 0; i < live_clauses.size(); ++i) {
clause& cls1 = *clauses[live_clauses[i]];
literal lit = find_blocked(cls1);
if (lit != null_literal) {
m_removed.setx(cls1.id(), true, false);
removed = true;
live_clauses[i] = live_clauses.back();
live_clauses.pop_back();
--i;
}
}
}
//std::cout << "\n";
m_bce_use_list.erase(cls0);
clauses.pop_back();
blits.pop_back();
return live_clauses.empty();
}
literal bceq::find_blocked(clause const& cls) {
TRACE("bceq", tout << cls << "\n";);
unsigned sz = cls.size();
for (unsigned i = 0; i < sz; ++i) {
m_marked[(~cls[i]).index()] = true;
}
literal result = null_literal;
for (unsigned i = 0; i < sz; ++i) {
literal lit = cls[i];
if (is_blocked(lit)) {
TRACE("bceq", tout << "is blocked " << lit << " : " << cls << "\n";);
result = lit;
break;
}
}
for (unsigned i = 0; i < sz; ++i) {
m_marked[(~cls[i]).index()] = false;
}
return result;
}
bool bceq::is_blocked(literal lit) const {
clause_use_list& uses = m_use_list->get(~lit);
unsigned sz = uses.size();
for (unsigned i = 0; i < sz; ++i) {
clause const& cls = *uses[i];
unsigned sz = cls.size();
bool is_axiom = m_removed.get(cls.id(), false);
for (unsigned i = 0; !is_axiom && i < sz; ++i) {
is_axiom = m_marked[cls[i].index()] && cls[i] != ~lit;
}
TRACE("bceq", tout << "resolvent " << lit << " : " << cls << " " << (is_axiom?"axiom":"non-axiom") << "\n";);
if (!is_axiom) {
return false;
}
}
return true;
}
void bceq::init_rbits() {
m_rbits.reset();
for (unsigned i = 0; i < m_solver.num_vars(); ++i) {
uint64 lo = m_rand() + (m_rand() << 16);
uint64 hi = m_rand() + (m_rand() << 16);
m_rbits.push_back(lo + (hi << 32ULL));
}
}
void bceq::init_reconstruction_stack() {
m_rstack.reset();
m_bstack.reset();
// decomposition already creates a blocked stack in the proper order.
m_rstack.append(m_L);
m_bstack.append(m_L_blits);
}
uint64 bceq::eval_clause(clause const& cls) const {
uint64 b = 0;
unsigned sz = cls.size();
for (unsigned i = 0; i < sz; ++i) {
literal lit = cls[i];
uint64 val = m_rbits[lit.var()];
if (lit.sign()) {
val = ~val;
}
b |= val;
}
return b;
}
void bceq::sat_sweep() {
init_rbits();
init_reconstruction_stack();
for (unsigned i = 0; i < m_rstack.size(); ++i) {
clause const& cls = *m_rstack[i];
literal block_lit = m_bstack[i];
uint64 b = eval_clause(cls);
// v = 0, b = 0 -> v := 1
// v = 0, b = 1 -> v := 0
// v = 1, b = 0 -> v := 0
// v = 1, b = 1 -> v := 1
m_rbits[block_lit.var()] ^= ~b;
}
DEBUG_CODE(verify_sweep(););
}
void bceq::verify_sweep() {
DEBUG_CODE(
for (unsigned i = 0; i < m_L.size(); ++i) {
uint64 b = eval_clause(*m_L[i]);
SASSERT((~b) == 0);
});
}
struct u64_hash { unsigned operator()(uint64 u) const { return (unsigned)u; } };
struct u64_eq { bool operator()(uint64 u1, uint64 u2) const { return u1 == u2; } };
void bceq::extract_partition() {
unsigned num_vars = m_solver.num_vars();
map<uint64, unsigned, u64_hash, u64_eq> table;
union_find<> union_find(m_union_find_ctx);
for (unsigned i = 0; i < num_vars; ++i) {
m_s->mk_var(true, true);
union_find.mk_var();
}
for (unsigned i = 0; i < m_L.size(); ++i) {
m_s->mk_clause(m_L[i]->size(), m_L[i]->begin());
}
for (unsigned i = 0; i < num_vars; ++i) {
uint64 val = m_rbits[i];
unsigned index;
if (table.find(val, index)) {
union_find.merge(i, index);
}
else if (table.find(~val, index)) {
union_find.merge(i, index);
}
else {
table.insert(val, i);
}
}
TRACE("sat", union_find.display(tout););
//
// Preliminary version:
// A more appropriate is to walk each pair,
// and refine partition based on SAT results.
//
for (unsigned i = 0; i < num_vars; ++i) {
if (!union_find.is_root(i)) continue;
unsigned v = union_find.next(i);
unsigned last_v = UINT_MAX;
if (!m_solver.was_eliminated(i)) {
last_v = i;
}
while (v != i) {
if (!m_solver.was_eliminated(v)) {
if (last_v != UINT_MAX) {
if (check_equality(v, last_v)) {
// last_v was eliminated.
}
else {
// TBD: refine partition.
}
}
last_v = v;
}
v = union_find.next(v);
}
}
}
bool bceq::check_equality(unsigned v1, unsigned v2) {
TRACE("sat", tout << "check: " << v1 << " = " << v2 << "\n";);
uint64 val1 = m_rbits[v1];
uint64 val2 = m_rbits[v2];
literal l1 = literal(v1, false);
literal l2 = literal(v2, false);
if (val1 != val2) {
SASSERT(val1 == ~val2);
l2.neg();
}
if (is_already_equiv(l1, l2)) {
TRACE("sat", tout << "Already equivalent: " << l1 << " " << l2 << "\n";);
return false;
}
literal lits[2];
lits[0] = l1;
lits[1] = ~l2;
lbool is_sat = m_s->check(2, lits);
if (is_sat == l_false) {
lits[0] = ~l1;
lits[1] = l2;
is_sat = m_s->check(2, lits);
}
if (is_sat == l_false) {
TRACE("sat", tout << "Found equivalent: " << l1 << " " << l2 << "\n";);
assert_equality(l1, l2);
}
else {
TRACE("sat", tout << "Not equivalent: " << l1 << " " << l2 << "\n";);
// TBD: if is_sat == l_true, then refine partition.
}
return is_sat == l_false;
}
bool bceq::is_already_equiv(literal l1, literal l2) {
watch_list const& w1 = m_solver.get_wlist(l1);
bool found = false;
for (unsigned i = 0; !found && i < w1.size(); ++i) {
watched const& w = w1[i];
found = w.is_binary_clause() && w.get_literal() == ~l2;
}
if (!found) return false;
found = false;
watch_list const& w2 = m_solver.get_wlist(~l1);
for (unsigned i = 0; !found && i < w2.size(); ++i) {
watched const& w = w2[i];
found = w.is_binary_clause() && w.get_literal() == l2;
}
return found;
}
void bceq::assert_equality(literal l1, literal l2) {
if (l2.sign()) {
l1.neg();
l2.neg();
}
literal_vector roots;
bool_var_vector vars;
for (unsigned i = 0; i < m_solver.num_vars(); ++i) {
roots.push_back(literal(i, false));
}
roots[l2.var()] = l1;
vars.push_back(l2.var());
elim_eqs elim(m_solver);
IF_VERBOSE(1,
for (unsigned i = 0; i < vars.size(); ++i) {
verbose_stream() << "var: " << vars[i] << " root: " << roots[vars[i]] << "\n";
});
elim(roots, vars);
}
void bceq::cleanup() {
m_solver.del_clauses(m_bin_clauses.begin(), m_bin_clauses.end());
m_bin_clauses.reset();
}
void bceq::operator()() {
if (!m_solver.m_config.m_bcd) return;
flet<bool> _disable_bcd(m_solver.m_config.m_bcd, false);
flet<bool> _disable_min(m_solver.m_config.m_core_minimize, false);
flet<bool> _disable_opt(m_solver.m_config.m_optimize_model, false);
flet<unsigned> _bound_maxc(m_solver.m_config.m_max_conflicts, 1500);
use_list ul;
solver s(m_solver.m_params, m_solver.rlimit(), 0);
s.m_config.m_bcd = false;
s.m_config.m_core_minimize = false;
s.m_config.m_optimize_model = false;
s.m_config.m_max_conflicts = 1500;
m_use_list = &ul;
m_s = &s;
ul.init(m_solver.num_vars());
init();
pure_decompose();
post_decompose();
IF_VERBOSE(1, verbose_stream() << "Decomposed set " << m_L.size() << " rest: " << m_R.size() << "\n";);
TRACE("sat",
tout << "Decomposed set " << m_L.size() << "\n";
for (unsigned i = 0; i < m_L.size(); ++i) {
clause const* cls = m_L[i];
if (cls) tout << *cls << "\n";
}
tout << "remainder " << m_R.size() << "\n";
for (unsigned i = 0; i < m_R.size(); ++i) {
clause const* cls = m_R[i];
if (cls) tout << *cls << "\n";
}
);
sat_sweep();
extract_partition();
cleanup();
}
};

89
src/sat/sat_bceq.h
View file

@ -1,89 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sat_bceq.h
Abstract:
Find equivalent literals based on blocked clause decomposition.
Author:
Nikolaj Bjorner (nbjorner) 2014-09-27.
Revision History:
--*/
#ifndef SAT_BCEQ_H_
#define SAT_BCEQ_H_
#include"sat_types.h"
#include"union_find.h"
namespace sat {
class solver;
class bceq {
typedef ptr_vector<clause> clause_use_list;
class use_list {
vector<ptr_vector<clause> > m_clauses;
public:
use_list() {}
void init(unsigned num_vars);
void reset() { m_clauses.reset(); }
void erase(clause& c);
void insert(clause& c);
ptr_vector<clause>& get(literal lit);
};
typedef std::pair<literal, literal> bin_clause;
typedef svector<bin_clause> bin_clauses;
solver & m_solver;
use_list* m_use_list;
use_list m_bce_use_list;
solver* m_s;
random_gen m_rand;
svector<clause*> m_clauses;
svector<clause*> m_L;
svector<clause*> m_R;
literal_vector m_L_blits;
literal_vector m_R_blits;
svector<clause*> m_bin_clauses;
svector<uint64> m_rbits;
svector<clause*> m_rstack; // stack of blocked clauses
literal_vector m_bstack; // stack of blocking literals
svector<bool> m_marked;
svector<bool> m_removed; // set of clauses removed (not considered in clause set during BCE)
union_find_default_ctx m_union_find_ctx;
unsigned_vector m_live_clauses;
void init();
void register_clause(clause* cls);
void unregister_clause(clause* cls);
void pure_decompose();
void pure_decompose(literal lit);
void pure_decompose(ptr_vector<clause>& uses, svector<clause*>& clauses);
void post_decompose();
literal find_blocked(clause const& cls);
bool bce(clause& cls);
bool is_blocked(literal lit) const;
void init_rbits();
void init_reconstruction_stack();
void sat_sweep();
void cleanup();
uint64 eval_clause(clause const& cls) const;
void verify_sweep();
void extract_partition();
bool check_equality(unsigned v1, unsigned v2);
bool is_already_equiv(literal l1, literal l2);
void assert_equality(literal l1, literal l2);
public:
bceq(solver & s);
void operator()();
};
};
#endif

2
src/sat/sat_config.cpp
View file

@ -111,8 +111,6 @@ namespace sat {
m_minimize_lemmas = p.minimize_lemmas(); m_minimize_lemmas = p.minimize_lemmas();
m_core_minimize = p.core_minimize(); m_core_minimize = p.core_minimize();
m_core_minimize_partial = p.core_minimize_partial(); m_core_minimize_partial = p.core_minimize_partial();
m_optimize_model = p.optimize_model();
m_bcd = p.bcd();
m_dyn_sub_res = p.dyn_sub_res(); m_dyn_sub_res = p.dyn_sub_res();
} }

2
src/sat/sat_config.h
View file

@ -72,8 +72,6 @@ namespace sat {
bool m_dyn_sub_res; bool m_dyn_sub_res;
bool m_core_minimize; bool m_core_minimize;
bool m_core_minimize_partial; bool m_core_minimize_partial;
bool m_optimize_model;
bool m_bcd;
symbol m_always_true; symbol m_always_true;

37
src/sat/sat_mus.cpp
View file

@ -20,11 +20,10 @@ Notes:
#include "sat_solver.h" #include "sat_solver.h"
#include "sat_mus.h" #include "sat_mus.h"
#include "sat_sls.h"
namespace sat { namespace sat {
mus::mus(solver& s):s(s), m_is_active(false), m_best_value(0), m_restart(0), m_max_restarts(0) {} mus::mus(solver& s):s(s), m_is_active(false),m_restart(0), m_max_restarts(0) {}
mus::~mus() {} mus::~mus() {}
@ -32,7 +31,6 @@ namespace sat {
m_core.reset(); m_core.reset();
m_mus.reset(); m_mus.reset();
m_model.reset(); m_model.reset();
m_best_value = 0;
m_max_restarts = (s.m_stats.m_restart - m_restart) + 10; m_max_restarts = (s.m_stats.m_restart - m_restart) + 10;
m_restart = s.m_stats.m_restart; m_restart = s.m_stats.m_restart;
} }
@ -45,21 +43,13 @@ namespace sat {
} }
void mus::update_model() { void mus::update_model() {
double new_value = s.m_wsls.evaluate_model(s.m_model);
if (m_model.empty()) { if (m_model.empty()) {
m_model.append(s.m_model); m_model.append(s.m_model);
m_best_value = new_value;
}
else if (m_best_value > new_value) {
m_model.reset();
m_model.append(s.m_model);
m_best_value = new_value;
} }
} }
lbool mus::operator()() { lbool mus::operator()() {
flet<bool> _disable_min(s.m_config.m_core_minimize, false); flet<bool> _disable_min(s.m_config.m_core_minimize, false);
flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
flet<bool> _is_active(m_is_active, true); flet<bool> _is_active(m_is_active, true);
IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";); IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
reset(); reset();
@ -120,9 +110,6 @@ namespace sat {
SASSERT(value_at(lit, s.get_model()) == l_false); SASSERT(value_at(lit, s.get_model()) == l_false);
mus.push_back(lit); mus.push_back(lit);
update_model(); update_model();
if (!core.empty()) {
// mr(); // TBD: measure
}
break; break;
} }
case l_false: case l_false:
@ -262,27 +249,5 @@ namespace sat {
IF_VERBOSE(3, verbose_stream() << "core verification: " << is_sat << " " << core << "\n";); IF_VERBOSE(3, verbose_stream() << "core verification: " << is_sat << " " << core << "\n";);
} }
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(), reuse_model);
tabu[i] = ~tabu[i];
if (is_sat == l_true) {
m_mus.push_back(tabu[i]);
m_core.erase(tabu[i]);
IF_VERBOSE(3, verbose_stream() << "in core " << tabu[i] << "\n";);
reuse_model = true;
}
else {
IF_VERBOSE(3, verbose_stream() << "NOT in core " << tabu[i] << "\n";);
reuse_model = false;
}
}
}
} }

2
src/sat/sat_mus.h
View file

@ -26,7 +26,6 @@ namespace sat {
literal_vector m_mus; literal_vector m_mus;
bool m_is_active; bool m_is_active;
model m_model; // model obtained during minimal unsat core model m_model; // model obtained during minimal unsat core
double m_best_value;
unsigned m_restart; unsigned m_restart;
unsigned m_max_restarts; unsigned m_max_restarts;
@ -41,7 +40,6 @@ namespace sat {
lbool mus1(); lbool mus1();
lbool mus2(); lbool mus2();
lbool qx(literal_set& assignment, literal_set& support, bool has_support); lbool qx(literal_set& assignment, literal_set& support, bool has_support);
void mr();
void reset(); void reset();
void set_core(); void set_core();
void update_model(); void update_model();

2
src/sat/sat_params.pyg
View file

@ -22,6 +22,4 @@ def_module_params('sat',
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
('core.minimize', BOOL, False, 'minimize computed core'), ('core.minimize', BOOL, False, 'minimize computed core'),
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

686
src/sat/sat_sls.cpp
View file

@ -1,686 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sat_sls.cpp
Abstract:
SLS for clauses in SAT solver
Author:
Nikolaj Bjorner (nbjorner) 2014-12-8
Notes:
--*/
#include "sat_sls.h"
#include "sat_solver.h"
namespace sat {
bool index_set::contains(unsigned idx) const {
return
(idx < m_index.size()) &&
(m_index[idx] < m_elems.size()) &&
(m_elems[m_index[idx]] == idx);
}
void index_set::insert(unsigned idx) {
m_index.reserve(idx+1);
if (!contains(idx)) {
m_index[idx] = m_elems.size();
m_elems.push_back(idx);
}
}
void index_set::remove(unsigned idx) {
if (!contains(idx)) return;
unsigned pos = m_index[idx];
m_elems[pos] = m_elems.back();
m_index[m_elems[pos]] = pos;
m_elems.pop_back();
}
unsigned index_set::choose(random_gen& rnd) const {
SASSERT(!empty());
return m_elems[rnd(num_elems())];
}
sls::sls(solver& s): s(s) {
m_prob_choose_min_var = 43;
m_clause_generation = 0;
}
sls::~sls() {
for (unsigned i = 0; i < m_bin_clauses.size(); ++i) {
m_alloc.del_clause(m_bin_clauses[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() && !s.canceled() && 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;
}
return l_undef;
}
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;
m_max_tries = 10*(s.num_vars() + m_clauses.size());
}
void sls::init_clauses() {
for (unsigned i = 0; i < m_bin_clauses.size(); ++i) {
m_alloc.del_clause(m_bin_clauses[i]);
}
m_bin_clauses.reset();
m_clauses.reset();
clause * const * it = s.begin_clauses();
clause * const * end = s.end_clauses();
for (; it != end; ++it) {
m_clauses.push_back(*it);
}
svector<solver::bin_clause> bincs;
s.collect_bin_clauses(bincs, false);
literal lits[2];
for (unsigned i = 0; i < bincs.size(); ++i) {
lits[0] = bincs[i].first;
lits[1] = bincs[i].second;
clause* cl = m_alloc.mk_clause(2, lits, false);
m_clauses.push_back(cl);
m_bin_clauses.push_back(cl);
}
}
void sls::init_model() {
m_num_true.reset();
m_model.reset();
m_model.append(s.get_model());
unsigned sz = m_clauses.size();
for (unsigned i = 0; i < sz; ++i) {
clause const& c = *m_clauses[i];
unsigned n = 0;
unsigned csz = c.size();
for (unsigned j = 0; j < csz; ++j) {
lbool val = value_at(c[j], m_model);
switch (val) {
case l_true:
++n;
break;
case l_undef:
++n;
m_model[c[j].var()] = c[j].sign()?l_false:l_true;
SASSERT(value_at(c[j], m_model) == l_true);
break;
default:
break;
}
}
m_num_true.push_back(n);
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() {
m_use_list.reset();
m_use_list.resize(s.num_vars()*2);
unsigned sz = m_clauses.size();
for (unsigned i = 0; i < sz; ++i) {
clause const& c = *m_clauses[i];
unsigned csz = c.size();
for (unsigned j = 0; j < csz; ++j) {
m_use_list[c[j].index()].push_back(i);
}
}
DEBUG_CODE(check_use_list(););
}
unsigned_vector const& sls::get_use(literal lit) {
SASSERT(lit.index() < m_use_list.size());
return m_use_list[lit.index()];
}
unsigned sls::get_break_count(literal lit, unsigned min_break) {
SASSERT(value_at(lit, m_model) == l_false);
unsigned result = 0;
unsigned_vector const& uses = get_use(~lit);
unsigned sz = uses.size();
for (unsigned i = 0; i < sz; ++i) {
if (m_num_true[uses[i]] == 1) {
++result;
if (result > min_break) return result;
}
}
return result;
}
bool sls::pick_flip(literal& lit) {
unsigned clause_idx = m_false.choose(m_rand);
clause const& c = *m_clauses[clause_idx];
SASSERT(!c.satisfied_by(m_model));
unsigned min_break = UINT_MAX;
unsigned sz = c.size();
m_min_vars.reset();
for (unsigned i = 0; i < sz; ++i) {
lit = c[i];
if (m_tabu[lit.var()]) continue;
unsigned break_count = get_break_count(lit, min_break);
if (break_count < min_break) {
min_break = break_count;
m_min_vars.reset();
m_min_vars.push_back(lit);
}
else if (break_count == min_break) {
m_min_vars.push_back(lit);
}
}
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;
}
else if (min_break == UINT_MAX) {
return false;
}
else {
lit = c[m_rand(c.size())];
return !m_tabu[lit.var()];
}
}
void sls::flip() {
literal lit;
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);
unsigned sz = use1.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned cl = use1[i];
m_num_true[cl]++;
SASSERT(m_num_true[cl] <= m_clauses[cl]->size());
if (m_num_true[cl] == 1) m_false.remove(cl);
}
unsigned_vector const& use2 = get_use(~lit);
sz = use2.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned cl = use2[i];
SASSERT(m_num_true[cl] > 0);
m_num_true[cl]--;
if (m_num_true[cl] == 0) m_false.insert(cl);
}
}
void sls::check_invariant() {
DEBUG_CODE(
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
bool is_sat = c.satisfied_by(m_model);
SASSERT(is_sat != m_false.contains(i));
SASSERT(is_sat == (m_num_true[i] > 0));
});
}
void sls::check_use_list() {
DEBUG_CODE(
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
for (unsigned j = 0; j < c.size(); ++j) {
unsigned idx = c[j].index();
SASSERT(m_use_list[idx].contains(i));
}
}
for (unsigned i = 0; i < m_use_list.size(); ++i) {
literal lit = to_literal(i);
for (unsigned j = 0; j < m_use_list[i].size(); ++j) {
clause const& c = *m_clauses[m_use_list[i][j]];
bool found = false;
for (unsigned k = 0; !found && k < c.size(); ++k) {
found = c[k] == lit;
}
SASSERT(found);
}
});
}
void sls::display(std::ostream& out) const {
out << "Model\n";
for (bool_var v = 0; v < m_model.size(); ++v) {
out << v << ": " << m_model[v] << "\n";
}
out << "Clauses\n";
unsigned sz = m_false.num_elems();
for (unsigned i = 0; i < sz; ++i) {
out << *m_clauses[m_false[i]] << "\n";
}
for (unsigned i = 0; i < m_clauses.size(); ++i) {
if (m_false.contains(i)) continue;
clause const& c = *m_clauses[i];
out << c << " " << m_num_true[i] << "\n";
}
bool has_tabu = false;
for (unsigned i = 0; !has_tabu && i < m_tabu.size(); ++i) {
has_tabu = m_tabu[i];
}
if (has_tabu) {
out << "Tabu: ";
for (unsigned i = 0; i < m_tabu.size(); ++i) {
if (m_tabu[i]) {
literal lit(i, false);
if (value_at(lit, m_model) == l_false) lit.neg();
out << lit << " ";
}
}
out << "\n";
}
}
wsls::wsls(solver& s):
sls(s)
{
m_smoothing_probability = 1; // 1/1000
}
wsls::~wsls() {}
void wsls::set_soft(unsigned sz, literal const* lits, double const* weights) {
m_soft.reset();
m_weights.reset();
m_soft.append(sz, lits);
m_weights.append(sz, weights);
}
void wsls::opt(unsigned sz, literal const* tabu, bool reuse_model) {
init(sz, tabu, reuse_model);
//
// Initialize m_clause_weights, m_hscore, m_sscore.
//
m_best_value = m_false.empty()?evaluate_model(m_model):-1.0;
m_best_model.reset();
m_clause_weights.reset();
m_hscore.reset();
m_sscore.reset();
m_H.reset();
m_S.reset();
m_best_model.append(s.get_model());
m_clause_weights.resize(m_clauses.size(), 1);
m_sscore.resize(s.num_vars(), 0.0);
m_hscore.resize(s.num_vars(), 0);
for (unsigned i = 0; i < m_soft.size(); ++i) {
literal lit = m_soft[i];
m_sscore[lit.var()] = m_weights[i];
if (value_at(lit, m_model) == l_true) {
m_sscore[lit.var()] = -m_sscore[lit.var()];
}
}
for (bool_var i = 0; i < s.num_vars(); ++i) {
m_hscore[i] = compute_hscore(i);
refresh_scores(i);
}
DEBUG_CODE(check_invariant(););
unsigned i = 0;
for (; !s.canceled() && m_best_value > 0 && i < m_max_tries; ++i) {
wflip();
if (m_false.empty()) {
double val = evaluate_model(m_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);
s.set_model(m_best_model);
IF_VERBOSE(1, verbose_stream() << "new value: " << val << " @ " << i << "\n";);
if (i*2 > m_max_tries) {
m_max_tries *= 2;
}
}
}
}
TRACE("sat", display(tout););
IF_VERBOSE(0, verbose_stream() << "tries " << i << "\n";);
}
void wsls::wflip() {
literal lit;
if (pick_wflip(lit)) {
// IF_VERBOSE(0, verbose_stream() << lit << " ";);
wflip(lit);
}
}
bool wsls::pick_wflip(literal & lit) {
unsigned idx;
if (!m_H.empty()) {
idx = m_H.choose(m_rand);
lit = literal(idx, false);
if (value_at(lit, m_model) == l_true) lit.neg();
SASSERT(value_at(lit, m_model) == l_false);
TRACE("sat", tout << "flip H(" << m_H.num_elems() << ") " << lit << "\n";);
}
else if (!m_S.empty()) {
double score = 0.0;
m_min_vars.reset();
for (unsigned i = 0; i < m_S.num_elems(); ++i) {
unsigned v = m_S[i];
SASSERT(m_sscore[v] > 0.0);
if (m_sscore[v] > score) {
m_min_vars.reset();
m_min_vars.push_back(literal(v, false));
score = m_sscore[v];
}
else if (m_sscore[v] == score) {
m_min_vars.push_back(literal(v, false));
}
}
lit = m_min_vars[m_rand(m_min_vars.size())]; // pick with largest sscore.
SASSERT(value_at(lit, m_model) == l_false);
TRACE("sat", tout << "flip S(" << m_min_vars.size() << "," << score << ") " << lit << "\n";);
}
else {
update_hard_weights();
if (!m_false.empty()) {
unsigned cls_idx = m_false.choose(m_rand);
clause const& c = *m_clauses[cls_idx];
lit = c[m_rand(c.size())];
TRACE("sat", tout << "flip hard(" << m_false.num_elems() << "," << c.size() << ") " << lit << "\n";);
}
else {
m_min_vars.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
lit = m_soft[i];
if (value_at(lit, m_model) == l_false) {
m_min_vars.push_back(lit);
}
}
if (m_min_vars.empty()) {
SASSERT(m_best_value == 0.0);
UNREACHABLE(); // we should have exited the main loop before.
return false;
}
else {
lit = m_min_vars[m_rand(m_min_vars.size())];
}
TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ", " << m_sscore[lit.var()] << ") " << lit << "\n";);
}
SASSERT(value_at(lit, m_model) == l_false);
}
return !m_tabu[lit.var()];
}
void wsls::wflip(literal lit) {
flip(lit);
unsigned v = lit.var();
m_sscore[v] = -m_sscore[v];
m_hscore[v] = compute_hscore(v);
refresh_scores(v);
recompute_hscores(lit);
}
void wsls::update_hard_weights() {
unsigned csz = m_clauses.size();
if (m_smoothing_probability >= m_rand(1000)) {
for (unsigned i = 0; i < csz; ++i) {
if (m_clause_weights[i] > 1 && !m_false.contains(i)) {
--m_clause_weights[i];
if (m_num_true[i] == 1) {
clause const& c = *m_clauses[i];
unsigned sz = c.size();
for (unsigned j = 0; j < sz; ++j) {
if (value_at(c[j], m_model) == l_true) {
++m_hscore[c[j].var()];
refresh_scores(c[j].var());
break;
}
}
}
}
}
}
else {
for (unsigned i = 0; i < csz; ++i) {
if (m_false.contains(i)) {
++m_clause_weights[i];
clause const& c = *m_clauses[i];
unsigned sz = c.size();
for (unsigned j = 0; j < sz; ++j) {
++m_hscore[c[j].var()];
refresh_scores(c[j].var());
}
}
}
}
DEBUG_CODE(check_invariant(););
}
double wsls::evaluate_model(model& mdl) {
SASSERT(m_false.empty());
double result = 0.0;
for (unsigned i = 0; i < m_soft.size(); ++i) {
literal lit = m_soft[i];
if (value_at(lit, mdl) != l_true) {
result += m_weights[i];
}
}
return result;
}
int wsls::compute_hscore(bool_var v) {
literal lit(v, false);
if (value_at(lit, m_model) == l_false) {
lit.neg();
}
SASSERT(value_at(lit, m_model) == l_true);
int hs = 0;
unsigned_vector const& use1 = get_use(~lit);
unsigned sz = use1.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned cl = use1[i];
if (m_num_true[cl] == 0) {
SASSERT(m_false.contains(cl));
hs += m_clause_weights[cl];
}
else {
SASSERT(!m_false.contains(cl));
}
}
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] == 1) {
SASSERT(!m_false.contains(cl));
hs -= m_clause_weights[cl];
}
}
return hs;
}
void wsls::recompute_hscores(literal lit) {
SASSERT(value_at(lit, m_model) == l_true);
TRACE("sat", tout << lit.var() << " := " << m_hscore[lit.var()] << "\n";);
unsigned_vector const& use1 = get_use(lit);
unsigned sz = use1.size();
for (unsigned i = 0; i < sz; ++i) {
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);
sz = use2.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned cl = use2[i];
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]);
}
else if (m_num_true[cl] == 1) {
adjust_pivot_value(~lit, cl, -static_cast<int>(m_clause_weights[cl]));
}
// else n+1 -> n >= 2
}
}
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;
}
}
}
void wsls::refresh_scores(bool_var v) {
if (m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) {
m_H.insert(v);
}
else {
m_H.remove(v);
}
if (m_sscore[v] > 0) {
if (m_hscore[v] == 0 && !m_tabu[v]) {
m_S.insert(v);
}
else {
m_S.remove(v);
}
}
else if (m_sscore[v] < 0) {
m_S.remove(v);
}
}
void wsls::check_invariant() {
sls::check_invariant();
// The hscore is the reward for flipping the truth value of variable v.
// hscore(v) = Sum weight(c) for num_true(c) = 0 and v in c
// - Sum weight(c) for num_true(c) = 1 and (v in c, M(v) or !v in c and !M(v))
DEBUG_CODE(
for (unsigned v = 0; v < s.num_vars(); ++v) {
int hs = compute_hscore(v);
CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n"););
SASSERT(m_hscore[v] == hs);
}
// The score(v) is the reward on soft clauses for flipping v.
for (unsigned j = 0; j < m_soft.size(); ++j) {
unsigned v = m_soft[j].var();
double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j];
SASSERT(m_sscore[v] == ss);
}
// m_H are values such that m_hscore > 0 and sscore = 0.
for (bool_var v = 0; v < m_hscore.size(); ++v) {
SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v));
}
// m_S are values such that hscore = 0, sscore > 0
for (bool_var v = 0; v < m_sscore.size(); ++v) {
SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v));
});
}
void wsls::display(std::ostream& out) const {
sls::display(out);
out << "Best model\n";
for (bool_var v = 0; v < m_best_model.size(); ++v) {
out << v << ": " << m_best_model[v] << " h: " << m_hscore[v];
if (m_sscore[v] != 0.0) out << " s: " << m_sscore[v];
out << "\n";
}
}
};

115
src/sat/sat_sls.h
View file

@ -1,115 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sat_sls.h
Abstract:
SLS for clauses in SAT solver
Author:
Nikolaj Bjorner (nbjorner) 2014-12-8
Notes:
--*/
#ifndef SAT_SLS_H_
#define SAT_SLS_H_
#include "util.h"
#include "sat_simplifier.h"
namespace sat {
class index_set {
unsigned_vector m_elems;
unsigned_vector m_index;
public:
unsigned num_elems() const { return m_elems.size(); }
unsigned operator[](unsigned idx) const { return m_elems[idx]; }
void reset() { m_elems.reset(); m_index.reset(); }
bool empty() const { return m_elems.empty(); }
bool contains(unsigned idx) const;
void insert(unsigned idx);
void remove(unsigned idx);
unsigned choose(random_gen& rnd) const;
};
class sls {
protected:
solver& s;
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
unsigned_vector m_num_true; // per clause, count of # true literals
svector<literal> m_min_vars; // literals with smallest break count
model m_model; // current model
clause_allocator m_alloc; // clause allocator
clause_vector m_bin_clauses; // binary clauses
svector<bool> m_tabu; // variables that cannot be swapped
public:
sls(solver& s);
virtual ~sls();
lbool operator()(unsigned sz, literal const* tabu, bool reuse_model);
void set_max_tries(unsigned mx) { m_max_tries = mx; }
virtual void display(std::ostream& out) const;
protected:
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();
unsigned_vector const& get_use(literal lit);
void flip(literal lit);
virtual void check_invariant();
void check_use_list();
private:
bool pick_flip(literal& lit);
void flip();
unsigned get_break_count(literal lit, unsigned min_break);
};
/**
\brief sls with weighted soft clauses.
*/
class wsls : public sls {
unsigned_vector m_clause_weights;
svector<int> m_hscore;
svector<double> m_sscore;
literal_vector m_soft;
svector<double> m_weights;
double m_best_value;
model m_best_model;
index_set m_H, m_S;
unsigned m_smoothing_probability;
public:
wsls(solver& s);
virtual ~wsls();
void set_soft(unsigned sz, literal const* lits, double const* weights);
bool has_soft() const { return !m_soft.empty(); }
void opt(unsigned sz, literal const* tabu, bool reuse_model);
virtual void display(std::ostream& out) const;
double evaluate_model(model& mdl);
private:
void wflip();
void wflip(literal lit);
void update_hard_weights();
bool pick_wflip(literal & lit);
virtual void check_invariant();
void refresh_scores(bool_var v);
int compute_hscore(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);
};
};
#endif

143
src/sat/sat_solver.cpp
View file

@ -20,7 +20,6 @@ Revision History:
#include"sat_integrity_checker.h" #include"sat_integrity_checker.h"
#include"luby.h" #include"luby.h"
#include"trace.h" #include"trace.h"
#include"sat_bceq.h"
#include"max_cliques.h" #include"max_cliques.h"
// define to update glue during propagation // define to update glue during propagation
@ -42,7 +41,6 @@ namespace sat {
m_asymm_branch(*this, p), m_asymm_branch(*this, p),
m_probing(*this, p), m_probing(*this, p),
m_mus(*this), m_mus(*this),
m_wsls(*this),
m_inconsistent(false), m_inconsistent(false),
m_num_frozen(0), m_num_frozen(0),
m_activity_inc(128), m_activity_inc(128),
@ -55,7 +53,6 @@ namespace sat {
m_conflicts = 0; m_conflicts = 0;
m_next_simplify = 0; m_next_simplify = 0;
m_num_checkpoints = 0; m_num_checkpoints = 0;
m_initializing_preferred = false;
} }
solver::~solver() { solver::~solver() {
@ -713,7 +710,7 @@ namespace sat {
// Search // Search
// //
// ----------------------- // -----------------------
lbool solver::check(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { lbool solver::check(unsigned num_lits, literal const* lits) {
pop_to_base_level(); pop_to_base_level();
IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
SASSERT(scope_lvl() == 0); SASSERT(scope_lvl() == 0);
@ -728,7 +725,7 @@ namespace sat {
init_search(); init_search();
propagate(false); propagate(false);
if (inconsistent()) return l_false; if (inconsistent()) return l_false;
init_assumptions(num_lits, lits, weights, max_weight); init_assumptions(num_lits, lits);
propagate(false); propagate(false);
if (check_inconsistent()) return l_false; if (check_inconsistent()) return l_false;
cleanup(); cleanup();
@ -914,12 +911,11 @@ namespace sat {
} }
} }
void solver::init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { void solver::init_assumptions(unsigned num_lits, literal const* lits) {
if (num_lits == 0 && m_user_scope_literals.empty()) { if (num_lits == 0 && m_user_scope_literals.empty()) {
return; return;
} }
retry_init_assumptions:
reset_assumptions(); reset_assumptions();
push(); push();
@ -943,16 +939,6 @@ namespace sat {
assign(nlit, justification()); assign(nlit, justification());
} }
if (weights && !inconsistent()) {
if (m_config.m_optimize_model) {
m_wsls.set_soft(num_lits, lits, weights);
}
if (!init_weighted_assumptions(num_lits, lits, weights, max_weight)) {
goto retry_init_assumptions;
}
return;
}
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i]; literal lit = lits[i];
SASSERT(is_external(lit.var())); SASSERT(is_external(lit.var()));
@ -962,109 +948,6 @@ namespace sat {
} }
bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) {
flet<bool> _min1(m_config.m_core_minimize, false);
m_weight = 0;
m_blocker.reset();
svector<lbool> values;
unsigned num_cores = 0;
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i];
SASSERT(is_external(lit.var()));
TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";);
SASSERT(m_scope_lvl == 1);
add_assumption(lit);
switch(value(lit)) {
case l_undef:
values.push_back(l_true);
assign(lit, justification());
if (num_cores*2 >= num_lits) {
break;
}
propagate(false);
if (inconsistent()) {
flet<bool> _init(m_initializing_preferred, true);
while (inconsistent()) {
if (!resolve_conflict()) {
return true;
}
propagate(true);
}
if (m_scope_lvl == 0) {
return false;
}
// backjump to last consistent assumption:
unsigned j;
m_weight = 0;
m_blocker.reset();
for (j = 0; j < i && value(lits[j]) == values[j]; ++j) {
if (values[j] == l_false) {
m_weight += weights[j];
m_blocker.push_back(lits[j]);
}
}
SASSERT(value(lits[j]) != values[j]);
SASSERT(j <= i);
SASSERT(j == 0 || value(lits[j-1]) == values[j-1]);
for (unsigned k = i; k >= j; --k) {
if (is_assumption(lits[k])) {
pop_assumption();
}
}
values.resize(j);
TRACE("sat", tout << "backjump " << (i - j + 1) << " steps " << num_cores << "\n";);
i = j - 1;
}
break;
case l_false:
++num_cores;
values.push_back(l_false);
SASSERT(!inconsistent());
set_conflict(justification(), ~lit);
m_conflict_lvl = scope_lvl();
resolve_conflict_for_unsat_core();
IF_VERBOSE(3, verbose_stream() << "(sat.core: " << m_core << ")\n";);
update_min_core();
SASSERT(m_min_core_valid);
m_weight += weights[i];
if (m_weight <= max_weight) {
m_blocker.push_back(lit);
}
TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";);
SASSERT(m_core.size() <= m_assumptions.size());
SASSERT(m_assumptions.size() <= i+1);
if (m_core.size() <= 3) {
m_inconsistent = true;
TRACE("opt", tout << "found small core: " << m_core << "\n";);
IF_VERBOSE(11, verbose_stream() << "(sat.core: " << m_core << ")\n";);
return true;
}
pop_assumption();
m_inconsistent = false;
break;
case l_true:
values.push_back(l_true);
SASSERT(m_justification[lit.var()].get_kind() != justification::NONE || lvl(lit) == 0);
break;
}
}
TRACE("sat", tout << "initialized\n";);
IF_VERBOSE(11, verbose_stream() << "(sat.blocker: " << m_blocker << "\nCore: " << m_min_core << ")\n";);
if (m_weight >= max_weight) {
// block the current correction set candidate.
++m_stats.m_blocked_corr_sets;
TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";);
IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";);
pop_to_base_level();
mk_clause_core(m_blocker);
return false;
}
return true;
}
void solver::update_min_core() { void solver::update_min_core() {
if (!m_min_core_valid || m_core.size() < m_min_core.size()) { if (!m_min_core_valid || m_core.size() < m_min_core.size()) {
m_min_core.reset(); m_min_core.reset();
@ -1148,11 +1031,6 @@ namespace sat {
m_min_core_valid = false; m_min_core_valid = false;
m_min_core.reset(); m_min_core.reset();
TRACE("sat", display(tout);); TRACE("sat", display(tout););
if (m_config.m_bcd) {
bceq bc(*this);
bc();
}
} }
/** /**
@ -1244,9 +1122,6 @@ namespace sat {
m_model[v] = value(v); m_model[v] = value(v);
} }
TRACE("sat_mc_bug", m_mc.display(tout);); TRACE("sat_mc_bug", m_mc.display(tout););
if (m_config.m_optimize_model) {
m_wsls.opt(0, 0, false);
}
m_mc(m_model); m_mc(m_model);
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
@ -1673,10 +1548,6 @@ namespace sat {
if (m_not_l == literal()) tout << "null literal\n"; if (m_not_l == literal()) tout << "null literal\n";
else tout << m_not_l << "\n";); else tout << m_not_l << "\n";);
if (m_initializing_preferred) {
SASSERT(m_conflict_lvl <= 1);
return resolve_conflict_for_init();
}
if (m_conflict_lvl <= 1 && tracking_assumptions()) { if (m_conflict_lvl <= 1 && tracking_assumptions()) {
resolve_conflict_for_unsat_core(); resolve_conflict_for_unsat_core();
return false; return false;
@ -3184,10 +3055,10 @@ namespace sat {
if (asms.empty()) { if (asms.empty()) {
bool_var v = mk_var(true, false); bool_var v = mk_var(true, false);
literal lit(v, false); literal lit(v, false);
init_assumptions(1, &lit, 0, 0); init_assumptions(1, &lit);
} }
else { else {
init_assumptions(asms.size(), asms.c_ptr(), 0, 0); init_assumptions(asms.size(), asms.c_ptr());
} }
propagate(false); propagate(false);
if (check_inconsistent()) return l_false; if (check_inconsistent()) return l_false;
@ -3249,10 +3120,10 @@ namespace sat {
if (asms.empty()) { if (asms.empty()) {
bool_var v = mk_var(true, false); bool_var v = mk_var(true, false);
literal lit(v, false); literal lit(v, false);
init_assumptions(1, &lit, 0, 0); init_assumptions(1, &lit);
} }
else { else {
init_assumptions(asms.size(), asms.c_ptr(), 0, 0); init_assumptions(asms.size(), asms.c_ptr());
} }
propagate(false); propagate(false);
if (check_inconsistent()) return l_false; if (check_inconsistent()) return l_false;

16
src/sat/sat_solver.h
View file

@ -33,7 +33,6 @@ Revision History:
#include"sat_iff3_finder.h" #include"sat_iff3_finder.h"
#include"sat_probing.h" #include"sat_probing.h"
#include"sat_mus.h" #include"sat_mus.h"
#include"sat_sls.h"
#include"params.h" #include"params.h"
#include"statistics.h" #include"statistics.h"
#include"stopwatch.h" #include"stopwatch.h"
@ -86,7 +85,6 @@ namespace sat {
asymm_branch m_asymm_branch; asymm_branch m_asymm_branch;
probing m_probing; probing m_probing;
mus m_mus; // MUS for minimal core extraction mus m_mus; // MUS for minimal core extraction
wsls m_wsls; // SLS facility for MaxSAT use
bool m_inconsistent; bool m_inconsistent;
// A conflict is usually a single justification. That is, a justification // A conflict is usually a single justification. That is, a justification
// for false. If m_not_l is not null_literal, then m_conflict is a // for false. If m_not_l is not null_literal, then m_conflict is a
@ -141,9 +139,6 @@ namespace sat {
friend class probing; friend class probing;
friend class iff3_finder; friend class iff3_finder;
friend class mus; friend class mus;
friend class sls;
friend class wsls;
friend class bceq;
friend struct mk_stat; friend struct mk_stat;
public: public:
solver(params_ref const & p, reslimit& l, extension * ext); solver(params_ref const & p, reslimit& l, extension * ext);
@ -280,10 +275,7 @@ namespace sat {
// //
// ----------------------- // -----------------------
public: public:
lbool check(unsigned num_lits = 0, literal const* lits = 0) { lbool check(unsigned num_lits = 0, literal const* lits = 0);
return check(num_lits, lits, 0, 0);
}
lbool check(unsigned num_lits, literal const* lits, double const* weights, double max_weight);
model const & get_model() const { return m_model; } model const & get_model() const { return m_model; }
bool model_is_current() const { return m_model_is_current; } bool model_is_current() const { return m_model_is_current; }
@ -311,11 +303,7 @@ namespace sat {
literal_vector m_min_core; literal_vector m_min_core;
bool m_min_core_valid; bool m_min_core_valid;
literal_vector m_blocker; void init_assumptions(unsigned num_lits, literal const* lits);
double m_weight;
bool m_initializing_preferred;
void init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight);
bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight);
void reassert_min_core(); void reassert_min_core();
void update_min_core(); void update_min_core();
void resolve_weighted(); void resolve_weighted();

29
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -105,13 +105,8 @@ public:
virtual void set_progress_callback(progress_callback * callback) {} virtual void set_progress_callback(progress_callback * callback) {}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
return check_sat(num_assumptions, assumptions, 0, 0);
}
void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) { void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
m_weights.reset();
if (weights != 0) { if (weights != 0) {
for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]); for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);
} }
@ -131,15 +126,11 @@ public:
for (unsigned i = 0; i < m_asms.size(); ++i) { for (unsigned i = 0; i < m_asms.size(); ++i) {
nweights.push_back((unsigned) m_weights[i]); nweights.push_back((unsigned) m_weights[i]);
} }
m_weights.reset();
m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr()); m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr());
} }
lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) { virtual lbool check_sat(unsigned sz, expr * const * assumptions) {
m_weights.reset();
if (weights != 0) {
m_weights.append(sz, weights);
}
SASSERT(m_weights.empty() == (m_weights.c_ptr() == 0));
m_solver.pop_to_base_level(); m_solver.pop_to_base_level();
dep2asm_t dep2asm; dep2asm_t dep2asm;
m_model = 0; m_model = 0;
@ -148,10 +139,10 @@ public:
r = internalize_assumptions(sz, assumptions, dep2asm); r = internalize_assumptions(sz, assumptions, dep2asm);
if (r != l_true) return r; if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight); r = m_solver.check(m_asms.size(), m_asms.c_ptr());
switch (r) { switch (r) {
case l_true: case l_true:
if (sz > 0 && !weights) { if (sz > 0) {
check_assumptions(dep2asm); check_assumptions(dep2asm);
} }
break; break;
@ -675,18 +666,6 @@ solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p) {
} }
lbool inc_sat_check_sat(solver& _s, unsigned sz, expr*const* soft, rational const* _weights, rational const& max_weight) {
inc_sat_solver& s = dynamic_cast<inc_sat_solver&>(_s);
vector<double> weights;
for (unsigned i = 0; _weights && i < sz; ++i) {
weights.push_back(_weights[i].get_double());
}
params_ref p;
p.set_bool("minimize_core", false);
s.updt_params(p);
return s.check_sat(sz, soft, weights.c_ptr(), max_weight.get_double());
}
void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* soft, rational const* _weights) { void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* soft, rational const* _weights) {
inc_sat_solver& s = dynamic_cast<inc_sat_solver&>(_s); inc_sat_solver& s = dynamic_cast<inc_sat_solver&>(_s);
vector<unsigned> weights; vector<unsigned> weights;

1
src/sat/sat_solver/inc_sat_solver.h
View file

@ -24,7 +24,6 @@ Notes:
solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p); solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p);
lbool inc_sat_check_sat(solver& s, unsigned sz, expr*const* soft, rational const* weights, rational const& max_weight);
void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights); void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights);