adding watches on Booleans

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

src/math/polysat/boolean.cpp

@@ -24,6 +24,8 @@ namespace polysat {
             m_level.push_back(UINT_MAX);
             m_reason.push_back(nullptr);
             m_lemma.push_back(nullptr);
+            m_watch.push_back({});
+            m_watch.push_back({});
             return var;
         }
         else {
@@ -46,6 +48,8 @@ namespace polysat {
         m_level[var] = UINT_MAX;
         m_reason[var] = nullptr;
         m_lemma[var] = nullptr;
+        m_watch[lit.index()].reset();
+        m_watch[(~lit).index()].reset();
         // TODO: this is disabled for now, since re-using variables for different constraints may be confusing during debugging. Should be enabled later.
         // m_unused.push_back(var);
     }

src/math/polysat/boolean.h

@@ -22,11 +22,14 @@ namespace polysat {
         svector<sat::bool_var>  m_unused;   // previously deleted variables that can be reused by new_var();
         svector<lbool>          m_value;    // current value (indexed by literal)
         svector<unsigned>       m_level;    // level of assignment (indexed by variable)
+        unsigned_vector         m_activity; // 
         svector<clause*>        m_reason;   // propagation reason, NULL for decisions (indexed by variable)
 
         // For enumerative backtracking we store the lemma we're handling with a certain decision
         svector<clause*>        m_lemma;
 
+        vector<ptr_vector<clause>>  m_watch;      // watch list for literals into clauses
+
     public:
         // allocated size (not the number of active variables)
         unsigned size() const { return m_level.size(); }
@@ -41,12 +44,17 @@ namespace polysat {
         bool is_propagation(sat::bool_var var) const { return is_assigned(var) && reason(var); }
         lbool value(sat::bool_var var) const { return value(sat::literal(var)); }
         lbool value(sat::literal lit) const { return m_value[lit.index()]; }
+        bool is_true(sat::literal lit) const { return value(lit) == l_true; }
+        bool is_false(sat::literal lit) const { return value(lit) == l_false; }
         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]; }
 
         clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; }
 
+        ptr_vector<clause>& watch(sat::literal lit) { return m_watch[lit.index()]; }
+        unsigned_vector& activity() { return m_activity; }
+
         /// Set the given literal to true
         void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma);
         void unassign(sat::literal lit);

src/math/polysat/clause.h

@@ -36,8 +36,10 @@ namespace polysat {
         unsigned m_level;
         pvar m_justified_var = null_var;  // The variable that was restricted by learning this lemma.
         p_dependency_ref m_dep;
+        bool m_redundant = false;
         sat::literal_vector m_literals;
 
+
         /* TODO: embed literals to save an indirection?
         unsigned m_num_literals;
         constraint* m_literals[0];
@@ -68,6 +70,7 @@ namespace polysat {
         bool empty() const { return m_literals.empty(); }
         unsigned size() const { return m_literals.size(); }
         sat::literal operator[](unsigned idx) const { return m_literals[idx]; }
+        sat::literal& operator[](unsigned idx) { return m_literals[idx]; }
 
         using const_iterator = typename sat::literal_vector::const_iterator;
         const_iterator begin() const { return m_literals.begin(); }
@@ -77,6 +80,9 @@ namespace polysat {
         bool is_currently_false(solver& s) const;
 
         std::ostream& display(std::ostream& out) const;
+
+        void set_redundant(bool r) { m_redundant = r; }
+        bool is_redundant() const { return m_redundant; }
     };
 
     inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }

src/math/polysat/log.h

@@ -75,6 +75,7 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
 #define LOG_H3(x) LOG_INDENT(LogLevel::Heading3, x)
 #define LOG(x)    LOG_(LogLevel::Default , x)
 #define LOG_V(x)  LOG_(LogLevel::Verbose , x)
+#define COND_LOG(c, x) if (c) LOG(x)
 
 #define IF_LOGGING(x) \
   do {                \

src/math/polysat/solver.cpp

@@ -40,8 +40,9 @@ namespace polysat {
         m_dm(m_value_manager, m_alloc),
         m_linear_solver(*this),
         m_conflict(*this),
-        m_free_vars(m_activity),
         m_bvars(),
+        m_free_pvars(m_activity),
+        m_free_bvars(m_bvars.activity()),
         m_constraints(m_bvars) {
     }
 
@@ -63,12 +64,11 @@ namespace polysat {
         while (inc()) {
             m_stats.m_num_iterations++;
             LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
-            LOG("Free variables: " << m_free_vars);
+            LOG("Free variables: " << m_free_pvars);
             LOG("Assignment:     " << assignments_pp(*this));
-            if (!m_conflict.empty()) LOG("Conflict:       " << m_conflict);
+            COND_LOG(is_conflict(), "Conflict:       " << m_conflict);
             IF_LOGGING(m_viable.log());
             if (!is_conflict() && m_constraints.should_gc()) m_constraints.gc(*this);
-
             if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; }
             else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
             else if (is_conflict()) resolve_conflict();
@@ -86,12 +86,12 @@ namespace polysat {
         m_justification.push_back(justification::unassigned());
         m_viable.push(sz);
         m_cjust.push_back({});
-        m_watch.push_back({});
+        m_pwatch.push_back({});
         m_activity.push_back(0);
         m_vars.push_back(sz2pdd(sz).mk_var(v));
         m_size.push_back(sz);
         m_trail.push_back(trail_instr_t::add_var_i);
-        m_free_vars.mk_var_eh(v);
+        m_free_pvars.mk_var_eh(v);
         return v;
     }
 
@@ -106,11 +106,11 @@ namespace polysat {
         m_cjust.pop_back();
         m_value.pop_back();
         m_justification.pop_back();
-        m_watch.pop_back();
+        m_pwatch.pop_back();
         m_activity.pop_back();
         m_vars.pop_back();
         m_size.pop_back();
-        m_free_vars.del_var_eh(v);
+        m_free_pvars.del_var_eh(v);
     }
 
     signed_constraint solver::eq(pdd const& p) {
@@ -146,8 +146,7 @@ namespace polysat {
         m_constraints.ensure_bvar(c.get());
         clause* unit = m_constraints.store(clause::from_unit(m_level, c, mk_dep_ref(dep)));
         c->set_unit_clause(unit);
-        if (dep != null_dependency)
+        if (dep != null_dependency && !c->is_external()) {
-            if (!c->is_external()) {
             m_constraints.register_external(c);
             m_trail.push_back(trail_instr_t::ext_constraint_i);
             m_ext_constraint_trail.push_back(c.get());
@@ -200,10 +199,45 @@ namespace polysat {
         }
         linear_propagate();
         SASSERT(wlist_invariant());
-        if (!is_conflict())
         SASSERT(assignment_invariant());
     }
 
+    void solver::propagate_watch(sat::literal lit) {
+        auto& wlist = m_bvars.watch(~lit);
+        unsigned end = 0;
+        unsigned sz = wlist.size();
+        bool flush = false;
+        for (unsigned j = 0; j < sz && !is_conflict(); ++j) {
+            clause& cl = *wlist[j];
+            SASSERT(cl.size() >= 2);
+            unsigned idx = cl[0] == lit ? 1 : 0;
+            SASSERT(cl[1 - idx] == lit);
+            if (flush || m_bvars.is_true(cl[idx])) {
+                wlist[end++] = &cl;
+                continue;
+            }
+            unsigned i = 2;
+            for (; i < cl.size() && m_bvars.is_false(cl[i]); ++i);
+            if (i < cl.size()) {
+                m_bvars.watch(cl[i]).push_back(&cl);
+                std::swap(cl[1 - idx], cl[i]);
+                continue;
+            }
+            wlist[end++] = &cl;
+            if (m_bvars.is_false(cl[idx])) {
+                set_conflict(cl);
+                flush = true;
+                continue;
+            }
+            unsigned level = 0;
+            for (i = 0; i < cl.size(); ++i)
+                if (cl[i] != lit)
+                    level = std::max(level, m_bvars.level(cl[i]));
+            assign_bool(level, cl[1 - idx], &cl, nullptr);
+        }
+        wlist.shrink(end);
+    }
+
     void solver::linear_propagate() {
 #if ENABLE_LINEAR_SOLVER
         switch (m_linear_solver.check()) {
@@ -221,11 +255,12 @@ namespace polysat {
         signed_constraint c = m_constraints.lookup(lit);
         SASSERT(c);
         activate_constraint(c);
+        propagate_watch(lit);
     }
 
     void solver::propagate(pvar v) {
         LOG_H2("Propagate v" << v);
-        auto& wlist = m_watch[v];
+        auto& wlist = m_pwatch[v];
         unsigned i = 0, j = 0, sz = wlist.size();
         for (; i < sz && !is_conflict(); ++i) 
             if (!wlist[i].propagate(*this, v))
@@ -238,7 +273,7 @@ namespace polysat {
     void solver::propagate(pvar v, rational const& val, signed_constraint c) {
         LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c);
         if (m_viable.is_viable(v, val)) {
-            m_free_vars.del_var_eh(v);
+            m_free_pvars.del_var_eh(v);
             assign_core(v, val, justification::propagation(m_level));        
         }
         else 
@@ -288,7 +323,7 @@ namespace polysat {
             case trail_instr_t::assign_i: {
                 auto v = m_search.back().var();
                 LOG_V("Undo assign_i: v" << v);
-                m_free_vars.unassign_var_eh(v);
+                m_free_pvars.unassign_var_eh(v);
                 m_justification[v] = justification::unassigned();
                 m_search.pop();
                 break;
@@ -344,7 +379,7 @@ namespace polysat {
     void solver::add_watch(signed_constraint c, pvar v) {
         SASSERT(c);
         LOG("Watching v" << v << " in constraint " << c);
-        m_watch[v].push_back(c);
+        m_pwatch[v].push_back(c);
     }
 
     void solver::erase_watch(signed_constraint c) {
@@ -358,7 +393,7 @@ namespace polysat {
     void solver::erase_watch(pvar v, signed_constraint c) {
         if (v == null_var)
             return;
-        auto& wlist = m_watch[v];
+        auto& wlist = m_pwatch[v];
         unsigned sz = wlist.size();
         for (unsigned i = 0; i < sz; ++i) {
             if (c == wlist[i]) {
@@ -372,10 +407,13 @@ namespace polysat {
     void solver::decide() {
         LOG_H2("Decide");
         SASSERT(can_decide());
-        decide(m_free_vars.next_var());
+        if (!m_free_bvars.empty())
+            bdecide(m_free_bvars.next_var());
+        else
+            pdecide(m_free_pvars.next_var());
     }
 
-    void solver::decide(pvar v) {
+    void solver::pdecide(pvar v) {
         LOG("Decide v" << v);
         IF_LOGGING(m_viable.log(v));
         rational val;
@@ -384,7 +422,7 @@ namespace polysat {
             // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing)
             //       (fail here in debug mode so we notice if we miss some)
             DEBUG_CODE( UNREACHABLE(); );
-            m_free_vars.unassign_var_eh(v);
+            m_free_pvars.unassign_var_eh(v);
             set_conflict(v);
             break;
         case dd::find_t::singleton:
@@ -398,6 +436,10 @@ namespace polysat {
         }
     }
 
+    void solver::bdecide(sat::bool_var b) {
+
+    }
+
     void solver::assign_core(pvar v, rational const& val, justification const& j) {
         if (j.is_decision()) 
             ++m_stats.m_num_decisions;
@@ -424,6 +466,11 @@ namespace polysat {
         m_conflict.set(v);
     }
 
+    void solver::set_conflict(clause& cl) {
+        for (auto lit : cl)
+            set_conflict(~m_constraints.lookup(lit));
+    }
+
     /**
      * Conflict resolution.
      * - m_conflict are constraints that are infeasible in the current assignment.
@@ -576,8 +623,7 @@ namespace polysat {
         if (choice == sat::null_literal) {
             // This case may happen when all undefined literals are false under the current variable assignment.
             // TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case.
-            for (auto lit : lemma) 
+            set_conflict(lemma);
-                set_conflict(~m_constraints.lookup(lit));
             return;
         }
 
@@ -694,8 +740,7 @@ namespace polysat {
         assign_bool(level, lit, reason, nullptr);
     }
 
-    /// Assign a boolean literal and put it on the search stack,
+    /// Assign a boolean literal and put it on the search stack
-    /// and activate the corresponding constraint.
     void solver::assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma) {
         LOG("Assigning boolean literal: " << lit);
         m_bvars.assign(lit, level, reason, lemma);
@@ -804,7 +849,7 @@ namespace polysat {
     }
 
     std::ostream& solver::display(std::ostream& out) const {
-        out << "Assignment:\n";
+        out << "Search Stack:\n";
         for (auto item : m_search) {
             if (item.is_assignment()) {
                 pvar v = item.var();
@@ -894,7 +939,7 @@ namespace polysat {
             bool is_positive = value == l_true;
             int64_t num_watches = 0;
             signed_constraint sc(c, is_positive);
-            for (auto const& wlist : m_watch) {
+            for (auto const& wlist : m_pwatch) {
                 auto n = std::count(wlist.begin(), wlist.end(), sc);
                 VERIFY(n <= 1);  // no duplicates in the watchlist
                 num_watches += n;
@@ -909,14 +954,22 @@ namespace polysat {
 
     /** Check that boolean assignment and constraint evaluation are consistent */
     bool solver::assignment_invariant() {
+        if (is_conflict())
+            return true;
+        bool ok = true;
         for (sat::bool_var v = m_bvars.size(); v-- > 0; ) {
             sat::literal lit(v);            
-            if (m_bvars.value(lit) == l_true)
+            auto c = m_constraints.lookup(lit);  
-                SASSERT(!m_constraints.lookup(lit).is_currently_false(*this));
+            if (!std::all_of(c->vars().begin(), c->vars().end(), [&](auto v) { return is_assigned(v); }))
-            if (m_bvars.value(lit) == l_false)
+                continue;
-                SASSERT(!m_constraints.lookup(lit).is_currently_true(*this));
+            ok &= (m_bvars.value(lit) != l_true) || !c.is_currently_false(*this);
+            ok &= (m_bvars.value(lit) != l_false) || !c.is_currently_true(*this);
+            if (!ok) {
+                LOG("assignment invariant is broken " << v << "\n" << *this);
+                break;
             }
-        return true;
+        }
+        return ok;
     }
 
     /// Check that all constraints on the stack are satisfied by the current model.

src/math/polysat/solver.h

@@ -74,15 +74,15 @@ namespace polysat {
         poly_dep_manager         m_dm;
         linear_solver            m_linear_solver;
         conflict_core            m_conflict;        
-        // constraints              m_stash_just;
+        bool_var_manager         m_bvars;       // Map boolean variables to constraints
-        var_queue                m_free_vars;
+        var_queue                m_free_pvars;  // free poly vars
+        var_queue                m_free_bvars;  // free Boolean variables
         stats                    m_stats;
 
-        uint64_t                 m_max_conflicts { std::numeric_limits<uint64_t>::max() };
+        uint64_t                 m_max_conflicts = std::numeric_limits<uint64_t>::max();
-        uint64_t                 m_max_decisions { std::numeric_limits<uint64_t>::max() };
+        uint64_t                 m_max_decisions = std::numeric_limits<uint64_t>::max();
+
 
-        // Map boolean variables to constraints
-        bool_var_manager         m_bvars;
 
         // Per constraint state
         constraint_manager       m_constraints;
@@ -93,7 +93,8 @@ namespace polysat {
         vector<rational>         m_value;         // assigned value
         vector<justification>    m_justification; // justification for variable assignment
         vector<signed_constraints> m_cjust;       // constraints justifying variable range.
-        vector<signed_constraints> m_watch;    // watch list datastructure into constraints.
+        vector<signed_constraints> m_pwatch;      // watch list datastructure into constraints.
+
         unsigned_vector          m_activity; 
         vector<pdd>              m_vars;
         unsigned_vector          m_size;     // store size of variables.
@@ -168,17 +169,20 @@ namespace polysat {
         void propagate(sat::literal lit);
         void propagate(pvar v);
         void propagate(pvar v, rational const& val, signed_constraint c);
+        void propagate_watch(sat::literal lit);
         void erase_watch(pvar v, signed_constraint c);
         void erase_watch(signed_constraint c);
         void add_watch(signed_constraint c);
         void add_watch(signed_constraint c, pvar v);
 
         void set_conflict(signed_constraint c);
+        void set_conflict(clause& cl);
         void set_conflict(pvar v);
 
-        bool can_decide() const { return !m_free_vars.empty(); }
+        bool can_decide() const { return !m_free_pvars.empty() || !m_free_bvars.empty(); }
         void decide();
-        void decide(pvar v);
+        void pdecide(pvar v);
+        void bdecide(sat::bool_var b);
 
         void narrow(pvar v);
         void linear_propagate();

src/test/polysat.cpp

@@ -869,8 +869,8 @@ namespace polysat {
 void tst_polysat() {
     // not working
     // polysat::test_fixed_point_arith_div_mul_inverse();
-    polysat::test_cjust();
+    // polysat::test_cjust();
-    //polysat::test_monot_bounds_simple(8);
+    polysat::test_monot_bounds_simple(8);
     return;