1 /***************************************************************************************[SimpSolver.cc]
2 Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
3 CRIL - Univ. Artois, France
4 LRI - Univ. Paris Sud, France (2009-2013)
5 Labri - Univ. Bordeaux, France
7 Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
8 CRIL - Univ. Artois, France
9 Labri - Univ. Bordeaux, France
11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
13 is based on. (see below).
15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
19 furnished to do so, subject to the following conditions:
21 - The above and below copyrights notices and this permission notice shall be included in all
22 copies or substantial portions of the Software;
23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
24 be used in any competitive event (sat competitions/evaluations) without the express permission of
25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
26 using Glucose Parallel as an embedded SAT engine (single core or not).
29 --------------- Original Minisat Copyrights
31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
32 Copyright (c) 2007-2010, Niklas Sorensson
34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
35 associated documentation files (the "Software"), to deal in the Software without restriction,
36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
38 furnished to do so, subject to the following conditions:
40 The above copyright notice and this permission notice shall be included in all copies or
41 substantial portions of the Software.
43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
48 **************************************************************************************************/
51 #include "simp/SimpSolver.h"
52 #include "utils/System.h"
54 using namespace Glucose;
56 //=================================================================================================
60 static const char* _cat = "SIMP";
62 static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false);
63 static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false);
64 static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true);
65 static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
66 static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX));
67 static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
68 static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false));
71 //=================================================================================================
72 // Constructor/Destructor:
75 SimpSolver::SimpSolver() :
78 , clause_lim (opt_clause_lim)
79 , subsumption_lim (opt_subsumption_lim)
80 , simp_garbage_frac (opt_simp_garbage_frac)
81 , use_asymm (opt_use_asymm)
82 , use_rcheck (opt_use_rcheck)
83 , use_elim (opt_use_elim)
88 , use_simplification (true)
89 , occurs (ClauseDeleted(ca))
90 , elim_heap (ElimLt(n_occ))
94 vec<Lit> dummy(1,lit_Undef);
95 ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
96 bwdsub_tmpunit = ca.alloc(dummy);
97 remove_satisfied = false;
101 SimpSolver::~SimpSolver()
107 SimpSolver::SimpSolver(const SimpSolver &s) : Solver(s)
109 , clause_lim (s.clause_lim)
110 , subsumption_lim (s.subsumption_lim)
111 , simp_garbage_frac (s.simp_garbage_frac)
112 , use_asymm (s.use_asymm)
113 , use_rcheck (s.use_rcheck)
114 , use_elim (s.use_elim)
116 , asymm_lits (s.asymm_lits)
117 , eliminated_vars (s.eliminated_vars)
118 , elimorder (s.elimorder)
119 , use_simplification (s.use_simplification)
120 , occurs (ClauseDeleted(ca))
121 , elim_heap (ElimLt(n_occ))
122 , bwdsub_assigns (s.bwdsub_assigns)
123 , n_touched (s.n_touched)
125 // TODO: Copy dummy... what is it???
126 vec<Lit> dummy(1,lit_Undef);
127 ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
128 bwdsub_tmpunit = ca.alloc(dummy);
129 remove_satisfied = false;
133 s.elimclauses.memCopyTo(elimclauses);
134 s.touched.memCopyTo(touched);
135 s.occurs.copyTo(occurs);
136 s.n_occ.memCopyTo(n_occ);
137 s.elim_heap.copyTo(elim_heap);
138 s.subsumption_queue.copyTo(subsumption_queue);
139 s.frozen.memCopyTo(frozen);
140 s.eliminated.memCopyTo(eliminated);
142 use_simplification = s.use_simplification;
143 bwdsub_assigns = s.bwdsub_assigns;
144 n_touched = s.n_touched;
145 bwdsub_tmpunit = s.bwdsub_tmpunit;
152 Var SimpSolver::newVar(bool sign, bool dvar) {
153 Var v = Solver::newVar(sign, dvar);
154 frozen .push((char)false);
155 eliminated.push((char)false);
157 if (use_simplification){
162 elim_heap .insert(v);
166 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
168 vec<Var> extra_frozen;
169 lbool result = l_True;
170 do_simp &= use_simplification;
173 // Assumptions must be temporarily frozen to run variable elimination:
174 for (int i = 0; i < assumptions.size(); i++){
175 Var v = var(assumptions[i]);
177 // If an assumption has been eliminated, remember it.
178 assert(!isEliminated(v));
183 extra_frozen.push(v);
186 result = lbool(eliminate(turn_off_simp));
189 if (result == l_True)
190 result = Solver::solve_();
191 else if (verbosity >= 1)
192 printf("===============================================================================\n");
194 if (result == l_True)
198 // Unfreeze the assumptions that were frozen:
199 for (int i = 0; i < extra_frozen.size(); i++)
200 setFrozen(extra_frozen[i], false);
208 bool SimpSolver::addClause_(vec<Lit>& ps)
211 for (int i = 0; i < ps.size(); i++)
212 assert(!isEliminated(var(ps[i])));
214 int nclauses = clauses.size();
216 if (use_rcheck && implied(ps))
219 if (!Solver::addClause_(ps))
222 if(!parsing && certifiedUNSAT) {
223 for (int i = 0; i < ps.size(); i++)
224 fprintf(certifiedOutput, "%i " , (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1) );
225 fprintf(certifiedOutput, "0\n");
228 if (use_simplification && clauses.size() == nclauses + 1){
229 CRef cr = clauses.last();
230 const Clause& c = ca[cr];
232 // NOTE: the clause is added to the queue immediately and then
233 // again during 'gatherTouchedClauses()'. If nothing happens
234 // in between, it will only be checked once. Otherwise, it may
235 // be checked twice unnecessarily. This is an unfortunate
236 // consequence of how backward subsumption is used to mimic
237 // forward subsumption.
238 subsumption_queue.insert(cr);
239 for (int i = 0; i < c.size(); i++){
240 occurs[var(c[i])].push(cr);
241 n_occ[toInt(c[i])]++;
242 touched[var(c[i])] = 1;
244 if (elim_heap.inHeap(var(c[i])))
245 elim_heap.increase(var(c[i]));
254 void SimpSolver::removeClause(CRef cr,bool inPurgatory)
256 const Clause& c = ca[cr];
258 if (use_simplification)
259 for (int i = 0; i < c.size(); i++){
260 n_occ[toInt(c[i])]--;
261 updateElimHeap(var(c[i]));
262 occurs.smudge(var(c[i]));
265 Solver::removeClause(cr,inPurgatory);
269 bool SimpSolver::strengthenClause(CRef cr, Lit l)
272 assert(decisionLevel() == 0);
273 assert(use_simplification);
275 // FIX: this is too inefficient but would be nice to have (properly implemented)
276 // if (!find(subsumption_queue, &c))
277 subsumption_queue.insert(cr);
279 if (certifiedUNSAT) {
280 for (int i = 0; i < c.size(); i++)
281 if (c[i] != l) fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
282 fprintf(certifiedOutput, "0\n");
289 if (certifiedUNSAT) {
290 fprintf(certifiedOutput, "d ");
291 for (int i = 0; i < c.size(); i++)
292 fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
293 fprintf(certifiedOutput, "0\n");
296 detachClause(cr, true);
299 remove(occurs[var(l)], cr);
301 updateElimHeap(var(l));
304 return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
308 // Returns FALSE if clause is always satisfied ('out_clause' should not be used).
309 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
314 bool ps_smallest = _ps.size() < _qs.size();
315 const Clause& ps = ps_smallest ? _qs : _ps;
316 const Clause& qs = ps_smallest ? _ps : _qs;
318 for (int i = 0; i < qs.size(); i++){
319 if (var(qs[i]) != v){
320 for (int j = 0; j < ps.size(); j++)
321 if (var(ps[j]) == var(qs[i]))
326 out_clause.push(qs[i]);
331 for (int i = 0; i < ps.size(); i++)
333 out_clause.push(ps[i]);
339 // Returns FALSE if clause is always satisfied.
340 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
344 bool ps_smallest = _ps.size() < _qs.size();
345 const Clause& ps = ps_smallest ? _qs : _ps;
346 const Clause& qs = ps_smallest ? _ps : _qs;
347 const Lit* __ps = (const Lit*)ps;
348 const Lit* __qs = (const Lit*)qs;
352 for (int i = 0; i < qs.size(); i++){
353 if (var(__qs[i]) != v){
354 for (int j = 0; j < ps.size(); j++)
355 if (var(__ps[j]) == var(__qs[i]))
356 if (__ps[j] == ~__qs[i])
369 void SimpSolver::gatherTouchedClauses()
371 if (n_touched == 0) return;
374 for (i = j = 0; i < subsumption_queue.size(); i++)
375 if (ca[subsumption_queue[i]].mark() == 0)
376 ca[subsumption_queue[i]].mark(2);
378 for (i = 0; i < touched.size(); i++)
380 const vec<CRef>& cs = occurs.lookup(i);
381 for (j = 0; j < cs.size(); j++)
382 if (ca[cs[j]].mark() == 0){
383 subsumption_queue.insert(cs[j]);
389 for (i = 0; i < subsumption_queue.size(); i++)
390 if (ca[subsumption_queue[i]].mark() == 2)
391 ca[subsumption_queue[i]].mark(0);
397 bool SimpSolver::implied(const vec<Lit>& c)
399 assert(decisionLevel() == 0);
401 trail_lim.push(trail.size());
402 for (int i = 0; i < c.size(); i++)
403 if (value(c[i]) == l_True){
406 }else if (value(c[i]) != l_False){
407 assert(value(c[i]) == l_Undef);
408 uncheckedEnqueue(~c[i]);
411 bool result = propagate() != CRef_Undef;
417 // Backward subsumption + backward subsumption resolution
418 bool SimpSolver::backwardSubsumptionCheck(bool verbose)
422 int deleted_literals = 0;
423 assert(decisionLevel() == 0);
425 while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
427 // Empty subsumption queue and return immediately on user-interrupt:
428 if (asynch_interrupt){
429 subsumption_queue.clear();
430 bwdsub_assigns = trail.size();
433 // Check top-level assignments by creating a dummy clause and placing it in the queue:
434 if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
435 Lit l = trail[bwdsub_assigns++];
436 ca[bwdsub_tmpunit][0] = l;
437 ca[bwdsub_tmpunit].calcAbstraction();
438 subsumption_queue.insert(bwdsub_tmpunit); }
440 CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
443 if (c.mark()) continue;
445 if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
446 printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
448 assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
450 // Find best variable to scan:
451 Var best = var(c[0]);
452 for (int i = 1; i < c.size(); i++)
453 if (occurs[var(c[i])].size() < occurs[best].size())
456 // Search all candidates:
457 vec<CRef>& _cs = occurs.lookup(best);
458 CRef* cs = (CRef*)_cs;
460 for (int j = 0; j < _cs.size(); j++)
463 else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
464 Lit l = c.subsumes(ca[cs[j]]);
467 subsumed++, removeClause(cs[j]);
468 else if (l != lit_Error){
471 if (!strengthenClause(cs[j], ~l))
474 // Did current candidate get deleted from cs? Then check candidate at index j again:
485 bool SimpSolver::asymm(Var v, CRef cr)
488 assert(decisionLevel() == 0);
490 if (c.mark() || satisfied(c)) return true;
492 trail_lim.push(trail.size());
494 for (int i = 0; i < c.size(); i++)
495 if (var(c[i]) != v && value(c[i]) != l_False)
496 uncheckedEnqueue(~c[i]);
500 if (propagate() != CRef_Undef){
503 if (!strengthenClause(cr, l))
512 bool SimpSolver::asymmVar(Var v)
514 assert(use_simplification);
516 const vec<CRef>& cls = occurs.lookup(v);
518 if (value(v) != l_Undef || cls.size() == 0)
521 for (int i = 0; i < cls.size(); i++)
522 if (!asymm(v, cls[i]))
525 return backwardSubsumptionCheck();
529 static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
531 elimclauses.push(toInt(x));
536 static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
538 int first = elimclauses.size();
541 // Copy clause to elimclauses-vector. Remember position where the
542 // variable 'v' occurs:
543 for (int i = 0; i < c.size(); i++){
544 elimclauses.push(toInt(c[i]));
550 // Swap the first literal with the 'v' literal, so that the literal
551 // containing 'v' will occur first in the clause:
552 uint32_t tmp = elimclauses[v_pos];
553 elimclauses[v_pos] = elimclauses[first];
554 elimclauses[first] = tmp;
556 // Store the length of the clause last:
557 elimclauses.push(c.size());
562 bool SimpSolver::eliminateVar(Var v)
565 assert(!isEliminated(v));
566 assert(value(v) == l_Undef);
568 // Split the occurrences into positive and negative:
570 const vec<CRef>& cls = occurs.lookup(v);
572 for (int i = 0; i < cls.size(); i++)
573 (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
575 // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
576 // clause must exceed the limit on the maximal clause size (if it is set):
581 for (int i = 0; i < pos.size(); i++)
582 for (int j = 0; j < neg.size(); j++)
583 if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
584 (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
587 // Delete and store old clauses:
588 eliminated[v] = true;
589 setDecisionVar(v, false);
592 if (pos.size() > neg.size()){
593 for (int i = 0; i < neg.size(); i++)
594 mkElimClause(elimclauses, v, ca[neg[i]]);
595 mkElimClause(elimclauses, mkLit(v));
597 for (int i = 0; i < pos.size(); i++)
598 mkElimClause(elimclauses, v, ca[pos[i]]);
599 mkElimClause(elimclauses, ~mkLit(v));
603 // Produce clauses in cross product:
604 vec<Lit>& resolvent = add_tmp;
605 for (int i = 0; i < pos.size(); i++)
606 for (int j = 0; j < neg.size(); j++)
607 if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
610 for (int i = 0; i < cls.size(); i++)
611 removeClause(cls[i]);
613 // Free occurs list for this variable:
614 occurs[v].clear(true);
616 // Free watchers lists for this variable, if possible:
617 if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
618 if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
620 return backwardSubsumptionCheck();
624 bool SimpSolver::substitute(Var v, Lit x)
627 assert(!isEliminated(v));
628 assert(value(v) == l_Undef);
630 if (!ok) return false;
632 eliminated[v] = true;
633 setDecisionVar(v, false);
634 const vec<CRef>& cls = occurs.lookup(v);
636 vec<Lit>& subst_clause = add_tmp;
637 for (int i = 0; i < cls.size(); i++){
638 Clause& c = ca[cls[i]];
640 subst_clause.clear();
641 for (int j = 0; j < c.size(); j++){
643 subst_clause.push(var(p) == v ? x ^ sign(p) : p);
647 if (!addClause_(subst_clause))
650 removeClause(cls[i]);
658 void SimpSolver::extendModel()
663 if(model.size()==0) model.growTo(nVars());
665 for (i = elimclauses.size()-1; i > 0; i -= j){
666 for (j = elimclauses[i--]; j > 1; j--, i--)
667 if (modelValue(toLit(elimclauses[i])) != l_False)
670 x = toLit(elimclauses[i]);
671 model[var(x)] = lbool(!sign(x));
677 bool SimpSolver::eliminate(bool turn_off_elim)
683 else if (!use_simplification)
686 // Main simplification loop:
689 int toPerform = clauses.size()<=4800000;
692 printf("c Too many clauses... No preprocessing\n");
695 while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
697 gatherTouchedClauses();
698 // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
699 if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
700 !backwardSubsumptionCheck(true)){
701 ok = false; goto cleanup; }
703 // Empty elim_heap and return immediately on user-interrupt:
704 if (asynch_interrupt){
705 assert(bwdsub_assigns == trail.size());
706 assert(subsumption_queue.size() == 0);
707 assert(n_touched == 0);
711 // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
712 for (int cnt = 0; !elim_heap.empty(); cnt++){
713 Var elim = elim_heap.removeMin();
715 if (asynch_interrupt) break;
717 if (isEliminated(elim) || value(elim) != l_Undef) continue;
719 if (verbosity >= 2 && cnt % 100 == 0)
720 printf("elimination left: %10d\r", elim_heap.size());
723 // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
724 bool was_frozen = frozen[elim];
726 if (!asymmVar(elim)){
727 ok = false; goto cleanup; }
728 frozen[elim] = was_frozen; }
730 // At this point, the variable may have been set by assymetric branching, so check it
731 // again. Also, don't eliminate frozen variables:
732 if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
733 ok = false; goto cleanup; }
735 checkGarbage(simp_garbage_frac);
738 assert(subsumption_queue.size() == 0);
742 // If no more simplification is needed, free all simplification-related data structures:
744 touched .clear(true);
747 elim_heap.clear(true);
748 subsumption_queue.clear(true);
750 use_simplification = false;
751 remove_satisfied = true;
752 ca.extra_clause_field = false;
754 // Force full cleanup (this is safe and desirable since it only happens once):
759 cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
763 if (verbosity >= 0 && elimclauses.size() > 0)
764 printf("c | Eliminated clauses: %10.2f Mb |\n",
765 double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
774 void SimpSolver::cleanUpClauses()
778 for (i = j = 0; i < clauses.size(); i++)
779 if (ca[clauses[i]].mark() == 0)
780 clauses[j++] = clauses[i];
781 clauses.shrink(i - j);
785 //=================================================================================================
786 // Garbage Collection methods:
789 void SimpSolver::relocAll(ClauseAllocator& to)
791 if (!use_simplification) return;
795 for (int i = 0; i < nVars(); i++){
796 vec<CRef>& cs = occurs[i];
797 for (int j = 0; j < cs.size(); j++)
801 // Subsumption queue:
803 for (int i = 0; i < subsumption_queue.size(); i++)
804 ca.reloc(subsumption_queue[i], to);
808 ca.reloc(bwdsub_tmpunit, to);
812 void SimpSolver::garbageCollect()
814 // Initialize the next region to a size corresponding to the estimated utilization degree. This
815 // is not precise but should avoid some unnecessary reallocations for the new region:
816 ClauseAllocator to(ca.size() - ca.wasted());
819 to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
821 Solver::relocAll(to);
823 printf("| Garbage collection: %12d bytes => %12d bytes |\n",
824 ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);