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

// Remove the clause "clauseAddress" from the list of clauses currently watched by "WL".
inline void Thread::removeWL(int WL, int clauseAddress)
{
  int Size = WLVec[WL].size();
  int Ptr  = 0;
  while(Ptr < Size && WLVec[WL][Ptr] != clauseAddress) { Ptr++; }
  WLVec[WL].rem(Ptr);
}

// Remove the clause "clauseAddress" from "binClauseVec".
inline void Thread::removeWLBIN(int WL0, int WL1, int clauseAddress)
{
  // Variables.
  int clause;

  if ((clause = binClauseVec[WL0 ^ 1].containsOdd(clauseAddress)) < binClauseVec[WL0 ^ 1].size())
    { 
      binClauseVec[WL0 ^ 1].rem(clause); 
      binClauseVec[WL0 ^ 1].rem(clause - 1); 
    }

  if ((clause = binClauseVec[WL1 ^ 1].containsOdd(clauseAddress)) < binClauseVec[WL1 ^ 1].size())
    { 
      binClauseVec[WL1 ^ 1].rem(clause); 
      binClauseVec[WL1 ^ 1].rem(clause - 1); 
    }
}

// Sort the list of clauses to be deleted with increasing activity.
void Thread::sortDeletedClausesVec(int Low, int High)
{     
  // A variant of Quicksort is used to sort the list of clauses by increasing activity.
  if (High > Low && Low < (deletedClausesVec.size()>>2))
    {
      int Pivot = clauseActivity[deletedClausesVec[High]];
      int I = Low - 1;
      int J = High;
      int H;
 
      while (true)
	{
	  do { I++; } while (Pivot > clauseActivity[deletedClausesVec[I]]);
	  do { J--; } while (Pivot < clauseActivity[deletedClausesVec[J]] && J > 0);
          if (I >= J) { break; }
	  H = deletedClausesVec[I];    
	  deletedClausesVec[I] = deletedClausesVec[J];
	  deletedClausesVec[J] = H;
	}
  
      H = deletedClausesVec[I];    
      deletedClausesVec[I] = deletedClausesVec[High];
      deletedClausesVec[High] = H;
      
      sortDeletedClausesVec(Low,I-1);   
      sortDeletedClausesVec(I+1,High); 
    }
  
  return;
}

// Clean both the local and the global clause database by removing less active clauses.
void Thread::cleanClauseDB(void)
{ 
  // Variables.
  int  EndPos = clauseVec.size();
  int* tmpClause;
  int  Ptr, nPtr;
  int  EmptyClauses = 0;
  int  numClausesDeleted;
  int  Clause;

  // Currently on decision level 0?
  if (currentDL == 0)
    {    
      // Check all clauses and delete the ones that are already satisfied on decision level 0, since
      // these clauses are not relevant for the current subproblem. Of course, clauses of the original 
      // CNF file can't be deleted, such clauses get "deactivated" by removing the watched literals and 
      // "reactivated" during "getNewDecisionStackAddDeactivatedClauses" when receiving a new subproblem.
      for (Ptr=0; Ptr<EndPos; Ptr++)
        {
	  // Get the next clause.
	  tmpClause = clauseVec[Ptr];

	  // "tmpClause" currently not "deactivated", not a unit clause, and also satisfied?
	  if((WLRL[Ptr << 2] != 0) && tmpClause[clauseLengthPos] > 2 && satisfiedClause(tmpClause))
            {
	      // Remove the watched literals of "tmpClause".
	      if(tmpClause[clauseLengthPos] == 3) { removeWLBIN(WLRL[Ptr<<2],WLRL[(Ptr<<2)+1],Ptr); }
	      else { removeWL(WLRL[Ptr<<2],Ptr); removeWL(WLRL[(Ptr<<2)+1],Ptr); }
	      WLRL[Ptr<<2]     = 0;
	      WLRL[(Ptr<<2)+1] = 0;
	      WLRL[(Ptr<<2)+2] = 0;
	      WLRL[(Ptr<<2)+3] = 0;

	      // In case that "tmpClause" is not one of the original clauses and consists of more 
	      // than "maxClauseSize" literals, it should be a good idea to delete "tmpClause".
	      if (Ptr >= myCEIBase && tmpClause[clauseLengthPos] > maxClauseSize) 
		{ theClauseDB->deleteClause(clauseVec[Ptr],myThreadNum); clauseVec[Ptr] = NULL; }
            }
        }
    }
  else
    {
      // Initialize "deletedClauseVec".
      deletedClausesVec.clearFast();

      // Initialization (save the last 512 clauses).
      EndPos = clauseVec.size() - 512;           

      // First of all, mark all clauses currently forcing an implication so that these clauses can't be deleted.
      for (Ptr=DLLookupArray[1]; Ptr<ucEI; Ptr++) 
	{ if (forcingClauseDS[Ptr] > -1) { clauseLocked[forcingClauseDS[Ptr]] = true; } }
        
      // Determine which clauses are candidates to be deleted.
      for(Ptr=myCEIBase; Ptr<EndPos; Ptr++)
        {
	  // "Normalize" clause activity.
	  clauseActivity[Ptr] = clauseActivity[Ptr] >> 1;

	  // Current clause not locked and containing more than "maxClauseSize" literals?
	  if (WLRL[Ptr<<2] != 0 && !clauseLocked[Ptr] && clauseVec[Ptr][clauseLengthPos] > maxClauseSize)
	    { deletedClausesVec.push(Ptr); }
	  else 
	    { if (clauseVec[Ptr] == NULL) { EmptyClauses++; } }
        }
      
      // Undo all "forcing clause locks".
      for (Ptr=DLLookupArray[1]; Ptr<ucEI; Ptr++)  
	{ if (forcingClauseDS[Ptr] > 0) { clauseLocked[forcingClauseDS[Ptr]] = false; } }
      
      // How many candidates do we have?
      if(deletedClausesVec.size() > 512)
        {
	  // Increment the number of local "clause deletion" operations.
	  localDeletedCount++;

	  // Sort "deletedClauseVec" with an increasing clause activity.
	  sortDeletedClausesVec(0,deletedClausesVec.size()-1); 
	  
	  // Don't delete all clauses in "deletedClausVec", but only the most "inactive" ones.
	  numClausesDeleted = deletedClausesVec.size() >> 2;
	  
	  // Increment the number of empty entries within "clauseVec".
	  EmptyClauses = EmptyClauses + numClausesDeleted;
	  
	  // Now, delete the most "inactive" clauses.
	  for(Ptr=0; Ptr<numClausesDeleted; Ptr++)
            {
	      // Get clause number / address.
	      Clause = deletedClausesVec[Ptr];
	      
	      // Remove watched literals.
	      removeWL(WLRL[ Clause<<2   ],Clause);
	      removeWL(WLRL[(Clause<<2)+1],Clause);
	      WLRL[ Clause<<2   ] = 0;
	      WLRL[(Clause<<2)+1] = 0;

	      // Set the global "to be deleted" flag for thread "myThreadNum".
	      theClauseDB->deleteClause(clauseVec[Clause],myThreadNum);

	      // Remove the clause from the local clause database.
	      clauseVec[Clause] = NULL;
            }
        }
      
      // Now, test if we deleted a lot of local clauses. Then the local database gets 
      // compacted to get rid of all "NULL entries" within the different arrays. 
      if (EmptyClauses > 8192)
        {
	  // Define some kind of "helper array" to store the "new" position 
	  // of the clauses after shrinking the local clause database.
	  vec<int> HA; HA.growTo(clauseVec.size() - myCEIBase + 1);

	  // Initialization.
	  nPtr   = myCEIBase;
	  EndPos = clauseVec.size();

	  // Shrink local clause database.
	  for (Ptr=myCEIBase; Ptr<EndPos; Ptr++)
            {
	      if (clauseVec[Ptr] != 0)
                {
		  // Move current clause.
		  HA[Ptr-myCEIBase]    = nPtr;
		  clauseVec[nPtr]      = clauseVec[Ptr];
		  WLRL[nPtr<<2]        = WLRL[Ptr<<2];
		  WLRL[(nPtr<<2)+1]    = WLRL[(Ptr<<2)+1];
		  WLRL[(nPtr<<2)+2]    = WLRL[(Ptr<<2)+2];
		  WLRL[(nPtr<<2)+3]    = WLRL[(Ptr<<2)+3];
		  clauseActivity[nPtr] = clauseActivity[Ptr];
		  nPtr++;
                }
            }

	  // Remove empty entries, which are now located as 
	  // one block at the end of the various arrays.
	  clauseVec.popto(nPtr); 
	  WLRL.popto(nPtr<<2); 
	  clauseActivity.popto(nPtr); 
	  clauseLocked.popto(nPtr);
	  
	  // Update current "forcing clauses".
	  for (Ptr=0; Ptr<ucEI; Ptr++)
            { 
	      if (forcingClauseDS[Ptr] >= myCEIBase) 
		{ forcingClauseDS[Ptr] = HA[forcingClauseDS[Ptr] - myCEIBase]; }
	    }
	  
	  // Update "binClauseVec".
	  int MaxLit = (numLiterals << 1) + 1;
	  for (Ptr=0; Ptr<=MaxLit; Ptr++)
	    {
	      for (nPtr=1; nPtr<binClauseVec[Ptr].size(); nPtr+=2)
		{
		  if (binClauseVec[Ptr][nPtr] >= myCEIBase) 
		    { binClauseVec[Ptr][nPtr] = HA[binClauseVec[Ptr][nPtr] - myCEIBase]; }
		}
	    }
	  
	  // Update "WLVec".
	  for (Ptr=0; Ptr<=MaxLit; Ptr++)
	    {
	      for (nPtr=0; nPtr<WLVec[Ptr].size(); nPtr++)
		{ 
		  if (WLVec[Ptr][nPtr] >= myCEIBase) 
		    { WLVec[Ptr][nPtr] = HA[WLVec[Ptr][nPtr] - myCEIBase]; }
		}
	    }
        } 
    }

  // So, after cleaning the local clause database, what about the global one?
  int C = localDeletedCount + (masterControl->numThreads * myThreadNum);
  int T = (masterControl->numThreads << 1) + 1;
  if ((C % T) == myThreadNum) { theClauseDB->cleanMasterClauseDB(); }

  return;
}