Skip to content

Commit

Permalink
re-add pb extraction
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <[email protected]>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Aug 26, 2020
1 parent 9c77fbc commit 526d76b
Show file tree
Hide file tree
Showing 7 changed files with 118 additions and 94 deletions.
3 changes: 1 addition & 2 deletions src/ast/rewriter/seq_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,7 @@ Module Name:
Nikolaj Bjorner (nbjorner) 2015-12-5
Murphy Berzish 2017-02-21
Notes:
Caleb Stanford 2020-07-07
--*/

Expand Down
85 changes: 85 additions & 0 deletions src/sat/ba/ba_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5052,6 +5052,91 @@ namespace sat {
return ok;
}

bool ba_solver::extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& add_cardinality,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& add_pb) {

unsigned_vector coeffs;
literal_vector lits;
for (constraint* cp : m_constraints) {
switch (cp->tag()) {
case card_t: {
card const& c = cp->to_card();
unsigned n = c.size();
unsigned k = c.k();

if (c.lit() == null_literal) {
// c.lits() >= k
// <=>
// ~c.lits() <= n - k
lits.reset();
for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]);
add_cardinality(lits.size(), lits.c_ptr(), n - k);
}
else {
//
// c.lit() <=> c.lits() >= k
//
// (c.lits() < k) or c.lit()
// = (c.lits() + (n - k + 1)*~c.lit()) <= n
//
// ~c.lit() or (c.lits() >= k)
// = ~c.lit() or (~c.lits() <= n - k)
// = k*c.lit() + ~c.lits() <= n
//
lits.reset();
coeffs.reset();
for (literal l : c) lits.push_back(l), coeffs.push_back(1);
lits.push_back(~c.lit()); coeffs.push_back(n - k + 1);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);

lits.reset();
coeffs.reset();
for (literal l : c) lits.push_back(~l), coeffs.push_back(1);
lits.push_back(c.lit()); coeffs.push_back(k);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);
}
break;
}
case ba_solver::pb_t: {
ba_solver::pb const& p = cp->to_pb();
lits.reset();
coeffs.reset();
unsigned sum = 0;
for (ba_solver::wliteral wl : p) sum += wl.first;

if (p.lit() == null_literal) {
// w1 + .. + w_n >= k
// <=>
// ~wl + ... + ~w_n <= sum_of_weights - k
for (ba_solver::wliteral wl : p) lits.push_back(~(wl.second)), coeffs.push_back(wl.first);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), sum - p.k());
}
else {
// lit <=> w1 + .. + w_n >= k
// <=>
// lit or w1 + .. + w_n <= k - 1
// ~lit or w1 + .. + w_n >= k
// <=>
// (sum - k + 1)*~lit + w1 + .. + w_n <= sum
// k*lit + ~wl + ... + ~w_n <= sum
lits.push_back(p.lit()), coeffs.push_back(p.k());
for (ba_solver::wliteral wl : p) lits.push_back(~(wl.second)), coeffs.push_back(wl.first);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), sum);

lits.reset();
coeffs.reset();
lits.push_back(~p.lit()), coeffs.push_back(sum + 1 - p.k());
for (ba_solver::wliteral wl : p) lits.push_back(wl.second), coeffs.push_back(wl.first);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), sum);
}
break;
}
case ba_solver::xr_t:
return false;
}
}
return true;
}

};

Expand Down
3 changes: 3 additions & 0 deletions src/sat/ba/ba_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -579,6 +579,9 @@ namespace sat {

bool validate() override;

bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& add_cardinlaity,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& add_pb) override;


};

Expand Down
11 changes: 10 additions & 1 deletion src/sat/euf/euf_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -418,5 +418,14 @@ namespace euf {
NOT_IMPLEMENTED_YET();
return nullptr;
}


bool solver::extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {
if (m_true)
return false;
for (auto* e : m_extensions)
if (!e->extract_pb(card, pb))
return false;
return true;
}
}
4 changes: 4 additions & 0 deletions src/sat/euf/euf_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,10 @@ namespace euf {
bool check_model(sat::model const& m) const override;
unsigned max_var(unsigned w) const override;

bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;


sat::literal internalize(sat::sat_internalizer& si, expr* e, bool sign, bool root) override;
model_converter* get_model();

Expand Down
6 changes: 6 additions & 0 deletions src/sat/sat_extension.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Revision History:
--*/
#pragma once

#include <functional>
#include "sat/sat_types.h"
#include "util/params.h"
#include "util/statistics.h"
Expand Down Expand Up @@ -83,6 +84,11 @@ namespace sat {
virtual bool is_blocked(literal l, ext_constraint_idx) = 0;
virtual bool check_model(model const& m) const = 0;
virtual unsigned max_var(unsigned w) const = 0;

virtual bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {
return true;
}
};

};
Expand Down
100 changes: 9 additions & 91 deletions src/sat/sat_local_search.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -322,6 +322,7 @@ namespace sat {
add_unit(~c[0], null_literal);
return;
}
m_is_pb = true;
unsigned id = m_constraints.size();
m_constraints.push_back(constraint(k, id));
for (unsigned i = 0; i < sz; ++i) {
Expand Down Expand Up @@ -414,99 +415,16 @@ namespace sat {
}
m_num_non_binary_clauses = s.m_clauses.size();

if (s.get_extension())
throw default_exception("local search is incompatible with extensions");

#if 0
// copy cardinality clauses
ba_solver* ext = dynamic_cast<ba_solver*>(s.get_extension());
if (ext) {
unsigned_vector coeffs;
literal_vector lits;
for (ba_solver::constraint* cp : ext->m_constraints) {
switch (cp->tag()) {
case ba_solver::card_t: {
ba_solver::card const& c = cp->to_card();
unsigned n = c.size();
unsigned k = c.k();

if (c.lit() == null_literal) {
// c.lits() >= k
// <=>
// ~c.lits() <= n - k
lits.reset();
for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]);
add_cardinality(lits.size(), lits.c_ptr(), n - k);
}
else {
//
// c.lit() <=> c.lits() >= k
//
// (c.lits() < k) or c.lit()
// = (c.lits() + (n - k + 1)*~c.lit()) <= n
//
// ~c.lit() or (c.lits() >= k)
// = ~c.lit() or (~c.lits() <= n - k)
// = k*c.lit() + ~c.lits() <= n
//
m_is_pb = true;
lits.reset();
coeffs.reset();
for (literal l : c) lits.push_back(l), coeffs.push_back(1);
lits.push_back(~c.lit()); coeffs.push_back(n - k + 1);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);

lits.reset();
coeffs.reset();
for (literal l : c) lits.push_back(~l), coeffs.push_back(1);
lits.push_back(c.lit()); coeffs.push_back(k);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);
}
break;
}
case ba_solver::pb_t: {
ba_solver::pb const& p = cp->to_pb();
lits.reset();
coeffs.reset();
m_is_pb = true;
unsigned sum = 0;
for (ba_solver::wliteral wl : p) sum += wl.first;

if (p.lit() == null_literal) {
// w1 + .. + w_n >= k
// <=>
// ~wl + ... + ~w_n <= sum_of_weights - k
for (ba_solver::wliteral wl : p) lits.push_back(~(wl.second)), coeffs.push_back(wl.first);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), sum - p.k());
}
else {
// lit <=> w1 + .. + w_n >= k
// <=>
// lit or w1 + .. + w_n <= k - 1
// ~lit or w1 + .. + w_n >= k
// <=>
// (sum - k + 1)*~lit + w1 + .. + w_n <= sum
// k*lit + ~wl + ... + ~w_n <= sum
lits.push_back(p.lit()), coeffs.push_back(p.k());
for (ba_solver::wliteral wl : p) lits.push_back(~(wl.second)), coeffs.push_back(wl.first);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), sum);

lits.reset();
coeffs.reset();
lits.push_back(~p.lit()), coeffs.push_back(sum + 1 - p.k());
for (ba_solver::wliteral wl : p) lits.push_back(wl.second), coeffs.push_back(wl.first);
add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), sum);
}
break;
}
case ba_solver::xr_t:
throw default_exception("local search is incompatible with enabling xor solving");
break;
}
}
}
#endif

extension* ext = s.get_extension();
std::function<void(unsigned, literal const*, unsigned)> card =
[&](unsigned sz, literal const* c, unsigned k) { add_cardinality(sz, c, k); };
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)> pb =
[&](unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { add_pb(sz, c, coeffs, k); };
if (ext && !ext->extract_pb(card, pb))
throw default_exception("local search is incomplete with extensions beyond PB");

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

0 comments on commit 526d76b

Please sign in to comment.