solver.h

多核环境下运行了可满足性分析的工具软件

    bool     enqueue          (Lit p, Clause* from = NULL);                            // Test if fact 'p' contradicts current state, enqueue otherwise.
    Clause*  propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
    void     cancelUntil      (int level);                                             // Backtrack until a certain level.
    void     analyze          (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
    void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
    bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
    lbool    search           (int nof_conflicts, int nof_learnts);                    // Search for a given number of conflicts.
    void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
    void     removeSatisfied  (vec<Clause*>& cs);                                      // Shrink 'cs' to contain only non-satisfied clauses.
    
    // Maintaining Variable/Clause activity:
    //
    void     varDecayActivity ();                      // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
    void     varBumpActivity  (Var v);                 // Increase a variable with the current 'bump' value.
    void     claDecayActivity ();                      // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
    void     claBumpActivity  (Clause& c);             // Increase a clause with the current 'bump' value.

    // Operations on clauses:
    //
    void     attachClause     (Clause& c);             // Attach a clause to watcher lists.
    void     detachClause     (Clause& c);             // Detach a clause to watcher lists.
    void     removeClause     (Clause& c);             // Detach and free a clause.
    bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
    bool     satisfied        (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.

    // Misc:
    //
    int      decisionLevel    ()      const; // Gives the current decisionlevel.
    uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
    double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...

    // Debug:
    void     printLit         (Lit l);
    template<class C>
    void     printClause      (const C& c);
    void     verifyModel      ();
    void     checkLiteralCount();

    // Static helpers:
    //

    // Returns a random float 0 <= x < 1. Seed must never be 0.
    static inline double drand(double& seed) {
      seed *= 1389796;
      int q = (int)(seed / 2147483647);
      seed -= (double)q * 2147483647;
      return seed / 2147483647; }
    
    // Returns a random integer 0 <= x < size. Seed must never be 0.
    static inline int irand(double& seed, int size) {
      return (int)(drand(seed) * size); }
  };
  
  
  //=================================================================================================
  // Implementation of inline methods:
  
  
  inline void Solver::insertVarOrder(Var x) {
    if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); }
  
  //inline void Solver::varDecayActivity() { var_inc *= var_decay; }
  inline void Solver::varBumpActivity(Var v) {
    if ( (activity[v] += var_inc) > 1e100 ) {
      // Rescale:
      for (int i = 0; i < nVars(); i++)
	activity[i] *= 1e-100;
      var_inc *= 1e-100; }
    
    // Update order_heap with respect to new activity:
    if (order_heap.inHeap(v))
      order_heap.decrease(v); }
  
  //inline void Solver::claDecayActivity() { cla_inc *= clause_decay; }
  inline void Solver::claBumpActivity (Clause& c) {
    if ( (c.activity() += cla_inc) > 1e20 ) {
      // Rescale:
      for (int i = 0; i < learnts.size(); i++)
	learnts[i]->activity() *= 1e-20;
      cla_inc *= 1e-20; } }
  
  inline bool     Solver::enqueue         (Lit p, Clause* from)   { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
  inline bool     Solver::locked          (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
  inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
  
  inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
  inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level[x] & 31); }
  inline lbool    Solver::value         (Var x) const   { return toLbool(assigns[x]); }
  inline lbool    Solver::value         (Lit p) const   { return toLbool(assigns[var(p)]) ^ sign(p); }
  inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
  inline int      Solver::nAssigns      ()      const   { return trail.size(); }
  inline int      Solver::nClauses      ()      const   { return clauses.size(); }
  inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
  inline int      Solver::nVars         ()      const   { return assigns.size(); }
  inline void     Solver::setPolarity   (Var v, bool b) { polarity    [v] = (char)b; }
  inline void     Solver::setDecisionVar(Var v, bool b) { decision_var[v] = (char)b; if (b) { insertVarOrder(v); } }
  inline bool     Solver::solve         ()              { vec<Lit> tmp; return solve(tmp); }
 inline bool     Solver::okay          ()      const   { return ok; }


 //=================================================================================================
 // Debug + etc:

#define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) )
 
 static inline void logLit(FILE* f, Lit l)
   {
     fprintf(f, "%sx%d", sign(l) ? "~" : "", var(l)+1);
   }
 
 static inline void logLits(FILE* f, const vec<Lit>& ls)
   {
     fprintf(f, "[ ");
     if (ls.size() > 0){
       logLit(f, ls[0]);
       for (int i = 1; i < ls.size(); i++){
	 fprintf(f, ", ");
	 logLit(f, ls[i]);
       }
     }
     fprintf(f, "] ");
   }
 
 static inline const char* showBool(bool b) { return b ? "true" : "false"; }
 
 
 // Just like 'assert()' but expression will be evaluated in the release version as well.
 static inline void check(bool expr) { assert(expr); }
 

 inline void Solver::printLit(Lit l)
   {
     reportf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
   }
 
 
 template<class C>
   inline void Solver::printClause(const C& c)
   {
     for (int i = 0; i < c.size(); i++){
       printLit(c[i]);
       fprintf(stderr, " ");
     }
   }
 
} // end namespace minisat

//=================================================================================================

#endif