From d3183fafc79ebe972312ce9bb1f3b840800964b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Jan 2025 13:39:26 -0800 Subject: [PATCH] remove binspr experiment --- src/params/sat_params.pyg | 1 - src/sat/CMakeLists.txt | 1 - src/sat/sat_binspr.cpp | 484 -------------------------------------- src/sat/sat_binspr.h | 108 --------- src/sat/sat_config.cpp | 2 - src/sat/sat_config.h | 1 - src/sat/sat_solver.cpp | 5 - src/sat/sat_solver.h | 3 - 8 files changed, 605 deletions(-) delete mode 100644 src/sat/sat_binspr.cpp delete mode 100644 src/sat/sat_binspr.h diff --git a/src/params/sat_params.pyg b/src/params/sat_params.pyg index 370bf1dea..d45b4c0bf 100644 --- a/src/params/sat_params.pyg +++ b/src/params/sat_params.pyg @@ -72,7 +72,6 @@ def_module_params('sat', ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'), ('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'), - ('binspr', BOOL, False, 'enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models'), ('anf', BOOL, False, 'enable ANF based simplification in-processing'), ('anf.delay', UINT, 2, 'delay ANF simplification by in-processing round'), ('anf.exlin', BOOL, False, 'enable extended linear simplification'), diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index 48e6959b3..2f2c76da6 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -7,7 +7,6 @@ z3_add_component(sat sat_asymm_branch.cpp sat_bcd.cpp sat_big.cpp - sat_binspr.cpp sat_clause.cpp sat_clause_set.cpp sat_clause_use_list.cpp diff --git a/src/sat/sat_binspr.cpp b/src/sat/sat_binspr.cpp deleted file mode 100644 index acfd12980..000000000 --- a/src/sat/sat_binspr.cpp +++ /dev/null @@ -1,484 +0,0 @@ -/*++ - Copyright (c) 2019 Microsoft Corporation - - Module Name: - - sat_binspr.cpp - - Abstract: - - Inprocessing step for creating SPR binary clauses. - - Author: - - Nikolaj Bjorner, Marijn Heule 2019-4-29 - - Notes: - - - L = { lit1, lit2 } - G := { touched_L(C) | C in F and C intersects with L, and not F|L |-_unit untouch_L(C) } - G & ~L is satisfiable - ------------ - Learn ~lit1 or ~lit2 - - -Marijn's version: - - L = { lit1, lit2 } - alpha = L + units in F|L - G := { touched_alpha(C) | C in F and C intersects with L, and not F|L |-_unit untouch_alpha(C) } - G & ~L is satisfiable - --------------------- - Learn ~L - - - - - Alternative: - - for p in literals: - push(1) - propagate(p) - candidates = literals \ units - for (C or p) in use(p) and candidates != empty: - push(1) - propagate(~C) - if inconsistent(): - learn C (subsumes C or p) - else: - candidates' := C union ~(consequences of propagate(~C)) - candidates := candidates' intersect candidates - pop(1) - for q in candidates: - add (~q or ~p) - pop(1) - - The idea is that all clauses using p must satisfy - q in C or F|pq |-1 untouched(C) - The clauses that contain q are not restricted: We directly create G := (~p or ~q) & q, which is satisfiable - Let pqM |= F, we claim then that ~pqM |= F - - - every clause (C or q) that contains q is satisfied by ~pqM - - every clause (C or p) that does not contain q positively, but contains p satisfies F|pq |-1 untouched(C) - Therefore pqM |= untouched(C) and therefore already M |= untouched(C) - - all other clauses are satisfied by pqM, but contain neither p, nor q, - so it is already the case that M satisfies the clause. - - Alternative: - - for p in literals: - push(1) - propagate(p) - candidates = {} - for (C or p) in use(p): - push(1) - propagate(~C) - if inconsistent(): - learn C (subsumes C or p) - else: - candidates := candidates union C union ~(consequences of propagate(~C)) - pop(1) - for q in candidates: - push(1) - propagate(q) - incons := true - for (C or p) in use(p) and incons: - push(1) - propagate(~C) - incons := inconsistent() - pop(1) - pop(1) - if incons: - add (~p or ~q) - pop(1) - - The idea is similar to the previous alternative, but it allows a candidate to - not be directly unit derivable in all clauses C or p, but could be a failed literal - under the assumption ~C. - The motivation for this variant is that it is unlikely that we need failed literals to - close both (C_1 or p),..., (C_n or p) for all clauses containing p. - - Alternative: - - - 1. extract BIG - Use BIG to limit cone enumeration - 2. for each literal lit: - enumerate k1 in cone of lit - enumerate lit2 in use(~k1) - check if cone of lit2 contains k2 such that lit1 in use(~k2) - - --*/ - -#include "sat/sat_binspr.h" -#include "sat/sat_solver.h" -#include "sat/sat_big.h" - -namespace sat { - - struct binspr::report { - binspr& m_binspr; - stopwatch m_watch; - report(binspr& b): - m_binspr(b) { - m_watch.start(); - } - ~report() { - m_watch.stop(); - unsigned nb = m_binspr.m_bin_clauses; - IF_VERBOSE(2, verbose_stream() << " (sat-binspr :binary " << nb << m_watch << ")\n"); - } - }; - - void binspr::operator()() { - s = alloc(solver, m_solver.params(), m_solver.rlimit()); - m_solver.pop_to_base_level(); - s->copy(m_solver, true); - unsigned num = s->num_vars(); - m_bin_clauses = 0; - - report _rep(*this); - m_use_list.reset(); - m_use_list.reserve(num * 2); - for (clause* c : s->m_clauses) { - if (!c->frozen() && !c->was_removed()) { - for (literal lit : *c) { - m_use_list[lit.index()].push_back(c); - } - } - } - TRACE("sat", s->display(tout);); - algorithm2(); - if (!s->inconsistent()) { - params_ref p; - p.set_uint("sat.max_conflicts", 10000); - p.set_bool("sat.binspr", false); - s->updt_params(p); - s->check(0, nullptr); - } - - if (s->inconsistent()) { - s->set_conflict(); - } - else { - s->pop_to_base_level(); - for (unsigned i = m_solver.init_trail_size(); i < s->init_trail_size(); ++i) { - literal lit = s->trail_literal(i); - m_solver.assign(lit, s->get_justification(lit)); - } - TRACE("sat", tout << "added " << (s->init_trail_size() - m_solver.init_trail_size()) << " units\n";); - } - } - - - /** - F, p |- ~u, - F, p, q |- ~v, - { p, v } u C in F - { q, u } u D in F - - Then use { p, ~u, q, ~v } as alpha, L = { p, q } - - for u in ~consequences of p: - for (u u D) in use(u): - for q in D, unassigned: - for v in ~consequences(q) | ({p, v} u C) in use(v): - check_spr(p, q, u, v) - */ - - void binspr::algorithm2() { - mk_masks(); - unsigned num_lits = 2 * s->num_vars(); - for (unsigned l_idx = 0; l_idx < num_lits && !s->inconsistent(); ++l_idx) { - s->checkpoint(); - literal p = to_literal(l_idx); - TRACE("sat", tout << "p " << p << " " << s->value(p) << "\n";); - if (is_used(p) && s->value(p) == l_undef) { - s->push(); - s->assign_scoped(p); - unsigned sz_p = s->m_trail.size(); - s->propagate(false); - if (s->inconsistent()) { - s->pop(1); - s->assign_unit(~p); - s->propagate(false); - TRACE("sat", s->display(tout << "unit\n");); - IF_VERBOSE(0, verbose_stream() << "unit " << (~p) << "\n"); - continue; - } - for (unsigned i = sz_p; !s->inconsistent() && i < s->m_trail.size(); ++i) { - literal u = ~s->m_trail[i]; - TRACE("sat", tout << "p " << p << " u " << u << "\n";); - for (clause* cp : m_use_list[u.index()]) { - for (literal q : *cp) { - if (s->inconsistent()) - break; - if (s->value(q) != l_undef) - continue; - - s->push(); - s->assign_scoped(q); - unsigned sz_q = s->m_trail.size(); - s->propagate(false); - if (s->inconsistent()) { - // learn ~p or ~q - s->pop(1); - block_binary(p, q, true); - s->propagate(false); - continue; - } - bool found = false; - for (unsigned j = sz_q; !found && j < s->m_trail.size(); ++j) { - literal v = ~s->m_trail[j]; - for (clause* cp2 : m_use_list[v.index()]) { - if (cp2->contains(p)) { - if (check_spr(p, q, u, v)) { - found = true; - break; - } - } - } - } - s->pop(1); - if (found) { - block_binary(p, q, false); - s->propagate(false); - TRACE("sat", s->display(tout);); - } - } - } - } - s->pop(1); - } - } - } - - bool binspr::is_used(literal lit) const { - return !m_use_list[lit.index()].empty() || !s->get_wlist(~lit).empty(); - } - - bool binspr::check_spr(literal p, literal q, literal u, literal v) { - SASSERT(s->value(p) == l_true); - SASSERT(s->value(q) == l_true); - SASSERT(s->value(u) == l_false); - SASSERT(s->value(v) == l_false); - init_g(p, q, u, v); - literal lits[4] = { p, q, ~u, ~v }; - for (unsigned i = 0; g_is_sat() && i < 4; ++i) { - binary_are_unit_implied(lits[i]); - clauses_are_unit_implied(lits[i]); - } - TRACE("sat", tout << p << " " << q << " " << u << " " << v << " " << g_is_sat() << "\n";); - return g_is_sat(); - } - - void binspr::binary_are_unit_implied(literal p) { - for (watched const& w : s->get_wlist(~p)) { - if (!g_is_sat()) { - break; - } - if (!w.is_binary_non_learned_clause()) { - continue; - } - - clear_alpha(); - VERIFY(touch(p)); - literal lit = w.get_literal(); - SASSERT(lit != p); - - if (touch(lit)) { - add_touched(); - continue; - } - - bool inconsistent = (s->value(lit) == l_true); - if (s->value(lit) == l_undef) { - s->push(); - s->assign_scoped(~lit); - s->propagate(false); - inconsistent = s->inconsistent(); - s->pop(1); - } - - if (!inconsistent) { - TRACE("sat", tout << "not implied: " << p << " " << lit << "\n";); - m_state = 0; - add_touched(); - } - } - } - - void binspr::clauses_are_unit_implied(literal p) { - for (clause* cp : m_use_list[p.index()]) { - if (!g_is_sat()) break; - clause_is_unit_implied(*cp); - } - } - - void binspr::clause_is_unit_implied(clause const& c) { - s->push(); - clear_alpha(); - for (literal lit : c) { - if (touch(lit)) { - continue; - } - else if (s->value(lit) == l_true) { - s->pop(1); - return; - } - else if (s->value(lit) != l_false) { - s->assign_scoped(~lit); - } - } - s->propagate(false); - bool inconsistent = s->inconsistent(); - s->pop(1); - if (!inconsistent) { - add_touched(); - } - } - - - void binspr::block_binary(literal lit1, literal lit2, bool learned) { - IF_VERBOSE(2, verbose_stream() << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n"); - TRACE("sat", tout << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n";); - s->mk_clause(~lit1, ~lit2, learned ? sat::status::redundant() : sat::status::asserted()); - ++m_bin_clauses; - } - - void binspr::g_add_unit(literal lit1, literal lit2) { - if (lit1.var() < lit2.var()) { - m_state &= 0x2; - } - else { - m_state &= 0x4; - } - } - - void binspr::g_add_binary(literal lit1, literal lit2, bool flip2) { - bool flip1 = false; - if (lit1.var() > lit2.var()) { std::swap(flip1, flip2); } - m_state &= ((flip1?0x5:0xA) | (flip2?0x3:0xC)); - } - - // 0 -> 10 - // 1 -> 01 - // * -> 11 - // 00 -> 1000 - // 10 -> 0100 - // 01 -> 0010 - // 11 -> 0001 - // *1 -> 00110011 - // *0 -> 11001100 - // 0* -> 10101010 - // 1* -> 01010101 - // **1 -> 00001111 - // **0 -> 11110000 - - /** - \brief create masks (lsb is left) - i = 0: 1010101010101010 - i = 1: 1100110011001100 - i = 2: 1111000011110000 - */ - unsigned binspr::mk_mask(unsigned i) { - // variable number i is false. - unsigned mask0 = (1 << (1 << i)) - 1; // 2^i bits of ones - unsigned pos = 1 << (i+1); // how many bits in mask - - unsigned mask = mask0; - while (pos < 32) { - mask |= (mask0 << pos); - pos += 1 << (i + 1); - } - return mask; - } - - void binspr::mk_masks() { - for (unsigned i = 0; i < max_lits; ++i) { - m_false[i] = mk_mask(i); - m_true[i] = m_false[i] << (1 << i); - } - } - - /** - \brief create Boolean function table - corresponding to disjunction of literals - */ - - void binspr::add_touched() { - - unsigned mask = 0; - for (unsigned i = 0; i < 4; ++i) { - switch (m_vals[i]) { - case l_true: - mask |= m_true[i]; - break; - case l_false: - mask |= m_false[i]; - break; - default: - break; - } - } - m_state &= mask; - TRACE("sat", - { - bool_var vars[4]; - vars[0] = m_p; vars[1] = m_q; vars[2] = m_u; vars[3] = m_v; - tout << "touched: "; - for (unsigned i = 0; i < 4; ++i) { - switch (m_vals[i]) { - case l_true: - tout << literal(vars[i], false) << " "; - break; - case l_false: - tout << literal(vars[i], true) << " "; - break; - default: - break; - } - } - display_mask(tout << " ", m_state); - }); - } - - void binspr::init_g(literal p, literal q, literal u, literal v) { - m_p = p.var(); - m_q = q.var(); - m_u = u.var(); - m_v = v.var(); - m_state = ~0; - clear_alpha(); - VERIFY(touch(~p)); - VERIFY(touch(~q)); - add_touched(); - } - - void binspr::clear_alpha() { - m_vals[0] = m_vals[1] = m_vals[2] = m_vals[3] = l_undef; - } - - bool binspr::touch(literal p) { - bool_var v = p.var(); - if (v == m_p) m_vals[0] = to_lbool(!p.sign()); - else if (v == m_q) m_vals[1] = to_lbool(!p.sign()); - else if (v == m_u) m_vals[2] = to_lbool(!p.sign()); - else if (v == m_v) m_vals[3] = to_lbool(!p.sign()); - else return false; - return true; - } - - std::ostream& binspr::display_mask(std::ostream& out, unsigned mask) const { - for (unsigned i = 0; i < 4; ++i) { - out << m_vals[i] << " "; - } - out << " - "; - for (unsigned i = 0; i < 32; ++i) { - out << (0 != (mask & (1 << i)) ? 1 : 0); - } - return out << "\n"; - } -} - diff --git a/src/sat/sat_binspr.h b/src/sat/sat_binspr.h deleted file mode 100644 index f533ff489..000000000 --- a/src/sat/sat_binspr.h +++ /dev/null @@ -1,108 +0,0 @@ -/*++ - Copyright (c) 2019 Microsoft Corporation - - Module Name: - - sat_binspr.h - - Abstract: - - Inprocessing step for creating SPR binary clauses. - - Author: - - Nikolaj Bjorner, Marijn Heule 2019-4-29 - - Notes: - - - --*/ -#pragma once - -#include "util/params.h" -#include "util/statistics.h" -#include "sat/sat_clause.h" -#include "sat/sat_types.h" - -namespace sat { - class solver; - - class binspr { - enum states { - unit = 0xA, // 1010 - unit_or_other_nunit = 0xB, // 1011 - either = 0xE, // 1110 - nand = 0x7, // 0111 - not_pr = 0x0 - }; - - solver& m_solver; - scoped_ptr s; - unsigned m_bin_clauses{ 0 }; - unsigned m_stopped_at{ 0 }; - vector m_use_list; - unsigned m_limit1{ 0 }, m_limit2{ 0 }; - bool_vector m_mark, m_mark2; - literal_vector m_must_candidates, m_may_candidates; - unsigned m_state{ 0 }; - - void init_g() { m_state = 0x7; } - void g_add_binary(literal l1, literal l2, bool flip2); - void g_add_unit(literal l1, literal l2); // l1 is a unit - bool g_is_sat() { return m_state != 0; } - - void init_g(literal p, literal q, literal u, literal v); - - - struct report; - - void block_binary(literal lit1, literal lit2, bool learned); - void double_lookahead(); - - void check_spr_single_lookahead(literal lit); - void check_spr(literal lit1); - void check_spr(literal lit1, literal lit2); - bool check_spr(literal p, literal q, literal s, literal r); - void binary_are_unit_implied(literal lit1, literal lit2); - void clauses_are_unit_implied(literal lit1, literal lit2); - void clause_is_unit_implied(literal lit1, literal lit2, clause& c); - bool is_used(literal lit) const; - void update_candidates(bool& first, unsigned sz1); - void collect_candidates(literal lit, literal const* begin, literal const* end); - void strengthen_clause(literal lit, literal const* begin, literal const* end); - - bool_var m_p{ 0 }, m_q{ 0 }, m_u{ 0 }, m_v{ 0 }; - lbool m_vals[4]; - - void algorithm2(); - void algorithm2(literal lit, clause const& c); - void clear_alpha(); - void add_touched(); - bool touch(literal p); - void binary_are_unit_implied(literal p); - void clauses_are_unit_implied(literal p); - void clause_is_unit_implied(clause const& c); - static const unsigned max_lits = 5; // = log(32) - unsigned m_true[max_lits], m_false[max_lits]; - unsigned mk_function(svector const& lits); - void mk_masks(); - unsigned mk_mask(unsigned i); - - std::ostream& display_mask(std::ostream& out, unsigned mask) const; - - public: - - binspr(solver& s): m_solver(s), m_stopped_at(0), m_limit1(1000), m_limit2(300) { - memset(m_true, 0, sizeof(unsigned) * max_lits); - memset(m_false, 0, sizeof(unsigned) * max_lits); - } - - void operator()(); - - void updt_params(params_ref const& p) {} - - void collect_statistics(statistics& st) const {} - - }; -} - diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 7ee747b5b..338ea8692 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -106,8 +106,6 @@ namespace sat { else m_local_search_mode = local_search_mode::wsat; m_local_search_dbg_flips = p.local_search_dbg_flips(); - //m_binspr = p.binspr(); - m_binspr = false; // prevent adventurous users from trying feature that isn't ready m_anf_simplify = p.anf(); m_anf_delay = p.anf_delay(); m_anf_exlin = p.anf_exlin(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index a47f041b0..d032e64a1 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -119,7 +119,6 @@ namespace sat { bool m_local_search; local_search_mode m_local_search_mode; bool m_local_search_dbg_flips; - bool m_binspr; bool m_cut_simplify; unsigned m_cut_delay; bool m_cut_aig; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1f069e3cb..4390729fd 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -54,7 +54,6 @@ namespace sat { m_asymm_branch(*this, p), m_probing(*this, p), m_mus(*this), - m_binspr(*this), m_inconsistent(false), m_searching(false), m_conflict(justification(0)), @@ -2099,10 +2098,6 @@ namespace sat { m_par->to_solver(*this); } - if (m_config.m_binspr && !inconsistent()) { - m_binspr(); - } - if (m_config.m_anf_simplify && m_simplifications > m_config.m_anf_delay && !inconsistent()) { anf_simplifier anf(*this); anf_simplifier::config cfg; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index a12a23a6f..5b96cc1b8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -42,7 +42,6 @@ Revision History: #include "sat/sat_cut_simplifier.h" #include "sat/sat_probing.h" #include "sat/sat_mus.h" -#include "sat/sat_binspr.h" #include "sat/sat_drat.h" #include "sat/sat_parallel.h" #include "sat/sat_local_search.h" @@ -114,7 +113,6 @@ namespace sat { probing m_probing; bool m_is_probing { false }; mus m_mus; // MUS for minimal core extraction - binspr m_binspr; bool m_inconsistent; bool m_searching; // A conflict is usually a single justification. That is, a justification @@ -215,7 +213,6 @@ namespace sat { friend class cleaner; friend class asymm_branch; friend class big; - friend class binspr; friend class drat; friend class elim_eqs; friend class bcd;