thread.cpp

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

{
  // Initialization.
  myThreadNum              = TN;
  myCEIBase                = 0;
  masterControl            = CO;
  theClauseDB              = masterControl->theClauseDB;
  theDecisionQueue         = DQ;
  sEI                      = 0;
  ucEI                     = 0;
  numClausesAdded          = 0;
  currentDL                = 0;
  restartCount             = 0;
  restartInc               = 100;
  restartMax               = 8192;
  DSprogress               = 0;
  literalActivityIncCount  = 0;
  conflictingClauseAddress = 0;
  decisionCount            = 0;
  localDeletedCount        = 0;
  cleanOften               = 4096;

  // Allocate various memory blocks.
  DecisionStack.growTo(numLiterals+1,0);
  newDecisionStack.growTo(numLiterals+1,0);
  Assignment.growTo(numLiterals+1,0);
  forcingClauseDS.growTo(numLiterals+1,0);
  DSLookupArray.growTo(numLiterals+1,0);
  DLLookupArray.growTo(numLiterals+1,0);
  unitClauseCheckVec.growTo(numLiterals+1,0);
  literalActivity.growTo((numLiterals << 1)+2,0);
  WLVec.growTo((numLiterals << 1)+2,0);
  binClauseVec.growTo((numLiterals << 1)+2,0);
  caLitCheckArray.growTo(numLiterals+1,0);
  caNewClause.growTo(numLiterals+1,0);
  caLitStack.growTo(numLiterals+1,0);
  WLRL.getMem(theClauseDB->masterBaseClauseVec.size() << 3);
  clauseVec.getMem(theClauseDB->masterBaseClauseVec.size() << 3); 
  clauseLocked.getMem(theClauseDB->masterBaseClauseVec.size() << 3);
  clauseActivity.getMem(theClauseDB->masterBaseClauseVec.size() << 3);
  deletedClausesVec.getMem(theClauseDB->masterBaseClauseVec.size() << 3);
  unitClauseVec.getMem(numLiterals+1);

  // Initialization.
  myVSIDS = new VSIDS(&literalActivity[0]);
  theClauseDB->makeMyLock(myThreadNum);

  // Initialization.
  int V = numLiterals; int C = 0; while (V >>= 1) { C++; } C = C >> 1;
  reduceOften = 512 * C; if (reduceOften > 16384) { reduceOften = 16384; }

  // Initialization.
  unitClauseSearchArray.growTo(IQSize+1,0);
  for (int L=0; L<=IQSize; L++) { unitClauseSearchArray[L].getMem(512); }       
}

// Destructor.
Thread::~Thread(void) { /* Nothing has to be done. */ }

// The main routine of the SAT-solving threads.	
void Thread::SatThread()
{
  // Add all clauses of the original CNF file.
  addNewClausesAndBacktrack(true);

  // Initialization.
  numClausesAdded = 0;
  myCEIBase       = clauseVec.size();
  myVSIDS->sort(true);
  
  // The thread with ID 0 does some preprocessing and then starts solving the overall benchmark
  // instance, while all other threads are waiting for a new and unchecked subproblem to solve.
  if (myThreadNum == 0)
    {
      // Push all literals that occur only in one "polarity" in the original 
      // CNF file as implications onto the decision stack.
      pushUnusedLits();

      // Push all "unit clause literals" within the original 
      // CNF file as implications onto the decision stack.
      pushAllUnitClauses();

      if (!unitPropagationLookahead(true))
        { 
	  // Conflict on decision level 0, problem is unsatisfiable. Stop search process.
	  masterControl->done(); 
	  theDecisionQueue->getDecisionStack(newDecisionStack); 
	  return; 
	}
    }
  else
    {
      bool OK = false;
      while(!OK)
        {
	  // Try to get a new and unchecked subproblem.
	  if (!getNewDecisionStack()) { return; }

	  // Push all "unit clause literals" found so far as implications onto the decision stack.
	  OK = pushAllUnitClauses();
        }

      // Initialize "DSprogress".
      DSprogress=0;
    }

  // Main SAT-solving loop, quite similar to other modern SAT engines.
  while(true)
    {
      // Select and assign the next variable. Not only "free" variables, but also all current 
      // implications for which "Boolean Constraint Propagation" hasn't been done so far, will 
      // be covered by "decide" (implications are selected first).
      if(decide())
        {
	  // Perform "Boolean Constraint Propagation" for the selection made by "decide".
	  while(!BCP())
            {
	      // Ok, we've got a conflict. So, let's analyze it, add 
	      // new clauses, and then backtrack.
	      if (!analyzeConflict() || !addNewClausesAndBacktrack(false))
                {                    
		  // Conflict on decision level 0, current (sub)problem is unsatisfiable.
		  // Try to get a new and unchecked suproblem.
		  if (!getNewDecisionStackAddDeactivatedClauses()) { return; }
                }
                
	      // What about doing some "preprocessing" again?
	      if (currentDL == 0 && (DSprogress + 256) < ucEI)
                { 
		  while (!unitPropagationLookahead(false))
                    {
		      // Conflict on decision level 0, current (sub)problem is unsatisfiable.
		      // Try to get a new and unchecked suproblem.
		      if (!getNewDecisionStackAddDeactivatedClauses()) { return; }
                    }
                }

	      // At this point there is definitely a new implication: either the one based on 
	      // the conflict clause generated just before or an implication that has its source in 
	      // one of the added clauses from other threads. So, we have to call "decide" again 
	      // to select this implication for the next execution of "BCP".
	      decide();
            }
        }
      else 
        {
	  // At this point either the problem is solved (no unassigned variable left) or 
	  // we are running out of time with respect to the given CPU limit.
	  if(masterControl->masterDone==0 && (getTime() - masterControl->startTime) <= maxTime)
            {
	      // Save the satisfying variable assignment.
	      masterControl->problemSolved(Assignment); 
            }

	  // Stop the search.
	  masterControl->done();
	  theDecisionQueue->getDecisionStack(newDecisionStack);
	  return;
        }
    }
}