modify backoff mechanisms and theory exchange

src/ast/sls/sat_ddfw.cpp

@@ -81,14 +81,14 @@ namespace sat {
     void ddfw::log() {
         double sec = m_stopwatch.get_current_seconds();        
         double kflips_per_sec = sec > 0 ? (m_flips - m_last_flips) / (1000.0 * sec) : 0.0;
-        if (m_last_flips == 0) {
+        if (m_logs++ % 30 == 0) {
-            IF_VERBOSE(1, verbose_stream() << "(sat.ddfw :unsat :models :kflips/sec  :flips  :restarts  :reinits  :unsat_vars  :shifts";
+            IF_VERBOSE(2, verbose_stream() << "(sat.ddfw :unsat :models :kflips/sec   :flips :restarts   :reinits  :unsat_vars  :shifts";
                        verbose_stream() << ")\n");
         }
-        IF_VERBOSE(1, verbose_stream() << "(sat.ddfw " 
+        IF_VERBOSE(2, verbose_stream() << "(sat.ddfw " 
                    << std::setw(07) << m_min_sz 
                    << std::setw(07) << m_models.size()
-                   << std::setw(10) << kflips_per_sec
+                   << std::setw(11) << std::fixed << std::setprecision(4) << kflips_per_sec
                    << std::setw(10) << m_flips 
                    << std::setw(10) << m_restart_count
                    << std::setw(11) << m_reinit_count
@@ -214,6 +214,10 @@ namespace sat {
     }
 
     void ddfw::init(unsigned sz, literal const* assumptions) {
+        if (sz == 0 && m_initialized) {            
+            m_stopwatch.start();
+            return;
+        }
         m_assumptions.reset();
         m_assumptions.append(sz, assumptions);
         add_assumptions();
@@ -235,6 +239,8 @@ namespace sat {
         m_last_flips = 0;
         m_shifts = 0;
         m_stopwatch.start();
+        if (sz == 0)        
+            m_initialized = true;
     }
 
     void ddfw::reinit() {
@@ -423,7 +429,7 @@ namespace sat {
             m_model[i] = to_lbool(value(i));
         save_priorities();
         if (m_plugin && !m_in_external_flip)
-            m_last_result = m_plugin->on_save_model();   
+            m_last_result = m_plugin->on_save_model();
     }
 
     void ddfw::save_best_values() {

src/ast/sls/sat_ddfw.h

@@ -99,6 +99,7 @@ namespace sat {
         unsigned         m_restart_count = 0, m_reinit_count = 0;
         uint64_t         m_restart_next = 0, m_reinit_next = 0;
         uint64_t         m_flips = 0, m_last_flips = 0, m_shifts = 0;
+        unsigned         m_logs = 0;
         unsigned         m_min_sz = UINT_MAX;
         u_map<unsigned>  m_models;
         stopwatch        m_stopwatch;
@@ -168,7 +169,7 @@ namespace sat {
         void check_with_plugin();
         void check_without_plugin();
 
-        // flip activity
+        // flip 
         bool do_flip();
 
         bool_var pick_var(double& reward);     
@@ -216,6 +217,7 @@ namespace sat {
 
         void flip(bool_var v);
         bool m_in_external_flip = false;
+        bool m_initialized = false;
 
 
     public:

src/ast/sls/sls_arith_clausal.cpp

@@ -218,8 +218,12 @@ namespace sls {
         m_best_delta = 0;
         m_best_abs_value = num_t(-1);
         m_best_last_step = UINT_MAX;
+        m_num_lookaheads = 0;
         for (auto const& u : a.m_updates)
             lookahead(u.m_var, u.m_delta);
+
+//        verbose_stream() << a.m_updates.size() << " " << m_num_lookaheads << " lookaheads\n";
+        ctx.rlimit().inc(1 + m_num_lookaheads/10);
         critical_move(m_best_var, m_best_delta, mt);        
         return m_best_var;
     }
@@ -247,11 +251,11 @@ namespace sls {
         m_last_delta = delta;
         if (!a.can_update_num(v, delta))
             return;
-        ctx.rlimit().inc();
         auto score = get_score(v, delta);
         auto& vi = a.m_vars[v];        
         num_t abs_value = abs(vi.value() + delta);
         unsigned last_step = vi.last_step(delta);
+        ++m_num_lookaheads;
         if (score < a.m_best_score)
             return;
         if (score > a.m_best_score ||
@@ -338,10 +342,21 @@ namespace sls {
 
     template<typename num_t>
     void arith_clausal<num_t>::check_restart() {
+
         if (m_no_improve <= 500000)
             return;
+#if 0
+        if (a.m_stats.m_steps < a.m_config.restart_next)
+            return;
+
         
-        IF_VERBOSE(2, verbose_stream() << "restart sls-arith\n");
+        ++a.m_stats.m_restarts;
+        a.m_config.restart_next = std::max(a.m_config.restart_next, a.m_stats.m_steps);
+        
+        a.m_config.restart_next += (2 * a.m_stats.m_restarts * a.m_config.restart_base)/3;
+#endif    
+        
+        IF_VERBOSE(2, verbose_stream() << "restart sls-arith " << a.m_config.restart_next << "\n");
         TRACE("arith", tout << "restart\n";);
         // reset values of (arithmetical) variables at bounds.
         for (auto& vi : a.m_vars) {

src/ast/sls/sls_arith_clausal.h

@@ -76,6 +76,7 @@ namespace sls {
         num_t    m_best_delta;
         var_t    m_best_var = UINT_MAX;
         unsigned m_best_last_step = 0;
+        unsigned m_num_lookaheads = 0;
 
         // avoid checking the same updates twice
         var_t m_last_var = UINT_MAX;

src/ast/sls/sls_smt_plugin.cpp

@@ -101,7 +101,7 @@ namespace sls {
         if (!m_ddfw)
             return;
         m_result = m_ddfw->check(0, nullptr);
-        IF_VERBOSE(2, verbose_stream() << "sls-result " << m_result << "\n");
+        IF_VERBOSE(3, verbose_stream() << "sls-result " << m_result << "\n");
         for (auto v : m_shared_bool_vars) {
             auto w = m_smt_bool_var2sls_bool_var[v];
             m_rewards[v] = m_ddfw->get_reward_avg(w);
@@ -110,7 +110,7 @@ namespace sls {
     }
 
     void smt_plugin::bounded_run(unsigned max_iterations) {
-        verbose_stream() << "bounded run " << max_iterations << "\n";
+        IF_VERBOSE(3, verbose_stream() << "(sls-bounded :" << max_iterations << ")\n");
         m_ddfw->rlimit().reset_count();
         m_ddfw->rlimit().push(max_iterations);
         {
@@ -229,6 +229,7 @@ namespace sls {
     }
     
     void smt_plugin::export_phase_to_sls() {
+#if 0
         IF_VERBOSE(2, verbose_stream() << "SMT -> SLS phase\n");
         for (auto v : m_shared_bool_vars) {
             auto w = m_smt_bool_var2sls_bool_var[v];
@@ -236,9 +237,11 @@ namespace sls {
                 flip(w);            
             m_ddfw->bias(w) = m_sat_phase[v] ? 1 : -1;
         }
+#endif
     }
 
     void smt_plugin::smt_phase_to_sls() {
+#if 0
         IF_VERBOSE(2, verbose_stream() << "SMT -> SLS phase\n");
         for (auto v : m_shared_bool_vars) {
             auto w = m_smt_bool_var2sls_bool_var[v];
@@ -247,9 +250,17 @@ namespace sls {
                 flip(w);            
             m_ddfw->bias(w) = phase ? 1 : -1;
         }
+#endif
     }
 
     void smt_plugin::smt_values_to_sls() {
+        if (m_value_smt2sls_delay < m_value_smt2sls_delay_threshold) {
+            m_value_smt2sls_delay++;
+            return;
+        }
+        verbose_stream() << m_value_smt2sls_delay << " " << m_value_smt2sls_delay_threshold << "\n";
+        m_value_smt2sls_delay_threshold += m_value_smt2sls_delay_threshold/3;
+        m_value_smt2sls_delay = 0;
         IF_VERBOSE(2, verbose_stream() << "SMT -> SLS values\n");
         for (auto const& [t, t_sync] : m_smt2sync_uninterp) {
             expr_ref val_t(m);

src/ast/sls/sls_smt_plugin.h

@@ -63,6 +63,9 @@ namespace sls {
         std::thread m_thread;
         std::mutex  m_mutex;
 
+        unsigned m_value_smt2sls_delay = 0;
+        unsigned m_value_smt2sls_delay_threshold = 50;
+
         sat::literal_vector m_units;
         model_ref m_sls_model;
 

src/smt/theory_sls.cpp

@@ -209,6 +209,7 @@ namespace smt {
             m_smt_plugin->smt_units_to_sls();
             ++m_stats.m_num_restart_sls;
             bounded_run(m_restart_ls_steps);
+            inc_restart_ls_steps();
             if (m_smt_plugin)
                 m_smt_plugin->sls_activity_to_smt();
         }
@@ -235,6 +236,14 @@ namespace smt {
     }
 
     bool theory_sls::shared_clauses_are_true() const {
+#if 0
+        for (auto const& cl : m_shared_clauses) {
+            for (auto lit : cl)
+                verbose_stream() << lit << " : " << ctx.get_assignment(lit);
+            verbose_stream() << "\n";
+        }
+#endif
+
         for (auto const& cl : m_shared_clauses)
             if (all_of(cl, [this](sat::literal lit) { return ctx.get_assignment(lit) != l_true; }))
                 return false;

src/smt/theory_sls.h

@@ -65,8 +65,9 @@ namespace smt {
         unsigned m_restart_ls_steps_inc = 10000;
         unsigned m_restart_ls_steps_max = 300000;
         unsigned m_final_check_ls_steps = 30000;
-        unsigned m_final_check_ls_steps_dec = 10000;
+        unsigned m_final_check_ls_steps_delta = 10000;
         unsigned m_final_check_ls_steps_min = 10000;
+        unsigned m_final_check_ls_steps_max = 30000;
         bool     m_has_unassigned_clause_after_resolve = false;
         unsigned m_after_resolve_decide_gap = 4;
         unsigned m_after_resolve_decide_count = 0;
@@ -84,7 +85,7 @@ namespace smt {
         }
         void dec_final_check_ls_steps() {
             if (m_final_check_ls_steps > m_final_check_ls_steps_min)
-                m_final_check_ls_steps -= m_final_check_ls_steps_dec;
+                m_final_check_ls_steps -= m_final_check_ls_steps_delta;
         }
 
         bool shared_clauses_are_true() const;