From 44fcf60a72342e0580e92ed70a4d2f528a50b520 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Feb 2023 15:06:21 -0800
Subject: [PATCH] wip experiments with sls

---
 src/sat/smt/arith_sls.cpp        | 19 +++++++++++++++----
 src/sat/smt/arith_sls.h          |  1 +
 src/sat/smt/euf_local_search.cpp | 14 +++++++++++++-
 3 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/arith_sls.cpp b/src/sat/smt/arith_sls.cpp
index 8183fe1ba..6cecb4dbb 100644
--- a/src/sat/smt/arith_sls.cpp
+++ b/src/sat/smt/arith_sls.cpp
@@ -35,9 +35,8 @@ namespace arith {
         unsigned num_steps = 0;
         for (unsigned v = 0; v < s.s().num_vars(); ++v)
             init_bool_var_assignment(v);
-        m_best_min_unsat = unsat().size();
         verbose_stream() << "max arith steps " << m_max_arith_steps << "\n";
-        //m_max_arith_steps = 10000;
+        m_max_arith_steps = std::max(1000u, m_max_arith_steps);
         while (m.inc() && m_best_min_unsat > 0 && num_steps < m_max_arith_steps) {
             if (!flip())
                 break;
@@ -50,6 +49,7 @@ namespace arith {
                 save_best_values();
             }
         }
+        store_best_values();
         log();
         return unsat().empty() ? l_true : l_undef;
     }
@@ -59,6 +59,11 @@ namespace arith {
     }
 
     void sls::save_best_values() {
+        for (unsigned v = 0; v < s.get_num_vars(); ++v)
+            m_vars[v].m_best_value = m_vars[v].m_value;
+    }
+
+    void sls::store_best_values() {
         // first compute assignment to terms
         // then update non-basic variables in tableau.
         for (auto const& [t, v] : m_terms) {
@@ -80,7 +85,7 @@ namespace arith {
             int64_t old_value = 0;
             if (s.is_registered_var(v))
                 old_value = to_numeral(s.get_ivalue(v).x);
-            int64_t new_value = value(v);
+            int64_t new_value = m_vars[v].m_best_value;
             if (old_value == new_value)
                 continue;
             s.ensure_column(v);
@@ -104,6 +109,9 @@ namespace arith {
         for (unsigned i = 0; i < d->num_clauses(); ++i)
             for (sat::literal lit : *d->get_clause_info(i).m_clause)
                 init_literal(lit);
+        for (unsigned v = 0; v < s.s().num_vars(); ++v)
+            init_bool_var_assignment(v);
+        m_best_min_unsat = std::numeric_limits<unsigned>::max();
     }
 
     void sls::set_bounds_begin() {        
@@ -115,7 +123,7 @@ namespace arith {
     }
 
     void sls::set_bounds_end(unsigned num_literals) {
-        m_max_arith_steps = (m_config.L * m_max_arith_steps) / num_literals;
+        m_max_arith_steps = (m_config.L * m_max_arith_steps); // / num_literals;
     }
 
     bool sls::flip() {
@@ -323,6 +331,9 @@ namespace arith {
             int64_t dtt_old = dtt(ineq);
             int64_t delta = coeff * (new_value - old_value);
             int64_t dtt_new = dtt(ineq.m_args_value + delta, ineq);
+
+            if (dtt_old == dtt_new)
+                continue;
             
             for (auto cl : m_bool_search->get_use_list(lit)) {
                 auto const& clause = get_clause_info(cl);
diff --git a/src/sat/smt/arith_sls.h b/src/sat/smt/arith_sls.h
index 9682376be..706fff1dd 100644
--- a/src/sat/smt/arith_sls.h
+++ b/src/sat/smt/arith_sls.h
@@ -148,6 +148,7 @@ namespace arith {
         void paws();
         int64_t dscore(var_t v, int64_t new_value) const;
         void save_best_values();
+        void store_best_values();
         void add_vars();
         sls::ineq& new_ineq(ineq_kind op, int64_t const& bound);
         void add_arg(sat::literal lit, ineq& ineq, int64_t const& c, var_t v);
diff --git a/src/sat/smt/euf_local_search.cpp b/src/sat/smt/euf_local_search.cpp
index 5357c0837..0572afc39 100644
--- a/src/sat/smt/euf_local_search.cpp
+++ b/src/sat/smt/euf_local_search.cpp
@@ -40,9 +40,11 @@ namespace euf {
 
             // Non-boolean literals are assumptions to Boolean search
             literal_vector assumptions;
+#if 0
             for (unsigned v = 0; v < phase.size(); ++v)
                 if (!is_propositional(literal(v)))
                     assumptions.push_back(literal(v, !bool_search.get_value(v)));
+#endif
 
             verbose_stream() << "assumptions " << assumptions.size() << "\n";
 
@@ -51,6 +53,14 @@ namespace euf {
             lbool r = bool_search.check(assumptions.size(), assumptions.data(), nullptr);
             bool_search.rlimit().pop();
 
+#if 0
+            // restore state to optimal model
+            auto const& mdl = bool_search.get_model();
+            for (unsigned i = 0; i < mdl.size(); ++i)
+                if ((mdl[i] == l_true) != bool_search.get_value(i))
+                    bool_search.flip(i);
+#endif
+
             for (auto* th : m_solvers) 
                 th->local_search(phase);
 
@@ -92,7 +102,9 @@ namespace euf {
                 count_literal(l);
         }
 
-        m_max_bool_steps = (m_ls_config.L * num_bool) / num_literals;
+        m_max_bool_steps = (m_ls_config.L * num_bool); // / num_literals;
+        m_max_bool_steps = std::max(10000u, m_max_bool_steps);
+        verbose_stream() << "num literals " << num_literals << " num bool " << num_bool << " max bool steps " << m_max_bool_steps << "\n";
 
         for (auto* th : m_solvers)
             th->set_bounds_end(num_literals);