Polysat: add simpler monotonicity unit test + minor changes (#5348)

* Add simpler versions of monotonicity puzzle

* band-aid fix to conflicts during revert_decision

* minor changes

src/math/polysat/boolean.cpp

@@ -41,7 +41,8 @@ namespace polysat {
         m_level[var] = UINT_MAX;
         m_reason[var] = nullptr;
         m_lemma[var] = nullptr;
-        m_unused.push_back(var);
+        // 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);
     }
 
     void bool_var_manager::assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma) {

src/math/polysat/constraint.h

@@ -93,7 +93,7 @@ namespace polysat {
         unsigned         m_ref_count = 0;
         // bool             m_stored = false;  ///< Whether it has been inserted into the constraint_manager to be tracked by level
         unsigned         m_storage_level;  ///< Controls lifetime of the constraint object. Always a base level (for external dependencies the level at which it was created, and for others the maximum storage level of its external dependencies).
-        unsigned         m_active_level;  ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level.
+        unsigned         m_active_level = UINT_MAX;  ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level.
         ckind_t          m_kind;
         p_dependency_ref m_dep;
         unsigned_vector  m_vars;
@@ -172,7 +172,7 @@ namespace polysat {
         friend class constraint_manager;
 
         unsigned m_ref_count = 0;
-        unsigned m_level;
+        unsigned m_level;  // TODO: this is "storage" level, rename accordingly
         // unsigned m_next_guess = UINT_MAX;  // next guess for enumerative backtracking
         unsigned m_next_guess = 0;  // next guess for enumerative backtracking
         p_dependency_ref m_dep;

src/math/polysat/solver.cpp

@@ -85,6 +85,15 @@ namespace polysat {
     }
 
 #if POLYSAT_LOGGING_ENABLED
+    void solver::log_viable() {
+        // only for small problems
+        if (m_viable.size() < 10) {
+            for (pvar v = 0; v < m_viable.size(); ++v) {
+                log_viable(v);
+            }
+        }
+    }
+
     void solver::log_viable(pvar v) {
         if (size(v) <= 5) {
             vector<rational> xs;
@@ -115,11 +124,7 @@ namespace polysat {
             LOG("Free variables: " << m_free_vars);
             LOG("Assignments:    " << assignment());
             LOG("Conflict:       " << m_conflict);
-            IF_LOGGING({
+            IF_LOGGING(log_viable());
-                for (pvar v = 0; v < m_viable.size(); ++v) {
-                    log_viable(v);
-                }
-            });
 
             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; }
@@ -450,6 +455,12 @@ namespace polysat {
         m_conflict.push_back(&c); 
     }
 
+    void solver::set_conflict(clause& cl) {
+        LOG("Conflict: " << cl);
+        SASSERT(!is_conflict());
+        m_conflict.push_back(&cl);
+    }
+
     void solver::set_conflict(pvar v) {
         SASSERT(!is_conflict());
         m_conflict.append(m_cjust[v]);
@@ -750,11 +761,7 @@ namespace polysat {
     // Guess a literal from the given clause; returns the guessed constraint
     sat::literal solver::decide_bool(clause& lemma) {
         LOG_H3("Guessing literal in lemma: " << lemma);
-        IF_LOGGING({
+        IF_LOGGING(log_viable());
-            for (pvar v = 0; v < m_viable.size(); ++v) {
-                log_viable(v);
-            }
-        });
         LOG("Boolean assignment: " << m_bvars);
 
         auto is_suitable = [this](sat::literal lit) -> bool {
@@ -775,15 +782,32 @@ namespace polysat {
         unsigned num_choices = 0;  // TODO: should probably cache this?
 
         for (sat::literal lit : lemma) {
+            IF_LOGGING({
+                auto value = m_bvars.value(lit);
+                auto c = m_constraints.lookup(lit.var());
+                bool is_false;
+                if (value == l_undef) {
+                    c->assign(!lit.sign());
+                    is_false = c->is_currently_false(*this);
+                    c->unassign();
+                }
+                else
+                    is_false = c->is_currently_false(*this);
+                LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c) << ", currently_false=" << is_false);
+            });
             if (is_suitable(lit)) {
                 num_choices++;
                 if (choice == sat::null_literal)
                     choice = lit;
             }
         }
+        LOG_V("num_choices: " << num_choices);
 
-        SASSERT(choice != sat::null_literal);  // must succeed for at least one
+        if (num_choices == 0)
-        if (num_choices == 1)
+            // 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.
+            set_conflict(lemma);
+        else if (num_choices == 1)
             propagate_bool(choice, &lemma);
         else
             decide_bool(choice, lemma);
@@ -847,19 +871,33 @@ namespace polysat {
 
         add_non_viable(v, val);
 
-        for (constraint* c : m_conflict.units()) {
+        auto confl = std::move(m_conflict);
+        m_conflict.reset();
+
+        for (constraint* c : confl.units()) {
             // Add the conflict as justification for the exclusion of 'val'
             push_cjust(v, c);
             // NOTE: in general, narrow may change the conflict.
             //       But since we just backjumped, narrowing should not result in an additional conflict.
+            // TODO: this call to "narrow" may still lead to a conflict,
+            //       because we do not detect all conflicts immediately.
+            //       Consider:
+            //       - Assert constraint zx > yx, watching y and z.
+            //       - Guess x = 0.
+            //       - We have a conflict but we don't know. It will be discovered when y and z are assigned,
+            //         and then may lead to an assertion failure through this call to narrow.
             c->narrow(*this);
+            if (is_conflict()) {
+                LOG_H1("Conflict during revert_decision/narrow!");
+                return;
             }
-        m_conflict.reset();
+        }
+        // m_conflict.reset();
 
         learn_lemma(v, std::move(reason));
 
         if (is_conflict()) {
-            LOG_H1("Conflict during revert_decision!");
+            LOG_H1("Conflict during revert_decision/learn_lemma!");
             return;
         }
 
@@ -896,6 +934,7 @@ namespace polysat {
             // TODO: what to do when reason is NULL?
             // * this means we were unable to build a lemma for the current conflict.
             // * the reason for reverting this decision then needs to be the (negation of the) conflicting literals. Or we give up on resolving this lemma?
+            // TODO: do not include 'base' unit constraints (only in dependencies)
             SASSERT(m_conflict.clauses().empty());  // not sure how to handle otherwise
             unsigned reason_lvl = m_constraints.lookup(lit.var())->level();
             p_dependency_ref reason_dep(m_constraints.lookup(lit.var())->dep(), m_dm);

src/math/polysat/solver.h

@@ -173,6 +173,8 @@ namespace polysat {
          * (Inefficient, but useful for debugging small instances.)
          */
         void log_viable(pvar v);
+        /** Like log_viable but for all variables */
+        void log_viable();
 
         /**
          * undo trail operations for backtracking.
@@ -214,6 +216,7 @@ namespace polysat {
         void add_watch(constraint& c, pvar v);
 
         void set_conflict(constraint& c);
+        void set_conflict(clause& cl);
         void set_conflict(pvar v);
 
         unsigned_vector m_marks;

src/test/polysat.cpp

@@ -354,15 +354,14 @@ namespace polysat {
      * 
      * We do overflow checks by doubling the base bitwidth here.
      */
-    static void test_monot() {
+    static void test_monot(unsigned base_bw = 5) {
         scoped_solver s(__func__);
 
-        auto baseBw = 5;
+        auto max_int_const = rational::power_of_two(base_bw) - 1;
-        auto max_int_const = 31; // (2^5 - 1) -- change this when you change baseBw
 
-        auto bw = 2 * baseBw;
+        unsigned bw = 2 * base_bw;
         auto max_int = s.var(s.add_var(bw));
-        s.add_eq(max_int - max_int_const);
+        s.add_eq(max_int + (-max_int_const));
 
         auto tb1 = s.var(s.add_var(bw));
         s.add_ule(tb1, max_int);
@@ -499,11 +498,13 @@ namespace polysat {
         s.expect_unsat();
         s.pop();
 
-        s.push();
+        NOT_IMPLEMENTED_YET();  // this is just a note to continue here once we get the above expect_unsat to pass.
-        s.add_ult(quot3 + em, a);
+
-        s.check();
+        // s.push();
-        s.expect_unsat();
+        // s.add_ult(quot3 + em, a);
-        s.pop();
+        // s.check();
+        // s.expect_unsat();
+        // s.pop();
     }
 
     /*
@@ -579,12 +580,69 @@ namespace polysat {
         s.pop();
     }
 
-    /*
+    /** Monotonicity under bounds,
-     * Transcribed from https://github.com/NikolajBjorner/polysat/blob/main/puzzles/bv.smt2 .
+     * puzzle extracted from https://github.com/NikolajBjorner/polysat/blob/main/puzzles/bv.smt2
+     *
+     * x, y, z \in [0..2^64[
+     * x, y, z < 2^32
+     * y <= x
+     * x*z < 2^32
+     * y*z >= 2^32
+     */
+    static void test_monot_bounds(unsigned base_bw = 32) {
+        scoped_solver s(__func__);
+        unsigned bw = 2 * base_bw;
+        auto x = s.var(s.add_var(bw));
+        auto y = s.var(s.add_var(bw));
+        auto z = s.var(s.add_var(bw));
+        auto zero = x - x;
+        auto bound = (zero + 2).pow(base_bw);
+        s.add_ult(x, bound);
+        s.add_ult(y, bound);
+        s.add_ult(z, bound);
+        // TODO: try alternative:
+        // TODO: maybe we should normalize equations where one side is a constant?
+        // TODO: should we always express a < b as a <= b - 1 ?  [ well, no. this only works if b > 0. ]
+        // s.add_ule(x, bound - 1);
+        // s.add_ule(y, bound - 1);
+        // s.add_ule(z, bound - 1);
+        s.add_ule(y, x);
+        s.add_ult(x*z, bound);
+        s.add_ule(bound, y*z);
+        s.check();
+        s.expect_unsat();
+    }
 
+    /** Monotonicity under bounds, simplified even more.
+     *
+     * x, y, z \in [0..2^64[
+     * x, y, z < 2^32
+     * z <= y
+     * y*x < z*x
+     */
+    static void test_monot_bounds_simple(unsigned base_bw = 32) {
+        scoped_solver s(__func__);
+        unsigned bw = 2 * base_bw;
+        auto y = s.var(s.add_var(bw));
+        auto x = s.var(s.add_var(bw));
+        auto z = s.var(s.add_var(bw));
+        auto zero = x - x;
+        auto bound = (zero + 2).pow(base_bw);
+        s.add_ult(x, bound);
+        s.add_ult(y, bound);
+        s.add_ult(z, bound);
+        s.add_ule(z, y);
+        s.add_ult(y*x, z*x);
+        s.check();
+        s.expect_unsat();
+    }
+
+    /*
+     * Transcribed from https://github.com/NikolajBjorner/polysat/blob/main/puzzles/bv.smt2
+     *
      * We do overflow checks by doubling the base bitwidth here.
      */
-    static void test_fixed_point_arith_div_mul_inverse2() {
+    static void test_monot_bounds_full() {
         scoped_solver s(__func__);
 
         auto baseBw = 5;
@@ -686,8 +744,10 @@ void tst_polysat() {
     polysat::test_ineq_basic4();
     polysat::test_ineq_basic5();
     polysat::test_ineq_basic6();
-    polysat::test_fixed_point_arith_div_mul_inverse2();
     polysat::test_fixed_point_arith_div_mul_inverse();
+    polysat::test_monot_bounds_simple(2);
+    polysat::test_monot_bounds(2);
+    polysat::test_monot_bounds_full();
     polysat::test_fixed_point_arith_mul_div_inverse();
 #if 0
     // worry about this later