1 /******************************************
2 Copyright (c) 2016, Yuri Malitsky and Horst Samulowitz
3 Copyright (c) 2018, Mate Soos
4
5 Permission is hereby granted, free of charge, to any person obtaining a copy
6 of this software and associated documentation files (the "Software"), to deal
7 in the Software without restriction, including without limitation the rights
8 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9 copies of the Software, and to permit persons to whom the Software is
10 furnished to do so, subject to the following conditions:
11
12 The above copyright notice and this permission notice shall be included in
13 all copies or substantial portions of the Software.
14
15 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
21 THE SOFTWARE.
22 ***********************************************/
23
24 #include <vector>
25 #include <cmath>
26
27 #include "solver.h"
28 #include "sqlstats.h"
29 #include "satzilla_features_calc.h"
30
31 using std::vector;
32 using namespace CMSat;
33
34 template<class Function, class Function2>
for_one_clause(const Watched & cl,const Lit lit,Function func_each_cl,Function2 func_each_lit) const35 void SatZillaFeaturesCalc::for_one_clause(
36 const Watched& cl
37 , const Lit lit
38 , Function func_each_cl
39 , Function2 func_each_lit
40 ) const {
41 unsigned neg_vars = 0;
42 unsigned pos_vars = 0;
43 unsigned size = 0;
44
45 switch (cl.getType()) {
46 case CMSat::watch_binary_t: {
47 if (cl.red()) {
48 //only irred cls
49 break;
50 }
51 if (lit > cl.lit2()) {
52 //only count once
53 break;
54 }
55
56 pos_vars += !lit.sign();
57 pos_vars += !cl.lit2().sign();
58 size = 2;
59 neg_vars = size - pos_vars;
60 func_each_cl(size, pos_vars, neg_vars);
61 func_each_lit(lit, size, pos_vars, neg_vars);
62 func_each_lit(cl.lit2(), size, pos_vars, neg_vars);
63 break;
64 }
65
66 case CMSat::watch_clause_t: {
67 const Clause& clause = *solver->cl_alloc.ptr(cl.get_offset());
68 if (clause.red()) {
69 //only irred cls
70 break;
71 }
72 if (clause[0] < clause[1]) {
73 //only count once
74 break;
75 }
76
77 for (const Lit cl_lit : clause) {
78 pos_vars += !cl_lit.sign();
79 }
80 size = clause.size();
81 neg_vars = size - pos_vars;
82 func_each_cl(size, pos_vars, neg_vars);
83 for (const Lit cl_lit : clause) {
84 func_each_lit(cl_lit, size, pos_vars, neg_vars);
85 }
86 break;
87 }
88
89 case CMSat::watch_idx_t: {
90 // This should never be here
91 assert(false);
92 exit(-1);
93 break;
94 }
95 }
96 }
97
98 template<class Function, class Function2>
for_all_clauses(Function func_each_cl,Function2 func_each_lit) const99 void SatZillaFeaturesCalc::for_all_clauses(Function func_each_cl, Function2 func_each_lit) const
100 {
101 for (size_t i = 0; i < solver->nVars() * 2; i++) {
102 Lit lit = Lit::toLit(i);
103 for (const Watched & w : solver->watches[lit]) {
104 for_one_clause(w, lit, func_each_cl, func_each_lit);
105 }
106 }
107 }
108
fill_vars_cls()109 void SatZillaFeaturesCalc::fill_vars_cls()
110 {
111 satzilla_feat.numVars = solver->get_num_free_vars();
112 satzilla_feat.numClauses = solver->longIrredCls.size() + solver->binTri.irredBins;
113 myVars.resize(solver->nVars());
114
115 auto func_each_cl = [&](unsigned /*size*/, unsigned pos_vars, unsigned /*neg_vars*/) -> bool {
116 if (pos_vars <= 1 ) {
117 satzilla_feat.horn += 1;
118 return true;
119 }
120 return false;
121 };
122 auto func_each_lit = [&](Lit lit, unsigned /*size*/, unsigned pos_vars, unsigned /*neg_vars*/) -> void {
123 if (pos_vars <= 1 ) {
124 myVars[lit.var()].horn++;
125 }
126
127 if (!lit.sign()) {
128 myVars[lit.var()].numPos++;
129 }
130 myVars[lit.var()].size++;
131 };
132 for_all_clauses(func_each_cl, func_each_lit);
133 }
134
calculate_clause_stats()135 void SatZillaFeaturesCalc::calculate_clause_stats()
136 {
137 auto empty_func = [](const Lit, unsigned /*size*/, unsigned /*pos_vars*/, unsigned /*neg_vars*/) -> void {};
138 auto func_each_cl = [&](unsigned size, unsigned pos_vars, unsigned /*neg_vars*/) -> void {
139 if (size == 0 ) {
140 return;
141 }
142
143 double _size = (double)size / (double)satzilla_feat.numVars;
144 satzilla_feat.vcg_cls_min = std::min(satzilla_feat.vcg_cls_min, _size);
145 satzilla_feat.vcg_cls_max = std::max(satzilla_feat.vcg_cls_max, _size);
146 satzilla_feat.vcg_cls_mean += _size;
147
148 double _pnr = 0.5 + ((2.0 * (double)pos_vars - (double)size) / (2.0 * (double)size));
149 satzilla_feat.pnr_cls_min = std::min(satzilla_feat.pnr_cls_min, _pnr);
150 satzilla_feat.pnr_cls_max = std::max(satzilla_feat.pnr_cls_max, _pnr);
151 satzilla_feat.pnr_cls_mean += _pnr;
152 };
153 for_all_clauses(func_each_cl, empty_func);
154
155 satzilla_feat.vcg_cls_mean /= (double)satzilla_feat.numClauses;
156 satzilla_feat.pnr_cls_mean /= (double)satzilla_feat.numClauses;
157 satzilla_feat.horn /= (double)satzilla_feat.numClauses;
158 satzilla_feat.binary = float_div(solver->binTri.irredBins, satzilla_feat.numClauses);
159
160 satzilla_feat.vcg_cls_spread = satzilla_feat.vcg_cls_max - satzilla_feat.vcg_cls_min;
161 satzilla_feat.pnr_cls_spread = satzilla_feat.pnr_cls_max - satzilla_feat.pnr_cls_min;
162 }
163
calculate_variable_stats()164 void SatZillaFeaturesCalc::calculate_variable_stats()
165 {
166 if (satzilla_feat.numVars == 0)
167 return;
168
169 for ( int vv = 0; vv < (int)myVars.size(); vv++ ) {
170 if ( myVars[vv].size == 0 ) {
171 continue;
172 }
173
174 double _size = myVars[vv].size / (double)satzilla_feat.numClauses;
175 satzilla_feat.vcg_var_min = std::min(satzilla_feat.vcg_var_min, _size);
176 satzilla_feat.vcg_var_max = std::max(satzilla_feat.vcg_var_max, _size);
177 satzilla_feat.vcg_var_mean += _size;
178
179 double _pnr = 0.5 + ((2.0 * myVars[vv].numPos - myVars[vv].size)
180 / (2.0 * myVars[vv].size));
181 satzilla_feat.pnr_var_min = std::min(satzilla_feat.pnr_var_min, _pnr);
182 satzilla_feat.pnr_var_max = std::max(satzilla_feat.pnr_var_max, _pnr);
183 satzilla_feat.pnr_var_mean += _pnr;
184
185 double _horn = myVars[vv].horn / (double)satzilla_feat.numClauses;
186 satzilla_feat.horn_min = std::min(satzilla_feat.horn_min, _horn);
187 satzilla_feat.horn_max = std::max(satzilla_feat.horn_max, _horn);
188 satzilla_feat.horn_mean += _horn;
189 }
190
191 if (satzilla_feat.vcg_var_mean > 0) {
192 satzilla_feat.vcg_var_mean /= (double)satzilla_feat.numVars;
193 }
194 if (satzilla_feat.pnr_var_mean > 0) {
195 satzilla_feat.pnr_var_mean /= (double)satzilla_feat.numVars;
196 }
197 if (satzilla_feat.horn_mean > 0) {
198 satzilla_feat.horn_mean /= (double)satzilla_feat.numVars;
199 }
200
201 satzilla_feat.vcg_var_spread = satzilla_feat.vcg_var_max - satzilla_feat.vcg_var_min;
202 satzilla_feat.pnr_var_spread = satzilla_feat.pnr_var_max - satzilla_feat.pnr_var_min;
203 satzilla_feat.horn_spread = satzilla_feat.horn_max - satzilla_feat.horn_min;
204 }
205
calculate_extra_clause_stats()206 void SatZillaFeaturesCalc::calculate_extra_clause_stats()
207 {
208 auto empty_func = [](const Lit, unsigned /*size*/, unsigned /*pos_vars*/, unsigned /*neg_vars*/) -> void {};
209 auto each_clause = [&](unsigned size, unsigned pos_vars, unsigned /*neg_vars*/) -> void {
210 if ( size == 0 ) {
211 return;
212 }
213
214 double _size = (double)size / (double)satzilla_feat.numVars;
215 satzilla_feat.vcg_cls_std += (satzilla_feat.vcg_cls_mean - _size) * (satzilla_feat.vcg_cls_mean - _size);
216
217 double _pnr = 0.5 + ((2.0 * (double)pos_vars - (double)size) / (2.0 * (double)size));
218 satzilla_feat.pnr_cls_std += (satzilla_feat.pnr_cls_mean - _pnr) * (satzilla_feat.pnr_cls_mean - _pnr);
219 };
220 for_all_clauses(each_clause, empty_func);
221
222 if ( satzilla_feat.vcg_cls_std > satzilla_feat.eps && satzilla_feat.vcg_cls_mean > satzilla_feat.eps ) {
223 satzilla_feat.vcg_cls_std = std::sqrt(satzilla_feat.vcg_cls_std / (double)satzilla_feat.numClauses) / satzilla_feat.vcg_cls_mean;
224 } else {
225 satzilla_feat.vcg_cls_std = 0;
226 }
227 if ( satzilla_feat.pnr_cls_std > satzilla_feat.eps && satzilla_feat.pnr_cls_mean > satzilla_feat.eps ) {
228 satzilla_feat.pnr_cls_std = std::sqrt(satzilla_feat.pnr_cls_std / (double)satzilla_feat.numClauses) / satzilla_feat.pnr_cls_mean;
229 } else {
230 satzilla_feat.pnr_cls_std = 0;
231 }
232 }
233
calculate_extra_var_stats()234 void SatZillaFeaturesCalc::calculate_extra_var_stats()
235 {
236 if (satzilla_feat.numVars == 0)
237 return;
238
239 for ( int vv = 0; vv < (int)myVars.size(); vv++ ) {
240 if ( myVars[vv].size == 0 ) {
241 continue;
242 }
243
244 double _size = myVars[vv].size / (double)satzilla_feat.numClauses;
245 satzilla_feat.vcg_var_std += (satzilla_feat.vcg_var_mean - _size) * (satzilla_feat.vcg_var_mean - _size);
246
247 double _pnr = 0.5 + ((2.0 * myVars[vv].numPos - myVars[vv].size) / (2.0 * myVars[vv].size));
248 satzilla_feat.pnr_var_std += (satzilla_feat.pnr_var_mean - _pnr) * (satzilla_feat.pnr_var_mean - _pnr);
249
250 double _horn = myVars[vv].horn / (double)satzilla_feat.numClauses;
251 satzilla_feat.horn_std += (satzilla_feat.horn_mean - _horn) * (satzilla_feat.horn_mean - _horn);
252 }
253 if ( satzilla_feat.vcg_var_std > satzilla_feat.eps && satzilla_feat.vcg_var_mean > satzilla_feat.eps ) {
254 satzilla_feat.vcg_var_std = std::sqrt(satzilla_feat.vcg_var_std / (double)satzilla_feat.numVars) / satzilla_feat.vcg_var_mean;
255 } else {
256 satzilla_feat.vcg_var_std = 0;
257 }
258
259 if ( satzilla_feat.pnr_var_std > satzilla_feat.eps && satzilla_feat.pnr_var_mean > satzilla_feat.eps
260 && satzilla_feat.pnr_var_mean != 0
261 ) {
262 satzilla_feat.pnr_var_std = std::sqrt(satzilla_feat.pnr_var_std / (double)satzilla_feat.numVars) / satzilla_feat.pnr_var_mean;
263 } else {
264 satzilla_feat.pnr_var_std = 0;
265 }
266
267 if ( satzilla_feat.horn_std / (double)satzilla_feat.numVars > satzilla_feat.eps && satzilla_feat.horn_mean > satzilla_feat.eps
268 && satzilla_feat.horn_mean != 0
269 ) {
270 satzilla_feat.horn_std = std::sqrt(satzilla_feat.horn_std / (double)satzilla_feat.numVars) / satzilla_feat.horn_mean;
271 } else {
272 satzilla_feat.horn_std = 0;
273 }
274 }
275
calculate_cl_distributions(const vector<ClOffset> & clauses,struct SatZillaFeatures::Distrib & distrib_data)276 void SatZillaFeaturesCalc::calculate_cl_distributions(
277 const vector<ClOffset>& clauses
278 , struct SatZillaFeatures::Distrib& distrib_data
279 ) {
280 if (clauses.empty()) {
281 return;
282 }
283
284 double glue_mean = 0;
285 double glue_var = 0;
286
287 double size_mean = 0;
288 double size_var = 0;
289
290 double activity_mean = 0;
291 double activity_var = 0;
292
293 //Calculate means
294 double cla_inc = solver->get_cla_inc();
295 for(ClOffset off: clauses)
296 {
297 const Clause& cl = *solver->cl_alloc.ptr(off);
298 size_mean += cl.size();
299 glue_mean += cl.stats.glue;
300 if (cl.red()) {
301 activity_mean += (double)cl.stats.activity/cla_inc;
302 }
303 }
304 size_mean /= clauses.size();
305 glue_mean /= clauses.size();
306 activity_mean /= clauses.size();
307
308 //Calculate variances
309 for(ClOffset off: clauses)
310 {
311 const Clause& cl = *solver->cl_alloc.ptr(off);
312 size_var += std::pow(size_mean-cl.size(), 2);
313 glue_var += std::pow(glue_mean-cl.stats.glue, 2);
314 activity_var += std::pow(activity_mean-(double)cl.stats.activity/cla_inc, 2);
315 }
316 size_var /= clauses.size();
317 glue_var /= clauses.size();
318 activity_var /= clauses.size();
319
320 //Assign calculated values
321 distrib_data.glue_distr_mean = glue_mean;
322 distrib_data.glue_distr_var = glue_var;
323 distrib_data.size_distr_mean = size_mean;
324 distrib_data.size_distr_var = size_var;
325 distrib_data.activity_distr_mean = activity_mean;
326 distrib_data.activity_distr_var = activity_var;
327 }
328
normalise_values()329 void SatZillaFeaturesCalc::normalise_values()
330 {
331 if (satzilla_feat.vcg_var_min == std::numeric_limits<double>::max())
332 satzilla_feat.vcg_var_min = -1;
333 if (satzilla_feat.vcg_var_max == std::numeric_limits<double>::min())
334 satzilla_feat.vcg_var_max = -1;
335
336 if (satzilla_feat.vcg_cls_min == std::numeric_limits<double>::max())
337 satzilla_feat.vcg_cls_min = -1;
338 if (satzilla_feat.vcg_cls_max == std::numeric_limits<double>::min())
339 satzilla_feat.vcg_cls_max = -1;
340
341 if (satzilla_feat.pnr_var_min == std::numeric_limits<double>::max())
342 satzilla_feat.pnr_var_min = -1;
343 if (satzilla_feat.pnr_var_max == std::numeric_limits<double>::min())
344 satzilla_feat.pnr_var_max = -1;
345
346 if (satzilla_feat.horn_min == std::numeric_limits<double>::max())
347 satzilla_feat.horn_min = -1;
348 if (satzilla_feat.horn_max == std::numeric_limits<double>::min())
349 satzilla_feat.horn_max = -1;
350
351 if (satzilla_feat.pnr_cls_min == std::numeric_limits<double>::max())
352 satzilla_feat.pnr_cls_min = -1;
353 if (satzilla_feat.pnr_cls_max == std::numeric_limits<double>::min())
354 satzilla_feat.pnr_cls_max = -1;
355 }
356
extract()357 SatZillaFeatures SatZillaFeaturesCalc::extract()
358 {
359 double start_time = cpuTime();
360 fill_vars_cls();
361
362 satzilla_feat.numVars = 0;
363 for ( int vv = 0; vv < (int)myVars.size(); vv++ ) {
364 if ( myVars[vv].size > 0 ) {
365 satzilla_feat.numVars++;
366 }
367 }
368 if (satzilla_feat.numVars > 0 && satzilla_feat.numClauses > 0) {
369 satzilla_feat.var_cl_ratio = (double)satzilla_feat.numVars/ (double)satzilla_feat.numClauses;
370 }
371
372 if (satzilla_feat.numClauses > 0 && satzilla_feat.numVars > 0) {
373 calculate_clause_stats();
374 calculate_variable_stats();
375
376 calculate_extra_clause_stats();
377 calculate_extra_var_stats();
378
379 if (!solver->longRedCls[0].empty()) {
380 calculate_cl_distributions(solver->longRedCls[0], satzilla_feat.red_cl_distrib);
381 }
382 if (!solver->longIrredCls.empty()) {
383 calculate_cl_distributions(solver->longIrredCls, satzilla_feat.irred_cl_distrib);
384 }
385 }
386 normalise_values();
387
388 double time_used = cpuTime() - start_time;
389 if (solver->conf.verbosity) {
390 cout << "c [szfeat] satzilla features extracted "
391 << solver->conf.print_times(time_used)
392 << endl;
393 }
394
395 if (solver->sqlStats) {
396 solver->sqlStats->time_passed_min(
397 solver
398 , "satzilla"
399 , time_used
400 );
401 }
402
403 return satzilla_feat;
404 }
405