可以运行的clause LS，下一步移植到CCAnr到本程序

.vscode/launch.json

@@ -9,7 +9,7 @@
             "type": "cppdbg",
             "request": "launch",
             "program": "${workspaceFolder}/atpg",
-            "args": ["test.bench"],
+            "args": ["c432.bench"],
             "stopAtEntry": false,
             "cwd": "${fileDirname}",
             "environment": [],

circuit.cpp

@@ -58,7 +58,7 @@ void Circuit::init_topo_index() {
 void Circuit::print_circuit() {
     static const char* type2name[9] = {"AND", "NAND", "OR", "NOR", "XOR", "XNOR", "NOT", "BUF", "IN"};
     for(Gate* gate : gates) {
-        printf("Gate: %3s (t:%4s v:%d pi:%d po:%d s:%d p:%d s0:%d s1:%d fpl0:%d fpl1:%d)  Inputs:", gate->name.c_str(), type2name[gate->type], gate->value, gate->pi, gate->po, gate->stem, gate->propagate, gate->fault_detected[0], gate->fault_detected[1], gate->fault_propagate_length[0], gate->fault_propagate_length[1]);
+        printf("Gate: %3s (t:%4s v:%d ss:%d pi:%d po:%d s:%d p:%d s0:%d s1:%d fpl0:%d fpl1:%d)  Inputs:", gate->name.c_str(), type2name[gate->type], gate->value, gate->stem_satisfied, gate->pi, gate->po, gate->stem, gate->propagate, gate->fault_detected[0], gate->fault_detected[1], gate->fault_propagate_length[0], gate->fault_propagate_length[1]);
         for(Gate* in : gate->fan_ins) {
             printf(" %s(%d)", in->name.c_str(), gate->is_detected(in));
         }

clause.cpp

@@ -1,5 +1,7 @@
 #include "clause.h"
 
+#include <fstream>
+
 ll Clause::total_cost;
 
 void Clause::update_satisfied_lit_count() {
@@ -44,6 +46,21 @@ std::vector<Clause*> *lit_related_clauses;
 int *lit_value;
 int *CC;
 
+void write_cnf() {
+    std::ofstream f("test.cnf");
+
+    f << "p cnf " << num_vars << " " << num_clauses << std::endl;
+
+    for(auto& c : clauses) {
+        for(auto &lit : c->lits) {
+            f << lit << " ";
+        }
+        f << "0" << std::endl;
+    }
+
+    f.close();
+}   
+
 void flip(int var) {
 
     // printf("value: [ ");
@@ -74,8 +91,6 @@ void flip(int var) {
     }
     CC[var] = 0;
 
-
-
 }
 
 void add_to_tmp_clause(int x) {
@@ -121,11 +136,14 @@ void init_data_structs(Circuit* circuit) {
             lit_related_clauses[abs(lit)].push_back(clause);
         }
     }
+
+    write_cnf();
 }
 
 void reset_data_structs() {
     for(int i=1; i<=num_vars; i++) {
-        lit_value[i] = 0;
+        lit_value[i] = rand() % 2;
+        CC[i] = 1;
     }
 }
 
@@ -145,7 +163,7 @@ void build_clauses(Circuit* circuit) {
                 add_to_tmp_clause(0);
 
                 add_to_tmp_clause(g->id);
-                add_to_tmp_clause(-(g->fan_ins[0]->id));
+                add_to_tmp_clause(g->fan_ins[0]->id);
                 add_to_tmp_clause(0);
                 break;
             case Gate::BUF:
@@ -158,52 +176,52 @@ void build_clauses(Circuit* circuit) {
                 add_to_tmp_clause(0);
                 break;
             case Gate::AND:
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(-g->id);
                     add_to_tmp_clause(g->fan_ins[i]->id);
                     add_to_tmp_clause(0);
                 }
 
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(-g->fan_ins[i]->id);
                 }
                 add_to_tmp_clause(g->id);
                 add_to_tmp_clause(0);
                 break;
             case Gate::NAND:
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(g->id);
                     add_to_tmp_clause(g->fan_ins[i]->id);
                     add_to_tmp_clause(0);
                 }
 
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(-g->fan_ins[i]->id);
                 }
                 add_to_tmp_clause(-g->id);
                 add_to_tmp_clause(0);
                 break;
             case Gate::OR:
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(g->fan_ins[i]->id);
                 }
                 add_to_tmp_clause(-g->id);
                 add_to_tmp_clause(0);
 
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(g->id);
                     add_to_tmp_clause(-g->fan_ins[i]->id);
                     add_to_tmp_clause(0);
                 }
                 break;
             case Gate::NOR:
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(g->fan_ins[i]->id);
                 }
                 add_to_tmp_clause(g->id);
                 add_to_tmp_clause(0);
 
-                for(int i=1; i<g->fan_ins.size(); i++) {
+                for(int i=0; i<g->fan_ins.size(); i++) {
                     add_to_tmp_clause(-g->id);
                     add_to_tmp_clause(-g->fan_ins[i]->id);
                     add_to_tmp_clause(0);

clause.h

@@ -32,5 +32,7 @@ namespace ClauseLS {
     void add_to_tmp_clause(int x);
     void build_clauses(Circuit* circuit);
 
+    void write_cnf();
+
     void flip(int var);
 }

ls.cpp

@@ -22,22 +22,17 @@ bool Circuit::local_search() {
     for(int i=0; i<MAX_STEPS; i++) {
 
         auto start = std::chrono::system_clock::now();
-        printf("[FLIP] stem: %lld, fault:%lld, stem_cnt: %lld, fault_cnt:%lld, fpl_score: %lld citcuit-score: %lld\n", stem_total_cost, fault_total_weight, stem_total_cnt, fault_total_cnt, fault_propagate_score, ls_circuit_score());
+        printf("[FLIP] stem: %lld, fault:%lld, stem_cnt: %lld, fault_cnt:%lld, fpl_score: %lld citcuit-score: %lld\n", stem_total_cost, fault_total_weight, stems.size() - stem_total_cnt, fault_total_cnt, fault_propagate_score, ls_circuit_score());
 
         int id = ls_pick();
 
-        printf("pick: %d\n", id);
+        ls_flip_var(id);
-
-        //printf("flip: %d.  fc: %d.  %d\n", id, ClauseLS::falsified_clauses.size(), Clause::total_cost);
 
         if(stem_total_cnt == stems.size()) {
-            //printf("FIND SOLUTION!\n");
+            printf("FIND SOLUTION!\n");
-            printf("[UP] stem: %lld, fault:%lld, stem_cnt: %lld, fault_cnt:%lld, fpl_score: %lld citcuit-score: %lld\n", stem_total_cost, fault_total_weight, stem_total_cnt, fault_total_cnt, fault_propagate_score, ls_circuit_score());
             break;
         }
 
-        ls_flip_var(id);
-
         assert(is_valid_circuit());
 
         auto end = std::chrono::system_clock::now();
@@ -55,6 +50,8 @@ bool Circuit::local_search() {
 
 void Circuit::ls_statistics() {
 
+    static int pattern = 0;
+
     int last_undetect = global_fault_undetected_count;
 
     for(Gate* g : gates) {
@@ -68,10 +65,13 @@ void Circuit::ls_statistics() {
         }
     }
 
-    printf("coverage: %.2f%% undected_fault: %d delta: %d\n", 
+    if(global_fault_undetected_count - last_undetect < 0) {
-        (gates.size() * 2.0 - global_fault_undetected_count) / (gates.size() * 2.0) * 100,
+        pattern++;
-        global_fault_undetected_count, global_fault_undetected_count - last_undetect);
+    }
 
+    printf("coverage: %.2f%% undected_fault: %d delta: %d total-pt:%d\n", 
+        (gates.size() * 2.0 - global_fault_undetected_count) / (gates.size() * 2.0) * 100,
+        global_fault_undetected_count, global_fault_undetected_count - last_undetect, pattern);
 
     printf("flip-cnt: %d flip-time: %.3fs update-cnt: %d update-time: %.3fs\n", flip_cnt, flip_time, update_cnt, update_time);
     printf("time-per-update: %.2fms\n", update_time / update_cnt * 1000);
@@ -136,9 +136,12 @@ int Circuit::ls_pick() {
     if(var == -1) {
         ls_update_weight();
 
-        printf("[UP]\n");
+        printf("[UP] stem: %lld, fault:%lld, stem_cnt: %lld, fault_cnt:%lld, fpl_score: %lld citcuit-score: %lld\n", stem_total_cost, fault_total_weight, stems.size() - stem_total_cnt, fault_total_cnt, fault_propagate_score, ls_circuit_score());
 
-        printf("fals: %d\n", ClauseLS::falsified_clauses.size());
+        if(ClauseLS::falsified_clauses.size() == 0) {
+            print_circuit();
+            exit(-1);
+        }
 
         auto it = std::next(ClauseLS::falsified_clauses.begin(), rand() % ClauseLS::falsified_clauses.size());
 
@@ -215,10 +218,6 @@ void Circuit::ls_init_stems() {
 }
 
 void Circuit::ls_flip_var(int var) {
-
-
-    
-
     ClauseLS::flip(var);
 
     if(id2gate.count(var) && id2gate[var]->stem) {
@@ -261,6 +260,15 @@ void Circuit::ls_init_weight() {
 
 void Circuit::ls_random_circuit() {
 
+    // random init clauseLS
+    for(int i=1; i<=ClauseLS::num_vars; i++) {
+        int new_v = rand() % 2;
+        if(new_v != ClauseLS::lit_value[i]) {
+            //ls_flip_var(i);
+            ClauseLS::flip(i);
+        }
+    }
+
     // init assignment
     for(Gate* s : stems) {
         s->value = ClauseLS::lit_value[s->id];
@@ -332,6 +340,7 @@ void Circuit::ls_reset_data() {
 
 
 void Circuit::ls_flip_stem(Gate* stem) {
+
     stem->value = !stem->value;
 
     // update CC

makefile

@@ -7,7 +7,7 @@
 #编译工具用g++，以同时支持C和C++程序，以及二者的混合编译
 CC=g++
 
-CPPFLAGS=-O0 -std=c++17 -g
+CPPFLAGS=-O3 -std=c++17
  
 #使用$(winldcard *.c)来获取工作目录下的所有.c文件的列表
 #sources:=main.cpp command.c

option.h

@@ -1,9 +1,9 @@
 #pragma once
 
-const double SP = 0.01;
+const double SP = 0.0001;
 const int MAX_STEPS = 1000000000;
 
-const int SAMPLING_COUNT = 1000;
+const int SAMPLING_COUNT = 25;
 
 const int STEM_INC = 2;
 const int STEM_WEIGHT_MAX = 1e9;

test.cnf

@@ -0,0 +1,515 @@
+p cnf 196 514
+-37 -1 0
+37 1 0
+-38 -2 0
+38 2 0
+-39 -4 0
+39 4 0
+-40 -6 0
+40 6 0
+-41 -8 0
+41 8 0
+-42 -10 0
+42 10 0
+-43 -12 0
+43 12 0
+-44 -14 0
+44 14 0
+-45 -16 0
+45 16 0
+-46 -18 0
+46 18 0
+-47 -20 0
+47 20 0
+-48 -22 0
+48 22 0
+-49 -24 0
+49 24 0
+-50 -26 0
+50 26 0
+-51 -28 0
+51 28 0
+-52 -30 0
+52 30 0
+-53 -32 0
+53 32 0
+-54 -34 0
+54 34 0
+55 37 0
+55 2 0
+-37 -2 -55 0
+3 38 56 0
+-56 -3 0
+-56 -38 0
+5 38 57 0
+-57 -5 0
+-57 -38 0
+58 39 0
+58 6 0
+-39 -6 -58 0
+61 41 0
+61 10 0
+-41 -10 -61 0
+64 43 0
+64 14 0
+-43 -14 -64 0
+67 45 0
+67 18 0
+-45 -18 -67 0
+70 47 0
+70 22 0
+-47 -22 -70 0
+73 49 0
+73 26 0
+-49 -26 -73 0
+76 51 0
+76 30 0
+-51 -30 -76 0
+79 53 0
+79 34 0
+-53 -34 -79 0
+7 40 59 0
+-59 -7 0
+-59 -40 0
+9 40 60 0
+-60 -9 0
+-60 -40 0
+11 42 62 0
+-62 -11 0
+-62 -42 0
+13 42 63 0
+-63 -13 0
+-63 -42 0
+15 44 65 0
+-65 -15 0
+-65 -44 0
+17 44 66 0
+-66 -17 0
+-66 -44 0
+19 46 68 0
+-68 -19 0
+-68 -46 0
+21 46 69 0
+-69 -21 0
+-69 -46 0
+23 48 71 0
+-71 -23 0
+-71 -48 0
+25 48 72 0
+-72 -25 0
+-72 -48 0
+27 50 74 0
+-74 -27 0
+-74 -50 0
+29 50 75 0
+-75 -29 0
+-75 -50 0
+31 52 77 0
+-77 -31 0
+-77 -52 0
+33 52 78 0
+-78 -33 0
+-78 -52 0
+35 54 80 0
+-80 -35 0
+-80 -54 0
+36 54 81 0
+-81 -36 0
+-81 -54 0
+-82 55 0
+-82 58 0
+-82 61 0
+-82 64 0
+-82 67 0
+-82 70 0
+-82 73 0
+-82 76 0
+-82 79 0
+-55 -58 -61 -64 -67 -70 -73 -76 -79 82 0
+-83 -82 0
+83 82 0
+-84 -82 0
+84 82 0
+-85 -82 0
+85 82 0
+-86 -83 -55 0
+-86 83 55 0
+86 -83 55 0
+86 83 -55 0
+-87 -83 -58 0
+-87 83 58 0
+87 -83 58 0
+87 83 -58 0
+-88 -83 -61 0
+-88 83 61 0
+88 -83 61 0
+88 83 -61 0
+-89 -83 -64 0
+-89 83 64 0
+89 -83 64 0
+89 83 -64 0
+-90 -83 -67 0
+-90 83 67 0
+90 -83 67 0
+90 83 -67 0
+-91 -83 -70 0
+-91 83 70 0
+91 -83 70 0
+91 83 -70 0
+95 1 0
+95 84 0
+-1 -84 -95 0
+-92 -83 -73 0
+-92 83 73 0
+92 -83 73 0
+92 83 -73 0
+96 84 0
+96 4 0
+-84 -4 -96 0
+-93 -83 -76 0
+-93 83 76 0
+93 -83 76 0
+93 83 -76 0
+97 84 0
+97 8 0
+-84 -8 -97 0
+-94 -83 -79 0
+-94 83 79 0
+94 -83 79 0
+94 83 -79 0
+98 84 0
+98 12 0
+-84 -12 -98 0
+99 84 0
+99 16 0
+-84 -16 -99 0
+100 84 0
+100 20 0
+-84 -20 -100 0
+101 84 0
+101 24 0
+-84 -24 -101 0
+102 84 0
+102 28 0
+-84 -28 -102 0
+103 84 0
+103 32 0
+-84 -32 -103 0
+104 86 0
+104 56 0
+-86 -56 -104 0
+105 86 0
+105 57 0
+-86 -57 -105 0
+106 87 0
+106 59 0
+-87 -59 -106 0
+108 88 0
+108 62 0
+-88 -62 -108 0
+110 89 0
+110 65 0
+-89 -65 -110 0
+112 90 0
+112 68 0
+-90 -68 -112 0
+114 91 0
+114 71 0
+-91 -71 -114 0
+116 92 0
+116 74 0
+-92 -74 -116 0
+118 93 0
+118 77 0
+-93 -77 -118 0
+120 94 0
+120 80 0
+-94 -80 -120 0
+107 87 0
+107 60 0
+-87 -60 -107 0
+109 88 0
+109 63 0
+-88 -63 -109 0
+111 89 0
+111 66 0
+-89 -66 -111 0
+113 90 0
+113 69 0
+-90 -69 -113 0
+115 91 0
+115 72 0
+-91 -72 -115 0
+117 92 0
+117 75 0
+-92 -75 -117 0
+119 93 0
+119 78 0
+-93 -78 -119 0
+121 94 0
+121 81 0
+-94 -81 -121 0
+-130 104 0
+-130 106 0
+-130 108 0
+-130 110 0
+-130 112 0
+-130 114 0
+-130 116 0
+-130 118 0
+-130 120 0
+-104 -106 -108 -110 -112 -114 -116 -118 -120 130 0
+-122 -105 0
+122 105 0
+-123 -107 0
+123 107 0
+-124 -109 0
+124 109 0
+-125 -111 0
+125 111 0
+-126 -113 0
+126 113 0
+-127 -115 0
+127 115 0
+-128 -117 0
+128 117 0
+-129 -119 0
+129 119 0
+-131 -121 0
+131 121 0
+-132 -130 0
+132 130 0
+-133 -130 0
+133 130 0
+-134 -130 0
+134 130 0
+-135 -132 -104 0
+-135 132 104 0
+135 -132 104 0
+135 132 -104 0
+-136 -132 -106 0
+-136 132 106 0
+136 -132 106 0
+136 132 -106 0
+-137 -132 -108 0
+-137 132 108 0
+137 -132 108 0
+137 132 -108 0
+-138 -132 -110 0
+-138 132 110 0
+138 -132 110 0
+138 132 -110 0
+144 3 0
+144 133 0
+-3 -133 -144 0
+-139 -132 -112 0
+-139 132 112 0
+139 -132 112 0
+139 132 -112 0
+145 133 0
+145 7 0
+-133 -7 -145 0
+-140 -132 -114 0
+-140 132 114 0
+140 -132 114 0
+140 132 -114 0
+146 133 0
+146 11 0
+-133 -11 -146 0
+-141 -132 -116 0
+-141 132 116 0
+141 -132 116 0
+141 132 -116 0
+147 133 0
+147 15 0
+-133 -15 -147 0
+-142 -132 -118 0
+-142 132 118 0
+142 -132 118 0
+142 132 -118 0
+148 133 0
+148 19 0
+-133 -19 -148 0
+-143 -132 -120 0
+-143 132 120 0
+143 -132 120 0
+143 132 -120 0
+149 133 0
+149 23 0
+-133 -23 -149 0
+150 133 0
+150 27 0
+-133 -27 -150 0
+151 133 0
+151 31 0
+-133 -31 -151 0
+152 133 0
+152 35 0
+-133 -35 -152 0
+153 135 0
+153 122 0
+-135 -122 -153 0
+154 136 0
+154 123 0
+-136 -123 -154 0
+155 137 0
+155 124 0
+-137 -124 -155 0
+156 138 0
+156 125 0
+-138 -125 -156 0
+157 139 0
+157 126 0
+-139 -126 -157 0
+158 140 0
+158 127 0
+-140 -127 -158 0
+159 141 0
+159 128 0
+-141 -128 -159 0
+160 142 0
+160 129 0
+-142 -129 -160 0
+161 143 0
+161 131 0
+-143 -131 -161 0
+-162 153 0
+-162 154 0
+-162 155 0
+-162 156 0
+-162 157 0
+-162 158 0
+-162 159 0
+-162 160 0
+-162 161 0
+-153 -154 -155 -156 -157 -158 -159 -160 -161 162 0
+-163 -162 0
+163 162 0
+-164 -162 0
+164 162 0
+165 5 0
+165 163 0
+-5 -163 -165 0
+166 163 0
+166 9 0
+-163 -9 -166 0
+167 163 0
+167 13 0
+-163 -13 -167 0
+168 163 0
+168 17 0
+-163 -17 -168 0
+169 163 0
+169 21 0
+-163 -21 -169 0
+170 163 0
+170 25 0
+-163 -25 -170 0
+171 163 0
+171 29 0
+-163 -29 -171 0
+172 163 0
+172 33 0
+-163 -33 -172 0
+173 163 0
+173 36 0
+-163 -36 -173 0
+174 2 0
+174 95 0
+174 144 0
+174 165 0
+-2 -95 -144 -165 -174 0
+175 96 0
+175 145 0
+175 166 0
+175 6 0
+-96 -145 -166 -6 -175 0
+176 97 0
+176 146 0
+176 167 0
+176 10 0
+-97 -146 -167 -10 -176 0
+177 98 0
+177 147 0
+177 168 0
+177 14 0
+-98 -147 -168 -14 -177 0
+178 99 0
+178 148 0
+178 169 0
+178 18 0
+-99 -148 -169 -18 -178 0
+179 100 0
+179 149 0
+179 170 0
+179 22 0
+-100 -149 -170 -22 -179 0
+180 101 0
+180 150 0
+180 171 0
+180 26 0
+-101 -150 -171 -26 -180 0
+181 102 0
+181 151 0
+181 172 0
+181 30 0
+-102 -151 -172 -30 -181 0
+182 103 0
+182 152 0
+182 173 0
+182 34 0
+-103 -152 -173 -34 -182 0
+-183 -174 0
+183 174 0
+-188 175 0
+-188 176 0
+-188 177 0
+-188 178 0
+-188 179 0
+-188 180 0
+-188 181 0
+-188 182 0
+-175 -176 -177 -178 -179 -180 -181 -182 188 0
+-184 -177 0
+184 177 0
+-185 -179 0
+185 179 0
+-186 -180 0
+186 180 0
+-187 -181 0
+187 181 0
+183 188 193 0
+-193 -183 0
+-193 -188 0
+189 176 0
+189 184 0
+-176 -184 -189 0
+190 176 0
+190 177 0
+190 185 0
+190 178 0
+-176 -177 -185 -178 -190 0
+191 178 0
+191 177 0
+191 186 0
+-178 -177 -186 -191 0
+192 176 0
+192 177 0
+192 180 0
+192 187 0
+-176 -177 -180 -187 -192 0
+194 175 0
+194 176 0
+194 189 0
+194 178 0
+-175 -176 -189 -178 -194 0
+195 175 0
+195 176 0
+195 190 0
+195 191 0
+-175 -176 -190 -191 -195 0
+196 175 0
+196 189 0
+196 190 0
+196 192 0
+-175 -189 -190 -192 -196 0