Merge a636fb3e83 into 477a1d817d

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_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;
     }
 

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

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

@@ -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;

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

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) \

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";
+}