1 /****************************************************************************************[Solver.h]
2 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 Copyright (c) 2007-2010, Niklas Sorensson
5 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 associated documentation files (the "Software"), to deal in the Software without restriction,
7 including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 **************************************************************************************************/
21 #ifndef Minisat_Solver_h
22 #define Minisat_Solver_h
24 #include "libs/minisat/Vec.h"
25 #include "libs/minisat/Heap.h"
26 #include "libs/minisat/Alg.h"
27 #include "libs/minisat/IntMap.h"
28 #include "libs/minisat/Options.h"
29 #include "libs/minisat/SolverTypes.h"
34 //=================================================================================================
35 // Solver -- the main class:
40 // Constructor/Destructor:
45 // Problem specification:
47 Var
newVar (lbool upol
= l_Undef
, bool dvar
= true); // Add a new variable with parameters specifying variable mode.
48 void releaseVar(Lit l
); // Make literal true and promise to never refer to variable again.
50 bool addClause (const vec
<Lit
>& ps
); // Add a clause to the solver.
51 bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
52 bool addClause (Lit p
); // Add a unit clause to the solver.
53 bool addClause (Lit p
, Lit q
); // Add a binary clause to the solver.
54 bool addClause (Lit p
, Lit q
, Lit r
); // Add a ternary clause to the solver.
55 bool addClause (Lit p
, Lit q
, Lit r
, Lit s
); // Add a quaternary clause to the solver.
56 bool addClause_( vec
<Lit
>& ps
); // Add a clause to the solver without making superflous internal copy. Will
57 // change the passed vector 'ps'.
61 bool simplify (); // Removes already satisfied clauses.
62 bool solve (const vec
<Lit
>& assumps
); // Search for a model that respects a given set of assumptions.
63 lbool
solveLimited (const vec
<Lit
>& assumps
); // Search for a model that respects a given set of assumptions (With resource constraints).
64 bool solve (); // Search without assumptions.
65 bool solve (Lit p
); // Search for a model that respects a single assumption.
66 bool solve (Lit p
, Lit q
); // Search for a model that respects two assumptions.
67 bool solve (Lit p
, Lit q
, Lit r
); // Search for a model that respects three assumptions.
68 bool okay () const; // FALSE means solver is in a conflicting state
70 bool implies (const vec
<Lit
>& assumps
, vec
<Lit
>& out
);
72 // Iterate over clauses and top-level assignments:
73 ClauseIterator
clausesBegin() const;
74 ClauseIterator
clausesEnd() const;
75 TrailIterator
trailBegin() const;
76 TrailIterator
trailEnd () const;
78 void toDimacs (FILE* f
, const vec
<Lit
>& assumps
); // Write CNF to file in DIMACS-format.
79 void toDimacs (const char *file
, const vec
<Lit
>& assumps
);
80 void toDimacs (FILE* f
, Clause
& c
, vec
<Var
>& map
, Var
& max
);
82 // Convenience versions of 'toDimacs()':
83 void toDimacs (const char* file
);
84 void toDimacs (const char* file
, Lit p
);
85 void toDimacs (const char* file
, Lit p
, Lit q
);
86 void toDimacs (const char* file
, Lit p
, Lit q
, Lit r
);
90 void setPolarity (Var v
, lbool b
); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
91 void setDecisionVar (Var v
, bool b
); // Declare if a variable should be eligible for selection in the decision heuristic.
95 lbool
value (Var x
) const; // The current value of a variable.
96 lbool
value (Lit p
) const; // The current value of a literal.
97 lbool
modelValue (Var x
) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
98 lbool
modelValue (Lit p
) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
99 int nAssigns () const; // The current number of assigned literals.
100 int nClauses () const; // The current number of original clauses.
101 int nLearnts () const; // The current number of learnt clauses.
102 int nVars () const; // The current number of variables.
103 int nFreeVars () const;
104 void printStats () const; // Print some current statistics to standard output.
106 // Resource contraints:
108 void setConfBudget(int64_t x
);
109 void setPropBudget(int64_t x
);
111 void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
112 void clearInterrupt(); // Clear interrupt indicator flag.
116 virtual void garbageCollect();
117 void checkGarbage(double gf
);
120 // Extra results: (read-only member variable)
122 vec
<lbool
> model
; // If problem is satisfiable, this vector contains the model (if any).
123 LSet conflict
; // If problem is unsatisfiable (possibly under assumptions),
124 // this vector represent the final conflict clause expressed in the assumptions.
126 // Mode of operation:
131 double random_var_freq
;
134 int ccmin_mode
; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
135 int phase_saving
; // Controls the level of phase saving (0=none, 1=limited, 2=full).
136 bool rnd_pol
; // Use random polarities for branching heuristics.
137 bool rnd_init_act
; // Initialize variable activities with a small random value.
138 double garbage_frac
; // The fraction of wasted memory allowed before a garbage collection is triggered.
139 int min_learnts_lim
; // Minimum number to set the learnts limit to.
141 int restart_first
; // The initial restart limit. (default 100)
142 double restart_inc
; // The factor with which the restart limit is multiplied in each restart. (default 1.5)
143 double learntsize_factor
; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)
144 double learntsize_inc
; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
146 int learntsize_adjust_start_confl
;
147 double learntsize_adjust_inc
;
149 // Statistics: (read-only member variable)
151 uint64_t solves
, starts
, decisions
, rnd_decisions
, propagations
, conflicts
;
152 uint64_t dec_vars
, num_clauses
, num_learnts
, clauses_literals
, learnts_literals
, max_literals
, tot_literals
;
156 // Helper structures:
158 struct VarData
{ CRef reason
; int level
; };
159 static inline VarData
mkVarData(CRef cr
, int l
){ VarData d
= {cr
, l
}; return d
; }
164 Watcher(CRef cr
, Lit p
) : cref(cr
), blocker(p
) {}
165 bool operator==(const Watcher
& w
) const { return cref
== w
.cref
; }
166 bool operator!=(const Watcher
& w
) const { return cref
!= w
.cref
; }
169 struct WatcherDeleted
171 const ClauseAllocator
& ca
;
172 WatcherDeleted(const ClauseAllocator
& _ca
) : ca(_ca
) {}
173 bool operator()(const Watcher
& w
) const { return ca
[w
.cref
].mark() == 1; }
177 const IntMap
<Var
, double>& activity
;
178 bool operator () (Var x
, Var y
) const { return activity
[x
] > activity
[y
]; }
179 VarOrderLt(const IntMap
<Var
, double>& act
) : activity(act
) { }
182 struct ShrinkStackElem
{
185 ShrinkStackElem(uint32_t _i
, Lit _l
) : i(_i
), l(_l
){}
190 vec
<CRef
> clauses
; // List of problem clauses.
191 vec
<CRef
> learnts
; // List of learnt clauses.
192 vec
<Lit
> trail
; // Assignment stack; stores all assigments made in the order they were made.
193 vec
<int> trail_lim
; // Separator indices for different decision levels in 'trail'.
194 vec
<Lit
> assumptions
; // Current set of assumptions provided to solve by the user.
196 VMap
<double> activity
; // A heuristic measurement of the activity of a variable.
197 VMap
<lbool
> assigns
; // The current assignments.
198 VMap
<char> polarity
; // The preferred polarity of each variable.
199 VMap
<lbool
> user_pol
; // The users preferred polarity of each variable.
200 VMap
<char> decision
; // Declares if a variable is eligible for selection in the decision heuristic.
201 VMap
<VarData
> vardata
; // Stores reason and level for each variable.
202 OccLists
<Lit
, vec
<Watcher
>, WatcherDeleted
, MkIndexLit
>
203 watches
; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
205 Heap
<Var
,VarOrderLt
>order_heap
; // A priority queue of variables ordered with respect to the variable activity.
207 bool ok
; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
208 double cla_inc
; // Amount to bump next clause with.
209 double var_inc
; // Amount to bump next variable with.
210 int qhead
; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
211 int simpDB_assigns
; // Number of top-level assignments since last execution of 'simplify()'.
212 int64_t simpDB_props
; // Remaining number of propagations that must be made before next execution of 'simplify()'.
213 double progress_estimate
;// Set by 'search()'.
214 bool remove_satisfied
; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
215 Var next_var
; // Next variable to be created.
218 vec
<Var
> released_vars
;
221 // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
222 // used, exept 'seen' wich is used in several places.
225 vec
<ShrinkStackElem
>analyze_stack
;
226 vec
<Lit
> analyze_toclear
;
230 double learntsize_adjust_confl
;
231 int learntsize_adjust_cnt
;
233 // Resource contraints:
235 int64_t conflict_budget
; // -1 means no budget.
236 int64_t propagation_budget
; // -1 means no budget.
237 bool asynch_interrupt
;
239 // Main internal methods:
241 void insertVarOrder (Var x
); // Insert a variable in the decision order priority queue.
242 Lit
pickBranchLit (); // Return the next decision variable.
243 void newDecisionLevel (); // Begins a new decision level.
244 void uncheckedEnqueue (Lit p
, CRef from
= CRef_Undef
); // Enqueue a literal. Assumes value of literal is undefined.
245 bool enqueue (Lit p
, CRef from
= CRef_Undef
); // Test if fact 'p' contradicts current state, enqueue otherwise.
246 CRef
propagate (); // Perform unit propagation. Returns possibly conflicting clause.
247 void cancelUntil (int level
); // Backtrack until a certain level.
248 void analyze (CRef confl
, vec
<Lit
>& out_learnt
, int& out_btlevel
); // (bt = backtrack)
249 void analyzeFinal (Lit p
, LSet
& out_conflict
); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
250 bool litRedundant (Lit p
); // (helper method for 'analyze()')
251 lbool
search (int nof_conflicts
); // Search for a given number of conflicts.
252 lbool
solve_ (); // Main solve method (assumptions given in 'assumptions').
253 void reduceDB (); // Reduce the set of learnt clauses.
254 void removeSatisfied (vec
<CRef
>& cs
); // Shrink 'cs' to contain only non-satisfied clauses.
255 void rebuildOrderHeap ();
257 // Maintaining Variable/Clause activity:
259 void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
260 void varBumpActivity (Var v
, double inc
); // Increase a variable with the current 'bump' value.
261 void varBumpActivity (Var v
); // Increase a variable with the current 'bump' value.
262 void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
263 void claBumpActivity (Clause
& c
); // Increase a clause with the current 'bump' value.
265 // Operations on clauses:
267 void attachClause (CRef cr
); // Attach a clause to watcher lists.
268 void detachClause (CRef cr
, bool strict
= false); // Detach a clause to watcher lists.
269 void removeClause (CRef cr
); // Detach and free a clause.
270 bool isRemoved (CRef cr
) const; // Test if a clause has been removed.
271 bool locked (const Clause
& c
) const; // Returns TRUE if a clause is a reason for some implication in the current state.
272 bool satisfied (const Clause
& c
) const; // Returns TRUE if a clause is satisfied in the current state.
276 int decisionLevel () const; // Gives the current decisionlevel.
277 uint32_t abstractLevel (Var x
) const; // Used to represent an abstraction of sets of decision levels.
278 CRef
reason (Var x
) const;
279 int level (Var x
) const;
280 double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
281 bool withinBudget () const;
282 void relocAll (ClauseAllocator
& to
);
287 // Returns a random float 0 <= x < 1. Seed must never be 0.
288 static inline double drand(double& seed
) {
290 int q
= (int)(seed
/ 2147483647);
291 seed
-= (double)q
* 2147483647;
292 return seed
/ 2147483647; }
294 // Returns a random integer 0 <= x < size. Seed must never be 0.
295 static inline int irand(double& seed
, int size
) {
296 return (int)(drand(seed
) * size
); }
300 //=================================================================================================
301 // Implementation of inline methods:
303 inline CRef
Solver::reason(Var x
) const { return vardata
[x
].reason
; }
304 inline int Solver::level (Var x
) const { return vardata
[x
].level
; }
306 inline void Solver::insertVarOrder(Var x
) {
307 if (!order_heap
.inHeap(x
) && decision
[x
]) order_heap
.insert(x
); }
309 inline void Solver::varDecayActivity() { var_inc
*= (1 / var_decay
); }
310 inline void Solver::varBumpActivity(Var v
) { varBumpActivity(v
, var_inc
); }
311 inline void Solver::varBumpActivity(Var v
, double inc
) {
312 if ( (activity
[v
] += inc
) > 1e100
) {
314 for (int i
= 0; i
< nVars(); i
++)
315 activity
[i
] *= 1e-100;
318 // Update order_heap with respect to new activity:
319 if (order_heap
.inHeap(v
))
320 order_heap
.decrease(v
); }
322 inline void Solver::claDecayActivity() { cla_inc
*= (1 / clause_decay
); }
323 inline void Solver::claBumpActivity (Clause
& c
) {
324 if ( (c
.activity() += cla_inc
) > 1e20
) {
326 for (int i
= 0; i
< learnts
.size(); i
++)
327 ca
[learnts
[i
]].activity() *= 1e-20;
328 cla_inc
*= 1e-20; } }
330 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac
); }
331 inline void Solver::checkGarbage(double gf
){
332 if (ca
.wasted() > ca
.size() * gf
)
335 // NOTE: enqueue does not set the ok flag! (only public methods do)
336 inline bool Solver::enqueue (Lit p
, CRef from
) { return value(p
) != l_Undef
? value(p
) != l_False
: (uncheckedEnqueue(p
, from
), true); }
337 inline bool Solver::addClause (const vec
<Lit
>& ps
) { ps
.copyTo(add_tmp
); return addClause_(add_tmp
); }
338 inline bool Solver::addEmptyClause () { add_tmp
.clear(); return addClause_(add_tmp
); }
339 inline bool Solver::addClause (Lit p
) { add_tmp
.clear(); add_tmp
.push(p
); return addClause_(add_tmp
); }
340 inline bool Solver::addClause (Lit p
, Lit q
) { add_tmp
.clear(); add_tmp
.push(p
); add_tmp
.push(q
); return addClause_(add_tmp
); }
341 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
); }
342 inline bool Solver::addClause (Lit p
, Lit q
, Lit r
, Lit s
){ add_tmp
.clear(); add_tmp
.push(p
); add_tmp
.push(q
); add_tmp
.push(r
); add_tmp
.push(s
); return addClause_(add_tmp
); }
344 inline bool Solver::isRemoved (CRef cr
) const { return ca
[cr
].mark() == 1; }
345 inline bool Solver::locked (const Clause
& c
) const { return value(c
[0]) == l_True
&& reason(var(c
[0])) != CRef_Undef
&& ca
.lea(reason(var(c
[0]))) == &c
; }
346 inline void Solver::newDecisionLevel() { trail_lim
.push(trail
.size()); }
348 inline int Solver::decisionLevel () const { return trail_lim
.size(); }
349 inline uint32_t Solver::abstractLevel (Var x
) const { return 1 << (level(x
) & 31); }
350 inline lbool
Solver::value (Var x
) const { return assigns
[x
]; }
351 inline lbool
Solver::value (Lit p
) const { return assigns
[var(p
)] ^ sign(p
); }
352 inline lbool
Solver::modelValue (Var x
) const { return model
[x
]; }
353 inline lbool
Solver::modelValue (Lit p
) const { return model
[var(p
)] ^ sign(p
); }
354 inline int Solver::nAssigns () const { return trail
.size(); }
355 inline int Solver::nClauses () const { return num_clauses
; }
356 inline int Solver::nLearnts () const { return num_learnts
; }
357 inline int Solver::nVars () const { return next_var
; }
358 // TODO: nFreeVars() is not quite correct, try to calculate right instead of adapting it like below:
359 inline int Solver::nFreeVars () const { return (int)dec_vars
- (trail_lim
.size() == 0 ? trail
.size() : trail_lim
[0]); }
360 inline void Solver::setPolarity (Var v
, lbool b
){ user_pol
[v
] = b
; }
361 inline void Solver::setDecisionVar(Var v
, bool b
)
363 if ( b
&& !decision
[v
]) dec_vars
++;
364 else if (!b
&& decision
[v
]) dec_vars
--;
369 inline void Solver::setConfBudget(int64_t x
){ conflict_budget
= conflicts
+ x
; }
370 inline void Solver::setPropBudget(int64_t x
){ propagation_budget
= propagations
+ x
; }
371 inline void Solver::interrupt(){ asynch_interrupt
= true; }
372 inline void Solver::clearInterrupt(){ asynch_interrupt
= false; }
373 inline void Solver::budgetOff(){ conflict_budget
= propagation_budget
= -1; }
374 inline bool Solver::withinBudget() const {
375 return !asynch_interrupt
&&
376 (conflict_budget
< 0 || conflicts
< (uint64_t)conflict_budget
) &&
377 (propagation_budget
< 0 || propagations
< (uint64_t)propagation_budget
); }
379 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
380 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
381 // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
382 inline bool Solver::solve () { budgetOff(); assumptions
.clear(); return solve_() == l_True
; }
383 inline bool Solver::solve (Lit p
) { budgetOff(); assumptions
.clear(); assumptions
.push(p
); return solve_() == l_True
; }
384 inline bool Solver::solve (Lit p
, Lit q
) { budgetOff(); assumptions
.clear(); assumptions
.push(p
); assumptions
.push(q
); return solve_() == l_True
; }
385 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
; }
386 inline bool Solver::solve (const vec
<Lit
>& assumps
){ budgetOff(); assumps
.copyTo(assumptions
); return solve_() == l_True
; }
387 inline lbool
Solver::solveLimited (const vec
<Lit
>& assumps
){ assumps
.copyTo(assumptions
); return solve_(); }
388 inline bool Solver::okay () const { return ok
; }
390 inline ClauseIterator
Solver::clausesBegin() const { return ClauseIterator(ca
, &clauses
[0]); }
391 inline ClauseIterator
Solver::clausesEnd () const { return ClauseIterator(ca
, &clauses
[clauses
.size()]); }
392 inline TrailIterator
Solver::trailBegin () const { return TrailIterator(&trail
[0]); }
393 inline TrailIterator
Solver::trailEnd () const {
394 return TrailIterator(&trail
[decisionLevel() == 0 ? trail
.size() : trail_lim
[0]]); }
396 inline void Solver::toDimacs (const char* file
){ vec
<Lit
> as
; toDimacs(file
, as
); }
397 inline void Solver::toDimacs (const char* file
, Lit p
){ vec
<Lit
> as
; as
.push(p
); toDimacs(file
, as
); }
398 inline void Solver::toDimacs (const char* file
, Lit p
, Lit q
){ vec
<Lit
> as
; as
.push(p
); as
.push(q
); toDimacs(file
, as
); }
399 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
); }
402 //=================================================================================================
406 //=================================================================================================