Add gc.learned_pop parameter and sat_gc benchmark for push/pop learned clause cleanup

- src/params/sat_params.pyg: Add gc.learned_pop (bool, default true) parameter
- src/sat/sat_config.h: Add m_gc_learned_pop field to config
- src/sat/sat_config.cpp: Read gc.learned_pop from params
- src/sat/sat_solver.cpp: Gate the user_pop cleanup on m_config.m_gc_learned_pop
- src/test/sat_gc.cpp: New benchmark showing 6000+ clauses removed per run
- src/test/main.cpp: Register tst_sat_gc in FOR_EACH_EXTRA_TEST
- src/test/CMakeLists.txt: Add sat_gc.cpp to test sources

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/83cecb0d-37c4-4f96-a987-7d73ae8fabc3

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

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'),

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();
 

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;
 

src/sat/sat_solver.cpp

@@ -3727,7 +3727,7 @@ namespace sat {
         // 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 (old_sz < 3) {
+        if (m_config.m_gc_learned_pop && old_sz < 3) {
             unsigned j = 0;
             for (clause* c : m_learned) {
                 if (c->scope_lim() > old_sz) {

src/test/CMakeLists.txt

@@ -122,6 +122,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

src/test/main.cpp

@@ -167,6 +167,7 @@
     X(theory_pb) \
     X(simplex) \
     X(sat_user_scope) \
+    X(sat_gc) \
     X_ARGV(ddnf) \
     X(ddnf1) \
     X(model_evaluator) \

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 <iostream>
+
+// 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<unsigned>(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";
+}