mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

constraint id

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-14 16:27:22 -07:00
parent 5c6cef4735
commit c1c0f776fb
2 changed files with 60 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

83
src/sat/sat_local_search.cpp
View file

@ -50,7 +50,7 @@ namespace sat {
var_info& vi = m_vars[v]; var_info& vi = m_vars[v];
for (unsigned k = 0; k < 2; pol = !pol, k++) { for (unsigned k = 0; k < 2; pol = !pol, k++) {
for (unsigned i = 0; i < m_vars[v].m_watch[pol].size(); ++i) { for (unsigned i = 0; i < m_vars[v].m_watch[pol].size(); ++i) {
constraint const& c = m_constraints[m_vars[v].m_watch[pol][i]]; constraint const& c = m_constraints[m_vars[v].m_watch[pol][i].m_constraint_id];
for (unsigned j = 0; j < c.size(); ++j) { for (unsigned j = 0; j < c.size(); ++j) {
bool_var w = c[j].var(); bool_var w = c[j].var();
if (w == v || is_neighbor.contains(w)) continue; if (w == v || is_neighbor.contains(w)) continue;
@ -97,10 +97,11 @@ namespace sat {
void local_search::init_scores() { void local_search::init_scores() {
for (unsigned v = 0; v < num_vars(); ++v) { for (unsigned v = 0; v < num_vars(); ++v) {
bool is_true = cur_solution(v); bool is_true = cur_solution(v);
int_vector& truep = m_vars[v].m_watch[is_true]; coeff_vector& truep = m_vars[v].m_watch[is_true];
int_vector& falsep = m_vars[v].m_watch[!is_true]; coeff_vector& falsep = m_vars[v].m_watch[!is_true];
for (unsigned i = 0; i < falsep.size(); ++i) { for (unsigned i = 0; i < falsep.size(); ++i) {
constraint& c = m_constraints[falsep[i]]; constraint& c = m_constraints[falsep[i].m_constraint_id];
SASSERT(falsep[i].m_coeff == 1);
// will --slack // will --slack
if (c.m_slack <= 0) { if (c.m_slack <= 0) {
dec_slack_score(v); dec_slack_score(v);
@ -109,7 +110,8 @@ namespace sat {
} }
} }
for (unsigned i = 0; i < truep.size(); ++i) { for (unsigned i = 0; i < truep.size(); ++i) {
constraint& c = m_constraints[truep[i]]; SASSERT(truep[i].m_coeff == 1);
constraint& c = m_constraints[truep[i].m_constraint_id];
// will --true_terms_count[c] // will --true_terms_count[c]
// will ++slack // will ++slack
if (c.m_slack <= -1) { if (c.m_slack <= -1) {
@ -230,8 +232,8 @@ namespace sat {
m_constraints.push_back(constraint(k)); m_constraints.push_back(constraint(k));
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
m_vars.reserve(c[i].var() + 1); m_vars.reserve(c[i].var() + 1);
literal t(~c[i]); literal t(~c[i]);
m_vars[t.var()].m_watch[is_pos(t)].push_back(id); m_vars[t.var()].m_watch[is_pos(t)].push_back(pbcoeff(id, 1));
m_constraints.back().push(t); m_constraints.back().push(t);
} }
if (sz == 1 && k == 0) { if (sz == 1 && k == 0) {
@ -239,6 +241,20 @@ namespace sat {
} }
} }
void local_search::add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) {
unsigned id = m_constraints.size();
m_constraints.push_back(constraint(k));
for (unsigned i = 0; i < sz; ++i) {
m_vars.reserve(c[i].var() + 1);
literal t(~c[i]);
m_vars[t.var()].m_watch[is_pos(t)].push_back(pbcoeff(id, coeffs[i]));
m_constraints.back().push(t); // add coefficient to constraint?
}
if (sz == 1 && k == 0) {
m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100;
}
}
local_search::local_search() : local_search::local_search() :
m_par(0) { m_par(0) {
} }
@ -289,6 +305,7 @@ namespace sat {
if (ext) { if (ext) {
literal_vector lits; literal_vector lits;
unsigned sz = ext->m_cards.size(); unsigned sz = ext->m_cards.size();
unsigned_vector coeffs;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
card_extension::card& c = *ext->m_cards[i]; card_extension::card& c = *ext->m_cards[i];
unsigned n = c.size(); unsigned n = c.size();
@ -303,27 +320,27 @@ namespace sat {
add_cardinality(lits.size(), lits.c_ptr(), n - k); add_cardinality(lits.size(), lits.c_ptr(), n - k);
} }
else { else {
// TBD: this doesn't really work because scores are not properly updated for general PB constraints.
NOT_IMPLEMENTED_YET();
// //
// c.lit() <=> c.lits() >= k // c.lit() <=> c.lits() >= k
// //
// (c.lits() < k) or c.lit() // (c.lits() < k) or c.lit()
// = (c.lits() + (n - k - 1)*~c.lit()) <= n // = (c.lits() + (n - k + 1)*~c.lit()) <= n
// //
// ~c.lit() or (c.lits() >= k) // ~c.lit() or (c.lits() >= k)
// = ~c.lit() or (~c.lits() <= n - k) // = ~c.lit() or (~c.lits() <= n - k)
// = k*c.lit() + ~c.lits() <= n // = k*c.lit() + ~c.lits() <= n
// //
lits.reset(); lits.reset();
for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]); coeffs.reset();
for (unsigned j = 0; j < n - k - 1; ++j) lits.push_back(~c.lit()); for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]), coeffs.push_back(1);
add_cardinality(lits.size(), lits.c_ptr(), n); lits.push_back(~c.lit()); coeffs.push_back(n - k + 1);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);
lits.reset(); lits.reset();
for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]); coeffs.reset();
for (unsigned j = 0; j < k; ++j) lits.push_back(c.lit()); for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]), coeffs.push_back(1);
add_cardinality(lits.size(), lits.c_ptr(), n); lits.push_back(c.lit()); coeffs.push_back(k);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);
} }
} }
// //
@ -474,10 +491,10 @@ namespace sat {
l = *cit; l = *cit;
best_var = v = l.var(); best_var = v = l.var();
bool tt = cur_solution(v); bool tt = cur_solution(v);
int_vector const& falsep = m_vars[v].m_watch[!tt]; coeff_vector const& falsep = m_vars[v].m_watch[!tt];
int_vector::const_iterator it = falsep.begin(), end = falsep.end(); coeff_vector::const_iterator it = falsep.begin(), end = falsep.end();
for (; it != end; ++it) { for (; it != end; ++it) {
int slack = constraint_slack(*it); int slack = constraint_slack(it->m_constraint_id);
if (slack < 0) if (slack < 0)
++best_bsb; ++best_bsb;
else if (slack == 0) else if (slack == 0)
@ -489,10 +506,10 @@ namespace sat {
if (is_true(l)) { if (is_true(l)) {
v = l.var(); v = l.var();
unsigned bsb = 0; unsigned bsb = 0;
int_vector const& falsep = m_vars[v].m_watch[!cur_solution(v)]; coeff_vector const& falsep = m_vars[v].m_watch[!cur_solution(v)];
int_vector::const_iterator it = falsep.begin(), end = falsep.end(); coeff_vector::const_iterator it = falsep.begin(), end = falsep.end();
for (; it != end; ++it) { for (; it != end; ++it) {
int slack = constraint_slack(*it); int slack = constraint_slack(it->m_constraint_id);
if (slack < 0) { if (slack < 0) {
if (bsb == best_bsb) { if (bsb == best_bsb) {
break; break;
@ -541,12 +558,12 @@ namespace sat {
m_vars[flipvar].m_value = !cur_solution(flipvar); m_vars[flipvar].m_value = !cur_solution(flipvar);
bool flip_is_true = cur_solution(flipvar); bool flip_is_true = cur_solution(flipvar);
int_vector const& truep = m_vars[flipvar].m_watch[flip_is_true]; coeff_vector const& truep = m_vars[flipvar].m_watch[flip_is_true];
int_vector const& falsep = m_vars[flipvar].m_watch[!flip_is_true]; coeff_vector const& falsep = m_vars[flipvar].m_watch[!flip_is_true];
int_vector::const_iterator it = truep.begin(), end = truep.end(); coeff_vector::const_iterator it = truep.begin(), end = truep.end();
for (; it != end; ++it) { for (; it != end; ++it) {
unsigned ci = *it; unsigned ci = it->m_constraint_id;
constraint& c = m_constraints[ci]; constraint& c = m_constraints[ci];
--c.m_slack; --c.m_slack;
if (c.m_slack == -1) { // from 0 to -1: sat -> unsat if (c.m_slack == -1) { // from 0 to -1: sat -> unsat
@ -555,7 +572,7 @@ namespace sat {
} }
it = falsep.begin(), end = falsep.end(); it = falsep.begin(), end = falsep.end();
for (; it != end; ++it) { for (; it != end; ++it) {
unsigned ci = *it; unsigned ci = it->m_constraint_id;
constraint& c = m_constraints[ci]; constraint& c = m_constraints[ci];
++c.m_slack; ++c.m_slack;
if (c.m_slack == 0) { // from -1 to 0: unsat -> sat if (c.m_slack == 0) { // from -1 to 0: unsat -> sat
@ -576,12 +593,12 @@ namespace sat {
int org_flipvar_slack_score = slack_score(flipvar); int org_flipvar_slack_score = slack_score(flipvar);
bool flip_is_true = cur_solution(flipvar); bool flip_is_true = cur_solution(flipvar);
int_vector& truep = m_vars[flipvar].m_watch[flip_is_true]; coeff_vector& truep = m_vars[flipvar].m_watch[flip_is_true];
int_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true]; coeff_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true];
// update related clauses and neighbor vars // update related clauses and neighbor vars
for (unsigned i = 0; i < truep.size(); ++i) { for (unsigned i = 0; i < truep.size(); ++i) {
constraint & c = m_constraints[truep[i]]; constraint & c = m_constraints[truep[i].m_constraint_id];
//++true_terms_count[c]; //++true_terms_count[c];
--c.m_slack; --c.m_slack;
switch (c.m_slack) { switch (c.m_slack) {
@ -605,7 +622,7 @@ namespace sat {
if (is_true(c[j])) if (is_true(c[j]))
inc_slack_score(v); inc_slack_score(v);
} }
unsat(truep[i]); unsat(truep[i].m_constraint_id);
break; break;
case 0: // from 1 to 0 case 0: // from 1 to 0
for (unsigned j = 0; j < c.size(); ++j) { for (unsigned j = 0; j < c.size(); ++j) {
@ -623,7 +640,7 @@ namespace sat {
} }
} }
for (unsigned i = 0; i < falsep.size(); ++i) { for (unsigned i = 0; i < falsep.size(); ++i) {
constraint& c = m_constraints[falsep[i]]; constraint& c = m_constraints[falsep[i].m_constraint_id];
//--true_terms_count[c]; //--true_terms_count[c];
++c.m_slack; ++c.m_slack;
switch (c.m_slack) { switch (c.m_slack) {
@ -648,7 +665,7 @@ namespace sat {
if (is_true(c[j])) if (is_true(c[j]))
dec_slack_score(v); dec_slack_score(v);
} }
sat(falsep[i]); sat(falsep[i].m_constraint_id);
break; break;
case -1: // from -2 to -1 case -1: // from -2 to -1
for (unsigned j = 0; j < c.size(); ++j) { for (unsigned j = 0; j < c.size(); ++j) {

11
src/sat/sat_local_search.h
View file

@ -59,7 +59,14 @@ namespace sat {
class local_search { class local_search {
struct pbcoeff {
unsigned m_constraint_id;
unsigned m_coeff;
pbcoeff(unsigned id, unsigned coeff):
m_constraint_id(id), m_coeff(coeff) {}
};
typedef svector<bool> bool_vector; typedef svector<bool> bool_vector;
typedef svector<pbcoeff> coeff_vector;
// data structure for a term in objective function // data structure for a term in objective function
struct ob_term { struct ob_term {
@ -79,7 +86,7 @@ namespace sat {
int m_time_stamp; // the flip time stamp int m_time_stamp; // the flip time stamp
int m_cscc; // how many times its constraint state configure changes since its last flip int m_cscc; // how many times its constraint state configure changes since its last flip
bool_var_vector m_neighbors; // neighborhood variables bool_var_vector m_neighbors; // neighborhood variables
int_vector m_watch[2]; coeff_vector m_watch[2];
var_info(): var_info():
m_value(true), m_value(true),
m_bias(50), m_bias(50),
@ -241,6 +248,8 @@ namespace sat {
void add_soft(bool_var v, int weight); void add_soft(bool_var v, int weight);
void add_cardinality(unsigned sz, literal const* c, unsigned k); void add_cardinality(unsigned sz, literal const* c, unsigned k);
void add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k);
lbool check(); lbool check();