Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Apr 16, 2022
1 parent 8e70112 commit 807121a
Show file tree
Hide file tree
Showing 5 changed files with 212 additions and 24 deletions.
83 changes: 83 additions & 0 deletions src/opt/maxres.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -649,6 +649,7 @@ class maxres : public maxsmt_solver_base {
}
}


void max_resolve(exprs const& core, rational const& w) {
SASSERT(!core.empty());
expr_ref fml(m), asum(m);
Expand Down Expand Up @@ -699,6 +700,88 @@ class maxres : public maxsmt_solver_base {
}
}

#if 0

void bin_max_resolve(exprs const& _core, rational const& w) {
expr_ref_vector core(m, _core.size(), _core.data());
expr_ref fml(m), cls(m);
for (unsigned i = 0; i + 1 < core.size(); ++i) {
expr* a = core.get(i);
expr* b = core.get(i + 1);
expr_ref u = mk_fresh_bool("u");
expr_ref v = mk_fresh_bool("v");
// u = a or b
// v = a and b
cls = m.mk_or(a, b);
fml = m.mk_implies(u, cls);
add(fml);
update_model(u, cls);
m_defs.push_back(fml);
cls = m.mk_and(a, b);
fml = m.mk_implies(v, cls);
add(fml);
update_model(v, cls);
m_defs.push_back(fml);
new_assumption(u, w);
core.push_back(v);
}
}

struct unfold_record {
ptr_vector<expr> ws;
rational weight;
};

void bin_delay_max_resolve(exprs const& _core, rational const& w) {
expr_ref_vector core(m, _core.size(), _core.data()), us(m), partial(m);
expr_ref fml(m), cls(m);
for (expr* c : core) {
unfold_record ws;
if (!m_unfold.find(c, ws))
continue;
for (expr* f : ws.ws)
new_assumption(f, ws.weight);
}
if (core.size() <= 1)
return;

for (expr* core)
partial.push_back(nullptr);

for (unsigned i = 0; i + 1 < core.size(); ++i) {
expr* a = core.get(i);
expr* b = core.get(i + 1);
expr_ref u = mk_fresh_bool("u");
expr_ref v = mk_fresh_bool("v");
// u = a or b
// v = a and b
cls = m.mk_or(a, b);
fml = m.mk_implies(u, cls);
add(fml);
update_model(u, cls);
m_defs.push_back(fml);
cls = m.mk_and(a, b);
fml = m.mk_implies(v, cls);
add(fml);
update_model(v, cls);
m_defs.push_back(fml);
us.push_back(u);
core.push_back(v);

unfold_record r;
r.ws.push_back(u);
if (partial.get(i))
r.ws.push_back(partia.get(i));
if (partial.get(i + 1))
r.ws.push_back(partia.get(i + 1));
partial.push_back(m.mk_and(r.ws));
m_unfold.insert(partial.back(), r);
}
expr_ref u = mk_and(us);
new_assumption(u, w);
}
#endif

// cs is a correction set (a complement of a (maximal) satisfying assignment).
void cs_max_resolve(exprs const& cs, rational const& w) {
if (cs.empty()) return;
Expand Down
86 changes: 86 additions & 0 deletions src/opt/opt_preprocess.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,93 @@ Module Name:
#pragma once

#include "opt/opt_preprocess.h"
#include "util/max_cliques.h"

namespace opt {

expr_ref_vector preprocess::propagate(expr* f, lbool& is_sat) {
expr_ref_vector asms(m);
asms.push_back(f);
is_sat = s.check_sat(asms);
return s.get_trail(1);
}

bool preprocess::prop_mutexes(vector<soft>& softs, rational& lower) {
expr_ref_vector fmls(m);
obj_map<expr, rational> new_soft = soft2map(softs, fmls);

params_ref p;
p.set_uint("max_conflicts", 1);
s.updt_params(p);

obj_hashtable<expr> pfmls, nfmls;
for (expr* f : fmls)
if (m.is_not(f, f))
nfmls.insert(f);
else
pfmls.insert(f);

u_map<expr*> ids;
unsigned_vector ps;
for (expr* f : fmls) {
ids.insert(f->get_id(), f);
ps.push_back(f->get_id());
}

u_map<uint_set> conns;

for (expr* f : fmls) {
lbool is_sat;
expr_ref_vector trail = propagate(f, is_sat);
if (is_sat == l_false) {
rational w = new_soft[f];
lower += w;
s.assert_expr(m.mk_not(f));
new_soft.remove(f);
continue;
}

expr_ref_vector mux(m);
for (expr* g : trail) {
if (m.is_not(g, g)) {
if (pfmls.contains(g))
mux.push_back(g);
}
else if (nfmls.contains(g))
mux.push_back(m.mk_not(g));
}
uint_set reach;
for (expr* g : mux)
reach.insert(g->get_id());
conns.insert(f->get_id(), reach);
}

p.set_uint("max_conflicts", UINT_MAX);
s.updt_params(p);

struct neg_literal {
unsigned negate(unsigned id) {
throw default_exception("unexpected call");
}
};
max_cliques<neg_literal> mc;
vector<unsigned_vector> mutexes;
mc.cliques(ps, conns, mutexes);

for (auto& mux : mutexes) {
expr_ref_vector _mux(m);
for (auto p : mux)
_mux.push_back(ids[p]);
process_mutex(_mux, new_soft, lower);
}

softs.reset();
for (auto const& [k, v] : new_soft)
softs.push_back(soft(expr_ref(k, m), v, false));
m_trail.reset();
return true;
}

obj_map<expr, rational> preprocess::soft2map(vector<soft> const& softs, expr_ref_vector& fmls) {
obj_map<expr, rational> new_soft;
for (soft const& sf : softs) {
Expand Down Expand Up @@ -104,6 +188,8 @@ namespace opt {
bool preprocess::operator()(vector<soft>& soft, rational& lower) {
if (!find_mutexes(soft, lower))
return false;
if (false && !prop_mutexes(soft, lower))
return false;
return true;
}
};
2 changes: 2 additions & 0 deletions src/opt/opt_preprocess.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,10 @@ namespace opt {
solver& s;
expr_ref_vector m_trail;

expr_ref_vector propagate(expr* f, lbool& is_sat);
obj_map<expr, rational> soft2map(vector<soft> const& softs, expr_ref_vector& fmls);
bool find_mutexes(vector<soft>& softs, rational& lower);
bool prop_mutexes(vector<soft>& softs, rational& lower);
void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower);

public:
Expand Down
2 changes: 1 addition & 1 deletion src/smt/smt_consequences.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -612,7 +612,7 @@ namespace smt {
}
}
vector<unsigned_vector> _mutexes;
mc.cliques(ps, _mutexes);
mc.cliques2(ps, _mutexes);
for (auto const& mux : _mutexes) {
expr_ref_vector lits(m);
for (unsigned idx : mux) {
Expand Down
63 changes: 40 additions & 23 deletions src/util/max_cliques.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,29 @@ class max_cliques : public T {
m_next.reserve(max);
m_tc.reserve(m_next.size());
}

struct compare_degree {
u_map<uint_set>& conns;
compare_degree(u_map<uint_set>& conns): conns(conns) {}
bool operator()(unsigned x, unsigned y) const {
return conns[x].num_elems() < conns[y].num_elems();
}
};


void init(unsigned_vector const& ps, u_map<uint_set>& conns) {

uint_set vars;

for (unsigned p : ps)
vars.insert(p);

for (unsigned v : ps) {
uint_set reach;
get_reachable(v, vars, reach);
conns.insert(v, reach);
}
}

public:
void add_edge(unsigned src, unsigned dst) {
Expand All @@ -92,7 +115,7 @@ class max_cliques : public T {
m_next[dst].push_back(src);
}

void cliques(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {
void cliques1(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {
init(ps);
unsigned_vector clique;
uint_set vars;
Expand Down Expand Up @@ -124,35 +147,29 @@ class max_cliques : public T {
}
}


// better quality cliques
void cliques2(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {

uint_set all_vars, todo;
void cliques2(unsigned_vector const& ps, vector<unsigned_vector>& cs) {
u_map<uint_set> conns;

init(ps);
// compute connections using TC of implication graph
init(ps, conns);
cliques(ps, conns, cs);
}

struct compare_degree {
u_map<uint_set>& conns;
compare_degree(u_map<uint_set>& conns): conns(conns) {}
bool operator()(unsigned x, unsigned y) const {
return conns[x].num_elems() < conns[y].num_elems();
}
};
// cliques after connections are computed.
void cliques(unsigned_vector const& ps, u_map<uint_set>& conns, vector<unsigned_vector>& cliques) {

unsigned maxp = 1;
for (unsigned p : ps)
maxp = std::max(p, maxp);

uint_set todo;
compare_degree lt(conns);
heap<compare_degree> heap(m_next.size(), lt);
heap<compare_degree> heap(maxp + 1, lt);

for (unsigned p : ps) {
all_vars.insert(p);
for (unsigned p : ps) {
todo.insert(p);
}

for (unsigned v : ps) {
uint_set reach;
get_reachable(v, all_vars, reach);
conns.insert(v, reach);
heap.insert(v);
heap.insert(p);
}

while (!todo.empty()) {
Expand Down

0 comments on commit 807121a

Please sign in to comment.