add unsat core, activity, quick pass for viable

src/math/polysat/boolean.h

@@ -56,6 +56,7 @@ namespace polysat {
         unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
         unsigned level(sat::literal lit) const { return level(lit.var()); }
         clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_reason[var]; }
+        unsigned dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
 
         clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; }
        

src/math/polysat/conflict.cpp

@@ -243,6 +243,7 @@ namespace polysat {
         for (unsigned v : m_vars) {
             if (!is_pmarked(v))
                 continue;
+            s.inc_activity(v);
             auto eq = s.eq(s.var(v), s.get_value(v));
             cm().ensure_bvar(eq.get());
             if (eq.bvalue(s) == l_undef) 
@@ -285,7 +286,11 @@ namespace polysat {
     bool conflict::resolve_value(pvar v) {
         // NOTE:
         // In the "standard" case where "v = val" is on the stack:
-        //      - core contains both false and true constraints (originally only false ones, but additional true ones may come from saturation)
+        //      - core contains both false and true constraints 
+        //        (originally only false ones, but additional true ones may come from saturation)
+
+        // forbidden interval projection is performed at top level
+        SASSERT(v != conflict_var());
 
         if (is_bailout()) {
             if (!s.m_justification[v].is_decision())
@@ -293,8 +298,7 @@ namespace polysat {
             return false;
         }
 
-        // forbidden interval projection is performed at top level
-        SASSERT(v != conflict_var());
+        s.inc_activity(v); 
         
         m_vars.remove(v);
 

src/math/polysat/solver.cpp

@@ -147,7 +147,6 @@ namespace polysat {
 #endif
     }
 
-
     bool solver::can_propagate() {
         return m_qhead < m_search.size() && !is_conflict();
     }
@@ -175,6 +174,8 @@ namespace polysat {
         LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
         signed_constraint c = lit2cnstr(lit);
         SASSERT(c);
+        if (c->is_active())
+            return;
         activate_constraint(c);
         auto& wlist = m_bvars.watch(~lit);
         unsigned i = 0, j = 0, sz = wlist.size();
@@ -460,8 +461,7 @@ namespace polysat {
      *    viable solutions by excluding the previous guess.
      *
      */
-    void solver::resolve_conflict() {
-        IF_VERBOSE(1, verbose_stream() << "resolve conflict\n");
+    void solver::resolve_conflict() {        
         LOG_H2("Resolve conflict");
         LOG("\n" << *this);
         LOG("search state: " << m_search);
@@ -521,6 +521,36 @@ namespace polysat {
         return m_conflict.resolve_value(v);
     }
 
+    /**
+    * Variable activity accounting.
+    * As a placeholder we increment activity 
+    * 1. when a variable assignment is used in a conflict.
+    * 2. when a variable propagation is resolved against.
+    * The hypothesis that this is useful should be tested against a 
+    * broader suite of benchmarks and tested with micro-benchmarks.
+    * It should be tested in conjunction with restarts.
+    */
+    void solver::inc_activity(pvar v) {
+        unsigned& act = m_activity[v];
+        act += m_activity_inc;
+        m_free_pvars.activity_increased_eh(v);
+        if (act > (1 << 24))
+            rescale_activity();
+    }
+
+    void solver::decay_activity() {
+        m_activity_inc *= m_variable_decay;
+        m_activity_inc /= 100;
+    }
+
+    void solver::rescale_activity() {
+        for (unsigned& act : m_activity) {
+            act >>= 14;
+        }
+        m_activity_inc >>= 14;
+    }
+
+
     /** Conflict resolution case where boolean literal 'lit' is on top of the stack 
     *   NOTE: boolean resolution should work normally even in bailout mode.
     */
@@ -537,17 +567,12 @@ namespace polysat {
     }
 
     void solver::unsat_core(unsigned_vector& deps) {
-        NOT_IMPLEMENTED_YET();   // TODO: needs to be fixed to work with conflict_core
-        /*
         deps.reset();
-        p_dependency_ref conflict_dep(m_dm);
-        for (auto& c : m_conflict.units())
-            if (c)
-                conflict_dep = m_dm.mk_join(c->unit_dep(), conflict_dep);
-        for (auto& c : m_conflict.clauses())
-            conflict_dep = m_dm.mk_join(c->dep(), conflict_dep);
-        m_dm.linearize(conflict_dep, deps);
-        */
+        for (auto c : m_conflict) {
+            auto d = m_bvars.dep(c.blit());
+            if (d != null_dependency)
+                deps.push_back(d);
+        }
     }
 
     void solver::learn_lemma(clause& lemma) {

src/math/polysat/solver.h

@@ -189,6 +189,13 @@ namespace polysat {
         void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);
 
+        // activity of variables based on standard VSIDS
+        unsigned m_activity_inc = 128;
+        unsigned m_variable_decay = 110;
+        void inc_activity(pvar v);
+        void decay_activity();
+        void rescale_activity();
+
         void report_unsat();
         void learn_lemma(clause& lemma);
         void backjump(unsigned new_level);
@@ -198,7 +205,7 @@ namespace polysat {
         void simplify();
 
         unsigned m_conflicts_at_restart = 0;
-        unsigned m_restart_threshold = UINT_MAX;
+        unsigned m_restart_threshold = 100;
         unsigned m_restart_init = 100;
         unsigned m_luby_idx = 0;
         bool should_restart();

src/math/polysat/viable.cpp

@@ -10,6 +10,14 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
     Jakob Rath 2021-04-6
 
+Notes:
+
+TODO: Investigate in depth a notion of phase caching for variables.
+The Linear solver can be used to supply a phase in some cases.
+In other cases, the phase of a variable assignment across branches
+might be used in a call to is_viable. With phase caching on, it may
+just check if the cached phase is viable without detecting that it is a propagation.
+
 --*/
 
 
@@ -17,7 +25,6 @@ Author:
 #include "math/polysat/viable.h"
 #include "math/polysat/solver.h"
 
-
 namespace polysat {
 
     viable::viable(solver& s) : s(s) {}
@@ -139,6 +146,13 @@ namespace polysat {
         if (!e)
             return true;
         entry* first = e;
+        entry* last = e->prev();
+
+        // quick check: last interval doesn't wrap around, so hi_val
+        // has not been covered
+        if (last->interval.lo_val() < last->interval.hi_val())
+            return true;
+
         auto const& max_value = s.var2pdd(v).max_value();
         do {
             if (e->interval.is_full())
@@ -221,6 +235,17 @@ namespace polysat {
 
         entry* first = e;
         entry* last = first->prev();
+
+        // quick check: last interval does not wrap around
+        // and has space for 2 unassigned values.
+        auto& max_value = s.var2pdd(v).max_value();
+        if (last->interval.lo_val() < last->interval.hi_val() &&
+            last->interval.hi_val() < max_value) {
+            lo = last->interval.hi_val();
+            return dd::find_t::multiple;
+        }
+
+        // find lower bound
         if (last->interval.currently_contains(lo))
             lo = last->interval.hi_val();
         do {
@@ -234,7 +259,8 @@ namespace polysat {
         if (e->interval.currently_contains(lo))
             return dd::find_t::empty;
 
-        rational hi = s.var2pdd(v).max_value();
+        // find upper bound
+        rational hi = max_value;
         e = last;
         do {
             if (!e->interval.currently_contains(hi))
@@ -271,7 +297,7 @@ namespace polysat {
             }
             for (auto sc : e->side_cond)
                 core.insert(sc);
-            e->src->set_var_dependent(); // ?
+            e->src->set_var_dependent(); 
             core.insert(e->src);
             e = n;
         }             

src/test/polysat.cpp

@@ -318,7 +318,7 @@ namespace polysat {
         s.add_eq(n*q1 - a + b);
         s.add_eq(n*q2 + r2 - c*a + c*b);
         s.add_ult(r2, n);
-        s.add_diseq(n);
+        s.add_diseq(r2);
         s.check();
         s.expect_unsat();
     }
@@ -1067,19 +1067,7 @@ namespace polysat {
 
 void tst_polysat() {
 
- //   polysat::test_ineq_axiom1();
- //   polysat::test_ineq_axiom2();
- //   polysat::test_ineq_axiom3();
- //   polysat::test_ineq_non_axiom1();
-#if 0
-    polysat::test_ineq_non_axiom4(32, 5);
-    polysat::test_ineq_axiom4();
-    polysat::test_ineq_axiom5();
-    polysat::test_ineq_axiom6();
-#endif
 
-    // working
-    // NOT: polysat::test_fixed_point_arith_mul_div_inverse();
             
     // polysat::test_monot_bounds(8);
 
@@ -1107,6 +1095,10 @@ void tst_polysat() {
 
     polysat::test_var_minimize();
 
+    polysat::test_ineq1();
+    polysat::test_ineq2();
+    polysat::test_monot();
+
     return;
 
     polysat::test_ineq_axiom1();
@@ -1115,22 +1107,15 @@ void tst_polysat() {
     polysat::test_ineq_axiom4();
     polysat::test_ineq_axiom5();
     polysat::test_ineq_axiom6();
+#if 0
+    polysat::test_ineq_non_axiom4(32, 5);
+#endif
 
     // inefficient conflicts:
     // Takes time: polysat::test_monot_bounds_full();
 
-#if 0
-    // worry about this later
-    polysat::test_ineq1();
-    polysat::test_ineq2();
-#endif
-
-    // not working
     polysat::test_monot_bounds_simple(8);
     polysat::test_fixed_point_arith_div_mul_inverse();
-    polysat::test_monot();
-    polysat::test_ineq2();
-    polysat::test_ineq1();
 
 }