From 01897831fb58de35c0202a1fbdfb71f0fa5f64b4 Mon Sep 17 00:00:00 2001
From: Miguel Neves <t-mineve@microsoft.com>
Date: Tue, 10 Oct 2017 15:59:53 -0700
Subject: [PATCH] Dynamic delta trigger decrease

---
 src/sat/sat_lookahead.cpp | 5 ++++-
 src/sat/sat_lookahead.h   | 5 +++--
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 59149ec0f..63b013ca0 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -914,6 +914,7 @@ namespace sat {
 
     void lookahead::init() {
         m_delta_trigger = 0.0;
+        m_delta_decrease = 0.0;
         m_config.m_dl_success = 0.8;
         m_inconsistent = false;
         m_qhead = 0;
@@ -1608,6 +1609,7 @@ namespace sat {
     void lookahead::compute_lookahead_reward() {
         init_lookahead_reward();
         TRACE("sat", display_lookahead(tout); );
+        m_delta_decrease = pow(m_config.m_delta_rho, 1.0 / (double)m_lookahead.size());
         unsigned base = 2;
         bool change = true;
         literal last_changed = null_literal;
@@ -1811,7 +1813,8 @@ namespace sat {
                 }
             }
             else {
-                m_delta_trigger *= m_config.m_delta_rho;
+                SASSERT(m_delta_decrease > 0.0);
+                m_delta_trigger *= m_delta_decrease;
             }
         }
     }
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 4011996bb..76f5437b5 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -89,7 +89,7 @@ namespace sat {
                 m_min_cutoff = 30;
                 m_preselect = false;
                 m_level_cand = 600;
-                m_delta_rho = (double)0.99995;
+                m_delta_rho = (double)0.25;
                 m_dl_max_iterations = 2;
                 m_tc1_limit = 10000000;
                 m_reward_type = ternary_reward;
@@ -146,7 +146,8 @@ namespace sat {
         };
 
         config                 m_config;
-        double                 m_delta_trigger; 
+        double                 m_delta_trigger;
+        double                 m_delta_decrease;
 
         drat                   m_drat;
         literal_vector         m_assumptions;