1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #include "distillerlong.h"
24 #include "clausecleaner.h"
25 #include "time_mem.h"
26 #include "solver.h"
27 #include "watchalgos.h"
28 #include "clauseallocator.h"
29 #include "sqlstats.h"
30
31 #include <iomanip>
32 using namespace CMSat;
33 using std::cout;
34 using std::endl;
35
36 #ifdef VERBOSE_DEBUG
37 #define VERBOSE_SUBSUME_NONEXIST
38 #endif
39
40 //#define VERBOSE_SUBSUME_NONEXIST
41
DistillerLong(Solver * _solver)42 DistillerLong::DistillerLong(Solver* _solver) :
43 solver(_solver)
44 {}
45
distill(const bool red,bool fullstats)46 bool DistillerLong::distill(const bool red, bool fullstats)
47 {
48 assert(solver->ok);
49 numCalls++;
50 Stats other;
51
52
53 if (!red) {
54 runStats.clear();
55 if (!distill_long_cls_all(solver->longIrredCls, 1)) {
56 goto end;
57 }
58 other = runStats;
59 } else {
60 runStats.clear();
61 if (!distill_long_cls_all(solver->longRedCls[0], 10.0)) {
62 goto end;
63 }
64 runStats.clear();
65 if (!distill_long_cls_all(solver->longRedCls[1], solver->conf.distill_red_tier1_ratio)) {
66 goto end;
67 }
68 }
69
70 end:
71 runStats += other;
72 globalStats += runStats;
73 if (solver->conf.verbosity && fullstats) {
74 if (solver->conf.verbosity >= 3)
75 runStats.print(solver->nVars());
76 else
77 runStats.print_short(solver);
78 }
79 runStats.clear();
80
81 return solver->okay();
82 }
83
84 struct ClauseSizeSorterInv
85 {
ClauseSizeSorterInvClauseSizeSorterInv86 ClauseSizeSorterInv(const ClauseAllocator& _cl_alloc) :
87 cl_alloc(_cl_alloc)
88 {}
89
90 const ClauseAllocator& cl_alloc;
91
operator ()ClauseSizeSorterInv92 bool operator()(const ClOffset off1, const ClOffset off2) const
93 {
94 const Clause* cl1 = cl_alloc.ptr(off1);
95 const Clause* cl2 = cl_alloc.ptr(off2);
96
97 return cl1->size() > cl2->size();
98 }
99 };
100
go_through_clauses(vector<ClOffset> & cls)101 bool DistillerLong::go_through_clauses(
102 vector<ClOffset>& cls
103 ) {
104 bool time_out = false;
105 vector<ClOffset>::iterator i, j;
106 i = j = cls.begin();
107 for (vector<ClOffset>::iterator end = cls.end()
108 ; i != end
109 ; i++
110 ) {
111 //Check if we are in state where we only copy offsets around
112 if (time_out || !solver->ok) {
113 *j++ = *i;
114 continue;
115 }
116
117 //if done enough, stop doing it
118 if ((int64_t)solver->propStats.bogoProps-(int64_t)oldBogoProps >= maxNumProps
119 || solver->must_interrupt_asap()
120 ) {
121 if (solver->conf.verbosity >= 3) {
122 cout
123 << "c Need to finish distillation -- ran out of prop (=allocated time)"
124 << endl;
125 }
126 runStats.timeOut++;
127 time_out = true;
128 }
129
130 //Get pointer
131 ClOffset offset = *i;
132 ClOffset offset2;
133 Clause& cl = *solver->cl_alloc.ptr(offset);
134 if (cl.used_in_xor() &&
135 solver->conf.force_preserve_xors
136 ) {
137 offset2 = offset;
138 goto copy;
139 }
140
141 //Time to dereference
142 maxNumProps -= 5;
143
144 //If we already tried this clause, then move to next
145 if (cl.getdistilled() || cl._xor_is_detached) {
146 *j++ = *i;
147 continue;
148 }
149 cl.set_distilled(true);
150 runStats.checkedClauses++;
151 assert(cl.size() > 2);
152
153 //we will detach the clause no matter what
154 maxNumProps -= solver->watches[cl[0]].size();
155 maxNumProps -= solver->watches[cl[1]].size();
156
157 maxNumProps -= cl.size();
158 if (solver->satisfied_cl(cl)) {
159 solver->detachClause(cl);
160 solver->free_cl(&cl);
161 continue;
162 }
163
164 //Try to distill clause
165 offset2 = try_distill_clause_and_return_new(
166 offset
167 , cl.red()
168 , cl.stats
169 );
170
171 copy:
172 if (offset2 != CL_OFFSET_MAX) {
173 *j++ = offset2;
174 }
175 }
176 cls.resize(cls.size()- (i-j));
177
178 return time_out;
179 }
180
distill_long_cls_all(vector<ClOffset> & offs,double time_mult)181 bool DistillerLong::distill_long_cls_all(
182 vector<ClOffset>& offs
183 , double time_mult
184 ) {
185 assert(solver->ok);
186 if (time_mult == 0.0) {
187 return solver->okay();
188 }
189
190 if (solver->conf.verbosity >= 6) {
191 cout
192 << "c Doing distillation branch for long clauses"
193 << endl;
194 }
195
196 double myTime = cpuTime();
197 const size_t origTrailSize = solver->trail_size();
198
199 //Time-limiting
200 maxNumProps =
201 solver->conf.distill_long_cls_time_limitM*1000LL*1000ULL
202 *solver->conf.global_timeout_multiplier;
203
204 if (solver->litStats.irredLits + solver->litStats.redLits <
205 (500ULL*1000ULL*solver->conf.var_and_mem_out_mult)
206 ) {
207 maxNumProps *=2;
208 }
209 maxNumProps *= time_mult;
210 orig_maxNumProps = maxNumProps;
211
212 //stats setup
213 oldBogoProps = solver->propStats.bogoProps;
214 runStats.potentialClauses += offs.size();
215 runStats.numCalled += 1;
216
217 /*std::sort(offs.begin()
218 , offs.end()
219 , ClauseSizeSorterInv(solver->cl_alloc)
220 );*/
221
222 bool time_out = go_through_clauses(offs);
223
224 const double time_used = cpuTime() - myTime;
225 const double time_remain = float_div(
226 maxNumProps - ((int64_t)solver->propStats.bogoProps-(int64_t)oldBogoProps),
227 orig_maxNumProps);
228 if (solver->conf.verbosity >= 2) {
229 cout << "c [distill] long cls"
230 << " tried: " << runStats.checkedClauses << "/" << offs.size()
231 << " cl-short:" << runStats.numClShorten
232 << " lit-r:" << runStats.numLitsRem
233 << solver->conf.print_times(time_used, time_out, time_remain)
234 << endl;
235 }
236 if (solver->sqlStats) {
237 solver->sqlStats->time_passed(
238 solver
239 , "distill long cls"
240 , time_used
241 , time_out
242 , time_remain
243 );
244 }
245
246 //Update stats
247 runStats.time_used += cpuTime() - myTime;
248 runStats.zeroDepthAssigns += solver->trail_size() - origTrailSize;
249
250 return solver->okay();
251 }
252
try_distill_clause_and_return_new(ClOffset offset,const bool red,const ClauseStats & stats)253 ClOffset DistillerLong::try_distill_clause_and_return_new(
254 ClOffset offset
255 , const bool red
256 , const ClauseStats& stats
257 ) {
258 #ifdef DRAT_DEBUG
259 if (solver->conf.verbosity >= 6) {
260 cout << "Trying to distill clause:" << lits << endl;
261 }
262 #endif
263
264 //Try to enqueue the literals in 'queueByBy' amounts and see if we fail
265 solver->detachClause(offset, false);
266 Clause& cl = *solver->cl_alloc.ptr(offset);
267 (*solver->drat) << deldelay << cl << fin;
268
269 uint32_t orig_size = cl.size();
270 uint32_t i = 0;
271 uint32_t j = 0;
272 for (uint32_t sz = cl.size(); i < sz; i++) {
273 if (solver->value(cl[i]) != l_False) {
274 cl[j++] = cl[i];
275 }
276 }
277 cl.resize(j);
278
279 solver->new_decision_level();
280 bool True_confl = false;
281 PropBy confl;
282 i = 0;
283 j = 0;
284 for (uint32_t sz = cl.size(); i < sz; i++) {
285 const Lit lit = cl[i];
286 lbool val = solver->value(lit);
287 if (val == l_Undef) {
288 solver->enqueue(~lit);
289 cl[j++] = cl[i];
290
291 maxNumProps -= 5;
292 confl = solver->propagate<true>();
293 if (!confl.isNULL()) {
294 break;
295 }
296 } else if (val == l_False) {
297 // skip
298 } else {
299 assert(val == l_True);
300 cl[j++] = cl[i];
301 True_confl = true;
302 confl = solver->varData[cl[i].var()].reason;
303 break;
304 }
305 }
306 assert(solver->ok);
307 cl.resize(j);
308
309 //Couldn't simplify the clause
310 if (j == orig_size && !True_confl && confl.isNULL()) {
311 solver->cancelUntil<false, true>(0);
312 solver->attachClause(cl);
313 solver->drat->forget_delay();
314 return offset;
315 }
316
317 #ifdef VERBOSE_DEBUG
318 if (j < i && solver->conf.verbosity >= 5) {
319 cout
320 << "c Distillation branch effective." << endl
321 << "c --> shortened cl:" << cl<< endl
322 << "c --> orig size:" << orig_size << endl
323 << "c --> new size:" << j << endl;
324 }
325 #endif
326
327 bool lits_set = false;
328 if (red && j > 1 && (!confl.isNULL() || True_confl)) {
329 #ifdef VERBOSE_DEBUG
330 if (solver->conf.verbosity >= 5) {
331 cout
332 << "c Distillation even more effective." << endl
333 << "c --> orig shortened cl:" << cl << endl;
334 }
335 #endif
336 maxNumProps -= 20;
337 lits.clear();
338 if (True_confl) {
339 lits.push_back(cl[cl.size()-1]);
340 }
341 solver->simple_create_learnt_clause(confl, lits, True_confl);
342 if (lits.size() < cl.size()) {
343 #ifdef VERBOSE_DEBUG
344 if (solver->conf.verbosity >= 5) {
345 cout
346 << "c --> more shortened cl:" << lits << endl;
347 }
348 #endif
349 lits_set = true;
350 }
351 }
352 solver->cancelUntil<false, true>(0);
353 runStats.numLitsRem += orig_size - cl.size();
354 runStats.numClShorten++;
355
356 //Make new clause
357 if (!lits_set) {
358 lits.resize(cl.size());
359 std::copy(cl.begin(), cl.end(), lits.begin());
360 }
361 solver->free_cl(offset);
362 Clause *cl2 = solver->add_clause_int(lits, red, stats);
363 (*solver->drat) << findelay;
364
365 if (cl2 != NULL) {
366 cl2->set_distilled(true);
367 return solver->cl_alloc.get_offset(cl2);
368 } else {
369 //it became a bin/unit/zero
370 return CL_OFFSET_MAX;
371 }
372 }
373
operator +=(const Stats & other)374 DistillerLong::Stats& DistillerLong::Stats::operator+=(const Stats& other)
375 {
376 time_used += other.time_used;
377 timeOut += other.timeOut;
378 zeroDepthAssigns += other.zeroDepthAssigns;
379 numClShorten += other.numClShorten;
380 numLitsRem += other.numLitsRem;
381 checkedClauses += other.checkedClauses;
382 potentialClauses += other.potentialClauses;
383 numCalled += other.numCalled;
384
385 return *this;
386 }
387
print_short(const Solver * _solver) const388 void DistillerLong::Stats::print_short(const Solver* _solver) const
389 {
390 cout
391 << "c [distill] long"
392 << " useful: "<< numClShorten
393 << "/" << checkedClauses << "/" << potentialClauses
394 << " lits-rem: " << numLitsRem
395 << " 0-depth-assigns: " << zeroDepthAssigns
396 << _solver->conf.print_times(time_used, timeOut)
397 << endl;
398 }
399
print(const size_t nVars) const400 void DistillerLong::Stats::print(const size_t nVars) const
401 {
402 cout << "c -------- DISTILL STATS --------" << endl;
403 print_stats_line("c time"
404 , time_used
405 , ratio_for_stat(time_used, numCalled)
406 , "per call"
407 );
408
409 print_stats_line("c timed out"
410 , timeOut
411 , stats_line_percent(timeOut, numCalled)
412 , "% of calls"
413 );
414
415 print_stats_line("c distill/checked/potential"
416 , numClShorten
417 , checkedClauses
418 , potentialClauses
419 );
420
421 print_stats_line("c lits-rem",
422 numLitsRem
423 );
424 print_stats_line("c 0-depth-assigns",
425 zeroDepthAssigns
426 , stats_line_percent(zeroDepthAssigns, nVars)
427 , "% of vars"
428 );
429 cout << "c -------- DISTILL STATS END --------" << endl;
430 }
431
mem_used() const432 double DistillerLong::mem_used() const
433 {
434 double mem_used = sizeof(DistillerLong);
435 mem_used += lits.size()*sizeof(Lit);
436 return mem_used;
437 }
438