conflict2

src/math/polysat/conflict2.cpp

@@ -29,6 +29,38 @@ Notes:
 
 namespace polysat {
 
+    struct inf_resolve_bool : public inference {
+        sat::literal m_lit;
+        clause const& m_clause;
+        inf_resolve_bool(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {}
+        std::ostream& display(std::ostream& out) const override {
+            return out << "Resolve upon " << m_lit << " with " << m_clause;
+        }
+    };
+
+    struct inf_resolve_with_assignment : public inference {
+        solver& s;
+        sat::literal lit;
+        signed_constraint c;
+        inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
+        std::ostream& display(std::ostream& out) const override {
+            out << "Resolve upon " << lit << " with assignment:";
+            for (pvar v : c->vars())
+                if (s.is_assigned(v))
+                    out << " " << assignment_pp(s, v, s.get_value(v), true);
+            return out;
+        }
+    };
+
+    struct inf_resolve_value : public inference {
+        solver& s;
+        pvar v;
+        inf_resolve_value(solver& s, pvar v) : s(s), v(v) {}
+        std::ostream& display(std::ostream& out) const override {
+            return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true);
+        }
+    };
+
     conflict2::conflict2(solver& s) : s(s) {
         // TODO: m_log_conflicts is always false even if "polysat.log_conflicts=true" is given on the command line
         if (true || s.get_config().m_log_conflicts)
@@ -50,9 +82,21 @@ namespace polysat {
         m_vars.reset();
         m_var_occurrences.reset();
         m_lemmas.reset();
+        m_kind = conflict2_kind_t::ok;
         SASSERT(empty());
     }
 
+    void conflict2::set_bailout() {
+        SASSERT(m_kind == conflict2_kind_t::ok);
+        m_kind = conflict2_kind_t::bailout;
+        s.m_stats.m_num_bailouts++;
+    }
+
+    void conflict2::set_backjump() {
+        SASSERT(m_kind == conflict2_kind_t::ok);
+        m_kind = conflict2_kind_t::backjump;
+    }
+
     void conflict2::init(signed_constraint c) {
         SASSERT(empty());
         if (c.bvalue(s) == l_false) {
@@ -66,25 +110,23 @@ namespace polysat {
             insert_vars(c);
         }
         SASSERT(!empty());
+        logger().begin_conflict();
     }
 
     void conflict2::init(pvar v, bool by_viable_fallback) {
-        // NOTE: do forbidden interval projection in this method (rather than keeping a separate state like we did before)
-        // Option 1: forbidden interval projection
-        // Option 2: add all constraints from m_viable + dependent variables
-
         if (by_viable_fallback) {
             // Conflict detected by viable fallback:
             // initial conflict is the unsat core of the univariate solver
             signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v);
             for (auto c : unsat_core)
                 insert(c);
-            return;
+            logger().begin_conflict("unsat core from viable fallback");
+            // TODO: apply conflict resolution plugins here too?
+        } else {
+            VERIFY(s.m_viable.resolve(v, *this));
+            set_backjump();
+            logger().begin_conflict("forbidden interval lemma");
         }
-
-        // TODO:
-        // VERIFY(s.m_viable.resolve(v, *this));
-        // log_inference(inf_fi_lemma(v));
     }
 
     bool conflict2::contains(sat::literal lit) const {
@@ -108,11 +150,17 @@ namespace polysat {
         }
     }
 
-    void conflict2::remove(signed_constraint c) {
+    void conflict2::insert_eval(signed_constraint c) {
-        SASSERT(contains(c));
+        switch (c.bvalue(s)) {
-        m_literals.remove(c.blit().index());
+        case l_undef:
-        for (pvar v : c->vars())
+            s.assign_eval(c.blit());
-            m_var_occurrences[v]--;
+            break;
+        case l_true:
+            break;
+        case l_false:
+            break;
+        }
+        insert(c);
     }
 
     void conflict2::insert_vars(signed_constraint c) {
@@ -121,7 +169,99 @@ namespace polysat {
                 m_vars.insert(v);
     }
 
+    void conflict2::remove(signed_constraint c) {
+        SASSERT(contains(c));
+        m_literals.remove(c.blit().index());
+        for (pvar v : c->vars())
+            m_var_occurrences[v]--;
+    }
+
+
+    void conflict2::resolve_bool(sat::literal lit, clause const& cl) {
+        // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
+        //       clause: x \/ u \/ v
+        //       resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
+
+        SASSERT(contains(lit));
+        SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
+        SASSERT(!contains(~lit));
+        SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
+
+        remove(s.lit2cnstr(lit));
+        for (sat::literal other : cl)
+            if (other != lit)
+                insert(s.lit2cnstr(~other));
+
+        logger().log(inf_resolve_bool(lit, cl));
+    }
+
+    void conflict2::resolve_with_assignment(sat::literal lit) {
+        // The reason for lit is conceptually:
+        //    x1 = v1 /\ ... /\ xn = vn ==> lit
+
+        SASSERT(contains(lit));
+        SASSERT(!contains(~lit));
+
+        unsigned const lvl = s.m_bvars.level(lit);
+        signed_constraint c = s.lit2cnstr(lit);
+/*
+        // TODO: why bail_vars?
+        bool has_decision = false;
+        for (pvar v : c->vars())
+            if (s.is_assigned(v) && s.m_justification[v].is_decision())
+                m_bail_vars.insert(v), has_decision = true;
+        if (!has_decision) {
+            remove(c);
+            for (pvar v : c->vars())
+                if (s.is_assigned(v) && s.get_level(v) <= lvl)
+                    m_vars.insert(v);
+        }
+*/
+            remove(c);
+            for (pvar v : c->vars())
+                if (s.is_assigned(v) && s.get_level(v) <= lvl)
+                    m_vars.insert(v);
+
+        logger().log(inf_resolve_with_assignment(s, lit, c));
+    }
+
+    bool conflict2::resolve_value(pvar v) {
+        SASSERT(contains_pvar(v));
+
+        if (is_bailout())
+            return false;
+
+        auto const& j = s.m_justification[v];
+
+        // if (j.is_decision() && m_bail_vars.contains(v))
+        //     return false;
+
+        s.inc_activity(v);
+        m_vars.remove(v);
+
+        if (j.is_propagation()) {
+            for (auto const& c : s.m_viable.get_constraints(v))
+                insert_eval(c);
+            for (auto const& i : s.m_viable.units(v)) {
+                insert_eval(s.eq(i.lo(), i.lo_val()));
+                insert_eval(s.eq(i.hi(), i.hi_val()));
+            }
+        }
+        logger().log(inf_resolve_value(s, v));
+
+        // TODO: call conflict resolution plugins here; "return true" if successful
+
+        // No conflict resolution plugin succeeded => give up and bail out
+        set_bailout();
+        // Need to keep the variable in case of decision
+        if (s.is_assigned(v) && j.is_decision())
+            m_vars.insert(v);
+        logger().log("bailout");
+        return false;
+    }
+
     std::ostream& conflict2::display(std::ostream& out) const {
         out << "TODO\n";
+        return out;
     }
 }

src/math/polysat/conflict2.h

@@ -12,8 +12,9 @@ Author:
 
 Notes:
 
-    A conflict state is of the form <Vars, Constraints>
+    A conflict state is of the form <Vars, Constraints, Lemmas>
-    Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignent.
+    Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignment.
+    Lemmas provide justifications for newly created constraints.
 
     The conflict state is unsatisfiable under background clauses F.
     Dually, the negation is a consequence of F.
@@ -23,14 +24,14 @@ Notes:
     Assignments are of the form:
 
     lit <- D => lit              - lit is propagated by the clause D => lit
-    lit <- ?                     - lit is a decision literal.
     lit <- asserted              - lit is asserted
     lit <- Vars                  - lit is propagated from variable evaluation.
 
     v = value <- D               - v is assigned value by constraints D
     v = value <- ?               - v is a decision literal.
 
-    - All literals should be assigned in the stack prior to their use.
+    - All literals should be assigned in the stack prior to their use;
+      or justified by one of the side lemmas.
 
     l <- D => l,       < Vars, { l } u C >   ===>   < Vars, C u D >
     l <- ?,            < Vars, { l } u C >   ===>   ~l <- (C & Vars = value(Vars) => ~l)
@@ -66,6 +67,15 @@ Lemma:       y < z or xz <= xy or O(x,y)
 
 
 
+TODO:
+- update notes/example above
+- question: if a side lemma justifies a constraint, then we resolve over one of the premises of the lemma; do we want to update the lemma or not?
+- conflict resolution plugins
+    - may generate lemma
+        - post-processing/simplification on lemma (e.g., literal subsumption; can be done in solver)
+    - may force backjumping without further conflict resolution (e.g., if applicable lemma was found by global analysis of search state)
+    - bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something)
+    - force a restart if we get a bailout lemma or non-asserting conflict?
 
 
 --*/
@@ -84,6 +94,15 @@ namespace polysat {
     class conflict_iterator;
     class inference_logger;
 
+    enum class conflict2_kind_t {
+        // standard conflict resolution
+        ok,
+        // bailout lemma because no appropriate conflict resolution method applies
+        bailout,
+        // force backjumping without further conflict resolution because a good lemma has been found
+        backjump,
+    };
+
     class conflict2 {
         solver& s;
         scoped_ptr<inference_logger> m_logger;
@@ -91,17 +110,14 @@ namespace polysat {
         // current conflict core consists of m_literals and m_vars
         indexed_uint_set m_literals;        // set of boolean literals in the conflict
         uint_set m_vars;                    // variable assignments used as premises, shorthand for literals (x := v)
+        // uint_set m_bail_vars;               // tracked for cone of influence but not directly involved in conflict resolution
 
         unsigned_vector m_var_occurrences;  // for each variable, the number of constraints in m_literals that contain it
 
         // additional lemmas generated during conflict resolution
         vector<clause_ref> m_lemmas;
 
-        // TODO:
+        conflict2_kind_t m_kind = conflict2_kind_t::ok;
-        // conflict resolution plugins
-        // - may generate lemma
-        // - may force backjumping without further conflict resolution
-        // - bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something)
 
     public:
         conflict2(solver& s);
@@ -111,6 +127,13 @@ namespace polysat {
         bool empty() const;
         void reset();
 
+        uint_set const& vars() const { return m_vars; }
+
+        bool is_bailout() const { return m_kind == conflict2_kind_t::bailout; }
+        bool is_backjumping() const { return m_kind == conflict2_kind_t::backjump; }
+        void set_bailout();
+        void set_backjump();
+
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** conflict because there is no viable value for the variable v */
@@ -118,6 +141,7 @@ namespace polysat {
 
         bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
         bool contains(sat::literal lit) const;
+        bool contains_pvar(pvar v) const { return m_vars.contains(v) /* || m_bail_vars.contains(v) */; }
 
         /**
          * Insert constraint c into conflict state.
@@ -130,9 +154,21 @@ namespace polysat {
         /** Insert assigned variables of c */
         void insert_vars(signed_constraint c);
 
+        /** Evaluate constraint under assignment and insert it into conflict state. */
+        void insert_eval(signed_constraint c);
+
         /** Remove c from core */
         void remove(signed_constraint c);
 
+        /** Perform boolean resolution with the clause upon the given literal. */
+        void resolve_bool(sat::literal lit, clause const& cl);
+
+        /** lit was fully evaluated under the assignment.  */
+        void resolve_with_assignment(sat::literal lit);
+
+        /** Perform resolution with "v = value <- ..." */
+        bool resolve_value(pvar v);
+
         std::ostream& display(std::ostream& out) const;
     };
 

src/math/polysat/inference_logger.cpp

@@ -85,7 +85,7 @@ namespace polysat {
         out().flush();
     }
 
-    void file_inference_logger::log_inference(inference const& inf) {
+    void file_inference_logger::log(inference const& inf) {
         out() << hline() << "\n";
         out() << inf << "\n";
         log_conflict_state();

src/math/polysat/inference_logger.h

@@ -48,8 +48,8 @@ namespace polysat {
         /// Begin next conflict
         virtual void begin_conflict(char const* text = nullptr) = 0;
         /// Log inference and the current state.
-        virtual void log_inference(inference const& inf) = 0;
+        virtual void log(inference const& inf) = 0;
-        virtual void log_inference(char const* name) { log_inference(inference_named(name)); }
+        virtual void log(char const* name) { log(inference_named(name)); }
         virtual void log_var(pvar v) = 0;
         /// Log relevant part of search state and viable.
         virtual void end_conflict() = 0;
@@ -63,7 +63,7 @@ namespace polysat {
     class dummy_inference_logger : public inference_logger {
     public:
         virtual void begin_conflict(char const* text) override {}
-        virtual void log_inference(inference const& inf) override {}
+        virtual void log(inference const& inf) override {}
         virtual void log_var(pvar v) override {}
         virtual void end_conflict() override {}
         virtual void log_conflict_state() override {}
@@ -89,7 +89,7 @@ namespace polysat {
         /// Begin next conflict
         void begin_conflict(char const* text) override;
         /// Log inference and the current state.
-        void log_inference(inference const& inf) override;
+        void log(inference const& inf) override;
         void log_var(pvar v) override;
         /// Log relevant part of search state and viable.
         void end_conflict() override;

src/math/polysat/interval.h

@@ -141,11 +141,12 @@ namespace polysat {
     };
 
     inline std::ostream& operator<<(std::ostream& os, eval_interval const& i) {
-        auto& m = i.hi().manager();
         if (i.is_full())
             return os << "full";
-        else
+        else {
+            auto& m = i.hi().manager();
             return os << i.symbolic() << " := [" << m.normalize(i.lo_val()) << ";" << m.normalize(i.hi_val()) << "[";
+        }
     }
 
 

src/math/polysat/solver.cpp

@@ -645,7 +645,7 @@ namespace polysat {
                 LOG_H2("Working on " << search_item_pp(m_search, item));
                 LOG(m_justification[v]);
                 LOG("Conflict: " << m_conflict);
-                inc_activity(v);
+                // inc_activity(v);  // done in resolve_value
                 justification& j = m_justification[v];
                 if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
                     m_conflict.end_conflict();
@@ -887,6 +887,7 @@ namespace polysat {
     }
 
     void solver::assign_eval(sat::literal lit) {
+        SASSERT(lit2cnstr(lit).is_currently_true(*this));
         unsigned level = 0;
         // NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
         for (auto v : lit2cnstr(lit)->vars())

src/math/polysat/solver.h

@@ -95,6 +95,7 @@ namespace polysat {
         friend class test_polysat;
         friend class test_fi;
         friend struct inference_resolve_with_assignment;
+        friend struct inf_resolve_with_assignment;
 
         reslimit&                m_lim;
         params_ref               m_params;

src/math/polysat/viable.cpp

@@ -629,6 +629,10 @@ namespace polysat {
         }
     };
 
+    bool viable::resolve(pvar v, conflict2& core) {
+        NOT_IMPLEMENTED_YET();
+    }
+
     bool viable::resolve(pvar v, conflict& core) {
         if (has_viable(v))
             return false;

src/math/polysat/viable.h

@@ -23,6 +23,7 @@ Author:
 #include "util/small_object_allocator.h"
 #include "math/polysat/types.h"
 #include "math/polysat/conflict.h"
+#include "math/polysat/conflict2.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/forbidden_intervals.h"
 #include "math/polysat/univariate/univariate_solver.h"
@@ -111,6 +112,7 @@ namespace polysat {
         * \pre there are no viable values for v
         */
         bool resolve(pvar v, conflict& core);
+        bool resolve(pvar v, conflict2& core);
 
         /** Log all viable values for the given variable.
          * (Inefficient, but useful for debugging small instances.)