1 /***************************************************************************************[Solver.h]
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 **************************************************************************************************/
50 #ifndef Glucose_Solver_h
51 #define Glucose_Solver_h
55 #include "utils/Options.h"
56 #include "core/SolverTypes.h"
57 #include "core/BoundedQueue.h"
58 #include "core/Constants.h"
59 #include "mtl/Clone.h"
64 //=================================================================================================
65 // Solver -- the main class:
67 class Solver : public Clone {
69 friend class SolverConfiguration;
73 // Constructor/Destructor:
76 Solver(const Solver &s);
83 virtual Clone* clone() const {
84 return new Solver(*this);
87 // Problem specification:
89 virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
90 bool addClause (const vec<Lit>& ps); // Add a clause to the solver.
91 bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
92 bool addClause (Lit p); // Add a unit clause to the solver.
93 bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
94 bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
95 virtual bool addClause_( vec<Lit>& ps); // Add a clause to the solver without making superflous internal copy. Will
96 // change the passed vector 'ps'.
100 bool simplify (); // Removes already satisfied clauses.
101 bool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
102 lbool solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
103 bool solve (); // Search without assumptions.
104 bool solve (Lit p); // Search for a model that respects a single assumption.
105 bool solve (Lit p, Lit q); // Search for a model that respects two assumptions.
106 bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions.
107 bool okay () const; // FALSE means solver is in a conflicting state
109 // Convenience versions of 'toDimacs()':
110 void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
111 void toDimacs (const char *file, const vec<Lit>& assumps);
112 void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
113 void toDimacs (const char* file);
114 void toDimacs (const char* file, Lit p);
115 void toDimacs (const char* file, Lit p, Lit q);
116 void toDimacs (const char* file, Lit p, Lit q, Lit r);
118 // Display clauses and literals
119 void printLit(Lit l);
120 void printClause(CRef c);
121 void printInitialClause(CRef c);
125 void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
126 void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
130 lbool value (Var x) const; // The current value of a variable.
131 lbool value (Lit p) const; // The current value of a literal.
132 lbool modelValue (Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
133 lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
134 int nAssigns () const; // The current number of assigned literals.
135 int nClauses () const; // The current number of original clauses.
136 int nLearnts () const; // The current number of learnt clauses.
137 int nVars () const; // The current number of variables.
138 int nFreeVars () const;
140 inline char valuePhase(Var v) {return polarity[v];}
143 void setIncrementalMode();
144 void initNbInitialVars(int nb);
145 void printIncrementalStats();
146 bool isIncremental();
147 // Resource contraints:
149 void setConfBudget(int64_t x);
150 void setPropBudget(int64_t x);
152 void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
153 void clearInterrupt(); // Clear interrupt indicator flag.
157 virtual void garbageCollect();
158 void checkGarbage(double gf);
161 // Extra results: (read-only member variable)
163 vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
164 vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions),
165 // this vector represent the final conflict clause expressed in the assumptions.
167 // Mode of operation:
170 int verbEveryConflicts;
173 // Constants For restarts
177 double sizeTrailQueue;
179 // Constants for reduce DB
182 int specialIncReduceDB;
183 unsigned int lbLBDFrozenClause;
185 // Constant for reducing clause
186 int lbSizeMinimizingClause;
187 unsigned int lbLBDMinimizingClause;
189 // Constant for heuristic
191 double max_var_decay;
193 double random_var_freq;
195 int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
196 int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
197 bool rnd_pol; // Use random polarities for branching heuristics.
198 bool rnd_init_act; // Initialize variable activities with a small random value.
200 // Constant for Memory managment
201 double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
203 // Certified UNSAT ( Thanks to Marijn Heule)
204 FILE* certifiedOutput;
209 uint32_t panicModeLastRemoved, panicModeLastRemovedShared;
211 bool useUnaryWatched; // Enable unary watched literals
212 bool promoteOneWatchedClause; // One watched clauses are promotted to two watched clauses if found empty
214 // Functions useful for multithread solving
215 // Useless in the sequential case
216 // Overide in ParallelSolver
217 virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl);
218 virtual bool parallelImportClauses(); // true if the empty clause was received
219 virtual void parallelImportUnaryClauses();
220 virtual void parallelExportUnaryClause(Lit p);
221 virtual void parallelExportClauseDuringSearch(Clause &c);
222 virtual bool parallelJobIsFinished();
223 virtual bool panicModeIsEnabled();
227 // Statistics: (read-only member variable)
228 uint64_t nbPromoted; // Number of clauses from unary to binary watch scheme
229 uint64_t originalClausesSeen; // Number of original clauses seen
230 uint64_t sumDecisionLevels;
232 uint64_t nbRemovedClauses,nbRemovedUnaryWatchedClauses, nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart;
233 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
238 // Helper structures:
240 struct VarData { CRef reason; int level; };
241 static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
246 Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
247 bool operator==(const Watcher& w) const { return cref == w.cref; }
248 bool operator!=(const Watcher& w) const { return cref != w.cref; }
249 /* Watcher &operator=(Watcher w) {
251 this->blocker = w.blocker;
257 struct WatcherDeleted
259 const ClauseAllocator& ca;
260 WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
261 bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
265 const vec<double>& activity;
266 bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
267 VarOrderLt(const vec<double>& act) : activity(act) { }
274 bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
275 double cla_inc; // Amount to bump next clause with.
276 vec<double> activity; // A heuristic measurement of the activity of a variable.
277 double var_inc; // Amount to bump next variable with.
278 OccLists<Lit, vec<Watcher>, WatcherDeleted>
279 watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
280 OccLists<Lit, vec<Watcher>, WatcherDeleted>
281 watchesBin; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
282 OccLists<Lit, vec<Watcher>, WatcherDeleted>
283 unaryWatches; // Unary watch scheme (clauses are seen when they become empty
284 vec<CRef> clauses; // List of problem clauses.
285 vec<CRef> learnts; // List of learnt clauses.
286 vec<CRef> unaryWatchedClauses; // List of imported clauses (after the purgatory) // TODO put inside ParallelSolver
288 vec<lbool> assigns; // The current assignments.
289 vec<char> polarity; // The preferred polarity of each variable.
290 vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
291 vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
293 vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
294 vec<VarData> vardata; // Stores reason and level for each variable.
295 int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
296 int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
297 int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
298 vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
299 Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
300 double progress_estimate;// Set by 'search()'.
301 bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
303 int reduceOnSizeSize; // See XMinisat paper
304 vec<unsigned int> permDiff; // permDiff[var] contains the current conflict number... Used to count the number of LBD
307 // UPDATEVARACTIVITY trick (see competition'09 companion paper)
308 vec<Lit> lastDecisionLevel;
312 int nbclausesbeforereduce; // To know when it is time to reduce clause database
314 // Used for restart strategies
315 bqueue<unsigned int> trailQueue,lbdQueue; // Bounded queues for restarts.
316 float sumLBD; // used to compute the global average of LBD. Restarts...
318 CRef lastLearntClause;
321 // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
322 // used, exept 'seen' wich is used in several places.
325 vec<Lit> analyze_stack;
326 vec<Lit> analyze_toclear;
330 // Initial reduceDB strategy
332 double learntsize_adjust_confl;
333 int learntsize_adjust_cnt;
335 // Resource contraints:
337 int64_t conflict_budget; // -1 means no budget.
338 int64_t propagation_budget; // -1 means no budget.
339 bool asynch_interrupt;
341 // Variables added for incremental mode
342 int incremental; // Use incremental SAT Solver
343 int nbVarsInitialFormula; // nb VAR in formula without assumptions (incremental SAT)
344 double totalTime4Sat,totalTime4Unsat;
345 int nbSatCalls,nbUnsatCalls;
346 vec<int> assumptionPositions,initialPositions;
349 // Main internal methods:
351 void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
352 Lit pickBranchLit (); // Return the next decision variable.
353 void newDecisionLevel (); // Begins a new decision level.
354 void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined.
355 bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
356 CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause.
357 CRef propagateUnaryWatches(Lit p); // Perform propagation on unary watches of p, can find only conflicts
358 void cancelUntil (int level); // Backtrack until a certain level.
359 void analyze (CRef confl, vec<Lit>& out_learnt, vec<Lit> & selectors, int& out_btlevel,unsigned int &nblevels,unsigned int &szWithoutSelectors); // (bt = backtrack)
360 void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
361 bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
362 lbool search (int nof_conflicts); // Search for a given number of conflicts.
363 virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false); // Main solve method (assumptions given in 'assumptions').
364 virtual void reduceDB (); // Reduce the set of learnt clauses.
365 void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
366 void rebuildOrderHeap ();
368 // Maintaining Variable/Clause activity:
370 void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
371 void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value.
372 void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
373 void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
374 void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value.
376 // Operations on clauses:
378 void attachClause (CRef cr); // Attach a clause to watcher lists.
379 void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists.
380 void detachClausePurgatory(CRef cr, bool strict = false);
381 void attachClausePurgatory(CRef cr);
382 void removeClause (CRef cr, bool inPurgatory = false); // Detach and free a clause.
383 bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
384 bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
386 unsigned int computeLBD(const vec<Lit> & lits,int end=-1);
387 unsigned int computeLBD(const Clause &c);
388 void minimisationWithBinaryResolution(vec<Lit> &out_learnt);
390 virtual void relocAll (ClauseAllocator& to);
394 int decisionLevel () const; // Gives the current decisionlevel.
395 uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
396 CRef reason (Var x) const;
397 int level (Var x) const;
398 double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
399 bool withinBudget () const;
400 inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
405 // Returns a random float 0 <= x < 1. Seed must never be 0.
406 static inline double drand(double& seed) {
408 int q = (int)(seed / 2147483647);
409 seed -= (double)q * 2147483647;
410 return seed / 2147483647; }
412 // Returns a random integer 0 <= x < size. Seed must never be 0.
413 static inline int irand(double& seed, int size) {
414 return (int)(drand(seed) * size); }
418 //=================================================================================================
419 // Implementation of inline methods:
421 inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
422 inline int Solver::level (Var x) const { return vardata[x].level; }
424 inline void Solver::insertVarOrder(Var x) {
425 if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
427 inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
428 inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
429 inline void Solver::varBumpActivity(Var v, double inc) {
430 if ( (activity[v] += inc) > 1e100 ) {
432 for (int i = 0; i < nVars(); i++)
433 activity[i] *= 1e-100;
436 // Update order_heap with respect to new activity:
437 if (order_heap.inHeap(v))
438 order_heap.decrease(v); }
440 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
441 inline void Solver::claBumpActivity (Clause& c) {
442 if ( (c.activity() += cla_inc) > 1e20 ) {
444 for (int i = 0; i < learnts.size(); i++)
445 ca[learnts[i]].activity() *= 1e-20;
446 cla_inc *= 1e-20; } }
448 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
449 inline void Solver::checkGarbage(double gf){
450 if (ca.wasted() > ca.size() * gf)
453 // NOTE: enqueue does not set the ok flag! (only public methods do)
454 inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
455 inline bool Solver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
456 inline bool Solver::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); }
457 inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
458 inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
459 inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
460 inline bool Solver::locked (const Clause& c) const {
462 return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c;
464 (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
466 (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
468 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
470 inline int Solver::decisionLevel () const { return trail_lim.size(); }
471 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
472 inline lbool Solver::value (Var x) const { return assigns[x]; }
473 inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
474 inline lbool Solver::modelValue (Var x) const { return model[x]; }
475 inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
476 inline int Solver::nAssigns () const { return trail.size(); }
477 inline int Solver::nClauses () const { return clauses.size(); }
478 inline int Solver::nLearnts () const { return learnts.size(); }
479 inline int Solver::nVars () const { return vardata.size(); }
480 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
481 inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
482 inline void Solver::setDecisionVar(Var v, bool b)
484 if ( b && !decision[v]) dec_vars++;
485 else if (!b && decision[v]) dec_vars--;
490 inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
491 inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
492 inline void Solver::interrupt(){ asynch_interrupt = true; }
493 inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
494 inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
495 inline bool Solver::withinBudget() const {
496 return !asynch_interrupt &&
497 (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
498 (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
500 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
501 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
502 // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
503 inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; }
504 inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
505 inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
506 inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
507 inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
508 inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
509 inline bool Solver::okay () const { return ok; }
511 inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
512 inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
513 inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
514 inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
518 //=================================================================================================
522 inline void Solver::printLit(Lit l)
524 printf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
528 inline void Solver::printClause(CRef cr)
531 for (int i = 0; i < c.size(); i++){
537 inline void Solver::printInitialClause(CRef cr)
540 for (int i = 0; i < c.size(); i++){
541 if(!isSelector(var(c[i]))) {
548 //=================================================================================================
553 reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {
556 bool operator()(CRef x, CRef y) {
558 // Main criteria... Like in MiniSat we keep all binary clauses
559 if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
561 if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
562 if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
564 // Second one based on literal block distance
565 if (ca[x].lbd() > ca[y].lbd()) return 1;
566 if (ca[x].lbd() < ca[y].lbd()) return 0;
569 // Finally we can use old activity or size, we choose the last one
570 return ca[x].activity() < ca[y].activity();
571 //return x->size() < y->size();
573 //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }