Deal with projection set

src/sbva.cpp

@@ -139,14 +139,15 @@ class Formula {
 
     Formula(SBVA::Config& _config) : config(_config) { }
 
-    void init_cnf(uint32_t _num_vars) {
+    void init_cnf(uint32_t _num_vars, const set<uint32_t>* _sampl_vars) {
         num_vars = _num_vars;
         lit_count_adjust.resize(num_vars * 2);
         lit_to_clauses.resize(num_vars * 2);
         adjacency_matrix_width = num_vars * 4;
         adjacency_matrix.resize(num_vars);
         found_header = true;
         curr_clause = 0;
+        if (_sampl_vars != nullptr) sampl_vars = *_sampl_vars;
         assert(cache == nullptr);
         cache = new ClauseCache;
     }
@@ -335,7 +336,8 @@ class Formula {
         return std::make_pair(num_vars, num_clauses-adj_deleted);
     }
 
-    vector<int> get_cnf(uint32_t& ret_num_vars, uint32_t& ret_num_cls) {
+    vector<int> get_cnf(uint32_t& ret_num_vars, uint32_t& ret_num_cls,
+            set<uint32_t>* ret_sampl_vars) {
         vector<int> ret;
         ret_num_cls = num_clauses - adj_deleted;
         ret_num_vars = num_vars;
@@ -346,6 +348,7 @@ class Formula {
             }
             ret.push_back(0);
         }
+        if (ret_sampl_vars != nullptr) *ret_sampl_vars = sampl_vars;
         return ret;
     }
 
@@ -713,11 +716,11 @@ class Formula {
                     int clause_idx = get<1>(pair);
                     int idx = get<2>(pair);
 
-                    (*matched_clauses_swap)[(insert_idx)] = (*matched_clauses)[(idx)];
-                    (*matched_clauses_id_swap)[(insert_idx)] = (*matched_clauses_id)[(idx)];
+                    (*matched_clauses_swap)[(insert_idx)] = (*matched_clauses)[idx];
+                    (*matched_clauses_id_swap)[(insert_idx)] = (*matched_clauses_id)[idx];
                     insert_idx += 1;
 
-                    clauses_to_remove.push_back(make_tuple(clause_idx, (*matched_clauses_id)[(idx)]));
+                    clauses_to_remove.push_back(make_tuple(clause_idx, (*matched_clauses_id)[idx]));
                 }
 
                 swap(matched_clauses,matched_clauses_swap);
@@ -737,14 +740,10 @@ class Formula {
                 }
             }
 
-            if (matched_lits.size() == 1) {
-                continue;
-            }
-
+            if (matched_lits.size() == 1) continue;
             if (matched_lits.size() <= config.matched_lits_cutoff &&
-                    matched_clauses->size() <= config.matched_cls_cutoff) {
+                    matched_clauses->size() <= config.matched_cls_cutoff)
                 continue;
-            }
 
             int matched_clause_count = matched_clauses->size();
             int matched_lit_count = matched_lits.size();
@@ -756,12 +755,10 @@ class Formula {
                 }
                 cout << endl;
                 cout << "  mclauses:\n";
-                for (int matched_clause : (*matched_clauses)) {
+                for (int matched_clause : *matched_clauses) {
                     clauses[matched_clause].print("   -> ");
                 }
-                cout << endl;
-
-                cout << "--------------------" << endl;
+                cout << endl << "--------------------" << endl;
             }
             assert(lit_to_clauses.size() == num_vars*2);
             assert(lit_count_adjust.size() == num_vars*2);
@@ -770,6 +767,23 @@ class Formula {
             num_vars += 1;
             int new_var = num_vars;
 
+            // Check if all in proj. Then we can add it to the sampl_vars
+            if (config.preserve_model_cnt) {
+                bool add_to_sampl_vars = true;
+                for (int matched_clause : *matched_clauses) {
+                    for(const auto&l: clauses[matched_clause].lits) {
+                        if (sampl_vars.count(abs(l)) == 0) {
+                            add_to_sampl_vars = false;
+                            break;
+                        }
+                    }
+                }
+                if (add_to_sampl_vars) sampl_vars.insert(new_var);
+                if (config.verbosity)
+                    cout << "Adding " << new_var << " to sampl_vars? "
+                        << add_to_sampl_vars << endl;
+            }
+
             // Prepare to add new clauses.
             uint32_t new_sz = num_clauses + matched_lit_count + matched_clause_count +
                 (config.preserve_model_cnt ? 1 : 0);
@@ -835,12 +849,15 @@ class Formula {
             }
 
             // Preserving model count:
-            //
-            // The only case where we add a model is if both assignments for the auxiiliary variable satisfy the formula
-            // for the same assignment of the original variables. This only happens if all(matched_lits) *AND*
+            // -----
+            // The only case where we add a model is if both assignments for the
+            // auxiiliary variable satisfy the formula
+            // for the same assignment of the original variables.
+            // This only happens if all(matched_lits) *AND*
             // all(matches_clauses) are satisfied.
             //
-            // The easiest way to fix this is to add one clause that constrains all(matched_lits) => -f
+            // The easiest way to fix this is to add one clause that
+            // constrains all(matched_lits) => -f
             if (config.preserve_model_cnt) {
                 int new_clause = num_clauses + matched_lit_count + matched_clause_count;
                 auto cls = Clause();
@@ -939,6 +956,7 @@ class Formula {
     size_t num_clauses = 0;
     size_t curr_clause = 0;
     int adj_deleted = 0;
+    set<uint32_t> sampl_vars;
     vector<Clause> clauses;
     SBVA::Config& config;
     ClauseCache* cache = nullptr;
@@ -981,16 +999,17 @@ void CNF::to_proof(FILE* file) {
     f->to_proof(file);
 }
 
-vector<int> CNF::get_cnf(uint32_t& ret_num_vars, uint32_t& ret_num_cls) {
+vector<int> CNF::get_cnf(uint32_t& ret_num_vars, uint32_t& ret_num_cls,
+        set<uint32_t>* ret_sampl_vars) {
     Formula* f = (Formula*)data;
-    return f->get_cnf(ret_num_vars, ret_num_cls);
+    return f->get_cnf(ret_num_vars, ret_num_cls, ret_sampl_vars);
 }
 
 
-void CNF::init_cnf(uint32_t num_vars, Config& config) {
+void CNF::init_cnf(uint32_t num_vars, Config& config, const set<uint32_t>* _sampl_vars) {
     assert(data == nullptr);
     Formula* f = new Formula(config);
-    f->init_cnf(num_vars);
+    f->init_cnf(num_vars, _sampl_vars);
     data = (void*)f;
 }
 

src/sbva.h

@@ -24,12 +24,11 @@ THE SOFTWARE.
 #pragma once
 
 #include <cstdio>
-#include <ctime>
 #include <limits>
 #include <vector>
+#include <set>
 #include <cstdint>
 #include <utility>
-#include <functional>
 
 namespace SBVA {
 
@@ -53,15 +52,17 @@ struct CNF {
     void run(Tiebreak t);
 
     std::pair<int, int> to_cnf(FILE*);
-    std::vector<int> get_cnf(uint32_t& ret_num_vars, uint32_t& ret_num_cls);
+    std::vector<int> get_cnf(uint32_t& ret_num_vars, uint32_t& ret_num_cls,
+            std::set<uint32_t>* ret_sampl_vars = nullptr);
 
     void to_proof(FILE*);
 
     // Read in CNF from file
     void parse_cnf(FILE* file, Config& config);
 
     // This is how to add a CNF clause by clause
-    void init_cnf(uint32_t num_vars, Config& config);
+    void init_cnf(uint32_t num_vars, Config& config,
+            const std::set<uint32_t>* sampl_vars = nullptr);
     void add_cl(const std::vector<int>& cl_lits);
     void finish_cnf();
 

src/test.cpp

@@ -29,6 +29,7 @@ THE SOFTWARE.
 
 #include "sbva.h"
 #include <iostream>
+#include <set>
 using std::cout;
 using std::endl;