修改项目结构，更新makefile
This commit is contained in:
parent
c3efc6aafb
commit
f02012ea75
2
.gitignore
vendored
2
.gitignore
vendored
@ -1,3 +1,3 @@
|
||||
*.o
|
||||
*.d*
|
||||
output.txt
|
||||
build
|
||||
2
.vscode/launch.json
vendored
2
.vscode/launch.json
vendored
@ -9,7 +9,7 @@
|
||||
"type": "cppdbg",
|
||||
"request": "launch",
|
||||
"program": "${workspaceFolder}/atpg",
|
||||
"args": ["c432.bench"],
|
||||
"args": ["${workspaceFolder}/benchmark/c432.bench"],
|
||||
"stopAtEntry": false,
|
||||
"cwd": "${fileDirname}",
|
||||
"environment": [],
|
||||
|
||||
5
.vscode/settings.json
vendored
5
.vscode/settings.json
vendored
@ -24,6 +24,9 @@
|
||||
"string_view": "cpp",
|
||||
"tuple": "cpp",
|
||||
"type_traits": "cpp",
|
||||
"typeinfo": "cpp"
|
||||
"typeinfo": "cpp",
|
||||
"sstream": "cpp",
|
||||
"ostream": "cpp",
|
||||
"iostream": "cpp"
|
||||
}
|
||||
}
|
||||
515
.vscode/test.cnf
vendored
Normal file
515
.vscode/test.cnf
vendored
Normal file
@ -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
|
||||
BIN
CCAnr/CCAnr
Executable file
BIN
CCAnr/CCAnr
Executable file
Binary file not shown.
BIN
CCAnr/CCAnr+cnc
BIN
CCAnr/CCAnr+cnc
Binary file not shown.
@ -1,3 +1,2 @@
|
||||
all: basis.hpp basis.cpp cnc.hpp cnc.cpp indusLS.hpp indusLS.cpp main.cpp
|
||||
g++ -s -O3 -DNDEBUG -static *.cpp -o CCAnr+cnc
|
||||
|
||||
CCAnr: cca.cpp cca.h basis.h cw.h preprocessor.h
|
||||
g++ cca.cpp -O3 -static -o CCAnr
|
||||
|
||||
269
CCAnr/basis.cpp
269
CCAnr/basis.cpp
@ -1,269 +0,0 @@
|
||||
#include "basis.hpp"
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <cstdlib>
|
||||
#include <cmath>
|
||||
#include <sys/times.h> //these two h files are for linux
|
||||
#include <unistd.h>
|
||||
#include "cnc.hpp" // cnc_unit_last
|
||||
|
||||
using namespace std;
|
||||
|
||||
|
||||
int cutoff_time;
|
||||
|
||||
bool shouldPrint = false;
|
||||
|
||||
/*parameters of the instance*/
|
||||
int num_vars;
|
||||
int num_clauses;
|
||||
|
||||
/* literal arrays */
|
||||
lit* var_lit[MAX_VARS];
|
||||
int var_lit_count[MAX_VARS];
|
||||
lit* clause_lit[MAX_CLAUSES];
|
||||
int clause_lit_count[MAX_CLAUSES];
|
||||
|
||||
lit clause_xor_org[MAX_CLAUSES];
|
||||
|
||||
int score1[MAX_VARS];
|
||||
int score0[MAX_VARS];
|
||||
|
||||
int tries;
|
||||
struct _the_best_s the_best;
|
||||
|
||||
static struct tms start;
|
||||
double get_runtime(void) {
|
||||
struct tms stop;
|
||||
times(&stop);
|
||||
return (double) (stop.tms_utime - start.tms_utime +stop.tms_stime - start.tms_stime) / sysconf(_SC_CLK_TCK);
|
||||
}
|
||||
void record_runtime(void) {
|
||||
times(&start);
|
||||
}
|
||||
|
||||
|
||||
|
||||
/*
|
||||
* Read in the problem.
|
||||
*/
|
||||
int build_instance(const char *filename)
|
||||
{
|
||||
char *line = new char[1000000];
|
||||
int *temp_lit = new int[MAX_VARS];
|
||||
char tempstr1[10];
|
||||
char tempstr2[10];
|
||||
|
||||
|
||||
int cur_lit;
|
||||
int i;
|
||||
int v,c;//var, clause
|
||||
|
||||
ifstream infile(filename);
|
||||
if(!infile)
|
||||
return 0;
|
||||
|
||||
|
||||
/*** build problem data structures of the instance ***/
|
||||
infile.getline(line,1000000);
|
||||
while (line[0] != 'p')
|
||||
infile.getline(line,1000000);
|
||||
|
||||
|
||||
sscanf(line, "%s %s %d %d", tempstr1, tempstr2, &num_vars, &num_clauses);
|
||||
|
||||
//cout << num_vars << '\t' << num_clauses << "\n";
|
||||
|
||||
if(num_vars>=MAX_VARS || num_clauses>=MAX_CLAUSES)
|
||||
{
|
||||
//cout<<"c the size of instance exceeds out limitation, please enlarge MAX_VARS and (or) MAX_CLAUSES."<<endl;
|
||||
exit(1);
|
||||
}
|
||||
|
||||
for (c = 0; c < num_clauses; c++)
|
||||
{
|
||||
clause_lit_count[c] = 0;
|
||||
clause_lit[c]=NULL;
|
||||
}
|
||||
|
||||
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
{
|
||||
var_lit_count[v] = 0;
|
||||
var_lit[v]=NULL;
|
||||
}
|
||||
|
||||
|
||||
//Now, read the clauses, one at a time.
|
||||
int lit_redundent, clause_redundent;
|
||||
int redundent_clause_count = 0;
|
||||
for (c = 0; c < num_clauses; )
|
||||
{
|
||||
clause_redundent = 0;
|
||||
clause_lit_count[c] = 0;
|
||||
|
||||
infile>>cur_lit;
|
||||
while (cur_lit != 0) {
|
||||
lit_redundent = 0;
|
||||
for(int p = 0; p < clause_lit_count[c]; p++)
|
||||
{
|
||||
if(cur_lit == temp_lit[p]){
|
||||
//cout << "c " << filename << ": WARNING! literal " << cur_lit << " redundent in clause " << c + redundent_clause_count << endl;
|
||||
lit_redundent = 1;
|
||||
break;
|
||||
}
|
||||
else if(cur_lit == -temp_lit[p]){
|
||||
//cout << "c " << filename << ": WARNING! conflict variable " << abs(cur_lit) << " detected in the clause " << c + redundent_clause_count << endl;
|
||||
clause_redundent = 1;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if(lit_redundent == 0)
|
||||
{
|
||||
temp_lit[clause_lit_count[c]] = cur_lit;
|
||||
clause_lit_count[c]++;
|
||||
}
|
||||
|
||||
infile>>cur_lit;
|
||||
}
|
||||
|
||||
if(clause_redundent == 0)
|
||||
{
|
||||
clause_lit[c] = new lit[clause_lit_count[c]+1];
|
||||
|
||||
clause_xor_org[c].reset();
|
||||
for(i=0; i<clause_lit_count[c]; ++i)
|
||||
{
|
||||
|
||||
clause_lit[c][i].clause_num = c;
|
||||
clause_lit[c][i].var_num = abs(temp_lit[i]);
|
||||
if (temp_lit[i] > 0) clause_lit[c][i].sense = 1;
|
||||
else clause_lit[c][i].sense = 0;
|
||||
|
||||
clause_xor_org[c] ^= clause_lit[c][i];
|
||||
|
||||
var_lit_count[clause_lit[c][i].var_num]++;
|
||||
}
|
||||
clause_lit[c][i].var_num=0;
|
||||
clause_lit[c][i].clause_num = -1;
|
||||
|
||||
c++;
|
||||
}
|
||||
else
|
||||
{
|
||||
num_clauses--;
|
||||
clause_lit_count[c] = 0;
|
||||
redundent_clause_count++;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
//creat var literal arrays
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
{
|
||||
var_lit[v] = new lit[var_lit_count[v] + 1];
|
||||
var_lit_count[v] = 0; //reset to 0, for build up the array
|
||||
}
|
||||
|
||||
|
||||
//scan all clauses to build up var literal arrays
|
||||
for (c = 0; c < num_clauses; ++c)
|
||||
{
|
||||
for(i=0; i<clause_lit_count[c]; ++i)
|
||||
{
|
||||
v = clause_lit[c][i].var_num;
|
||||
var_lit[v][var_lit_count[v]] = clause_lit[c][i];
|
||||
++var_lit_count[v];
|
||||
|
||||
if(clause_lit[c][i].sense==1) score1[v]++;
|
||||
else score0[v]++;
|
||||
}
|
||||
}
|
||||
|
||||
for (v=1; v<=num_vars; ++v) //set boundary
|
||||
var_lit[v][var_lit_count[v]].clause_num=-1;
|
||||
|
||||
the_best.soln = new int[num_vars + 1];
|
||||
the_best.opt_unsat = num_clauses;
|
||||
the_best.opt_time = -1;
|
||||
the_best.opt_try = 0;
|
||||
the_best.source = 0;
|
||||
|
||||
|
||||
delete [] temp_lit;
|
||||
delete [] line;
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
void update_best_soln(const int opt, const int *soln, const int source) {
|
||||
for(int v = 1; v <= num_vars; v++)
|
||||
the_best.soln[v] = soln[v];
|
||||
|
||||
//if (!shouldPrint)
|
||||
// cout << "o " << opt << endl;
|
||||
|
||||
the_best.opt_unsat = opt;
|
||||
the_best.opt_time = get_runtime();
|
||||
the_best.opt_try = tries;
|
||||
the_best.source = source;
|
||||
|
||||
//cout << "c optInfo\t" << opt << "\t" << the_best.opt_time << "\t" << tries << "\t" << source << endl;
|
||||
}
|
||||
|
||||
|
||||
void update_best_value(const int opt) {
|
||||
|
||||
//if (!shouldPrint)
|
||||
// cout << "o " << opt << endl;
|
||||
|
||||
the_best.opt_unsat = opt;
|
||||
|
||||
}
|
||||
|
||||
|
||||
void print_best_solution(void) {
|
||||
//cout << "c SOLN_BEGIN\t" << get_runtime() << endl;;
|
||||
cout << "v";
|
||||
for (int i = 1; i <= num_vars; i++) {
|
||||
cout << " " << i * ((the_best.soln[i] << 1) - 1);
|
||||
}
|
||||
cout << endl;
|
||||
//cout << "c SOLN_END\t" << get_runtime() << endl;
|
||||
cout << flush;
|
||||
}
|
||||
|
||||
bool verify_sol(void) {
|
||||
int c, j;
|
||||
int flag;
|
||||
|
||||
|
||||
for (c = 0; c < num_clauses; ++c) {
|
||||
flag = 0;
|
||||
for(j = 0; j < clause_lit_count[c]; ++j) {
|
||||
if (the_best.soln[clause_lit[c][j].var_num] == clause_lit[c][j].sense) {
|
||||
flag = 1;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if(flag ==0){
|
||||
|
||||
cout<<"c Error: the assignment is not a solution."<<endl;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
|
||||
/*if (verify_unsat == the_best.opt_unsat) {
|
||||
return 1;
|
||||
} else {
|
||||
cout << "c ERROR: find opt=" << the_best.opt_unsat << ", but verified opt=" << verify_unsat << endl;
|
||||
cout << "o " << verify_unsat << endl;
|
||||
the_best.opt_unsat = verify_unsat;
|
||||
return 0;
|
||||
}*/
|
||||
}
|
||||
|
||||
378
CCAnr/basis.h
Normal file
378
CCAnr/basis.h
Normal file
@ -0,0 +1,378 @@
|
||||
#ifndef _BASIS_H_
|
||||
#define _BASIS_H_
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <cstdlib>
|
||||
#include <cmath>
|
||||
|
||||
using namespace std;
|
||||
|
||||
enum type{SAT3, SAT5, SAT7, strSAT} probtype;
|
||||
|
||||
/* limits on the size of the problem. */
|
||||
#define MAX_VARS 4000010
|
||||
#define MAX_CLAUSES 20000000
|
||||
|
||||
|
||||
// Define a data structure for a literal in the SAT problem.
|
||||
struct lit {
|
||||
int clause_num; //clause num, begin with 0
|
||||
int var_num; //variable num, begin with 1
|
||||
int sense; //is 1 for true literals, 0 for false literals.
|
||||
};
|
||||
|
||||
/*parameters of the instance*/
|
||||
int num_vars; //var index from 1 to num_vars
|
||||
int num_clauses; //clause index from 0 to num_clauses-1
|
||||
int max_clause_len;
|
||||
int min_clause_len;
|
||||
int formula_len=0;
|
||||
double avg_clause_len;
|
||||
double ratio;
|
||||
|
||||
/* literal arrays */
|
||||
lit* var_lit[MAX_VARS]; //var_lit[i][j] means the j'th literal of var i.
|
||||
int var_lit_count[MAX_VARS]; //amount of literals of each var
|
||||
lit* clause_lit[MAX_CLAUSES]; //clause_lit[i][j] means the j'th literal of clause i.
|
||||
int clause_lit_count[MAX_CLAUSES]; // amount of literals in each clause
|
||||
|
||||
lit* org_clause_lit[MAX_CLAUSES]; //clause_lit[i][j] means the j'th literal of clause i.
|
||||
int org_clause_lit_count[MAX_CLAUSES]; // amount of literals in each clause
|
||||
int simplify=0;
|
||||
|
||||
/* Information about the variables. */
|
||||
int score[MAX_VARS];
|
||||
int time_stamp[MAX_VARS];
|
||||
int conf_change[MAX_VARS];
|
||||
int* var_neighbor[MAX_VARS];
|
||||
int var_neighbor_count[MAX_VARS];
|
||||
//int pscore[MAX_VARS];
|
||||
int fix[MAX_VARS];
|
||||
|
||||
|
||||
/* Information about the clauses */
|
||||
int clause_weight[MAX_CLAUSES];
|
||||
int sat_count[MAX_CLAUSES];
|
||||
int sat_var[MAX_CLAUSES];
|
||||
//int sat_var2[MAX_CLAUSES];
|
||||
|
||||
//unsat clauses stack
|
||||
int unsat_stack[MAX_CLAUSES]; //store the unsat clause number
|
||||
int unsat_stack_fill_pointer;
|
||||
int index_in_unsat_stack[MAX_CLAUSES];//which position is a clause in the unsat_stack
|
||||
|
||||
int this_try_best_unsat_stack_fill_pointer;
|
||||
|
||||
//variables in unsat clauses
|
||||
int unsatvar_stack[MAX_VARS];
|
||||
int unsatvar_stack_fill_pointer;
|
||||
int index_in_unsatvar_stack[MAX_VARS];
|
||||
int unsat_app_count[MAX_VARS]; //a varible appears in how many unsat clauses
|
||||
|
||||
//configuration changed decreasing variables (score>0 and confchange=1)
|
||||
int goodvar_stack[MAX_VARS];
|
||||
int goodvar_stack_fill_pointer;
|
||||
int already_in_goodvar_stack[MAX_VARS];
|
||||
|
||||
//unit clauses preprocess
|
||||
lit unitclause_queue[MAX_VARS];
|
||||
int unitclause_queue_beg_pointer=0;
|
||||
int unitclause_queue_end_pointer=0;
|
||||
int clause_delete[MAX_CLAUSES];
|
||||
|
||||
/* Information about solution */
|
||||
int cur_soln[MAX_VARS]; //the current solution, with 1's for True variables, and 0's for False variables
|
||||
|
||||
//cutoff
|
||||
int max_tries = 10000;
|
||||
int tries;
|
||||
int max_flips = 2000000000;
|
||||
int step;
|
||||
|
||||
void setup_datastructure();
|
||||
void free_memory();
|
||||
int build_instance(char *filename);
|
||||
void build_neighbor_relation();
|
||||
|
||||
void free_memory()
|
||||
{
|
||||
int i;
|
||||
for (i = 0; i < num_clauses; i++)
|
||||
{
|
||||
delete[] clause_lit[i];
|
||||
}
|
||||
|
||||
for(i=1; i<=num_vars; ++i)
|
||||
{
|
||||
delete[] var_lit[i];
|
||||
delete[] var_neighbor[i];
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* Read in the problem.
|
||||
*/
|
||||
int temp_lit[MAX_VARS]; //the max length of a clause can be MAX_VARS
|
||||
int build_instance(char *filename)
|
||||
{
|
||||
char line[1000000];
|
||||
char tempstr1[10];
|
||||
char tempstr2[10];
|
||||
int cur_lit;
|
||||
int i,j;
|
||||
int v,c;//var, clause
|
||||
|
||||
ifstream infile(filename);
|
||||
if(!infile.is_open())
|
||||
return 0;
|
||||
|
||||
/*** build problem data structures of the instance ***/
|
||||
infile.getline(line,1000000);
|
||||
while (line[0] != 'p')
|
||||
infile.getline(line,1000000);
|
||||
|
||||
sscanf(line, "%s %s %d %d", tempstr1, tempstr2, &num_vars, &num_clauses);
|
||||
ratio = double(num_clauses)/num_vars;
|
||||
|
||||
if(num_vars>=MAX_VARS || num_clauses>=MAX_CLAUSES)
|
||||
{
|
||||
cout<<"the size of instance exceeds out limitation, please enlarge MAX_VARS and (or) MAX_CLAUSES."<<endl;
|
||||
exit(-1);
|
||||
}
|
||||
|
||||
for (c = 0; c < num_clauses; c++)
|
||||
{
|
||||
clause_lit_count[c] = 0;
|
||||
clause_delete[c] = 0;
|
||||
}
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
{
|
||||
var_lit_count[v] = 0;
|
||||
fix[v] = 0;
|
||||
}
|
||||
|
||||
max_clause_len = 0;
|
||||
min_clause_len = num_vars;
|
||||
|
||||
//Now, read the clauses, one at a time.
|
||||
for (c = 0; c < num_clauses; c++)
|
||||
{
|
||||
infile>>cur_lit;
|
||||
|
||||
while (cur_lit != 0) {
|
||||
temp_lit[clause_lit_count[c]] = cur_lit;
|
||||
clause_lit_count[c]++;
|
||||
|
||||
infile>>cur_lit;
|
||||
}
|
||||
|
||||
clause_lit[c] = new lit[clause_lit_count[c]+1];
|
||||
|
||||
for(i=0; i<clause_lit_count[c]; ++i)
|
||||
{
|
||||
clause_lit[c][i].clause_num = c;
|
||||
clause_lit[c][i].var_num = abs(temp_lit[i]);
|
||||
if (temp_lit[i] > 0) clause_lit[c][i].sense = 1;
|
||||
else clause_lit[c][i].sense = 0;
|
||||
|
||||
var_lit_count[clause_lit[c][i].var_num]++;
|
||||
}
|
||||
clause_lit[c][i].var_num=0;
|
||||
clause_lit[c][i].clause_num = -1;
|
||||
|
||||
//unit clause
|
||||
if(clause_lit_count[c]==1)
|
||||
{
|
||||
unitclause_queue[unitclause_queue_end_pointer++] = clause_lit[c][0];
|
||||
clause_delete[c]=1;
|
||||
}
|
||||
|
||||
if(clause_lit_count[c] > max_clause_len)
|
||||
max_clause_len = clause_lit_count[c];
|
||||
else if(clause_lit_count[c] < min_clause_len)
|
||||
min_clause_len = clause_lit_count[c];
|
||||
|
||||
formula_len += clause_lit_count[c];
|
||||
}
|
||||
infile.close();
|
||||
|
||||
avg_clause_len = (double)formula_len/num_clauses;
|
||||
|
||||
if(unitclause_queue_end_pointer>0)
|
||||
{
|
||||
simplify = 1;
|
||||
for (c = 0; c < num_clauses; c++)
|
||||
{
|
||||
org_clause_lit_count[c] = clause_lit_count[c];
|
||||
org_clause_lit[c] = new lit[clause_lit_count[c]+1];
|
||||
for(i=0; i<org_clause_lit_count[c]; ++i)
|
||||
{
|
||||
org_clause_lit[c][i] = clause_lit[c][i];
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
//creat var literal arrays
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
{
|
||||
var_lit[v] = new lit[var_lit_count[v]+1];
|
||||
var_lit_count[v] = 0; //reset to 0, for build up the array
|
||||
}
|
||||
//scan all clauses to build up var literal arrays
|
||||
for (c = 0; c < num_clauses; ++c)
|
||||
{
|
||||
for(i=0; i<clause_lit_count[c]; ++i)
|
||||
{
|
||||
v = clause_lit[c][i].var_num;
|
||||
var_lit[v][var_lit_count[v]] = clause_lit[c][i];
|
||||
++var_lit_count[v];
|
||||
}
|
||||
}
|
||||
for (v=1; v<=num_vars; ++v) //set boundary
|
||||
var_lit[v][var_lit_count[v]].clause_num=-1;
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
||||
void build_neighbor_relation()
|
||||
{
|
||||
int* neighbor_flag = new int[num_vars+1];
|
||||
int i,j,count;
|
||||
int v,c;
|
||||
|
||||
for(v=1; v<=num_vars; ++v)
|
||||
{
|
||||
var_neighbor_count[v] = 0;
|
||||
|
||||
if(fix[v]==1) continue;
|
||||
|
||||
for(i=1; i<=num_vars; ++i)
|
||||
neighbor_flag[i] = 0;
|
||||
neighbor_flag[v] = 1;
|
||||
|
||||
for(i=0; i<var_lit_count[v]; ++i)
|
||||
{
|
||||
c = var_lit[v][i].clause_num;
|
||||
if(clause_delete[c]==1) continue;
|
||||
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
{
|
||||
if(neighbor_flag[clause_lit[c][j].var_num]==0)
|
||||
{
|
||||
var_neighbor_count[v]++;
|
||||
neighbor_flag[clause_lit[c][j].var_num] = 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
neighbor_flag[v] = 0;
|
||||
|
||||
var_neighbor[v] = new int[var_neighbor_count[v]+1];
|
||||
|
||||
count = 0;
|
||||
for(i=1; i<=num_vars; ++i)
|
||||
{
|
||||
if(fix[i]==1) continue;
|
||||
|
||||
if(neighbor_flag[i]==1)
|
||||
{
|
||||
var_neighbor[v][count] = i;
|
||||
count++;
|
||||
}
|
||||
}
|
||||
var_neighbor[v][count]=0;
|
||||
}
|
||||
|
||||
delete[] neighbor_flag; neighbor_flag=NULL;
|
||||
}
|
||||
|
||||
|
||||
void print_solution()
|
||||
{
|
||||
int i;
|
||||
|
||||
cout<<"v ";
|
||||
for (i=1; i<=num_vars; i++) {
|
||||
if(cur_soln[i]==0) cout<<"-";
|
||||
cout<<i;
|
||||
if(i%10==0) cout<<endl<<"v ";
|
||||
else cout<<' ';
|
||||
}
|
||||
cout<<"0"<<endl;
|
||||
}
|
||||
|
||||
|
||||
int verify_sol()
|
||||
{
|
||||
int c,j;
|
||||
int flag;
|
||||
|
||||
if(simplify==0)
|
||||
{
|
||||
|
||||
for (c = 0; c<num_clauses; ++c)
|
||||
{
|
||||
flag = 0;
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
if (cur_soln[clause_lit[c][j].var_num] == clause_lit[c][j].sense) {flag = 1; break;}
|
||||
|
||||
if(flag ==0){//output the clause unsatisfied by the solution
|
||||
cout<<"c clause "<<c<<" is not satisfied"<<endl;
|
||||
|
||||
cout<<"c ";
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
{
|
||||
if(clause_lit[c][j].sense==0)cout<<"-";
|
||||
cout<<clause_lit[c][j].var_num<<" ";
|
||||
}
|
||||
cout<<endl;
|
||||
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
cout<<cur_soln[clause_lit[c][j].var_num]<<" ";
|
||||
cout<<endl;
|
||||
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if(simplify==1)
|
||||
{
|
||||
for (c = 0; c<num_clauses; ++c)
|
||||
{
|
||||
flag = 0;
|
||||
for(j=0; j<org_clause_lit_count[c]; ++j)
|
||||
if (cur_soln[org_clause_lit[c][j].var_num] == org_clause_lit[c][j].sense) {flag = 1; break;}
|
||||
|
||||
if(flag ==0){//output the clause unsatisfied by the solution
|
||||
cout<<"c clause "<<c<<" is not satisfied"<<endl;
|
||||
|
||||
if(clause_delete[c]==1)cout<<"c this clause is deleted by UP."<<endl;
|
||||
|
||||
cout<<"c ";
|
||||
for(j=0; j<org_clause_lit_count[c]; ++j)
|
||||
{
|
||||
if(org_clause_lit[c][j].sense==0)cout<<"-";
|
||||
cout<<org_clause_lit[c][j].var_num<<" ";
|
||||
}
|
||||
cout<<endl;
|
||||
|
||||
for(j=0; j<org_clause_lit_count[c]; ++j)
|
||||
cout<<cur_soln[org_clause_lit[c][j].var_num]<<" ";
|
||||
cout<<endl;
|
||||
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
@ -1,76 +0,0 @@
|
||||
#ifndef _BASIS_H_
|
||||
#define _BASIS_H_
|
||||
|
||||
/* limits on the size of the problem. */
|
||||
#define MAX_VARS 5000010
|
||||
#define MAX_CLAUSES 20000000
|
||||
|
||||
extern bool shouldPrint;
|
||||
|
||||
// Define a data structure for a literal in the SAT problem.
|
||||
struct lit {
|
||||
unsigned char sense:1; //is 1 for true literals, 0 for false literals.
|
||||
int clause_num:31; //clause num, begin with 0
|
||||
int var_num; //variable num, begin with 1
|
||||
|
||||
struct lit& operator^=(const struct lit &l) {
|
||||
sense ^= l.sense;
|
||||
clause_num ^= l.clause_num;
|
||||
var_num ^= l.var_num;
|
||||
return *this;
|
||||
}
|
||||
|
||||
void reset(void) {
|
||||
sense = 0;
|
||||
clause_num = 0;
|
||||
var_num = 0;
|
||||
}
|
||||
|
||||
bool operator==(const struct lit &l) const {
|
||||
return sense == l.sense && clause_num == l.clause_num && var_num == l.var_num;
|
||||
}
|
||||
|
||||
bool operator!=(const struct lit &l) const {
|
||||
return !(*this == l);
|
||||
}
|
||||
};
|
||||
|
||||
/*parameters of the instance*/
|
||||
extern int num_vars; //var index from 1 to num_vars
|
||||
extern int num_clauses; //clause index from 0 to num_clauses-1
|
||||
|
||||
/* literal arrays */
|
||||
extern lit* var_lit[MAX_VARS]; //var_lit[i][j] means the j'th literal of var i.
|
||||
extern int var_lit_count[MAX_VARS]; //amount of literals of each var
|
||||
extern lit* clause_lit[MAX_CLAUSES]; //clause_lit[i][j] means the j'th literal of clause i.
|
||||
extern int clause_lit_count[MAX_CLAUSES]; // amount of literals in each clause
|
||||
|
||||
// Used by CNC, but since it is hard to update, just put it here...
|
||||
extern lit clause_xor_org[MAX_CLAUSES];
|
||||
|
||||
extern int score1[MAX_VARS];
|
||||
extern int score0[MAX_VARS];
|
||||
|
||||
extern int tries;
|
||||
extern int cutoff_time;
|
||||
|
||||
struct _the_best_s {
|
||||
int *soln;
|
||||
int opt_unsat;
|
||||
double opt_time;
|
||||
int opt_try;
|
||||
int source;
|
||||
};
|
||||
extern struct _the_best_s the_best;
|
||||
|
||||
int build_instance(const char *filename);
|
||||
void print_best_solution(void);
|
||||
void update_best_soln(const int opt, const int *soln, const int source);
|
||||
void update_best_value(const int opt);
|
||||
|
||||
bool verify_sol(void);
|
||||
|
||||
void record_runtime(void);
|
||||
double get_runtime(void);
|
||||
|
||||
#endif
|
||||
292
CCAnr/cca.cpp
Normal file
292
CCAnr/cca.cpp
Normal file
@ -0,0 +1,292 @@
|
||||
#include "basis.h"
|
||||
#include "cca.h"
|
||||
#include "cw.h"
|
||||
#include "preprocessor.h"
|
||||
|
||||
#include <string.h>
|
||||
#include <sys/times.h> //these two h files are for linux
|
||||
#include <unistd.h>
|
||||
|
||||
#include "ccanr.h"
|
||||
|
||||
char * inst;
|
||||
int seed;
|
||||
|
||||
long long ls_no_improv_times;
|
||||
|
||||
bool aspiration_active;
|
||||
|
||||
static int pick_var(void)
|
||||
{
|
||||
int i,k,c,v;
|
||||
int best_var;
|
||||
lit* clause_c;
|
||||
|
||||
/**Greedy Mode**/
|
||||
/*CCD (configuration changed decreasing) mode, the level with configuation chekcing*/
|
||||
if(goodvar_stack_fill_pointer>0)
|
||||
{
|
||||
|
||||
//if(goodvar_stack_fill_pointer<balancePar)
|
||||
//{
|
||||
best_var = goodvar_stack[0];
|
||||
for(i=1; i<goodvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
v=goodvar_stack[i];
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var])
|
||||
{
|
||||
//if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
|
||||
//else if(unsat_app_count[v]==unsat_app_count[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
|
||||
if(time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
}
|
||||
return best_var;
|
||||
//}
|
||||
/*else
|
||||
{
|
||||
best_var = goodvar_stack[rand()%goodvar_stack_fill_pointer];
|
||||
for(int j=1;j<balancePar;++j)
|
||||
{
|
||||
v = goodvar_stack[rand()%goodvar_stack_fill_pointer];
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var])
|
||||
{
|
||||
//if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
|
||||
//else if(unsat_app_count[v]==unsat_app_count[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
if(time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
}
|
||||
return best_var;
|
||||
}*/
|
||||
}
|
||||
|
||||
|
||||
/*aspiration*/
|
||||
if (aspiration_active)
|
||||
{
|
||||
best_var = 0;
|
||||
for(i=0; i<unsatvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
if(score[unsatvar_stack[i]]>ave_weight)
|
||||
{
|
||||
best_var = unsatvar_stack[i];
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
for(++i; i<unsatvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
v=unsatvar_stack[i];
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var] && time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
|
||||
if(best_var!=0) return best_var;
|
||||
}
|
||||
/*****end aspiration*******************/
|
||||
|
||||
update_clause_weights();
|
||||
|
||||
/*focused random walk*/
|
||||
|
||||
c = unsat_stack[rand()%unsat_stack_fill_pointer];
|
||||
clause_c = clause_lit[c];
|
||||
best_var = clause_c[0].var_num;
|
||||
for(k=1; k<clause_lit_count[c]; ++k)
|
||||
{
|
||||
v=clause_c[k].var_num;
|
||||
|
||||
//using score
|
||||
//if(score[v]>score[best_var]) best_var = v;
|
||||
//else if(score[v]==score[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
|
||||
//using unweighted make
|
||||
if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
|
||||
//else if(unsat_app_count[v]==unsat_app_count[best_var] && time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
else if(unsat_app_count[v]==unsat_app_count[best_var])
|
||||
{
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
}
|
||||
|
||||
return best_var;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
//set functions in the algorithm
|
||||
void settings()
|
||||
{
|
||||
//set_clause_weighting();
|
||||
|
||||
//aspiration_active = false; //
|
||||
}
|
||||
|
||||
/*
|
||||
void local_search(int max_flips)
|
||||
{
|
||||
int flipvar;
|
||||
|
||||
for (step = 0; step<max_flips; step++)
|
||||
{
|
||||
//find a solution
|
||||
if(unsat_stack_fill_pointer==0) return;
|
||||
|
||||
flipvar = pick_var();
|
||||
|
||||
flip(flipvar);
|
||||
|
||||
time_stamp[flipvar] = step;
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
void local_search(long long no_improv_times)
|
||||
{
|
||||
int flipvar;
|
||||
long long notime = 1 + no_improv_times;
|
||||
|
||||
// printf("cur_sol: ");
|
||||
// for(int i=1; i<=num_vars; i++) {
|
||||
// printf("%d ", cur_soln[i]);
|
||||
// }
|
||||
// printf("\n");
|
||||
|
||||
while(--notime)
|
||||
{
|
||||
flipvar = pick_var();
|
||||
flip(flipvar);
|
||||
time_stamp[flipvar] = step;
|
||||
|
||||
|
||||
step++;
|
||||
if(unsat_stack_fill_pointer < this_try_best_unsat_stack_fill_pointer)
|
||||
{
|
||||
this_try_best_unsat_stack_fill_pointer = unsat_stack_fill_pointer;
|
||||
notime = 1 + no_improv_times;
|
||||
}
|
||||
|
||||
if(unsat_stack_fill_pointer == 0)
|
||||
{
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
return;
|
||||
}
|
||||
|
||||
void default_settings()
|
||||
{
|
||||
seed = 1;
|
||||
ls_no_improv_times = 200000;
|
||||
p_scale = 0.3;
|
||||
q_scale = 0.7;
|
||||
threshold = 50;
|
||||
|
||||
aspiration_active = false; //
|
||||
}
|
||||
|
||||
int CCAnr::module_pick_var() {
|
||||
return pick_var();
|
||||
}
|
||||
void CCAnr::module_flip_var(int flipvar) {
|
||||
flip(flipvar);
|
||||
time_stamp[flipvar] = step;
|
||||
step++;
|
||||
if(unsat_stack_fill_pointer < this_try_best_unsat_stack_fill_pointer)
|
||||
{
|
||||
this_try_best_unsat_stack_fill_pointer = unsat_stack_fill_pointer;
|
||||
}
|
||||
|
||||
if(unsat_stack_fill_pointer == 0)
|
||||
{
|
||||
printf("[CCAnr] find solution!\n");
|
||||
|
||||
if(verify_sol()!=1) {
|
||||
cout<<"c Sorry, something is wrong."<<endl;
|
||||
exit(-1);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
int* CCAnr::module_cur_soln() {
|
||||
return cur_soln;
|
||||
}
|
||||
|
||||
void CCAnr::module_reset() {
|
||||
settings();
|
||||
init();
|
||||
}
|
||||
|
||||
void CCAnr::module_init()
|
||||
{
|
||||
int seed,i;
|
||||
int satisfy_flag=0;
|
||||
struct tms start, stop;
|
||||
|
||||
cout<<"c This is CCAnr 2.0 [Version: 2018.01.28] [Author: Shaowei Cai]."<<endl;
|
||||
|
||||
times(&start);
|
||||
|
||||
default_settings();
|
||||
|
||||
build_instance("test.cnf");
|
||||
|
||||
srand(seed);
|
||||
|
||||
//if(unitclause_queue_end_pointer > 0) preprocess();
|
||||
|
||||
build_neighbor_relation();
|
||||
|
||||
scale_ave=(threshold+1)*q_scale; //
|
||||
|
||||
cout<<"c Instance: Number of variables = "<<num_vars<<endl;
|
||||
cout<<"c Instance: Number of clauses = "<<num_clauses<<endl;
|
||||
cout<<"c Instance: Ratio = "<<ratio<<endl;
|
||||
cout<<"c Instance: Formula length = "<<formula_len<<endl;
|
||||
cout<<"c Instance: Avg (Min,Max) clause length = "<<avg_clause_len<<" ("<<min_clause_len<<","<<max_clause_len<<")"<<endl;
|
||||
cout<<"c Algorithmic: Random seed = "<<seed<<endl;
|
||||
cout<<"c Algorithmic: ls_no_improv_steps = " << ls_no_improv_times << endl;
|
||||
cout<<"c Algorithmic: swt_p = " << p_scale << endl;
|
||||
cout<<"c Algorithmic: swt_q = " << q_scale << endl;
|
||||
cout<<"c Algorithmic: swt_threshold = " << threshold << endl;
|
||||
cout<<"c Algorithmic: scale_ave = " << scale_ave << endl;
|
||||
if(aspiration_active) cout<<"c Algorithmic: aspiration_active = true" << endl;
|
||||
else cout<<"c Algorithmic: aspiration_active = false" << endl;
|
||||
|
||||
// for (tries = 0; tries <= max_tries; tries++)
|
||||
// {
|
||||
// settings();
|
||||
|
||||
// init();
|
||||
|
||||
// local_search(ls_no_improv_times);
|
||||
|
||||
// if (unsat_stack_fill_pointer==0)
|
||||
// {
|
||||
// if(verify_sol()==1) {satisfy_flag = 1; break;}
|
||||
// else cout<<"c Sorry, something is wrong."<<endl;/////
|
||||
// }
|
||||
// }
|
||||
|
||||
// times(&stop);
|
||||
// double comp_time = double(stop.tms_utime - start.tms_utime +stop.tms_stime - start.tms_stime) / sysconf(_SC_CLK_TCK);
|
||||
|
||||
// if(satisfy_flag==1)
|
||||
// {
|
||||
// cout<<"s SATISFIABLE"<<endl;
|
||||
// //print_solution();
|
||||
// }
|
||||
// else cout<<"s UNKNOWN"<<endl;
|
||||
|
||||
// cout<<"c solveSteps = "<<tries<<" tries + "<<step<<" steps (each try has "<<max_flips<<" steps)."<<endl;
|
||||
// cout<<"c solveTime = "<<comp_time<<endl;
|
||||
|
||||
// free_memory();
|
||||
|
||||
return;
|
||||
}
|
||||
295
CCAnr/cca.h
Normal file
295
CCAnr/cca.h
Normal file
@ -0,0 +1,295 @@
|
||||
/************************************=== CCAnr ===***************************************
|
||||
** CCAnr is a local search solver for the Boolean Satisfiability (SAT) problem,
|
||||
** which is especially designed for non-random instances.
|
||||
** CCAnr is designed and implemented by Shaowei Cai (email: shaoweicai.cs@gmail.com),
|
||||
*****************************************************************************************/
|
||||
|
||||
/*****************************=== Develpment history ===*************************************
|
||||
** 2011.5
|
||||
** SWCC (Smoothed Weighting and Configuration Checking) by Shaowei Cai
|
||||
** New Idea: Configuration Checking (CC)
|
||||
** A variable is configuration changed, if since its last flip, at least one of its
|
||||
** neighboring var has been flipped.
|
||||
** In the greedy mode, Swcc picks the best Configuration Changed Decreasing var to flip.
|
||||
** In the random mode, it updates weights, and flips the oldest var in a random unsat clause.
|
||||
|
||||
** 2011.9
|
||||
** SWCCA (Smoothed Weighting and Configuration Checking with Aspiration) by Shaowei Cai
|
||||
** New Idea: CC with Aspiration (CCA)
|
||||
** Modification: in greedy mode, it first prefers to flip the best CCD var. If there is
|
||||
** no CCD variable, then flip the best significant decreasing var, i.e., with a great
|
||||
** positive score (in Swcca, bigger than averaged clause weight), if there exsit such vars.
|
||||
|
||||
** 2013.4
|
||||
** CCAnr (CCA for non-random SAT)
|
||||
** Modifications: Generalize the smoothig fomula as w(ci)=w(ci)*p+ave_w*q; pick the greediest
|
||||
** variable in the diversification mode.
|
||||
************************************************************************************************/
|
||||
|
||||
|
||||
#ifndef _CCA_H_
|
||||
#define _CCA_H_
|
||||
|
||||
#include "basis.h"
|
||||
|
||||
#define pop(stack) stack[--stack ## _fill_pointer]
|
||||
#define push(item, stack) stack[stack ## _fill_pointer++] = item
|
||||
|
||||
inline void unsat(int clause)
|
||||
{
|
||||
index_in_unsat_stack[clause] = unsat_stack_fill_pointer;
|
||||
push(clause,unsat_stack);
|
||||
|
||||
//update appreance count of each var in unsat clause and update stack of vars in unsat clauses
|
||||
int v;
|
||||
for(lit* p=clause_lit[clause]; (v=p->var_num)!=0; p++)
|
||||
{
|
||||
unsat_app_count[v]++;
|
||||
if(unsat_app_count[v]==1)
|
||||
{
|
||||
index_in_unsatvar_stack[v] = unsatvar_stack_fill_pointer;
|
||||
push(v,unsatvar_stack);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
inline void sat(int clause)
|
||||
{
|
||||
int index,last_unsat_clause;
|
||||
|
||||
//since the clause is satisfied, its position can be reused to store the last_unsat_clause
|
||||
last_unsat_clause = pop(unsat_stack);
|
||||
index = index_in_unsat_stack[clause];
|
||||
unsat_stack[index] = last_unsat_clause;
|
||||
index_in_unsat_stack[last_unsat_clause] = index;
|
||||
|
||||
//update appreance count of each var in unsat clause and update stack of vars in unsat clauses
|
||||
int v,last_unsat_var;
|
||||
for(lit* p=clause_lit[clause]; (v=p->var_num)!=0; p++)
|
||||
{
|
||||
unsat_app_count[v]--;
|
||||
if(unsat_app_count[v]==0)
|
||||
{
|
||||
last_unsat_var = pop(unsatvar_stack);
|
||||
index = index_in_unsatvar_stack[v];
|
||||
unsatvar_stack[index] = last_unsat_var;
|
||||
index_in_unsatvar_stack[last_unsat_var] = index;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//initiation of the algorithm
|
||||
void init()
|
||||
{
|
||||
int v,c;
|
||||
int i,j;
|
||||
int clause;
|
||||
|
||||
//Initialize edge weights
|
||||
for (c = 0; c<num_clauses; c++)
|
||||
clause_weight[c] = 1;
|
||||
|
||||
//init unsat_stack
|
||||
unsat_stack_fill_pointer = 0;
|
||||
unsatvar_stack_fill_pointer = 0;
|
||||
|
||||
//init solution
|
||||
for (v = 1; v <= num_vars; v++) {
|
||||
|
||||
if(fix[v]==0){
|
||||
if(rand()%2==1) cur_soln[v] = 1;
|
||||
else cur_soln[v] = 0;
|
||||
|
||||
time_stamp[v] = 0;
|
||||
conf_change[v] = 1;
|
||||
unsat_app_count[v] = 0;
|
||||
|
||||
//pscore[v] = 0;
|
||||
}
|
||||
}
|
||||
|
||||
/* figure out sat_count, and init unsat_stack */
|
||||
for (c=0; c<num_clauses; ++c)
|
||||
{
|
||||
if(clause_delete[c]==1) continue;
|
||||
|
||||
sat_count[c] = 0;
|
||||
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
{
|
||||
if (cur_soln[clause_lit[c][j].var_num] == clause_lit[c][j].sense)
|
||||
{
|
||||
sat_count[c]++;
|
||||
sat_var[c] = clause_lit[c][j].var_num;
|
||||
}
|
||||
}
|
||||
|
||||
if (sat_count[c] == 0)
|
||||
unsat(c);
|
||||
}
|
||||
|
||||
/*figure out var score*/
|
||||
int lit_count;
|
||||
for (v=1; v<=num_vars; v++)
|
||||
{
|
||||
if(fix[v]==1)
|
||||
{
|
||||
score[v] = -100000;
|
||||
continue;
|
||||
}
|
||||
|
||||
score[v] = 0;
|
||||
|
||||
lit_count = var_lit_count[v];
|
||||
|
||||
for(i=0; i<lit_count; ++i)
|
||||
{
|
||||
c = var_lit[v][i].clause_num;
|
||||
if (sat_count[c]==0) score[v]++;
|
||||
else if (sat_count[c]==1 && var_lit[v][i].sense==cur_soln[v]) score[v]--;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
int flag;
|
||||
//compute pscore and record sat_var and sat_var2 for 2sat clauses
|
||||
for (c=0; c<num_clauses; ++c)
|
||||
{
|
||||
if(clause_delete[c]==1) continue;
|
||||
|
||||
if (sat_count[c]==1)
|
||||
{
|
||||
for(j=0;j<clause_lit_count[c];++j)
|
||||
{
|
||||
v=clause_lit[c][j].var_num;
|
||||
if(v!=sat_var[c])pscore[v]++;
|
||||
}
|
||||
}
|
||||
else if(sat_count[c]==2)
|
||||
{
|
||||
flag=0;
|
||||
for(j=0;j<clause_lit_count[c];++j)
|
||||
{
|
||||
v=clause_lit[c][j].var_num;
|
||||
if(clause_lit[c][j].sense == cur_soln[v])
|
||||
{
|
||||
pscore[v]--;
|
||||
if(flag==0){sat_var[c] = v; flag=1;}
|
||||
else {sat_var2[c] = v; break;}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
|
||||
//init goodvars stack
|
||||
goodvar_stack_fill_pointer = 0;
|
||||
for (v=1; v<=num_vars; v++)
|
||||
{
|
||||
if(fix[v]==1) continue;
|
||||
if(score[v]>0)// && conf_change[v]==1)
|
||||
{
|
||||
already_in_goodvar_stack[v] = 1;
|
||||
push(v,goodvar_stack);
|
||||
|
||||
}
|
||||
else already_in_goodvar_stack[v] = 0;
|
||||
}
|
||||
|
||||
//setting for the virtual var 0
|
||||
time_stamp[0]=0;
|
||||
//pscore[0]=0;
|
||||
|
||||
this_try_best_unsat_stack_fill_pointer = unsat_stack_fill_pointer;
|
||||
}
|
||||
|
||||
|
||||
void flip(int flipvar)
|
||||
{
|
||||
cur_soln[flipvar] = 1 - cur_soln[flipvar];
|
||||
|
||||
int i,j;
|
||||
int v,c;
|
||||
|
||||
lit* clause_c;
|
||||
|
||||
int org_flipvar_score = score[flipvar];
|
||||
|
||||
//update related clauses and neighbor vars
|
||||
for(lit *q = var_lit[flipvar]; (c=q->clause_num)>=0; q++)
|
||||
{
|
||||
clause_c = clause_lit[c];
|
||||
if(cur_soln[flipvar] == q->sense)
|
||||
{
|
||||
++sat_count[c];
|
||||
|
||||
if (sat_count[c] == 2) //sat_count from 1 to 2
|
||||
score[sat_var[c]] += clause_weight[c];
|
||||
else if (sat_count[c] == 1) // sat_count from 0 to 1
|
||||
{
|
||||
sat_var[c] = flipvar;//record the only true lit's var
|
||||
for(lit* p=clause_c; (v=p->var_num)!=0; p++) score[v] -= clause_weight[c];
|
||||
|
||||
sat(c);
|
||||
}
|
||||
}
|
||||
else // cur_soln[flipvar] != cur_lit.sense
|
||||
{
|
||||
--sat_count[c];
|
||||
if (sat_count[c] == 1) //sat_count from 2 to 1
|
||||
{
|
||||
for(lit* p=clause_c; (v=p->var_num)!=0; p++)
|
||||
{
|
||||
if(p->sense == cur_soln[v] )
|
||||
{
|
||||
score[v] -= clause_weight[c];
|
||||
sat_var[c] = v;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (sat_count[c] == 0) //sat_count from 1 to 0
|
||||
{
|
||||
for(lit* p=clause_c; (v=p->var_num)!=0; p++) score[v] += clause_weight[c];
|
||||
unsat(c);
|
||||
}//end else if
|
||||
|
||||
}//end else
|
||||
}
|
||||
|
||||
score[flipvar] = -org_flipvar_score;
|
||||
|
||||
/*update CCD */
|
||||
int index;
|
||||
|
||||
conf_change[flipvar] = 0;
|
||||
//remove the vars no longer goodvar in goodvar stack
|
||||
for(index=goodvar_stack_fill_pointer-1; index>=0; index--)
|
||||
{
|
||||
v = goodvar_stack[index];
|
||||
if(score[v]<=0)
|
||||
{
|
||||
goodvar_stack[index] = pop(goodvar_stack);
|
||||
already_in_goodvar_stack[v] = 0;
|
||||
}
|
||||
}
|
||||
|
||||
//update all flipvar's neighbor's conf_change to be 1, add goodvar
|
||||
int* p;
|
||||
for(p=var_neighbor[flipvar]; (v=*p)!=0; p++)
|
||||
{
|
||||
conf_change[v] = 1;
|
||||
|
||||
if(score[v]>0 && already_in_goodvar_stack[v] ==0)
|
||||
{
|
||||
push(v,goodvar_stack);
|
||||
already_in_goodvar_stack[v] = 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
9
CCAnr/ccanr.h
Normal file
9
CCAnr/ccanr.h
Normal file
@ -0,0 +1,9 @@
|
||||
namespace CCAnr {
|
||||
|
||||
void module_init();
|
||||
int module_pick_var();
|
||||
void module_flip_var(int var);
|
||||
void module_reset();
|
||||
|
||||
int* module_cur_soln();
|
||||
}
|
||||
594
CCAnr/cnc.cpp
594
CCAnr/cnc.cpp
@ -1,594 +0,0 @@
|
||||
#include "cnc.hpp"
|
||||
#include "basis.hpp"
|
||||
#include "indusLS.hpp"
|
||||
#include <assert.h>
|
||||
#include <algorithm>
|
||||
#include <cstdlib>
|
||||
#include <iostream>
|
||||
using std::rand;
|
||||
using std::swap;
|
||||
using std::cout;
|
||||
using std::endl;
|
||||
|
||||
static inline bool with_prob(double p) {
|
||||
return (rand() % 10000000) * 0.0000001 < p;
|
||||
}
|
||||
|
||||
static lit org_unitclause_queue[MAX_VARS];
|
||||
static int org_unitclause_count;
|
||||
|
||||
static lit unitclause_queue[MAX_VARS];
|
||||
static char sense_in_queue[MAX_VARS];
|
||||
static int unitclause_queue_beg_pointer, unitclause_queue_end_pointer;
|
||||
static char clause_delete[MAX_CLAUSES];
|
||||
static int cp_clause_lit_count[MAX_CLAUSES];
|
||||
static lit clause_xor[MAX_CLAUSES];
|
||||
static int fix_soln[MAX_VARS];
|
||||
|
||||
static int unassigned_var[MAX_VARS];
|
||||
static int index_in_unassigned_var[MAX_VARS];
|
||||
static int unassigned_count;
|
||||
|
||||
static int clause_delete_count;
|
||||
static int conflict;
|
||||
|
||||
static float prob;
|
||||
|
||||
static void (* unit_propagation) ();
|
||||
static bool (* choose_sense) (int);
|
||||
|
||||
double cnc_unit_last;
|
||||
|
||||
static long long cnc_slot_age; // reset on the beginning of the slot
|
||||
|
||||
static long long cnc_age;
|
||||
static long long vage[MAX_VARS], vage_pos[MAX_VARS], vage_cnt[MAX_VARS];
|
||||
static inline void vage_touch(int v, bool sense) {
|
||||
vage[v] = cnc_age * num_vars + unassigned_count;
|
||||
vage_pos[v] += sense;
|
||||
vage_cnt[v]++;
|
||||
}
|
||||
|
||||
|
||||
|
||||
struct _canbest_s {
|
||||
int opt_unsat;
|
||||
int *soln;
|
||||
};
|
||||
|
||||
static struct _canbest_s *canbest;
|
||||
static int canbest_cap;
|
||||
static int canbest_count = 0;
|
||||
static int canbest_max_opt;
|
||||
|
||||
static void canbest_make_space(void) {
|
||||
if (canbest_count < canbest_cap)
|
||||
return;
|
||||
|
||||
for (int i = canbest_count - 1; i >= 0; --i) {
|
||||
if (canbest[i].opt_unsat == canbest_max_opt) {
|
||||
swap(canbest[i], canbest[--canbest_count]);
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
assert(0);
|
||||
}
|
||||
|
||||
static void canbest_update_max_opt(void) {
|
||||
if (canbest_count < canbest_cap) {
|
||||
canbest_max_opt = num_clauses;
|
||||
} else {
|
||||
canbest_max_opt = 0;
|
||||
for (int i = 0; i < canbest_count; ++i)
|
||||
if (canbest_max_opt < canbest[i].opt_unsat)
|
||||
canbest_max_opt = canbest[i].opt_unsat;
|
||||
}
|
||||
}
|
||||
|
||||
void cnc_init(int cb_cap) {
|
||||
for (int c = 0; c < num_clauses; ++c)
|
||||
if (1 == clause_lit_count[c])
|
||||
org_unitclause_queue[org_unitclause_count++] = clause_lit[c][0];
|
||||
|
||||
canbest_cap = cb_cap;
|
||||
canbest = new _canbest_s[canbest_cap];
|
||||
for (int i = 0; i < canbest_cap; ++i)
|
||||
canbest[i].soln = new int[num_vars + 1];
|
||||
canbest_max_opt = num_clauses;
|
||||
}
|
||||
|
||||
static inline void remove_unassigned_var(int var)
|
||||
{
|
||||
int index, last_unassigned_var;
|
||||
|
||||
last_unassigned_var = unassigned_var[--unassigned_count];
|
||||
index = index_in_unassigned_var[var];
|
||||
unassigned_var[index] = last_unassigned_var;
|
||||
index_in_unassigned_var[last_unassigned_var]=index;
|
||||
}
|
||||
|
||||
static void assign(int var, bool sense)
|
||||
{
|
||||
assert(var > 0 && var <= num_vars);
|
||||
assert(1 == sense || 0 == sense);
|
||||
|
||||
int c;
|
||||
int i;
|
||||
lit cur;
|
||||
|
||||
vage_touch(var, sense);
|
||||
|
||||
fix_soln[var] = sense;
|
||||
|
||||
remove_unassigned_var(var);
|
||||
|
||||
for(i = 0; i<var_lit_count[var]; ++i)
|
||||
{
|
||||
cur = var_lit[var][i];
|
||||
c = cur.clause_num;
|
||||
|
||||
if(clause_delete[c]==1) continue;
|
||||
|
||||
if(cur.sense == sense)//then remove the clause from the formula (by marking it as deleted).
|
||||
{
|
||||
clause_delete[c]=1; clause_delete_count++;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (cp_clause_lit_count[c]==1)//then it becomes an empty clause
|
||||
{
|
||||
clause_delete[c]=1;
|
||||
clause_delete_count++;
|
||||
conflict++;
|
||||
cp_clause_lit_count[c]=0;
|
||||
}
|
||||
else
|
||||
{
|
||||
--cp_clause_lit_count[c];
|
||||
clause_xor[c] ^= cur;
|
||||
|
||||
if (cp_clause_lit_count[c]==1)//newly generated unit clause
|
||||
{
|
||||
lit tmplit = clause_xor[c];
|
||||
|
||||
/*
|
||||
{ // Check if clause_xor is point to the only unit literal
|
||||
bool found = false;
|
||||
for(int j=0; j<clause_lit_count[c]; ++j) {
|
||||
// if fix_soln[v]==-2, v must be in unit queue
|
||||
// we won't reach here if the unit clause is being assigning
|
||||
if(fix_soln[clause_lit[c][j].var_num] < 0) {
|
||||
if (found || clause_xor[c] != clause_lit[c][j]) {
|
||||
cout << "error: xor value is invalid" << endl;
|
||||
abort();
|
||||
}
|
||||
found = true;
|
||||
}
|
||||
}
|
||||
if (!found) {
|
||||
cout << "error: xor value is point to unknown literal" << endl;
|
||||
abort();
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
int tmpvar=tmplit.var_num;
|
||||
|
||||
if (sense_in_queue[tmpvar] == -1)
|
||||
{
|
||||
unitclause_queue[unitclause_queue_end_pointer++] = tmplit;
|
||||
sense_in_queue[tmpvar] = tmplit.sense;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (sense_in_queue[tmpvar]!=tmplit.sense)
|
||||
{
|
||||
fix_soln[tmpvar]=-2;//mark this var as a conflicting var
|
||||
//clause_delete[c]=1; clause_delete_count++;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
void unit_propagation_order()
|
||||
{
|
||||
lit uc_lit;
|
||||
int uc_var;
|
||||
bool uc_sense;
|
||||
|
||||
//while (unitclause_queue_beg_pointer < unitclause_queue_end_pointer)
|
||||
//{
|
||||
|
||||
uc_lit = unitclause_queue[unitclause_queue_beg_pointer++];
|
||||
|
||||
uc_var = uc_lit.var_num;
|
||||
uc_sense = uc_lit.sense;
|
||||
|
||||
if(fix_soln[uc_var]==0 || fix_soln[uc_var]==1) return;
|
||||
|
||||
if (fix_soln[uc_var]==-2) {
|
||||
choose_sense(uc_var);
|
||||
}
|
||||
|
||||
assign(uc_var, uc_sense);
|
||||
//}
|
||||
}
|
||||
|
||||
void unit_propagation_random()
|
||||
{
|
||||
lit uc_lit;
|
||||
int uc_var;
|
||||
bool uc_sense;
|
||||
int index;
|
||||
|
||||
//while (unitclause_queue_beg_pointer < unitclause_queue_end_pointer)
|
||||
//{
|
||||
|
||||
if(unitclause_queue_end_pointer==unitclause_queue_beg_pointer+1)
|
||||
{
|
||||
uc_lit = unitclause_queue[--unitclause_queue_end_pointer];
|
||||
}
|
||||
else{
|
||||
//index = unitclause_queue_beg_pointer+rand()%(unitclause_queue_end_pointer-unitclause_queue_beg_pointer);
|
||||
index = rand()%unitclause_queue_end_pointer;
|
||||
uc_lit = unitclause_queue[index];
|
||||
unitclause_queue[index] = unitclause_queue[--unitclause_queue_end_pointer];
|
||||
}
|
||||
|
||||
//uc_lit = unitclause_queue[unitclause_queue_beg_pointer++];
|
||||
|
||||
uc_var = uc_lit.var_num;
|
||||
uc_sense = uc_lit.sense;
|
||||
|
||||
if(fix_soln[uc_var]==0 || fix_soln[uc_var]==1) return;
|
||||
|
||||
if (fix_soln[uc_var]==-2) {
|
||||
uc_sense = choose_sense(uc_var);
|
||||
}
|
||||
|
||||
assign(uc_var, uc_sense);
|
||||
//}
|
||||
}
|
||||
|
||||
|
||||
|
||||
void unit_propagation_vers_order()
|
||||
{
|
||||
lit uc_lit;
|
||||
int uc_var;
|
||||
bool uc_sense;
|
||||
|
||||
//while (unitclause_queue_beg_pointer < unitclause_queue_end_pointer)
|
||||
//{
|
||||
|
||||
uc_lit = unitclause_queue[--unitclause_queue_end_pointer];
|
||||
|
||||
uc_var = uc_lit.var_num;
|
||||
uc_sense = uc_lit.sense;
|
||||
|
||||
if(fix_soln[uc_var]==0 || fix_soln[uc_var]==1) return;
|
||||
|
||||
if (fix_soln[uc_var]==-2) {
|
||||
choose_sense(uc_var);
|
||||
}
|
||||
|
||||
assign(uc_var, uc_sense);
|
||||
//}
|
||||
}
|
||||
|
||||
bool choose_greedy_sense0(int var)
|
||||
{
|
||||
|
||||
if(score1[var]>score0[var]) return 1;
|
||||
else if(score0[var]>score1[var]) return 0;
|
||||
else return rand()%2;
|
||||
}
|
||||
|
||||
//greedy
|
||||
bool choose_greedy_sense(int var)
|
||||
{
|
||||
int i,c;
|
||||
lit cur;
|
||||
|
||||
int count1=0, count0=0;
|
||||
|
||||
for(i = 0; i<var_lit_count[var]; ++i)
|
||||
{
|
||||
cur = var_lit[var][i];
|
||||
c = cur.clause_num;
|
||||
|
||||
if(clause_delete[c]==1) continue;
|
||||
|
||||
if(cur.sense == 1)
|
||||
count1++;
|
||||
else
|
||||
count0++;
|
||||
}
|
||||
|
||||
if(count1>count0) return 1;
|
||||
else if(count1<count0) return 0;
|
||||
else return rand()%2;
|
||||
}
|
||||
|
||||
//weighted greedy
|
||||
bool choose_greedy_sense2(int var)
|
||||
{
|
||||
int i,c;
|
||||
lit cur;
|
||||
|
||||
int count1=0, count0=0;
|
||||
int large_number=100;
|
||||
|
||||
for(i = 0; i<var_lit_count[var]; ++i)
|
||||
{
|
||||
cur = var_lit[var][i];
|
||||
c = cur.clause_num;
|
||||
|
||||
if(clause_delete[c]==1) continue;
|
||||
|
||||
if(cur.sense == 1)
|
||||
count1 += large_number/cp_clause_lit_count[c];
|
||||
//count1++;
|
||||
else
|
||||
count0 += large_number/cp_clause_lit_count[c];
|
||||
//count0++;
|
||||
}
|
||||
|
||||
if(count1>count0) return 1;
|
||||
else if(count1<count0) return 0;
|
||||
else return rand()%2;
|
||||
}
|
||||
|
||||
|
||||
//random
|
||||
bool choose_random_sense(int var)
|
||||
{
|
||||
(void) var;
|
||||
return rand()%2;
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool choose_sense_prob0(int var)
|
||||
{
|
||||
if (with_prob(prob))
|
||||
return choose_random_sense(var);
|
||||
else return choose_greedy_sense0(var);
|
||||
|
||||
}
|
||||
|
||||
bool choose_sense_prob(int var)
|
||||
{
|
||||
if (with_prob(prob))
|
||||
return choose_random_sense(var);
|
||||
else return choose_greedy_sense(var);
|
||||
|
||||
}
|
||||
|
||||
|
||||
bool choose_sense_prob2(int var)
|
||||
{
|
||||
if (with_prob(prob))
|
||||
return choose_random_sense(var);
|
||||
else return choose_greedy_sense2(var);
|
||||
|
||||
}
|
||||
|
||||
int vage_window;
|
||||
void unit_propagation_age()
|
||||
{
|
||||
lit uc_lit;
|
||||
int uc_var;
|
||||
bool uc_sense;
|
||||
|
||||
// don't go through all var in queue, its too slow.
|
||||
const int unitlen = unitclause_queue_end_pointer - unitclause_queue_beg_pointer;
|
||||
int besti = (rand() % unitlen) + unitclause_queue_beg_pointer;
|
||||
for (int j = 0; j < vage_window; j++) {
|
||||
int i = (rand() % unitlen) + unitclause_queue_beg_pointer;
|
||||
if (vage[unitclause_queue[i].var_num] < vage[unitclause_queue[besti].var_num]) {
|
||||
besti = i;
|
||||
}
|
||||
}
|
||||
|
||||
uc_lit = unitclause_queue[besti];
|
||||
uc_var = uc_lit.var_num;
|
||||
uc_sense = uc_lit.sense;
|
||||
|
||||
unitclause_queue[besti] = unitclause_queue[--unitclause_queue_end_pointer];
|
||||
|
||||
if(fix_soln[uc_var]==0 || fix_soln[uc_var]==1) return;
|
||||
|
||||
if (fix_soln[uc_var]==-2) {
|
||||
uc_sense = choose_sense(uc_var);
|
||||
}
|
||||
|
||||
assign(uc_var, uc_sense);
|
||||
}
|
||||
|
||||
double lb_last_prob;
|
||||
static bool choose_sense_lb(int var) {
|
||||
if (with_prob(lb_last_prob))
|
||||
return lb_get_last(var);
|
||||
else
|
||||
return lb_get_prob(var);
|
||||
}
|
||||
|
||||
static void set_functions(void)
|
||||
{
|
||||
// int rand_res = rand() % 3;
|
||||
// if (0 == rand_res) unit_propagation = unit_propagation_order; //ord
|
||||
// else if (1 == rand_res) unit_propagation = unit_propagation_vers_order;//ver
|
||||
// else unit_propagation = unit_propagation_random;//random
|
||||
|
||||
// Rand can take 1% lower wrong ratio than others
|
||||
//unit_propagation = unit_propagation_order;
|
||||
//unit_propagation = unit_propagation_vers_order;
|
||||
//unit_propagation = unit_propagation_random;
|
||||
unit_propagation = unit_propagation_age;
|
||||
|
||||
|
||||
//choose_sense = choose_greedy_sense;
|
||||
//choose_sense = choose_greedy_sense2;
|
||||
//choose_sense = choose_random_sense;
|
||||
choose_sense = choose_sense_lb;
|
||||
|
||||
}
|
||||
|
||||
static void cnc_process_one(void)
|
||||
{
|
||||
int as_var;
|
||||
bool as_sense;
|
||||
|
||||
int c,v,i;
|
||||
|
||||
++cnc_slot_age;
|
||||
++cnc_age;
|
||||
set_functions();
|
||||
|
||||
for (i=0; i<num_vars; ++i)
|
||||
{
|
||||
v=i+1;
|
||||
unassigned_var[i]=v;
|
||||
index_in_unassigned_var[v]=i;
|
||||
|
||||
fix_soln[v]=-1;
|
||||
sense_in_queue[v]=-1;
|
||||
}
|
||||
unassigned_count = num_vars;
|
||||
|
||||
for (c = 0; c < num_clauses; c++)
|
||||
{
|
||||
cp_clause_lit_count[c] = clause_lit_count[c];
|
||||
clause_delete[c]=0;
|
||||
clause_xor[c] = clause_xor_org[c];
|
||||
}
|
||||
|
||||
clause_delete_count=0;
|
||||
conflict=0;
|
||||
|
||||
|
||||
unitclause_queue_beg_pointer=0;
|
||||
unitclause_queue_end_pointer=0;
|
||||
for(i = 0; i<org_unitclause_count; ++i)
|
||||
{
|
||||
lit tmplit = org_unitclause_queue[i];
|
||||
int tmpvar = tmplit.var_num;
|
||||
|
||||
if (sense_in_queue[tmpvar] == -1)
|
||||
{
|
||||
sense_in_queue[tmpvar] = tmplit.sense;
|
||||
unitclause_queue[unitclause_queue_end_pointer++] = tmplit;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (sense_in_queue[tmpvar]!=tmplit.sense)
|
||||
fix_soln[tmpvar]=-2;//mark this var as conflicting
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
if (tries > 1 && with_prob(cnc_unit_last)) {
|
||||
int var;
|
||||
for (int i = 0; i < unitclause_queue_end_pointer; ++i) {
|
||||
if (unitclause_queue[i].sense != lb_get_last(unitclause_queue[i].var_num)) {
|
||||
unitclause_queue[i].sense = 1 - unitclause_queue[i].sense;
|
||||
var = unitclause_queue[i].var_num;
|
||||
sense_in_queue[var] = unitclause_queue[i].sense;
|
||||
assert(unitclause_queue[i].sense == lb_get_last(unitclause_queue[i].var_num));
|
||||
}
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
|
||||
|
||||
while (unassigned_count>0)
|
||||
{
|
||||
if (clause_delete_count==num_clauses)
|
||||
{
|
||||
for (int i=0; i<unassigned_count; ++i)
|
||||
fix_soln[unassigned_var[i]]=rand()%2;
|
||||
|
||||
unassigned_count=0;
|
||||
|
||||
break;
|
||||
}
|
||||
|
||||
if (unitclause_queue_beg_pointer < unitclause_queue_end_pointer)
|
||||
{
|
||||
unit_propagation();
|
||||
}
|
||||
else {
|
||||
as_var = unassigned_var[rand()%unassigned_count];
|
||||
as_sense = choose_sense(as_var);
|
||||
assign(as_var, as_sense);
|
||||
}
|
||||
|
||||
if (conflict >= canbest_max_opt) break;
|
||||
}
|
||||
|
||||
if (conflict < canbest_max_opt) {
|
||||
if (the_best.opt_try != tries && conflict < the_best.opt_unsat) {
|
||||
// Best solution has been searched by LS, or init
|
||||
update_best_soln(conflict, fix_soln, 1);
|
||||
//cout << "c CNC_UPDATE_AT\t" << cnc_slot_age << "\t" << cnc_age << "\t" << tries << endl;
|
||||
} else if (the_best.opt_try == tries && conflict < the_best.opt_unsat) {
|
||||
// We have updated the best soln in this time slot
|
||||
// We found a better soln than the_best, and this the_best has not been searched by LS.
|
||||
// So move the_best to canbest, and update the_best by this new soln
|
||||
canbest_make_space();
|
||||
swap(the_best.soln, canbest[canbest_count].soln);
|
||||
canbest[canbest_count].opt_unsat = the_best.opt_unsat;
|
||||
canbest_count++;
|
||||
|
||||
update_best_soln(conflict, fix_soln, 1);
|
||||
//cout << "c CNC_UPDATE_AT\t" << cnc_slot_age << "\t" << cnc_age << "\t" << tries << endl;
|
||||
} else {
|
||||
canbest_make_space();
|
||||
canbest[canbest_count].opt_unsat = conflict;
|
||||
for (int v = 1; v <= num_vars; ++v)
|
||||
canbest[canbest_count].soln[v] = fix_soln[v];
|
||||
canbest_count++;
|
||||
}
|
||||
|
||||
canbest_update_max_opt();
|
||||
}
|
||||
}
|
||||
|
||||
bool cnc_get_canbest(const int* &soln, int &opt) {
|
||||
if (0 == canbest_count)
|
||||
return false;
|
||||
|
||||
opt = canbest[0].opt_unsat;
|
||||
int pos = 0;
|
||||
for (int i = 1; i < canbest_count; ++i) {
|
||||
if (opt > canbest[i].opt_unsat) {
|
||||
opt = canbest[i].opt_unsat;
|
||||
pos = i;
|
||||
}
|
||||
}
|
||||
soln = canbest[pos].soln;
|
||||
swap(canbest[pos], canbest[--canbest_count]);
|
||||
canbest_update_max_opt();
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
void cnc_process(long long step_num) {
|
||||
cnc_slot_age = 0;
|
||||
|
||||
++step_num;
|
||||
while (--step_num) {
|
||||
cnc_process_one();
|
||||
}
|
||||
}
|
||||
@ -1,13 +0,0 @@
|
||||
#ifndef _CNC_H_
|
||||
#define _CNC_H_
|
||||
|
||||
extern double cnc_unit_last;
|
||||
extern double lb_last_prob;
|
||||
extern double refer_gbest_prob;
|
||||
extern int vage_window;
|
||||
|
||||
void cnc_init(int cb_cap);
|
||||
void cnc_process(const long long step_num);
|
||||
bool cnc_get_canbest(const int* &soln, int &opt);
|
||||
|
||||
#endif
|
||||
103
CCAnr/cw.h
Normal file
103
CCAnr/cw.h
Normal file
@ -0,0 +1,103 @@
|
||||
#ifndef _CW_H_
|
||||
#define _CW_H_
|
||||
|
||||
#include "basis.h"
|
||||
|
||||
#define sigscore ave_weight //significant score needed for aspiration
|
||||
|
||||
int ave_weight=1;
|
||||
int delta_total_weight=0;
|
||||
|
||||
/**************************************** clause weighting for 3sat **************************************************/
|
||||
|
||||
int threshold;
|
||||
float p_scale;//w=w*p+ave_w*q
|
||||
float q_scale=0;
|
||||
int scale_ave;//scale_ave==ave_weight*q_scale
|
||||
|
||||
int q_init=0;
|
||||
|
||||
void smooth_clause_weights()
|
||||
{
|
||||
int i,j,c,v;
|
||||
int new_total_weight=0;
|
||||
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
score[v] = 0;
|
||||
|
||||
//smooth clause score and update score of variables
|
||||
for (c = 0; c<num_clauses; ++c)
|
||||
{
|
||||
clause_weight[c] = clause_weight[c]*p_scale+scale_ave;
|
||||
if(clause_weight[c]<1) clause_weight[c] = 1;
|
||||
|
||||
new_total_weight+=clause_weight[c];
|
||||
|
||||
//update score of variables in this clause
|
||||
if (sat_count[c]==0)
|
||||
{
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
{
|
||||
score[clause_lit[c][j].var_num] += clause_weight[c];
|
||||
}
|
||||
}
|
||||
else if(sat_count[c]==1)
|
||||
score[sat_var[c]]-=clause_weight[c];
|
||||
}
|
||||
|
||||
ave_weight=new_total_weight/num_clauses;
|
||||
}
|
||||
|
||||
void update_clause_weights()
|
||||
{
|
||||
int i,v;
|
||||
|
||||
for(i=0; i < unsat_stack_fill_pointer; ++i)
|
||||
clause_weight[unsat_stack[i]]++;
|
||||
|
||||
for(i=0; i<unsatvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
v = unsatvar_stack[i];
|
||||
score[v] += unsat_app_count[v];
|
||||
if(score[v]>0 && conf_change[v]==1 && already_in_goodvar_stack[v] ==0)
|
||||
{
|
||||
push(v,goodvar_stack);
|
||||
already_in_goodvar_stack[v] =1;
|
||||
}
|
||||
}
|
||||
|
||||
delta_total_weight+=unsat_stack_fill_pointer;
|
||||
if(delta_total_weight>=num_clauses)
|
||||
{
|
||||
ave_weight+=1;
|
||||
delta_total_weight -= num_clauses;
|
||||
|
||||
//smooth weights
|
||||
if(ave_weight>threshold)
|
||||
smooth_clause_weights();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void set_clause_weighting()
|
||||
{
|
||||
threshold=300;
|
||||
p_scale=0.3;
|
||||
if(q_init==0)
|
||||
{
|
||||
if(ratio<=15) q_scale=0;
|
||||
else q_scale=0.7;
|
||||
}
|
||||
else
|
||||
{
|
||||
if(q_scale<0.5) //0
|
||||
q_scale = 0.7;
|
||||
else
|
||||
q_scale = 0;
|
||||
}
|
||||
|
||||
scale_ave=(threshold+1)*q_scale;
|
||||
q_init = 1;
|
||||
}
|
||||
|
||||
#endif
|
||||
@ -1,676 +0,0 @@
|
||||
#include "basis.hpp"
|
||||
#include <cerrno>
|
||||
#include <cstdlib>
|
||||
#include <iostream>
|
||||
#include <assert.h>
|
||||
|
||||
using namespace std;
|
||||
|
||||
#define pop(stack) stack[--stack ## _fill_pointer]
|
||||
#define push(item, stack) stack[stack ## _fill_pointer++] = item
|
||||
|
||||
#define sigscore ave_weight //significant score needed for aspiration
|
||||
|
||||
/* Information about the variables. */
|
||||
static int score[MAX_VARS];
|
||||
static int conf_change[MAX_VARS];
|
||||
static long long time_stamp[MAX_VARS];
|
||||
|
||||
static int* var_neighbor[MAX_VARS];
|
||||
|
||||
/* Information about the clauses */
|
||||
static int clause_weight[MAX_CLAUSES];
|
||||
static int sat_count[MAX_CLAUSES];
|
||||
static int sat_var[MAX_CLAUSES];
|
||||
|
||||
//unsat clauses stack
|
||||
static int unsat_stack[MAX_CLAUSES]; //store the unsat clause number
|
||||
static int unsat_stack_fill_pointer; // NEED TO UPDATE IN RESTART PROCEDURE
|
||||
static int index_in_unsat_stack[MAX_CLAUSES];//which position is a clause in the unsat_stack
|
||||
|
||||
//variables in unsat clauses
|
||||
static int unsatvar_stack[MAX_VARS];
|
||||
static int unsatvar_stack_fill_pointer; // NEED TO UPDATE IN RESTART PROCEDURE
|
||||
static int index_in_unsatvar_stack[MAX_VARS];
|
||||
static int unsat_app_count[MAX_VARS]; //a varible appears in how many unsat clauses
|
||||
|
||||
//configuration changed decreasing variables (score>0 and confchange=1)
|
||||
static int goodvar_stack[MAX_VARS];
|
||||
static int goodvar_stack_fill_pointer; // NEED TO UPDATE IN RESTART PROCEDURE
|
||||
static int already_in_goodvar_stack[MAX_VARS];
|
||||
|
||||
/* Information about solution */
|
||||
static int cur_soln[MAX_VARS]; //the current solution, with 1's for True variables, and 0's for False variables
|
||||
|
||||
//cutoff
|
||||
static long long step; // LS私有step，每次init之后置为零
|
||||
|
||||
int balancePar;
|
||||
|
||||
bool aspiration_active;
|
||||
|
||||
|
||||
|
||||
|
||||
// local search local best
|
||||
// which is the best soln in this time slot
|
||||
static int lb_soln[MAX_VARS];
|
||||
static int lb_opt;
|
||||
static void lb_copy(void) {
|
||||
for (int v = 1; v <= num_vars; v++)
|
||||
lb_soln[v] = cur_soln[v];
|
||||
}
|
||||
static int lb_pos[MAX_VARS], lb_neg[MAX_VARS];
|
||||
static void lb_update(int mut) {
|
||||
for (int v = 1; v <= num_vars; v++) {
|
||||
assert(0 == lb_soln[v] || 1 == lb_soln[v]);
|
||||
lb_pos[v] += lb_soln[v] * mut;
|
||||
lb_neg[v] += !lb_soln[v] * mut;
|
||||
}
|
||||
}
|
||||
bool lb_get_prob(int v) {
|
||||
int sum = lb_pos[v] + lb_neg[v];
|
||||
if (0 == sum) {
|
||||
//return lb_soln[v];
|
||||
return rand() & 1;
|
||||
} else {
|
||||
return (rand() % sum) < lb_pos[v];
|
||||
}
|
||||
}
|
||||
bool lb_get_last(int v) {
|
||||
if (lb_neg[v] + lb_pos[v])
|
||||
return lb_soln[v];
|
||||
else
|
||||
return rand() & 1;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
void build_neighbor_relation(void)
|
||||
{
|
||||
int *neighbor_flag = new int[MAX_VARS];
|
||||
int *temp_neighbor = new int[MAX_VARS];
|
||||
|
||||
int temp_neighbor_count;
|
||||
int i,j,count;
|
||||
int v,c,n;
|
||||
|
||||
for(v=1; v<=num_vars; ++v)
|
||||
{
|
||||
//if(fix[v]==1) continue;
|
||||
|
||||
neighbor_flag[v] = 1;
|
||||
temp_neighbor_count = 0;
|
||||
|
||||
for(i=0; i<var_lit_count[v]; ++i)
|
||||
{
|
||||
c = var_lit[v][i].clause_num;
|
||||
//if(clause_delete[c]==1) continue;
|
||||
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
{
|
||||
n=clause_lit[c][j].var_num;
|
||||
if(neighbor_flag[n]!=1)
|
||||
{
|
||||
neighbor_flag[n] = 1;
|
||||
temp_neighbor[temp_neighbor_count++] = n;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
neighbor_flag[v] = 0;
|
||||
|
||||
var_neighbor[v] = new int[temp_neighbor_count+1];
|
||||
|
||||
count = 0;
|
||||
for(i=0; i<temp_neighbor_count; i++)
|
||||
{
|
||||
var_neighbor[v][count++] = temp_neighbor[i];
|
||||
neighbor_flag[temp_neighbor[i]] = 0;
|
||||
}
|
||||
|
||||
var_neighbor[v][count]=0;
|
||||
}
|
||||
|
||||
delete [] neighbor_flag;
|
||||
delete [] temp_neighbor;
|
||||
}
|
||||
|
||||
static inline void ls_update_best_soln(void) {
|
||||
update_best_soln(unsat_stack_fill_pointer, cur_soln, 2);
|
||||
//cout << "c LS_UPDATE_AT\t" << step << "\t" << tries << endl;
|
||||
}
|
||||
|
||||
static inline void unsat(int clause)
|
||||
{
|
||||
index_in_unsat_stack[clause] = unsat_stack_fill_pointer;
|
||||
push(clause,unsat_stack);
|
||||
|
||||
//update appreance count of each var in unsat clause and update stack of vars in unsat clauses
|
||||
int v;
|
||||
for(lit* p=clause_lit[clause]; (v=p->var_num)!=0; p++)
|
||||
{
|
||||
unsat_app_count[v]++;
|
||||
if(unsat_app_count[v]==1)
|
||||
{
|
||||
index_in_unsatvar_stack[v] = unsatvar_stack_fill_pointer;
|
||||
push(v,unsatvar_stack);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static inline void sat(int clause)
|
||||
{
|
||||
int index,last_unsat_clause;
|
||||
|
||||
//since the clause is satisfied, its position can be reused to store the last_unsat_clause
|
||||
last_unsat_clause = pop(unsat_stack);
|
||||
index = index_in_unsat_stack[clause];
|
||||
unsat_stack[index] = last_unsat_clause;
|
||||
index_in_unsat_stack[last_unsat_clause] = index;
|
||||
|
||||
//update appreance count of each var in unsat clause and update stack of vars in unsat clauses
|
||||
int v,last_unsat_var;
|
||||
for(lit* p=clause_lit[clause]; (v=p->var_num)!=0; p++)
|
||||
{
|
||||
unsat_app_count[v]--;
|
||||
if(unsat_app_count[v]==0)
|
||||
{
|
||||
last_unsat_var = pop(unsatvar_stack);
|
||||
index = index_in_unsatvar_stack[v];
|
||||
unsatvar_stack[index] = last_unsat_var;
|
||||
index_in_unsatvar_stack[last_unsat_var] = index;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static void flip(int flipvar)
|
||||
{
|
||||
cur_soln[flipvar] = 1 - cur_soln[flipvar];
|
||||
|
||||
int v,c;
|
||||
|
||||
lit* clause_c;
|
||||
|
||||
int org_flipvar_score = score[flipvar];
|
||||
|
||||
//update related clauses and neighbor vars
|
||||
for(lit *q = var_lit[flipvar]; (c=q->clause_num)>=0; q++)
|
||||
{
|
||||
clause_c = clause_lit[c];
|
||||
if(cur_soln[flipvar] == q->sense)
|
||||
{
|
||||
++sat_count[c];
|
||||
|
||||
if (sat_count[c] == 2) //sat_count from 1 to 2
|
||||
score[sat_var[c]] += clause_weight[c];
|
||||
else if (sat_count[c] == 1) // sat_count from 0 to 1
|
||||
{
|
||||
sat_var[c] = flipvar;//record the only true lit's var
|
||||
for(lit* p=clause_c; (v=p->var_num)!=0; p++) score[v] -= clause_weight[c];
|
||||
|
||||
sat(c);
|
||||
}
|
||||
}
|
||||
else // cur_soln[flipvar] != cur_lit.sense
|
||||
{
|
||||
--sat_count[c];
|
||||
if (sat_count[c] == 1) //sat_count from 2 to 1
|
||||
{
|
||||
for(lit* p=clause_c; (v=p->var_num)!=0; p++)
|
||||
{
|
||||
if(p->sense == cur_soln[v] )
|
||||
{
|
||||
score[v] -= clause_weight[c];
|
||||
sat_var[c] = v;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (sat_count[c] == 0) //sat_count from 1 to 0
|
||||
{
|
||||
for(lit* p=clause_c; (v=p->var_num)!=0; p++) score[v] += clause_weight[c];
|
||||
unsat(c);
|
||||
}//end else if
|
||||
|
||||
}//end else
|
||||
}
|
||||
|
||||
score[flipvar] = -org_flipvar_score;
|
||||
|
||||
/*update CCD */
|
||||
int index;
|
||||
|
||||
conf_change[flipvar] = 0;
|
||||
//remove the vars no longer goodvar in goodvar stack
|
||||
for(index=goodvar_stack_fill_pointer-1; index>=0; index--)
|
||||
{
|
||||
v = goodvar_stack[index];
|
||||
if(score[v]<=0)
|
||||
{
|
||||
goodvar_stack[index] = pop(goodvar_stack);
|
||||
already_in_goodvar_stack[v] = 0;
|
||||
}
|
||||
}
|
||||
|
||||
//update all flipvar's neighbor's conf_change to be 1, add goodvar
|
||||
int* p;
|
||||
for(p=var_neighbor[flipvar]; (v=*p)!=0; p++)
|
||||
{
|
||||
conf_change[v] = 1;
|
||||
|
||||
if(score[v]>0 && already_in_goodvar_stack[v] ==0)
|
||||
{
|
||||
push(v,goodvar_stack);
|
||||
already_in_goodvar_stack[v] = 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/*************weighting ************************************************/
|
||||
|
||||
// swt
|
||||
static int ave_weight=1;
|
||||
static int delta_total_weight=0;
|
||||
int threshold;
|
||||
float p_scale;//w=w*p+ave_w*q
|
||||
float q_scale;
|
||||
int scale_ave;//scale_ave==ave_weight*q_scale
|
||||
|
||||
|
||||
static void smooth_clause_weights_swt(void)
|
||||
{
|
||||
int j,c,v;
|
||||
int new_total_weight=0;
|
||||
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
score[v] = 0;
|
||||
|
||||
//smooth clause score and update score of variables
|
||||
for (c = 0; c<num_clauses; ++c)
|
||||
{
|
||||
clause_weight[c] = clause_weight[c]*p_scale+scale_ave;
|
||||
if(clause_weight[c]<1) clause_weight[c] = 1;
|
||||
|
||||
new_total_weight+=clause_weight[c];
|
||||
|
||||
//update score of variables in this clause
|
||||
if (sat_count[c]==0)
|
||||
{
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
{
|
||||
score[clause_lit[c][j].var_num] += clause_weight[c];
|
||||
}
|
||||
}
|
||||
else if(sat_count[c]==1)
|
||||
score[sat_var[c]]-=clause_weight[c];
|
||||
}
|
||||
|
||||
|
||||
goodvar_stack_fill_pointer = 0;
|
||||
for (v = 1; v <= num_vars; v++) {
|
||||
if(score[v]>0 && conf_change[v]==1) {
|
||||
already_in_goodvar_stack[v] = 1;
|
||||
push(v,goodvar_stack);
|
||||
} else {
|
||||
already_in_goodvar_stack[v] = 0;
|
||||
}
|
||||
}
|
||||
|
||||
ave_weight=new_total_weight/num_clauses;
|
||||
}
|
||||
|
||||
static void weighting_swt(void)
|
||||
{
|
||||
int i,v;
|
||||
|
||||
for(i=0; i < unsat_stack_fill_pointer; ++i)
|
||||
clause_weight[unsat_stack[i]]++;
|
||||
|
||||
for(i=0; i<unsatvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
v = unsatvar_stack[i];
|
||||
score[v] += unsat_app_count[v];
|
||||
//if(score[v]>0 && conf_change[v]==1 && already_in_goodvar_stack[v] ==0)
|
||||
if(score[v]>0 && already_in_goodvar_stack[v] ==0)
|
||||
{
|
||||
push(v,goodvar_stack);
|
||||
already_in_goodvar_stack[v] =1;
|
||||
}
|
||||
}
|
||||
|
||||
delta_total_weight+=unsat_stack_fill_pointer;
|
||||
if(delta_total_weight>=num_clauses)
|
||||
{
|
||||
ave_weight+=1;
|
||||
delta_total_weight -= num_clauses;
|
||||
|
||||
//smooth weights
|
||||
if(ave_weight>threshold)
|
||||
smooth_clause_weights_swt();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
/**********************************PAWS weighting*************************************************/
|
||||
const int dec_weight =1;
|
||||
const float MY_RAND_MAX_FLOAT = 10000000.0;
|
||||
const int MY_RAND_MAX_INT = 10000000;
|
||||
const float BASIC_SCALE = 0.0000001; //1.0f/MY_RAND_MAX_FLOAT;
|
||||
float smooth_probability;
|
||||
int large_clause_count_threshold;
|
||||
|
||||
//for PAWS (for large ksat)
|
||||
int large_weight_clauses[MAX_CLAUSES];
|
||||
int large_weight_clauses_count=0;
|
||||
|
||||
|
||||
void inc_clause_weights_paws()
|
||||
{
|
||||
int i, j, c, v;
|
||||
|
||||
for(i=0; i < unsat_stack_fill_pointer; ++i)
|
||||
{
|
||||
c = unsat_stack[i];
|
||||
clause_weight[c]++;
|
||||
if(clause_weight[c] == 2)
|
||||
{
|
||||
large_weight_clauses[large_weight_clauses_count++] = c;
|
||||
}
|
||||
}
|
||||
|
||||
for(i=0; i<unsatvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
v = unsatvar_stack[i];
|
||||
score[v] += unsat_app_count[v];
|
||||
if(score[v]>0 && conf_change[v]>0 && already_in_goodvar_stack[v] ==0)//
|
||||
{
|
||||
push(v,goodvar_stack);
|
||||
already_in_goodvar_stack[v] =1;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void smooth_clause_weights_paws()
|
||||
{
|
||||
int i, j,clause, var;
|
||||
for(i=0; i<large_weight_clauses_count; i++)
|
||||
{
|
||||
clause = large_weight_clauses[i];
|
||||
if(sat_count[clause]>0)
|
||||
{
|
||||
clause_weight[clause]-=dec_weight;
|
||||
|
||||
if(clause_weight[clause]==1)
|
||||
{
|
||||
large_weight_clauses[i] = large_weight_clauses[--large_weight_clauses_count];
|
||||
i--;
|
||||
}
|
||||
if(sat_count[clause] == 1)
|
||||
{
|
||||
var = sat_var[clause];
|
||||
score[var]+=dec_weight;
|
||||
if(score[var]>0 && conf_change[var]>0 && already_in_goodvar_stack[var]==0)
|
||||
{
|
||||
push(var,goodvar_stack);
|
||||
already_in_goodvar_stack[var]=1;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void weighting_paws()
|
||||
{
|
||||
if( ((rand()%MY_RAND_MAX_INT)*BASIC_SCALE)<smooth_probability && large_weight_clauses_count>large_clause_count_threshold )
|
||||
smooth_clause_weights_paws();
|
||||
else
|
||||
inc_clause_weights_paws();
|
||||
}
|
||||
|
||||
/**************************setting clause weighting scheme***********************/
|
||||
|
||||
void (* update_clause_weights)();
|
||||
|
||||
void default_clause_weighting(int weighting_type)
|
||||
{
|
||||
if(weighting_type==1)
|
||||
{
|
||||
//swt
|
||||
update_clause_weights = weighting_swt;
|
||||
threshold=50;//560; // 500
|
||||
p_scale=0.3;//0.52;
|
||||
q_scale=0.7;//0.42;
|
||||
scale_ave=(threshold+1)*q_scale;
|
||||
}
|
||||
else
|
||||
{
|
||||
//paws
|
||||
update_clause_weights = weighting_paws;
|
||||
smooth_probability = 0.1;
|
||||
large_clause_count_threshold = 10;//do we need this parameter?
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
/********************************************end weighting************************************/
|
||||
|
||||
static int pick_var(void)
|
||||
{
|
||||
int i,k,c,v;
|
||||
int best_var;
|
||||
lit* clause_c;
|
||||
|
||||
/**Greedy Mode**/
|
||||
/*CCD (configuration changed decreasing) mode, the level with configuation chekcing*/
|
||||
if(goodvar_stack_fill_pointer>0)
|
||||
{
|
||||
|
||||
//if(goodvar_stack_fill_pointer<balancePar)
|
||||
//{
|
||||
best_var = goodvar_stack[0];
|
||||
for(i=1; i<goodvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
v=goodvar_stack[i];
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var])
|
||||
{
|
||||
//if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
|
||||
//else if(unsat_app_count[v]==unsat_app_count[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
|
||||
if(time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
}
|
||||
return best_var;
|
||||
//}
|
||||
/*else
|
||||
{
|
||||
best_var = goodvar_stack[rand()%goodvar_stack_fill_pointer];
|
||||
for(int j=1;j<balancePar;++j)
|
||||
{
|
||||
v = goodvar_stack[rand()%goodvar_stack_fill_pointer];
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var])
|
||||
{
|
||||
//if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
|
||||
//else if(unsat_app_count[v]==unsat_app_count[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
if(time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
}
|
||||
return best_var;
|
||||
}*/
|
||||
}
|
||||
|
||||
|
||||
/*aspiration*/
|
||||
if (aspiration_active)
|
||||
{
|
||||
best_var = 0;
|
||||
for(i=0; i<unsatvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
if(score[unsatvar_stack[i]]>ave_weight)
|
||||
{
|
||||
best_var = unsatvar_stack[i];
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
for(++i; i<unsatvar_stack_fill_pointer; ++i)
|
||||
{
|
||||
v=unsatvar_stack[i];
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var] && time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
|
||||
if(best_var!=0) return best_var;
|
||||
}
|
||||
/*****end aspiration*******************/
|
||||
|
||||
update_clause_weights();
|
||||
|
||||
/*focused random walk*/
|
||||
|
||||
c = unsat_stack[rand()%unsat_stack_fill_pointer];
|
||||
clause_c = clause_lit[c];
|
||||
best_var = clause_c[0].var_num;
|
||||
for(k=1; k<clause_lit_count[c]; ++k)
|
||||
{
|
||||
v=clause_c[k].var_num;
|
||||
|
||||
//using score
|
||||
//if(score[v]>score[best_var]) best_var = v;
|
||||
//else if(score[v]==score[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
|
||||
//using unweighted make
|
||||
if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
|
||||
//else if(unsat_app_count[v]==unsat_app_count[best_var] && time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
else if(unsat_app_count[v]==unsat_app_count[best_var])
|
||||
{
|
||||
if(score[v]>score[best_var]) best_var = v;
|
||||
else if(score[v]==score[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
|
||||
}
|
||||
}
|
||||
|
||||
return best_var;
|
||||
}
|
||||
|
||||
|
||||
//set functions in the algorithm
|
||||
|
||||
void ls_init(void) {
|
||||
build_neighbor_relation();
|
||||
}
|
||||
|
||||
void ls_restart(const int *soln, const int opt) {
|
||||
int v, c, i;
|
||||
for (c = 0; c<num_clauses; c++)
|
||||
clause_weight[c] = 1;
|
||||
for (v = 1; v <= num_vars; ++v) {
|
||||
assert(0 == soln[v] || 1 == soln[v]);
|
||||
cur_soln[v] = soln[v];
|
||||
}
|
||||
|
||||
unsat_stack_fill_pointer = 0;
|
||||
unsatvar_stack_fill_pointer = 0;
|
||||
|
||||
step = 0;
|
||||
|
||||
for (v = 1; v <= num_vars; v++) {
|
||||
time_stamp[v] = 0;
|
||||
conf_change[v] = 1;
|
||||
unsat_app_count[v] = 0;
|
||||
}
|
||||
|
||||
/* figure out sat_count, and init unsat_stack */
|
||||
for (c = 0; c < num_clauses; ++c) {
|
||||
sat_count[c] = 0;
|
||||
for(i = 0; i < clause_lit_count[c]; ++i) {
|
||||
if (cur_soln[clause_lit[c][i].var_num] == clause_lit[c][i].sense) {
|
||||
sat_count[c]++;
|
||||
sat_var[c] = clause_lit[c][i].var_num;
|
||||
}
|
||||
}
|
||||
if (sat_count[c] == 0)
|
||||
unsat(c);
|
||||
}
|
||||
|
||||
/*figure out var score*/
|
||||
int lit_count;
|
||||
for (v = 1; v <= num_vars; v++) {
|
||||
score[v] = 0;
|
||||
lit_count = var_lit_count[v];
|
||||
|
||||
for(i = 0; i < lit_count; ++i) {
|
||||
c = var_lit[v][i].clause_num;
|
||||
if (sat_count[c] == 0)
|
||||
score[v]++;
|
||||
else if (sat_count[c] == 1 && var_lit[v][i].sense == cur_soln[v])
|
||||
score[v]--;
|
||||
}
|
||||
}
|
||||
|
||||
//init goodvars stack
|
||||
goodvar_stack_fill_pointer = 0;
|
||||
for (v = 1; v <= num_vars; v++) {
|
||||
if(score[v]>0) {
|
||||
already_in_goodvar_stack[v] = 1;
|
||||
push(v,goodvar_stack);
|
||||
} else {
|
||||
already_in_goodvar_stack[v] = 0;
|
||||
}
|
||||
}
|
||||
|
||||
//setting for the virtual var 0
|
||||
time_stamp[0] = 0;
|
||||
|
||||
lb_opt = opt;
|
||||
lb_copy();
|
||||
|
||||
|
||||
}
|
||||
|
||||
int lb_update_reduce;
|
||||
void ls_process(long long no_improv_times) {
|
||||
int flipvar;
|
||||
long long notime = 1 + no_improv_times;
|
||||
while (--notime) {
|
||||
step++;
|
||||
|
||||
flipvar = pick_var();
|
||||
flip(flipvar);
|
||||
time_stamp[flipvar] = step;
|
||||
|
||||
if (unsat_stack_fill_pointer < lb_opt) {
|
||||
lb_opt = unsat_stack_fill_pointer;
|
||||
lb_copy();
|
||||
notime = 1 + no_improv_times;
|
||||
}
|
||||
|
||||
if (unsat_stack_fill_pointer < the_best.opt_unsat) {
|
||||
update_best_value(unsat_stack_fill_pointer);
|
||||
lb_update(tries);
|
||||
|
||||
if(the_best.opt_unsat==0) {
|
||||
ls_update_best_soln();
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
if (get_runtime() >= cutoff_time) {
|
||||
return;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
int b = tries / lb_update_reduce;
|
||||
if (0 == b)
|
||||
b = 1;
|
||||
lb_update(b);
|
||||
}
|
||||
|
||||
@ -1,21 +0,0 @@
|
||||
#ifndef _INDUSLS_HPP_
|
||||
#define _INDUSLS_HPP_
|
||||
|
||||
extern int balancePar;
|
||||
extern int lb_update_reduce;
|
||||
extern bool aspiration_active;
|
||||
|
||||
extern int threshold;
|
||||
extern float p_scale;//w=w*p+ave_w*q
|
||||
extern float q_scale;
|
||||
|
||||
void ls_init(void);
|
||||
void ls_process(long long no_improv_times);
|
||||
void ls_restart(const int *soln, const int opt);
|
||||
|
||||
void default_clause_weighting(int weighting_type);
|
||||
|
||||
bool lb_get_prob(int v);
|
||||
bool lb_get_last(int v);
|
||||
|
||||
#endif
|
||||
@ -1,48 +0,0 @@
|
||||
MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010 Niklas Sorensson
|
||||
Glucose -- Copyright (c) 2009-2012, Gilles Audemard, Laurent Simon
|
||||
Coprocessor -- Copyright (c) 2012-2014, Norbert Manthey
|
||||
CCAnr+cnc -- Copyright (c) 2021, Shaowei Cai, Chuan Luo
|
||||
|
||||
Permission is hereby granted, free of charge, to use this software for
|
||||
evaluation and research purposes.
|
||||
|
||||
The permission to use the code of Coprocessor within the submission
|
||||
of the solver CPSparrow version sc14 for the SAT Competition 2014
|
||||
has been granted.
|
||||
|
||||
This license does not allow this software to be used in a commercial context.
|
||||
|
||||
It is further prohibited to use this software or a substantial portion of it
|
||||
in a competition or a similar competetive event, such as the SAT, SMT or QBF,
|
||||
MaxSAT or HWMCC competitions or evaluations, without explicit written
|
||||
permission by the copyright holder.
|
||||
|
||||
However, competition organizers are allowed to use this software as part of
|
||||
the evaluation process of a particular competition, evaluation or
|
||||
competetive event, if the copyright holder of this software submitted this
|
||||
software to this particular competition, evaluation or event explicitly.
|
||||
|
||||
This permission of using the software as part of a submission by the
|
||||
copyright holder to a competition, evaluation or competive event is only
|
||||
granted for one year and only for one particular instance of the competition
|
||||
to which this software was submitted by the copyright holder.
|
||||
|
||||
If a competition, evaluation or competetive event has multiple tracks,
|
||||
categories or sub-competitions, this license is only granted for the tracks
|
||||
respectively categories or sub-competitions, to which the software was
|
||||
explicitly submitted by the copyright holder.
|
||||
|
||||
All other usage is reserved.
|
||||
|
||||
The above copyright notice and this permission notice shall be included in
|
||||
all copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
|
||||
IN THE SOFTWARE.
|
||||
|
||||
274
CCAnr/main.cc
274
CCAnr/main.cc
@ -1,274 +0,0 @@
|
||||
#include "basis.hpp"
|
||||
#include "cnc.hpp"
|
||||
#include "indusLS.hpp"
|
||||
#include <sstream>
|
||||
#include <cstdlib>
|
||||
#include <iostream>
|
||||
#include <stdio.h>
|
||||
#include<string.h>
|
||||
#include "indusLS.hpp"
|
||||
using namespace std;
|
||||
|
||||
static void doLS_dynamic(void);
|
||||
static void doLS_static(void);
|
||||
|
||||
char * inst;
|
||||
int seed;
|
||||
|
||||
static int cnc_times, ls_no_improv_times;
|
||||
static int cb_cap;
|
||||
static void (*doLS) (void);
|
||||
|
||||
int weighting_type;
|
||||
|
||||
static void default_settings(void) {
|
||||
ios::sync_with_stdio(false);
|
||||
|
||||
cnc_times = 5;
|
||||
ls_no_improv_times = 50000000;
|
||||
doLS = doLS_dynamic;
|
||||
|
||||
cb_cap = 50;
|
||||
balancePar = 40;// no use;
|
||||
lb_last_prob = 1;
|
||||
lb_update_reduce = 1;
|
||||
vage_window = 10;
|
||||
|
||||
aspiration_active = false;
|
||||
|
||||
weighting_type = 1; //1->SWT; 2->PAWS
|
||||
default_clause_weighting(weighting_type);
|
||||
|
||||
seed = 1;
|
||||
cutoff_time = 3600;
|
||||
}
|
||||
|
||||
static void doLsRestartToCanBest(void) {
|
||||
const int *soln;
|
||||
int opt;
|
||||
if (cnc_get_canbest(soln, opt)) {
|
||||
//cout << "c LS force restart to opt=" << opt << " at " << get_runtime() << endl;
|
||||
ls_restart(soln, opt);
|
||||
}
|
||||
}
|
||||
|
||||
static void doLsRestartToBest(void) {
|
||||
ls_restart(the_best.soln, the_best.opt_unsat);
|
||||
}
|
||||
|
||||
|
||||
static void doCNC(void) {
|
||||
cnc_process(cnc_times);
|
||||
//if (the_best.opt_try == tries)
|
||||
// cout << "c CNC update: " << the_best.opt_unsat << " at " << the_best.opt_time << endl;
|
||||
}
|
||||
|
||||
|
||||
int max_no_improv_times=20000000;
|
||||
static void doLS_dynamic(void) {
|
||||
if (ls_no_improv_times*tries<max_no_improv_times)
|
||||
ls_process(ls_no_improv_times*tries);
|
||||
else
|
||||
ls_process(max_no_improv_times);
|
||||
}
|
||||
|
||||
static void doLS_static(void) {
|
||||
ls_process(ls_no_improv_times);
|
||||
}
|
||||
|
||||
/*
|
||||
* About shouldPrint:
|
||||
*
|
||||
* At the beginning, shouldPrint = false. o line is printed immediately by update_best_soln() in basis.cpp, while v line is not printed.
|
||||
* When there's 90s left, shouldPrint = true. o line will not be printed in update_best_soln(). These lines should be printed by main().
|
||||
* The reason is that, v line takes too much time. If doLS() updates solution too frequently, doLS() may take so much time on printing and left an incomplete v line.
|
||||
*
|
||||
* In conclusion, v line has to be printed by main() in any situation, and o line will be printed immediately in first 210s by update_best_soln().
|
||||
* In last 90s, update_best_soln() does not print o line, and which should be printed by main().
|
||||
* */
|
||||
|
||||
|
||||
|
||||
bool parse_arguments(int argc, char ** argv)
|
||||
{
|
||||
|
||||
bool flag_inst = false;
|
||||
default_settings();
|
||||
|
||||
for (int i=1; i<argc; i++)
|
||||
{
|
||||
if(strcmp(argv[i],"-inst")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
inst = argv[i];
|
||||
flag_inst = true;
|
||||
continue;
|
||||
}
|
||||
else if(strcmp(argv[i],"-seed")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
sscanf(argv[i], "%d", &seed);
|
||||
continue;
|
||||
}
|
||||
else if(strcmp(argv[i],"-cutoff_time")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
sscanf(argv[i], "%d", &cutoff_time);
|
||||
continue;
|
||||
}
|
||||
|
||||
else if(strcmp(argv[i],"-aspiration")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
int tmp;
|
||||
sscanf(argv[i], "%d", &tmp);
|
||||
if (tmp==1)
|
||||
aspiration_active = true;
|
||||
else aspiration_active = false;
|
||||
continue;
|
||||
}
|
||||
|
||||
else if(strcmp(argv[i],"-swt_threshold")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
sscanf(argv[i], "%d", &threshold);
|
||||
continue;
|
||||
}
|
||||
else if(strcmp(argv[i],"-swt_p")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
sscanf(argv[i], "%f", &p_scale);
|
||||
continue;
|
||||
}
|
||||
else if(strcmp(argv[i],"-swt_q")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
sscanf(argv[i], "%f", &q_scale);
|
||||
continue;
|
||||
}
|
||||
|
||||
|
||||
else if(strcmp(argv[i],"-dynamic")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
if(strcmp(argv[i], "0")==0)
|
||||
{
|
||||
doLS = doLS_static;
|
||||
continue;
|
||||
}
|
||||
else if(strcmp(argv[i], "1")==0)
|
||||
{
|
||||
doLS = doLS_dynamic;
|
||||
continue;
|
||||
}
|
||||
else return false;
|
||||
}
|
||||
else if(strcmp(argv[i],"-cnctimes")==0)
|
||||
{
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
sscanf(argv[i], "%d", &cnc_times);
|
||||
continue;
|
||||
}
|
||||
else if(strcmp(argv[i],"-ls_no_improv_steps")==0){
|
||||
i++;
|
||||
if(i>=argc) return false;
|
||||
sscanf(argv[i], "%d", &ls_no_improv_times);
|
||||
continue;
|
||||
}
|
||||
else return false;
|
||||
|
||||
}
|
||||
|
||||
if (flag_inst) return true;
|
||||
else return false;
|
||||
|
||||
}
|
||||
|
||||
int main(int argc, char* argv[]) {
|
||||
|
||||
int ret;
|
||||
|
||||
ret = parse_arguments(argc, argv);
|
||||
if(!ret) {cout<<"c Arguments Error!"<<endl; return -1;}
|
||||
|
||||
ret = build_instance(inst);
|
||||
if (0 == ret) {
|
||||
cout << "c Invalid filename: " << argv[1] << endl;
|
||||
return 1;
|
||||
}
|
||||
|
||||
record_runtime();
|
||||
|
||||
cnc_init(cb_cap);
|
||||
ls_init();
|
||||
|
||||
srand(seed);
|
||||
|
||||
for (tries = 1; ; tries++) {
|
||||
doCNC();
|
||||
|
||||
/*if (shouldPrint && the_best.opt_try == tries) {
|
||||
cout << "o " << the_best.opt_unsat << endl;
|
||||
print_best_solution();
|
||||
}*/
|
||||
|
||||
if(the_best.opt_unsat==0) break;
|
||||
|
||||
if (the_best.opt_try == tries)
|
||||
doLsRestartToBest();
|
||||
else
|
||||
doLsRestartToCanBest();
|
||||
|
||||
doLS();
|
||||
|
||||
if(the_best.opt_unsat==0) break;
|
||||
|
||||
/*if (shouldPrint && the_best.opt_try == tries && 2 == the_best.source) {
|
||||
cout << "o " << the_best.opt_unsat << endl;
|
||||
print_best_solution();
|
||||
}
|
||||
|
||||
if (!shouldPrint) {
|
||||
if (get_runtime() >= cutoff_time - 90) {
|
||||
shouldPrint = true;
|
||||
print_best_solution();
|
||||
}
|
||||
} else {
|
||||
const double now = get_runtime();
|
||||
double left = 2 * now / tries; // the time needed for two `CNC-LS' rounds
|
||||
if (left < 10.0)
|
||||
left = 10.0;
|
||||
// 6s to 10s are left.
|
||||
if (now >= cutoff_time - left) {
|
||||
break;
|
||||
}
|
||||
}*/
|
||||
const double now = get_runtime();
|
||||
if (now >= cutoff_time) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
//cout << "c TotalTry=" << tries << endl;
|
||||
//cout << "c Finished at " << get_runtime() << endl;
|
||||
//cout << "c " << inst << "\t" << the_best.opt_unsat << '\t' << the_best.opt_time << endl;
|
||||
|
||||
cout<<"s ";
|
||||
if (0==the_best.opt_unsat && verify_sol() ) {
|
||||
cout<<"SATISFIABLE"<<endl;
|
||||
print_best_solution();
|
||||
}
|
||||
else cout<<"UNKNOWN"<<endl;
|
||||
|
||||
|
||||
return 0;
|
||||
}
|
||||
133
CCAnr/preprocessor.h
Normal file
133
CCAnr/preprocessor.h
Normal file
@ -0,0 +1,133 @@
|
||||
#include "basis.h"
|
||||
//preprocess
|
||||
void unit_propagation()
|
||||
{
|
||||
lit uc_lit;
|
||||
int uc_clause;
|
||||
int uc_var;
|
||||
bool uc_sense;
|
||||
|
||||
int c,v;
|
||||
int i,j;
|
||||
lit cur, cur_c;
|
||||
|
||||
|
||||
//while (unitclause_queue_beg_pointer < unitclause_queue_end_pointer)
|
||||
for(unitclause_queue_beg_pointer=0; unitclause_queue_beg_pointer < unitclause_queue_end_pointer; unitclause_queue_beg_pointer++)
|
||||
{
|
||||
uc_lit = unitclause_queue[unitclause_queue_beg_pointer];
|
||||
|
||||
uc_var = uc_lit.var_num;
|
||||
uc_sense = uc_lit.sense;
|
||||
|
||||
if(fix[uc_var]==1) {if(uc_sense!=cur_soln[uc_var])cout<<"c wants to fix a variable twice, forbid."<<endl; continue;}
|
||||
|
||||
cur_soln[uc_var] = uc_sense;//fix the variable in unit clause
|
||||
fix[uc_var] = 1;
|
||||
|
||||
for(i = 0; i<var_lit_count[uc_var]; ++i)
|
||||
{
|
||||
cur = var_lit[uc_var][i];
|
||||
c = cur.clause_num;
|
||||
|
||||
if(clause_delete[c]==1) continue;
|
||||
|
||||
if(cur.sense == uc_sense)//then remove the clause from var's var_lit[] array
|
||||
{
|
||||
clause_delete[c]=1;
|
||||
}
|
||||
else
|
||||
{
|
||||
if(clause_lit_count[c]==2)
|
||||
{
|
||||
if(clause_lit[c][0].var_num == uc_var)
|
||||
{
|
||||
unitclause_queue[unitclause_queue_end_pointer++] = clause_lit[c][1];
|
||||
}
|
||||
else
|
||||
{
|
||||
unitclause_queue[unitclause_queue_end_pointer++] = clause_lit[c][0];
|
||||
}
|
||||
|
||||
clause_delete[c]=1;
|
||||
}
|
||||
else
|
||||
{
|
||||
for(j=0; j<clause_lit_count[c]; ++j)
|
||||
{
|
||||
if(clause_lit[c][j].var_num == uc_var)
|
||||
{
|
||||
clause_lit[c][j]=clause_lit[c][clause_lit_count[c]-1];
|
||||
|
||||
clause_lit_count[c]--;
|
||||
|
||||
break;
|
||||
}
|
||||
}//for
|
||||
}
|
||||
}
|
||||
|
||||
}//for
|
||||
|
||||
|
||||
|
||||
}//begpointer to endpointer for
|
||||
|
||||
}
|
||||
|
||||
|
||||
void preprocess()
|
||||
{
|
||||
int c,v,i;
|
||||
int delete_clause_count=0;
|
||||
int fix_var_count=0;
|
||||
|
||||
unit_propagation();
|
||||
|
||||
//rescan all clauses to build up var literal arrays
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
var_lit_count[v] = 0;
|
||||
|
||||
max_clause_len = 0;
|
||||
min_clause_len = num_vars;
|
||||
int formula_len=0;
|
||||
|
||||
for (c = 0; c < num_clauses; ++c)
|
||||
{
|
||||
if(clause_delete[c]==1) {
|
||||
delete_clause_count++;
|
||||
continue;
|
||||
}
|
||||
|
||||
for(i=0; i<clause_lit_count[c]; ++i)
|
||||
{
|
||||
v = clause_lit[c][i].var_num;
|
||||
var_lit[v][var_lit_count[v]] = clause_lit[c][i];
|
||||
++var_lit_count[v];
|
||||
}
|
||||
clause_lit[c][i].var_num=0; //new clause boundary
|
||||
clause_lit[c][i].clause_num = -1;
|
||||
|
||||
//about clause length
|
||||
formula_len += clause_lit_count[c];
|
||||
|
||||
if(clause_lit_count[c] > max_clause_len)
|
||||
max_clause_len = clause_lit_count[c];
|
||||
else if(clause_lit_count[c] < min_clause_len)
|
||||
min_clause_len = clause_lit_count[c];
|
||||
}
|
||||
|
||||
avg_clause_len = (double)formula_len/num_clauses;
|
||||
|
||||
for (v=1; v<=num_vars; ++v)
|
||||
{
|
||||
if(fix[v]==1)
|
||||
{
|
||||
fix_var_count++;
|
||||
}
|
||||
var_lit[v][var_lit_count[v]].clause_num=-1;//new var_lit boundary
|
||||
}
|
||||
|
||||
cout<<"c unit propagation fixes "<<fix_var_count<<" variables, and delets "<<delete_clause_count<<" clauses"<<endl;
|
||||
|
||||
}
|
||||
@ -1,16 +0,0 @@
|
||||
Instructions about how to compile and run CCAnr+cnc:
|
||||
|
||||
Compile CCAnr+cnc:
|
||||
make
|
||||
|
||||
Run CCAnr+cnc:
|
||||
./CCAnr+cnc
|
||||
-inst <cnf_instance>
|
||||
-seed <seed>
|
||||
-cutoff_time <cutoff_time>
|
||||
-dynamic {0,1} ##0 indicates performing non-dynamic method; 1 indicates performing dynamic method
|
||||
-cnctimes <cnc_times> ##indicate the value of cnc_times underlying CCAnr+cnc
|
||||
-ls_no_improv_steps <MaxNoImprSteps> ##indicate the value of MaxNoImprSteps underlying CCAnr+cnc
|
||||
-swt_p <\rho> ##indicate the value of \rho underlying CCAnr
|
||||
-swt_q <q> ##indicate the value of q underlying CCAnr
|
||||
-swt_threshold <\gamma> ##indicate the value of \gamma underlying CCAnr
|
||||
515
CCAnr/test.cnf
Normal file
515
CCAnr/test.cnf
Normal file
@ -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
|
||||
8829
_c6288.txt
8829
_c6288.txt
File diff suppressed because it is too large
Load Diff
207
c432.bench
207
c432.bench
@ -1,207 +0,0 @@
|
||||
# c432
|
||||
|
||||
INPUT(1)
|
||||
INPUT(4)
|
||||
INPUT(8)
|
||||
INPUT(11)
|
||||
INPUT(14)
|
||||
INPUT(17)
|
||||
INPUT(21)
|
||||
INPUT(24)
|
||||
INPUT(27)
|
||||
INPUT(30)
|
||||
INPUT(34)
|
||||
INPUT(37)
|
||||
INPUT(40)
|
||||
INPUT(43)
|
||||
INPUT(47)
|
||||
INPUT(50)
|
||||
INPUT(53)
|
||||
INPUT(56)
|
||||
INPUT(60)
|
||||
INPUT(63)
|
||||
INPUT(66)
|
||||
INPUT(69)
|
||||
INPUT(73)
|
||||
INPUT(76)
|
||||
INPUT(79)
|
||||
INPUT(82)
|
||||
INPUT(86)
|
||||
INPUT(89)
|
||||
INPUT(92)
|
||||
INPUT(95)
|
||||
INPUT(99)
|
||||
INPUT(102)
|
||||
INPUT(105)
|
||||
INPUT(108)
|
||||
INPUT(112)
|
||||
INPUT(115)
|
||||
|
||||
OUTPUT(223)
|
||||
OUTPUT(329)
|
||||
OUTPUT(370)
|
||||
OUTPUT(421)
|
||||
OUTPUT(430)
|
||||
OUTPUT(431)
|
||||
OUTPUT(432)
|
||||
|
||||
118 = NOT(1)
|
||||
119 = NOT(4)
|
||||
122 = NOT(11)
|
||||
123 = NOT(17)
|
||||
126 = NOT(24)
|
||||
127 = NOT(30)
|
||||
130 = NOT(37)
|
||||
131 = NOT(43)
|
||||
134 = NOT(50)
|
||||
135 = NOT(56)
|
||||
138 = NOT(63)
|
||||
139 = NOT(69)
|
||||
142 = NOT(76)
|
||||
143 = NOT(82)
|
||||
146 = NOT(89)
|
||||
147 = NOT(95)
|
||||
150 = NOT(102)
|
||||
151 = NOT(108)
|
||||
154 = NAND(118, 4)
|
||||
157 = NOR(8, 119)
|
||||
158 = NOR(14, 119)
|
||||
159 = NAND(122, 17)
|
||||
162 = NAND(126, 30)
|
||||
165 = NAND(130, 43)
|
||||
168 = NAND(134, 56)
|
||||
171 = NAND(138, 69)
|
||||
174 = NAND(142, 82)
|
||||
177 = NAND(146, 95)
|
||||
180 = NAND(150, 108)
|
||||
183 = NOR(21, 123)
|
||||
184 = NOR(27, 123)
|
||||
185 = NOR(34, 127)
|
||||
186 = NOR(40, 127)
|
||||
187 = NOR(47, 131)
|
||||
188 = NOR(53, 131)
|
||||
189 = NOR(60, 135)
|
||||
190 = NOR(66, 135)
|
||||
191 = NOR(73, 139)
|
||||
192 = NOR(79, 139)
|
||||
193 = NOR(86, 143)
|
||||
194 = NOR(92, 143)
|
||||
195 = NOR(99, 147)
|
||||
196 = NOR(105, 147)
|
||||
197 = NOR(112, 151)
|
||||
198 = NOR(115, 151)
|
||||
199 = AND(154, 159, 162, 165, 168, 171, 174, 177, 180)
|
||||
203 = NOT(199)
|
||||
213 = NOT(199)
|
||||
223 = NOT(199)
|
||||
224 = XOR(203, 154)
|
||||
227 = XOR(203, 159)
|
||||
230 = XOR(203, 162)
|
||||
233 = XOR(203, 165)
|
||||
236 = XOR(203, 168)
|
||||
239 = XOR(203, 171)
|
||||
242 = NAND(1, 213)
|
||||
243 = XOR(203, 174)
|
||||
246 = NAND(213, 11)
|
||||
247 = XOR(203, 177)
|
||||
250 = NAND(213, 24)
|
||||
251 = XOR(203, 180)
|
||||
254 = NAND(213, 37)
|
||||
255 = NAND(213, 50)
|
||||
256 = NAND(213, 63)
|
||||
257 = NAND(213, 76)
|
||||
258 = NAND(213, 89)
|
||||
259 = NAND(213, 102)
|
||||
260 = NAND(224, 157)
|
||||
263 = NAND(224, 158)
|
||||
264 = NAND(227, 183)
|
||||
267 = NAND(230, 185)
|
||||
270 = NAND(233, 187)
|
||||
273 = NAND(236, 189)
|
||||
276 = NAND(239, 191)
|
||||
279 = NAND(243, 193)
|
||||
282 = NAND(247, 195)
|
||||
285 = NAND(251, 197)
|
||||
288 = NAND(227, 184)
|
||||
289 = NAND(230, 186)
|
||||
290 = NAND(233, 188)
|
||||
291 = NAND(236, 190)
|
||||
292 = NAND(239, 192)
|
||||
293 = NAND(243, 194)
|
||||
294 = NAND(247, 196)
|
||||
295 = NAND(251, 198)
|
||||
296 = AND(260, 264, 267, 270, 273, 276, 279, 282, 285)
|
||||
300 = NOT(263)
|
||||
301 = NOT(288)
|
||||
302 = NOT(289)
|
||||
303 = NOT(290)
|
||||
304 = NOT(291)
|
||||
305 = NOT(292)
|
||||
306 = NOT(293)
|
||||
307 = NOT(294)
|
||||
308 = NOT(295)
|
||||
309 = NOT(296)
|
||||
319 = NOT(296)
|
||||
329 = NOT(296)
|
||||
330 = XOR(309, 260)
|
||||
331 = XOR(309, 264)
|
||||
332 = XOR(309, 267)
|
||||
333 = XOR(309, 270)
|
||||
334 = NAND(8, 319)
|
||||
335 = XOR(309, 273)
|
||||
336 = NAND(319, 21)
|
||||
337 = XOR(309, 276)
|
||||
338 = NAND(319, 34)
|
||||
339 = XOR(309, 279)
|
||||
340 = NAND(319, 47)
|
||||
341 = XOR(309, 282)
|
||||
342 = NAND(319, 60)
|
||||
343 = XOR(309, 285)
|
||||
344 = NAND(319, 73)
|
||||
345 = NAND(319, 86)
|
||||
346 = NAND(319, 99)
|
||||
347 = NAND(319, 112)
|
||||
348 = NAND(330, 300)
|
||||
349 = NAND(331, 301)
|
||||
350 = NAND(332, 302)
|
||||
351 = NAND(333, 303)
|
||||
352 = NAND(335, 304)
|
||||
353 = NAND(337, 305)
|
||||
354 = NAND(339, 306)
|
||||
355 = NAND(341, 307)
|
||||
356 = NAND(343, 308)
|
||||
357 = AND(348, 349, 350, 351, 352, 353, 354, 355, 356)
|
||||
360 = NOT(357)
|
||||
370 = NOT(357)
|
||||
371 = NAND(14, 360)
|
||||
372 = NAND(360, 27)
|
||||
373 = NAND(360, 40)
|
||||
374 = NAND(360, 53)
|
||||
375 = NAND(360, 66)
|
||||
376 = NAND(360, 79)
|
||||
377 = NAND(360, 92)
|
||||
378 = NAND(360, 105)
|
||||
379 = NAND(360, 115)
|
||||
380 = NAND(4, 242, 334, 371)
|
||||
381 = NAND(246, 336, 372, 17)
|
||||
386 = NAND(250, 338, 373, 30)
|
||||
393 = NAND(254, 340, 374, 43)
|
||||
399 = NAND(255, 342, 375, 56)
|
||||
404 = NAND(256, 344, 376, 69)
|
||||
407 = NAND(257, 345, 377, 82)
|
||||
411 = NAND(258, 346, 378, 95)
|
||||
414 = NAND(259, 347, 379, 108)
|
||||
415 = NOT(380)
|
||||
416 = AND(381, 386, 393, 399, 404, 407, 411, 414)
|
||||
417 = NOT(393)
|
||||
418 = NOT(404)
|
||||
419 = NOT(407)
|
||||
420 = NOT(411)
|
||||
421 = NOR(415, 416)
|
||||
422 = NAND(386, 417)
|
||||
425 = NAND(386, 393, 418, 399)
|
||||
428 = NAND(399, 393, 419)
|
||||
429 = NAND(386, 393, 407, 420)
|
||||
430 = NAND(381, 386, 422, 399)
|
||||
431 = NAND(381, 386, 425, 428)
|
||||
432 = NAND(381, 422, 425, 429)
|
||||
10
c432.report
10
c432.report
@ -1,10 +0,0 @@
|
||||
gates: 160
|
||||
primary input: 36
|
||||
primary output: 7
|
||||
simulate patterns: 0
|
||||
final patterns: 77
|
||||
faults: 524
|
||||
detect faults: 520
|
||||
redundant faults: 0
|
||||
test coverage:0.992
|
||||
time: 0.00859
|
||||
2484
c6288.bench
2484
c6288.bench
File diff suppressed because it is too large
Load Diff
26
check.log
26
check.log
@ -1,26 +0,0 @@
|
||||
[1/26] 任务 ./benchmark/c17.bench
|
||||
[2/26] 任务 ./benchmark/b06.bench
|
||||
[3/26] 任务 ./benchmark/b01.bench
|
||||
[4/26] 任务 ./benchmark/b03.bench
|
||||
[5/26] 任务 ./benchmark/b09.bench
|
||||
[6/26] 任务 ./benchmark/c880.bench
|
||||
[7/26] 任务 ./benchmark/b10.bench
|
||||
[8/26] 任务 ./benchmark/b08.bench
|
||||
[9/26] 任务 ./benchmark/c499.bench
|
||||
[10/26] 任务 ./benchmark/c1355.bench
|
||||
[11/26] 任务 ./benchmark/c3540.bench
|
||||
[12/26] 任务 ./benchmark/c1908.bench
|
||||
[13/26] 任务 ./benchmark/b11.bench
|
||||
[14/26] 任务 ./benchmark/c6288.bench
|
||||
[15/26] 任务 ./benchmark/c2670.bench
|
||||
[16/26] 任务 ./benchmark/b21.bench
|
||||
[17/26] 任务 ./benchmark/b13.bench
|
||||
[18/26] 任务 ./benchmark/b22.bench
|
||||
[19/26] 任务 ./benchmark/b17.bench
|
||||
[20/26] 任务 ./benchmark/b20.bench
|
||||
[21/26] 任务 ./benchmark/c7552.bench
|
||||
[22/26] 任务 ./benchmark/b12.bench
|
||||
[23/26] 任务 ./benchmark/c5315.bench
|
||||
[24/26] 任务 ./benchmark/b04.bench
|
||||
[25/26] 任务 ./benchmark/b07.bench
|
||||
[26/26] 任务 ./benchmark/c432.bench
|
||||
22
clause.cpp
22
clause.cpp
@ -59,28 +59,10 @@ void write_cnf() {
|
||||
}
|
||||
|
||||
f.close();
|
||||
}
|
||||
}
|
||||
|
||||
void flip(int var) {
|
||||
|
||||
// printf("value: [ ");
|
||||
|
||||
// for(int i=1; i<=num_vars; i++) {
|
||||
// printf("%d ", lit_value[i]);
|
||||
// }
|
||||
|
||||
// printf("]\n");
|
||||
|
||||
// for(auto& c : clauses) {
|
||||
|
||||
// printf("lits: [ ");
|
||||
// for(auto& lit : c->lits) {
|
||||
// printf("%d ", lit);
|
||||
// }
|
||||
// printf(" ] satifs_cnt: %d\n", c->satisfied_lit_count);
|
||||
|
||||
// }
|
||||
|
||||
lit_value[var] = !lit_value[var];
|
||||
|
||||
for(auto& clause : lit_related_clauses[var]) {
|
||||
@ -89,8 +71,8 @@ void flip(int var) {
|
||||
CC[abs(lit)] = 1;
|
||||
}
|
||||
}
|
||||
CC[var] = 0;
|
||||
|
||||
CC[var] = 0;
|
||||
}
|
||||
|
||||
void add_to_tmp_clause(int x) {
|
||||
|
||||
2
clause.h
2
clause.h
@ -24,6 +24,7 @@ namespace ClauseLS {
|
||||
extern std::vector<Clause*> *lit_related_clauses;
|
||||
extern int *lit_value;
|
||||
extern int *CC;
|
||||
extern int *score;
|
||||
extern std::unordered_set<Clause*> satisfied_clauses;
|
||||
extern std::unordered_set<Clause*> falsified_clauses;
|
||||
|
||||
@ -35,4 +36,5 @@ namespace ClauseLS {
|
||||
void write_cnf();
|
||||
|
||||
void flip(int var);
|
||||
|
||||
}
|
||||
2
crun
2
crun
@ -8,6 +8,6 @@ if [ $? -ne 0 ]; then
|
||||
echo "compile failed."
|
||||
else
|
||||
echo "========================"
|
||||
time ./atpg $1
|
||||
time ./atpg $1 2>&1 | tee output.txt
|
||||
fi
|
||||
|
||||
|
||||
34
ls.cpp
34
ls.cpp
@ -8,6 +8,7 @@
|
||||
#include <chrono>
|
||||
|
||||
#include "clause.h"
|
||||
#include "CCAnr/ccanr.h"
|
||||
|
||||
bool Circuit::local_search() {
|
||||
|
||||
@ -17,14 +18,17 @@ bool Circuit::local_search() {
|
||||
|
||||
ls_init_weight();
|
||||
|
||||
//CCAnr::module_reset();
|
||||
|
||||
ls_random_circuit();
|
||||
|
||||
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, stems.size() - 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();
|
||||
int id = ls_pick();
|
||||
|
||||
ls_flip_var(id);
|
||||
|
||||
@ -33,7 +37,7 @@ bool Circuit::local_search() {
|
||||
break;
|
||||
}
|
||||
|
||||
assert(is_valid_circuit());
|
||||
//assert(is_valid_circuit());
|
||||
|
||||
auto end = std::chrono::system_clock::now();
|
||||
std::chrono::duration<double> elapsed_seconds = end - start;
|
||||
@ -136,7 +140,7 @@ int Circuit::ls_pick() {
|
||||
if(var == -1) {
|
||||
ls_update_weight();
|
||||
|
||||
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("[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());
|
||||
|
||||
if(ClauseLS::falsified_clauses.size() == 0) {
|
||||
print_circuit();
|
||||
@ -150,9 +154,20 @@ int Circuit::ls_pick() {
|
||||
var = abs(lits[rand()%lits.size()]);
|
||||
}
|
||||
|
||||
int var_score = ls_pick_score(var);
|
||||
|
||||
assert(var != -1);
|
||||
|
||||
return var;
|
||||
|
||||
// int ccanr_var = CCAnr::module_pick_var();
|
||||
// int ccanr_score = ls_pick_score(ccanr_var);
|
||||
|
||||
// if(var_score > 0 && rand() % 100 <= 10) {
|
||||
// return var;
|
||||
// } else {
|
||||
// return ccanr_var;
|
||||
// }
|
||||
}
|
||||
|
||||
void Circuit::ls_init_stems() {
|
||||
@ -218,6 +233,7 @@ void Circuit::ls_init_stems() {
|
||||
}
|
||||
|
||||
void Circuit::ls_flip_var(int var) {
|
||||
//CCAnr::module_flip_var(var);
|
||||
ClauseLS::flip(var);
|
||||
|
||||
if(id2gate.count(var) && id2gate[var]->stem) {
|
||||
@ -235,14 +251,14 @@ ll Circuit::ls_pick_score(int var) {
|
||||
|
||||
ls_flip_var(var);
|
||||
|
||||
assert(old_score == ls_circuit_score());
|
||||
//assert(old_score == ls_circuit_score());
|
||||
|
||||
return new_score - old_score;
|
||||
}
|
||||
|
||||
ll Circuit::ls_circuit_score() {
|
||||
//ll score = - Clause::total_cost + fault_propagate_score + fault_total_weight;
|
||||
ll score = - Clause::total_cost;
|
||||
ll score = - Clause::total_cost + fault_propagate_score + fault_total_weight;
|
||||
//ll score = - Clause::total_cost;
|
||||
return score;
|
||||
}
|
||||
|
||||
@ -308,7 +324,7 @@ void Circuit::ls_random_circuit() {
|
||||
|
||||
}
|
||||
|
||||
assert(is_valid_circuit());
|
||||
//assert(is_valid_circuit());
|
||||
}
|
||||
|
||||
void Circuit::ls_reset_data() {
|
||||
@ -341,6 +357,8 @@ void Circuit::ls_reset_data() {
|
||||
|
||||
void Circuit::ls_flip_stem(Gate* stem) {
|
||||
|
||||
printf("flip-stem: %s\n", stem->name.c_str());
|
||||
|
||||
stem->value = !stem->value;
|
||||
|
||||
// update CC
|
||||
|
||||
2
main.cpp
2
main.cpp
@ -4,6 +4,7 @@
|
||||
|
||||
#include "circuit.h"
|
||||
#include "clause.h"
|
||||
#include "CCAnr/ccanr.h"
|
||||
|
||||
int main(int args, char* argv[]) {
|
||||
|
||||
@ -40,7 +41,6 @@ int main(int args, char* argv[]) {
|
||||
printf(" result: %d.\n", is_valid);
|
||||
if(!ls) break;
|
||||
if(!is_valid) break;
|
||||
|
||||
if(circuit->global_fault_undetected_count == 0) break;
|
||||
}
|
||||
|
||||
|
||||
105
makefile
105
makefile
@ -1,72 +1,35 @@
|
||||
#一个实用的makefile，能自动编译当前目录下所有.c/.cpp源文件，支持二者混合编译
|
||||
#并且当某个.c/.cpp、.h或依赖的源文件被修改后，仅重编涉及到的源文件，未涉及的不编译
|
||||
#详解文档：http://blog.csdn.net/huyansoft/article/details/8924624
|
||||
#author：胡彦 2013-5-21
|
||||
|
||||
#----------------------------------------------------------
|
||||
#编译工具用g++，以同时支持C和C++程序，以及二者的混合编译
|
||||
CC=g++
|
||||
# 定义源文件列表
|
||||
SOURCES := $(wildcard *.c) $(wildcard *.cpp)
|
||||
|
||||
CPPFLAGS=-O3 -std=c++17
|
||||
|
||||
#使用$(winldcard *.c)来获取工作目录下的所有.c文件的列表
|
||||
#sources:=main.cpp command.c
|
||||
|
||||
#变量sources得到当前目录下待编译的.c/.cpp文件的列表，两次调用winldcard、结果连在一起即可
|
||||
sources:=$(wildcard *.c) $(wildcard *.cpp) $(wildcard CCAnr/*.cpp)
|
||||
|
||||
#变量objects得到待生成的.o文件的列表，把sources中每个文件的扩展名换成.o即可。这里两次调用patsubst函数，第1次把sources中所有.cpp换成.o，第2次把第1次结果里所有.c换成.o
|
||||
objects:=$(patsubst %.c,%.o,$(patsubst %.cpp,%.o,$(sources)))
|
||||
|
||||
#变量dependence得到待生成的.d文件的列表，把objects中每个扩展名.o换成.d即可。也可写成$(patsubst %.o,%.d,$(objects))
|
||||
dependence:=$(objects:.o=.d)
|
||||
|
||||
#----------------------------------------------------------
|
||||
#当$(objects)列表里所有文件都生成后，便可调用这里的 $(CC) $^ -o $@ 命令生成最终目标all了
|
||||
#把all定义成第1个规则，使得可以把make all命令简写成make
|
||||
atpg: $(objects)
|
||||
$(CC) $(CPPFLAGS) $^ -o $@
|
||||
# @./$@ #编译后立即执行
|
||||
|
||||
#这段使用make的模式规则，指示如何由.c文件生成.o，即对每个.c文件，调用gcc -c XX.c -o XX.o命令生成对应的.o文件
|
||||
#如果不写这段也可以，因为make的隐含规则可以起到同样的效果
|
||||
%.o: %.c
|
||||
$(CC) $(CPPFLAGS) -c $< -o $@
|
||||
|
||||
#同上，指示如何由.cpp生成.o，可省略
|
||||
%.o: %.cpp
|
||||
$(CC) $(CPPFLAGS) -c $< -o $@
|
||||
|
||||
#----------------------------------------------------------
|
||||
include $(dependence) #注意该句要放在终极目标all的规则之后，否则.d文件里的规则会被误当作终极规则了
|
||||
|
||||
#因为这4行命令要多次凋用，定义成命令包以简化书写
|
||||
define gen_dep
|
||||
set -e; rm -f $@; \
|
||||
$(CC) -MM $(CPPFLAGS) $< > $@.$$$$; \
|
||||
sed 's,\($*\)\.o[ :]*,\1.o $@ : ,g' < $@.$$$$ > $@; \
|
||||
rm -f $@.$$$$
|
||||
endef
|
||||
|
||||
#指示如何由.c生成其依赖规则文件.d
|
||||
#这段使用make的模式规则，指示对每个.c文件，如何生成其依赖规则文件.d，调用上面的命令包即可
|
||||
%.d: %.c
|
||||
$(gen_dep)
|
||||
|
||||
#同上，指示对每个.cpp，如何生成其依赖规则文件.d
|
||||
%.d: %.cpp
|
||||
$(gen_dep)
|
||||
|
||||
#----------------------------------------------------------
|
||||
#清除所有临时文件（所有.o和.d）。之所以把clean定义成伪目标，是因为这个目标并不对应实际的文件
|
||||
.PHONY: clean
|
||||
clean: #.$$已在每次使用后立即删除。-f参数表示被删文件不存在时不报错
|
||||
rm -f all $(objects) $(dependence)
|
||||
|
||||
echo: #调试时显示一些变量的值
|
||||
@echo sources=$(sources)
|
||||
@echo objects=$(objects)
|
||||
@echo dependence=$(dependence)
|
||||
@echo CPPFLAGS=$(CPPFLAGS)
|
||||
|
||||
#提醒：当混合编译.c/.cpp时，为了能够在C++程序里调用C函数，必须把每一个要调用的C函数，其声明都包括在extern "C"{}块里面，这样C++链接时才能成功链接它们。
|
||||
# 将源文件列表转换为目标文件列表
|
||||
OBJECTS := $(addprefix build/,$(SOURCES:%=%.o))
|
||||
|
||||
# 声明编译器和编译选项
|
||||
CC := gcc
|
||||
CXX := g++
|
||||
CFLAGS := -Wall -Wextra -MMD -MP
|
||||
CXXFLAGS := -Wall -Wextra -MMD -MP
|
||||
|
||||
# 默认目标，编译所有目标文件
|
||||
atpg: $(OBJECTS)
|
||||
$(CXX) $(CXXFLAGS) $^ -o $@
|
||||
|
||||
# 生成目标文件的规则
|
||||
build/%.o: % | build
|
||||
$(CC) $(CFLAGS) -c $< -o $@
|
||||
|
||||
build/%.o: %.cpp | build
|
||||
$(CXX) $(CXXFLAGS) -c $< -o $@
|
||||
|
||||
# 包含依赖文件
|
||||
-include $(OBJECTS:.o=.d)
|
||||
|
||||
# 如果需要，则递归创建源文件的目录结构
|
||||
build:
|
||||
mkdir -p $(sort $(dir $(OBJECTS)))
|
||||
|
||||
# 清除所有目标文件和build目录
|
||||
clean:
|
||||
rm -rf build $(OBJECTS)
|
||||
|
||||
.PHONY: clean all
|
||||
Loading…
x
Reference in New Issue
Block a user