revive polynomial superposition (wip)

src/math/polysat/conflict.cpp

@@ -61,13 +61,17 @@ namespace polysat {
 
     class conflict_resolver {
         inf_saturate m_saturate;
+        ex_polynomial_superposition m_poly_sup;
 
     public:
         conflict_resolver(solver& s)
             : m_saturate(s)
+            , m_poly_sup(s)
         {}
 
         bool try_resolve_value(pvar v, conflict& core) {
+            if (m_poly_sup.perform(v, core))
+                return true;
             if (m_saturate.perform(v, core))
                 return true;
             return false;
@@ -212,7 +216,8 @@ namespace polysat {
     }
 
     void conflict::set(signed_constraint c) {
-        reset();
+        SASSERT(!empty());
+        remove_all();
         set_impl(c);
     }
 
@@ -223,7 +228,8 @@ namespace polysat {
             // - opposite input literals are handled separately
             // - other boolean conflicts will discover violated clause during boolean propagation
             VERIFY(false);  // fail here to force check when we encounter this case
-        } else {
+        }
+        else {
             // conflict due to assignment
             SASSERT(c.bvalue(s) == l_true);
             SASSERT(c.is_currently_false(s));
@@ -265,13 +271,11 @@ namespace polysat {
             }
             SASSERT(!m_vars.contains(v));
             // TODO: apply conflict resolution plugins here too?
-        } else {
+        }
+        else {
             logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
             set_backtrack();
             VERIFY(s.m_viable.resolve(v, *this));
-            // TODO: in general the forbidden interval lemma is not asserting.
-            //       but each branch exclude the current assignment.
-            //       in those cases we will (additionally?) need an abstraction that is asserting to make sure viable is updated properly.
         }
         SASSERT(!empty());
     }
@@ -317,6 +321,33 @@ namespace polysat {
                 m_vars.insert(v);
     }
 
+    void conflict::bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len) {
+        if (c.is_always_false()) {
+            VERIFY(false);  // TODO: this case can probably happen, but needs special attention
+        }
+        // Build lemma: premises ==> c
+        clause_builder cb(s);
+        for (unsigned i = 0; i < premises_len; ++i) {
+            SASSERT_EQ(premises[i].bvalue(s), l_true);
+            cb.push(~premises[i]);
+        }
+        SASSERT_EQ(c.bvalue(s), l_undef);
+        cb.push_new(c);
+        clause_ref lemma = cb.build();
+        SASSERT(lemma);
+        lemma->set_redundant(true);
+        set_side_lemma(c, lemma);
+        // TODO: we must "simulate" the propagation but don't want to put the literal onto the search stack.
+        s.assign_propagate(c.blit(), *lemma);
+        // s.m_search.pop();  // doesn't work... breaks m_trail and backjumping
+        SASSERT_EQ(c.bvalue(s), l_true);
+        // insert(c);
+    }
+
+    void conflict::bool_propagate(signed_constraint c, std::initializer_list<signed_constraint> premises) {
+        bool_propagate(c, std::data(premises), premises.size());
+    }
+
     void conflict::remove(signed_constraint c) {
         SASSERT(contains(c));
         m_literals.remove(c.blit().index());
@@ -324,6 +355,16 @@ namespace polysat {
             m_var_occurrences[v]--;
     }
 
+    void conflict::remove_all() {
+        SASSERT(!empty());
+        m_literals.reset();
+        m_vars.reset();
+        m_bail_vars.reset();
+        m_relevant_vars.reset();
+        m_var_occurrences.reset();
+        m_kind = conflict_kind_t::ok;
+    }
+
     void conflict::insert(signed_constraint c, clause_ref lemma) {
         unsigned const idx = c.blit().to_uint();
         SASSERT(!contains(c));  // not required, but this case should be checked

src/math/polysat/conflict.h

@@ -130,8 +130,11 @@ namespace polysat {
         ~conflict();
 
         inference_logger& logger();
+        void log_inference(inference const& inf) { logger().log(inf); }
 
         bool empty() const;
+
+        /** Reset to "no conflict" state. This is only appropriate when conflict resolution is complete or aborted. */
         void reset();
 
         using const_iterator = conflict_iterator;
@@ -193,8 +196,23 @@ namespace polysat {
         /** Evaluate constraint under assignment and insert it into conflict state. */
         void insert_eval(signed_constraint c);
 
+        /**
+         * Derive new constraint c by bool-propagation from premises c1, ..., cn;
+         * as if c was unit-propagated by the lemma c1 /\ ... /\ cn ==> c.
+         * Does not add c to the conflict state.
+         */
+        void bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len);
+        void bool_propagate(signed_constraint c, std::initializer_list<signed_constraint> premises);
+
         /** Remove c from core */
         void remove(signed_constraint c);
+        void remove_var(pvar v);
+        /**
+         * Remove all constraints and variables from the conflict state.
+         * Use this during conflict resolution if the core needs to be replaced.
+         * (It keeps the conflict level and side lemmas.)
+         */
+        void remove_all();
 
         /** Perform boolean resolution with the clause upon the given literal. */
         void resolve_bool(sat::literal lit, clause const& cl);

src/math/polysat/explain.cpp

@@ -1,15 +1,14 @@
-#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
 
-    Conflict explanation / resolution
+    Conflict explanation by polynomial superposition
 
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 --*/
 #include "math/polysat/explain.h"
@@ -18,6 +17,7 @@ Author:
 
 namespace polysat {
 
+/*
     struct post_propagate2 : public inference {
         const char* name;
         signed_constraint conclusion;
@@ -32,6 +32,7 @@ namespace polysat {
                 << " and " << premise2.blit() << ": " << premise2;
         }
     };
+*/
 
     struct inference_sup : public inference {
         const char* name;
@@ -60,6 +61,8 @@ namespace polysat {
             return {};
         // Only keep result if the degree in c2 was reduced.
         // (this condition might be too strict, but we use it for now to prevent looping)
+        // TODO: check total degree; only keep if total degree smaller or equal.
+        //       can always do this if c1 is linear.
         if (b.degree(v) <= r.degree(v))
             return {};
         signed_constraint c = s.eq(r);
@@ -75,6 +78,7 @@ namespace polysat {
     lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
         vector<signed_constraint> premises;
 
+#if 0
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
@@ -87,6 +91,14 @@ namespace polysat {
                 continue;
             if (!c1.is_currently_true(s))
                 continue;
+#else
+        for (auto c1 : s.m_viable.get_constraints(v)) {
+            if (!c1->contains_var(v))  // side conditions do not contain v; skip them here
+                continue;
+            if (!c1.is_eq())
+                continue;
+            SASSERT(c1.is_currently_true(s));
+#endif
             signed_constraint c = resolve1(v, c1, c2);
             if (!c)
                 continue;
@@ -95,43 +107,30 @@ namespace polysat {
             switch (c.bvalue(s)) {
             case l_false:
                 // new conflict state based on propagation and theory conflict
-                core.reset();
+                core.remove_all();
                 core.insert(c1);
                 core.insert(c2);
                 core.insert(~c);
-                core.log_inference(inference_sup("1", v, c2, c1));
+                core.log_inference(inference_sup("l_false", v, c2, c1));
                 return l_true;
             case l_undef:
-#if 0
+                inf_name = "l_undef";
-                core.reset();
+                // c evaluates to false,
-                core.insert(c1);
+                // c should be unit-propagated to l_true by c1 /\ c2 ==> c
-                core.insert(c2);
+                core.bool_propagate(c, {c1, c2});
-                core.insert(~c);
+                // TODO: log inference?
-                core.log_inference(inference_sup("1b", v, c2, c1));
-                return l_true;
-#else
-                SASSERT(premises.empty());
-                // Ensure that c is assigned and justified                    
-                premises.push_back(c1);
-                premises.push_back(c2);
-                // var dependency on c is lost
-                // c evaluates to false, when the clause ~c1 or ~c2 or c
-                // gets created, c is assigned to false by evaluation propagation
-                // It should have been assigned true by unit propagation.
-                core.replace(c2, c, premises);
-                core.log_inference(post_propagate2("superposition", c, c2, c1));
-                inf_name = "2";
                 SASSERT_EQ(l_true, c.bvalue(s));
                 SASSERT(c.is_currently_false(s));
                 break;
-#endif
+            case l_true:
+                inf_name = "l_true";
+                break;
             default:
+                UNREACHABLE();
                 break;
             }
 
-            // NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3).
             // c alone (+ variables) is now enough to represent the conflict.
-            core.reset();
             core.set(c);
             core.log_inference(inference_sup(inf_name, v, c2, c1));
             return c->contains_var(v) ? l_undef : l_true;
@@ -139,15 +138,13 @@ namespace polysat {
         return l_false;
     }
 
-    // TODO(later): check superposition into disequality again (see notes)
     // true = done, false = abort, undef = continue
-    // TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises)
     lbool ex_polynomial_superposition::try_explain1(pvar v, conflict& core) {
         for (auto c2 : core) {
-            if (!c2->contains_var(v))
-                continue;
             if (!c2.is_eq())
                 continue;
+            if (!c2->contains_var(v))
+                continue;
             if (!c2.is_currently_false(s))
                 continue;
             switch (find_replacement(c2, v, core)) {
@@ -162,6 +159,7 @@ namespace polysat {
         return l_false;
     }
 
+#if 0
     void ex_polynomial_superposition::reduce_by(pvar v, conflict& core) {
         bool progress = true;
         while (progress) {
@@ -235,9 +233,12 @@ namespace polysat {
         }
         return false;
     }
+#endif
 
-    bool ex_polynomial_superposition::try_explain(pvar v, conflict& core) {
+    bool ex_polynomial_superposition::perform(pvar v, conflict& core) {
+#if 0
         reduce_by(v, core);
+#endif
         lbool result = l_undef;
         while (result == l_undef)
             result = try_explain1(v, core);
@@ -245,4 +246,3 @@ namespace polysat {
     }
 
 }
-#endif

src/math/polysat/explain.h

@@ -1,15 +1,14 @@
-#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
 
-    Conflict explanation
+    Conflict explanation by polynomial superposition
 
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 --*/
 #pragma once
@@ -22,27 +21,18 @@ namespace polysat {
 
     class solver;
 
-    class explainer {
+    class ex_polynomial_superposition {
-        friend class conflict;
-    protected:
         solver& s;
-    public:
-        explainer(solver& s) :s(s) {}
-        virtual ~explainer() {}
-        virtual bool try_explain(pvar v, conflict& core) = 0;
-    };
 
-    class ex_polynomial_superposition : public explainer {
-    private:
         signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
         lbool find_replacement(signed_constraint c2, pvar v, conflict& core);
         void reduce_by(pvar v, conflict& core);
         bool reduce_by(pvar, signed_constraint c, conflict& core);
         lbool try_explain1(pvar v, conflict& core);
+
     public:
-        ex_polynomial_superposition(solver& s) : explainer(s) {}
+        ex_polynomial_superposition(solver& s) : s(s) {}
-        bool try_explain(pvar v, conflict& core) override;
+        bool perform(pvar v, conflict& core);
     };
 
 }
-#endif

src/math/polysat/saturation.cpp

@@ -97,7 +97,7 @@ namespace polysat {
         if (!inserting)
             return false;
 
-        core.reset();
+        core.remove_all();
         for (auto d : m_new_constraints)
             core.insert_eval(d);
         if (c.bvalue(s) != l_false)  // conflict is due to the evaluation of c, so it depends on the variable values