From fb4f6d654ae25db5a191f2ac2270c8ec7a867ac3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Feb 2017 23:35:50 -0800
Subject: [PATCH] add local search parameters and co-processor mode

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_config.cpp       |  2 ++
 src/sat/sat_config.h         |  1 +
 src/sat/sat_local_search.cpp | 10 ++++++----
 src/sat/sat_parallel.cpp     | 20 +++++++++++++++++++-
 src/sat/sat_parallel.h       |  1 +
 src/sat/sat_params.pyg       |  1 +
 src/sat/sat_solver.cpp       |  3 +++
 7 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index e5fac42ae..190e76ef8 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -36,6 +36,7 @@ namespace sat {
         m_glue_psm("glue_psm"),
         m_psm_glue("psm_glue") {
         m_num_threads = 1;
+        m_local_search = false;
         updt_params(p); 
     }
 
@@ -79,6 +80,7 @@ namespace sat {
         
         m_max_conflicts   = p.max_conflicts();
         m_num_threads     = p.threads();
+        m_local_search    = p.local_search();
         
         // These parameters are not exposed
         m_simplify_mult1  = _p.get_uint("simplify_mult1", 300);
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 6f29f485e..38805bc90 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -58,6 +58,7 @@ namespace sat {
         unsigned           m_burst_search;
         unsigned           m_max_conflicts;
         unsigned           m_num_threads;
+        bool               m_local_search;
 
         unsigned           m_simplify_mult1;
         double             m_simplify_mult2;
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 24d4ebbd0..6c210c6c4 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -300,8 +300,8 @@ namespace sat {
         timer.start();
         // ################## start ######################
         //std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
-        unsigned tries, step;
-        for (tries = 0; ; ++tries) {
+        unsigned tries, step = 0;
+        for (tries = 0; m_limit.inc(); ++tries) {
             reinit();
             for (step = 1; step <= max_steps; ++step) {
                 // feasible
@@ -318,8 +318,10 @@ namespace sat {
             }
             IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
 
-            if (!m_limit.inc()) 
-                break;
+            // tell the SAT solvers about the phase of variables.
+            if (m_par && tries % 10 == 0) {
+                m_par->set_phase(*this);
+            }
         }
         IF_VERBOSE(1, verbose_stream() << timer.get_seconds() << " " << (reach_known_best_value ? "reached":"not reached") << "\n";);
 
diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp
index aa9edefe0..c4bd66a8e 100644
--- a/src/sat/sat_parallel.cpp
+++ b/src/sat/sat_parallel.cpp
@@ -139,6 +139,8 @@ namespace sat {
                 }
             }
             limit = m_units.size();
+
+            _get_phase(s);
         }
     }
 
@@ -231,6 +233,12 @@ namespace sat {
     void parallel::get_phase(solver& s) {
         #pragma omp critical (par_solver)
         {
+            _get_phase(s);
+        }
+    }
+
+    void parallel::_get_phase(solver& s) {
+        if (!m_phase.empty()) {
             m_phase.reserve(s.num_vars(), 0);
             for (unsigned i = 0; i < s.num_vars(); ++i) {
                 if (m_phase[i] < 0) {
@@ -243,7 +251,7 @@ namespace sat {
         }
     }
 
-    void parallel::get_phase(local_search& s) {
+    void parallel::set_phase(local_search& s) {
         #pragma omp critical (par_solver)
         {
             m_phase.reserve(s.num_vars(), 0);
@@ -258,6 +266,16 @@ namespace sat {
         }
     }
 
+    void parallel::get_phase(local_search& s) {
+        #pragma omp critical (par_solver)
+        {
+            m_phase.reserve(s.num_vars(), 0);
+            for (unsigned i = 0; i < s.num_vars(); ++i) {
+                m_phase[i] += (s.get_phase(i) ? 1 : -1);
+            }
+        }
+    }
+
     
 };
 
diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h
index 0c2ba4ed9..ffbed5c0c 100644
--- a/src/sat/sat_parallel.h
+++ b/src/sat/sat_parallel.h
@@ -52,6 +52,7 @@ namespace sat {
 
         bool enable_add(clause const& c) const;
         void _get_clauses(solver& s);
+        void _get_phase(solver& s);
 
         typedef hashtable<unsigned, u_hash, u_eq> index_set;
         literal_vector m_units;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 97497a220..a8fe3295b 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -28,4 +28,5 @@ def_module_params('sat',
                           ('drat.check', BOOL, False, 'build up internal proof and check'),
                           ('cardinality.solver', BOOL, False, 'use cardinality solver'),
 	                  ('xor.solver', BOOL, False, 'use xor solver'),
+                          ('local_search', BOOL, False, 'add local search co-processor to find satisfiable solution'),
                        ))
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index cac06d52b..cf150217d 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -782,6 +782,9 @@ namespace sat {
         pop_to_base_level();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(at_base_lvl());
+        if (m_config.m_local_search && !m_local_search) {
+            m_local_search = alloc(local_search, *this);
+        }
         if ((m_config.m_num_threads > 1 || m_local_search) && !m_par) {
             return check_par(num_lits, lits);
         }