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