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
6
7 Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
8 CRIL - Univ. Artois, France
9 Labri - Univ. Bordeaux, France
10
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).
14
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:
20
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).
27
28
29 --------------- Original Minisat Copyrights
30
31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
32 Copyright (c) 2007-2010, Niklas Sorensson
33
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:
39
40 The above copyright notice and this permission notice shall be included in all copies or
41 substantial portions of the Software.
42
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 **************************************************************************************************/
49
50 #ifndef Glucose_Solver_h
51 #define Glucose_Solver_h
52
53 #include "mtl/Heap.h"
54 #include "mtl/Alg.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"
60 #include "core/SolverStats.h"
61
62
63 namespace Glucose {
64 // Core stats
65
66 enum CoreStats {
67 sumResSeen,
68 sumRes,
69 sumTrail,
70 nbPromoted,
71 originalClausesSeen,
72 sumDecisionLevels,
73 nbPermanentLearnts,
74 nbRemovedClauses,
75 nbRemovedUnaryWatchedClauses,
76 nbReducedClauses,
77 nbDL2,
78 nbBin,
79 nbUn,
80 nbReduceDB,
81 rnd_decisions,
82 nbstopsrestarts,
83 nbstopsrestartssame,
84 lastblockatrestart,
85 dec_vars,
86 clauses_literals,
87 learnts_literals,
88 max_literals,
89 tot_literals,
90 noDecisionConflict
91 } ;
92
93 #define coreStatsSize 24
94 //=================================================================================================
95 // Solver -- the main class:
96
97 class Solver : public Clone {
98
99 friend class SolverConfiguration;
100
101 public:
102
103 // Constructor/Destructor:
104 //
105 Solver();
106 Solver(const Solver &s);
107
108 virtual ~Solver();
109
110 /**
111 * Clone function
112 */
clone()113 virtual Clone* clone() const {
114 return new Solver(*this);
115 }
116
117 // Problem specification:
118 //
119 virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
120 bool addClause (const vec<Lit>& ps); // Add a clause to the solver.
121 bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
122 bool addClause (Lit p); // Add a unit clause to the solver.
123 bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
124 bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
125 virtual bool addClause_( vec<Lit>& ps); // Add a clause to the solver without making superflous internal copy. Will
126 // change the passed vector 'ps'.
127 // Solving:
128 //
129 bool simplify (); // Removes already satisfied clauses.
130 bool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
131 lbool solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
132 bool solve (); // Search without assumptions.
133 bool solve (Lit p); // Search for a model that respects a single assumption.
134 bool solve (Lit p, Lit q); // Search for a model that respects two assumptions.
135 bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions.
136 bool okay () const; // FALSE means solver is in a conflicting state
137
138 // Convenience versions of 'toDimacs()':
139 void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
140 void toDimacs (const char *file, const vec<Lit>& assumps);
141 void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
142 void toDimacs (const char* file);
143 void toDimacs (const char* file, Lit p);
144 void toDimacs (const char* file, Lit p, Lit q);
145 void toDimacs (const char* file, Lit p, Lit q, Lit r);
146
147 // Display clauses and literals
148 void printLit(Lit l);
149 void printClause(CRef c);
150 void printInitialClause(CRef c);
151
152 // Variable mode:
153 //
154 void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
155 void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
156
157 // Read state:
158 //
159 lbool value (Var x) const; // The current value of a variable.
160 lbool value (Lit p) const; // The current value of a literal.
161 lbool modelValue (Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
162 lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
163 int nAssigns () const; // The current number of assigned literals.
164 int nClauses () const; // The current number of original clauses.
165 int nLearnts () const; // The current number of learnt clauses.
166 int nVars () const; // The current number of variables.
167 int nFreeVars () ;
168
valuePhase(Var v)169 inline char valuePhase(Var v) {return polarity[v];}
170
171 // Incremental mode
172 void setIncrementalMode();
173 void initNbInitialVars(int nb);
174 void printIncrementalStats();
175 bool isIncremental();
176 // Resource contraints:
177 //
178 void setConfBudget(int64_t x);
179 void setPropBudget(int64_t x);
180 void budgetOff();
181 void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
182 void clearInterrupt(); // Clear interrupt indicator flag.
183
184 // Memory managment:
185 //
186 virtual void garbageCollect();
187 void checkGarbage(double gf);
188 void checkGarbage();
189
190 // Extra results: (read-only member variable)
191 //
192 vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
193 vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions),
194 // this vector represent the final conflict clause expressed in the assumptions.
195
196 // Mode of operation:
197 //
198 int verbosity;
199 int verbEveryConflicts;
200 int showModel;
201
202 // Constants For restarts
203 double K;
204 double R;
205 double sizeLBDQueue;
206 double sizeTrailQueue;
207
208 // Constants for reduce DB
209 int firstReduceDB;
210 int incReduceDB;
211 int specialIncReduceDB;
212 unsigned int lbLBDFrozenClause;
213 bool chanseokStrategy;
214 int coLBDBound; // Keep all learnts with lbd<=coLBDBound
215 // Constant for reducing clause
216 int lbSizeMinimizingClause;
217 unsigned int lbLBDMinimizingClause;
218
219 // Constant for heuristic
220 double var_decay;
221 double max_var_decay;
222 double clause_decay;
223 double random_var_freq;
224 double random_seed;
225 int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
226 int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
227 bool rnd_pol; // Use random polarities for branching heuristics.
228 bool rnd_init_act; // Initialize variable activities with a small random value.
229 bool randomizeFirstDescent; // the first decisions (until first cnflict) are made randomly
230 // Useful for syrup!
231
232 // Constant for Memory managment
233 double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
234
235 // Certified UNSAT ( Thanks to Marijn Heule
236 // New in 2016 : proof in DRAT format, possibility to use binary output
237 FILE* certifiedOutput;
238 bool certifiedUNSAT;
239 bool vbyte;
240
241 void write_char (unsigned char c);
242 void write_lit (int n);
243
244
245 // Panic mode.
246 // Save memory
247 uint32_t panicModeLastRemoved, panicModeLastRemovedShared;
248
249 bool useUnaryWatched; // Enable unary watched literals
250 bool promoteOneWatchedClause; // One watched clauses are promotted to two watched clauses if found empty
251
252 // Functions useful for multithread solving
253 // Useless in the sequential case
254 // Overide in ParallelSolver
255 virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl);
256 virtual bool parallelImportClauses(); // true if the empty clause was received
257 virtual void parallelImportUnaryClauses();
258 virtual void parallelExportUnaryClause(Lit p);
259 virtual void parallelExportClauseDuringSearch(Clause &c);
260 virtual bool parallelJobIsFinished();
261 virtual bool panicModeIsEnabled();
262
263
264 double luby(double y, int x);
265
266 // Statistics
267 vec<uint64_t> stats;
268
269 // Important stats completely related to search. Keep here
270 uint64_t solves,starts,decisions,propagations,conflicts,conflictsRestarts;
271
272 protected:
273
274 long curRestart;
275
276 // Alpha variables
277 bool glureduce;
278 uint32_t restart_inc;
279 bool luby_restart;
280 bool adaptStrategies;
281 uint32_t luby_restart_factor;
282 bool randomize_on_restarts, fixed_randomize_on_restarts, newDescent;
283 uint32_t randomDescentAssignments;
284 bool forceUnsatOnNewDescent;
285 // Helper structures:
286 //
287 struct VarData { CRef reason; int level; };
mkVarData(CRef cr,int l)288 static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
289
290 struct Watcher {
291 CRef cref;
292 Lit blocker;
WatcherWatcher293 Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
294 bool operator==(const Watcher& w) const { return cref == w.cref; }
295 bool operator!=(const Watcher& w) const { return cref != w.cref; }
296 /* Watcher &operator=(Watcher w) {
297 this->cref = w.cref;
298 this->blocker = w.blocker;
299 return *this;
300 }
301 */
302 };
303
304 struct WatcherDeleted
305 {
306 const ClauseAllocator& ca;
WatcherDeletedWatcherDeleted307 WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
operatorWatcherDeleted308 bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
309 };
310
311 struct VarOrderLt {
312 const vec<double>& activity;
operatorVarOrderLt313 bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
VarOrderLtVarOrderLt314 VarOrderLt(const vec<double>& act) : activity(act) { }
315 };
316
317
318 // Solver state:
319 //
320 int lastIndexRed;
321 bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
322 double cla_inc; // Amount to bump next clause with.
323 vec<double> activity; // A heuristic measurement of the activity of a variable.
324 double var_inc; // Amount to bump next variable with.
325 OccLists<Lit, vec<Watcher>, WatcherDeleted>
326 watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
327 OccLists<Lit, vec<Watcher>, WatcherDeleted>
328 watchesBin; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
329 OccLists<Lit, vec<Watcher>, WatcherDeleted>
330 unaryWatches; // Unary watch scheme (clauses are seen when they become empty
331 vec<CRef> clauses; // List of problem clauses.
332 vec<CRef> learnts; // List of learnt clauses.
333 vec<CRef> permanentLearnts; // The list of learnts clauses kept permanently
334 vec<CRef> unaryWatchedClauses; // List of imported clauses (after the purgatory) // TODO put inside ParallelSolver
335
336 vec<lbool> assigns; // The current assignments.
337 vec<char> polarity; // The preferred polarity of each variable.
338 vec<char> forceUNSAT;
339 void bumpForceUNSAT(Lit q); // Handles the forces
340
341 vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
342 vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
343 vec<int> nbpos;
344 vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
345 vec<VarData> vardata; // Stores reason and level for each variable.
346 int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
347 int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
348 int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
349 vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
350 Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
351 double progress_estimate;// Set by 'search()'.
352 bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
353 vec<unsigned int> permDiff; // permDiff[var] contains the current conflict number... Used to count the number of LBD
354
355
356 // UPDATEVARACTIVITY trick (see competition'09 companion paper)
357 vec<Lit> lastDecisionLevel;
358
359 ClauseAllocator ca;
360
361 int nbclausesbeforereduce; // To know when it is time to reduce clause database
362
363 // Used for restart strategies
364 bqueue<unsigned int> trailQueue,lbdQueue; // Bounded queues for restarts.
365 float sumLBD; // used to compute the global average of LBD. Restarts...
366 int sumAssumptions;
367 CRef lastLearntClause;
368
369
370 // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
371 // used, exept 'seen' wich is used in several places.
372 //
373 vec<char> seen;
374 vec<Lit> analyze_stack;
375 vec<Lit> analyze_toclear;
376 vec<Lit> add_tmp;
377 unsigned int MYFLAG;
378
379 // Initial reduceDB strategy
380 double max_learnts;
381 double learntsize_adjust_confl;
382 int learntsize_adjust_cnt;
383
384 // Resource contraints:
385 //
386 int64_t conflict_budget; // -1 means no budget.
387 int64_t propagation_budget; // -1 means no budget.
388 bool asynch_interrupt;
389
390 // Variables added for incremental mode
391 int incremental; // Use incremental SAT Solver
392 int nbVarsInitialFormula; // nb VAR in formula without assumptions (incremental SAT)
393 double totalTime4Sat,totalTime4Unsat;
394 int nbSatCalls,nbUnsatCalls;
395 vec<int> assumptionPositions,initialPositions;
396
397
398 // Main internal methods:
399 //
400 void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
401 Lit pickBranchLit (); // Return the next decision variable.
402 void newDecisionLevel (); // Begins a new decision level.
403 void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined.
404 bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
405 CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause.
406 CRef propagateUnaryWatches(Lit p); // Perform propagation on unary watches of p, can find only conflicts
407 void cancelUntil (int level); // Backtrack until a certain level.
408 void analyze (CRef confl, vec<Lit>& out_learnt, vec<Lit> & selectors, int& out_btlevel,unsigned int &nblevels,unsigned int &szWithoutSelectors); // (bt = backtrack)
409 void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
410 bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
411 lbool search (int nof_conflicts); // Search for a given number of conflicts.
412 virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false); // Main solve method (assumptions given in 'assumptions').
413 virtual void reduceDB (); // Reduce the set of learnt clauses.
414 void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
415 void rebuildOrderHeap ();
416
417 void adaptSolver(); // Adapt solver strategies
418
419 // Maintaining Variable/Clause activity:
420 //
421 void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
422 void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value.
423 void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
424 void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
425 void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value.
426
427 // Operations on clauses:
428 //
429 void attachClause (CRef cr); // Attach a clause to watcher lists.
430 void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists.
431 void detachClausePurgatory(CRef cr, bool strict = false);
432 void attachClausePurgatory(CRef cr);
433 void removeClause (CRef cr, bool inPurgatory = false); // Detach and free a clause.
434 bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
435 bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
436
437 template <typename T> unsigned int computeLBD(const T & lits,int end=-1);
438 void minimisationWithBinaryResolution(vec<Lit> &out_learnt);
439
440 virtual void relocAll (ClauseAllocator& to);
441
442 // Misc:
443 //
444 int decisionLevel () const; // Gives the current decisionlevel.
445 uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
446 CRef reason (Var x) const;
447 int level (Var x) const;
448 double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
449 bool withinBudget () const;
isSelector(Var v)450 inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
451
452 // Static helpers:
453 //
454
455 // Returns a random float 0 <= x < 1. Seed must never be 0.
drand(double & seed)456 static inline double drand(double& seed) {
457 seed *= 1389796;
458 int q = (int)(seed / 2147483647);
459 seed -= (double)q * 2147483647;
460 return seed / 2147483647; }
461
462 // Returns a random integer 0 <= x < size. Seed must never be 0.
irand(double & seed,int size)463 static inline int irand(double& seed, int size) {
464 return (int)(drand(seed) * size); }
465 };
466
467
468 //=================================================================================================
469 // Implementation of inline methods:
470
reason(Var x)471 inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
level(Var x)472 inline int Solver::level (Var x) const { return vardata[x].level; }
473
insertVarOrder(Var x)474 inline void Solver::insertVarOrder(Var x) {
475 if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
476
varDecayActivity()477 inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
varBumpActivity(Var v)478 inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
varBumpActivity(Var v,double inc)479 inline void Solver::varBumpActivity(Var v, double inc) {
480 if ( (activity[v] += inc) > 1e100 ) {
481 // Rescale:
482 for (int i = 0; i < nVars(); i++)
483 activity[i] *= 1e-100;
484 var_inc *= 1e-100; }
485
486 // Update order_heap with respect to new activity:
487 if (order_heap.inHeap(v))
488 order_heap.decrease(v); }
489
claDecayActivity()490 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
claBumpActivity(Clause & c)491 inline void Solver::claBumpActivity (Clause& c) {
492 if ( (c.activity() += cla_inc) > 1e20 ) {
493 // Rescale:
494 for (int i = 0; i < learnts.size(); i++)
495 ca[learnts[i]].activity() *= 1e-20;
496 cla_inc *= 1e-20; } }
497
checkGarbage(void)498 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
checkGarbage(double gf)499 inline void Solver::checkGarbage(double gf){
500 if (ca.wasted() > ca.size() * gf)
501 garbageCollect(); }
502
503 // NOTE: enqueue does not set the ok flag! (only public methods do)
enqueue(Lit p,CRef from)504 inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
addClause(const vec<Lit> & ps)505 inline bool Solver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
addEmptyClause()506 inline bool Solver::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); }
addClause(Lit p)507 inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
addClause(Lit p,Lit q)508 inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
addClause(Lit p,Lit q,Lit r)509 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); }
locked(const Clause & c)510 inline bool Solver::locked (const Clause& c) const {
511 if(c.size()>2)
512 return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c;
513 return
514 (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
515 ||
516 (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
517 }
newDecisionLevel()518 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
519
decisionLevel()520 inline int Solver::decisionLevel () const { return trail_lim.size(); }
abstractLevel(Var x)521 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
value(Var x)522 inline lbool Solver::value (Var x) const { return assigns[x]; }
value(Lit p)523 inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
modelValue(Var x)524 inline lbool Solver::modelValue (Var x) const { return model[x]; }
modelValue(Lit p)525 inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
nAssigns()526 inline int Solver::nAssigns () const { return trail.size(); }
nClauses()527 inline int Solver::nClauses () const { return clauses.size(); }
nLearnts()528 inline int Solver::nLearnts () const { return learnts.size(); }
nVars()529 inline int Solver::nVars () const { return vardata.size(); }
nFreeVars()530 inline int Solver::nFreeVars () {
531 int a = stats[dec_vars];
532 return (int)(a) - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
setPolarity(Var v,bool b)533 inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
setDecisionVar(Var v,bool b)534 inline void Solver::setDecisionVar(Var v, bool b)
535 {
536 if ( b && !decision[v]) stats[dec_vars]++;
537 else if (!b && decision[v]) stats[dec_vars]--;
538
539 decision[v] = b;
540 insertVarOrder(v);
541 }
setConfBudget(int64_t x)542 inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
setPropBudget(int64_t x)543 inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
interrupt()544 inline void Solver::interrupt(){ asynch_interrupt = true; }
clearInterrupt()545 inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
budgetOff()546 inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
withinBudget()547 inline bool Solver::withinBudget() const {
548 return !asynch_interrupt &&
549 (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
550 (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
551
552 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
553 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
554 // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
solve()555 inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; }
solve(Lit p)556 inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
solve(Lit p,Lit q)557 inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
solve(Lit p,Lit q,Lit r)558 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; }
solve(const vec<Lit> & assumps)559 inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
solveLimited(const vec<Lit> & assumps)560 inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
okay()561 inline bool Solver::okay () const { return ok; }
562
toDimacs(const char * file)563 inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
toDimacs(const char * file,Lit p)564 inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
toDimacs(const char * file,Lit p,Lit q)565 inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
toDimacs(const char * file,Lit p,Lit q,Lit r)566 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); }
567
568
569
570 //=================================================================================================
571 // Debug etc:
572
573
printLit(Lit l)574 inline void Solver::printLit(Lit l)
575 {
576 printf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
577 }
578
579
printClause(CRef cr)580 inline void Solver::printClause(CRef cr)
581 {
582 Clause &c = ca[cr];
583 for (int i = 0; i < c.size(); i++){
584 printLit(c[i]);
585 printf(" ");
586 }
587 }
588
printInitialClause(CRef cr)589 inline void Solver::printInitialClause(CRef cr)
590 {
591 Clause &c = ca[cr];
592 for (int i = 0; i < c.size(); i++){
593 if(!isSelector(var(c[i]))) {
594 printLit(c[i]);
595 printf(" ");
596 }
597 }
598 }
599
600 //=================================================================================================
601 struct reduceDBAct_lt {
602 ClauseAllocator& ca;
603
reduceDBAct_ltreduceDBAct_lt604 reduceDBAct_lt(ClauseAllocator& ca_) : ca(ca_) {
605 }
606
operatorreduceDBAct_lt607 bool operator()(CRef x, CRef y) {
608
609 // Main criteria... Like in MiniSat we keep all binary clauses
610 if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
611
612 if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
613 if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
614
615 return ca[x].activity() < ca[y].activity();
616 }
617 };
618
619 struct reduceDB_lt {
620 ClauseAllocator& ca;
621
reduceDB_ltreduceDB_lt622 reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {
623 }
624
operatorreduceDB_lt625 bool operator()(CRef x, CRef y) {
626
627 // Main criteria... Like in MiniSat we keep all binary clauses
628 if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
629
630 if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
631 if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
632
633 // Second one based on literal block distance
634 if (ca[x].lbd() > ca[y].lbd()) return 1;
635 if (ca[x].lbd() < ca[y].lbd()) return 0;
636
637
638 // Finally we can use old activity or size, we choose the last one
639 return ca[x].activity() < ca[y].activity();
640 //return x->size() < y->size();
641
642 //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
643 }
644 };
645
646
647 }
648
649
650 #endif
651