WIP revamp conflict state

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

src/math/polysat/conflict.cpp

@@ -50,8 +50,7 @@ namespace polysat {
         if (!m_vars.empty())
             out << " vars";
         for (auto v : m_vars)
-            if (is_pmarked(v))
+            out << " v" << v;
-                out << " v" << v;
         return out;
     }
 
@@ -83,7 +82,7 @@ namespace polysat {
         else {
             SASSERT(c.is_currently_false(s));
             // TBD: fails with test_subst       SASSERT(c.bvalue(s) == l_true);
-            c->set_var_dependent();
+            insert_vars(c);
             insert(c);
         }
         SASSERT(!empty());
@@ -140,6 +139,13 @@ namespace polysat {
             m_constraints.push_back(c);
     }
 
+    void conflict::insert_vars(signed_constraint c) {
+        for (pvar v : c->vars()) 
+            if (s.is_assigned(v)) 
+                m_vars.insert(v);  
+    }
+
+
 
     /**
      * Premises can either be justified by a Clause or by a value assignment.
@@ -210,7 +216,7 @@ namespace polysat {
         SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
         
         remove_literal(lit);        
-        unset_bmark(s.lit2cnstr(lit));         
+        unset_mark(s.lit2cnstr(lit));         
         for (sat::literal lit2 : cl)
             if (lit2 != lit)
                 insert(s.lit2cnstr(~lit2));
@@ -229,12 +235,7 @@ namespace polysat {
         remove_literal(lit);
         signed_constraint c = s.lit2cnstr(lit);
         unset_mark(c);
-        for (pvar v : c->vars()) {
+        insert_vars(c);
-            if (s.is_assigned(v) && s.get_level(v) <= lvl) {
-                m_vars.insert(v);  
-                inc_pref(v);
-            }
-        }
     }
 
     /** 
@@ -268,8 +269,6 @@ namespace polysat {
             lemma.push(~c);
 
         for (unsigned v : m_vars) {
-            if (!is_pmarked(v))
-                continue;
             auto eq = s.eq(s.var(v), s.get_value(v));
             cm().ensure_bvar(eq.get());
             if (eq.bvalue(s) == l_undef) 
@@ -406,19 +405,12 @@ namespace polysat {
         c->set_mark();
         if (c->has_bvar())
             set_bmark(c->bvar());    
-        if (c->is_var_dependent()) {
-            for (auto v : c->vars()) {
-                if (s.is_assigned(v))
-                    m_vars.insert(v);
-                inc_pref(v);
-            }
-        }
     }
 
     /**
      * unset marking on the constraint, but keep variable dependencies.
      */
-    void conflict::unset_bmark(signed_constraint c) {
+    void conflict::unset_mark(signed_constraint c) {
         if (!c->is_marked())
             return;
         c->unset_mark();
@@ -426,32 +418,6 @@ namespace polysat {
             unset_bmark(c->bvar());
     }
 
-    void conflict::unset_mark(signed_constraint c) {
-        if (!c->is_marked())
-            return;
-        unset_bmark(c);
-        if (!c->is_var_dependent()) 
-            return;
-        c->unset_var_dependent();
-        for (auto v : c->vars())
-            dec_pref(v);        
-    }
-
-    void conflict::inc_pref(pvar v) {
-        if (v >= m_pvar2count.size())
-            m_pvar2count.resize(v + 1);        
-        m_pvar2count[v]++;
-    }
-
-    void conflict::dec_pref(pvar v) {
-        SASSERT(m_pvar2count[v] > 0);
-        m_pvar2count[v]--;
-    }
-
-    bool conflict::is_pmarked(pvar v) const {
-        return m_pvar2count.get(v, 0) > 0;
-    }
-
     void conflict::set_bmark(sat::bool_var b) {
         if (b >= m_bvar2mark.size())
             m_bvar2mark.resize(b + 1);

src/math/polysat/conflict.h

@@ -10,6 +10,37 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
     Jakob Rath 2021-04-6
 
+Notes:
+
+    A conflict state is of the form <Vars, Constraints>
+    Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignent.
+    
+    The conflict state is unsatisfiable under background clauses F.
+    Dually, the negation is a consequence of F.
+
+    Conflict resolution resolves an assignment in the search stack against the conflict state.
+
+    Assignments are of the form:
+  
+    lit <- D => lit              - lit is propagated by the clause D => lit
+    lit <- ?                     - lit is a decision literal.
+    lit <- asserted              - lit is asserted
+    lit <- Vars                  - lit is propagated from variable evaluation.
+
+    v = value <- Cs              - v is assigned value by constraints Cs
+    v = value <- ?               - v is a decision literal.
+
+    - All literals should be assigned in the stack prior to their use.
+    
+    lit <- D => lit, < Vars, { lit } u Cs >   ===>   < Vars, Cs u D >
+    lit <- ?,        < Vars, { lit } u Cs >   ===>   ~lit <- (Cs & Vars = value(Vars) => ~lit)
+    lit <- asserted, < Vars, { lit } u Cs >   ===>   accumulate lit for a core
+    lit <- Vars',    < Vars, { lit } u Cs >   ===>   ~lit <- (Cs & Vars = value(Vars) => ~lit)
+
+    v = value <- Cs, < Vars u { v }, Cs >     ===>   
+    
+    
+    
 --*/
 #pragma once
 #include "math/polysat/constraint.h"
@@ -77,7 +108,7 @@ namespace polysat {
 
         void reset();
 
-        bool is_pmarked(pvar v) const;
+        bool contains_pvar(pvar v) const { return m_vars.contains(v); }
         bool is_bmarked(sat::bool_var b) const;
 
         /** conflict because the constraint c is false under current variable assignment */
@@ -88,6 +119,7 @@ namespace polysat {
         void set(clause const& cl);
 
         void insert(signed_constraint c);
+        void insert_vars(signed_constraint c);
         void insert(signed_constraint c, vector<signed_constraint> const& premises);
         void remove(signed_constraint c);
         void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);

src/math/polysat/constraint.h

@@ -146,7 +146,6 @@ namespace polysat {
         unsigned_vector     m_vars;
         lbool               m_external_sign = l_undef;
         bool                m_is_marked = false;
-        bool                m_is_var_dependent = false;
         bool                m_is_active = false;
         /** The boolean variable associated to this constraint, if any.
          *  If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
@@ -207,9 +206,6 @@ namespace polysat {
         void unset_mark() { m_is_marked = false; }
         bool is_marked() const { return m_is_marked; }
 
-        void set_var_dependent() { m_is_var_dependent = true; }
-        void unset_var_dependent() { m_is_var_dependent = false; }
-        bool is_var_dependent() const { return m_is_var_dependent;  }
 
         bool is_active() const { return m_is_active; }
         void set_active(bool f) { m_is_active = f; }

src/math/polysat/saturation.cpp

@@ -88,7 +88,7 @@ namespace polysat {
         for (auto d : m_new_constraints)
             core.insert(d);
         if (c.bvalue(s) != l_false)
-            c->set_var_dependent();
+            core.insert_vars(c);
         core.insert(~c);       
         LOG("Core " << core);
         return true;        

src/math/polysat/solver.cpp

@@ -534,7 +534,7 @@ namespace polysat {
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
-                if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) {
+                if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) {
                     m_search.pop_assignment();
                     continue;
                 }

src/math/polysat/viable.cpp

@@ -557,9 +557,10 @@ namespace polysat {
                 signed_constraint c = s.m_constraints.ult(lhs, rhs);
                 core.insert(c);
             }
-            for (auto sc : e->side_cond)
+            for (auto sc : e->side_cond) {
                 core.insert(sc);
-            e->src->set_var_dependent(); 
+                core.insert_vars(sc);
+            }
             core.insert(e->src);
             e = n;
         }