mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

add sls

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-12 19:24:31 -07:00
parent 1652c16163
commit 180b0d4ec9
8 changed files with 252 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/opt/pb_sls.cpp
View file

@ -20,49 +20,11 @@ Notes:
#include "smt_literal.h"
#include "ast_pp.h"
#include "th_rewriter.h"
#include "sat_sls.h"
namespace smt {
struct pb_sls::imp {
struct index_set {
unsigned_vector m_elems;
unsigned_vector m_index;
unsigned num_elems() const { return m_elems.size(); }
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 clause {
literal_vector m_lits;
scoped_mpz_vector m_weights;
@ -112,8 +74,8 @@ namespace smt {
expr_ref_vector m_trail;
obj_map<expr, unsigned> m_decl2var; // map declarations to Boolean variables.
ptr_vector<expr> m_var2decl; // reverse map
index_set m_hard_false; // list of hard clauses that are false.
index_set m_soft_false; // list of soft clauses that are false.
sat::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.
unsigned m_max_flips; // maximal number of flips
unsigned m_non_greedy_percent; // percent of moves to do non-greedy style
random_gen m_rng;

60
src/sat/sat_mus.cpp
View file

@ -36,6 +36,7 @@ namespace sat {
m_core.append(m_mus);
s.m_core.reset();
s.m_core.append(m_core);
m_model.reset();
}
lbool mus::operator()() {
@ -46,11 +47,12 @@ namespace sat {
literal_vector& core = m_core;
literal_vector& mus = m_mus;
core.append(s.get_core());
while (!core.empty()) {
TRACE("sat",
tout << "core: " << core << "\n";
tout << "mus: " << mus << "\n";);
tout << "mus: " << mus << "\n";);
if (s.m_cancel) {
set_core();
@ -59,7 +61,7 @@ namespace sat {
literal lit = core.back();
core.pop_back();
unsigned sz = mus.size();
//mus.push_back(~lit); // TBD: measure
mus.push_back(~lit); // TBD: measure
mus.append(core);
lbool is_sat = s.check(mus.size(), mus.c_ptr());
mus.resize(sz);
@ -76,9 +78,9 @@ namespace sat {
}
sz = core.size();
core.append(mus);
rmr();
measure_mr();
// rmr();
core.resize(sz);
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << mus << " " << core << ")\n";);
break;
}
case l_false:
@ -86,7 +88,6 @@ namespace sat {
if (new_core.contains(~lit)) {
break;
}
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << new_core << ")\n";);
core.reset();
for (unsigned i = 0; i < new_core.size(); ++i) {
literal lit = new_core[i];
@ -99,9 +100,27 @@ namespace sat {
}
TRACE("sat", tout << "new core: " << mus << "\n";);
set_core();
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << m_core << ")\n";);
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);
}
//
// TBD: eager model rotation allows rotating the same clause
// several times with respect to different models.
//
void mus::rmr() {
model& model = s.m_model;
literal lit = m_mus.back();
@ -146,16 +165,33 @@ namespace sat {
watch_list const& wlist = s.get_wlist(lit);
watch_list::const_iterator it = wlist.begin();
watch_list::const_iterator end = wlist.end();
for (; it != end; ++it) {
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();
TRACE("sat", tout << ~lit << " " << lit2 << " " << lit3 << "\n";);
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();
@ -163,15 +199,23 @@ namespace sat {
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";);
m_toswap.resize(sz);
return;
}
}
if (num_cand > 1) {
m_toswap.resize(sz);
}
else {
IF_VERBOSE(1, verbose_stream() << "wlist size: " << num_cand << " " << m_core.size() << "\n";);
}
}
}

3
src/sat/sat_mus.h
View file

@ -24,6 +24,8 @@ namespace sat {
literal_vector m_core;
literal_vector m_mus;
literal_vector m_toswap;
model m_model;
solver& s;
public:
mus(solver& s);
@ -32,6 +34,7 @@ namespace sat {
private:
lbool mus2();
void rmr();
void measure_mr();
bool has_single_unsat(literal& assumption_lit);
void find_swappable(literal lit);
void reset();

96
src/sat/sat_sls.cpp Normal file
View file

@ -0,0 +1,96 @@
/*++
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"
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) {
}
sls::~sls() {
}
#if 0
bool_var sls::pick_flip() {
unsigned clause_idx = m_false.choose(m_rand);
clause const& c = m_clauses[clause_idx];
unsigned result = UINT_MAX;
m_min_vars.reset();
for (unsigned i = 0; i < c.size(); ++i) {
}
}
void sls::flip(bool_var v) {
}
bool sls::local_search() {
for (unsigned i = 0; !m_false.empty() && i < m_max_flips; ++i) {
flip(pick_flip());
}
return m_false.empty();
}
#endif
lbool sls::operator()() {
#if 0
for (unsigned i = 0; i < m_max_tries; ++i) {
if (local_search()) {
return l_true;
}
}
#endif
return l_undef;
}
};

60
src/sat/sat_sls.h Normal file
View file

@ -0,0 +1,60 @@
/*++
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(); }
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 {
solver& s;
random_gen m_rand;
unsigned m_max_tries;
unsigned m_max_flips;
index_set m_false;
use_list m_use_list;
vector<clause> m_clauses;
public:
sls(solver& s);
~sls();
lbool operator()();
private:
bool local_search();
bool_var pick_flip();
void flip(bool_var v);
};
};
#endif

8
src/sat/sat_solver.cpp
View file

@ -48,6 +48,8 @@ namespace sat {
m_scope_lvl(0),
m_params(p) {
m_config.updt_params(p);
m_conflicts_since_gc = 0;
m_next_simplify = 0;
}
solver::~solver() {
@ -924,10 +926,8 @@ namespace sat {
m_conflicts_since_restart = 0;
m_restart_threshold = m_config.m_restart_initial;
m_luby_idx = 1;
m_conflicts_since_gc = 0;
m_gc_threshold = m_config.m_gc_initial;
m_min_d_tk = 1.0;
m_next_simplify = 0;
m_stopwatch.reset();
m_stopwatch.start();
m_core.reset();
@ -1667,6 +1667,10 @@ namespace sat {
}
reset_unmark(old_size);
if (m_config.m_minimize_core) {
// TBD:
// apply optional clause minimization by detecting subsumed literals.
// initial experiment suggests it has no effect.
m_mus(); // ignore return value on cancelation.
}
}

4
src/shell/dimacs_frontend.cpp
View file

@ -101,7 +101,7 @@ static void track_clauses(sat::solver const& src,
sat::clause * const * end = src.end_clauses();
svector<sat::solver::bin_clause> bin_clauses;
src.collect_bin_clauses(bin_clauses, false);
tracking_clauses.reserve(2*src.num_vars() + (end - it) + bin_clauses.size());
tracking_clauses.reserve(2*src.num_vars() + static_cast<unsigned>(end - it) + bin_clauses.size());
for (sat::bool_var v = 1; v < src.num_vars(); ++v) {
if (src.value(v) != l_undef) {
@ -114,7 +114,7 @@ static void track_clauses(sat::solver const& src,
for (; it != end; ++it) {
lits.reset();
sat::clause& cls = *(*it);
lits.append(cls.end()-cls.begin(), cls.begin());
lits.append(static_cast<unsigned>(cls.end()-cls.begin()), cls.begin());
track_clause(dst, lits, assumptions, tracking_clauses);
}
for (unsigned i = 0; i < bin_clauses.size(); ++i) {

30
src/test/hilbert_basis.cpp
View file

@ -540,6 +540,33 @@ static void tst19() {
saturate_basis(hb);
}
static void test_A_5_5_3() {
hilbert_basis hb;
for (unsigned i = 0; i < 15; ++i) {
vector<rational> v;
for (unsigned j = 0; j < 5; ++j) {
for (unsigned k = 0; k < 15; ++k) {
v.push_back(rational(k == i));
}
}
hb.add_ge(v, R(0));
}
for (unsigned i = 1; i <= 15; ++i) {
vector<rational> v;
for (unsigned k = 1; k <= 5; ++k) {
for (unsigned l = 1; l <= 5; ++l) {
for (unsigned j = 1; j <= 3; ++j) {
bool one = ((j*k <= i) && (((i - j) % 3) == 0); // fixme
v.push_back(rational(one));
}
}
}
hb.add_ge(v, R(0));
}
// etc.
saturate_basis(hb);
}
void tst_hilbert_basis() {
std::cout << "hilbert basis test\n";
// tst3();
@ -547,6 +574,9 @@ void tst_hilbert_basis() {
g_use_ordered_support = true;
test_A_5_5_3();
return;
tst18();
return;