review

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/conflict.cpp

@@ -303,6 +303,11 @@ namespace polysat {
     }
 
     void conflict::add_lemma(char const* name, clause_ref lemma) {
+
+        for (auto lit : *lemma) 
+            if (s.m_bvars.is_true(lit)) 
+                verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
+            
         LOG_H3("Lemma " << (name ? name : "<unknown>") << ": " << show_deref(lemma));
         SASSERT(lemma);
         lemma->set_redundant(true);

src/math/polysat/saturation.cpp

@@ -36,7 +36,7 @@ namespace polysat {
         IF_VERBOSE(1, auto const& cl = core.lemmas().back(); 
                    verbose_stream() << m_rule << " v" << v << " "; 
                    for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " "; 
-                   verbose_stream() << "\n");
+                   verbose_stream() << " " << *cl << "\n");
     }
 
     void saturation::perform(pvar v, conflict& core) {
@@ -74,6 +74,8 @@ namespace polysat {
             prop = true;
         if (try_factor_equality(v, core, i))
             prop = true;
+        if (try_mul_eq_bound(v, core, i))
+            prop = true;
         if (try_ugt_x(v, core, i))
             prop = true;
         if (try_ugt_y(v, core, i))
@@ -652,8 +654,67 @@ namespace polysat {
 
 
     // bench 5
+    // fairly ad-hoc rule derived from bench 5.
+    // The clause could also be added whenever narrowing the literal 2^k*x = 2^k*y
+    // It can be expected to be relatively common because these equalities come from
+    // bit-masking.
+    // 
+    // A bigger hammer for detecting such propagations may be through LIA or a variant
+    // 
+    // a*x - a*y + b*z = 0 0 <= x < b/a, 0 <= y < b/a => z = 0
+    // and then => x = y
+    // 
+    // the general lemma is that the linear term a*p = 0 is such that a*p does not overflow
+    // and therefore p = 0
+    // 
+    // TBD: encode the general lemma instead of this special case.
+    // 
     bool saturation::try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y) {
         set_rule("[x] 2^k*x = 2^k*y & x < 2^N-k => y = x or y >= 2^{N-k}");
+        auto& m = s.var2pdd(x);
+        unsigned N = m.power_of_2();
+        pdd y = m.zero();
+        pdd a = y, b = y, a2 = y;
+        pdd X = s.var(x);
+        if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
+            return false;
+        if (!a.is_val())
+            return false;
+        if (!a.val().is_power_of_two())
+            return false;
+        unsigned k = a.val().trailing_zeros();
+        if (k == 0)
+            return false;
+        b = -b;
+        if (b.leading_coefficient() != a.val())
+            return false;
+        for (auto c : core) {
+            if (!c->is_ule())
+                continue;
+            auto i = inequality::from_ule(c);
+            if (!is_x_l_Y(x, i, a2))
+                continue;
+            if (!a2.is_val())
+                continue;
+            // x*2^k = b, x <= a2 < 2^{N-k}
+            rational bound = rational::power_of_two(N - k);
+            if (i.is_strict() && a2.val() >= bound)
+                continue;
+            if (!i.is_strict() && a2.val() > bound)
+                continue;            
+            pdd Y = b.div(b.leading_coefficient());
+            rational Y_val;
+            if (!s.try_eval(Y, Y_val) || Y_val >= bound)
+                continue;
+            signed_constraint le = s.ule(Y, bound - 1);
+            m_lemma.reset();
+            m_lemma.insert_eval(~le);
+            m_lemma.insert_eval(~s.eq(y));
+            m_lemma.insert(~c);
+            if (propagate(x, core, axb_l_y, s.eq(X, Y)))
+                return true;
+        }
+
         return false;
     }
 

src/math/polysat/solver.cpp

@@ -52,6 +52,7 @@ namespace polysat {
         m_config.m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
         m_config.m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
         m_config.m_log_conflicts = pp.log_conflicts();
+        m_rand.set_seed(m_params.get_uint("random_seed", 0));
     }
 
     bool solver::should_search() {
@@ -241,9 +242,11 @@ namespace polysat {
         for (; i < sz && !is_conflict(); ++i)
             if (!propagate(v, wlist[i]))
                 wlist[j++] = wlist[i];
-        for (; i < sz; ++i)
+        for (; i < sz; ++i) 
             wlist[j++] = wlist[i];
         wlist.shrink(j);
+        if (is_conflict())
+            shuffle(wlist.size(), wlist.data(), m_rand);
         DEBUG_CODE(m_locked_wlist = std::nullopt;);
     }
 
@@ -968,7 +971,7 @@ namespace polysat {
 
         LOG("best_score: " << best_score);
         LOG("best_lemma: " << *best_lemma);
-
+            
         m_conflict.reset();
         backjump(jump_level);
 

src/math/polysat/solver.h

@@ -153,6 +153,7 @@ namespace polysat {
         bool_var_manager         m_bvars;       // Map boolean variables to constraints
         var_queue                m_free_pvars;  // free poly vars
         stats                    m_stats;
+        random_gen               m_rand;
 
         config                   m_config;
         // Per constraint state

src/math/polysat/viable.cpp

@@ -919,6 +919,9 @@ namespace polysat {
 
         SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); }));
 
+        // NSB review: bench23 exposes a scenario where s.m_bvars.value(lit) == l_true. So the viable lemma is mute, but the literal in the premise
+        // is a conflict.
+        // SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
         core.add_lemma("viable", lemma.build());
         core.logger().log(inf_fi(*this, v));
         return true;