thread.cpp

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

/********************************************************************************************
MiraXT -- Copyright (c) 2007, Tobias Schubert, Matthew Lewis, Natalia Kalinnik, Bernd Becker 

Permission is hereby granted, free of charge, to any person obtaining a copy of this 
software and associated documentation files (the "Software"), to deal in the Software 
without restriction, including without limitation the rights to use, copy, modify, merge, 
publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons 
to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING 
BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
********************************************************************************************/

class Thread
{

private:
  
  ControlStructure* masterControl;                          // Global control structure.
  DecisionQueue*    theDecisionQueue;                       // Global decision queue.
  clauseDB*         theClauseDB;                            // Global clause database.
  VSIDS*            myVSIDS;                                // VSIDS decision strategy.
  vec<int>          Assignment;                             // (Partial) assignment to the set of variables.
  vec<int>          DecisionStack;                          // Decision stack.
  vec<int>          newDecisionStack;                       // Stores the definition of a received subproblem.
  vec<int*>         clauseVec;                              // Pointer to all clauses the thread is currently  
                                                            // working on (all the clauses for which an entry in 
                                                            // "WLRL" exists). 
  vec<int>          unitClauseVec;                          // Stores all "unit clause literals" (clauses 
                                                            // containing just one literal). 
  vec<int>          unitClauseCheckVec;                     // Allows for a fast check if a "unit clause literal" 
                                                            // is already part of "unitClauseVec".
  vec<vec<int> >    binClauseVec;                           // Contains in an one-dimensional array for each literal 
                                                            // that occurs in a binary clause the second literal 
                                                            // followed by the clause number/address. 
                                                            // Example: clause 5 = (x2, x4), clause 17 = (x4, -x8) 
                                                            // --> binClauseVec[-x4] = (x2, 5, -x8, 17, ...).
                                                            // So, if x4 is set to 0, we can easily check which 
                                                            // binary clauses are forcing implications by  
                                                            // looking at "binClauseVec[-x4]".
  vec<int>          WLRL;                                   // The "Watched Literals Reference List" for each clause:
                                                            // 1st entry: watched literal 1.
                                                            // 2nd entry: watched literal 2.
                                                            // 3rd entry: "cache variable".
                                                            // 4th entry: currently not used, but taking four entries 
                                                            // per clause simplifies the access to WLRL given a 
                                                            // clause number / address.
                                                            // A WLRL can be seen as a compact representation of a clause.
  vec<vec<int> >    WLVec;                                  // Stores for each literal the clauses, that are 
                                                            // currently watched by this literal.
  vec<int>          forcingClauseDS;                        // Stores for all current implications within the 
                                                            // decision stack the reason (the "forcing clause").
  vec<int>          DSLookupArray;                          // Stores for each assigned literal the position 
                                                            // within the decision stack.
  vec<int>          DLLookupArray;                          // Stores for each decision level the position within the 
                                                            // decision stack at which the list of literals assigned 
                                                            // at the corresponding decision level starts.
  vec<int>          clauseActivity;                         // Activity of each clause (more "active" clauses 
                                                            // are less likely to be deleted). 
  vec<unsigned int> literalActivity;                        // Activity of each literal (more "active" literals are 
                                                            // more likely to be selected by the VSIDS strategy).
  vec<bool>         clauseLocked;                           // Each clause currently forcing an implication gets 
                                                            // locked to avoid that the clause will be deleted. 
  vec<int>          caNewClause;                            // Array for the conflict clause generated during 
                                                            // the conflict analysis procedure.
  vec<int>          caLitStack;                             // Conflict analysis stack, stores all literals that still 
                                                            // have to processed during conflict analysis.
  vec<int>          caLitCheckArray;                        // Array to decide which literal has been already processed 
                                                            // during conflict analysis.
  vec<int>          deletedClausesVec;                      // Stores all clauses that might be deleted during
                                                            // the execution of "cleanClauseDB".
  vec<vec<int> >    unitClauseSearchArray;                  // The "IQSize" different queues to perform 
                                                            // "Implication Queue Sorting".
  int               myThreadNum;                            // Each thread's unique ID. 
  int               myCEIBase;                              // Marks the end of the clauses of the original CNF file 
                                                            // within the thread's "clauseVec" array.
  int               sEI;                                    // "Stack End Index", indicating which assigned literals 
                                                            // within the decision stack have been already processed 
                                                            // (by performing BCP) and which ones not (implications). 
                                                            // So, it always holds that ucEI >= sEI.
  int               ucEI;                                   // "Unit Clause End Index", marking the end of all 
                                                            // current implications on top of the decision stack.
  int               currentDL;                              // Current decision level.
  int               restartCount;                           // Restart parameter.
  int               restartInc;                             // Restart parameter.
  int               restartMax;                             // Restart parameter.
  int               literalActivityIncCount;                // Counts how often the literal's activities have been 
                                                            // increased to decide when the counters should 
                                                            // be "normalized" again.
  int               reduceOften;                            // Also used to determine when to reduce the activity 
                                                            // of each literal.
  int               numClausesAdded;                        // Number of clauses added to the thread's 
                                                            // local clause database.
  int               decisionCount;                          // Counts the number of calls of the function "decide".
  int               localDeletedCount;                      // Counts how many clauses are locally deleted by a thread.
  int               DSprogress;                             // Used to determine when it's time to delete some clauses.
  int               cleanOften;                             // Also used to determine when to delete some clauses.
  int               conflictingClauseAddress;               // Number/adress of the current "conflicting clause". 

  bool addNewClausesAndBacktrack(bool InsertOriginalCNF);   // Integrate new clauses from the global clause databases 
                                                            // into the local one and backtrack. 
  void pushUnusedLits(void);                                // Push all literals that occur only in one "polarity" in 
                                                            // the original CNF file as implications onto the 
                                                            // decision stack.
  bool pushAllUnitClauses(void);                            // Push all implications forced by unit clauses 
                                                            // onto the decision stack.
  void popLitDS(int DL);                                    // Pop all literals with decision level greater or 
                                                            // equal "DL" from the decision stack.
  void pushImplication(int Literal, int forcingClause);     // Push an implication onto the decision stack.
  void pushDecision(int Literal);                           // Push a decision onto the decision stack.
  int  findWLinClause(int* ClauseAddr, int otherWL);        // Determine a WL in a new received clause. 
  bool satisfiedClause(int* Clause);                        // Check if "Clause" is currently satisfied.
  bool conflictingClause(int* Clause);                      // Check if "Clause" is unsatisfied and by this 
                                                            // forces a conflict.
  int  decide(void);                                        // Select and assign the next variable.
  bool decideImplication(void);                             // Determine the next implication to be processed.
  void resetUnitClauseSearchArray(void);                    // Reset "unitClauseSearchArray" (Implication Queue Sorting).
  void swapImplicationsDS(int P1, int P2);                  // Swap the implications on positions "P1" and "P2" 
                                                            // within the decision stack.
  void addUnitDecisionSort(int Literal);                    // Determine the correct implication queue of the 
                                                            // implication "Literal" within "unitClauseSearchArray".
  int  findMostRecentlyAssignedLiteral(void);               // Search "caLitStack" to determine the entry that 
                                                            // was most recently assigned.
  bool analyzeConflict(void);                               // Conflict analysis based on zChaff's 1UIP scheme.
  void restartSearch(void);                                 // Perform a restart operation.
  void increaseLiteralActivity(int Literal);                // Increase the activity of literal "Literal".
  void reduceLiteralActivity(void);                         // Reduce ("normalize") the literal's activities. 
  void increaseClauseActivity(int clauseNum);               // Increase the activity of clause "clauseNum".
  bool getNewDecisionStack(void);                           // Receive a new decision stack / subproblem.
  bool getNewDecisionStackAddDeactivatedClauses(void);      // Receive a new subproblem / decision stack, add original 
                                                            // clauses that have been "deactivated" during the last 
                                                            // run, and perform some "preprocessing".
  int  getDLDS(int pos);                                    // Determine the decision level that corresponds to the 
                                                            // entry at position "pos" within the decision stack.
  bool BCPBinary(void);                                     // Perform "Boolean Constraint Propagation", taking 
                                                            // only binary clauses into account. 
  bool BCP(void);                                           // Perform "Boolean Constraint Propagation".
  void removeWL(int WL, int clauseAddress);                 // Remove the clause "clauseAddress" from the list of 
                                                            // clauses currently watched by "WL". 
  void removeWLBIN(int WL0, int WL1, int clauseAddress);    // Remove the clause "clauseAddress" from "binClauseVec".   
  void sortDeletedClausesVec(int Low, int High);            // Sort the list of clauses to be deleted with increasing 
                                                            // activity.
  void cleanClauseDB(void);                                 // Clean both the local and the global clause database 
                                                            // by removing less active clauses.
  bool unitPropagationLookahead(bool firstCall);            // Preprocessing based on "Unit Propagation Lookahead".

public:

  Thread(int TN, ControlStructure *CO, DecisionQueue * DQ); // Constructor.
  ~Thread(void);                                            // Destructor.
  void SatThread(void);                                     // Main routine of the SAT-solving threads.
};

Thread::Thread(int TN, ControlStructure *CO, DecisionQueue * DQ)