1 #define __STDC_FORMAT_MACROS
2 #define __STDC_LIMIT_MACROS
3 /***********************************************************************************[SimpSolver.cc]
4 Copyright (c) 2006, Niklas Een, Niklas Sorensson
5 Copyright (c) 2007-2010, Niklas Sorensson
7 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
8 associated documentation files (the "Software"), to deal in the Software without restriction,
9 including without limitation the rights to use, copy, modify, merge, publish, distribute,
10 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
11 furnished to do so, subject to the following conditions:
13 The above copyright notice and this permission notice shall be included in all copies or
14 substantial portions of the Software.
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
17 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
18 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
19 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
20 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
21 **************************************************************************************************/
23 #include "libs/minisat/Sort.h"
24 #include "libs/minisat/SimpSolver.h"
25 #include "libs/minisat/System.h"
27 using namespace Minisat
;
29 //=================================================================================================
33 static const char* _cat
= "SIMP";
35 static BoolOption
opt_use_asymm (_cat
, "asymm", "Shrink clauses by asymmetric branching.", false);
36 static BoolOption
opt_use_rcheck (_cat
, "rcheck", "Check if a clause is already implied. (costly)", false);
37 static BoolOption
opt_use_elim (_cat
, "elim", "Perform variable elimination.", true);
38 static IntOption
opt_grow (_cat
, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
39 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
));
40 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
));
41 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));
44 //=================================================================================================
45 // Constructor/Destructor:
48 SimpSolver::SimpSolver() :
50 , clause_lim (opt_clause_lim
)
51 , subsumption_lim (opt_subsumption_lim
)
52 , simp_garbage_frac (opt_simp_garbage_frac
)
53 , use_asymm (opt_use_asymm
)
54 , use_rcheck (opt_use_rcheck
)
55 , use_elim (opt_use_elim
)
61 , use_simplification (true)
62 , occurs (ClauseDeleted(ca
))
63 , elim_heap (ElimLt(n_occ
))
67 vec
<Lit
> dummy(1,lit_Undef
);
68 ca
.extra_clause_field
= true; // NOTE: must happen before allocating the dummy clause below.
69 bwdsub_tmpunit
= ca
.alloc(dummy
);
70 remove_satisfied
= false;
74 SimpSolver::~SimpSolver()
79 Var
SimpSolver::newVar(lbool upol
, bool dvar
) {
80 Var v
= Solver::newVar(upol
, dvar
);
82 frozen
.insert(v
, (char)false);
83 eliminated
.insert(v
, (char)false);
85 if (use_simplification
){
86 n_occ
.insert( mkLit(v
), 0);
87 n_occ
.insert(~mkLit(v
), 0);
89 touched
.insert(v
, 0);
95 void SimpSolver::releaseVar(Lit l
)
97 assert(!isEliminated(var(l
)));
98 if (!use_simplification
&& var(l
) >= max_simp_var
)
99 // Note: Guarantees that no references to this variable is
100 // left in model extension datastructure. Could be improved!
101 Solver::releaseVar(l
);
103 // Otherwise, don't allow variable to be reused.
104 Solver::addClause(l
);
108 lbool
SimpSolver::solve_(bool do_simp
, bool turn_off_simp
)
110 vec
<Var
> extra_frozen
;
111 lbool result
= l_True
;
113 do_simp
&= use_simplification
;
116 // Assumptions must be temporarily frozen to run variable elimination:
117 for (int i
= 0; i
< assumptions
.size(); i
++){
118 Var v
= var(assumptions
[i
]);
120 // If an assumption has been eliminated, remember it.
121 assert(!isEliminated(v
));
126 extra_frozen
.push(v
);
129 result
= lbool(eliminate(turn_off_simp
));
132 if (result
== l_True
)
133 result
= Solver::solve_();
134 else if (verbosity
>= 1)
135 printf("===============================================================================\n");
137 if (result
== l_True
&& extend_model
)
141 // Unfreeze the assumptions that were frozen:
142 for (int i
= 0; i
< extra_frozen
.size(); i
++)
143 setFrozen(extra_frozen
[i
], false);
150 bool SimpSolver::addClause_(vec
<Lit
>& ps
)
153 for (int i
= 0; i
< ps
.size(); i
++)
154 assert(!isEliminated(var(ps
[i
])));
157 int nclauses
= clauses
.size();
159 if (use_rcheck
&& implied(ps
))
162 if (!Solver::addClause_(ps
))
165 if (use_simplification
&& clauses
.size() == nclauses
+ 1){
166 CRef cr
= clauses
.last();
167 const Clause
& c
= ca
[cr
];
169 // NOTE: the clause is added to the queue immediately and then
170 // again during 'gatherTouchedClauses()'. If nothing happens
171 // in between, it will only be checked once. Otherwise, it may
172 // be checked twice unnecessarily. This is an unfortunate
173 // consequence of how backward subsumption is used to mimic
174 // forward subsumption.
175 subsumption_queue
.insert(cr
);
176 for (int i
= 0; i
< c
.size(); i
++){
177 occurs
[var(c
[i
])].push(cr
);
179 touched
[var(c
[i
])] = 1;
181 if (elim_heap
.inHeap(var(c
[i
])))
182 elim_heap
.increase(var(c
[i
]));
190 void SimpSolver::removeClause(CRef cr
)
192 const Clause
& c
= ca
[cr
];
194 if (use_simplification
)
195 for (int i
= 0; i
< c
.size(); i
++){
197 updateElimHeap(var(c
[i
]));
198 occurs
.smudge(var(c
[i
]));
201 Solver::removeClause(cr
);
205 bool SimpSolver::strengthenClause(CRef cr
, Lit l
)
208 assert(decisionLevel() == 0);
209 assert(use_simplification
);
211 // FIX: this is too inefficient but would be nice to have (properly implemented)
212 // if (!find(subsumption_queue, &c))
213 subsumption_queue
.insert(cr
);
219 detachClause(cr
, true);
222 remove(occurs
[var(l
)], cr
);
224 updateElimHeap(var(l
));
227 return c
.size() == 1 ? enqueue(c
[0]) && propagate() == CRef_Undef
: true;
231 // Returns FALSE if clause is always satisfied ('out_clause' should not be used).
232 bool SimpSolver::merge(const Clause
& _ps
, const Clause
& _qs
, Var v
, vec
<Lit
>& out_clause
)
237 bool ps_smallest
= _ps
.size() < _qs
.size();
238 const Clause
& ps
= ps_smallest
? _qs
: _ps
;
239 const Clause
& qs
= ps_smallest
? _ps
: _qs
;
241 for (int i
= 0; i
< qs
.size(); i
++){
242 if (var(qs
[i
]) != v
){
243 for (int j
= 0; j
< ps
.size(); j
++)
244 if (var(ps
[j
]) == var(qs
[i
])){
250 out_clause
.push(qs
[i
]);
255 for (int i
= 0; i
< ps
.size(); i
++)
257 out_clause
.push(ps
[i
]);
263 // Returns FALSE if clause is always satisfied.
264 bool SimpSolver::merge(const Clause
& _ps
, const Clause
& _qs
, Var v
, int& size
)
268 bool ps_smallest
= _ps
.size() < _qs
.size();
269 const Clause
& ps
= ps_smallest
? _qs
: _ps
;
270 const Clause
& qs
= ps_smallest
? _ps
: _qs
;
271 const Lit
* __ps
= (const Lit
*)ps
;
272 const Lit
* __qs
= (const Lit
*)qs
;
276 for (int i
= 0; i
< qs
.size(); i
++){
277 if (var(__qs
[i
]) != v
){
278 for (int j
= 0; j
< ps
.size(); j
++)
279 if (var(__ps
[j
]) == var(__qs
[i
])){
280 if (__ps
[j
] == ~__qs
[i
])
294 void SimpSolver::gatherTouchedClauses()
296 if (n_touched
== 0) return;
299 for (i
= j
= 0; i
< subsumption_queue
.size(); i
++)
300 if (ca
[subsumption_queue
[i
]].mark() == 0)
301 ca
[subsumption_queue
[i
]].mark(2);
303 for (i
= 0; i
< nVars(); i
++)
305 const vec
<CRef
>& cs
= occurs
.lookup(i
);
306 for (j
= 0; j
< cs
.size(); j
++)
307 if (ca
[cs
[j
]].mark() == 0){
308 subsumption_queue
.insert(cs
[j
]);
314 for (i
= 0; i
< subsumption_queue
.size(); i
++)
315 if (ca
[subsumption_queue
[i
]].mark() == 2)
316 ca
[subsumption_queue
[i
]].mark(0);
322 bool SimpSolver::implied(const vec
<Lit
>& c
)
324 assert(decisionLevel() == 0);
326 trail_lim
.push(trail
.size());
327 for (int i
= 0; i
< c
.size(); i
++)
328 if (value(c
[i
]) == l_True
){
331 }else if (value(c
[i
]) != l_False
){
332 assert(value(c
[i
]) == l_Undef
);
333 uncheckedEnqueue(~c
[i
]);
336 bool result
= propagate() != CRef_Undef
;
342 // Backward subsumption + backward subsumption resolution
343 bool SimpSolver::backwardSubsumptionCheck(bool verbose
)
347 int deleted_literals
= 0;
348 assert(decisionLevel() == 0);
350 while (subsumption_queue
.size() > 0 || bwdsub_assigns
< trail
.size()){
352 // Empty subsumption queue and return immediately on user-interrupt:
353 if (asynch_interrupt
){
354 subsumption_queue
.clear();
355 bwdsub_assigns
= trail
.size();
358 // Check top-level assignments by creating a dummy clause and placing it in the queue:
359 if (subsumption_queue
.size() == 0 && bwdsub_assigns
< trail
.size()){
360 Lit l
= trail
[bwdsub_assigns
++];
361 ca
[bwdsub_tmpunit
][0] = l
;
362 ca
[bwdsub_tmpunit
].calcAbstraction();
363 subsumption_queue
.insert(bwdsub_tmpunit
); }
365 CRef cr
= subsumption_queue
.peek(); subsumption_queue
.pop();
368 if (c
.mark()) continue;
370 if (verbose
&& verbosity
>= 2 && cnt
++ % 1000 == 0)
371 printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue
.size(), subsumed
, deleted_literals
);
373 assert(c
.size() > 1 || value(c
[0]) == l_True
); // Unit-clauses should have been propagated before this point.
375 // Find best variable to scan:
376 Var best
= var(c
[0]);
377 for (int i
= 1; i
< c
.size(); i
++)
378 if (occurs
[var(c
[i
])].size() < occurs
[best
].size())
381 // Search all candidates:
382 vec
<CRef
>& _cs
= occurs
.lookup(best
);
383 CRef
* cs
= (CRef
*)_cs
;
385 for (int j
= 0; j
< _cs
.size(); j
++)
388 else if (!ca
[cs
[j
]].mark() && cs
[j
] != cr
&& (subsumption_lim
== -1 || ca
[cs
[j
]].size() < subsumption_lim
)){
389 Lit l
= c
.subsumes(ca
[cs
[j
]]);
392 subsumed
++, removeClause(cs
[j
]);
393 else if (l
!= lit_Error
){
396 if (!strengthenClause(cs
[j
], ~l
))
399 // Did current candidate get deleted from cs? Then check candidate at index j again:
410 bool SimpSolver::asymm(Var v
, CRef cr
)
413 assert(decisionLevel() == 0);
415 if (c
.mark() || satisfied(c
)) return true;
417 trail_lim
.push(trail
.size());
419 for (int i
= 0; i
< c
.size(); i
++)
420 if (var(c
[i
]) != v
&& value(c
[i
]) != l_False
)
421 uncheckedEnqueue(~c
[i
]);
425 if (propagate() != CRef_Undef
){
428 if (!strengthenClause(cr
, l
))
437 bool SimpSolver::asymmVar(Var v
)
439 assert(use_simplification
);
441 const vec
<CRef
>& cls
= occurs
.lookup(v
);
443 if (value(v
) != l_Undef
|| cls
.size() == 0)
446 for (int i
= 0; i
< cls
.size(); i
++)
447 if (!asymm(v
, cls
[i
]))
450 return backwardSubsumptionCheck();
454 static void mkElimClause(vec
<uint32_t>& elimclauses
, Lit x
)
456 elimclauses
.push(toInt(x
));
461 static void mkElimClause(vec
<uint32_t>& elimclauses
, Var v
, Clause
& c
)
463 int first
= elimclauses
.size();
466 // Copy clause to elimclauses-vector. Remember position where the
467 // variable 'v' occurs:
468 for (int i
= 0; i
< c
.size(); i
++){
469 elimclauses
.push(toInt(c
[i
]));
475 // Swap the first literal with the 'v' literal, so that the literal
476 // containing 'v' will occur first in the clause:
477 uint32_t tmp
= elimclauses
[v_pos
];
478 elimclauses
[v_pos
] = elimclauses
[first
];
479 elimclauses
[first
] = tmp
;
481 // Store the length of the clause last:
482 elimclauses
.push(c
.size());
487 bool SimpSolver::eliminateVar(Var v
)
490 assert(!isEliminated(v
));
491 assert(value(v
) == l_Undef
);
493 // Split the occurrences into positive and negative:
495 const vec
<CRef
>& cls
= occurs
.lookup(v
);
497 for (int i
= 0; i
< cls
.size(); i
++)
498 (find(ca
[cls
[i
]], mkLit(v
)) ? pos
: neg
).push(cls
[i
]);
500 // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
501 // clause must exceed the limit on the maximal clause size (if it is set):
506 for (int i
= 0; i
< pos
.size(); i
++)
507 for (int j
= 0; j
< neg
.size(); j
++)
508 if (merge(ca
[pos
[i
]], ca
[neg
[j
]], v
, clause_size
) &&
509 (++cnt
> cls
.size() + grow
|| (clause_lim
!= -1 && clause_size
> clause_lim
)))
512 // Delete and store old clauses:
513 eliminated
[v
] = true;
514 setDecisionVar(v
, false);
517 if (pos
.size() > neg
.size()){
518 for (int i
= 0; i
< neg
.size(); i
++)
519 mkElimClause(elimclauses
, v
, ca
[neg
[i
]]);
520 mkElimClause(elimclauses
, mkLit(v
));
522 for (int i
= 0; i
< pos
.size(); i
++)
523 mkElimClause(elimclauses
, v
, ca
[pos
[i
]]);
524 mkElimClause(elimclauses
, ~mkLit(v
));
527 for (int i
= 0; i
< cls
.size(); i
++)
528 removeClause(cls
[i
]);
530 // Produce clauses in cross product:
531 vec
<Lit
>& resolvent
= add_tmp
;
532 for (int i
= 0; i
< pos
.size(); i
++)
533 for (int j
= 0; j
< neg
.size(); j
++)
534 if (merge(ca
[pos
[i
]], ca
[neg
[j
]], v
, resolvent
) && !addClause_(resolvent
))
537 // Free occurs list for this variable:
538 occurs
[v
].clear(true);
540 // Free watchers lists for this variable, if possible:
541 if (watches
[ mkLit(v
)].size() == 0) watches
[ mkLit(v
)].clear(true);
542 if (watches
[~mkLit(v
)].size() == 0) watches
[~mkLit(v
)].clear(true);
544 return backwardSubsumptionCheck();
548 bool SimpSolver::substitute(Var v
, Lit x
)
551 assert(!isEliminated(v
));
552 assert(value(v
) == l_Undef
);
554 if (!ok
) return false;
556 eliminated
[v
] = true;
557 setDecisionVar(v
, false);
558 const vec
<CRef
>& cls
= occurs
.lookup(v
);
560 vec
<Lit
>& subst_clause
= add_tmp
;
561 for (int i
= 0; i
< cls
.size(); i
++){
562 Clause
& c
= ca
[cls
[i
]];
564 subst_clause
.clear();
565 for (int j
= 0; j
< c
.size(); j
++){
567 subst_clause
.push(var(p
) == v
? x
^ sign(p
) : p
);
570 removeClause(cls
[i
]);
572 if (!addClause_(subst_clause
))
580 void SimpSolver::extendModel()
585 for (i
= elimclauses
.size()-1; i
> 0; i
-= j
){
586 for (j
= elimclauses
[i
--]; j
> 1; j
--, i
--)
587 if (modelValue(toLit(elimclauses
[i
])) != l_False
)
590 x
= toLit(elimclauses
[i
]);
591 model
[var(x
)] = lbool(!sign(x
));
597 bool SimpSolver::eliminate(bool turn_off_elim
)
601 else if (!use_simplification
)
604 // Main simplification loop:
606 while (n_touched
> 0 || bwdsub_assigns
< trail
.size() || elim_heap
.size() > 0){
608 gatherTouchedClauses();
609 // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
610 if ((subsumption_queue
.size() > 0 || bwdsub_assigns
< trail
.size()) &&
611 !backwardSubsumptionCheck(true)){
612 ok
= false; goto cleanup
; }
614 // Empty elim_heap and return immediately on user-interrupt:
615 if (asynch_interrupt
){
616 assert(bwdsub_assigns
== trail
.size());
617 assert(subsumption_queue
.size() == 0);
618 assert(n_touched
== 0);
622 // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
623 for (int cnt
= 0; !elim_heap
.empty(); cnt
++){
624 Var elim
= elim_heap
.removeMin();
626 if (asynch_interrupt
) break;
628 if (isEliminated(elim
) || value(elim
) != l_Undef
) continue;
630 if (verbosity
>= 2 && cnt
% 100 == 0)
631 printf("elimination left: %10d\r", elim_heap
.size());
634 // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
635 bool was_frozen
= frozen
[elim
];
637 if (!asymmVar(elim
)){
638 ok
= false; goto cleanup
; }
639 frozen
[elim
] = was_frozen
; }
641 // At this point, the variable may have been set by assymetric branching, so check it
642 // again. Also, don't eliminate frozen variables:
643 if (use_elim
&& value(elim
) == l_Undef
&& !frozen
[elim
] && !eliminateVar(elim
)){
644 ok
= false; goto cleanup
; }
646 checkGarbage(simp_garbage_frac
);
649 assert(subsumption_queue
.size() == 0);
653 // If no more simplification is needed, free all simplification-related data structures:
655 touched
.clear(true);
658 elim_heap
.clear(true);
659 subsumption_queue
.clear(true);
661 use_simplification
= false;
662 remove_satisfied
= true;
663 ca
.extra_clause_field
= false;
664 max_simp_var
= nVars();
666 // Force full cleanup (this is safe and desirable since it only happens once):
674 if (verbosity
>= 1 && elimclauses
.size() > 0)
675 printf("| Eliminated clauses: %10.2f Mb |\n",
676 double(elimclauses
.size() * sizeof(uint32_t)) / (1024*1024));
682 //=================================================================================================
683 // Garbage Collection methods:
686 void SimpSolver::relocAll(ClauseAllocator
& to
)
688 if (!use_simplification
) return;
692 for (int i
= 0; i
< nVars(); i
++){
694 vec
<CRef
>& cs
= occurs
[i
];
695 for (int j
= 0; j
< cs
.size(); j
++)
699 // Subsumption queue:
701 for (int i
= subsumption_queue
.size(); i
> 0; i
--){
702 CRef cr
= subsumption_queue
.peek(); subsumption_queue
.pop();
703 if (ca
[cr
].mark()) continue;
705 subsumption_queue
.insert(cr
);
710 ca
.reloc(bwdsub_tmpunit
, to
);
714 void SimpSolver::garbageCollect()
716 // Initialize the next region to a size corresponding to the estimated utilization degree. This
717 // is not precise but should avoid some unnecessary reallocations for the new region:
718 ClauseAllocator
to(ca
.size() - ca
.wasted());
720 to
.extra_clause_field
= ca
.extra_clause_field
; // NOTE: this is important to keep (or lose) the extra fields.
722 Solver::relocAll(to
);
724 printf("| Garbage collection: %12d bytes => %12d bytes |\n",
725 ca
.size()*ClauseAllocator::Unit_Size
, to
.size()*ClauseAllocator::Unit_Size
);