adding skeleton for local search

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

contrib/cmake/src/sat/CMakeLists.txt

@@ -12,6 +12,7 @@ z3_add_component(sat
     sat_elim_eqs.cpp
     sat_iff3_finder.cpp
     sat_integrity_checker.cpp
+    sat_local_search.cpp
     sat_model_converter.cpp
     sat_mus.cpp
     sat_parallel.cpp

src/sat/sat_local_search.cpp

@@ -0,0 +1,77 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_local_search.cpp
+
+Abstract:
+   
+    Local search module for cardinality clauses.
+
+Author:
+
+    Sixue Liu 2017-2-21
+
+Notes:
+
+--*/
+
+#include "sat_local_search.h"
+
+namespace sat {
+
+    void local_search::init() {
+
+    }
+
+    bool_var local_search::pick_var() {
+
+        return null_bool_var;
+    }
+
+    void local_search::flip(bool_var v) {
+
+       
+    }
+
+    bool local_search::tie_breaker_sat(int, int) {
+
+        return false;
+    }
+
+    bool local_search::tie_breaker_ccd(int, int) {
+
+        return false;
+    }
+
+    void local_search::calculate_and_update_ob() {
+
+    }
+    
+    void local_search::verify_solution() {
+
+    }
+    
+    void local_search::display(std::ostream& out) {
+
+    }
+
+    local_search::local_search(solver& s) {
+
+    }
+    
+    local_search::~local_search() {
+
+    }
+    
+    void local_search::add_soft(literal l, double weight) {
+
+    }
+    
+    lbool local_search::operator()() {
+        return l_undef;
+    }
+    
+
+}

src/sat/sat_local_search.h

@@ -0,0 +1,125 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_local_search.h
+
+Abstract:
+   
+    Local search module for cardinality clauses.
+
+Author:
+
+    Sixue Liu 2017-2-21
+
+Notes:
+
+--*/
+#ifndef _SAT_LOCAL_SEARCH_H_
+#define _SAT_LOCAL_SEARCH_H_
+
+#include "vector.h"
+#include "sat_types.h"
+
+namespace sat {
+
+    class local_search {
+
+        typedef svector<bool> bool_vector;
+
+        // data structure for a term in objective function
+        struct ob_term {
+            int var_id;		// variable id, begin with 1
+            int coefficient;	// non-zero integer
+        };
+
+        // data structure for a term in constraint
+        struct term {
+            int constraint_id;	// constraint it belongs to
+            int var_id;		// variable id, begin with 1
+            bool sense;		// 1 for positive, 0 for negative
+            //int coefficient;	// all constraints are cardinality: coefficient=1
+        };
+
+        // parameters of the instance
+        int	num_vars;		// var index from 1 to num_vars
+        int	num_constraints;	// constraint index from 1 to num_constraint
+        int	max_constraint_len;
+        int	min_constraint_len;
+        
+        // objective function: maximize
+        int		ob_num_terms;		// how many terms are in the objective function
+        ob_term*	ob_constraint;		// the objective function *constraint*, sorting as decending order
+        
+        
+        // terms arrays
+        vector<svector<term> > var_term; //var_term[i][j] means the j'th term of var i
+        vector<svector<term> > constraint_term; // constraint_term[i][j] means the j'th term of constraint i
+        
+        // information about the variable
+        int_vector	       coefficient_in_ob_constraint; // initilized to be 0
+        int_vector             score; 
+        int_vector            sscore;  // slack score
+        
+        int_vector             time_stamp;         // the flip time stamp
+        bool_vector	       conf_change;        // whether its configure changes since its last flip
+        int_vector             cscc;               // how many times its constraint state configure changes since its last flip
+        vector<int_vector>     var_neighbor;       // all of its neighborhoods variable
+        /* TBD: other scores */
+        
+        // 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; 
+        
+        // unsat constraint stack
+        int_vector unsat_stack;	                 // store all the unsat constraits
+        int_vector index_in_unsat_stack;         // which position is a contraint in the unsat_stack
+        
+        // configuration changed decreasing variables (score>0 and conf_change==true)
+        int_vector goodvar_stack;
+        bool_vector already_in_goodvar_stack;
+        // information about solution
+        bool_vector      cur_solution;	// the current solution
+        int              objective_value;	// the objective function value corresponds to the current solution
+        bool_vector      best_solution;	// the best solution so far
+        int		 best_objective_value = 0;	// 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
+        int		max_steps = 2000000000; // < 2147483647
+        
+        // for tuning
+        int	s_id = 0;	// strategy id
+
+        void init();
+        bool_var  pick_var();
+        void flip(bool_var v);
+        bool tie_breaker_sat(int, int);
+        bool tie_breaker_ccd(int, int);
+
+
+        void calculate_and_update_ob();
+
+        void verify_solution();
+
+        void display(std::ostream& out);
+
+    public:
+        local_search(solver& s);
+
+        ~local_search();
+
+        void add_soft(literal l, double weight);
+        
+        lbool operator()();
+
+        
+    };
+}
+
+#endif

src/sat/sat_lookahead.h

@@ -281,7 +281,7 @@ namespace sat {
                 }
 
                 //
-                // lit1 => lit2.
+                // lit1 => lit2.n
                 // if lit2 is a node, put lit1 above lit2
                 //
 
@@ -351,23 +351,34 @@ namespace sat {
             }
         }
 
+        lbool backtrack(literal_vector& trail) {
+            if (inconsistent()) {                       
+                if (trail.empty()) return l_false;      
+                pop();                                  
+                assign(~trail.back());                  
+                trail.pop_back();               
+                return l_true;
+            }
+            return l_undef;
+        }
+
         lbool search() {
             literal_vector trail;
 
-#define BACKTRACK                                       \
-            if (inconsistent()) {                       \
-                if (trail.empty()) return l_false;      \
-                pop();                                  \
-                assign(~trail.back());                  \
-                trail.pop_back();                       \
-                continue;                               \
-            }                                           \
-
             while (true) {
                 s.checkpoint();
-                BACKTRACK;
+                switch (backtrack(trail)) {
+                case l_true: continue;
+                case l_false: return l_false;
+                case l_undef: break;
+                }
+
                 literal l = choose();
-                BACKTRACK;
+                switch (backtrack(trail)) {
+                case l_true: continue;
+                case l_false: return l_false;
+                case l_undef: break;
+                }
                 if (l == null_literal) {
                     return l_true;
                 }