testing decomposition during pre-processing

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

src/opt/opt_params.pyg

@@ -9,8 +9,6 @@ def_module_params('opt',
                           ('print_model', BOOL, False, 'display model for satisfiable constraints'),
                           ('debug_conflict', BOOL, False, 'debug conflict resolution'),
                           ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'iwmax' (iterative), 'bwmax' (bisection)"),
-                          ('pb_conflict_freq', UINT, 0, 'conflict frequency for pb theory'),
-                          ('pb_learn_comp', BOOL, True, 'learn complement literals'),
                           ('elim_01', BOOL, True, 'eliminate 01 variables')
 
                           ))

src/opt/weighted_maxsat.cpp

@@ -410,9 +410,6 @@ namespace opt {
             if (m_engine == symbol("iwmax")) {
                 return iterative_solve();
             }
-            if (m_engine == symbol("bwmax")) {
-                return bisection_solve();
-            }
             if (m_engine == symbol("pwmax")) {
                 return pb_solve();
             }
@@ -509,7 +506,7 @@ namespace opt {
             lbool result = l_false;
             unsigned nsc = 0;
             m_upper = cost;
-            while (log_cost <= cost && result == l_false) {
+            while (result == l_false) {
                 bound = wth().set_min_cost(log_cost);
                 s.push_core();
                 ++nsc;
@@ -520,6 +517,9 @@ namespace opt {
                 if (result == l_false) {
                     m_lower = log_cost;        
                 }
+                if (log_cost > cost) {
+                    break;
+                }
                 log_cost *= rational(2);
                 if (m_cancel) {
                     result = l_undef;
@@ -560,50 +560,6 @@ namespace opt {
             return is_sat;            
         }
 
-        lbool bisection_solve() {
-            TRACE("opt", tout << "weighted maxsat\n";);
-            scoped_ensure_theory wth(*this);
-            solver::scoped_push _s(s);
-            lbool is_sat = l_true;
-            bool was_sat = false;
-            expr_ref_vector bounds(m);
-            for (unsigned i = 0; i < m_soft.size(); ++i) {
-                wth().assert_weighted(m_soft[i].get(), m_weights[i]);
-            }
-            solver::scoped_push __s(s);
-            m_lower = rational::zero();
-            m_upper = wth().get_min_cost();
-            while (m_lower < m_upper && is_sat != l_undef) {
-                rational cost = div(m_upper + m_lower, rational(2));
-                bounds.push_back(wth().set_min_cost(cost));
-                is_sat = s.check_sat_core(1,bounds.c_ptr()+bounds.size()-1);
-                if (m_cancel) {
-                    is_sat = l_undef;
-                }
-                switch(is_sat) {
-                case l_true: {
-                    if (wth().is_optimal()) {
-                        s.get_model(m_model);
-                    }
-                    expr_ref fml = wth().mk_block();
-                    s.assert_expr(fml);
-                    m_upper = wth().get_min_cost();
-                    break;
-                }
-                case l_false: {
-                    m_lower = cost;
-                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bwmax min cost: " << m_lower << ")\n";);
-                    break;
-                }
-                case l_undef:
-                    break;
-                }
-            }
-            if (was_sat) {
-                is_sat = l_true;
-            }
-            return is_sat;
-        }
 
         // convert bounds constraint into pseudo-Boolean
 
@@ -708,6 +664,12 @@ namespace opt {
             m_lower = m_upper = rational::zero();
             obj_map<expr, unsigned> ans_index;
 
+#ifdef WPM2b
+            // change from CP'13
+            for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
+                al.push_back(s.get_assertion(i));
+            }
+#endif
             vector<rational> amk;
             vector<uint_set> sc;
             for (unsigned i = 0; i < m_soft.size(); ++i) {
@@ -796,7 +758,10 @@ namespace opt {
                     }
                 }
                 rational k;
+                std::cout << "new bound";
                 is_sat = new_bound(al, ws, bs, k);
+                std::cout << " " << k << "\n";
+                std::cout.flush();
                 if (is_sat != l_true) {
                     return is_sat;
                 }
@@ -830,8 +795,7 @@ namespace opt {
             al2.append(al);
             // w_j*b_j > k
             al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k)));
-            is_sat = bound(al2, ws, bs, k);
+            return bound(al2, ws, bs, k);
-            return is_sat;
         }
 
         // 
@@ -844,7 +808,7 @@ namespace opt {
                     expr_ref_vector const& bs,
                     rational& k) {
             expr_ref_vector nbs(m);
-            m_solver.push_core();
+            opt_solver::scoped_push _sc(m_solver);
             for (unsigned i = 0; i < al.size(); ++i) {
                 m_solver.assert_expr(al[i]);
             }
@@ -854,7 +818,6 @@ namespace opt {
             m_imp->re_init(nbs, ws); 
             lbool is_sat = m_imp->pb_simplify_solve();
             k = m_imp->m_lower;
-            m_solver.pop_core(1);
             return is_sat;
         }
 
@@ -952,3 +915,54 @@ namespace opt {
 
 };
 
+#if 0
+// The case m_lower = 0, m_upper = 1 is not handled correctly.
+// cost becomes 0
+
+        lbool bisection_solve() {
+            TRACE("opt", tout << "weighted maxsat\n";);
+            scoped_ensure_theory wth(*this);
+            solver::scoped_push _s(s);
+            lbool is_sat = l_true;
+            bool was_sat = false;
+            expr_ref_vector bounds(m);
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
+                wth().assert_weighted(m_soft[i].get(), m_weights[i]);
+            }
+            solver::scoped_push __s(s);
+            m_lower = rational::zero();
+            m_upper = wth().get_min_cost();
+            while (m_lower < m_upper && is_sat != l_undef) {
+                rational cost = div(m_upper + m_lower, rational(2));
+                
+                bounds.push_back(wth().set_min_cost(cost));
+                is_sat = s.check_sat_core(1,bounds.c_ptr()+bounds.size()-1);
+                if (m_cancel) {
+                    is_sat = l_undef;
+                }
+                switch(is_sat) {
+                case l_true: {
+                    if (wth().is_optimal()) {
+                        s.get_model(m_model);
+                    }
+                    expr_ref fml = wth().mk_block();
+                    s.assert_expr(fml);
+                    m_upper = wth().get_min_cost();
+                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bwmax max cost: " << m_upper << ")\n";);
+                    break;
+                }
+                case l_false: {
+                    m_lower = cost;
+                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bwmax min cost: " << m_lower << ")\n";);
+                    break;
+                }
+                case l_undef:
+                    break;
+                }
+            }
+            if (was_sat) {
+                is_sat = l_true;
+            }
+            return is_sat;
+        }
+#endif

src/tactic/core/pb_preprocess_tactic.cpp

@@ -55,32 +55,31 @@ public:
         }
     }
 
-    void set_value(app* e, expr* v) {
-        SASSERT(e->get_num_args() == 0);  
-        SASSERT(is_uninterp_const(e));
-        m_const.push_back(std::make_pair(e, v));
-        m_refs.push_back(e);
-        m_refs.push_back(v);
-    }
-
     void set_value(expr* e, bool p) {
-        if (m.is_not(e, e)) {
+        while (m.is_not(e, e)) {
-            set_value(e, !p);
+            p = !p;
         }
-        else {
         SASSERT(is_app(e));
-            set_value(to_app(e), p?m.mk_true():m.mk_false());
+        set_value_p(to_app(e), p?m.mk_true():m.mk_false());        
-        }
     }
 
     virtual model_converter * translate(ast_translation & translator) {
         pb_preproc_model_converter* mc = alloc(pb_preproc_model_converter, translator.to());
         for (unsigned i = 0; i < m_const.size(); ++i) {
-            mc->set_value(translator(m_const[i].first), translator(m_const[i].second));
+            mc->set_value_p(translator(m_const[i].first), translator(m_const[i].second));
         }
         return mc;
     }
 
+private:
+    void set_value_p(app* e, expr* v) {
+        SASSERT(e->get_num_args() == 0);  
+        SASSERT(is_uninterp_const(e));
+        m_const.push_back(std::make_pair(e, v));
+        m_refs.push_back(e);
+        m_refs.push_back(v);
+    }
+
 };
 
 class pb_preprocess_tactic : public tactic {
@@ -165,12 +164,12 @@ public:
         g->inc_depth();        
         result.push_back(g.get());       
         while (simplify(g, *pp));
+        // decompose(g);
     }
 
     bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) {
         reset();
         normalize(g);
-        decompose(g);
         if (g->inconsistent()) {
             return false;
         }
@@ -205,11 +204,11 @@ public:
             rec const& r = it->m_value;
             if (r.pos.empty()) {                
                 replace(r.neg, e, m.mk_false(), g);
-                mc.set_value(e, m.mk_false());
+                mc.set_value(e, false);
             }
             else if (r.neg.empty()) {
                 replace(r.pos, e, m.mk_true(), g);
-                mc.set_value(e, m.mk_true());
+                mc.set_value(e, true);
             }
             if (g->inconsistent()) return false;
             ++it;
@@ -220,6 +219,7 @@ public:
         while (it != m_vars.end()) {
             
             app * e = it->m_key;
+            SASSERT(is_uninterp_const(e));
             rec const& r = it->m_value;
             if (r.pos.size() == 1 && !r.neg.empty()) {
                 resolve(mc, r.pos[0], r.neg, e, true, g);
@@ -305,17 +305,99 @@ private:
         }
     }
 
+    unsigned log2ceil(unsigned n) {
+        unsigned p = 1;
+        while (n > 0) {
+            n /= 2;
+            ++p;
+        }
+        return p;
+    }
+
+    /**
+       \brief decompose large sums into smaller sums by intoducing
+       auxilary variables.
+    */
     void decompose(goal_ref const& g) {
-#if 0
+        expr_ref fml1(m), fml2(m);
-        // TBD
         for (unsigned i = 0; !g->inconsistent() && i < g->size(); ++i) {
             expr* e = g->form(i);
-            if (pb.is_ge(e) && to_app(e)->get_num_args() > 20) {
+            unsigned_vector cuts;
-                // TBD: decompose inequality int smaller ones.
+            if (cut(e, cuts)) {
+                app* a = to_app(e);
+                expr_ref_vector  cut_args(m);
+                vector<rational> cut_coeffs;
+                if (cuts.size() < 2) continue;
+                unsigned start = 0;
+                for (unsigned j = 0; j < cuts.size(); ++j) {
+                    unsigned end = cuts[j];
+                    fml1 = decompose_cut(a, start, end, cut_args, cut_coeffs); 
+                    g->assert_expr(fml1);
+                    start = end;
+                    TRACE("pb", tout << fml1 << "\n";);
+                }
+                fml2 = pb.mk_ge(cut_args.size(), cut_coeffs.c_ptr(), cut_args.c_ptr(), pb.get_k(e));
+                g->update(i, fml2);
+                TRACE("pb", tout << fml2 << "\n";);
             }
         }
-#endif
     }
+    bool cut(expr* e, unsigned_vector& cuts) {
+        if (!pb.is_ge(e)) return false;
+        if (to_app(e)->get_num_args() <= 20) return false;
+        unsigned n = 0, cut = 0;
+        unsigned sz = to_app(e)->get_num_args();
+        for (unsigned i = 0; i < sz; ++i) {
+            rational r = pb.get_coeff(e, i); 
+            if (!r.is_unsigned()) {
+                return false;
+            }                
+            n += r.get_unsigned();
+            if (2*log2ceil(n) < cut) {
+                cuts.push_back(i+1);
+                n = 0; 
+                cut = 0;
+            }
+            else {
+                ++cut;
+            }
+        }
+        if (!cuts.empty() && cuts.back() + 20 >= sz) {
+            cuts.pop_back();
+        }
+        cuts.push_back(sz);
+        return true;
+    }
+
+    expr_ref decompose_cut(app* e, unsigned start, unsigned end, 
+                           expr_ref_vector& cut_args,
+                           vector<rational>& cut_coeffs) {
+        unsigned n = 0, j = 1;
+        vector<rational> coeffs;
+        expr_ref_vector args(m);
+        app_ref z(m);
+        expr_ref fml1(m), fml(m);
+
+        for (unsigned i = start; i < end; ++i) {
+            rational r = pb.get_coeff(e, i); 
+            n += r.get_unsigned();
+            args.push_back(e->get_arg(i));
+            coeffs.push_back(r);
+        }
+
+        while (j <= n) {
+            z = m.mk_fresh_const("z", m.mk_bool_sort());
+            coeffs.push_back(-rational(j));
+            args.push_back(z);
+            cut_coeffs.push_back(rational(j));
+            cut_args.push_back(z);            
+            j <<= 1;
+        }
+        fml1 = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), rational(0));
+        m_r(fml1, fml);
+        return fml;
+    }
+    
 
     void process_vars(unsigned i, goal_ref const& g) {
         expr* r, *e;
@@ -341,7 +423,7 @@ private:
     void classify_vars(unsigned idx, app* e) {
         expr* r;
         if (m.is_not(e, r) && is_uninterp_const(r)) {
-            insert(idx, e, false);
+            insert(idx, to_app(r), false);
             return;
         }
         if (is_uninterp_const(e)) {
@@ -365,6 +447,7 @@ private:
     }
 
     void insert(unsigned i, app* e, bool pos) {
+        SASSERT(is_uninterp_const(e));
         if (!m_vars.contains(e)) {
             m_vars.insert(e, rec());
         }
@@ -585,82 +668,3 @@ tactic * mk_pb_preprocess_tactic(ast_manager & m, params_ref const & p) {
     return alloc(pb_preprocess_tactic, m);
 }
 
-#if 0
-
-    struct resolve_t {
-        app*  e;
-        expr* lhs;
-        expr* rhs;
-        expr* res;
-        resolve_t(app* e, expr* lhs, expr* rhs, expr* res):
-            e(e), lhs(lhs), rhs(rhs), res(res)
-        {}        
-    };
-
-    svector<resolve_t>               m_resolve;
-
-    void satisfy(model_ref& mdl, expr* e) {
-        if (m.is_true(e)) {
-            return;
-        }
-        if (pb.is_ge(e)) {
-            rational k = pb.get_k(e);
-            rational c(0);
-            app* a = to_app(e);
-            for (unsigned i = 0; c < k && i < a->get_num_args(); ++i) {
-                expr* arg = a->get_arg(i);
-                if (is_uninterp_const(arg)) {
-                    mdl->register_decl(to_app(arg)->get_decl(), m.mk_true());
-                    std::cout << mk_pp(arg, m) << " |-> true\n";
-                    c += pb.get_coeff(a, i);
-                }
-                else if (m.is_not(arg, arg) && is_uninterp_const(arg)) {
-                    mdl->register_decl(to_app(arg)->get_decl(), m.mk_false());
-                    std::cout << mk_pp(arg, m) << " |-> false\n";
-                    c += pb.get_coeff(a, i);
-                }
-            }
-            SASSERT(c >= k);
-            return;
-        }
-        UNREACHABLE();
-    }
-
-        for (unsigned i = m_resolve.size(); i > 0; ) {
-            --i;
-            resolve_t const& r = m_resolve[i];
-            expr_ref tmp1(m), tmp2(m), tmp3(m), tmp4(m);
-            VERIFY(mdl->eval(r.rhs, tmp2));
-            satisfy(mdl, tmp2);
-
-            VERIFY(mdl->eval(r.lhs, tmp1));
-            satisfy(mdl, tmp1);
-            
-            if (m.is_false(tmp2) || m.is_false(tmp1)) {
-                VERIFY(mdl->eval(r.res, tmp3));
-                th_rewriter rw(m);
-                rw(r.res, tmp4);
-                std::cout << "L:" << mk_pp(r.lhs,m) << " " << tmp1 << "\n";
-                std::cout << "R:" << mk_pp(r.rhs,m) << " " << tmp2 << "\n";
-                std::cout << "LR:" << mk_pp(r.res,m) << "\n" << tmp4 << "\n" << tmp3 << "\n";
-                exit(0);
-            }
-            VERIFY(mdl->eval(r.e, tmp3));
-            if (r.e == tmp3) {
-                mdl->register_decl(r.e->get_decl(), m.mk_true());
-            }
-            // evaluate lhs, rhs
-            // determine how to 
-            // assign e based on residue.            
-        }
-
-    void resolve(app* e, expr* lhs, expr* rhs, expr* res) {
-        m_refs.push_back(e);
-        m_refs.push_back(lhs);
-        m_refs.push_back(rhs);
-        m_refs.push_back(res);
-        m_resolve.push_back(resolve_t(e, lhs, rhs, res));
-    }
-
-
-#endif