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

// Perform "Boolean Constraint Propagation", taking only binary clauses into account.
inline bool Thread::BCPBinary(void)
{
  int  newDecision = DecisionStack[sEI-1];
  int* BinArray    = binClauseVec[newDecision];
  int  Max         = binClauseVec[newDecision].size();
  int  Pos         = 0;
  int  Literal;

  // Take a look at all binary clauses containing the Literal "newDecision" to 
  // search for further implications and conflicts.
  while(Pos < Max)
    {	
      // Get the second literal of the next binary clause.
      Literal = BinArray[Pos];

      // Second literal currently unassigned (--> implication) or incorrectly assigned (--> conflict)?
      if (Assignment[Literal >> 1] == 0)
        { pushImplication(Literal,BinArray[Pos+1]); }
      else 
	{ 
	  if (Assignment[Literal >> 1] != Literal) 
	    { conflictingClauseAddress = BinArray[Pos+1]; return false; }
	}

      // Check the next binary clause containing "newDecision".
      Pos = Pos + 2;
    }

  // Everything is ok.
  return true;
}

// Perform "Boolean Constraint Propagation".
bool Thread::BCP(void)
{
  // Variables.
  int        newDecisionInv = DecisionStack[sEI-1] ^ 1;   // Get the next decision.
  vec<int>*  myWLVec        = &(WLVec[newDecisionInv]);   // Get the relevant "WLVec" array.
  int        Ptr            = myWLVec->size() - 1;
  int        WL1;
  int        clauseNum;
  int        WLRLAddr;
  int        oldWL1value;
  int        newWL;
  int*       cPtr;

  // First of all, perform "Boolean Constraint Propagation" on binary clauses only.
  if (!BCPBinary()) { return false; }

  // Check all clauses, where "newDecisionInv" is currently a watched literal.
  while (Ptr != -1)
    {
      // Get the next clause to be checked.
      clauseNum = (*myWLVec)[Ptr];
      WLRLAddr  = clauseNum << 2;

      // Modify "WL1" in such a way that it stores the second WL of the clause under consideration.
      WL1       = WLRL[WLRLAddr];
      WL1       = WL1 ^ WLRL[WLRLAddr + 1];
      WL1       = WL1 ^ newDecisionInv;
        
      // What about the truth value of "WL1"?
      if ((WL1 ^ Assignment[WL1 >> 1]) != 0)
        {
	  // Ok, "WL1" is currently either unassigned or incorrectly assigned.

	  // Set "WL1" to the incorrect truth value (not satisfying the clause) to guarantee that "WL1" will 
	  // not be selected as a "new" watched literal instead of "newDecisionInv" (in case that "WL1" is 
	  // currently unassigned, the cache variable can't be used as the new WL, and we therefor have to search 
	  // the complete clause for a new watched literal).
	  oldWL1value          = Assignment[WL1 >> 1];
	  Assignment[WL1 >> 1] = WL1 ^ 1;
	  
	  // Get the current "cache variable".
	  newWL = WLRL[WLRLAddr + 2];
	  
	  // What about taking the cache variable as the new WL?
	  if ((Assignment[newWL >> 1] ^ newWL) == 1)
            {
	      // The cache variable is incorrectly assigned, we have to look 
	      // at the complete clause to search for a new watched literal.

	      // Get the the start address of the entire clause.
	      cPtr = clauseVec[clauseNum] + clauseStart; 

	      // Check the clause "literal by literal", searching for an unassigned literal 
	      // or a literal that satisfies the clause under consideration. 
	      do { newWL = (*cPtr); cPtr++; } while ((Assignment[newWL>>1] ^ newWL) == 1);                
            }
         
	  // Undo setting "WL1" to the incorrect truth value.
	  Assignment[WL1 >> 1] = oldWL1value;
                 
	  // At this point, "newWL" contains either the CV, an other literal of the clause (in both cases 
	  // the literal can be used as the new WL), or the "clause end marker" 0 (then we've got either an 
	  // implication or a conflict, depending on the truth value of "WL1").

	  // Which of three cases mentioned before do we have?
	  if(newWL != 0)
            {
	      // Save the new watched literal.
	      WLRL[WLRLAddr]     = newWL;
	      WLRL[WLRLAddr + 1] = WL1;
	      WLRL[WLRLAddr + 2] = newDecisionInv;
	      
	      // Remove the current clause from the list of clauses for 
	      // which "newDecisionInv" is a watched literal.
	      myWLVec->rem(Ptr);
	      
	      // Add the current clause to the list of clauses that are "watched" by "newWL".
	      WLVec[newWL].push(clauseNum);
            }          
	  else
            {
	      // Increase the clause's activity.
	      increaseClauseActivity(clauseNum);

	      // Lastly, check if we have an implication or a conflict.
	      if (oldWL1value == 0)
                { pushImplication(WL1, clauseNum); }
	      else
                { conflictingClauseAddress = clauseNum; return false; }
            }
        }

      // Check the next clause.
      Ptr--; 
    }

  // Everything went fine.
  return true;
}