diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 4e4db015f..24d4ebbd0 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -21,6 +21,7 @@
 #include "sat_solver.h"
 #include "card_extension.h"
 #include "sat_params.hpp"
+#include "timer.h"
 
 namespace sat {
 
@@ -65,7 +66,7 @@ namespace sat {
     void local_search::init_cur_solution() {
         //cur_solution.resize(num_vars() + 1, false);
         for (unsigned v = 0; v < num_vars(); ++v) {
-            cur_solution[v] = (rand() % 2 == 1);
+            cur_solution[v] = (m_rand() % 2 == 1);
         }
     }
 
@@ -138,7 +139,7 @@ namespace sat {
         init_cur_solution();
         
         // init varibale information
-        // variable 0 is the virtual variable
+        // the last variable is the virtual variable
 
         m_vars.back().m_score = INT_MIN;
         m_vars.back().m_conf_change = false;       
@@ -169,8 +170,6 @@ namespace sat {
         if (objective_value > best_objective_value) {
             best_solution = cur_solution;
             best_objective_value = objective_value;
-            stop = clock();
-            best_time = (double)(stop - start) / CLOCKS_PER_SEC;
         }
     }
     
@@ -197,7 +196,8 @@ namespace sat {
         }
     }
 
-    local_search::local_search(solver& s) {
+    local_search::local_search(solver& s) : 
+        m_par(0) {
 
         // copy units
         unsigned trail_sz = s.init_trail_size();
@@ -264,7 +264,7 @@ namespace sat {
                 add_cardinality(lits.size(), lits.c_ptr(), n);
             }
             //
-            // optionally handle xor constraints.
+            // xor constraints should be disabled.
             //
             SASSERT(ext->m_xors.empty());            
         }
@@ -273,24 +273,31 @@ namespace sat {
     local_search::~local_search() {
     }
     
-    void local_search::add_soft(int v, int weight) {
-        // TBD
-        ob_term t;
-        t.var_id = v;
-        t.coefficient = weight;
-        ob_constraint.push_back(t);
+    void local_search::add_soft(bool_var v, int weight) {
+        ob_constraint.push_back(ob_term(v, weight));
+    }
+
+    lbool local_search::check(parallel& p) {
+        flet<parallel*> _p(m_par, &p);
+        return check();
+    }
+
+    lbool local_search::check() {
+        return check(0, 0);
     }
     
-    lbool local_search::operator()() {
+    lbool local_search::check(unsigned sz, literal const* assumptions) {
         //sat_params params;
         //std::cout << "my parameter value: " << params.cliff() << "\n";
+        unsigned num_constraints = m_constraints.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            add_clause(1, assumptions + i);
+        }
         init();
-        bool reach_cutoff_time = false;
         bool reach_known_best_value = false;
         bool_var flipvar;
-        double elapsed_time = 0;
-        //clock_t start = clock(), stop;  // TBD, use stopwatch facility
-        start = clock();
+        timer timer;
+        timer.start();
         // ################## start ######################
         //std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
         unsigned tries, step;
@@ -309,25 +316,20 @@ namespace sat {
                 flip(flipvar);
                 m_vars[flipvar].m_time_stamp = step;
             }
-            if (tries % 10 == 0) {
-                // take a look at watch
-                stop = clock();
-                elapsed_time = (double)(stop - start) / CLOCKS_PER_SEC;
-                std::cout << tries << ": " << elapsed_time << '\n';
-            }
-            if (elapsed_time > cutoff_time)
-                reach_cutoff_time = true;
-            if (reach_known_best_value || reach_cutoff_time)
+            IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
+
+            if (!m_limit.inc()) 
                 break;
         }
-        if (reach_known_best_value) {
-            std::cout << elapsed_time << "\n";
-        }
-        else {
-            std::cout << -1 << "\n";
-        }
+        IF_VERBOSE(1, verbose_stream() << timer.get_seconds() << " " << (reach_known_best_value ? "reached":"not reached") << "\n";);
+
+        // remove unit clauses from assumptions.
+        m_constraints.shrink(num_constraints);
         //print_solution();
-        std::cout << tries * max_steps + step << '\n';
+        IF_VERBOSE(1, verbose_stream() << tries * max_steps + step << '\n';);
+        if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true
+            return l_true;
+        }
         // TBD: adjust return status
         return l_undef;
     }
@@ -354,7 +356,7 @@ namespace sat {
             case -2:  // from -1 to -2
                 for (unsigned j = 0; j < c.size(); ++j) {
                     v = c[j].var();
-                    // flipping the slack increasing var will no long sat this constraint
+                    // flipping the slack increasing var will no longer satisfy this constraint
                     if (is_true(c[j])) {
                         //score[v] -= constraint_weight[c];
                         dec_score(v);
@@ -378,7 +380,7 @@ namespace sat {
                     v = c[j].var();
                     // flip the slack decreasing var will falsify this constraint
                     if (is_false(c[j])) {
-                        //score[v] -= constraint_weight[c];
+                        // score[v] -= constraint_weight[c];
                         dec_score(v);
                         dec_slack_score(v);
                     }
@@ -459,14 +461,13 @@ namespace sat {
                 vi.m_in_goodvar_stack = true;
             }
         }
-
     }
 
     bool local_search::tie_breaker_sat(bool_var v, bool_var best_var)  {
         // most improvement on objective value
         int v_imp = cur_solution[v] ? -coefficient_in_ob_constraint.get(v, 0) : coefficient_in_ob_constraint.get(v, 0);
         int b_imp = cur_solution[best_var] ? -coefficient_in_ob_constraint.get(best_var, 0) : coefficient_in_ob_constraint.get(best_var, 0);
-        //std::cout << v_imp << "\n";
+        // std::cout << v_imp << "\n";
         // break tie 1: max imp
         // break tie 2: conf_change
         // break tie 3: time_stamp
@@ -521,7 +522,7 @@ namespace sat {
         }
 
         // Diversification Mode
-        constraint const& c = m_constraints[m_unsat_stack[rand() % m_unsat_stack.size()]]; // a random unsat constraint
+        constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; // a random unsat constraint
         // Within c, from all slack increasing var, choose the oldest one
         unsigned c_size = c.size();
         for (unsigned i = 0; i < c_size; ++i) {
@@ -534,13 +535,10 @@ namespace sat {
 
     void local_search::set_parameters()  {
 
-        srand(m_config.seed());
-        cutoff_time = m_config.cutoff_time();
+        m_rand.set_seed(m_config.seed());
         s_id = m_config.strategy_id();
         best_known_value = m_config.best_known_value();
 
-
-
         if (s_id == 0)
             max_steps = 2 * num_vars();
         else {
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index 4d51fe519..cba49e8ed 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -21,30 +21,29 @@
 
 #include "vector.h"
 #include "sat_types.h"
+#include "rlimit.h"
 
 namespace sat {
 
+    class parallel;
+
     class local_search_config {
         unsigned m_seed;
-        unsigned m_cutoff_time;
         unsigned m_strategy_id;
         int      m_best_known_value;
     public:
         local_search_config()
         {
             m_seed = 0;
-            m_cutoff_time = 1;
             m_strategy_id = 0;
             m_best_known_value = INT_MAX;
         }
 
         unsigned seed() const { return m_seed; }
-        unsigned cutoff_time() const { return m_cutoff_time;  }
         unsigned strategy_id() const { return m_strategy_id;  }
         unsigned best_known_value() const { return m_best_known_value;  }
 
         void set_seed(unsigned s) { m_seed = s;  }
-        void set_cutoff_time(unsigned t) { m_cutoff_time = t;  }
         void set_strategy_id(unsigned i) { m_strategy_id = i; }
         void set_best_known_value(unsigned v) { m_best_known_value = v; }
     };
@@ -58,21 +57,8 @@ namespace sat {
         struct ob_term {
             bool_var var_id;                     // variable id, begin with 1
             int coefficient;                     // non-zero integer
+            ob_term(bool_var v, int c): var_id(v), coefficient(c) {}
         };
-
-        // data structure for a term in constraint
-        struct term {
-            bool_var var_id;                     // variable id, begin with 1
-            bool sense;                          // 1 for positive, 0 for negative
-            //int coefficient;                   // all constraints are cardinality: coefficient=1
-        };
-
-        
-        // objective function: maximize
-        svector<ob_term>   ob_constraint;        // the objective function *constraint*, sorted in decending order
-                        
-        // information about the variable
-        int_vector             coefficient_in_ob_constraint; // initialized to be 0
         
         struct var_info {
             bool m_conf_change;                  // whether its configure changes since its last flip
@@ -92,6 +78,24 @@ namespace sat {
             {}
         };
 
+        struct constraint {
+            unsigned        m_k;
+            int             m_slack;
+            literal_vector  m_literals;
+            constraint(unsigned k) : m_k(k), m_slack(0) {}
+            unsigned size() const { return m_literals.size(); }
+            literal const& operator[](unsigned idx) const { return m_literals[idx]; }
+        };
+
+        local_search_config m_config;
+
+        // objective function: maximize
+        svector<ob_term>   ob_constraint;        // the objective function *constraint*, sorted in decending order
+                        
+        // information about the variable
+        int_vector             coefficient_in_ob_constraint; // var! initialized to be 0
+        
+
         vector<var_info>       m_vars;
 
         inline int score(bool_var v) const { return m_vars[v].m_score; }
@@ -107,23 +111,14 @@ namespace sat {
         inline int  time_stamp(bool_var v) const { return m_vars[v].m_time_stamp; }
         inline int  cscc(bool_var v) const { return m_vars[v].m_cscc; }
         inline void inc_cscc(bool_var v) { m_vars[v].m_cscc++; }
-
-        unsigned num_vars() const { return m_vars.size() - 1; }     // var index from 1 to num_vars
         
         /* TBD: other scores */
         
-        struct constraint {
-            unsigned        m_k;
-            int             m_slack;
-            literal_vector  m_literals;
-            constraint(unsigned k) : m_k(k), m_slack(0) {}
-            unsigned size() const { return m_literals.size(); }
-            literal const& operator[](unsigned idx) const { return m_literals[idx]; }
-        };
 
         vector<constraint> m_constraints;
 
         inline bool is_pos(literal t) const { return !t.sign(); }
+        inline bool is_true(bool_var v) const { return cur_solution[v]; }
         inline bool is_true(literal l) const { return cur_solution[l.var()] != l.sign(); }
         inline bool is_false(literal l) const { return cur_solution[l.var()] == l.sign(); }
 
@@ -141,22 +136,21 @@ namespace sat {
         int_vector goodvar_stack;
 
         // information about solution
-        bool_vector      cur_solution;         // the current solution
+        bool_vector      cur_solution;         // !var: the current solution
         int              objective_value;      // the objective function value corresponds to the current solution
-        bool_vector      best_solution;        // the best solution so far
+        bool_vector      best_solution;        // !var: the best solution so far
         int       best_objective_value = -1;   // the objective value corresponds to the best solution so far
         // for non-known instance, set as maximal
         int   best_known_value = INT_MAX;      // best known value for this instance
         
-        // cutoff
-        int      cutoff_time = 1;              // seconds
         unsigned      max_steps = 2000000000;  // < 2147483647
-        clock_t start, stop;
-        double			best_time;
         
         // for tuning
         int   s_id = 0;                        // strategy id
 
+        reslimit    m_limit;
+        random_gen  m_rand;
+        parallel*   m_par;
 
         void init();
         void reinit();
@@ -220,24 +214,31 @@ namespace sat {
             m_unsat_stack.pop_back();
         }
 
+
     public:
         local_search(solver& s);
 
+        reslimit& rlimit() { return m_limit; }
+
         ~local_search();
 
-        void add_soft(int l, int weight);
+        void add_soft(bool_var v, int weight);
 
         void add_cardinality(unsigned sz, literal const* c, unsigned k);
         
-        lbool operator()();
+        lbool check();
 
-        lbool check(unsigned sz, literal const* assumptions) { return l_undef; } // TBD
+        lbool check(unsigned sz, literal const* assumptions);
 
-        void cancel() {} // TBD
+        lbool check(parallel& p);
 
         local_search_config& config() { return m_config;  }
 
-        local_search_config m_config;
+        unsigned num_vars() const { return m_vars.size() - 1; }     // var index from 1 to num_vars
+
+        void set_phase(bool_var v, bool f) {}
+
+        bool get_phase(bool_var v) const { return is_true(v); }
     };
 }
 
diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp
index bc7ac408e..aa9edefe0 100644
--- a/src/sat/sat_parallel.cpp
+++ b/src/sat/sat_parallel.cpp
@@ -106,6 +106,7 @@ namespace sat {
         for (unsigned i = 0; i < num_extra_solvers; ++i) {        
             m_limits.push_back(reslimit());
         }
+        
         for (unsigned i = 0; i < num_extra_solvers; ++i) {
             s.m_params.set_uint("random_seed", s.m_rand());
             if (i == 1 + num_threads/2) {
@@ -204,5 +205,59 @@ namespace sat {
         return (c.size() <= 40 && c.glue() <= 8) || c.glue() <= 2;
     }
 
+    void parallel::set_phase(solver& s) {
+        #pragma omp critical (par_solver)
+        {
+            m_phase.reserve(s.num_vars(), 0);
+            for (unsigned i = 0; i < s.num_vars(); ++i) {
+                if (s.value(i) != l_undef) {
+                    m_phase[i] += (s.value(i) == l_true) ? 1 : -1;
+                    continue;
+                }
+                switch (s.m_phase[i]) {
+                case POS_PHASE:
+                    m_phase[i]++;
+                    break;
+                case NEG_PHASE:
+                    m_phase[i]--;
+                    break;
+                default:
+                    break;
+                }
+            }
+        }
+    }
+
+    void parallel::get_phase(solver& s) {
+        #pragma omp critical (par_solver)
+        {
+            m_phase.reserve(s.num_vars(), 0);
+            for (unsigned i = 0; i < s.num_vars(); ++i) {
+                if (m_phase[i] < 0) {
+                    s.m_phase[i] = NEG_PHASE;
+                }
+                else if (m_phase[i] > 0) {
+                    s.m_phase[i] = POS_PHASE;
+                }
+            }
+        }
+    }
+
+    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) {
+                if (m_phase[i] < 0) {
+                    s.set_phase(i, false);
+                }
+                else if (m_phase[i] > 0) {
+                    s.set_phase(i, true);
+                }
+            }
+        }
+    }
+
+    
 };
 
diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h
index 56dc83aba..0c2ba4ed9 100644
--- a/src/sat/sat_parallel.h
+++ b/src/sat/sat_parallel.h
@@ -26,6 +26,8 @@ Revision History:
 
 namespace sat {
 
+    class local_search;
+
     class parallel {
 
         // shared pool of learned clauses.
@@ -56,6 +58,7 @@ namespace sat {
         index_set      m_unit_set;
         literal_vector m_lits;
         vector_pool    m_pool;
+        int_vector     m_phase;
 
         scoped_limits      m_scoped_rlimit;
         vector<reslimit>   m_limits;
@@ -86,6 +89,15 @@ namespace sat {
         
         // receive clauses from shared clause pool
         void get_clauses(solver& s);
+
+        // exchange phase of variables.
+        void set_phase(solver& s);
+
+        void get_phase(solver& s);
+        
+        void set_phase(local_search& s);
+
+        void get_phase(local_search& s);
     };
 
 };
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 50e046905..cac06d52b 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -864,7 +864,7 @@ namespace sat {
 
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
         int num_threads = static_cast<int>(m_config.m_num_threads);
-        int num_extra_solvers = num_threads - 1 + (m_local_search ? 1 : 0);
+        int num_extra_solvers = num_threads - 1 - (m_local_search ? 1 : 0);
         sat::parallel par(*this);
         par.reserve(num_threads, 1 << 12);
         par.init_solvers(*this, num_extra_solvers);
@@ -878,7 +878,7 @@ namespace sat {
         for (int i = 0; i < num_threads; ++i) {
             try {                
                 lbool r = l_undef;
-                if (m_local_search && i + 1 == num_extra_solvers) {
+                if (m_local_search && i == num_extra_solvers) {
                     r = m_local_search->check(num_lits, lits);
                 }
                 else if (i < num_extra_solvers) {
@@ -898,7 +898,7 @@ namespace sat {
                 }
                 if (first) {
                     if (m_local_search) {
-                        m_local_search->cancel();
+                        m_local_search->rlimit().cancel();
                     }
                     for (int j = 0; j < num_extra_solvers; ++j) {
                         if (i != j) {
diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp
index a835f6a35..f4dee3061 100644
--- a/src/test/sat_local_search.cpp
+++ b/src/test/sat_local_search.cpp
@@ -1,10 +1,13 @@
 #include "sat_local_search.h"
 #include "sat_solver.h"
+#include "cancel_eh.h"
+#include "scoped_ctrl_c.h"
+#include "scoped_timer.h"
 
 static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
 {
-    char	line[16383];
-    int	cur_term;
+    char  line[16383];
+    int   cur_term;
     // for temperally storage
 
     std::ifstream infile(filename);
@@ -62,7 +65,6 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
     }
 
     infile.close();
-	
     return true;
 }
 
@@ -78,7 +80,9 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
     char const* file_name = argv[i + 1];
     ++i;
 
-	int v;
+    int cutoff_time = 1;
+
+    int v;
     while (i + 1 < argc) {
         std::cout << argv[i + 1] << "\n";
         // set other ad hoc parameters.
@@ -86,19 +90,19 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
             switch (argv[i + 1][1]) {
             case 's': // seed
                 v = atoi(argv[i + 2]);
-                local_search.m_config.set_seed(v);
+                local_search.config().set_seed(v);
                 break;
             case 't': // cutoff_time
                 v = atoi(argv[i + 2]);
-                local_search.m_config.set_cutoff_time(v);
+                cutoff_time = v;
                 break;
             case 'i': // strategy_id
                 v = atoi(argv[i + 2]);
-                local_search.m_config.set_strategy_id(v);
+                local_search.config().set_strategy_id(v);
                 break;
             case 'b': // best_known_value
                 v = atoi(argv[i + 2]);
-                local_search.m_config.set_best_known_value(v);
+                local_search.config().set_best_known_value(v);
                 break;
             default:
                 ++i;
@@ -114,10 +118,13 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
     }
 
     //std::cout << "local instance built\n";
-    local_search();
 
-    // sat::solver s;
-    // populate the sat solver with clauses and cardinality consrtaints from the input
-    // call the lookahead solver.
-    // TBD
+
+    // set up cancellation/timeout environment.
+
+    cancel_eh<reslimit> eh(local_search.rlimit());
+    scoped_ctrl_c ctrlc(eh, false, true);
+    scoped_timer timer(cutoff_time*1000, &eh);        
+    local_search.check();    
+
 }