remove justified vars

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

src/math/polysat/clause.h

@@ -33,7 +33,6 @@ namespace polysat {
         friend class constraint_manager;
 
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
-        pvar m_justified_var = null_var;  // The variable that was restricted by learning this lemma.
         bool m_redundant = false;
         sat::literal_vector m_literals;
 
@@ -60,9 +59,6 @@ namespace polysat {
         static clause_ref from_literals(sat::literal_vector literals);
 
 
-        pvar justified_var() const { return m_justified_var; }
-        void set_justified_var(pvar v) { SASSERT(m_justified_var == null_var); m_justified_var = v; }
-
         bool empty() const { return m_literals.empty(); }
         unsigned size() const { return m_literals.size(); }
         sat::literal operator[](unsigned idx) const { return m_literals[idx]; }

src/math/polysat/solver.cpp

@@ -20,18 +20,14 @@ Author:
 #include "math/polysat/explain.h"
 #include "math/polysat/log.h"
 #include "math/polysat/variable_elimination.h"
+#include "util/luby.h"
 
 // For development; to be removed once the linear solver works well enough
 #define ENABLE_LINEAR_SOLVER 0
 
 namespace polysat {
 
-    dd::pdd_manager& solver::sz2pdd(unsigned sz) {
+
-        m_pdd.reserve(sz + 1);
-        if (!m_pdd[sz]) 
-            m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz));
-        return *m_pdd[sz];
-    }
 
     solver::solver(reslimit& lim): 
         m_lim(lim),
@@ -73,16 +69,29 @@ namespace polysat {
             LOG("Assignment:     " << assignments_pp(*this));
             if (is_conflict()) LOG("Conflict:       " << m_conflict);
             IF_LOGGING(m_viable.log());
-            if (!is_conflict() && m_constraints.should_gc()) m_constraints.gc(*this);
+            if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
-            else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
             else if (is_conflict()) resolve_conflict();
             else if (can_propagate()) propagate();
             else if (!can_decide()) { LOG_H2("SAT"); SASSERT(verify_sat()); return l_true; }
+            else if (m_constraints.should_gc()) m_constraints.gc(*this);
+            else if (should_simplify()) simplify();
+            else if (should_restart()) restart();
             else decide();
         }
         LOG_H2("UNDEF (resource limit)");
         return l_undef;
     }
+
+    dd::pdd_manager& solver::sz2pdd(unsigned sz) {
+        m_pdd.reserve(sz + 1);
+        if (!m_pdd[sz])
+            m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz));
+        return *m_pdd[sz];
+    }
+
+    dd::pdd_manager& solver::var2pdd(pvar v) {
+        return sz2pdd(size(v));
+    }
         
     unsigned solver::add_var(unsigned sz) {
         pvar v = m_value.size();
@@ -136,7 +145,6 @@ namespace polysat {
 #if ENABLE_LINEAR_SOLVER
         m_linear_solver.new_constraint(*c.get());
 #endif
-
     }
 
 
@@ -243,6 +251,37 @@ namespace polysat {
 #endif
     }
 
+    /*
+    * This is a place holder for in-processing simplification
+    */
+    bool solver::should_simplify() {
+        return false;
+    }
+
+    void solver::simplify() {
+
+    }
+
+    /*
+    * Basic restart functionality.
+    * restarts make more sense when the order of variable 
+    * assignments and the values assigned to variables can be diversified.
+    */
+    bool solver::should_restart() {
+        if (m_stats.m_num_conflicts - m_conflicts_at_restart < m_restart_threshold)
+            return false;
+        if (base_level() + 2 > m_level)
+            return false;
+        return true;        
+    }
+
+    void solver::restart() {
+        ++m_stats.m_num_restarts;
+        pop_levels(m_level - base_level());
+        m_conflicts_at_restart = m_stats.m_num_conflicts;
+        m_restart_threshold = m_restart_init * get_luby(++m_luby_idx);
+    }
+
     void solver::pop_levels(unsigned num_levels) {
         if (num_levels == 0)
             return;
@@ -518,10 +557,9 @@ namespace polysat {
         */
     }
 
-    void solver::learn_lemma(pvar v, clause& lemma) {
+    void solver::learn_lemma(clause& lemma) {
         LOG("Learning: "<< lemma);
         SASSERT(!lemma.empty());
-        lemma.set_justified_var(v);
         add_lemma(lemma);
         if (!is_conflict())
             decide_bool(lemma);
@@ -566,7 +604,6 @@ namespace polysat {
         signed_constraint c = lit2cnstr(choice);
         if (num_choices > 1)
             push_level();        
-        push_cjust(lemma.justified_var(), c);
 
         if (num_choices == 1)
             assign_propagate(choice, lemma);
@@ -594,8 +631,8 @@ namespace polysat {
         
         // The justification for this restriction is the guessed constraint from the lemma.
         // cjust[v] will be updated accordingly by decide_bool.
-        m_viable.add_non_viable(v, val);
+        // m_viable.add_non_viable(v, val);
-        learn_lemma(v, *lemma);
+        learn_lemma(*lemma);
 
         if (!is_conflict())
             narrow(v);
@@ -831,6 +868,7 @@ namespace polysat {
         st.update("polysat conflicts",    m_stats.m_num_conflicts);
         st.update("polysat bailouts",     m_stats.m_num_bailouts);
         st.update("polysat propagations", m_stats.m_num_propagations);
+        st.update("polysat restarts",     m_stats.m_num_restarts);
     }
 
     bool solver::invariant() {

src/math/polysat/solver.h

@@ -44,6 +44,7 @@ namespace polysat {
             unsigned m_num_propagations;
             unsigned m_num_conflicts;
             unsigned m_num_bailouts;
+            unsigned m_num_restarts;
             void reset() { memset(this, 0, sizeof(*this)); }
             stats() { reset(); }
         };
@@ -140,6 +141,7 @@ namespace polysat {
         void del_var();
 
         dd::pdd_manager& sz2pdd(unsigned sz);
+        dd::pdd_manager& var2pdd(pvar v);
 
         void push_level();
         void pop_levels(unsigned num_levels);
@@ -195,10 +197,20 @@ namespace polysat {
         void revert_bool_decision(sat::literal lit);
 
         void report_unsat();
-        void learn_lemma(pvar v, clause& lemma);
+        void learn_lemma(clause& lemma);
         void backjump(unsigned new_level);
         void add_lemma(clause& lemma);
 
+        bool should_simplify();
+        void simplify();
+
+        unsigned m_conflicts_at_restart = 0;
+        unsigned m_restart_threshold = UINT_MAX;
+        unsigned m_restart_init = 100;
+        unsigned m_luby_idx = 0;
+        bool should_restart();
+        void restart();
+
         signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
         void assert_constraint(signed_constraint c, unsigned dep);
         static void insert_constraint(signed_constraints& cs, signed_constraint c);

src/math/polysat/viable2.cpp

@@ -138,7 +138,7 @@ namespace polysat {
         if (!e)
             return true;
         entry* first = e;
-        auto const& max_value = s.m_pdd[v]->max_value();
+        auto const& max_value = s.var2pdd(v).max_value();
         do {
             if (e->interval.is_full())
                 return false;
@@ -174,10 +174,10 @@ namespace polysat {
 
     void viable2::add_non_viable(pvar v, rational const& lo_val, signed_constraint const& c) { 
         entry* ne = alloc_entry();
-        rational const& max_value = s.m_pdd[v]->max_value();
+        rational const& max_value = s.var2pdd(v).max_value();
         rational hi_val = (lo_val == max_value) ? rational::zero() : lo_val + 1;
-        pdd lo = s.m_pdd[v]->mk_val(lo_val);
+        pdd lo = s.var2pdd(v).mk_val(lo_val);
-        pdd hi = s.m_pdd[v]->mk_val(hi_val);
+        pdd hi = s.var2pdd(v).mk_val(hi_val);
         ne->interval = eval_interval::proper(lo, lo_val, hi, hi_val); 
         ne->src = c;     
         intersect(v, ne);
@@ -204,7 +204,7 @@ namespace polysat {
     }
 
     rational viable2::max_viable(pvar v) { 
-        rational hi = s.m_pdd[s.size(v)]->max_value();
+        rational hi = s.var2pdd(v).max_value();
         auto* e = m_viable[v];
         if (!e)
             return hi;
@@ -244,7 +244,7 @@ namespace polysat {
         if (e->interval.currently_contains(lo))
             return dd::find_t::empty;
 
-        rational hi = s.m_pdd[s.size(v)]->max_value();
+        rational hi = s.var2pdd(v).max_value();
         e = last;
         do {
             if (!e->interval.currently_contains(hi))