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 "subsumestrengthen.h"
24 #include "occsimplifier.h"
25 #include "solver.h"
26 #include "watchalgos.h"
27 #include "clauseallocator.h"
28 #include "sqlstats.h"
29 #include "solver.h"
30 #include "solvertypes.h"
31 #include "subsumeimplicit.h"
32 #include <array>
33
34 //#define VERBOSE_DEBUG
35
36 using namespace CMSat;
37
SubsumeStrengthen(OccSimplifier * _simplifier,Solver * _solver)38 SubsumeStrengthen::SubsumeStrengthen(
39 OccSimplifier* _simplifier
40 , Solver* _solver
41 ) :
42 simplifier(_simplifier)
43 , solver(_solver)
44 {
45 }
46
subsume_and_unlink_and_markirred(const ClOffset offset)47 uint32_t SubsumeStrengthen::subsume_and_unlink_and_markirred(const ClOffset offset)
48 {
49 Clause& cl = *solver->cl_alloc.ptr(offset);
50 assert(!cl.getRemoved());
51 assert(!cl.freed());
52
53 #ifdef VERBOSE_DEBUG
54 cout << "subsume-ing with clause: " << cl << endl;
55 #endif
56
57 Sub0Ret ret = subsume_and_unlink(
58 offset
59 , cl
60 , cl.abst
61 );
62
63 //If irred is subsumed by redundant, make the redundant into irred
64 if (cl.red()
65 && ret.subsumedIrred
66 ) {
67 #ifdef STATS_NEEDED
68 solver->stats_del_cl(&cl);
69 #endif
70 cl.makeIrred();
71 solver->litStats.redLits -= cl.size();
72 solver->litStats.irredLits += cl.size();
73 if (!cl.getOccurLinked()) {
74 simplifier->linkInClause(cl);
75 } else {
76 for(const Lit l: cl) {
77 simplifier->n_occurs[l.toInt()]++;
78 }
79 }
80 }
81
82 //Combine stats
83 cl.combineStats(ret.stats);
84
85 return ret.numSubsumed;
86 }
87 template SubsumeStrengthen::Sub0Ret SubsumeStrengthen::subsume_and_unlink(
88 const ClOffset offset
89 , const vector<Lit>& ps
90 , const cl_abst_type abs
91 , const bool removeImplicit
92 );
93
94 /**
95 @brief Backward-subsumption using given clause
96 */
97 template<class T>
subsume_and_unlink(const ClOffset offset,const T & ps,const cl_abst_type abs,const bool removeImplicit)98 SubsumeStrengthen::Sub0Ret SubsumeStrengthen::subsume_and_unlink(
99 const ClOffset offset
100 , const T& ps
101 , const cl_abst_type abs
102 , const bool removeImplicit
103 ) {
104 Sub0Ret ret;
105
106 subs.clear();
107 find_subsumed(offset, ps, abs, subs, removeImplicit);
108
109 //Go through each clause that can be subsumed
110 for (const ClOffset offs: subs) {
111 Clause *tmp = solver->cl_alloc.ptr(offs);
112 ret.stats = ClauseStats::combineStats(tmp->stats, ret.stats);
113 #ifdef VERBOSE_DEBUG
114 cout << "-> subsume removing:" << *tmp << endl;
115 #endif
116
117 if (!tmp->red()) {
118 ret.subsumedIrred = true;
119 }
120
121 simplifier->unlink_clause(offs, true, false, true);
122 ret.numSubsumed++;
123
124 //If we are waaay over time, just exit
125 if (*simplifier->limit_to_decrease < -20LL*1000LL*1000LL)
126 break;
127 }
128
129 return ret;
130 }
131
strengthen_subsume_and_unlink_and_markirred(const ClOffset offset)132 SubsumeStrengthen::Sub1Ret SubsumeStrengthen::strengthen_subsume_and_unlink_and_markirred(const ClOffset offset)
133 {
134 subs.clear();
135 subsLits.clear();
136 Sub1Ret ret;
137 Clause& cl = *solver->cl_alloc.ptr(offset);
138 assert(!cl.getRemoved());
139 assert(!cl.freed());
140
141 if (solver->conf.verbosity >= 6)
142 cout << "strengthen_subsume_and_unlink_and_markirred-ing with clause:" << cl << endl;
143
144 findStrengthened(
145 offset
146 , cl
147 , cl.abst
148 , subs
149 , subsLits
150 );
151
152 for (size_t j = 0
153 ; j < subs.size() && solver->okay()
154 ; j++
155 ) {
156 ClOffset offset2 = subs[j];
157 Clause& cl2 = *solver->cl_alloc.ptr(offset2);
158 #ifdef USE_GAUSS
159 if (cl2.used_in_xor() &&
160 solver->conf.force_preserve_xors)
161 {
162 continue;
163 }
164 #endif
165
166 if (subsLits[j] == lit_Undef) { //Subsume
167 #ifdef VERBOSE_DEBUG
168 if (solver->conf.verbosity >= 6)
169 cout << "subsumed clause " << cl2 << endl;
170 #endif
171
172 //If subsumes a irred, and is redundant, make it irred
173 if (cl.red()
174 && !cl2.red()
175 ) {
176 #ifdef STATS_NEEDED
177 solver->stats_del_cl(&cl);
178 #endif
179 cl.makeIrred();
180 solver->litStats.redLits -= cl.size();
181 solver->litStats.irredLits += cl.size();
182 if (!cl.getOccurLinked()) {
183 simplifier->linkInClause(cl);
184 } else {
185 for(const Lit l: cl) {
186 simplifier->n_occurs[l.toInt()]++;
187 }
188 }
189 }
190
191 //Update stats
192 cl.combineStats(cl2.stats);
193
194 simplifier->unlink_clause(offset2, true, false, true);
195 ret.sub++;
196 } else { //Strengthen
197 #ifdef VERBOSE_DEBUG
198 if (solver->conf.verbosity >= 6) {
199 cout << "strenghtened clause " << cl2 << endl;
200 }
201 #endif
202 #ifdef USE_GAUSS
203 if (cl2.used_in_xor() &&
204 solver->conf.force_preserve_xors)
205 {
206 continue;
207 }
208 #endif
209 remove_literal(offset2, subsLits[j]);
210
211 ret.str++;
212 if (!solver->ok)
213 return ret;
214
215 //If we are waaay over time, just exit
216 if (*simplifier->limit_to_decrease < -20LL*1000LL*1000LL)
217 break;
218 }
219 }
220
221 return ret;
222 }
223
randomise_clauses_order()224 void SubsumeStrengthen::randomise_clauses_order()
225 {
226 const size_t sz = simplifier->clauses.size();
227 for (size_t i = 0
228 ; i + 1 < sz
229 ; i++
230 ) {
231 std::swap(
232 simplifier->clauses[i]
233 , simplifier->clauses[i+solver->mtrand.randInt(simplifier->clauses.size()-1-i)]
234 );
235 }
236 }
237
backw_sub_long_with_long()238 void SubsumeStrengthen::backw_sub_long_with_long()
239 {
240 //If clauses are empty, the system below segfaults
241 if (simplifier->clauses.empty())
242 return;
243
244 double myTime = cpuTime();
245 size_t wenThrough = 0;
246 size_t subsumed = 0;
247 const int64_t orig_limit = simplifier->subsumption_time_limit;
248 randomise_clauses_order();
249 const size_t max_go_through =
250 solver->conf.subsume_gothrough_multip*(double)simplifier->clauses.size();
251
252 while (*simplifier->limit_to_decrease > 0
253 && wenThrough < max_go_through
254 ) {
255 *simplifier->limit_to_decrease -= 3;
256 wenThrough++;
257
258 //Print status
259 if (solver->conf.verbosity >= 5
260 && wenThrough % 10000 == 0
261 ) {
262 cout << "toDecrease: " << *simplifier->limit_to_decrease << endl;
263 }
264
265 const size_t at = wenThrough % simplifier->clauses.size();
266 const ClOffset offset = simplifier->clauses[at];
267 Clause* cl = solver->cl_alloc.ptr(offset);
268
269 //Has already been removed
270 if (cl->freed() || cl->getRemoved())
271 continue;
272
273
274 *simplifier->limit_to_decrease -= 10;
275 subsumed += subsume_and_unlink_and_markirred(offset);
276 }
277
278 const double time_used = cpuTime() - myTime;
279 const bool time_out = (*simplifier->limit_to_decrease <= 0);
280 const double time_remain = float_div(*simplifier->limit_to_decrease, orig_limit);
281 if (solver->conf.verbosity) {
282 cout
283 << "c [occ-sub-long-w-long] rem cl: " << subsumed
284 << " tried: " << wenThrough << "/" << simplifier->clauses.size()
285 << " (" << std::setprecision(1) << std::fixed
286 << stats_line_percent(wenThrough, simplifier->clauses.size())
287 << "%)"
288 << solver->conf.print_times(time_used, time_out, time_remain)
289 << endl;
290 }
291 if (solver->sqlStats) {
292 solver->sqlStats->time_passed(
293 solver
294 , "occ-sub-long-w-long"
295 , time_used
296 , time_out
297 , time_remain
298 );
299 }
300
301 //Update time used
302 runStats.subsumedBySub += subsumed;
303 runStats.subsumeTime += cpuTime() - myTime;
304 }
305
backw_str_long_with_long()306 bool SubsumeStrengthen::backw_str_long_with_long()
307 {
308 assert(solver->ok);
309
310 double myTime = cpuTime();
311 size_t wenThrough = 0;
312 const int64_t orig_limit = *simplifier->limit_to_decrease;
313 Sub1Ret ret;
314
315 randomise_clauses_order();
316 while(*simplifier->limit_to_decrease > 0
317 && wenThrough < 1.5*(double)2*simplifier->clauses.size()
318 && solver->okay()
319 ) {
320 *simplifier->limit_to_decrease -= 10;
321 wenThrough++;
322
323 //Print status
324 if (solver->conf.verbosity >= 5
325 && wenThrough % 10000 == 0
326 ) {
327 cout << "toDecrease: " << *simplifier->limit_to_decrease << endl;
328 }
329
330 const size_t at = wenThrough % simplifier->clauses.size();
331 ClOffset offset = simplifier->clauses[at];
332 Clause* cl = solver->cl_alloc.ptr(offset);
333
334 //Has already been removed
335 if (cl->freed() || cl->getRemoved())
336 continue;
337
338 ret += strengthen_subsume_and_unlink_and_markirred(offset);
339
340 }
341
342 const double time_used = cpuTime() - myTime;
343 const bool time_out = *simplifier->limit_to_decrease <= 0;
344 const double time_remain = float_div(*simplifier->limit_to_decrease, orig_limit);
345
346 if (solver->conf.verbosity) {
347 cout
348 << "c [occ-sub-str-long-w-long] sub: " << ret.sub
349 << " str: " << ret.str
350 << " tried: " << wenThrough << "/" << simplifier->clauses.size()
351 << " ("
352 << stats_line_percent(wenThrough, simplifier->clauses.size())
353 << ") "
354 << solver->conf.print_times(time_used, time_out, time_remain)
355 << endl;
356 }
357 if (solver->sqlStats) {
358 solver->sqlStats->time_passed(
359 solver
360 , "occ-sub-str-long-w-long"
361 , time_used
362 , time_out
363 , time_remain
364 );
365 }
366
367 //Update time used
368 runStats.subsumedByStr += ret.sub;
369 runStats.litsRemStrengthen += ret.str;
370 runStats.strengthenTime += cpuTime() - myTime;
371
372 return solver->okay();
373 }
374
375 /**
376 @brief Helper function for findStrengthened
377
378 Used to avoid duplication of code
379 */
380 template<class T>
fillSubs(const ClOffset offset,const T & cl,const cl_abst_type abs,vector<ClOffset> & out_subsumed,vector<Lit> & out_lits,const Lit lit)381 void inline SubsumeStrengthen::fillSubs(
382 const ClOffset offset
383 , const T& cl
384 , const cl_abst_type abs
385 , vector<ClOffset>& out_subsumed
386 , vector<Lit>& out_lits
387 , const Lit lit
388 ) {
389 Lit litSub;
390 watch_subarray_const cs = solver->watches[lit];
391 *simplifier->limit_to_decrease -= (long)cs.size()*2+ 40;
392 for (const Watched *it = cs.begin(), *end = cs.end()
393 ; it != end
394 ; ++it
395 ) {
396 if (!it->isClause())
397 continue;
398
399 if (it->get_offset() == offset
400 || !subsetAbst(abs, it->getAbst())
401 ) {
402 continue;
403 }
404
405 ClOffset offset2 = it->get_offset();
406 const Clause& cl2 = *solver->cl_alloc.ptr(offset2);
407 if (cl2.getRemoved()
408 || cl.size() > cl2.size())
409 {
410 continue;
411 }
412
413 *simplifier->limit_to_decrease -= (long)((cl.size() + cl2.size())/4);
414 litSub = subset1(cl, cl2);
415 if (litSub != lit_Error) {
416 out_subsumed.push_back(it->get_offset());
417 out_lits.push_back(litSub);
418
419 #ifdef VERBOSE_DEBUG
420 if (litSub == lit_Undef) cout << "subsume-d: ";
421 else cout << "strengthen_subsume_and_unlink_and_markirred-ed (lit: "
422 << litSub
423 << ") clause offset: "
424 << it->get_offset()
425 << endl;
426 #endif
427 }
428 }
429 }
430
431 /**
432 @brief Checks if clauses are subsumed or could be strenghtened with given clause
433
434 Checks if:
435 * any clause is subsumed with given clause
436 * the given clause could perform self-subsuming resolution on any other clause
437
438 @param[in] ps The clause to perform the above listed algos with
439 @param[in] abs The abstraction of clause ps
440 @param[out] out_subsumed The clauses that could be modified by ps
441 @param[out] out_lits Defines HOW these clauses could be modified. By removing
442 literal, or by subsumption (in this case, there is lit_Undef here)
443 */
444 template<class T>
findStrengthened(ClOffset offset,const T & cl,const cl_abst_type abs,vector<ClOffset> & out_subsumed,vector<Lit> & out_lits)445 void SubsumeStrengthen::findStrengthened(
446 ClOffset offset
447 , const T& cl
448 , const cl_abst_type abs
449 , vector<ClOffset>& out_subsumed
450 , vector<Lit>& out_lits
451 )
452 {
453 #ifdef VERBOSE_DEBUG
454 cout << "findStrengthened: " << cl << endl;
455 #endif
456
457 uint32_t minVar = var_Undef;
458 uint32_t bestSize = std::numeric_limits<uint32_t>::max();
459 for (uint32_t i = 0; i < cl.size(); i++){
460 uint32_t newSize =
461 solver->watches[cl[i]].size()
462 + solver->watches[~cl[i]].size();
463
464 if (newSize < bestSize) {
465 minVar = cl[i].var();
466 bestSize = newSize;
467 }
468 }
469 assert(minVar != var_Undef);
470 *simplifier->limit_to_decrease -= (long)cl.size();
471
472 fillSubs(offset, cl, abs, out_subsumed, out_lits, Lit(minVar, true));
473 fillSubs(offset, cl, abs, out_subsumed, out_lits, Lit(minVar, false));
474 }
475
handle_added_long_cl(int64_t * limit_to_decrease,const bool main_run)476 bool SubsumeStrengthen::handle_added_long_cl(
477 int64_t* limit_to_decrease, const bool main_run)
478 {
479 int64_t orig_limit = *limit_to_decrease;
480 size_t origTrailSize = solver->trail_size();
481 const double start_time = cpuTime();
482 Sub1Ret stat;
483 bool interrupted = false;
484
485 //NOTE added_long_cl CAN CHANGE while the below is running!
486 for(size_t i = 0
487 ; i < simplifier->added_long_cl.size()
488 && *simplifier->limit_to_decrease >= 0
489 ; i++
490 ) {
491 const ClOffset offs = simplifier->added_long_cl[i];
492 Clause* cl = solver->cl_alloc.ptr(offs);
493 if (cl->freed() || cl->getRemoved())
494 continue;
495
496 cl->stats.marked_clause = 0;
497 auto ret = strengthen_subsume_and_unlink_and_markirred(offs);
498 stat += ret;
499 if (!solver->ok) {
500 goto end;
501 }
502
503 if ((i&0xfff) == 0xfff
504 && solver->must_interrupt_asap()
505 ) {
506 interrupted = true;
507 goto end;
508 }
509 }
510 if (*simplifier->limit_to_decrease < 0) {
511 interrupted = true;
512 }
513
514 end:
515
516 //we still have to clear the marks
517 if (interrupted) {
518 for(const ClOffset offs: simplifier->added_long_cl) {
519 Clause* cl = solver->cl_alloc.ptr(offs);
520 if (cl->freed() || cl->getRemoved())
521 continue;
522
523 cl->stats.marked_clause = 0;
524 }
525 }
526
527 if (main_run) {
528 const bool time_out = *limit_to_decrease <= 0;
529 const double time_used = cpuTime() - start_time;
530 const double time_remain = float_div(*limit_to_decrease, orig_limit);
531 if (solver->conf.verbosity) {
532 cout
533 << "c [occ-sub-str-w-added-long] "
534 << " sub: " << stat.sub
535 << " str: " << stat.str
536 << " 0-depth ass: " << solver->trail_size() - origTrailSize
537 << solver->conf.print_times(time_used, time_out, time_remain)
538 << endl;
539 }
540 if (solver->sqlStats) {
541 solver->sqlStats->time_passed(
542 solver
543 , "occ-sub-str-w-added-long"
544 , time_used
545 , time_out
546 , time_remain
547 );
548 }
549 }
550
551 return solver->okay();
552 }
553
remove_literal(ClOffset offset,const Lit toRemoveLit)554 void SubsumeStrengthen::remove_literal(ClOffset offset, const Lit toRemoveLit)
555 {
556 Clause& cl = *solver->cl_alloc.ptr(offset);
557 #ifdef VERBOSE_DEBUG
558 cout << "-> Strenghtening clause :" << cl;
559 cout << " with lit: " << toRemoveLit << endl;
560 #endif
561
562 *simplifier->limit_to_decrease -= 5;
563
564 (*solver->drat) << deldelay << cl << fin;
565 cl.strengthen(toRemoveLit);
566 simplifier->added_cl_to_var.touch(toRemoveLit.var());
567 cl.recalc_abst_if_needed();
568 (*solver->drat) << add << cl
569 #ifdef STATS_NEEDED
570 << solver->sumConflicts
571 #endif
572 << fin << findelay;
573 if (!cl.red()) {
574 simplifier->n_occurs[toRemoveLit.toInt()]--;
575 simplifier->elim_calc_need_update.touch(toRemoveLit.var());
576 simplifier->removed_cl_with_var.touch(toRemoveLit.var());
577 }
578
579 runStats.litsRemStrengthen++;
580 removeWCl(solver->watches[toRemoveLit], offset);
581 if (cl.red())
582 solver->litStats.redLits--;
583 else
584 solver->litStats.irredLits--;
585
586 simplifier->clean_clause(offset);
587 }
588 /**
589 @brief Decides only using abstraction if clause A could subsume clause B
590
591 @note: It can give false positives. Never gives false negatives.
592
593 For A to subsume B, everything that is in A MUST be in B. So, if (A & ~B)
594 contains even one bit, it means that A contains something that B doesn't. So
595 A may be a subset of B only if (A & ~B) == 0
596 */
subsetAbst(const cl_abst_type A,const cl_abst_type B)597 bool SubsumeStrengthen::subsetAbst(const cl_abst_type A, const cl_abst_type B)
598 {
599 return ((A & ~B) == 0);
600 }
601
602 //A subsumes B (A <= B)
603 template<class T1, class T2>
subset(const T1 & A,const T2 & B)604 bool SubsumeStrengthen::subset(const T1& A, const T2& B)
605 {
606 #ifdef MORE_DEUBUG
607 cout << "A:" << A << endl;
608 for(size_t i = 1; i < A.size(); i++) {
609 assert(A[i-1] < A[i]);
610 }
611
612 cout << "B:" << B << endl;
613 for(size_t i = 1; i < B.size(); i++) {
614 assert(B[i-1] < B[i]);
615 }
616 #endif
617
618 bool ret;
619 uint32_t i = 0;
620 uint32_t i2;
621 Lit lastB = lit_Undef;
622 for (i2 = 0; i2 < B.size(); i2++) {
623 if (lastB != lit_Undef)
624 assert(lastB < B[i2]);
625
626 lastB = B[i2];
627 //Literals are ordered
628 if (A[i] < B[i2]) {
629 ret = false;
630 goto end;
631 }
632 else if (A[i] == B[i2]) {
633 i++;
634
635 //went through the whole of A now, so A subsumes B
636 if (i == A.size()) {
637 ret = true;
638 goto end;
639 }
640 }
641 }
642 ret = false;
643
644 end:
645 *simplifier->limit_to_decrease -= (long)i2*4 + (long)i*4;
646 return ret;
647 }
648
649 /**
650 @brief Decides if A subsumes B, or if not, if A could strenghten B
651
652 @note: Assumes 'seen' is cleared (will leave it cleared)
653
654 Helper function for strengthening. Does two things in one go:
655 1) decides if clause A could subsume clause B
656 2) decides if clause A could be used to perform self-subsuming resoltuion on
657 clause B
658
659 @return lit_Error, if neither (1) or (2) is true. Returns lit_Undef (1) is true,
660 and returns the literal to remove if (2) is true
661 */
662 template<class T1, class T2>
subset1(const T1 & A,const T2 & B)663 Lit SubsumeStrengthen::subset1(const T1& A, const T2& B)
664 {
665 Lit retLit = lit_Undef;
666
667 uint32_t i = 0;
668 uint32_t i2;
669 for (i2 = 0; i2 < B.size(); i2++) {
670 if (A[i] == ~B[i2] && retLit == lit_Undef) {
671 retLit = B[i2];
672 i++;
673 if (i == A.size())
674 goto end;
675
676 continue;
677 }
678
679 //Literals are ordered
680 if (A[i] < B[i2]) {
681 retLit = lit_Error;
682 goto end;
683 }
684
685 if (A[i] == B[i2]) {
686 i++;
687
688 if (i == A.size())
689 goto end;
690 }
691 }
692 retLit = lit_Error;
693
694 end:
695 *simplifier->limit_to_decrease -= (long)i2*4 + (long)i*4;
696 return retLit;
697 }
698
699 template<class T>
find_smallest_watchlist_for_clause(const T & ps) const700 size_t SubsumeStrengthen::find_smallest_watchlist_for_clause(const T& ps) const
701 {
702 size_t min_i = 0;
703 size_t min_num = solver->watches[ps[min_i]].size();
704 for (uint32_t i = 1; i < ps.size(); i++){
705 const size_t this_num = solver->watches[ps[i]].size();
706 if (this_num < min_num) {
707 min_i = i;
708 min_num = this_num;
709 }
710 }
711 *simplifier->limit_to_decrease -= (long)ps.size();
712
713 return min_i;
714 }
715
716 /**
717 @brief Finds clauses that are backward-subsumed by given clause
718
719 Only handles backward-subsumption. Uses occurrence lists
720 @param[out] out_subsumed The set of clauses subsumed by the given
721 */
find_subsumed(const ClOffset offset,const T & ps,const cl_abst_type abs,vector<ClOffset> & out_subsumed,bool removeImplicit)722 template<class T> void SubsumeStrengthen::find_subsumed(
723 const ClOffset offset //Will not match with index of the name value
724 , const T& ps //Literals in clause
725 , const cl_abst_type abs //Abstraction of literals in clause
726 , vector<ClOffset>& out_subsumed //List of clause indexes subsumed
727 , bool removeImplicit
728 ) {
729 #ifdef VERBOSE_DEBUG
730 cout << "find_subsumed: ";
731 for (const Lit lit: ps) {
732 cout << lit << " , ";
733 }
734 cout << endl;
735 #endif
736
737 const size_t smallest = find_smallest_watchlist_for_clause(ps);
738
739 //Go through the occur list of the literal that has the smallest occur list
740 watch_subarray occ = solver->watches[ps[smallest]];
741 *simplifier->limit_to_decrease -= (long)occ.size()*8 + 40;
742
743 Watched* it = occ.begin();
744 Watched* it2 = occ.begin();
745 size_t numBinFound = 0;
746 for (const Watched* end = occ.end()
747 ; it != end
748 ; ++it
749 ) {
750 if (removeImplicit) {
751 if (it->isBin()
752 && ps.size() == 2
753 && ps[!smallest] == it->lit2()
754 && !it->red()
755 ) {
756 /*cout
757 << "ps " << ps << " could subsume this bin: "
758 << ps[smallest] << ", " << it->lit2()
759 << endl;*/
760 numBinFound++;
761
762 //We cannot remove ourselves
763 if (numBinFound > 1) {
764 removeWBin(solver->watches, it->lit2(), ps[smallest], it->red());
765 solver->binTri.irredBins--;
766 continue;
767 }
768 }
769 }
770 *it2++ = *it;
771
772 if (!it->isClause()) {
773 continue;
774 }
775
776 *simplifier->limit_to_decrease -= 15;
777
778 if (it->get_offset() == offset
779 || !subsetAbst(abs, it->getAbst())
780 ) {
781 continue;
782 }
783
784 const ClOffset offset2 = it->get_offset();
785 Clause& cl2 = *solver->cl_alloc.ptr(offset2);
786
787 if (ps.size() > cl2.size() || cl2.getRemoved())
788 continue;
789
790 *simplifier->limit_to_decrease -= 50;
791 if (subset(ps, cl2)) {
792 out_subsumed.push_back(offset2);
793 #ifdef VERBOSE_DEBUG
794 cout << "subsumed cl offset: " << offset2 << endl;
795 #endif
796 }
797 }
798 occ.shrink(it-it2);
799 }
800 template void SubsumeStrengthen::find_subsumed(
801 const ClOffset offset
802 , const std::array<Lit, 2>& ps
803 , const cl_abst_type abs //Abstraction of literals in clause
804 , vector<ClOffset>& out_subsumed //List of clause indexes subsumed
805 , bool removeImplicit
806 );
807
mem_used() const808 size_t SubsumeStrengthen::mem_used() const
809 {
810 size_t b = 0;
811 b += subs.capacity()*sizeof(ClOffset);
812 b += subsLits.capacity()*sizeof(Lit);
813
814 return b;
815 }
816
finishedRun()817 void SubsumeStrengthen::finishedRun()
818 {
819 globalstats += runStats;
820 }
821
print_short(const Solver * solver) const822 void SubsumeStrengthen::Stats::print_short(const Solver* solver) const
823 {
824 cout << "c [occ-substr] long"
825 << " subBySub: " << subsumedBySub
826 << " subByStr: " << subsumedByStr
827 << " lits-rem-str: " << litsRemStrengthen
828 << solver->conf.print_times(subsumeTime+strengthenTime)
829 << endl;
830 }
831
print() const832 void SubsumeStrengthen::Stats::print() const
833 {
834 cout << "c -------- SubsumeStrengthen STATS ----------" << endl;
835 print_stats_line("c cl-subs"
836 , subsumedBySub + subsumedByStr
837 , " Clauses"
838 );
839 print_stats_line("c cl-str rem lit"
840 , litsRemStrengthen
841 , " Lits"
842 );
843 print_stats_line("c cl-sub T"
844 , subsumeTime
845 , " s"
846 );
847 print_stats_line("c cl-str T"
848 , strengthenTime
849 , " s"
850 );
851 cout << "c -------- SubsumeStrengthen STATS END ----------" << endl;
852 }
853
operator +=(const Stats & other)854 SubsumeStrengthen::Stats& SubsumeStrengthen::Stats::operator+=(const Stats& other)
855 {
856 subsumedBySub += other.subsumedBySub;
857 subsumedByStr += other.subsumedByStr;
858 litsRemStrengthen += other.litsRemStrengthen;
859
860 subsumeTime += other.subsumeTime;
861 strengthenTime += other.strengthenTime;
862
863 return *this;
864 }
865
backw_sub_str_long_with_implicit(const vector<Lit> & lits)866 SubsumeStrengthen::Sub1Ret SubsumeStrengthen::backw_sub_str_long_with_implicit(
867 const vector<Lit>& lits
868 ) {
869 subs.clear();
870 subsLits.clear();
871
872 findStrengthened(
873 CL_OFFSET_MAX
874 , lits
875 , calcAbstraction(lits)
876 , subs
877 , subsLits
878 );
879
880 Sub1Ret ret;
881
882 for (size_t j = 0
883 ; j < subs.size() && solver->okay()
884 ; j++
885 ) {
886 ClOffset offset2 = subs[j];
887 Clause& cl2 = *solver->cl_alloc.ptr(offset2);
888 if (subsLits[j] == lit_Undef) { //Subsume
889 #ifdef VERBOSE_DEBUG
890 if (solver->conf.verbosity >= 6)
891 cout << "subsumed clause " << cl2 << endl;
892 #endif
893 #ifdef USE_GAUSS
894 if (cl2.used_in_xor() &&
895 solver->conf.force_preserve_xors)
896 {
897 continue;
898 }
899 #endif
900
901 if (!cl2.red()) {
902 ret.subsumedIrred = true;
903 }
904
905 simplifier->unlink_clause(offset2, true, false, true);
906 ret.sub++;
907 } else { //Strengthen
908 #ifdef VERBOSE_DEBUG
909 if (solver->conf.verbosity >= 6) {
910 cout << "strenghtened clause " << cl2 << endl;
911 }
912 #endif
913 #ifdef USE_GAUSS
914 if (cl2.used_in_xor() &&
915 solver->conf.force_preserve_xors)
916 {
917 //cout << "str-ing used in XOR with bin" << endl;
918 continue;
919 }
920 #endif
921 remove_literal(offset2, subsLits[j]);
922
923 ret.str++;
924 if (!solver->ok)
925 return ret;
926
927 //If we are waaay over time, just exit
928 if (*simplifier->limit_to_decrease < -20LL*1000LL*1000LL)
929 break;
930 }
931 }
932
933 return ret;
934 }
935
backw_sub_str_long_with_bins_watch(const Lit lit,const bool redundant_too)936 bool SubsumeStrengthen::backw_sub_str_long_with_bins_watch(
937 const Lit lit
938 , const bool redundant_too
939 ) {
940 watch_subarray ws = solver->watches[lit];
941 for (size_t i = 0
942 ; i < ws.size() && *simplifier->limit_to_decrease > 0
943 ; i++
944 ) {
945 //Each BIN only once
946 if (ws[i].isBin()
947 && (redundant_too || lit < ws[i].lit2())
948 ) {
949 const bool red = ws[i].red();
950 tried_bin_tri++;
951 tmpLits.resize(2);
952 tmpLits[0] = lit;
953 tmpLits[1] = ws[i].lit2();
954 std::sort(tmpLits.begin(), tmpLits.end());
955
956 Sub1Ret ret = backw_sub_str_long_with_implicit(tmpLits);
957 subsumedBin += ret.sub;
958 strBin += ret.str;
959 if (!solver->ok)
960 return false;
961
962 if (red
963 && ret.subsumedIrred
964 ) {
965 solver->binTri.redBins--;
966 solver->binTri.irredBins++;
967 simplifier->n_occurs[tmpLits[0].toInt()]++;
968 simplifier->n_occurs[tmpLits[1].toInt()]++;
969 findWatchedOfBin(solver->watches, tmpLits[1], tmpLits[0], true).setRed(false);
970 findWatchedOfBin(solver->watches, tmpLits[0], tmpLits[1], true).setRed(false);
971 }
972 continue;
973 }
974
975 //Must be a longer clause, break
976 //assert(ws[i].isClause());
977 //break;
978 }
979
980 return true;
981 }
982
backw_sub_str_long_with_bins()983 bool SubsumeStrengthen::backw_sub_str_long_with_bins()
984 {
985 //Stats
986 int64_t orig_time_limit = *simplifier->limit_to_decrease;
987 const size_t origTrailSize = solver->trail_size();
988 double myTime = cpuTime();
989 subsumedBin = 0;
990 strBin = 0;
991
992 //Randomize start in the watchlist
993 size_t upI;
994 upI = solver->mtrand.randInt(solver->watches.size()-1);
995
996 size_t numDone = 0;
997 for (; numDone < solver->watches.size() && *simplifier->limit_to_decrease > 0
998 ; upI = (upI +1) % solver->watches.size(), numDone++
999
1000 ) {
1001 Lit lit = Lit::toLit(upI);
1002 if (!backw_sub_str_long_with_bins_watch(lit, true)) {
1003 break;
1004 }
1005 }
1006
1007 const double time_used = cpuTime() - myTime;
1008 const bool time_out = *simplifier->limit_to_decrease <= 0;
1009 const double time_remain = float_div(*simplifier->limit_to_decrease, orig_time_limit);
1010 if (solver->conf.verbosity) {
1011 cout
1012 << "c [occ-backw-sub-str-long-w-bins]"
1013 << " subs: " << subsumedBin
1014 << " str: " << strBin
1015 << " tried: " << tried_bin_tri
1016 << " 0-depth ass: " << solver->trail_size() - origTrailSize
1017 << solver->conf.print_times(time_used, time_out, time_remain)
1018 << endl;
1019 }
1020
1021 if (solver->sqlStats) {
1022 solver->sqlStats->time_passed(
1023 solver
1024 , "occ-backw-sub-str-long-w-bins"
1025 , time_used
1026 , time_out
1027 , time_remain
1028 );
1029 }
1030
1031 //runStats.zeroDepthAssigns = solver->trail_size() - origTrailSize;
1032
1033 return solver->okay();
1034 }
1035
1036