mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

remove unused bdd based variable elimination

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-14 16:07:41 -07:00
parent e41090df83
commit 81f10912ae
5 changed files with 6 additions and 427 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/CMakeLists.txt
View file

@ -17,7 +17,6 @@ z3_add_component(sat
sat_ddfw_wrapper.cpp
sat_drat.cpp
sat_elim_eqs.cpp
sat_elim_vars.cpp
sat_gc.cpp
sat_integrity_checker.cpp
sat_local_search.cpp

335
src/sat/sat_elim_vars.cpp
View file

@ -1,335 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
sat_elim_vars.cpp
Abstract:
Helper class for eliminating variables
Author:
Nikolaj Bjorner (nbjorner) 2017-10-14
Revision History:
--*/
#include "sat/sat_simplifier.h"
#include "sat/sat_elim_vars.h"
#include "sat/sat_solver.h"
namespace sat{
elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) {
m_mark_lim = 0;
m_max_literals = 11;
m_miss = 0;
m_hit1 = 0;
m_hit2 = 0;
}
bool elim_vars::operator()(bool_var v) {
if (s.value(v) != l_undef)
return false;
literal pos_l(v, false);
literal neg_l(v, true);
unsigned num_bin_pos = simp.num_nonlearned_bin(pos_l);
if (num_bin_pos > m_max_literals) return false;
unsigned num_bin_neg = simp.num_nonlearned_bin(neg_l);
if (num_bin_neg > m_max_literals) return false;
clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.num_irredundant() + neg_occs.num_irredundant();
if (clause_size == 0) {
return false;
}
reset_mark();
mark_var(v);
if (!mark_literals(pos_occs)) return false;
if (!mark_literals(neg_occs)) return false;
if (!mark_literals(pos_l)) return false;
if (!mark_literals(neg_l)) return false;
// associate index with each variable.
sort_marked();
dd::bdd b1 = elim_var(v);
double sz1 = b1.cnf_size();
if (sz1 > 2*clause_size) {
++m_miss;
return false;
}
if (sz1 <= clause_size) {
++m_hit1;
return elim_var(v, b1);
}
m.try_cnf_reorder(b1);
sz1 = b1.cnf_size();
if (sz1 <= clause_size) {
++m_hit2;
return elim_var(v, b1);
}
++m_miss;
return false;
}
bool elim_vars::elim_var(bool_var v, dd::bdd const& b) {
literal pos_l(v, false);
literal neg_l(v, true);
clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
// eliminate variable
simp.m_pos_cls.reset();
simp.m_neg_cls.reset();
simp.collect_clauses(pos_l, simp.m_pos_cls);
simp.collect_clauses(neg_l, simp.m_neg_cls);
VERIFY(!simp.is_external(v));
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
simp.save_clauses(mc_entry, simp.m_pos_cls);
simp.save_clauses(mc_entry, simp.m_neg_cls);
s.m_eliminated[v] = true;
++s.m_stats.m_elim_var_bdd;
simp.remove_bin_clauses(pos_l);
simp.remove_bin_clauses(neg_l);
simp.remove_clauses(pos_occs, pos_l);
simp.remove_clauses(neg_occs, neg_l);
pos_occs.reset();
neg_occs.reset();
literal_vector lits;
add_clauses(v, b, lits);
return true;
}
dd::bdd elim_vars::elim_var(bool_var v) {
unsigned index = 0;
for (bool_var w : m_vars) {
m_var2index[w] = index++;
}
literal pos_l(v, false);
literal neg_l(v, true);
clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
dd::bdd b1 = make_clauses(pos_l);
dd::bdd b2 = make_clauses(neg_l);
dd::bdd b3 = make_clauses(pos_occs);
dd::bdd b4 = make_clauses(neg_occs);
dd::bdd b0 = b1 && b2 && b3 && b4;
dd::bdd b = m.mk_exists(m_var2index[v], b0);
TRACE("elim_vars",
tout << "eliminate " << v << "\n";
for (watched const& w : simp.get_wlist(~pos_l)) {
if (w.is_binary_non_learned_clause()) {
tout << pos_l << " " << w.get_literal() << "\n";
}
}
m.display(tout, b1);
for (watched const& w : simp.get_wlist(~neg_l)) {
if (w.is_binary_non_learned_clause()) {
tout << neg_l << " " << w.get_literal() << "\n";
}
}
m.display(tout, b2);
clause_use_list::iterator itp = pos_occs.mk_iterator();
while (!itp.at_end()) {
clause const& c = itp.curr();
tout << c << "\n";
itp.next();
}
m.display(tout, b3);
clause_use_list::iterator itn = neg_occs.mk_iterator();
while (!itn.at_end()) {
clause const& c = itn.curr();
tout << c << "\n";
itn.next();
}
m.display(tout, b4);
tout << "eliminated:\n";
tout << b << "\n";
tout << b.cnf_size() << "\n";
);
return b;
}
void elim_vars::add_clauses(bool_var v0, dd::bdd const& b, literal_vector& lits) {
if (b.is_true()) {
// no-op
}
else if (b.is_false()) {
SASSERT(lits.size() > 0);
literal_vector c(lits);
if (simp.cleanup_clause(c))
return;
switch (c.size()) {
case 0:
s.set_conflict();
break;
case 1:
simp.propagate_unit(c[0]);
break;
case 2:
s.m_stats.m_mk_bin_clause++;
simp.add_non_learned_binary_clause(c[0], c[1]);
simp.back_subsumption1(c[0], c[1], false);
break;
default: {
if (c.size() == 3)
s.m_stats.m_mk_ter_clause++;
else
s.m_stats.m_mk_clause++;
clause* cp = s.alloc_clause(c.size(), c.data(), false);
s.m_clauses.push_back(cp);
simp.m_use_list.insert(*cp);
if (simp.m_sub_counter > 0)
simp.back_subsumption1(*cp);
else
simp.back_subsumption0(*cp);
break;
}
}
}
else {
unsigned v = m_vars[b.var()];
lits.push_back(literal(v, false));
add_clauses(v0, b.lo(), lits);
lits.pop_back();
lits.push_back(literal(v, true));
add_clauses(v0, b.hi(), lits);
lits.pop_back();
}
}
void elim_vars::get_clauses(dd::bdd const& b, literal_vector & lits, clause_vector& clauses, literal_vector& units) {
if (b.is_true()) {
return;
}
if (b.is_false()) {
if (lits.size() > 1) {
clause* c = s.alloc_clause(lits.size(), lits.data(), false);
clauses.push_back(c);
}
else {
units.push_back(lits.back());
}
return;
}
// if (v hi lo)
// (v | lo) & (!v | hi)
// if (v T lo) -> (v | lo)
unsigned v = m_vars[b.var()];
lits.push_back(literal(v, false));
get_clauses(b.lo(), lits, clauses, units);
lits.pop_back();
lits.push_back(literal(v, true));
get_clauses(b.hi(), lits, clauses, units);
lits.pop_back();
}
void elim_vars::reset_mark() {
m_vars.reset();
m_mark.resize(s.num_vars());
m_var2index.resize(s.num_vars());
m_occ.resize(s.num_vars());
++m_mark_lim;
if (m_mark_lim == 0) {
++m_mark_lim;
m_mark.fill(0);
}
}
class elim_vars::compare_occ {
elim_vars& ev;
public:
compare_occ(elim_vars& ev):ev(ev) {}
bool operator()(bool_var v1, bool_var v2) const {
return ev.m_occ[v1] < ev.m_occ[v2];
}
};
void elim_vars::sort_marked() {
std::sort(m_vars.begin(), m_vars.end(), compare_occ(*this));
}
void elim_vars::shuffle_vars() {
unsigned sz = m_vars.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned x = m_rand(sz);
unsigned y = m_rand(sz);
std::swap(m_vars[x], m_vars[y]);
}
}
void elim_vars::mark_var(bool_var v) {
if (m_mark[v] != m_mark_lim) {
m_mark[v] = m_mark_lim;
m_vars.push_back(v);
m_occ[v] = 1;
}
else {
++m_occ[v];
}
}
bool elim_vars::mark_literals(clause_use_list & occs) {
clause_use_list::iterator it = occs.mk_iterator();
while (!it.at_end()) {
clause const& c = it.curr();
for (literal l : c) {
mark_var(l.var());
}
if (num_vars() > m_max_literals) return false;
it.next();
}
return true;
}
bool elim_vars::mark_literals(literal lit) {
watch_list& wl = simp.get_wlist(lit);
for (watched const& w : wl) {
if (w.is_binary_non_learned_clause()) {
mark_var(w.get_literal().var());
}
}
return num_vars() <= m_max_literals;
}
dd::bdd elim_vars::make_clauses(clause_use_list & occs) {
dd::bdd result = m.mk_true();
for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) {
clause const& c = it.curr();
dd::bdd cl = m.mk_false();
for (literal l : c) {
cl |= mk_literal(l);
}
result &= cl;
}
return result;
}
dd::bdd elim_vars::make_clauses(literal lit) {
dd::bdd result = m.mk_true();
watch_list& wl = simp.get_wlist(~lit);
for (watched const& w : wl) {
if (w.is_binary_non_learned_clause()) {
result &= (mk_literal(lit) || mk_literal(w.get_literal()));
}
}
return result;
}
dd::bdd elim_vars::mk_literal(literal l) {
return l.sign() ? m.mk_nvar(m_var2index[l.var()]) : m.mk_var(m_var2index[l.var()]);
}
};

72
src/sat/sat_elim_vars.h
View file

@ -1,72 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
sat_elim_vars.h
Abstract:
Helper class for eliminating variables
Author:
Nikolaj Bjorner (nbjorner) 2017-10-14
Revision History:
--*/
#pragma once
#include "sat/sat_types.h"
#include "math/dd/dd_bdd.h"
namespace sat {
class solver;
class simplifier;
class elim_vars {
class compare_occ;
simplifier& simp;
solver& s;
dd::bdd_manager m;
random_gen m_rand;
svector<bool_var> m_vars;
unsigned_vector m_mark;
unsigned m_mark_lim;
unsigned_vector m_var2index;
unsigned_vector m_occ;
unsigned m_miss;
unsigned m_hit1;
unsigned m_hit2;
unsigned m_max_literals;
unsigned num_vars() const { return m_vars.size(); }
void reset_mark();
void mark_var(bool_var v);
void sort_marked();
void shuffle_vars();
bool mark_literals(clause_use_list & occs);
bool mark_literals(literal lit);
dd::bdd make_clauses(clause_use_list & occs);
dd::bdd make_clauses(literal lit);
dd::bdd mk_literal(literal l);
void get_clauses(dd::bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units);
void add_clauses(bool_var v, dd::bdd const& b, literal_vector& lits);
bool elim_var(bool_var v, dd::bdd const& b);
dd::bdd elim_var(bool_var v);
public:
elim_vars(simplifier& s);
bool operator()(bool_var v);
unsigned hit2() const { return m_hit1; } // first round bdd construction is minimal
unsigned hit1() const { return m_hit2; } // minimal after reshufling
unsigned miss() const { return m_miss; } // not-minimal
};
};

23
src/sat/sat_simplifier.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include "sat/sat_simplifier.h"
#include "sat/sat_simplifier_params.hpp"
#include "sat/sat_solver.h"
#include "sat/sat_elim_vars.h"
#include "sat/sat_integrity_checker.h"
#include "util/stopwatch.h"
#include "util/trace.h"
@ -111,9 +110,6 @@ namespace sat {
bool simplifier::cce_enabled() const { return bce_enabled_base() && (m_cce || m_acce); }
bool simplifier::abce_enabled() const { return bce_enabled_base() && m_abce; }
bool simplifier::bca_enabled() const { return bce_enabled_base() && m_bca; }
bool simplifier::elim_vars_bdd_enabled() const {
return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded();
}
bool simplifier::elim_vars_enabled() const {
return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars && single_threaded();
}
@ -2076,24 +2072,19 @@ namespace sat {
};
void simplifier::elim_vars() {
if (!elim_vars_enabled()) return;
if (!elim_vars_enabled())
return;
elim_var_report rpt(*this);
bool_var_vector vars;
order_vars_for_elim(vars);
sat::elim_vars elim_bdd(*this);
for (bool_var v : vars) {
checkpoint();
if (m_elim_counter < 0)
break;
if (is_external(v)) {
// skip
}
else if (try_eliminate(v)) {
m_num_elim_vars++;
}
else if (elim_vars_bdd_enabled() && elim_bdd(v)) {
m_num_elim_vars++;
}
if (is_external(v))
; // skip
else if (try_eliminate(v))
m_num_elim_vars++;
}
m_pos_cls.finalize();
@ -2126,8 +2117,6 @@ namespace sat {
m_subsumption = p.subsumption();
m_subsumption_limit = p.subsumption_limit();
m_elim_vars = p.elim_vars();
m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy?
m_elim_vars_bdd_delay = p.elim_vars_bdd_delay();
m_incremental_mode = s.get_config().m_incremental && !p.override_incremental();
}

2
src/sat/sat_simplifier_params.pyg
View file

@ -23,8 +23,6 @@ def_module_params(module_name='sat',
('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
('probing', BOOL, True, 'apply failed literal detection during simplification'),
('probing_limit', UINT, 5000000, 'limit to the number of probe calls'),
('probing_cache', BOOL, True, 'add binary literals as lemmas'),