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

// Pop all literals with decision level greater or equal "DL" from the decision stack.
inline void Thread::popLitDS(int DL)
{
  // Variables.
  int StopPos = DLLookupArray[DL];
  int Literal; 

  // Wrong parameter?
  if (DL > currentDL) { return; }

  // Reset "unitClauseSearchArray" necessary to perform "Implication Queue Sorting".
  resetUnitClauseSearchArray();
  
  // Clear the decision stack "literal by literal".
  while (ucEI > StopPos)
    {
      // Decrement the "Unit Clause End Index".
      ucEI--;
      
      // Read current Literal.
      Literal = DecisionStack[ucEI] >> 1;

      // Unassign "Literal".
      Assignment[Literal] = 0;
    }

  // Initialize "Stack End Index".
  sEI = ucEI;

  // Determine the correct decision level.
  if (DL == 0) { currentDL = 0; } else { currentDL = DL - 1; }

  // Reset the VSIDS pointers.
  myVSIDS->resetVSIDSPtr();
  
  // We are done.
  return;
}

// Push all literals that occur only in one "polarity" in the original CNF file 
// as implications onto the decision stack.
void Thread::pushUnusedLits(void)
{
  // Variables.
  int L, P; 

  // Check all variables/literals.
  for(P=1; P<=numLiterals; P++)	
    {
      L = P << 1;

      // Check activity of "L".
      if (literalActivity[L] == 0)
        { if (Assignment[P] == 0) { pushImplication(L^1,0); } }
      else
	{
	  // Check activity of "-L".
	  if (literalActivity[L^1] == 0) 
	    { if (Assignment[P] == 0) { pushImplication(L,0); } }
	}
    }
}

// Push all implications forced by unit clauses found onto the decision stack.
bool Thread::pushAllUnitClauses(void)
{
  // Variables.
  int Literal;
  
  // Check the "unitClauseVec" array.
  for(int L=0; L<unitClauseVec.size(); L++)
    {
      // Read the next implication.
      Literal = unitClauseVec[L];

      // "Literal" currently unassigned?
      if (Assignment[Literal >> 1] == 0) 
	{
	  // Push "Literal" as an implication onto the decision stack.
	  // This function is always executed on decision level 0 (just before 
	  // starting the search process). So, the "forcing clause" doesn't matter 
	  // and is therefor set to 0.
	  pushImplication(Literal,0); 
	}
      else 
	{ 
	  // If "Literal" is already set to the complementary truth value, we've got a problem.
	  if (Assignment[Literal >> 1] == (Literal ^ 1)) { return false; } 
	}
    }

  // Everything is ok.
  return true;
} 

// Push a decision onto the decision stack.
inline void Thread::pushDecision(int Literal)
{
  // Increase the current decision level.
  currentDL++;

  // Save the beginning of the new decision level within the decision stack.
  DLLookupArray[currentDL] = sEI;

  // Save the position of "Literal" within the decision stack.
  DSLookupArray[Literal >> 1] = sEI;

  // Set "Literal" to the desired truth value.
  Assignment[Literal >> 1] = Literal;

  // Push the decision on top of the decision stack.
  DecisionStack[sEI] = Literal;  

  // Set the "forcingClauseDS" entry to "-1" to indicate that we added a decision.
  forcingClauseDS[sEI] = -1;

  // Update counters.
  sEI++; ucEI = sEI;
}

// Push an implication onto the decision stack.
inline void Thread::pushImplication(int Literal, int forcingClause)
{
  // Do some calculations necessary to perform "Implication Queue Sorting".
  addUnitDecisionSort(Literal);

  // Set "Literal" to the desired truth value.
  Assignment[Literal >> 1] = Literal;

  // Save the position of "Literal" within the decision stack.
  DSLookupArray[Literal >> 1] = ucEI;

  // Push the implication on top of the decision stack.
  DecisionStack[ucEI] = Literal;

  // Store the reason for the implication "Literal".
  forcingClauseDS[ucEI] = forcingClause;

  // Increment "Unit Clause End Index", marking the end of all 
  // current implications on top of the decision stack.
  ucEI++;
}

// Restart the search by popping all variable assignments from decision levels 1 and greater.
void Thread::restartSearch(void) { popLitDS(1); }

// Determine the decision level that corresponds to the entry at position "pos" within the decision stack.
inline int Thread::getDLDS(int pos)
{
  // Variables.
  int  bottom = 0;
  int  top    = currentDL;
  bool done   = false;
  int  mid;
  int  tmp;

  // Search for the corresponding decision level.
  while (top > bottom && !done)
    {
      mid = (top + bottom) >> 1;
      tmp = DLLookupArray[mid];

      if (tmp == pos || (tmp < pos && (mid == currentDL || DLLookupArray[mid+1] > pos)))
	{ done = true; }
      else
	{ if (tmp < pos) { bottom = mid + 1; } else { top = mid - 1; } }
    }

  // Determine the correct return value.
  mid = (top + bottom) >> 1;

  // Return decision level.
  return mid;
}

// Receive a new subproblem / decision stack. 
bool Thread::getNewDecisionStack(void)
{
  // Any new and unchecked subproblems available?
  if (!theDecisionQueue->getDecisionStack(newDecisionStack)) { return false; }

  // Pop all assigned literals.
  popLitDS(0);

  // Treat all elements of the new decision stack as implications.
  int L=0; while(newDecisionStack[L] != 0) { pushImplication(newDecisionStack[L],0); L++; }  

  // Initialize "DSprogress".
  DSprogress=0;  

  // Everything went fine.
  return true;
}

// Receive a new subproblem / decision stack, add original clauses that have been 
// "deactivated" during the last run, and perform some "preprocessing".
bool Thread::getNewDecisionStackAddDeactivatedClauses(void)
{
  // Variables.
  bool OK = false;
  int  C;
  int  WL0;
  int  WL1;
  int* Clause;

  while (!OK)
    {
      while (!OK)
	{
	  // Try to get a new and unchecked subproblem.
	  if (!getNewDecisionStack()) { return false; }
	  
	  // Push all "unit clause literals" found so far as implications onto the decision stack.
	  OK = pushAllUnitClauses();
	}

      // Check all original clauses if they have been "deactivated" during the last run, because
      // they were satisfied on decision level 0. Determine if such clauses are still satisfied 
      // on decision level 0 in the actual run. If not, "activate" them.
      for(C=0; C<myCEIBase; C++)
        {
	  // Get current Clause.
	  Clause = clauseVec[C];

	  // "Clause" deactivated (no WLRL entry) and currently not satisfied?
	  if(WLRL[C << 2] == 0 && !satisfiedClause(Clause))
            {	      
	      // Ok, let's activate "Clause" again.

	      // Get the watched literals.
	      WL0 = Clause[clauseStart];
	      WL1 = Clause[clauseStart+1];
	      
	      // Binary or regular clause?
	      if (Clause[clauseLengthPos] == 3) 
                {
		  // Check if the current binary clause is already stored in "binClauseVec[WL0 ^ 1]".
		  if (binClauseVec[WL0 ^ 1].containsEven(WL1) == binClauseVec[WL0 ^ 1].size())
                    {
		      binClauseVec[WL0 ^ 1].push(WL1);
		      binClauseVec[WL0 ^ 1].push(C);
                    }

		  // Check if the current binary clause is already stored in "binClauseVec[WL1 ^ 1]".
		  if (binClauseVec[WL1 ^ 1].containsEven(WL0) == binClauseVec[WL1 ^ 1].size())
                    {
		      binClauseVec[WL1 ^ 1].push(WL0);
		      binClauseVec[WL1 ^ 1].push(C);
                    }
                }
	      else
                {
		  // "Regular" clause, store in "WLVec" that "WLO" and "WL1" are 
		  // currently watching the current clause.
		  WLVec[WL0].push(C);
		  WLVec[WL1].push(C);
                }

	      // Set the two WLs, the cache variable, and the currently unused 4th entry.
	      WLRL[C << 2      ] = clauseVec[C][clauseStart];
	      WLRL[(C << 2) + 1] = clauseVec[C][clauseStart+1];
	      WLRL[(C << 2) + 2] = clauseVec[C][clauseStart+1];
	      WLRL[(C << 2) + 3] = 0;
            }
        }
      
      // Initialize clause deletion parameter.
      DSprogress = sEI >> 2;

      // Preprocessing.
      if (!unitPropagationLookahead(false)) { OK = false; } 
    }

  // Initialize restart parameters.
  if (restartInc >= 8192) { restartInc = 512; }

  // Everything is ok.
  return true;
}