thread_ca.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.
********************************************************************************************/

// Search "caLitStack" to determine the entry that was most recently assigned.
int Thread::findMostRecentlyAssignedLiteral(void)
{
  // Variables.
  int Max    = caLitStack.size();
  int MaxPos = -1;
  int RetPos =  0; 
  int P;
  int Pos;

  // Check all elements of "caLitStack".
  for(P=0; P<Max; P++)
    {
      // Get the position of the "Pth" entry of "caLitStack" within the decision stack. 
      Pos = DSLookupArray[caLitStack[P] >> 1];

      // New maximum found?
      if (Pos > MaxPos) { MaxPos = Pos; RetPos = P; }
    }

  // Return the position of the most recently assigned literal that 
  // is currently an element of "caLitStack".
  return RetPos;
}

// Conflict analysis based on zChaff's 1UIP scheme.
bool Thread::analyzeConflict(void)
{
  // Conflict on decision level 0, problem unsatisfiable?
  if (currentDL == 0) { return false; }
  
  // Increment restart parameter.
  restartCount++;
  
  // Increase the conflicting clause's activity.
  increaseClauseActivity(conflictingClauseAddress);

  // Variables.
  int  Ptr               = 0;
  int* conflictingClause = clauseVec[conflictingClauseAddress];
  int  conflictingDL     = 0;
  int  cutDL;
  int  L;
  int  Pos;
  int  Literal;

  // Initialize the arrays.
  caNewClause.clearFast();
  caLitStack.clearFast();

  // Determine the maximum decision level of all literals of the conflicting clause.
  // This step is mandatory, since we might integrate clauses generated by other threads 
  // that force a conflict on a decision level other than the thread's current decision level.
  Ptr = clauseStart;
  while((L = conflictingClause[Ptr]) != 0)
    { 
      if (conflictingDL < DSLookupArray[L >> 1]) 
	{ conflictingDL = DSLookupArray[L >> 1]; } 
      Ptr++; 
    }
  conflictingDL = getDLDS(conflictingDL);
  
  // Conflict on decision level 0, problem unsatisfiable?
  if (conflictingDL == 0) { return false; }

  // Determine the "cut decision level" to decide which of the variable assignments involved
  // in the current conflict are on the "reason side" and which assignments are on the "conflict side".
  cutDL = DLLookupArray[conflictingDL];

  // Similar to other implementations of "conflict analysis": first analyse the 
  // conflicting clause and then check all the forcing clauses of literals that are 
  // saved in "caLitStack" until the stack is empty. 
  do
    { 
      // Check the current clause under consideration "literal by literal"
      Ptr = clauseStart;
      while ((L = (conflictingClause[Ptr] >> 1)) != 0)
	{
	  // Has literal "L" already been checked during conflict analysis?
	  if (caLitCheckArray[L] == 0)
	    {
	      // Get the position of "L" within the decision stack.
	      Pos = DSLookupArray[L];      

	      // Get the current truth value of "L".
	      Literal = Assignment[L];
	      
	      // Is "L" on the reason or on the conflict side?
	      if (Pos < cutDL)
		{ 
		  // Reason side.
		  caNewClause.push(Literal ^ 1); 
		  increaseLiteralActivity(Literal ^ 1); 
		}    
	      else
		{ 
		  // Conflict side.
		  caLitStack.push(Literal); 
		  increaseLiteralActivity(Literal ^ 1); 
		}
	      
	      // Save that "L" has been processed during conflict analysis.
	      caLitCheckArray[L] = 1;
	    }
	  
	  // Let's take a look at the next literal.
	  Ptr++;
	}

      // Pick the next element from the "conflict analysis literal stack" 
      // and analyze the corresponding forcing clause.
      if (caLitStack.size() > 0)
	{
	  // Determine the entry with the highest decision level within "caLitStack".
	  Pos = findMostRecentlyAssignedLiteral();

	  // Get the next literal to be checked.
	  Literal = caLitStack[Pos];

	  // Remove "Literal" from the "conflict analysis literal stack".
	  caLitStack.rem(Pos);

	  // Get the forcing clause which was responsible for assigning "Literal".
	  L = forcingClauseDS[DSLookupArray[Literal >> 1]];

	  // If the stack gets empty, then the last pick is the UIP.
	  if (caLitStack.size() == 0) 
	    { caNewClause.push(Literal^1); }
	  else 
	    { increaseClauseActivity(L); conflictingClause = clauseVec[L]; }
	}
    }
  while(caLitStack.size() != 0);

  // Add the "clause end marker".
  caNewClause.push(0);	

  // Reset the temporary arrays.
  while(cutDL < ucEI) { caLitCheckArray[DecisionStack[cutDL]>>1] = 0; cutDL++; }
  Ptr = 0; while(caNewClause[Ptr] != 0) { caLitCheckArray[caNewClause[Ptr]>>1] = 0; Ptr++; }
  
  // Add the generated conflict clause to the global clause database.
  theClauseDB->addNewClause(caNewClause, caNewClause.size(), myThreadNum);

  // Ok, everything went fine.
  return true;
}