LazyInfo Class Reference

List of all members.

Public Member Functions
	LazyInfo (MLN *mln, Domain *domain)
	~LazyInfo ()
int	getVarCount ()
void	copyMLN ()
void	setHardClauseWeight ()
void	removeSoftClauses ()
void	reset ()
bool	isActive (int atom)
bool	isDeactivated (int atom)
void	setActive (int atom)
void	setInactive (int atom)
void	updatePredArray ()
void	getSupersetClauses (Array< IntClause * > &supersetClauses)
void	selectClauses (const Array< IntClause * > &supersetClauses, Array< Array< int > * > &walksatClauses, Array< int > &walksatClauseWts)
void	getWalksatClauses (Predicate *inputPred, Array< Array< int > * > &walksatClauses, Array< int > &walksatClauseWts, bool const &active)
	Get clauses and weights activated by the predicate inputPred, if active is true.
void	getWalksatClauses (Array< Array< int > * > &allClauses, Array< int > &allClauseWeights)
void	getWalksatClausesWhenFlipped (int atom, Array< Array< int > * > &walksatClauses, Array< int > &walksatClauseWts)
int	getUnSatCostPerPred (Predicate *pred, Array< Array< int > * > &walksatClauses, Array< int > &walksatClauseWts)
int	getUnSatCostWhenFlipped (int atom, Array< Array< int > * > &walksatClauses, Array< int > &walksatClauseWts)
void	setVarVals (int newVals[])
void	flipVar (int atom)
bool	getVarVal (int atom)
void	setVarVal (int atom, bool val)
Predicate *	getVar (int atom)
void	setAllActive ()
void	setAllInactive ()
void	setAllFalse ()
void	removeVars (Array< int > indices)
void	setSampleSat (bool s)
bool	getSampleSat ()
void	setPrevDB ()
int	getNumDBAtoms ()
bool	activateRandomAtom (Array< Array< int > * > &walksatClauses, Array< int > &walksatClauseWts, int &toflip)
void	chooseOtherToFlip (int atom, Array< Array< int > * > &walksatClauses, Array< int > &walksatClauseWts)
void	setOthersInBlockToFalse (const int &atomIdx, const int &blockIdx)
void	initBlocks ()
int	getBlock (int atom)
bool	inBlock (int atom)
bool	inBlockWithEvidence (int atom)
bool	getInBlock ()
void	setInBlock (const bool val)
int	getOtherAtom ()
void	setOtherAtom (const int val)
void	setEvidence (const int atom, const bool val)
bool	getEvidence (const int atom)
void	incrementNumDBAtoms ()
void	decrementNumDBAtoms ()
void	printIntClauses (Array< IntClause * > clauses)
void	propagateFixedAtoms (Array< Array< int > * > &clauses, Array< int > &clauseWeights, bool *fixedAtoms, int maxFixedAtoms)
Static Public Attributes
static double	HARD_WT
static double	WSCALE

---

Detailed Description

Definition at line 79 of file lazyinfo.h.

---

Member Function Documentation

void LazyInfo::getWalksatClauses	(	Predicate *	inputPred,
		Array< Array< int > * > &	walksatClauses,
		Array< int > &	walksatClauseWts,
		bool const &	active
	)			[inline]

Get clauses and weights activated by the predicate inputPred, if active is true.

If false, inactive clauses (and their weights) containing inputPred are retrieved. If inputPred is NULL, then all active (or inactive) clauses and their weights are retrieved.

Definition at line 406 of file lazyinfo.h.

References Array< Type >::append(), HashArray< Type, HashFn, EqualFn >::append(), Array< Type >::clear(), HashArray< Type, HashFn, EqualFn >::contains(), IntClause::deleteIntPredicates(), HashArray< Type, HashFn, EqualFn >::find(), Clause::getActiveClauses(), MLN::getClause(), MLN::getClausesContainingPred(), Domain::getDB(), Database::getDeactivatedStatus(), Predicate::getId(), Clause::getInactiveClauses(), IntClause::getIntPredicates(), MLN::getNumClauses(), IntClause::getWt(), Clause::getWt(), Clause::isHardClause(), IntClause::isSatisfied(), IntClause::setWt(), HashArray< Type, HashFn, EqualFn >::size(), Array< Type >::size(), updatePredArray(), and WSCALE.

Referenced by activateRandomAtom(), chooseOtherToFlip(), getWalksatClauses(), getWalksatClausesWhenFlipped(), and propagateFixedAtoms().

{
    // Randomizer
  int seed;
  struct timeval tv;
  struct timezone tzp;
  gettimeofday(&tv,&tzp);
  seed = (unsigned int)((( tv.tv_sec & 0177 ) * 1000000) + tv.tv_usec);
  srandom(seed);
  
  Clause *fclause;
  IntClause *intClause;
  int clauseCnt;
  IntClauseHashArray clauseHashArray;

  Array<IntClause *>* intClauses = new Array<IntClause *>; 
  
  const Array<IndexClause*>* indexClauses = NULL;
      
  if(inputPred == NULL)
  {
        clauseCnt = mln_->getNumClauses();
  }
  else
  {
        if (domain_->getDB()->getDeactivatedStatus(inputPred)) return;
        int predid = inputPred->getId(); 
        indexClauses = mln_->getClausesContainingPred(predid);
        clauseCnt = indexClauses->size();
  }

  int clauseno = 0;
  while(clauseno < clauseCnt)
  {
        if(inputPred)
          fclause = (Clause *) (*indexClauses)[clauseno]->clause;                       
        else
          fclause = (Clause *) mln_->getClause(clauseno);
        
        double wt = fclause->getWt();
    intClauses->clear();
        bool ignoreActivePreds = false;

    if (active)
    {
          fclause->getActiveClauses(inputPred, domain_, intClauses,
                                    &predHashArray_, ignoreActivePreds);
    }
    else
    {
      fclause->getInactiveClauses(inputPred, domain_, intClauses,
                                  &predHashArray_);
    }
    updatePredArray();
cout << "intClauses size " << intClauses->size() << endl;
        for (int i = 0; i < intClauses->size(); i++)
    {
      intClause = (*intClauses)[i];

                // If using samplesat, then do clause selection
          if (sampleSat_)
          {
                assert(prevDB_);

                  // Pos. clause not satisfied in prev. iteration: don't activate
          // Neg. clause satisfied in prev. iteration: don't activate
        bool sat = intClause->isSatisfied(&predHashArray_, prevDB_);
                if ((wt >= 0 && !sat) ||
            (wt < 0 && sat))
                {
                  intClause->deleteIntPredicates();
                  delete intClause;
                  continue;
                }

          // In dead clauses: don't activate
        if (deadClauses_.contains(intClause))
        {
          intClause->deleteIntPredicates();
          delete intClause;
          continue;
        }

          // With prob. exp(-wt) don't ever activate it
                double threshold =
                  fclause->isHardClause() ? RAND_MAX : RAND_MAX*(1-exp(-abs(wt)));

                if (random() > threshold)
                {
                  deadClauses_.append(intClause);
                  continue;
                }
          }

          int pos = clauseHashArray.find(intClause);
          if(pos >= 0)
          {
                clauseHashArray[pos]->addWt(wt);
                intClause->deleteIntPredicates();
                delete intClause;
                continue;
          }
           
          intClause->setWt(wt);
          clauseHashArray.append(intClause);
        }
        clauseno++;     
  } //while(clauseno < clauseCnt)
          
  Array<int>* litClause;
  for(int i = 0; i < clauseHashArray.size(); i++)
  {
        intClause = clauseHashArray[i];
        double weight = intClause->getWt();
        litClause = (Array<int> *)intClause->getIntPredicates();
        walksatClauses.append(litClause);
        if (sampleSat_)
    {
      if (weight >= 0) walksatClauseWts.append(1);
      else walksatClauseWts.append(-1);
    }
        else
        {
      if (weight >= 0)
        walksatClauseWts.append((int)(weight*LazyInfo::WSCALE + 0.5));
      else
        walksatClauseWts.append((int)(weight*LazyInfo::WSCALE - 0.5));
        }
        
    delete intClause;
  }
                 
  delete intClauses;
}

---

The documentation for this class was generated from the following files:

• src/infer/lazyinfo.h
• src/infer/intclause.cpp

---