mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-24 03:57:51 +00:00
Code Activity

unsat core for SAT solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-29 08:39:34 -07:00
commit 0e9511b597
27 changed files with 2422 additions and 1456 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_params.pyg
View file

@ -17,4 +17,5 @@ def_module_params('sat',
('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses')))
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

130
src/sat/sat_solver.cpp
View file

@ -697,7 +697,7 @@ namespace sat {
try {
if (inconsistent()) return l_false;
init_search();
init_assumptons(num_lits, lits);
init_assumptions(num_lits, lits);
propagate(false);
if (inconsistent()) return l_false;
cleanup();
@ -707,6 +707,7 @@ namespace sat {
if (r != l_undef)
return r;
pop(scope_lvl());
reinit_assumptions();
m_conflicts_since_restart = 0;
m_restart_threshold = m_config.m_restart_initial;
}
@ -861,12 +862,23 @@ namespace sat {
m_assumption_set.reset();
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
SASSERT(is_external(l.var()));
m_assumption_set.insert(l);
m_assumptions.push_back(l);
mk_clause(1, &l);
}
}
void solver::reinit_assumptions() {
if (tracking_assumptions()) {
push();
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
literal l = m_assumptions[i];
mk_clause(1, &l);
}
}
}
bool solver::tracking_assumptions() const {
return !m_assumptions.empty();
}
@ -1010,6 +1022,7 @@ namespace sat {
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
IF_VERBOSE(30, display_status(verbose_stream()););
pop(scope_lvl());
reinit_assumptions();
m_conflicts_since_restart = 0;
switch (m_config.m_restart) {
case RS_GEOMETRIC:
@ -1340,7 +1353,6 @@ namespace sat {
}
bool solver::resolve_conflict_core() {
TRACE("sat_conflict", tout << "conflict detected\n";);
m_stats.m_conflict++;
m_conflicts++;
@ -1348,8 +1360,15 @@ namespace sat {
m_conflicts_since_gc++;
m_conflict_lvl = get_max_lvl(m_not_l, m_conflict);
if (m_conflict_lvl == 0)
if (m_conflict_lvl <= 1 && tracking_assumptions()) {
resolve_conflict_for_unsat_core();
return false;
}
TRACE("sat_conflict", tout << "conflict detected\n";);
if (m_conflict_lvl == 0) {
return false;
}
m_lemma.reset();
forget_phase_of_vars(m_conflict_lvl);
@ -1464,6 +1483,108 @@ namespace sat {
return true;
}
void solver::process_antecedent_for_unsat_core(literal antecedent) {
bool_var var = antecedent.var();
unsigned var_lvl = lvl(var);
SASSERT(var < num_vars());
if (!is_marked(var)) {
mark(var);
m_unmark.push_back(var);
if (is_assumption(antecedent)) {
m_core.push_back(antecedent);
}
}
}
void solver::resolve_conflict_for_unsat_core() {
TRACE("sat_conflict", display(tout););
if (m_conflict_lvl == 0) {
return;
}
unsigned old_size = m_unmark.size();
m_core.reset();
int idx = skip_literals_above_conflict_level();
if (m_not_l != null_literal) {
TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";);
process_antecedent_for_unsat_core(m_not_l);
}
literal consequent = m_not_l;
justification js = m_conflict;
do {
TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
tout << "js kind: " << js.get_kind() << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
process_antecedent_for_unsat_core(~(js.get_literal()));
break;
case justification::TERNARY:
process_antecedent_for_unsat_core(~(js.get_literal1()));
process_antecedent_for_unsat_core(~(js.get_literal2()));
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
unsigned i = 0;
if (consequent != null_literal) {
SASSERT(c[0] == consequent || c[1] == consequent);
if (c[0] == consequent) {
i = 1;
}
else {
process_antecedent_for_unsat_core(~c[0]);
i = 2;
}
}
unsigned sz = c.size();
for (; i < sz; i++)
process_antecedent_for_unsat_core(~c[i]);
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(consequent, js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it)
process_antecedent_for_unsat_core(*it);
break;
}
default:
UNREACHABLE();
break;
}
while (idx >= 0) {
literal l = m_trail[idx];
if (is_marked(l.var()))
break;
SASSERT(idx > 0);
idx--;
}
if (idx < 0) {
break;
}
consequent = m_trail[idx];
if (lvl(consequent) < m_conflict_lvl) {
break;
}
bool_var c_var = consequent.var();
SASSERT(lvl(consequent) == m_conflict_lvl);
js = m_justification[c_var];
idx--;
}
while (idx > 0);
reset_unmark(old_size);
}
unsigned solver::get_max_lvl(literal consequent, justification js) {
if (!m_ext)
return scope_lvl();
@ -1552,6 +1673,7 @@ namespace sat {
}
}
/**
\brief js is an external justification. Collect its antecedents and store at m_ext_antecedents.
*/
@ -1960,7 +2082,7 @@ namespace sat {
clause_wrapper cw = m_clauses_to_reinit[i];
bool reinit = false;
if (cw.is_binary()) {
o if (propagate_bin_clause(cw[0], cw[1])) {
if (propagate_bin_clause(cw[0], cw[1])) {
if (scope_lvl() > 0) {
m_clauses_to_reinit[j] = cw;
j++;

5
src/sat/sat_solver.h
View file

@ -120,6 +120,7 @@ namespace sat {
scoped_ptr<solver> m_clone; // for debugging purposes
literal_vector m_assumptions;
literal_set m_assumption_set;
literal_vector m_core;
void del_clauses(clause * const * begin, clause * const * end);
@ -254,6 +255,7 @@ namespace sat {
public:
lbool check(unsigned num_lits = 0, literal const* lits = 0);
model const & get_model() const { return m_model; }
literal_vector const& get_core() const { return m_core; }
model_converter const & get_model_converter() const { return m_mc; }
protected:
@ -270,6 +272,7 @@ namespace sat {
lbool bounded_search();
void init_search();
void init_assumptions(unsigned num_lits, literal const* lits);
void reinit_assumptions();
bool tracking_assumptions() const;
bool is_assumption(literal l) const;
void simplify_problem();
@ -317,8 +320,10 @@ namespace sat {
literal_vector m_ext_antecedents;
bool resolve_conflict();
bool resolve_conflict_core();
void resolve_conflict_for_unsat_core();
unsigned get_max_lvl(literal consequent, justification js);
void process_antecedent(literal antecedent, unsigned & num_marks);
void process_antecedent_for_unsat_core(literal antecedent);
void fill_ext_antecedents(literal consequent, justification js);
unsigned skip_literals_above_conflict_level();
void forget_phase_of_vars(unsigned from_lvl);

3
src/sat/tactic/atom2bool_var.cpp
View file

@ -90,8 +90,9 @@ struct collect_boolean_interface_proc {
template<typename T>
void operator()(T const & g) {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++)
for (unsigned i = 0; i < sz; i++) {
process(g.form(i));
}
}
void operator()(unsigned sz, expr * const * fs) {

30
src/sat/tactic/goal2sat.cpp
View file

@ -360,14 +360,40 @@ struct goal2sat::imp {
SASSERT(m_result_stack.empty());
}
void add_assumption(expr* d, expr* literal_d) {
}
void operator()(goal const & g) {
m_interface_vars.reset();
collect_boolean_interface(g, m_interface_vars);
unsigned size = g.size();
expr_ref f(m), d_new(m);
ptr_vector<expr> deps;
for (unsigned idx = 0; idx < size; idx++) {
expr * f = g.form(idx);
f = g.form(idx);
// Add assumptions.
if (g.dep(idx)) {
expr_dependency * dep = g.dep(idx);
deps.reset();
m.linearize(dep, deps);
for (unsigned i = 0; i < deps.size(); ++i) {
expr * d = deps[i];
expr * d1;
SASSERT(m.is_bool(d));
if (is_uninterp_const(d)) {
add_assumption(d, d);
}
else if (m.is_not(d, d1) && is_uninterp_const(d1)) {
add_assumption(d, d);
}
else {
// create fresh variable, map back to dependency.
add_assumption(d, d_new);
}
}
}
process(f);
}
}

2
src/sat/tactic/sat_tactic.cpp
View file

@ -46,8 +46,8 @@ class sat_tactic : public tactic {
expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
fail_if_proof_generation("sat", g);
fail_if_unsat_core_generation("sat", g);
bool produce_models = g->models_enabled();
bool produce_core = g->unsat_core_enabled();
TRACE("before_sat_solver", g->display(tout););
g->elim_redundancies();