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

// Preprocessing based on a "Unit Propagation Lookahead" mechanism.
// Note, that "unitPropagationLookahead" works properly only when executed on decision level 0.
bool Thread::unitPropagationLookahead(bool firstCall)
{
  // Variables.
  int            C; 
  int            L;
  int            Ptr;
  int            Literal;
  int            startPtr;
  int            endPtr;
  int            sEIstart;
  int            Ctr = 0;
  int*           tmpClause;
  bool           BCPValue1;
  bool           BCPValue2;
  vec<vec<int> > Lit2Clauses;
  vec<int>       Lits2Search;
  vec<bool>      Lits2SearchCheck;
  vec<int>       tmpDS;
  vec<int>       foundImplications;                       
  long long      myStartTime = getTime();

  // Initialization.
  Lit2Clauses.growTo((numLiterals<<1)+2);
  Lits2Search.getMem(numLiterals+1);
  tmpDS.growTo(numLiterals+1);
  foundImplications.getMem(numLiterals+1);

  // Store for each literal the clauses it is part of.
  for (C=0; C<myCEIBase; C++)
    {
      tmpClause = clauseVec[C];
      L         = clauseStart;
      
      while (tmpClause[L] != 0) { Lit2Clauses[tmpClause[L]].push(C); L++; }
    }
  
  // "Stack End Index" not equal to "Unit Clause End Index"?
  if(sEI != ucEI)
    {
      // Ok, we currently have some implications on the decision stack, so process them first.

      // Update "sEI" if necessary.
      if (sEI == 0) { sEI++; }

      // Process all implications on the decision stack.
      while ((BCPValue1 = BCP()) && sEI != ucEI && sEI <= numLiterals) { sEI++; }

      // Reset "unitClauseSearchArray" (used for "Implication Queue Sorting").
      resetUnitClauseSearchArray();

      // Let's take a look at the results.
      if (!BCPValue1) { return false; }
      if (sEI > numLiterals) { return true; }
    }

  // What about deleting some clauses?
  if ((DSprogress+512) < ucEI) { cleanClauseDB(); DSprogress = ucEI; }
  
  // Is "unitPropagationLookahead" called by the thread that starts solving the entire benchmark problem?
  if (firstCall)
    {
      // Ok, then perform "Unit Propagation Lookahead" for all variables.

      // Initialization.
      Lits2SearchCheck.growTo(numLiterals+1, true);

      // Push all variables onto "Lits2Search".
      for (L=1; L<=numLiterals; L++) { Lits2Search.push(L); }
    }
  else
    {
      // Ok, "unitPropagationLookahead" was called by another thread during the search process.

      // Initialization.
      Lits2SearchCheck.growTo(numLiterals+1, false);

      // For each currently assigned literal we first select the clauses, where the "opposite" 
      // literal is part of. Afterwards, all literals of these clauses are pushed onto "Lits2Search" 
      // and are the ones "Unit Propagation Lookahead" will be performed for.
      for (L=0; L<sEI; L++)
	{
	  for (C=0; C<Lit2Clauses[DecisionStack[L]^1].size(); C++)
	    {
	      tmpClause = clauseVec[Lit2Clauses[DecisionStack[L]^1][C]];
	      Ptr       = clauseStart;

	      while (tmpClause[Ptr] != 0)
		{ 
		  Literal = tmpClause[Ptr] >> 1;

		  if (!Lits2SearchCheck[Literal] && Assignment[Literal] == 0)
		    { 
		      Lits2Search.push(Literal); 
		      Lits2SearchCheck[Literal] = true; 
		    }

		  Ptr++;
		}
	    }
	}                
    }
  
  // Now, it's time for "Unit Propagation Lookahead".
  while (true)
    {  
      // Store the current value of "sEI".
      sEIstart = sEI;

      // Perform the unit propagation lookahead for all literals within "Lits2Search".
      while (Lits2Search.size() != 0)
	{
	  // Increment "Ctr".
	  Ctr++;
      
	  // Get the next literal.
	  Literal = Lits2Search.last();
	  Lits2SearchCheck[Literal] = false;
	  Lits2Search.pop();

	  // "Literal" still unassigned?
	  if (Assignment[Literal] == 0) 
	    {
	      // Initialization.
	      startPtr = sEI;

	      // Push "Literal" as a decision on the decision stack and see what happens.
	      pushDecision(Literal << 1); 
	      while ((BCPValue1 = BCP()) && sEI != ucEI && sEI <= numLiterals) { sEI++; }
	      endPtr = sEI;

	      // Satisfying variable assignment found?
	      if (BCPValue1 && sEI > numLiterals) { return true; }

	      // Store all implications forced by setting "Literal".
	      for (L=startPtr; L<endPtr; L++) { tmpDS[L] = DecisionStack[L]; }
	      
	      // Undo the decision and all the implications forced by this decision.
	      popLitDS(1);
	      
	      // Push "-Literal" as a decision on the decision stack and see what happens.
	      pushDecision((Literal << 1) + 1);
	      while((BCPValue2 = BCP()) && sEI != ucEI && sEI <= numLiterals) { sEI++; }
	      
	      // Satisfying variable assignment found?
	      if (BCPValue2 && sEI > numLiterals) { return true; }
 
	      // Subproblem unsatisfiable?
	      if (!BCPValue1 && !BCPValue2) { resetUnitClauseSearchArray(); return false; }
	
	      // Compare the sets of implications forced by "Literal" and "-Literal".
	      for (L=startPtr; L<endPtr; L++)
		{ if (tmpDS[L] == Assignment[tmpDS[L] >> 1]) { foundImplications.push(tmpDS[L]); } }

	      // Undo the decision and all the implications forced by this decision.
	      popLitDS(1);

	      // Has one of the two decisions forced a conflict, while the other option was "successful"?
	      if (BCPValue1 && !BCPValue2) 
		{ pushImplication(Literal<<1,0); }
	      else
		{ if (!BCPValue1 && BCPValue2) { pushImplication((Literal<<1)+1,0); } }

	      // Push all implications that are forced by the decisions "Literal" and "-Literal"
	      // onto the decision stack.
	      while(foundImplications.size() != 0)
		{ pushImplication(foundImplications.last(),0); foundImplications.pop(); }

	      // So, if we have any new implications on the stack, process them first before 
	      // performing the next "Unit Propagation Lookahead" step. 
	      if (sEI != ucEI) 
		{
		  // Update "Stack End Index".
		  sEI++;

		  // Process all implications on the decision stack.
		  while((BCPValue1 = BCP()) && sEI != ucEI && sEI <= numLiterals) { sEI++; }

		  // Let's take a look at the results.
		  if (!BCPValue1) { resetUnitClauseSearchArray(); return false; }
		  if (sEI > numLiterals) { return true; } 
		}
	    }

	  // Is it time for some checks?
	  if ((Ctr & 4095) == 0)
	    {
	      // Should the overall search process be stopped?
	      if (masterControl->masterDone != 0) { return true; }

	      // What about the preprocessing CPU limit?
	      if ((getTime() - myStartTime) >= maxPreTime) { return true; }
	    }
	}

      // Any mandatory variable assignments found?
      if (sEIstart == sEI) { return true; }

      // Should the overall search process be stopped?
      if (masterControl->masterDone != 0) { return true; }

      // What about the preprocessing CPU limit?
      if ((getTime() - myStartTime) >= maxPreTime) { return true; }
      
      // Determine the next set of literals for which "Unit Propagation Lookahead" will be performed.
      for (L=sEIstart; L<sEI; L++)
	{
	  for (C=0; C<Lit2Clauses[DecisionStack[L]^1].size(); C++)
	    {
	      tmpClause = clauseVec[Lit2Clauses[DecisionStack[L]^1][C]];
	      Ptr       = clauseStart;

	      while (tmpClause[Ptr] != 0)
		{ 
		  Literal = tmpClause[Ptr] >> 1;

		  if (!Lits2SearchCheck[Literal] && Assignment[Literal] == 0)
		    { 
		      Lits2Search.push(Literal); 
		      Lits2SearchCheck[Literal] = true; 
		    }

		  Ptr++;
		}
	    }
	}                	
    }
}