tuning pd-maxres

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

src/sat/sat_solver.cpp

@@ -54,6 +54,7 @@ namespace sat {
         m_conflicts               = 0;
         m_next_simplify           = 0;
         m_num_checkpoints         = 0;
+        m_initializing_preferred  = false;
     }
 
     solver::~solver() {
@@ -407,6 +408,7 @@ namespace sat {
         for (unsigned i = 1; i < num_lits; i++) {
             literal l    = cls[i];
             lbool val    = value(l);
+            CTRACE("sat", val != l_false, tout << l << ":=" << val;);
             SASSERT(val == l_false);
             if (max_false_idx == UINT_MAX || lvl(l) > lvl(cls[max_false_idx]))
                 max_false_idx = i;
@@ -894,8 +896,7 @@ namespace sat {
         }
 
     retry_init_assumptions:
-        m_assumptions.reset();
+        reset_assumptions();
-        m_assumption_set.reset();        
         push();
 
         propagate(false);
@@ -931,25 +932,19 @@ namespace sat {
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
             SASSERT(is_external(lit.var()));  
-            m_assumption_set.insert(lit);       
+            add_assumption(lit);  
-            m_assumptions.push_back(lit);       
             assign(lit, justification());       
         }
     }
 
-    void solver::resolve_weighted() {
-        flet<bool> _min1(m_config.m_minimize_core, false);
-        flet<bool> _min2(m_config.m_minimize_core_partial, false);
-        m_conflict_lvl = m_scope_lvl;
-        resolve_conflict_for_unsat_core();
-    }
 
     bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) {
-        double weight = 0;
+        flet<bool> _min1(m_config.m_minimize_core, false);
-        literal_vector blocker;
+        flet<bool> _min2(m_config.m_minimize_core_partial, false);
+        m_weight = 0;
+        m_blocker.reset();
         m_min_core_valid = false;
         m_min_core.reset();
-        unsigned old_sz = 0;
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
             SASSERT(is_external(lit.var()));  
@@ -958,55 +953,42 @@ namespace sat {
 
             switch(value(lit)) {
             case l_undef:
-                m_assumption_set.insert(lit);       
+                add_assumption(lit);  
-                m_assumptions.push_back(lit);     
-                old_sz = m_qhead;
                 assign(lit, justification());
                 propagate(false);
                 if (inconsistent()) {
-                    resolve_weighted();
+                    pop_assumption();
-                    m_assumption_set.pop();
+                    flet<bool> _init(m_initializing_preferred, true);
-                    m_assumptions.pop_back();
+                    while (inconsistent()) {
-                    unassign_vars(old_sz);
+                        if (!resolve_conflict()) {
-                    m_inconsistent = false;
+                            return true;
-                    update_min_core();
+                        }
-                    blocker.reset();
+                        propagate(true);
-                    for (unsigned j = 0; j < m_core.size(); ++j) {
-                        blocker.push_back(~m_core[j]);
                     }
-                    TRACE("sat", tout << "Blocker: " << blocker << "\n";);
+                    if (m_scope_lvl == 0) {
-                    mk_clause(blocker);
+                        return false;
-                    propagate(false);
-                    if (inconsistent()) {
-                        //
-                        // TBD: this could be improved by emulating normal
-                        // conflict resolution and backjumping directly and
-                        // continuing with the backjumped state instead of
-                        // baling out using the best core so far.
-                        //
-                        resolve_weighted();
-                        update_min_core();
-                        IF_VERBOSE(1, verbose_stream() << "Conflicting assignment: " << m_core << "\n"
-                                   << "Core: " << m_min_core << "\n";);
-                        pop_to_base_level();
-                        reassert_min_core();
-                        return true;
                     }
-                    SASSERT(value(lit) == l_false);         
+                    for (; i < num_lits; ++i) {
-                    IF_VERBOSE(11, 
+                        literal lit = lits[i];
-                               verbose_stream() << "undef: " << lit << " : " << blocker << "\n";
+                        if (value(lit) == l_undef) {
-                               verbose_stream() << m_assumptions << "\n";);
+                            assign(lit, justification());
+                            add_assumption(lit);  
+                        }                        
+                    }
+                    return true;
                 }
-                blocker.push_back(~lit);
                 break;                
                 
             case l_false: 
-                m_assumption_set.insert(lit);       
+                add_assumption(lit);  
-                m_assumptions.push_back(lit);       
                 SASSERT(!inconsistent());
                 set_conflict(justification(), ~lit);
-                resolve_weighted();
+                m_conflict_lvl = m_scope_lvl;
-                weight += weights[i];
+                resolve_conflict_for_unsat_core();
+                m_weight += weights[i];
+                if (m_weight <= max_weight) {
+                    m_blocker.push_back(lit);
+                }
                 TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";);
                 SASSERT(m_core.size() <= m_assumptions.size());
                 SASSERT(m_assumptions.size() <= i+1);
@@ -1018,34 +1000,37 @@ namespace sat {
                 }
                 update_min_core();
                 SASSERT(m_min_core_valid);
-                VERIFY(m_assumptions.back() == m_assumption_set.pop());
+                pop_assumption();
-                m_assumptions.pop_back();
                 m_inconsistent = false; 
-                if (weight < max_weight) {
-                    blocker.push_back(lit);
-                }
                 break;
-            case l_true:
+            case l_true: {
+                justification j = m_justification[lit.var()];
+                if (j.get_kind() == justification::NONE) {
+                    add_assumption(lit);
+                }            
                 break;
             }
+            }
         }
         TRACE("sat", tout << "initialized\n";);
-        IF_VERBOSE(11, verbose_stream() << "Blocker: " << blocker << " - " << m_min_core << "\n";);
+        IF_VERBOSE(11, verbose_stream() << "Blocker: " << m_blocker << "\nCore: " << m_min_core << "\n";);
-        if (m_min_core_valid && blocker.size() >= m_min_core.size()) {
+        if (m_min_core_valid && m_blocker.size() >= m_min_core.size()) {
             reassert_min_core();
         }
-        else if (weight > max_weight) {
+        else if (m_weight >= max_weight) {
-            ++m_stats.m_blocked_corr_sets;
-            TRACE("opt", tout << "blocking soft correction set: " << blocker << "\n";); 
             // block the current correction set candidate.
-            IF_VERBOSE(11, verbose_stream() << "blocking " << blocker << "\n";);
+            ++m_stats.m_blocked_corr_sets;
+            TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); 
+            IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";);
             pop_to_base_level();
-            mk_clause(blocker);
+            mk_clause(m_blocker);
             return false;
         }
         return true;
     }
 
+
+
     void solver::update_min_core() {
         if (!m_min_core_valid || m_core.size() < m_min_core.size()) {
             m_min_core.reset();
@@ -1054,17 +1039,31 @@ namespace sat {
         }        
     }
 
+    void solver::reset_assumptions() {
+        m_assumptions.reset();
+        m_assumption_set.reset();                
+    }
+
+    void solver::add_assumption(literal lit) {
+        m_assumption_set.insert(lit);       
+        m_assumptions.push_back(lit);                   
+    }
+
+    void solver::pop_assumption() {
+        VERIFY(m_assumptions.back() == m_assumption_set.pop());
+        m_assumptions.pop_back();
+    }
+
     void solver::reassert_min_core() {
         SASSERT(m_min_core_valid);
         pop_to_base_level();
         push();
-        m_assumption_set.reset();
+        reset_assumptions();
-        m_assumptions.reset();
+        TRACE("sat", tout << "reassert: " << m_min_core << "\n";);
         for (unsigned i = 0; i < m_min_core.size(); ++i) {
             literal lit = m_min_core[i];
-            SASSERT(is_external(lit.var()));  
+            SASSERT(is_external(lit.var()));
-            m_assumption_set.insert(lit);       
+            add_assumption(lit);  
-            m_assumptions.push_back(lit);       
             assign(lit, justification());       
         }
         propagate(false);
@@ -1629,6 +1628,10 @@ namespace sat {
               if (m_not_l == literal()) tout << "null literal\n";
               else tout << m_not_l << "\n";);
 
+        if (m_initializing_preferred) {
+            SASSERT(m_conflict_lvl <= 1);
+            return resolve_conflict_for_init();
+        }
         if (m_conflict_lvl <= 1 && tracking_assumptions()) {
             resolve_conflict_for_unsat_core();
             return false;
@@ -1656,7 +1659,7 @@ namespace sat {
 
         do {
             TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
-                  tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
+                  tout << "num_marks: " << num_marks << ", js: " << js << "\n";);
             switch (js.get_kind()) {
             case justification::NONE:
                 break;
@@ -1814,6 +1817,120 @@ namespace sat {
         }
     }
 
+    bool solver::resolve_conflict_for_init() {
+        if (m_conflict_lvl == 0) {
+            return false;
+        }        
+        m_lemma.reset();
+        m_lemma.push_back(null_literal); // asserted literal
+        if (m_not_l != null_literal) {
+            TRACE("sat", tout << "not_l: " << m_not_l << "\n";);            
+            process_antecedent_for_init(m_not_l);
+        }
+        literal consequent = m_not_l;
+        justification js   = m_conflict;
+
+        SASSERT(m_trail.size() > 0);
+        unsigned idx = m_trail.size();
+        while (process_consequent_for_init(consequent, js)) {
+            while (true) {
+                --idx;
+                literal l = m_trail[idx];
+                if (is_marked(l.var()))
+                    break;
+                SASSERT(idx > 0);
+            }
+            consequent     = m_trail[idx];
+            bool_var c_var = consequent.var();
+            if (lvl(consequent) == 0) {
+                return false;
+            }
+            SASSERT(m_conflict_lvl == 1);
+            js = m_justification[c_var];
+            reset_mark(c_var);
+        }
+
+        unsigned new_scope_lvl = 0;
+        m_lemma[0] = ~consequent;
+        for (unsigned i = 1; i < m_lemma.size(); ++i) {
+            bool_var var = m_lemma[i].var();
+            if (is_marked(var)) {
+                reset_mark(var);
+                new_scope_lvl = std::max(new_scope_lvl, lvl(var));
+            }
+            else {
+                m_lemma[i] = m_lemma.back();
+                m_lemma.pop_back();
+                --i;
+            }
+        }
+        TRACE("sat", tout << "lemma: " << m_lemma << "\n"; display(tout); tout << "assignment:\n"; display_assignment(tout););
+        if (new_scope_lvl == 0) {
+            pop_reinit(m_scope_lvl);
+        }
+        else {
+            unassign_vars(idx);
+        }
+        mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
+        TRACE("sat", tout << "Trail: " << m_trail << "\n";);
+        m_inconsistent = false;
+        return true;
+    }
+
+    bool solver::process_consequent_for_init(literal consequent, justification const& js) {
+        switch (js.get_kind()) {
+        case justification::NONE:
+            return false;
+        case justification::BINARY:
+            process_antecedent_for_init(~(js.get_literal()));
+            break;
+        case justification::TERNARY:
+            process_antecedent_for_init(~(js.get_literal1()));
+            process_antecedent_for_init(~(js.get_literal2()));
+            break;
+        case justification::CLAUSE: {
+            clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
+            unsigned i   = 0;
+            if (consequent != null_literal) {
+                SASSERT(c[0] == consequent || c[1] == consequent);
+                if (c[0] == consequent) {
+                    i = 1;
+                }
+                else {
+                    process_antecedent_for_init(~c[0]);
+                    i = 2;
+                }
+            }
+            unsigned sz  = c.size();
+            for (; i < sz; i++)
+                process_antecedent_for_init(~c[i]);
+            break;
+        }
+        case justification::EXT_JUSTIFICATION: {
+            fill_ext_antecedents(consequent, js);
+            literal_vector::iterator it  = m_ext_antecedents.begin();
+            literal_vector::iterator end = m_ext_antecedents.end();
+            for (; it != end; ++it)
+                process_antecedent_for_init(*it);
+            break;
+        }
+        default:
+            UNREACHABLE();
+            break;
+        }
+        return true;
+    }
+
+    void solver::process_antecedent_for_init(literal antecedent) {
+        bool_var var     = antecedent.var();
+        SASSERT(var < num_vars());
+        if (!is_marked(var) && lvl(var) > 0) {
+            mark(var);
+            m_lemma.push_back(~antecedent);
+        }
+    }
+
+
     void solver::resolve_conflict_for_unsat_core() {
         TRACE("sat", display(tout);
               unsigned level = 0;
@@ -2489,8 +2606,7 @@ namespace sat {
     }
 
     void solver::pop_to_base_level() {
-        m_assumptions.reset();
+        reset_assumptions();
-        m_assumption_set.reset();
         pop(scope_lvl());
     }
 
@@ -2756,9 +2872,7 @@ namespace sat {
     }
 
     void solver::display_assignment(std::ostream & out) const {
-        for (unsigned i = 0; i < m_trail.size(); i++)
+        out << m_trail << "\n";
-            out << m_trail[i] << " ";
-        out << "\n";
     }
 
     /**

src/sat/sat_solver.h

@@ -300,11 +300,17 @@ namespace sat {
         
         literal_vector m_min_core;
         bool           m_min_core_valid;
+        literal_vector m_blocker;
+        double         m_weight;
+        bool           m_initializing_preferred;
         void init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight);
         bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight);
         void reassert_min_core();
         void update_min_core();
         void resolve_weighted();
+        void reset_assumptions();
+        void add_assumption(literal lit);
+        void pop_assumption();
         void reinit_assumptions();
         bool tracking_assumptions() const;
         bool is_assumption(literal l) const;
@@ -353,11 +359,14 @@ namespace sat {
         literal_vector m_ext_antecedents;
         bool resolve_conflict();
         bool resolve_conflict_core();
-        void resolve_conflict_for_unsat_core();
         unsigned get_max_lvl(literal consequent, justification js);
         void process_antecedent(literal antecedent, unsigned & num_marks);
+        void resolve_conflict_for_unsat_core();
         void process_antecedent_for_unsat_core(literal antecedent);
         void process_consequent_for_unsat_core(literal consequent, justification const& js);
+        bool resolve_conflict_for_init();
+        void process_antecedent_for_init(literal antecedent);
+        bool process_consequent_for_init(literal consequent, justification const& js);
         void fill_ext_antecedents(literal consequent, justification js);
         unsigned skip_literals_above_conflict_level();
         void forget_phase_of_vars(unsigned from_lvl);