Some notions were confused. Also, better peformance now

Author: msoos

src/arjun.cpp

@@ -224,7 +224,8 @@ set_get_macro(bool, distill)
 set_get_macro(bool, intree)
 set_get_macro(bool, bve_pre_simplify)
 set_get_macro(bool, simp)
-set_get_macro(uint32_t, incidence_sort)
+set_get_macro(uint32_t, unknown_sort)
+set_get_macro(uint32_t, incidence_count)
 set_get_macro(bool, or_gate_based)
 set_get_macro(bool, xor_gates_based)
 set_get_macro(bool, probe_based)

src/arjun.h

@@ -92,7 +92,8 @@ namespace ArjunNS {
         void set_intree(bool intree);
         void set_simp(bool simp);
         void set_bve_pre_simplify(bool bve_pre_simp);
-        void set_incidence_sort(uint32_t incidence_sort);
+        void set_unknown_sort(uint32_t unknown_sort);
+        void set_incidence_count(uint32_t incidence_count);
         void set_or_gate_based(bool or_gate_based);
         void set_xor_gates_based(bool xor_gates_based);
         void set_probe_based(bool probe_based);
@@ -121,7 +122,8 @@ namespace ArjunNS {
         bool get_distill() const;
         bool get_intree() const;
         bool get_bve_pre_simplify() const;
-        uint32_t get_incidence_sort() const;
+        uint32_t get_incidence_count() const;
+        uint32_t get_unknown_sort() const;
         bool get_or_gate_based() const;
         bool get_xor_gates_based() const;
         bool get_probe_based() const;

src/common.cpp

@@ -212,11 +212,11 @@ void Common::get_incidence()
     assert(inc.size() == orig_num_vars*2);
     for(uint32_t i = 0; i < orig_num_vars; i++) {
         Lit l = Lit(i, true);
-        if (conf.incidence_sort == 10) {
+        if (conf.incidence_count == 1) {
             incidence[l.var()] = inc[l.toInt()] + inc[(~l).toInt()];
-        } else if (conf.incidence_sort == 11) {
+        } else if (conf.incidence_count == 2) {
             incidence[l.var()] = std::max(inc[l.toInt()], inc[(~l).toInt()]);
-        } else {
+        } else if (conf.incidence_count == 3) {
             incidence[l.var()] = std::min(inc[l.toInt()],inc[(~l).toInt()]);
         }
     }
@@ -290,14 +290,7 @@ bool Common::preproc_and_duplicate()
     seen.resize(solver->nVars(), 0);
 
     get_incidence();
-    if (conf.incidence_sort == 4 || conf.incidence_sort == 5) {
-        #ifdef LOUVAIN_COMMS
-        calc_community_parts();
-        #else
-        cout << "ERROR: you must compile with louvain community libraries for this to work. Install https://github.com/meelgroup/louvain-community first." << endl;
-        exit(-1);
-        #endif
-    }
+    calc_community_parts();
     if (conf.simp && !simplify()) return false;
     get_incidence();
     duplicate_problem();
@@ -315,13 +308,18 @@ bool Common::preproc_and_duplicate()
     return true;
 }
 
-#ifdef LOUVAIN_COMMS
 void Common::calc_community_parts()
 {
-    double myTime = cpuTime();
-    if (conf.verb) {
-        cout << "c [arjun] Calculating Louvain Communities..." << endl;
+    if (!(conf.unknown_sort == 4 || conf.unknown_sort == 5)) {
+        return;
     }
+    #ifndef LOUVAIN_COMMS
+    cout << "ERROR: you must compile with louvain community libraries for this to work."
+        << " Install https://github.com/meelgroup/louvain-community first." << endl;
+    exit(-1);
+    #else
+    double myTime = cpuTime();
+    verb_print(1, "[arjun] Calculating Louvain Communities...");
 
     vector<vector<Lit>> cnf;
     solver->start_getting_small_clauses(
@@ -415,11 +413,8 @@ void Common::calc_community_parts()
     }
     solver->end_getting_small_clauses();
 
-    if (conf.verb) {
-        cout << "c [mis-comm] Number of communities: " << commpart_incs.size()
-        << " T: " << (cpuTime() - myTime)
-        << endl;
-    }
+    verb_print(1, "[mis-comm] Number of communities: " << commpart_incs.size() \
+            << " T: " << (cpuTime() - myTime));
+#endif
 }
 
-#endif

src/common.h

@@ -127,9 +127,7 @@ struct Common
     void start_with_clean_sampling_set();
     void duplicate_problem();
     void get_incidence();
-    #ifdef LOUVAIN_COMMS
     void calc_community_parts();
-    #endif
     void set_up_solver();
     vector<Lit> get_cnf();
     std::mt19937 random_source = std::mt19937(0);
@@ -266,7 +264,6 @@ struct IncidenceSorterCommPart
         if (part_a_inc != part_b_inc) {
             return part_a_inc < part_b_inc;
         }
-        return false;
 
         auto a_inc = comm->incidence[a];
         auto b_inc = comm->incidence[b];
@@ -311,17 +308,17 @@ struct IncidenceSorterCommPartToOtherComm
 template<class T>
 void Common::sort_unknown(T& unknown)
 {
-    if (conf.incidence_sort == 1 || conf.incidence_sort >= 10) {
+    if (conf.unknown_sort == 1 || conf.unknown_sort >= 10) {
         std::sort(unknown.begin(), unknown.end(), IncidenceSorter<uint32_t>(incidence));
-    } else if (conf.incidence_sort == 2) {
+    } else if (conf.unknown_sort == 2) {
         std::sort(unknown.begin(), unknown.end(), IncidenceSorter2<uint32_t>(incidence, incidence_probing));
-    } else if (conf.incidence_sort == 3) {
+    } else if (conf.unknown_sort == 3) {
         std::sort(unknown.begin(), unknown.end(), IncidenceSorter<uint32_t>(incidence_probing));
-    } else if (conf.incidence_sort == 4) {
+    } else if (conf.unknown_sort == 4) {
         std::sort(unknown.begin(), unknown.end(), IncidenceSorterCommPart(this));
-    } else if (conf.incidence_sort == 5) {
+    } else if (conf.unknown_sort == 5) {
         std::sort(unknown.begin(), unknown.end(), IncidenceSorterCommPartToOtherComm(this));
-    } else if (conf.incidence_sort == 6) {
+    } else if (conf.unknown_sort == 6) {
         std::shuffle(unknown.begin(), unknown.end(), random_source);
     } else {
         cout << "ERROR: wrong sorting mechanism given" << endl;

src/config.h

@@ -38,7 +38,8 @@ struct Config {
     int distill = 1;
     int intree = 1;
     int bve_pre_simplify = 1;
-    int incidence_sort = 10;
+    int incidence_count = 3; // this determines what incidence MEANS
+    int unknown_sort = 4; // this determines HOW we sort
     int or_gate_based = 1;
     int xor_gates_based = 1;
     int ite_gate_based = 1;

src/main.cpp

@@ -86,7 +86,7 @@ void add_arjun_options()
     ("verb,v", po::value(&conf.verb)->default_value(conf.verb), "verbosity")
     ("seed,s", po::value(&conf.seed)->default_value(conf.seed), "Seed")
 //     ("bve", po::value(&conf.bve)->default_value(conf.bve), "bve")
-    ("sort", po::value(&conf.incidence_sort)->default_value(conf.incidence_sort),
+    ("sort", po::value(&conf.unknown_sort)->default_value(conf.unknown_sort),
      "Which sorting mechanism.")
     ("recomp", po::value(&recompute_sampling_set)->default_value(recompute_sampling_set),
      "Recompute sampling set even if it's part of the CNF")
@@ -360,7 +360,7 @@ void set_config(ArjunNS::Arjun* arj) {
     arj->set_specified_order_fname(conf.specified_order_fname);
     arj->set_intree(conf.intree);
     arj->set_bve_pre_simplify(conf.bve_pre_simplify);
-    arj->set_incidence_sort(conf.incidence_sort);
+    arj->set_unknown_sort(conf.unknown_sort);
     if (gates) {
       arj->set_or_gate_based(conf.or_gate_based);
       arj->set_ite_gate_based(conf.ite_gate_based);

src/simplify.cpp

@@ -377,7 +377,6 @@ bool Common::remove_definable_by_gates()
         }
     }
 
-
     if (conf.verb > 4) cout << "c [arjun-simp] XOR Potential: " << potential << endl;
 
     order_sampl_set_for_simp();
@@ -386,7 +385,6 @@ bool Common::remove_definable_by_gates()
     // If this is large, it means it'd get removed anyway:
     //       bottom of the pie, we go through the pile in reverse order to try to remove
     vector<double> var_to_rel_position(orig_num_vars, 1.0);
-    std::sort(sampling_set->begin(), sampling_set->end(), IncidenceSorter<uint32_t>(incidence));
     for(uint32_t i = 0; i < sampling_set->size(); i++) {
         assert(sampling_set->at(i) < orig_num_vars);
         var_to_rel_position[sampling_set->at(i)] = (double)i/(double)sampling_set->size();
@@ -399,7 +397,7 @@ bool Common::remove_definable_by_gates()
             continue;
         }
 
-        // Only try removing if it's at the bottom X percent of incidence_sort
+        // Only try removing if it's at the bottom X percent of unknown_sort
         // If 0.01 is SMALLER, then we have to remove with backward LESS
         if (var_to_rel_position[v] < conf.no_gates_below) continue;
 
@@ -499,7 +497,7 @@ bool Common::remove_definable_by_gates()
 void Common::order_sampl_set_for_simp()
 {
     get_incidence();
-    std::sort(sampling_set->begin(), sampling_set->end(), IncidenceSorter<uint32_t>(incidence));
+    sort_unknown(*sampling_set);
     std::reverse(sampling_set->begin(), sampling_set->end()); //we want most likely independent as last
 }