adding unit test entry point

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

contrib/cmake/src/test/CMakeLists.txt

@@ -92,6 +92,7 @@ add_executable(test-z3
   rational.cpp
   rcf.cpp
   region.cpp
+  sat_local_search.cpp
   sat_lookahead.cpp
   sat_user_scope.cpp
   simple_parser.cpp

src/api/api_opt.cpp

@@ -129,7 +129,6 @@ extern "C" {
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit = mk_c(c)->get_rlimit();
-        std::cout << "Timeout: " << timeout << "\n";
         api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
             scoped_timer timer(timeout, &eh);

src/sat/card_extension.cpp

@@ -741,10 +741,17 @@ namespace sat {
         unsigned index = 2*m_cards.size();
         card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, literal(v, false), lits, k);
         m_cards.push_back(c);
+        if (v == null_bool_var) {
+            // it is an axiom.
+            init_watch(*c, true);
+            m_card_axioms.push_back(c);
+        }
+        else {
             init_watch(v);
             m_var_infos[v].m_card = c;
             m_var_trail.push_back(v);
         }
+    }
 
     void card_extension::add_xor(bool_var v, literal_vector const& lits) {
         m_has_xor = true;

src/sat/card_extension.h

@@ -21,10 +21,14 @@ Revision History:
 
 #include"sat_extension.h"
 #include"sat_solver.h"
+#include"scoped_ptr_vector.h"
 
 namespace sat {
     
     class card_extension : public extension {
+
+        friend class local_search;
+
         struct stats {
             unsigned m_num_propagations;
             unsigned m_num_conflicts;
@@ -118,6 +122,8 @@ namespace sat {
         ptr_vector<card>    m_cards;
         ptr_vector<xor>     m_xors;
 
+        scoped_ptr_vector<card> m_card_axioms;
+
         // watch literals
         svector<var_info>   m_var_infos;
         unsigned_vector     m_var_trail;

src/sat/sat_local_search.cpp

@@ -19,6 +19,7 @@
 
 #include "sat_local_search.h"
 #include "sat_solver.h"
+#include "card_extension.h"
 
 namespace sat {
 
@@ -153,29 +154,32 @@ namespace sat {
 
     }
 
+    void local_search::add_clause(unsigned sz, literal const* c) {
+        add_cardinality(sz, c, sz - 1);
+    }
+
+    void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) {
+        unsigned id = constraint_term.size();
+        constraint_term.push_back(svector<term>());
+        for (unsigned i = 0; i < sz; ++i) {
+            term t;
+            t.constraint_id = id;
+            t.var_id = c[i].var();
+            t.sense =  c[i].sign();
+            var_term[t.var_id].push_back(t);
+            constraint_term[id].push_back(t);
+        }
+        constraint_k.push_back(k);                
+    }
+
     local_search::local_search(solver& s) {
-
-        // TBD: use solver::copy as a guideline for importing state from a solver.
-
-        // TBD initialize variables
-        s.num_vars();
-
         // copy units
         unsigned trail_sz = s.init_trail_size();
         for (unsigned i = 0; i < trail_sz; ++i) {
-            unsigned id = constraint_term.size();
+            add_clause(1, s.m_trail.c_ptr() + i);
-            term t;
-            t.constraint_id = id;
-            t.var_id = s.m_trail[i].var();
-            t.sense =  s.m_trail[i].sign();
-            var_term[t.var_id].push_back(t);
-            constraint_term.push_back(svector<term>());
-            constraint_term[id].push_back(t);
-            constraint_k.push_back(0);
         }
 
-        // TBD copy binary:
+        // copy binary clauses
-        s.m_watches.size();
         {
             unsigned sz = s.m_watches.size();
             for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
@@ -189,45 +193,62 @@ namespace sat {
                     literal l2 = it->get_literal();
                     if (l.index() > l2.index()) 
                         continue;
-
+                    literal ls[2] = { l, l2 };
-                    unsigned id = constraint_term.size();
+                    add_clause(2, ls);
-                    constraint_term.push_back(svector<term>());
-                    
-                    // TBD: add clause l, l2;
-
-                    constraint_k.push_back(1);
                 }
             }
         }
 
-
+        // copy clauses
         clause_vector::const_iterator it =  s.m_clauses.begin();
         clause_vector::const_iterator end = s.m_clauses.end();
         for (; it != end; ++it) {
-            clause const& c = *(*it);
+            clause& c = *(*it);
-            unsigned sz = c.size();
+            add_clause(c.size(), c.begin());
-            unsigned id = constraint_term.size();
-            constraint_term.push_back(svector<term>());
-            for (unsigned i = 0; i < sz; ++i) {
-                term t;
-                t.constraint_id = id;
-                t.var_id = c[i].var();
-                t.sense =  c[i].sign();
-                var_term[t.var_id].push_back(t);
-                constraint_term[id].push_back(t);
-            }
-            constraint_k.push_back(sz-1);
         }
 
-        // TBD initialize cardinalities from m_ext, retrieve cardinality constraints.
+        // copy cardinality clauses
+        card_extension* ext = dynamic_cast<card_extension*>(s.get_extension());
+        if (ext) {
+            literal_vector lits;
+            unsigned sz = ext->m_cards.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                card_extension::card& c = *ext->m_cards[i];
+                unsigned n = c.size();
+                unsigned k = c.k();
+
+                // c.lit() <=> c.lits() >= k
+                // 
+                //    (c.lits() < k) or c.lit()
+                // =  (c.lits() + (n - k - 1)*~c.lit()) <= n    
+                //
+                //    ~c.lit() or (c.lits() >= k)
+                // =  ~c.lit() or (~c.lits() <= n - k)
+                // =  k*c.lit() + ~c.lits() <= n 
+                // 
+
+                lits.reset();
+                for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]);
+                for (unsigned j = 0; j < n - k - 1; ++j) lits.push_back(~c.lit());
+                add_cardinality(lits.size(), lits.c_ptr(), n);
+                
+                lits.reset();
+                for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]);
+                for (unsigned j = 0; j < k; ++j) lits.push_back(c.lit());
+                add_cardinality(lits.size(), lits.c_ptr(), n);
+            }
+            //
             // optionally handle xor constraints.
+            //
+            SASSERT(ext->m_xors.empty());            
+        }
+
 
         num_vars = s.num_vars();
         num_constraints = constraint_term.size();
     }
     
     local_search::~local_search() {
-
     }
     
     void local_search::add_soft(literal l, double weight) {
@@ -235,6 +256,46 @@ namespace sat {
     }
     
     lbool local_search::operator()() {
+	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();
+	// ################## start ######################
+	//cout << "Start initialize and local search, restart in every " << max_steps << " steps" << endl;
+	for (unsigned tries = 0; ; ++tries) {
+            init();
+            for (int step = 1; step <= max_steps; ++step) {
+                // feasible
+                if (m_unsat_stack.empty()) {
+                    calculate_and_update_ob();
+                    if (best_objective_value >= best_known_value) {
+                        reach_known_best_value = true;
+                        break;
+                    }
+                }
+                flipvar = pick_var();
+                flip(flipvar);
+                time_stamp[flipvar] = step;
+            }
+            // take a look at watch
+            stop = clock();
+            elapsed_time = (double)(stop - start) / CLOCKS_PER_SEC;
+            if (elapsed_time > cutoff_time)
+                reach_cutoff_time = true;
+            if (reach_known_best_value || reach_cutoff_time)
+                break;
+	}
+	if (reach_known_best_value) {
+            std::cout << elapsed_time << "\n";
+	}
+	else
+            std::cout << -1 << "\n";
+        //print_solution();
+
+        // TBD: adjust return status
         return l_undef;
     }
 

src/sat/sat_local_search.h

@@ -122,6 +122,10 @@ namespace sat {
 
         void unsat(int constraint_id) { m_unsat_stack.push_back(constraint_id); }
 
+        void add_clause(unsigned sz, literal const* c);
+
+        void add_cardinality(unsigned sz, literal const* c, unsigned k);
+
         // swap the deleted one with the last one and pop
         void sat(int c) {
             int last_unsat_constraint = m_unsat_stack.back();

src/test/main.cpp

@@ -230,6 +230,7 @@ int main(int argc, char ** argv) {
     TST(get_consequences);
     TST(pb2bv);
     TST_ARGV(sat_lookahead);
+    TST_ARGV(sat_local_search);
     //TST_ARGV(hs);
 }
 

src/test/sat_local_search.cpp

@@ -0,0 +1,136 @@
+#include "sat_local_search.h"
+#include "sat_solver.h"
+
+static int build_instance(char *filename, sat::solver& s, sat::local_search& ls)
+{
+    char	line[16383];
+    int	cur_term;
+    // for temperally storage
+    int	temp[16383];
+    int	temp_count;
+
+    std::ifstream infile(filename);
+    //if (infile == NULL) //linux
+    if (!infile)
+        return 0;
+    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;
+
+
+    // write in the objective function
+    temp_count = 0;
+    infile >> cur_term;
+    while (cur_term != 0) {
+        temp[temp_count++] = cur_term;
+        infile >> cur_term;
+    }
+    int ob_num_terms = temp_count;
+
+#if 0
+    TBD make this compile:
+    ob_constraint = new ob_term[ob_num_terms + 1];
+    // coefficient
+    ob_constraint[0].coefficient = 0;	// virtual var: all variables not in ob are pointed to this var
+    for (i = 1; i <= ob_num_terms; ++i) {
+        ob_constraint[i].coefficient = temp[i - 1];
+    }
+
+    sat::literal_vector lits;
+    // ob variable
+    temp_count = 0;
+    infile >> cur_term;
+    while (cur_term != 0) {
+        temp[temp_count++] = cur_term;
+        infile >> cur_term;
+    }
+    if (temp_count != ob_num_terms) {
+        cout << "Objective function format error." << endl;
+        exit(-1);
+    }
+    for (i = 1; i <= ob_num_terms; ++i) {
+        ob_constraint[i].var_id = temp[i - 1];
+        coefficient_in_ob_constraint[ob_constraint[i].var_id] = ob_constraint[i].coefficient;
+    }
+    // read the constraints, one at a time
+    card_extension* ext = 0;
+    int k;
+    for (c = 1; c <= num_constraints; ++c) {        
+        lits.reset();
+        infile >> cur_term;
+        while (cur_term != 0) {
+            lits.push_back(sat::literal(abs(cur_term), cur_term > 0));
+            infile >> cur_term;
+        }
+        infile >> k;
+        ext->add_at_least(null_bool_var, lits, lits.size() - k);
+    }
+#endif
+
+    infile.close();
+
+
+#if 0
+    Move all of this to initialization code for local search solver:
+
+    // create var_term array
+    for (v = 1; v <= num_vars; ++v) {
+        var_term[v] = new term[var_term_count[v]];
+        var_term_count[v] = 0; // reset to 0, for building up the array
+    }
+    // scan all constraints to build up var term arrays
+    for (c = 1; c <= num_constraints; ++c) {
+        for (i = 0; i < constraint_term_count[c]; ++i) {
+            v = constraint_term[c][i].var_id;
+            var_term[v][var_term_count[v]++] = constraint_term[c][i];
+        }
+    }
+
+
+    // build neighborhood relationship
+    bool *is_neighbor;
+    is_neighbor = new bool[num_vars + 1];
+    for (v = 1; v <= num_vars; ++v) {
+        // init as not neighbor
+        for (i = 1; i <= num_vars; ++i) {
+            is_neighbor[i] = false;
+        }
+        temp_count = 0;
+        // for each constraint v appears
+        for (i = 0; i < var_term_count[v]; ++i) {
+            c = var_term[v][i].constraint_id;
+            for (j = 0; j < constraint_term_count[c]; ++j) {
+                if (constraint_term[c][j].var_id == v)
+                    continue;
+                // not neighbor yet
+                if (!is_neighbor[constraint_term[c][j].var_id]) {
+                    is_neighbor[constraint_term[c][j].var_id] = true;
+                    temp[temp_count++] = constraint_term[c][j].var_id;
+                }
+            }
+        }
+        // create and build neighbor
+        var_neighbor_count[v] = temp_count;
+        var_neighbor[v] = new int[var_neighbor_count[v]];
+        for (i = 0; i < var_neighbor_count[v]; ++i) {
+            var_neighbor[v][i] = temp[i];
+        }
+    }
+    delete[] is_neighbor;
+
+#endif
+    return 1;
+}
+
+void tst_sat_local_search(char ** argv, int argc, int& i) {
+    if (argc != i + 2) {
+        std::cout << "require dimacs file name\n";
+        return;
+    }
+    // sat::solver s;
+    // populate the sat solver with clauses and cardinality consrtaints from the input
+    // call the lookahead solver.
+    // TBD
+}