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

// Check if "Clause" is currently satisfied.
inline bool Thread::satisfiedClause(int* Clause)
{
  int Ptr = clauseStart;
  int Literal;

  // Check the clause "literal by literal".
  while ((Literal = Clause[Ptr]) != 0)
    {
      if (Literal == Assignment[Literal >> 1]) { return true; }
      Ptr++;
    }

  // "Clause" currently not satisfied.
  return false;
}

// Check if "clause" is unsatisfied and by this forces a conflict.
inline bool Thread::conflictingClause(int* Clause)
{
  // Variables.
  int Ptr = clauseStart;
  int Literal;

  while((Literal = Clause[Ptr]) != 0)
    { if (Assignment[Literal >> 1] != (Literal ^ 1)) { return false; } Ptr++; }

  return true;
}

// Determine a WL in a new received clause. 
inline int Thread::findWLinClause(int* ClauseAddr, int otherWL)
{
  // Variables.
  int Ptr       = clauseStart;
  int HighestDL = -1;
  int Pos       = clauseStart;
  int Literal;
	
  // Check the clause "literal by literal".
  while ((Literal = (ClauseAddr[Ptr] >> 1)) != 0)
    {
      // Don't select the already determined WL twice.
      if (Literal != otherWL)
        {
	  // "Literal" unassigned or fulfilling the clause? 
	  if ((Assignment[Literal] == 0) || (Assignment[Literal] == ClauseAddr[Ptr])) { return Ptr; }

	  // Ok, "Literal" is assigned "incorrectly". But on which decision level?
	  if (DSLookupArray[Literal] > HighestDL) { HighestDL = DSLookupArray[Literal]; Pos = Ptr; }
        }
      Ptr++;
    }

  // At this point all literals of the clause are assigned "incorrectly" (--> conflict!), 
  // return the position of the literal with the highest decision level.
  return Pos;
}

// Integrate new clauses from the global clause databases into the local one and backtrack.
bool Thread::addNewClausesAndBacktrack(bool InsertOriginalCNF)
{
  // Variables.
  int  Ptr;
  int  WL0, WL1; 
  int  ClauseAddr;
  int* tmpClause;
  int  solved;
  int  freeLiterals;
  int  DLWL0;
  int  DLWL1;
  int  tmp;
 
  // Receive the next clause either from the set of original or generated clauses.
  if (InsertOriginalCNF) 
    { tmpClause = theClauseDB->getNewClauseInit(myThreadNum); }
  else 
    { tmpClause = theClauseDB->getNewClause(myThreadNum); }
  
  // Check the status of the current clause and integrate it into the local database if necessary.
  while(tmpClause != NULL)
    {

#ifdef ThreadKnowledgeSharing

      // Only clauses with a length less or equal "maxClauseSize", unsatisfied clauses, 
      // and clauses from the original CNF file will be integrated. 
      if (tmpClause[clauseLengthPos] <= maxClauseSize || conflictingClause(tmpClause) || InsertOriginalCNF)

#else

      // Don't integrate clauses generated by other threads.
      if (tmpClause[clauseThreadIDPos] == myThreadNum || InsertOriginalCNF)

#endif

        {
	  // Initialize the pointer to the first literal of the current clause.
	  Ptr = clauseStart;

	  // Get pointer to the current clause.
	  ClauseAddr = clauseVec.size();

	  // Save current clause in "clauseVec" to be able to access the complete clause if necessary.
	  clauseVec.push(tmpClause);

	  // Initialize the clause's activity.
	  clauseActivity.push(activityInc);

	  // Initialize the "clause locking" flag. 	  
	  clauseLocked.push(false); 
	  
	  // Increment "numClausesAdded".
	  numClausesAdded++;

	  // Unit clause?
	  if (tmpClause[clauseLengthPos] == 2) 
            {
	      // Set the two WLs, the cache variable, and the currently unused 4th position.
	      WLRL.push(tmpClause[Ptr]);
	      WLRL.push(0);
	      WLRL.push(0);
	      WLRL.push(0);
     
	      // Get the one and only watched literal.
	      WL0 = tmpClause[Ptr];
	      
	      // Now, check the status of the unit clause.
	      if(unitClauseCheckVec[WL0 >> 1] == 0)
		{     
		  // Until now there is no unit clause containing literal WL0 within the local database.
		  // So, store this information to know about such kind of implications 
		  // (in particular when receiving a new subproblem). 
		  unitClauseCheckVec[WL0 >> 1] = WL0;
		  unitClauseVec.push(WL0);

		  // In case that the current unit clause is part of the original CNF, 
		  // nothing further has to be done. The situation that the original CNF 
		  // file contains two unit clauses (x) and (-x) is detected 
		  // by "unitPropagationLookahead".
		  if(!InsertOriginalCNF)
		    {
		      // WL0 currently unassigned?
		      if (Assignment[WL0 >> 1] == 0)
			{ 
			  // Backtrack to decision level 0 and push implication "WL0".
			  popLitDS(1); pushImplication(WL0,ClauseAddr); 
			}
		      else
			{
			  // "WLO" is currently assigned, but on which decision level?
			  if (currentDL != 0 && DSLookupArray[WL0 >> 1] >= DLLookupArray[1])                
			    { 
			      // It's assigned on a decision level greater than 0, so backtrack  
			      // to decision level 0 and push implication "WL0".
			      popLitDS(1); pushImplication(WL0,ClauseAddr); 
			    }
			  else 
			    { 
			      // "WL0" was assigned on decision level 0, but what about the truth value?
			      if (Assignment[WL0 >> 1] == (WL0 ^ 1))
				{
				  // Conflict on decision level 0, current (sub)problem unsatisfiable.
				  return false; 
				}
			    }
			}                           
		    }
		}
	      else 
		{
		  // There is already a unit clause containing "WL0" within the local database.
		  if (unitClauseCheckVec[WL0 >> 1] == (WL0 ^ 1))
		    {
		      // Conflict on decision level 0, current (sub)problem unsatisfiable.
		      unitClauseVec.push(WL0);
		      masterControl->done();
		      return false;
		    }
		}
            }
	  else
            {
	      // Determine two watched literals.
	      WL0 = tmpClause[findWLinClause(tmpClause,0)];
	      WL1 = tmpClause[findWLinClause(tmpClause,WL0 >> 1)];
                
	      // Set the two WLs, the cache variable, and the currently unused 4th entry.
	      WLRL.push(WL0);
	      WLRL.push(WL1);
	      WLRL.push(WL0);
	      WLRL.push(0);
	      	      
	      // Binary clause?
	      if (tmpClause[clauseLengthPos] == 3) 
                {    
		  // Check if the current binary clause is already stored in "binClauseVec[WL0 ^ 1]".
		  if (InsertOriginalCNF || binClauseVec[WL0 ^ 1].containsEven(WL1) == binClauseVec[WL0 ^ 1].size())
                    {
		      binClauseVec[WL0 ^ 1].push(WL1);
		      binClauseVec[WL0 ^ 1].push(ClauseAddr);
                    }

		  // Check if the current binary clause is already stored in "binClauseVec[WL1 ^ 1]".
		  if (InsertOriginalCNF || binClauseVec[WL1 ^ 1].containsEven(WL0) == binClauseVec[WL1 ^ 1].size())
                    {
		      binClauseVec[WL1 ^ 1].push(WL0);
		      binClauseVec[WL1 ^ 1].push(ClauseAddr);
                    }
                }
	      else    
                {
		  // "Normal" clause, store in "WLVec" that "WLO" and "WL1" are currently watching the current clause.
		  WLVec[WL0].push(ClauseAddr);
		  WLVec[WL1].push(ClauseAddr);
                }
	      
	      // After adding the current clause, do some backtracking if necessary.
	      if(!InsertOriginalCNF)
                {	      
		  // Initialization.
		  Ptr          = clauseStart;
		  freeLiterals = 0;
		  solved       = 0;
		  
		  // Check clause status.
		  while((tmp = tmpClause[Ptr]) != 0 && (solved + freeLiterals) < 2)
                    { 
		      if (Assignment[tmp >> 1] == tmp) { solved++; }        // Clause is satisfied by literal "tmp".
		      if (Assignment[tmp >> 1] == 0)   { freeLiterals++; }  // Literal "tmp" currently unassigned.
		      Ptr++;
                    }
		  
		  // Conflict?
		  if (solved == 0 && freeLiterals == 0)
                    {
		      // Increment the watched literals activity.
		      increaseLiteralActivity(WL0); 
		      increaseLiteralActivity(WL1);
		 
		      // Get the decision level on which "WL0" has been assigned.
		      DLWL0 = getDLDS(DSLookupArray[WL0 >> 1]);

		      // Conflict on decision level 0, problem unsatisfiable?
		      if (DLWL0 == 0) { return false; } 
		      
		      // Get the decision level on which "WL1" has been assigned (DLWL1 =< DLWL0).
		      DLWL1 = getDLDS(DSLookupArray[WL1 >> 1]);
		      
		      // If both decision levels are equal we have to call "analyzeConflict", 
		      // otherwise we can easily preserve the conflict by just backtracking to the 
		      // decision level of "WL1". Then the current clause is no longer a 
		      // "conflicting clause" but forcing the implication "WL0".
		      if (DLWL0 == DLWL1)
                        {
			  // Store the conflicting clause.
			  conflictingClauseAddress = ClauseAddr;

			  // Analyze the conflict.
			  if (!analyzeConflict()) { return false; }

			  // Preserve the conflict by backtracking to decision level before DLWL1.
			  popLitDS(DLWL1);
                        }
		      else
                        {
			  // Backtrack.
			  popLitDS(DLWL1+1); 

			  // Push "WL0" as an implication onto the decision stack.
			  pushImplication(WL0,ClauseAddr);
                        }
                    }
		  else
		    {
		      // Implication I?
		      if (solved == 0 && freeLiterals == 1)
			{
			  // Get the decision level on which "WL1" has been assigned.
			  DLWL1 = getDLDS(DSLookupArray[WL1 >> 1]);

			  // Backtrack to decision level "DLWL1".
			  popLitDS(DLWL1+1);
			  
			  // Push "WL0" as an implication onto the decision stack.
			  pushImplication(WL0,ClauseAddr);
			}
		      else 
			{
			  // Implication II?
			  if(solved == 1 && freeLiterals == 0)
			    {
			      // Is it "WL1" that satisfies the clause?
			      if (Assignment[WL1 >> 1] == WL1) 
				{
				  // Swap the two watched literals.
				  WL0 = WL0 ^ WL1; 
				  WL1 = WL1 ^ WL0; 
				  WL0 = WL0 ^ WL1; 
				}

			      // Get the decision level on which "WL0" has been assigned.
			      DLWL0 = getDLDS(DSLookupArray[WL0 >> 1]);
			      	      
			      // Get the decision level on which "WL1" has been assigned.
			      DLWL1 = getDLDS(DSLookupArray[WL1 >> 1]);
			      
			      // Compare the two decision levels.
			      if(DLWL1 < DLWL0)
				{ 
				  // Ok, taking the new clause into account, "WL0" was correctly assigned 
				  // on decision level "DLWL0", but it is currently also an implication on 
				  // decision level "DLWL1", which is less than "DLWL0". So, let's backtrack 
				  // and push "WL0" as an implication on decision level "DLWL1".
				  popLitDS(DLWL1+1); pushImplication(WL0,ClauseAddr); 
				}
			    }
			}
		    }
                }
            }

	  // If the current clause belongs to the original CNF file, then initialize the literal's acitivities.
	  if(InsertOriginalCNF)
	    {
	      Ptr = clauseStart;
	      while((tmp = tmpClause[Ptr]) != 0) { literalActivity[tmp]++; Ptr++; }
	    }
        }
      else
        {
	  // Discarded clauses are marked "to be deleted".
	  theClauseDB->deleteClause(tmpClause, myThreadNum);
        }
                 
      // Receive the next clause either from the set of original or generated clauses.
      if (InsertOriginalCNF) 
	{ tmpClause = theClauseDB->getNewClauseInit(myThreadNum); }
      else 
	{ tmpClause = theClauseDB->getNewClause(myThreadNum); }
    }
  
  // Update restart parameters.
  if (currentDL == 0) { restartCount = 0; }

  // Everything is OK, i.e. no conflict on decision level 0.
  return true;         
}