diff --git a/src/params/sat_params.pyg b/src/params/sat_params.pyg index 2c76b89c4..7039361ec 100644 --- a/src/params/sat_params.pyg +++ b/src/params/sat_params.pyg @@ -36,6 +36,7 @@ def_module_params('sat', ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'), ('gc.burst', BOOL, False, 'perform eager garbage collection during initialization'), ('gc.defrag', BOOL, True, 'defragment clauses when garbage collecting'), + ('gc.learned_pop', BOOL, True, 'remove learned clauses when popping user scopes'), ('simplify.delay', UINT, 0, 'set initial delay of simplification by a conflict count'), ('force_cleanup', BOOL, False, 'force cleanup to remove tautologies and simplify clauses'), ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index c59ce7289..913c729d4 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -34,7 +34,8 @@ namespace sat { m_reinit_stack(false), m_inact_rounds(0), m_glue(255), - m_psm(255) { + m_psm(255), + m_scope_lim(0) { memcpy(m_lits, lits, sizeof(literal) * sz); mark_strengthened(); SASSERT(check_approx()); @@ -192,6 +193,7 @@ namespace sat { cls->m_psm = other.psm(); cls->m_frozen = other.frozen(); cls->m_approx = other.approx(); + cls->m_scope_lim = other.scope_lim(); return cls; } diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 0129febbf..56bd35db6 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -53,6 +53,7 @@ namespace sat { unsigned m_inact_rounds:8; unsigned m_glue:8; unsigned m_psm:8; // transient field used during gc + unsigned m_scope_lim:2; // user scope level when clause was learned (0-3, saturated: levels >=4 map to 3) literal m_lits[0]; static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } @@ -103,6 +104,8 @@ namespace sat { bool on_reinit_stack() const { return m_reinit_stack; } void set_reinit_stack(bool f) { m_reinit_stack = f; } + unsigned scope_lim() const { return m_scope_lim; } + void set_scope_lim(unsigned lim) { m_scope_lim = lim > 3 ? 3 : lim; } }; std::ostream & operator<<(std::ostream & out, clause_vector const & cs); diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 3dfb67f2a..4b02c2051 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -176,6 +176,7 @@ namespace sat { m_gc_k = std::min(255u, p.gc_k()); m_gc_burst = p.gc_burst(); m_gc_defrag = p.gc_defrag(); + m_gc_learned_pop = p.gc_learned_pop(); m_force_cleanup = p.force_cleanup(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 83241fe88..56a9030ab 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -152,6 +152,7 @@ namespace sat { unsigned m_gc_k; bool m_gc_burst; bool m_gc_defrag; + bool m_gc_learned_pop; bool m_force_cleanup; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 09f874e78..01605eccf 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -549,8 +549,10 @@ namespace sat { if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r); - if (st.is_redundant()) + if (st.is_redundant()) { + r->set_scope_lim(m_user_scope_literals.size()); m_learned.push_back(r); + } else m_clauses.push_back(r); if (m_config.m_drat) @@ -3721,6 +3723,25 @@ namespace sat { m_ext->user_pop(num_scopes); gc_vars(max_var); + + // remove learned clauses that were added during the popped user scopes. + // scope_lim is saturated at 3, so when old_sz < 3 we can precisely identify + // and remove clauses learned at scope levels above old_sz. + if (m_config.m_gc_learned_pop && old_sz < 3) { + unsigned j = 0; + for (clause* c : m_learned) { + if (c->scope_lim() > old_sz) { + // pop_to_base_level() ensures no clause is on the reinit stack at base level, + // so it is safe to detach and delete the clause. + SASSERT(!c->on_reinit_stack()); + detach_clause(*c); + del_clause(*c); + } + else + m_learned[j++] = c; + } + m_learned.shrink(j); + } TRACE(sat, display(tout);); m_qhead = 0; diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 319cd829b..43e263ce1 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -123,6 +123,7 @@ add_executable(test-z3 region.cpp sat_local_search.cpp sat_lookahead.cpp + sat_gc.cpp sat_user_scope.cpp scoped_timer.cpp scoped_vector.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index f1d874e00..4adacb0b1 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -168,6 +168,7 @@ X(theory_pb) \ X(simplex) \ X(sat_user_scope) \ + X(sat_gc) \ X_ARGV(ddnf) \ X(ddnf1) \ X(model_evaluator) \ diff --git a/src/test/sat_gc.cpp b/src/test/sat_gc.cpp new file mode 100644 index 000000000..39cb3c286 --- /dev/null +++ b/src/test/sat_gc.cpp @@ -0,0 +1,119 @@ + +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + sat_gc.cpp + +Abstract: + + Benchmark to test the effect of learned clause cleanup on user pop, + controlled by the sat.gc.learned_pop parameter. + + After push/check-sat/pop, learned clauses produced by conflict analysis + that uses only outer-scope clause reasons (and thus carries no scope-guard + literal) survive gc_vars. These stale clauses accumulate across repeated + push/pop cycles and can slow subsequent proofs. + + The gc.learned_pop parameter (default true) removes those clauses on each + pop so the clause database stays clean. + +--*/ + +#include "sat/sat_solver.h" +#include "util/util.h" +#include "util/stopwatch.h" +#include + +// Add random 3-SAT clauses on variables [base, base+n_vars). +static void add_random_3sat(sat::solver& s, unsigned base, unsigned n_vars, + unsigned n_clauses, random_gen& rng) { + while ((unsigned)s.num_vars() < base + n_vars) + s.mk_var(true, true); + for (unsigned i = 0; i < n_clauses; ++i) { + sat::literal lits[3]; + for (unsigned k = 0; k < 3; ++k) + lits[k] = sat::literal(base + rng(n_vars), rng(2) == 0); + s.mk_clause(3, lits); + } +} + +// Run the benchmark. +// +// Scenario: +// 1. Add a near-phase-transition random 3-SAT formula on N outer variables. +// Clause ratio > 4.27 means many instances are UNSAT. +// These outer-scope clauses carry no scope-guard literal. +// 2. Run cycles push/pop rounds. In each round the solver derives conflicts +// from those outer clauses, producing learned lemmas that do NOT carry the +// scope-guard literal and therefore survive gc_vars after pop. +// - gc.learned_pop=true: surviving clauses are removed on pop. +// - gc.learned_pop=false: they accumulate across all cycles. +// 3. Perform the final check-sat and measure time. +// +// The extra accumulated learned clauses (without gc.learned_pop) inflate watch +// lists for outer variables and slow subsequent BCP. +static void run_benchmark(bool gc_learned_pop, + unsigned n_vars, double ratio, unsigned cycles, + unsigned seed, + unsigned& out_learned, double& out_time) { + params_ref p; + p.set_bool("gc.learned_pop", gc_learned_pop); + p.set_uint("random_seed", seed); + reslimit rlim; + + sat::solver s(p, rlim); + s.mk_var(false, false); // variable 0 unused + + random_gen rng(seed); + unsigned n_clauses = static_cast(ratio * n_vars); + add_random_3sat(s, 1, n_vars, n_clauses, rng); + + // Push/pop cycles: each re-solves the same outer formula, generating + // learned lemmas from outer-scope clauses that survive pop when not cleaned. + for (unsigned c = 0; c < cycles; ++c) { + s.user_push(); + s.check(); + s.user_pop(1); + } + + out_learned = s.learned().size(); + + stopwatch sw; + sw.start(); + s.check(); + sw.stop(); + out_time = sw.get_seconds(); +} + +void tst_sat_gc() { + // Use a moderate near-phase-transition instance to demonstrate the effect. + // Increase n_vars, cycles, or ratio for a larger performance difference. + const unsigned n_vars = 200; + const double ratio = 4.5; + const unsigned cycles = 3; + const unsigned seed = 42; + + unsigned lrn_with, lrn_without; + double t_with, t_without; + + run_benchmark(true, n_vars, ratio, cycles, seed, lrn_with, t_with); + run_benchmark(false, n_vars, ratio, cycles, seed, lrn_without, t_without); + + std::cout << "sat.gc.learned_pop=true : learned=" << lrn_with + << " time=" << t_with << "s\n"; + std::cout << "sat.gc.learned_pop=false : learned=" << lrn_without + << " time=" << t_without << "s\n"; + + // The core invariant: gc.learned_pop removes stale inner-scope clauses. + VERIFY(lrn_with <= lrn_without); + + if (lrn_without > lrn_with) + std::cout << "Clauses cleaned up by gc.learned_pop: " + << (lrn_without - lrn_with) << "\n"; + if (t_without > t_with * 1.05) + std::cout << "Speedup: " << (t_without / t_with) << "x\n"; + else + std::cout << "(use larger n_vars/cycles to observe timing impact)\n"; +}