libs/minisat/Solver.h

   1 /****************************************************************************************[Solver.h]
   2 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
   3 Copyright (c) 2007-2010, Niklas Sorensson
   4
   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:
  10
  11 The above copyright notice and this permission notice shall be included in all copies or
  12 substantial portions of the Software.
  13
  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 **************************************************************************************************/
  20
  21 #ifndef Minisat_Solver_h
  22 #define Minisat_Solver_h
  23
  24 #include "Vec.h"
  25 #include "Heap.h"
  26 #include "Alg.h"
  27 #include "IntMap.h"
  28 #include "Options.h"
  29 #include "SolverTypes.h"
  30
  31
  32 namespace Minisat {
  33
  34 //=================================================================================================
  35 // Solver -- the main class:
  36
  37 class Solver {
  38 public:
  39
  40     // Constructor/Destructor:
  41     //
  42     Solver();
  43     virtual ~Solver();
  44
  45     // Problem specification:
  46     //
  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.
  49
  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'.
  58
  59     // Solving:
  60     //
  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
  69
  70     bool    implies      (const vec<Lit>& assumps, vec<Lit>& out);
  71
  72     // Iterate over clauses and top-level assignments:
  73     ClauseIterator clausesBegin() const;
  74     ClauseIterator clausesEnd()   const;
  75     TrailIterator  trailBegin()   const;
  76     TrailIterator  trailEnd  ()   const;
  77
  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);
  81
  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);
  87
  88     // Variable mode:
  89     //
  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.
  92
  93     // Read state:
  94     //
  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.
 105
 106     // Resource constraints:
 107     //
 108     void    setConfBudget(int64_t x);
 109     void    setPropBudget(int64_t x);
 110     void    budgetOff();
 111     void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
 112     void    clearInterrupt();     // Clear interrupt indicator flag.
 113
 114     // Memory managment:
 115     //
 116     virtual void garbageCollect();
 117     void    checkGarbage(double gf);
 118     void    checkGarbage();
 119
 120     // Extra results: (read-only member variable)
 121     //
 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.
 125
 126     // Mode of operation:
 127     //
 128     int       verbosity;
 129     double    var_decay;
 130     double    clause_decay;
 131     double    random_var_freq;
 132     double    random_seed;
 133     bool      luby_restart;
 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.
 140
 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)
 145
 146     int       learntsize_adjust_start_confl;
 147     double    learntsize_adjust_inc;
 148
 149     // Statistics: (read-only member variable)
 150     //
 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;
 153
 154 protected:
 155
 156     // Helper structures:
 157     //
 158     struct VarData { CRef reason; int level; };
 159     static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
 160
 161     struct Watcher {
 162         CRef cref;
 163         Lit  blocker;
 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; }
 167     };
 168
 169     struct WatcherDeleted
 170     {
 171         const ClauseAllocator& ca;
 172         WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
 173         bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
 174     };
 175
 176     struct VarOrderLt {
 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) { }
 180     };
 181
 182     struct ShrinkStackElem {
 183         uint32_t i;
 184         Lit      l;
 185         ShrinkStackElem(uint32_t _i, Lit _l) : i(_i), l(_l){}
 186     };
 187
 188     // Solver state:
 189     //
 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.
 195
 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).
 204
 205     Heap<Var,VarOrderLt>order_heap;       // A priority queue of variables ordered with respect to the variable activity.
 206
 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.
 216     ClauseAllocator     ca;
 217
 218     vec<Var>            released_vars;
 219     vec<Var>            free_vars;
 220
 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.
 223     //
 224     VMap<char>          seen;
 225     vec<ShrinkStackElem>analyze_stack;
 226     vec<Lit>            analyze_toclear;
 227     vec<Lit>            add_tmp;
 228
 229     double              max_learnts;
 230     double              learntsize_adjust_confl;
 231     int                 learntsize_adjust_cnt;
 232
 233     // Resource constraints:
 234     //
 235     int64_t             conflict_budget;    // -1 means no budget.
 236     int64_t             propagation_budget; // -1 means no budget.
 237     bool                asynch_interrupt;
 238
 239     // Main internal methods:
 240     //
 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 ();
 256
 257     // Maintaining Variable/Clause activity:
 258     //
 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.
 264
 265     // Operations on clauses:
 266     //
 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.
 273
 274     // Misc:
 275     //
 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);
 283
 284     // Static helpers:
 285     //
 286
 287     // Returns a random float 0 <= x < 1. Seed must never be 0.
 288     static inline double drand(double& seed) {
 289         seed *= 1389796;
 290         int q = (int)(seed / 2147483647);
 291         seed -= (double)q * 2147483647;
 292         return seed / 2147483647; }
 293
 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); }
 297 };
 298
 299
 300 //=================================================================================================
 301 // Implementation of inline methods:
 302
 303 inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
 304 inline int  Solver::level (Var x) const { return vardata[x].level; }
 305
 306 inline void Solver::insertVarOrder(Var x) {
 307     if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
 308
 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 ) {
 313         // Rescale:
 314         for (int i = 0; i < nVars(); i++)
 315             activity[i] *= 1e-100;
 316         var_inc *= 1e-100; }
 317
 318     // Update order_heap with respect to new activity:
 319     if (order_heap.inHeap(v))
 320         order_heap.decrease(v); }
 321
 322 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
 323 inline void Solver::claBumpActivity (Clause& c) {
 324         if ( (c.activity() += cla_inc) > 1e20 ) {
 325             // Rescale:
 326             for (int i = 0; i < learnts.size(); i++)
 327                 ca[learnts[i]].activity() *= 1e-20;
 328             cla_inc *= 1e-20; } }
 329
 330 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
 331 inline void Solver::checkGarbage(double gf){
 332     if (ca.wasted() > ca.size() * gf)
 333         garbageCollect(); }
 334
 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); }
 343
 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()); }
 347
 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)
 362 {
 363     if      ( b && !decision[v]) dec_vars++;
 364     else if (!b &&  decision[v]) dec_vars--;
 365
 366     decision[v] = b;
 367     insertVarOrder(v);
 368 }
 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); }
 378
 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; }
 389
 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]]); }
 395
 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); }
 400
 401
 402 //=================================================================================================
 403 // Debug etc:
 404
 405
 406 //=================================================================================================
 407 }
 408
 409 #endif