Solve boolean skeleton first

src/math/polysat/solver.cpp

@@ -278,6 +278,7 @@ namespace polysat {
             sc.narrow(*this, false);
         } else {
             // constraint state: active but unassigned (bvalue undef, but pwatch is set; e.g., new constraints generated for lemmas)
+#if 1
             if (c->vars().size() >= 2) {
                 unsigned other_v = c->var(1 - idx);
                 // Wait for the remaining variable to be assigned
@@ -293,6 +294,19 @@ namespace polysat {
                 SASSERT(sc.is_currently_false(*this));
                 assign_eval(~sc.blit());
             }
+#else
+            signed_constraint sc(c, true);
+            switch (sc.eval(*this)) {
+                case l_true:
+                    assign_eval(sc.blit());
+                    break;
+                case l_false:
+                    assign_eval(~sc.blit());
+                    break;
+                default:
+                    break;
+            }
+#endif
         }
         return false;
     }
@@ -559,6 +573,22 @@ namespace polysat {
     void solver::decide() {
         LOG_H2("Decide");
         SASSERT(can_decide());
+#if 1
+        // Simple hack to try deciding the boolean skeleton first
+        if (!can_bdecide()) {
+            // enqueue all not-yet-true clauses
+            for (auto const& cls : m_constraints.clauses()) {
+                for (auto const& cl : cls) {
+                    bool is_true = any_of(*cl, [&](sat::literal lit) { return m_bvars.is_true(lit); });
+                    if (is_true)
+                        continue;
+                    size_t undefs = count_if(*cl, [&](sat::literal lit) { return !m_bvars.is_assigned(lit); });
+                    if (undefs >= 2)
+                        m_lemmas.push_back(cl.get());
+                }
+            }
+        }
+#endif
         if (can_bdecide())
             bdecide();
         else

src/test/polysat.cpp

@@ -632,8 +632,6 @@ namespace polysat {
         // 8 * x + 3 == 0 is unsat
         static void test_parity1() {
             scoped_solver s(__func__);
-            simplify_clause simp(s);
-            clause_builder cb(s);
             auto x = s.var(s.add_var(8));
             auto y = s.var(s.add_var(8));
             auto z = s.var(s.add_var(8));
@@ -644,11 +642,23 @@ namespace polysat {
             s.expect_unsat();
         }
 
+        // 8 * u * x + 3 == 0 is unsat
+        static void test_parity1b() {
+            scoped_solver s(__func__);
+            auto u = s.var(s.add_var(8));
+            auto x = s.var(s.add_var(8));
+            auto y = s.var(s.add_var(8));
+            auto z = s.var(s.add_var(8));
+            s.add_clause({s.eq(u * x * y + z), s.eq(u * x * y + 5)}, false);
+            s.add_eq(y, 8);
+            s.add_eq(z, 3);
+            s.check();
+            s.expect_unsat();
+        }
+
         // 8 * x + 4 == 0 is unsat
         static void test_parity2() {
             scoped_solver s(__func__);
-            simplify_clause simp(s);
-            clause_builder cb(s);
             auto x = s.var(s.add_var(8));
             auto y = s.var(s.add_var(8));
             s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false);
@@ -660,8 +670,6 @@ namespace polysat {
         // x * y + 4 == 0 & 16 divides y is unsat
         static void test_parity3() {
             scoped_solver s(__func__);
-            simplify_clause simp(s);
-            clause_builder cb(s);
             auto x = s.var(s.add_var(8));
             auto y = s.var(s.add_var(8));
             s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false);
@@ -1628,25 +1636,10 @@ void tst_polysat() {
     collect_test_records = false;
     test_max_conflicts = 50;
     test_polysat::test_parity1();
-//    test_polysat::test_parity2();
+    // test_polysat::test_parity1b();
-//  test_polysat::test_parity3();
+    // test_polysat::test_parity2();
-    return;
+    // test_polysat::test_parity3();
-    // test_polysat::test_band5();
+    // test_polysat::test_ineq2();
-    // test_polysat::test_band5_clause();
-    // test_polysat::test_ineq_axiom1(32, 1);
-    // test_polysat::test_pop_conflict();
-    // test_polysat::test_l2();
-    // test_polysat::test_ineq1();
-    test_polysat::test_ineq2();
-    // test_polysat::test_quot_rem();
-    // test_polysat::test_ineq_non_axiom1(32, 3);
-    // test_polysat::test_monot_bounds_full();
-    // test_polysat::test_band2();
-    // test_polysat::test_quot_rem_incomplete();
-    // test_polysat::test_monot();
-    // test_polysat::test_fixed_point_arith_div_mul_inverse();
-    // test_polysat::test_monot_bounds_simple(8);
-    // test_polysat::test_ineq_non_axiom4(32, 7);
     return;
 #endif
 
@@ -1662,6 +1655,11 @@ void tst_polysat() {
         set_log_enabled(false);
     }
 
+    RUN(test_polysat::test_parity1());
+    RUN(test_polysat::test_parity1b());
+    RUN(test_polysat::test_parity2());
+    RUN(test_polysat::test_parity3());
+
     RUN(test_polysat::test_clause_simplify1());
 
     RUN(test_polysat::test_add_conflicts());

src/util/util.h

@@ -385,6 +385,14 @@ bool all_of(Container const& c, Predicate p)
     return std::all_of(begin(c), end(c), std::forward<Predicate>(p));
 }
 
+/** Compact version of std::any_of */
+template <typename Container, typename Predicate>
+bool any_of(Container const& c, Predicate p)
+{
+    using std::begin, std::end;  // allows begin(c) to also find c.begin()
+    return std::any_of(begin(c), end(c), std::forward<Predicate>(p));
+}
+
 /** Compact version of std::count */
 template <typename Container, typename Item>
 std::size_t count(Container const& c, Item x)