diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index e1fad2740..6d99ef47d 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -25,15 +25,21 @@
 namespace sat {
 
     void local_search::init() {
+
+        best_solution.resize(num_vars() + 1, false);
         constraint_slack.resize(num_constraints(), 0);
-        cur_solution.resize(num_vars(), false);
+        cur_solution.resize(num_vars() + 1, false);
         m_index_in_unsat_stack.resize(num_constraints(), 0);
-        coefficient_in_ob_constraint.resize(num_vars(), 0);
+        coefficient_in_ob_constraint.resize(num_vars() + 1, 0);
         var_neighbor.reset();
-	for (bool_var v = 0; v < num_vars(); ++v) {
-            bool_vector is_neighbor(num_vars(), false);
+
+        // for dummy var 0
+        var_neighbor.push_back(bool_var_vector());
+
+        for (bool_var v = 1; v <= num_vars(); ++v) {
+            bool_vector is_neighbor(num_vars() + 1, false);
             var_neighbor.push_back(bool_var_vector());
-            for (unsigned i = 0; i < var_term[v].size(); ++ i) {
+            for (unsigned i = 0; i < var_term[v].size(); ++i) {
                 unsigned c = var_term[v][i].constraint_id;
                 for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
                     bool_var w = constraint_term[c][j].var_id; 
@@ -42,17 +48,20 @@ namespace sat {
                     var_neighbor.back().push_back(w);
                 }
             }
-	}
+        }
+        for (unsigned i = 0; i < ob_constraint.size(); ++i)
+            coefficient_in_ob_constraint[ob_constraint[i].var_id] = ob_constraint[i].coefficient;
+
         set_parameters();
     }
 
     void local_search::reinit() {
-        reinit_greedy();
+        reinit_orig();
     }
 
     void local_search::init_cur_solution() {
-        cur_solution.resize(num_vars() + 1, false);
-        for (unsigned v = 0; v < num_vars(); ++v) {
+        //cur_solution.resize(num_vars() + 1, false);
+        for (unsigned v = 1; v <= num_vars(); ++v) {
             cur_solution[v] = (rand() % 2 == 1);
         }
     }
@@ -72,9 +81,9 @@ namespace sat {
         }
     }
 
-    // figure out variables scores, pscores and sscores
+    // figure out variables scores and sscores
     void local_search::init_scores() {
-        for (unsigned v = 0; v < num_vars(); ++v) {
+        for (unsigned v = 1; v <= num_vars(); ++v) {
             for (unsigned i = 0; i < var_term[v].size(); ++i) {
                 int c = var_term[v][i].constraint_id;
                 if (cur_solution[v] != var_term[v][i].sense) {
@@ -83,7 +92,7 @@ namespace sat {
                     if (constraint_slack[c] <= 0) {
                         --sscore[v];
                         if (constraint_slack[c] == 0)
-                            --score[v];
+                            --m_var_info[v].m_score;
                     }
                 }
                 else { // if (cur_solution[v] == var_term[v][i].sense)
@@ -92,20 +101,19 @@ namespace sat {
                     if (constraint_slack[c] <= -1) {
                         ++sscore[v];
                         if (constraint_slack[c] == -1)
-                            ++score[v];
+                            ++m_var_info[v].m_score;
                     }
                 }
             }
         }
     }
 
-    // init goodvars and okvars stack    
+    // init goodvars 
     void local_search::init_goodvars() {
         goodvar_stack.reset();
-        already_in_goodvar_stack.resize(num_vars(), false);
-        for (unsigned v = 0; v < num_vars(); ++v) {
-            if (score[v] > 0) { // && conf_change[v] == true
-                already_in_goodvar_stack[v] = true;
+        for (unsigned v = 1; v <= num_vars(); ++v) {
+            if (score(v) > 0) { // && conf_change[v] == true
+                m_var_info[v].m_in_goodvar_stack = true;
                 goodvar_stack.push_back(v);
             }
         }
@@ -123,60 +131,39 @@ namespace sat {
         // init varibale information
         // variable 0 is the virtual variable
 
-        score.reset(); 
+        m_var_info.reset(); 
         sscore.reset(); 
         time_stamp.reset(); 
-        conf_change.reset(); 
         cscc.reset();
 
-        score.resize(num_vars(), 0);          score[0] = INT_MIN;
-        sscore.resize(num_vars(), 0);         sscore[0] = INT_MIN;
-        time_stamp.resize(num_vars(), 0);     time_stamp[0] = max_steps;
-        conf_change.resize(num_vars(), true); conf_change[0] = false;
-        cscc.resize(num_vars(), 1);           cscc[0] = 0;
+        m_var_info.resize(num_vars() + 1, var_info()); 
+        m_var_info[0].m_score = INT_MIN;
+        m_var_info[0].m_conf_change = false;
+        sscore.resize(num_vars() + 1, 0);         sscore[0] = INT_MIN;
+        time_stamp.resize(num_vars() + 1, 0);     time_stamp[0] = max_steps + 1;
+        cscc.resize(num_vars() + 1, 1);           cscc[0] = 0;
+
 
         init_slack();
         init_scores();
-        init_goodvars();                
-    }
+        init_goodvars();
 
-    void local_search::reinit_greedy() {
-        constraint_slack = constraint_k;
-        
-        // init unsat stack
-        m_unsat_stack.reset();
-        
-        // init solution: greedy
-        init_cur_solution();
-        
-        // init varibale information
-        // variable 0 is the virtual variable
-
-        score.reset(); 
-        sscore.reset(); 
-        time_stamp.reset(); 
-        conf_change.reset(); 
-        cscc.reset();
-
-        score.resize(num_vars(), 0);          score[0] = INT_MIN;
-        sscore.resize(num_vars(), 0);         sscore[0] = INT_MIN;
-        time_stamp.resize(num_vars(), 0);     time_stamp[0] = max_steps;
-        conf_change.resize(num_vars(), true); conf_change[0] = false;
-        cscc.resize(num_vars(), 1);           cscc[0] = 0;
-        for (unsigned v = 0; v < num_vars(); ++v) {
-            // greedy here!!
-            if (coefficient_in_ob_constraint.get(v, 0) != 0)
-                cur_solution[v] = (coefficient_in_ob_constraint[v] > 0);
-        }
-
-        init_slack();
-        init_scores();
-        init_goodvars();        
     }
     
-
     void local_search::calculate_and_update_ob() {
-
+        unsigned i, v;
+        objective_value = 0;
+        for (i = 0; i < ob_constraint.size(); ++i) {
+            v = ob_constraint[i].var_id;
+            if (cur_solution[v])
+                objective_value += ob_constraint[i].coefficient;
+        }
+        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;
+        }
     }
     
     void local_search::verify_solution() {
@@ -195,7 +182,7 @@ namespace sat {
         unsigned id = constraint_term.size();
         constraint_term.push_back(svector<term>());
         for (unsigned i = 0; i < sz; ++i) {
-            var_term.resize(c[i].var() + 1);
+            var_term.reserve(c[i].var() + 1);
             term t;
             t.constraint_id = id;
             t.var_id = c[i].var();
@@ -282,26 +269,30 @@ namespace sat {
     local_search::~local_search() {
     }
     
-    void local_search::add_soft(literal l, double weight) {
-
+    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);
     }
     
     lbool local_search::operator()() {
-        sat_params params;
-        std::cout << "my parameter value: " << params.cliff() << "\n";
+        //sat_params params;
+        //std::cout << "my parameter value: " << params.cliff() << "\n";
         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
-        srand(0);                       // TBD, use random facility and parameters to set random seed.
-        set_parameters();
+        //clock_t start = clock(), stop;  // TBD, use stopwatch facility
+        start = clock();
         // ################## start ######################
-        std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
-        for (unsigned tries = 0; ; ++tries) {
+        //std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
+        unsigned tries, step;
+        for (tries = 0; ; ++tries) {
             reinit();
-            for (int step = 1; step <= max_steps; ++step) {
+            for (step = 1; step <= max_steps; ++step) {
                 // feasible
                 if (m_unsat_stack.empty()) {
                     calculate_and_update_ob();
@@ -317,30 +308,32 @@ namespace sat {
             // take a look at watch
             stop = clock();
             elapsed_time = (double)(stop - start) / CLOCKS_PER_SEC;
+            if (tries % 10 == 0) 
+                std::cout << tries << ": " << elapsed_time << '\n';
             if (elapsed_time > cutoff_time)
                 reach_cutoff_time = true;
-            if (reach_known_best_value || reach_cutoff_time)
-                break;
+            //if (reach_known_best_value || reach_cutoff_time)
+            //    break;
         }
         if (reach_known_best_value) {
             std::cout << elapsed_time << "\n";
         }
-        else
+        else {
             std::cout << -1 << "\n";
+        }
         //print_solution();
-
+        std::cout << tries * max_steps + step << '\n';
         // TBD: adjust return status
         return l_undef;
     }
 
-
     void local_search::flip(bool_var flipvar)
     {
         // already changed truth value!!!!
         cur_solution[flipvar] = !cur_solution[flipvar];
-        
+
         unsigned v, c;
-        int org_flipvar_score = score[flipvar];
+        int org_flipvar_score = score(flipvar);
         int org_flipvar_sscore = sscore[flipvar];
 
         // update related clauses and neighbor vars
@@ -358,7 +351,7 @@ namespace sat {
                         // flipping the slack increasing var will no long sat this constraint
                         if (cur_solution[v] == constraint_term[c][j].sense)
                             //score[v] -= constraint_weight[c];
-                            --score[v];
+                            --m_var_info[v].m_score;
                     }
                     break;
                 case -1: // from 0 to -1: sat -> unsat
@@ -366,7 +359,7 @@ namespace sat {
                         v = constraint_term[c][j].var_id;
                         ++cscc[v];
                         //score[v] += constraint_weight[c];
-                        ++score[v];
+                        ++m_var_info[v].m_score;
                         // slack increasing var
                         if (cur_solution[v] == constraint_term[c][j].sense)
                             ++sscore[v];
@@ -379,7 +372,7 @@ namespace sat {
                         // flip the slack decreasing var will falsify this constraint
                         if (cur_solution[v] != constraint_term[c][j].sense) {
                             //score[v] -= constraint_weight[c];
-                            --score[v];
+                            --m_var_info[v].m_score;
                             --sscore[v];
                         }
                     }
@@ -398,7 +391,7 @@ namespace sat {
                         // flip the slack decreasing var will no long falsify this constraint
                         if (cur_solution[v] != constraint_term[c][j].sense) {
                             //score[v] += constraint_weight[c];
-                            ++score[v];
+                            ++m_var_info[v].m_score;
                             ++sscore[v];
                         }
                     }
@@ -408,7 +401,7 @@ namespace sat {
                         v = constraint_term[c][j].var_id;
                         ++cscc[v];
                         //score[v] -= constraint_weight[c];
-                        --score[v];
+                        --m_var_info[v].m_score;
                         // slack increasing var no longer sat this var
                         if (cur_solution[v] == constraint_term[c][j].sense)
                             --sscore[v];
@@ -421,7 +414,7 @@ namespace sat {
                         // flip the slack increasing var will satisfy this constraint
                         if (cur_solution[v] == constraint_term[c][j].sense)
                             //score[v] += constraint_weight[c];
-                            ++score[v];
+                            ++m_var_info[v].m_score;
                     }
                     break;
                 default:
@@ -430,39 +423,42 @@ namespace sat {
             }
         }
 
-        score[flipvar] = -org_flipvar_score;
+        m_var_info[flipvar].m_score = -org_flipvar_score;
         sscore[flipvar] = -org_flipvar_sscore;
 
-        conf_change[flipvar] = false;
+        m_var_info[flipvar].m_conf_change = false;
         cscc[flipvar] = 0;
 
         /* update CCD */
-        // remove the vars no longer okvar in okvar stack
         // remove the vars no longer goodvar in goodvar stack
         for (unsigned i = goodvar_stack.size(); i > 0;) {
             --i;
             v = goodvar_stack[i];
-            if (score[v] <= 0) {
+            if (score(v) <= 0) {
                 goodvar_stack[i] = goodvar_stack.back();
                 goodvar_stack.pop_back();
-                already_in_goodvar_stack[v] = false;
+                m_var_info[v].m_in_goodvar_stack = false;
             }
         }
         // update all flipvar's neighbor's conf_change to true, add goodvar/okvar
-        for (unsigned i = 0; i < var_neighbor[flipvar].size(); ++i) {
+
+        unsigned sz = var_neighbor[flipvar].size();
+        for (unsigned i = 0; i < sz; ++i) {
             v = var_neighbor[flipvar][i];
-            conf_change[v] = true;
-            if (score[v] > 0 && !already_in_goodvar_stack[v]) {
+            m_var_info[v].m_conf_change = true;
+            if (score(v) > 0 && !already_in_goodvar_stack(v)) {
                 goodvar_stack.push_back(v);
-                already_in_goodvar_stack[v] = true;
+                m_var_info[v].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";
         // break tie 1: max imp
         // break tie 2: conf_change
         // break tie 3: time_stamp
@@ -470,8 +466,8 @@ namespace sat {
         return 
             (v_imp > b_imp) ||
             ((v_imp == b_imp) && 
-             ((conf_change[v] && !conf_change[best_var]) ||
-              ((conf_change[v] == conf_change[best_var]) && 
+             ((conf_change(v) && !conf_change(best_var)) ||
+              ((conf_change(v) == conf_change(best_var)) && 
                (time_stamp[v] < time_stamp[best_var]))));
     }
 
@@ -481,18 +477,18 @@ namespace sat {
         // break tie 3: cscc
         // break tie 4: oldest one
         return 
-             (score[v]  > score[best_var]) ||
-            ((score[v] == score[best_var]) &&
-              (sscore[v]  > sscore[best_var]) ||
-             ((sscore[v] == sscore[best_var]) &&
-               (cscc[v]  > cscc[best_var]) ||
-              ((cscc[v] == cscc[best_var]) && 
-               (time_stamp[v] < time_stamp[best_var]))));
+            ((score(v) > score(best_var)) ||
+             ((score(v) == score(best_var)) &&
+              ((sscore[v] > sscore[best_var]) ||
+               ((sscore[v] == sscore[best_var]) &&
+                ((cscc[v] > cscc[best_var]) ||
+                 ((cscc[v] == cscc[best_var]) && 
+                  (time_stamp[v] < time_stamp[best_var])))))));
     }
 
     bool_var local_search::pick_var() {
         int c, v;
-        bool_var best_var = num_vars()-1;
+        bool_var best_var = 0;
 
         // SAT Mode
         if (m_unsat_stack.empty()) {
@@ -521,32 +517,42 @@ namespace sat {
         // Diversification Mode
         c = m_unsat_stack[rand() % m_unsat_stack.size()]; // a random unsat constraint
         // Within c, from all slack increasing var, choose the oldest one
-        for (unsigned i = 0; i < constraint_term[c].size(); ++i) {
+        unsigned c_size = constraint_term[c].size();
+        for (unsigned i = 0; i < c_size; ++i) {
             v = constraint_term[c][i].var_id;
             if (cur_solution[v] == constraint_term[c][i].sense && time_stamp[v] < time_stamp[best_var])
                 best_var = v;
         }
-        //++rd;
         return best_var;
     }
 
     void local_search::set_parameters()  {
+
+        srand(m_config.seed());
+        cutoff_time = m_config.cutoff_time();
+        s_id = m_config.strategy_id();
+        best_known_value = m_config.best_known_value();
+
+
+
         if (s_id == 0)
-            max_steps = num_vars();
-        else if (s_id == 1)
-            max_steps = (int) (1.5 * num_vars());
-        else if (s_id == 1)
             max_steps = 2 * num_vars();
-        else if (s_id == 2)
-            max_steps = (int) (2.5 * num_vars());
-        else if (s_id == 3)
-            max_steps = 3 * num_vars();
         else {
             std::cout << "Invalid strategy id!" << std::endl;
             exit(-1);
         }
+
+        /*std::cout << "seed:\t" << m_config.seed() << '\n';
+          std::cout << "cutoff time:\t" << m_config.cutoff_time() << '\n';
+          std::cout << "strategy id:\t" << m_config.strategy_id() << '\n';
+          std::cout << "best_known_value:\t" << m_config.best_known_value() << '\n';
+          std::cout << "max_steps:\t" << max_steps << '\n';
+        */
     }
 
-    
-
+    void local_search::print_info() {
+        for (int v = 1; v <= num_vars(); ++v) {
+            std::cout << var_neighbor[v].size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << sscore[v] << '\n';
+        }
+    }
 }
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index 1d314abf8..97e1974f2 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -1,21 +1,21 @@
 /*++
-Copyright (c) 2017 Microsoft Corporation
+  Copyright (c) 2017 Microsoft Corporation
 
-Module Name:
+  Module Name:
 
-    sat_local_search.h
+  sat_local_search.h
 
-Abstract:
+  Abstract:
    
-    Local search module for cardinality clauses.
+  Local search module for cardinality clauses.
 
-Author:
+  Author:
 
-    Sixue Liu 2017-2-21
+  Sixue Liu 2017-2-21
 
-Notes:
+  Notes:
 
---*/
+  --*/
 #ifndef _SAT_LOCAL_SEARCH_H_
 #define _SAT_LOCAL_SEARCH_H_
 
@@ -24,8 +24,33 @@ Notes:
 
 namespace sat {
 
-    class local_search {
+    class local_search_config {
+        unsigned m_seed;
+        unsigned m_cutoff_time;
+        unsigned m_strategy_id;
+        unsigned m_best_known_value;
+    public:
+        local_search_config()
+        {
+            m_seed = 0;
+            m_cutoff_time = 1;
+            m_strategy_id = 0;
+            m_best_known_value = UINT_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; }
+    };
+
+    class local_search {
+		
         typedef svector<bool> bool_vector;
 
         // data structure for a term in objective function
@@ -52,17 +77,33 @@ namespace sat {
         vector<svector<term> > constraint_term;  // constraint_term[i][j] means the j'th term of constraint i
 
         // parameters of the instance
-        unsigned num_vars() const { return var_term.size(); }             // var index from 1 to num_vars
+        unsigned num_vars() const { return var_term.size() - 1; }             // var index from 1 to num_vars
         unsigned num_constraints() const { return constraint_term.size(); } // constraint index from 1 to num_constraint
 
         
         // information about the variable
         int_vector             coefficient_in_ob_constraint; // initialized to be 0
-        int_vector             score; 
+        // int_vector             score; 
         int_vector             sscore;           // slack score
         
+        struct var_info {
+            bool m_conf_change;                  // whether its configure changes since its last flip
+            bool m_in_goodvar_stack;
+            int  m_score;
+            var_info():
+                m_conf_change(true),
+                m_in_goodvar_stack(false),
+                m_score(0)
+            {}
+        };
+        svector<var_info>       m_var_info;
+
+        inline int score(unsigned v) const { return m_var_info[v].m_score; }
+        inline bool already_in_goodvar_stack(unsigned v) const { return m_var_info[v].m_in_goodvar_stack; }
+        inline bool conf_change(unsigned v) const { return m_var_info[v].m_conf_change; }
+
         int_vector             time_stamp;       // the flip time stamp
-        bool_vector            conf_change;      // whether its configure changes since its last flip
+        // bool_vector            conf_change;      
         int_vector             cscc;             // how many times its constraint state configure changes since its last flip
         vector<bool_var_vector>     var_neighbor;     // all of its neighborhoods variable
         /* TBD: other scores */
@@ -70,8 +111,8 @@ namespace sat {
         // information about the constraints
         int_vector constraint_k;                // the right side k of a constraint
         int_vector constraint_slack;            // =constraint_k[i]-true_terms[i], if >=0 then sat
-        int_vector nb_slack;                    // constraint_k - ob_var(same in ob) - none_ob_true_terms_count. if < 0: some ob var might be flipped to false, result in an ob decreasing
-        bool_vector has_true_ob_terms; 
+        //int_vector nb_slack;                    // constraint_k - ob_var(same in ob) - none_ob_true_terms_count. if < 0: some ob var might be flipped to false, result in an ob decreasing
+        //bool_vector has_true_ob_terms; 
         
         // unsat constraint stack
         int_vector m_unsat_stack;               // store all the unsat constraits
@@ -79,7 +120,7 @@ namespace sat {
         
         // configuration changed decreasing variables (score>0 and conf_change==true)
         int_vector goodvar_stack;
-        bool_vector already_in_goodvar_stack;
+        // bool_vector already_in_goodvar_stack;
 
         // information about solution
         bool_vector      cur_solution;        // the current solution
@@ -92,6 +133,8 @@ namespace sat {
         // cutoff
         int      cutoff_time = 1;            // seconds
         int      max_steps = 2000000000;     // < 2147483647
+        clock_t start, stop;
+        double			best_time;
         
         // for tuning
         int   s_id = 0;                      // strategy id
@@ -101,7 +144,6 @@ namespace sat {
 
         void reinit();
         void reinit_orig();
-        void reinit_greedy();
 
         void init_cur_solution();
         void init_slack();
@@ -124,11 +166,35 @@ namespace sat {
 
         void display(std::ostream& out);
 
-        void unsat(int constraint_id) { m_unsat_stack.push_back(constraint_id); }
+        void print_info();
+
+        bool check_goodvar() {
+            unsigned g = 0;
+            for (unsigned v = 1; v <= num_vars(); ++v) {
+                if (conf_change(v) && score(v) > 0) {
+                    ++g;
+                    if (!already_in_goodvar_stack(v))
+                        std::cout << "3\n";
+                }
+            }
+            if (g == goodvar_stack.size())
+                return true;
+            else {
+                if (g < goodvar_stack.size())
+                    std::cout << "1\n";
+                else
+                    std::cout << "2\n"; // delete too many
+                return false;
+            }
+        }
 
         void add_clause(unsigned sz, literal const* c);
 
 
+        void unsat(int c) {
+            m_index_in_unsat_stack[c] = m_unsat_stack.size();
+            m_unsat_stack.push_back(c);
+        }
         // swap the deleted one with the last one and pop
         void sat(int c) {
             int last_unsat_constraint = m_unsat_stack.back();
@@ -143,13 +209,15 @@ namespace sat {
 
         ~local_search();
 
-        void add_soft(literal l, double weight);
+        void add_soft(int l, int weight);
 
         void add_cardinality(unsigned sz, literal const* c, unsigned k);
         
         lbool operator()();
 
-        
+        local_search_config& config() { return m_config;  }
+
+        local_search_config m_config;
     };
 }
 
diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp
index 53720d094..6128e5e21 100644
--- a/src/test/sat_local_search.cpp
+++ b/src/test/sat_local_search.cpp
@@ -16,8 +16,8 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
     infile.getline(line, 16383);
     int num_vars, num_constraints;
     sscanf_s(line, "%d %d", &num_vars, &num_constraints);
-    //cout << "number of variables: " << num_vars << endl;
-    //cout << "number of constraints: " << num_constraints << endl;
+    //std::cout << "number of variables: " << num_vars << '\n';
+    //std::cout << "number of constraints: " << num_constraints << '\n';
 
 
     unsigned_vector coefficients;
@@ -44,12 +44,12 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
     }
 
     for (unsigned i = 0; i < lits.size(); ++i) {
-        local_search.add_soft(lits[i], coefficients[i]);
+        local_search.add_soft(lits[i].var(), coefficients[i]);
     }
     
     // read the constraints, one at a time
     int k;
-    for (int c = 1; c <= num_constraints; ++c) {        
+    for (int c = 0; c < num_constraints; ++c) {        
         lits.reset();
         infile >> cur_term;
         while (cur_term != 0) {
@@ -57,10 +57,12 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
             infile >> cur_term;
         }
         infile >> k;
-        local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast<unsigned>(lits.size() - k));
+        //local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast<unsigned>(lits.size() - k));
+        local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast<unsigned>(k));
     }
 
     infile.close();
+	
     return true;
 }
 
@@ -75,9 +77,34 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
     sat::local_search local_search(solver);
     char const* file_name = argv[i + 1];
     ++i;
+
+	int v;
     while (i + 1 < argc) {
         // set other ad hoc parameters.
-        std::cout << argv[i + 1] << "\n";
+		if (argv[i + 1][0] == '-' && i + 2 < argc) {
+			switch (argv[i + 1][1]) {
+			case 's': // seed
+				v = atoi(argv[i + 2]);
+				local_search.m_config.set_seed(v);
+				break;
+			case 't': // cutoff_time
+				v = atoi(argv[i + 2]);
+				local_search.m_config.set_cutoff_time(v);
+				break;
+			case 'i': // strategy_id
+				v = atoi(argv[i + 2]);
+				local_search.m_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);
+				break;
+			default:
+				++i;
+				v = -1;
+				break;
+			}
+		}
         ++i;
     }
 
@@ -85,7 +112,7 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
         return;
     }
 
-    std::cout << "local instance built\n";
+    //std::cout << "local instance built\n";
     local_search();
 
     // sat::solver s;