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 assumptionsSize () const; // The current number of variables.
139 int nFreeVars () const;
141 inline char valuePhase(Var v) {return polarity[v];}
144 void setIncrementalMode();
145 void initNbInitialVars(int nb);
146 void printIncrementalStats();
147 bool isIncremental();
148 // Resource contraints:
150 void setConfBudget(int64_t x);
151 void setPropBudget(int64_t x);
153 void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
154 void clearInterrupt(); // Clear interrupt indicator flag.
158 virtual void garbageCollect();
159 void checkGarbage(double gf);
162 // Extra results: (read-only member variable)
164 vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
165 vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions),
166 // this vector represent the final conflict clause expressed in the assumptions.
168 // Mode of operation:
171 int verbEveryConflicts;
174 // Constants For restarts
178 double sizeTrailQueue;
180 // Constants for reduce DB
183 int specialIncReduceDB;
184 unsigned int lbLBDFrozenClause;
186 // Constant for reducing clause
187 int lbSizeMinimizingClause;
188 unsigned int lbLBDMinimizingClause;
190 // Constant for heuristic
192 double max_var_decay;
194 double random_var_freq;
196 int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
197 int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
198 bool rnd_pol; // Use random polarities for branching heuristics.
199 bool rnd_init_act; // Initialize variable activities with a small random value.
201 // Constant for Memory managment
202 double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
204 // Certified UNSAT ( Thanks to Marijn Heule)
205 FILE* certifiedOutput;
210 uint32_t panicModeLastRemoved, panicModeLastRemovedShared;
212 bool useUnaryWatched; // Enable unary watched literals
213 bool promoteOneWatchedClause; // One watched clauses are promotted to two watched clauses if found empty
215 // Functions useful for multithread solving
216 // Useless in the sequential case
217 // Overide in ParallelSolver
218 virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl);
219 virtual bool parallelImportClauses(); // true if the empty clause was received
220 virtual void parallelImportUnaryClauses();
221 virtual void parallelExportUnaryClause(Lit p);
222 virtual void parallelExportClauseDuringSearch(Clause &c);
223 virtual bool parallelJobIsFinished();
224 virtual bool panicModeIsEnabled();
228 // Statistics: (read-only member variable)
229 uint64_t nbPromoted; // Number of clauses from unary to binary watch scheme
230 uint64_t originalClausesSeen; // Number of original clauses seen
231 uint64_t sumDecisionLevels;
233 uint64_t nbRemovedClauses,nbRemovedUnaryWatchedClauses, nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart;
234 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
239 // Helper structures:
241 struct VarData { CRef reason; int level; };
242 static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
247 Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
248 bool operator==(const Watcher& w) const { return cref == w.cref; }
249 bool operator!=(const Watcher& w) const { return cref != w.cref; }
250 /* Watcher &operator=(Watcher w) {
252 this->blocker = w.blocker;
258 struct WatcherDeleted
260 const ClauseAllocator& ca;
261 WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
262 bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
266 const vec<double>& activity;
267 bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
268 VarOrderLt(const vec<double>& act) : activity(act) { }
275 bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
276 double cla_inc; // Amount to bump next clause with.
277 vec<double> activity; // A heuristic measurement of the activity of a variable.
278 double var_inc; // Amount to bump next variable with.
279 OccLists<Lit, vec<Watcher>, WatcherDeleted>
280 watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
281 OccLists<Lit, vec<Watcher>, WatcherDeleted>
282 watchesBin; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
283 OccLists<Lit, vec<Watcher>, WatcherDeleted>
284 unaryWatches; // Unary watch scheme (clauses are seen when they become empty
285 vec<CRef> clauses; // List of problem clauses.
286 vec<CRef> learnts; // List of learnt clauses.
287 vec<CRef> unaryWatchedClauses; // List of imported clauses (after the purgatory) // TODO put inside ParallelSolver
289 vec<lbool> assigns; // The current assignments.
290 vec<char> polarity; // The preferred polarity of each variable.
291 vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
292 vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
294 vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
295 vec<VarData> vardata; // Stores reason and level for each variable.
296 int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
297 int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
298 int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
299 vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
300 Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
301 double progress_estimate;// Set by 'search()'.
302 bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
304 int reduceOnSizeSize; // See XMinisat paper
305 vec<unsigned int> permDiff; // permDiff[var] contains the current conflict number... Used to count the number of LBD
308 // UPDATEVARACTIVITY trick (see competition'09 companion paper)
309 vec<Lit> lastDecisionLevel;
313 int nbclausesbeforereduce; // To know when it is time to reduce clause database
315 // Used for restart strategies
316 bqueue<unsigned int> trailQueue,lbdQueue; // Bounded queues for restarts.
317 float sumLBD; // used to compute the global average of LBD. Restarts...
319 CRef lastLearntClause;
322 // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
323 // used, exept 'seen' wich is used in several places.
326 vec<Lit> analyze_stack;
327 vec<Lit> analyze_toclear;
331 // Initial reduceDB strategy
333 double learntsize_adjust_confl;
334 int learntsize_adjust_cnt;
336 // Resource contraints:
338 int64_t conflict_budget; // -1 means no budget.
339 int64_t propagation_budget; // -1 means no budget.
340 bool asynch_interrupt;
342 // Variables added for incremental mode
343 int incremental; // Use incremental SAT Solver
344 int nbVarsInitialFormula; // nb VAR in formula without assumptions (incremental SAT)
345 double totalTime4Sat,totalTime4Unsat;
346 int nbSatCalls,nbUnsatCalls;
347 vec<int> assumptionPositions,initialPositions;
350 // Main internal methods:
352 void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
353 Lit pickBranchLit (); // Return the next decision variable.
354 void newDecisionLevel (); // Begins a new decision level.
355 void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined.
356 bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
357 CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause.
358 CRef propagateUnaryWatches(Lit p); // Perform propagation on unary watches of p, can find only conflicts
359 void cancelUntil (int level); // Backtrack until a certain level.
360 void analyze (CRef confl, vec<Lit>& out_learnt, vec<Lit> & selectors, int& out_btlevel,unsigned int &nblevels,unsigned int &szWithoutSelectors); // (bt = backtrack)
361 void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
362 bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
363 lbool search (int nof_conflicts); // Search for a given number of conflicts.
364 virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false); // Main solve method (assumptions given in 'assumptions').
365 virtual void reduceDB (); // Reduce the set of learnt clauses.
366 void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
367 void rebuildOrderHeap ();
369 // Maintaining Variable/Clause activity:
371 void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
372 void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value.
373 void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
374 void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
375 void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value.
377 // Operations on clauses:
379 void attachClause (CRef cr); // Attach a clause to watcher lists.
380 void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists.
381 void detachClausePurgatory(CRef cr, bool strict = false);
382 void attachClausePurgatory(CRef cr);
383 void removeClause (CRef cr, bool inPurgatory = false); // Detach and free a clause.
384 bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
385 bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
387 unsigned int computeLBD(const vec<Lit> & lits,int end=-1);
388 unsigned int computeLBD(const Clause &c);
389 void minimisationWithBinaryResolution(vec<Lit> &out_learnt);
391 virtual void relocAll (ClauseAllocator& to);
395 int decisionLevel () const; // Gives the current decisionlevel.
396 uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
397 CRef reason (Var x) const;
398 int level (Var x) const;
399 double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
400 bool withinBudget () const;
401 inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
406 // Returns a random float 0 <= x < 1. Seed must never be 0.
407 static inline double drand(double& seed) {
409 int q = (int)(seed / 2147483647);
410 seed -= (double)q * 2147483647;
411 return seed / 2147483647; }
413 // Returns a random integer 0 <= x < size. Seed must never be 0.
414 static inline int irand(double& seed, int size) {
415 return (int)(drand(seed) * size); }
419 //=================================================================================================
420 // Implementation of inline methods:
422 inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
423 inline int Solver::level (Var x) const { return vardata[x].level; }
425 inline void Solver::insertVarOrder(Var x) {
426 if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
428 inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
429 inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
430 inline void Solver::varBumpActivity(Var v, double inc) {
431 if ( (activity[v] += inc) > 1e100 ) {
433 for (int i = 0; i < nVars(); i++)
434 activity[i] *= 1e-100;
437 // Update order_heap with respect to new activity:
438 if (order_heap.inHeap(v))
439 order_heap.decrease(v); }
441 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
442 inline void Solver::claBumpActivity (Clause& c) {
443 if ( (c.activity() += cla_inc) > 1e20 ) {
445 for (int i = 0; i < learnts.size(); i++)
446 ca[learnts[i]].activity() *= 1e-20;
447 cla_inc *= 1e-20; } }
449 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
450 inline void Solver::checkGarbage(double gf){
451 if (ca.wasted() > ca.size() * gf)
454 // NOTE: enqueue does not set the ok flag! (only public methods do)
455 inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
456 inline bool Solver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
457 inline bool Solver::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); }
458 inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
459 inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
460 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); }
461 inline bool Solver::locked (const Clause& c) const {
463 return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c;
465 (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
467 (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
469 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
471 inline int Solver::decisionLevel () const { return trail_lim.size(); }
472 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
473 inline lbool Solver::value (Var x) const { return assigns[x]; }
474 inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
475 inline lbool Solver::modelValue (Var x) const { return model[x]; }
476 inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
477 inline int Solver::nAssigns () const { return trail.size(); }
478 inline int Solver::nClauses () const { return clauses.size(); }
479 inline int Solver::nLearnts () const { return learnts.size(); }
480 inline int Solver::nVars () const { return vardata.size(); }
481 inline int Solver::assumptionsSize () const { return assumptions.size(); }
482 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
483 inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
484 inline void Solver::setDecisionVar(Var v, bool b)
486 if ( b && !decision[v]) dec_vars++;
487 else if (!b && decision[v]) dec_vars--;
492 inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
493 inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
494 inline void Solver::interrupt(){ asynch_interrupt = true; }
495 inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
496 inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
497 inline bool Solver::withinBudget() const {
498 return !asynch_interrupt &&
499 (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
500 (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
502 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
503 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
504 // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
505 inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; }
506 inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
507 inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
508 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; }
509 inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
510 inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
511 inline bool Solver::okay () const { return ok; }
513 inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
514 inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
515 inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
516 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); }
520 //=================================================================================================
524 inline void Solver::printLit(Lit l)
526 printf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
530 inline void Solver::printClause(CRef cr)
533 for (int i = 0; i < c.size(); i++){
539 inline void Solver::printInitialClause(CRef cr)
542 for (int i = 0; i < c.size(); i++){
543 if(!isSelector(var(c[i]))) {
550 //=================================================================================================
555 reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {
558 bool operator()(CRef x, CRef y) {
560 // Main criteria... Like in MiniSat we keep all binary clauses
561 if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
563 if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
564 if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
566 // Second one based on literal block distance
567 if (ca[x].lbd() > ca[y].lbd()) return 1;
568 if (ca[x].lbd() < ca[y].lbd()) return 0;
571 // Finally we can use old activity or size, we choose the last one
572 return ca[x].activity() < ca[y].activity();
573 //return x->size() < y->size();
575 //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }