Skip to content

Commit

Permalink
wip - local search for euf/arithmetic
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Feb 11, 2023
1 parent 46c8d78 commit 7bef2f3
Show file tree
Hide file tree
Showing 9 changed files with 716 additions and 172 deletions.
38 changes: 15 additions & 23 deletions src/sat/sat_ddfw.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ namespace sat {
else if (should_parallel_sync()) do_parallel_sync();
else shift_weights();
}
remove_assumptions();
log();
return m_min_sz == 0 ? l_true : l_undef;
}
Expand Down Expand Up @@ -244,7 +245,6 @@ namespace sat {
m_use_list_index.push_back(m_flat_use_list.size());
}


void ddfw::flip(bool_var v) {
++m_flips;
literal lit = literal(v, !value(v));
Expand Down Expand Up @@ -309,19 +309,15 @@ namespace sat {
log();

if (m_reinit_count % 2 == 0) {
for (auto& ci : m_clauses) {
ci.m_weight += 1;
}
for (auto& ci : m_clauses)
ci.m_weight += 1;
}
else {
for (auto& ci : m_clauses) {
if (ci.is_true()) {
ci.m_weight = m_config.m_init_clause_weight;
}
else {
ci.m_weight = m_config.m_init_clause_weight + 1;
}
}
for (auto& ci : m_clauses)
if (ci.is_true())
ci.m_weight = m_config.m_init_clause_weight;
else
ci.m_weight = m_config.m_init_clause_weight + 1;
}
init_clause_data();
++m_reinit_count;
Expand All @@ -341,11 +337,9 @@ namespace sat {
clause const& c = get_clause(i);
ci.m_trues = 0;
ci.m_num_trues = 0;
for (literal lit : c) {
if (is_true(lit)) {
ci.add(lit);
}
}
for (literal lit : c)
if (is_true(lit))
ci.add(lit);
switch (ci.m_num_trues) {
case 0:
for (literal lit : c) {
Expand Down Expand Up @@ -384,12 +378,10 @@ namespace sat {
void ddfw::reinit_values() {
for (unsigned i = 0; i < num_vars(); ++i) {
int b = bias(i);
if (0 == (m_rand() % (1 + abs(b)))) {
value(i) = (m_rand() % 2) == 0;
}
else {
value(i) = bias(i) > 0;
}
if (0 == (m_rand() % (1 + abs(b))))
value(i) = (m_rand() % 2) == 0;
else
value(i) = bias(i) > 0;
}
}

Expand Down
26 changes: 16 additions & 10 deletions src/sat/sat_ddfw.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,17 @@ namespace sat {
void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); }
};

class use_list {
ddfw& p;
unsigned i;
public:
use_list(ddfw& p, literal lit) :
p(p), i(lit.index()) {}
unsigned const* begin() { return p.m_flat_use_list.data() + p.m_use_list_index[i]; }
unsigned const* end() { return p.m_flat_use_list.data() + p.m_use_list_index[i + 1]; }
};

protected:

struct config {
Expand Down Expand Up @@ -102,15 +113,7 @@ namespace sat {

parallel* m_par;

class use_list {
ddfw& p;
unsigned i;
public:
use_list(ddfw& p, literal lit):
p(p), i(lit.index()) {}
unsigned const* begin() { return p.m_flat_use_list.data() + p.m_use_list_index[i]; }
unsigned const* end() { return p.m_flat_use_list.data() + p.m_use_list_index[i + 1]; }
};


void flatten_use_list();

Expand Down Expand Up @@ -163,7 +166,6 @@ namespace sat {
// flip activity
bool do_flip();
bool_var pick_var();
void flip(bool_var v);
void save_best_values();
void save_model();
void save_priorities();
Expand Down Expand Up @@ -245,6 +247,10 @@ namespace sat {

void remove_assumptions();

void flip(bool_var v);

use_list get_use_list(literal lit) { return use_list(*this, lit); }

};
}

17 changes: 6 additions & 11 deletions src/sat/sat_local_search.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -353,10 +353,7 @@ namespace sat {
DEBUG_CODE(verify_unsat_stack(););
}

local_search::local_search() :
m_is_unsat(false),
m_initializing(false),
m_par(nullptr) {
local_search::local_search() {
}

void local_search::reinit(solver& s, bool_vector const& phase) {
Expand All @@ -375,11 +372,10 @@ namespace sat {
m_vars.reserve(s.num_vars());
m_config.set_config(s.get_config());

if (m_config.phase_sticky()) {
unsigned v = 0;
unsigned v = 0;
if (m_config.phase_sticky())
for (var_info& vi : m_vars)
vi.m_bias = s.m_phase[v++] ? 98 : 2;
}
vi.m_bias = s.m_phase[v++] ? 98 : 2;

// copy units
unsigned trail_sz = s.init_trail_size();
Expand Down Expand Up @@ -419,9 +415,8 @@ namespace sat {
if (ext && (!ext->is_pb() || !ext->extract_pb(card, pb)))
throw default_exception("local search is incomplete with extensions beyond PB");

if (_init) {
init();
}
if (_init)
init();
}

local_search::~local_search() {
Expand Down
16 changes: 8 additions & 8 deletions src/sat/sat_local_search.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,21 +133,21 @@ namespace sat {
vector<constraint> m_constraints; // all constraints
literal_vector m_assumptions; // temporary assumptions
literal_vector m_prop_queue; // propagation queue
unsigned m_num_non_binary_clauses;
bool m_is_pb;
bool m_is_unsat;
unsigned m_num_non_binary_clauses = 0;
bool m_is_pb = false;
bool m_is_unsat = false;
unsigned_vector m_unsat_stack; // store all the unsat constraints
unsigned_vector m_index_in_unsat_stack; // which position is a constraint in the unsat_stack

// configuration changed decreasing variables (score>0 and conf_change==true)
bool_var_vector m_goodvar_stack;
bool m_initializing;
bool m_initializing = false;


// information about solution
unsigned m_best_unsat;
double m_best_unsat_rate;
double m_last_best_unsat_rate;
unsigned m_best_unsat = 0;
double m_best_unsat_rate = 0;
double m_last_best_unsat_rate = 0;
// for non-known instance, set as maximal
int m_best_known_value = INT_MAX; // best known value for this instance

Expand All @@ -159,7 +159,7 @@ namespace sat {

reslimit m_limit;
random_gen m_rand;
parallel* m_par;
parallel* m_par = nullptr;
model m_model;

inline int score(bool_var v) const { return m_vars[v].m_score; }
Expand Down
2 changes: 1 addition & 1 deletion src/sat/smt/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ z3_add_component(sat_smt
arith_axioms.cpp
arith_diagnostics.cpp
arith_internalize.cpp
arith_local_search.cpp
arith_sls.cpp
arith_solver.cpp
array_axioms.cpp
array_diagnostics.cpp
Expand Down
Loading

0 comments on commit 7bef2f3

Please sign in to comment.