VariableState Class Reference

Represents the state of propositional variables and clauses. More...

#include <variablestate.h>

List of all members.

Public Member Functions
	VariableState (GroundPredicateHashArray *const &unknownQueries, GroundPredicateHashArray *const &knownQueries, Array< TruthValue > *const &knownQueryValues, const Array< int > *const &allPredGndingsAreQueries, const bool &markHardGndClauses, const bool &trackParentClauseWts, const MLN *const &mln, const Domain *const &domain, const bool &lazy)
	Constructor for a VariableState.
	~VariableState ()
	Destructor.
void	addNewClauses (bool initial)
	New clauses are added to the state.
void	init ()
	Information about the state is reset and initialized.
void	initRandom ()
	Makes a random truth assigment to all (active) atoms.
void	initBlocksRandom ()
	Sets one atom in each block to true and the rest to false.
void	initMakeBreakCostWatch (const int &startClause)
	Initialize makeCost and breakCost and watch arrays based on the current variable assignment.
int	getNumAtoms ()
int	getNumClauses ()
int	getNumDeadClauses ()
int	getIndexOfRandomAtom ()
	Returns the absolute index of a random atom.
int	getIndexOfAtomInRandomFalseClause ()
	Returns the absolute index of a random atom in a random unsatisfied pos.
int	getRandomFalseClauseIndex ()
	Returns the index of a random unsatisfied pos.
long double	getCostOfFalseClauses ()
	Returns the cost of the unsatisfied positive and satisfied negative clauses.
int	getNumFalseClauses ()
	Returns the number of the unsatisfied positive and satisfied negative clauses.
bool	getValueOfAtom (const int &atomIdx)
	Returns the truth value of an atom.
bool	getValueOfLowAtom (const int &atomIdx)
	Returns the truth value of an atom in the best state.
void	setValueOfAtom (const int &atomIdx, const bool &value)
	Sets the truth value of an atom.
Array< int > &	getNegOccurenceArray (const int &atomIdx)
	Retrieves the negative occurence array of an atom.
Array< int > &	getPosOccurenceArray (const int &atomIdx)
	Retrieves the positive occurence array of an atom.
void	flipAtom (const int &toFlip)
	Flip the truth value of an atom and update info arrays.
void	flipAtomValue (const int &atomIdx)
	Flips the truth value of an atom.
long double	getImprovementByFlipping (const int &atomIdx)
	Calculates the improvement achieved by flipping an atom.
void	activateAtom (const int &atomIdx, const bool &ignoreActivePreds)
	If in lazy mode, an atom is activated and all clauses activated by this atom are added to the state.
bool	isActive (const int &atomIdx)
	Checks if an atom is active.
bool	isActive (const Predicate *pred)
	Checks if an atom is active.
Array< int > &	getOccurenceArray (const int &idx)
	Retrieves the occurence array of an atom.
int	incrementNumTrueLits (const int &clauseIdx)
	Increments the number of true literals in a clause.
int	decrementNumTrueLits (const int &clauseIdx)
	Decrements the number of true literals in a clause.
int	getNumTrueLits (const int &clauseIdx)
	Retrieves the number of true literals in a clause.
long double	getClauseCost (const int &clauseIdx)
	Retrieves the cost associated with a clause.
Array< int > &	getAtomsInClause (const int &clauseIdx)
	Retrieves the atoms in a clauses as an Array of ints.
void	addFalseClause (const int &clauseIdx)
	Marks a clause as false in the state.
void	removeFalseClause (const int &clauseIdx)
	Unmarks a clause as false in the state.
void	addBreakCost (const int &atomIdx, const long double &cost)
	Increases the breakcost of an atom.
void	subtractBreakCost (const int &atomIdx, const long double &cost)
	Decreases the breakcost of an atom.
void	addBreakCostToAtomsInClause (const int &clauseIdx, const long double &cost)
	Increases breakCost of all atoms in a given clause.
void	subtractBreakCostFromAtomsInClause (const int &clauseIdx, const long double &cost)
	Decreases breakCost of all atoms in a given clause.
void	addMakeCost (const int &atomIdx, const long double &cost)
	Increases makeCost of an atom.
void	subtractMakeCost (const int &atomIdx, const long double &cost)
	Decreases makeCost of an atom.
void	addMakeCostToAtomsInClause (const int &clauseIdx, const long double &cost)
	Increases makeCost of all atoms in a given clause.
void	subtractMakeCostFromAtomsInClause (const int &clauseIdx, const long double &cost)
	Decreases makeCost of all atoms in a given clause.
const int	getTrueLiteralOtherThan (const int &clauseIdx, const int &atomIdx1, const int &atomIdx2)
	Retrieves a true literal in a clause other than the two given.
const bool	isTrueLiteral (const int &literal)
	Checks if a literal is true (Negated and false or non-negated an true).
const int	getAtomInClause (const int &atomIdxInClause, const int &clauseIdx)
	Retrieves the absolute index of the nth atom in a clause.
const int	getRandomAtomInClause (const int &clauseIdx)
	Retrieves the absolute index of a random atom in a clause.
const int	getRandomTrueLitInClause (const int &clauseIdx)
	Retrieves the index of a random true literal in a clause.
const double	getMaxClauseWeight ()
const long double	getMakeCost (const int &atomIdx)
const long double	getBreakCost (const int &atomIdx)
const int	getClauseSize (const int &clauseIdx)
const int	getWatch1 (const int &clauseIdx)
void	setWatch1 (const int &clauseIdx, const int &atomIdx)
const int	getWatch2 (const int &clauseIdx)
void	setWatch2 (const int &clauseIdx, const int &atomIdx)
const bool	isBlockEvidence (const int &blockIdx)
const int	getBlockSize (const int &blockIdx)
const int	getBlockIndex (const int &atomIdx)
	Returns the index of the block which the atom with index atomIdx is in.
Array< int > &	getBlockArray (const int &blockIdx)
bool	getBlockEvidence (const int &blockIdx)
int	getNumBlocks ()
const long double	getLowCost ()
	Returns the cost of bad clauses in the optimum state.
const int	getLowBad ()
	Returns the number of bad clauses in the optimum state.
void	makeUnitCosts ()
	Turns all costs into units.
void	saveLowState ()
	Save current assignment as an optimum state.
int	getTrueFixedAtomInBlock (const int blockIdx)
	Returns index in block if a true fixed atom is in block, otherwise -1.
const GroundPredicateHashArray *	getGndPredHashArrayPtr () const
const GroundPredicateHashArray *	getUnePreds () const
const GroundPredicateHashArray *	getKnePreds () const
const Array< TruthValue > *	getKnePredValues () const
void	setGndClausesWtsToSumOfParentWts ()
	Sets the weight of a ground clause to the sum of its parents' weights.
void	getNumClauseGndings (Array< double > *const &numGndings, bool tv)
	Gets the number of (true or false) clause groundings in this state.
void	getNumClauseGndings (double numGndings[], int clauseCnt, bool tv)
	Gets the number of (true or false) clause groundings in this state.
void	getNumClauseGndingsWithUnknown (double numGndings[], int clauseCnt, bool tv, const Array< bool > *const &unknownPred)
	Gets the number of (true or false) clause groundings in this state.
void	setOthersInBlockToFalse (const int &atomIdx, const int &blockIdx)
	Sets the truth values of all atoms in a block except for the one given.
void	fixAtom (const int &atomIdx, const bool &value)
	Fixes an atom to a truth value.
Array< int > *	simplifyClauseFromFixedAtoms (const int &clauseIdx)
	Simplifies a clause using atoms which have been fixed.
const bool	isDeadClause (const int &clauseIdx)
	Checks if a clause is dead.
void	eliminateSoftClauses ()
	Marks soft clauses as dead.
void	killClauses (const int &startClause)
	Marks clauses as dead which were not good in the previous iteration of inference or are not picked according to a weighted coin flip.
const bool	clauseGoodInPrevious (const int &clauseIdx)
	Checks if a clause was good in the previous iteration of inference, i.e.
void	resetDeadClauses ()
	Resets all dead clauses to be alive again.
void	resetFixedAtoms ()
	Resets all fixed atoms to be not fixed again.
void	setLazy (const bool &l)
const bool	getLazy ()
void	setUseThreshold (const bool &t)
const bool	getUseThreshold ()
long double	getHardWt ()
const Domain *	getDomain ()
const MLN *	getMLN ()
void	printLowState (ostream &out)
	Prints the best state found to a stream.
void	printGndPred (const int &predIndex, ostream &out)
	Prints a ground predicate to a stream.
GroundPredicate *	getGndPred (const int &index)
	Gets a pointer to a GroundPredicate.
GroundClause *	getGndClause (const int &index)
	Gets a pointer to a GroundClause.
void	saveLowStateToGndPreds ()
	The atom assignment in the best state is saved to the ground predicates.
void	saveLowStateToDB ()
	The atom assignment in the best state is saved to the database.
const int	getGndPredIndex (GroundPredicate *const &gndPred)
	Gets the index of a GroundPredicate in this state.
void	getActiveClauses (Predicate *inputPred, Array< GroundClause * > &activeClauses, bool const &active, bool const &ignoreActivePreds)
	Gets clauses and weights activated by the predicate inputPred, if active is true.
void	getActiveClauses (Array< GroundClause * > &allClauses, bool const &ignoreActivePreds)
	Get all the active clauses in the database.
int	getNumActiveAtoms ()
void	addOneAtomToEachBlock ()
	Selects one atom in each block in the domain and adds it to the block here and sets it to true.
void	initLazyBlocks ()
	Initializes the block structures for the lazy version.
void	fillLazyBlocks ()
	Fills the blocks with the predicates in the domain blocks.

---

Detailed Description

Represents the state of propositional variables and clauses.

Some of this code is based on the MaxWalkSat package of Kautz et al.

All inference algorithms should have a VariableState to access the information needed in its predicates and clauses.

Each atom has its own index starting at 1. The negation of an atom with index a is represented by -a (this is why the indices do not start at 0). Each clause has its own index starting at 0.

A VariableState is either eager or lazy. Eager states build an MRF upfront based on an MLN and a domain. Thus, all ground clauses and predicates are in memory after building the MRF. Lazy states activate atoms and clauses as they are needed from the MLN and domain. An atom is activated if it is in an unsatisfied clause with the assumption of all atoms being false or if it is looked at during inference (it is flipped or the cost of flipping it is computed). Active clauses are those which contain active atoms.

Definition at line 93 of file variablestate.h.

---

Constructor & Destructor Documentation

VariableState::VariableState	(	GroundPredicateHashArray *const &	unknownQueries,
		GroundPredicateHashArray *const &	knownQueries,
		Array< TruthValue > *const &	knownQueryValues,
		const Array< int > *const &	allPredGndingsAreQueries,
		const bool &	markHardGndClauses,
		const bool &	trackParentClauseWts,
		const MLN *const &	mln,
		const Domain *const &	domain,
		const bool &	lazy
	)			[inline]

Constructor for a VariableState.

The hard clause weight is set. In lazy mode, the initial active atoms and clauses are retrieved and in eager mode, the MRF is built and the atoms and clauses are retrieved from it. In addition, all information arrays are filled with information.

Parameters:

	unknownQueries	Query predicates with unknown values used to build MRF in eager mode.
	knownQueries	Query predicates with known values used to build MRF in eager mode.
	knownQueryValues	Truth values of the known query predicates.
	allPredGndingsAreQueries	Array used to build MRF in eager mode.
	mln	mln and domain are used to build MRF in eager state and to retrieve active atoms in lazy state.
	domain	mln and domain are used to build MRF in eager state and to retrieve active atoms in lazy state.
	lazy	Flag stating whether lazy mode is used or not.

Definition at line 115 of file variablestate.h.

References addNewClauses(), addOneAtomToEachBlock(), HashArray< Type, HashFn, EqualFn >::append(), Array< Type >::clear(), MRF::deleteGndPredsGndClauseSets(), fillLazyBlocks(), getActiveClauses(), MRF::getBlockEvidence(), MRF::getBlocks(), Domain::getDB(), MRF::getGndClauses(), MRF::getGndPreds(), getNumClauses(), initLazyBlocks(), Database::setActiveStatus(), Database::setPerformingInference(), HashArray< Type, HashFn, EqualFn >::size(), and Array< Type >::size().

  {
    this->mln_ = (MLN*)mln;
    this->domain_ = (Domain*)domain;
    this->lazy_ = lazy;

      // Instantiate information
    baseNumAtoms_ = 0;
    activeAtoms_ = 0;
    numFalseClauses_ = 0;
    costOfFalseClauses_ = 0.0;
    lowCost_ = LDBL_MAX;
    lowBad_ = INT_MAX;

      // Clauses and preds are stored in gndClauses_ and gndPreds_
    gndClauses_ = new Array<GroundClause*>;
    gndPreds_ = new Array<GroundPredicate*>;

      // Set the hard clause weight
    setHardClauseWeight();

      // Lazy version: Produce state with initial active atoms and clauses
    if (lazy_)
    {
        // Unknown preds are treated as false
      domain_->getDB()->setPerformingInference(true);

        // Blocks are copied from the domain
      initLazyBlocks();

      clauseLimit_ = INT_MAX;
      noApprox_ = false;
      haveDeactivated_ = false;

        // Get initial set of active atoms (atoms in unsat. clauses)
        // Assumption is: all atoms are initially false except those in blocks

        // One atom in each block is set to true and activated
      addOneAtomToEachBlock();

//cout << "After addOneAtomToEachBlock" << endl;
//for (int i = 1; i < atom_.size(); i++)
//  cout << atom_[i] << endl;

      bool ignoreActivePreds = false;
      getActiveClauses(newClauses_, ignoreActivePreds);
      int defaultCnt = newClauses_.size();
      long double defaultCost = 0;

      for (int i = 0; i < defaultCnt; i++)
      {
        if (newClauses_[i]->isHardClause())
          defaultCost += hardWt_;
        else
          defaultCost += abs(newClauses_[i]->getWt());
      }

        // Clear ground clauses in the ground preds
      for (int i = 0; i < gndPredHashArray_.size(); i++)
        gndPredHashArray_[i]->removeGndClauses();

        // Delete new clauses
      for (int i = 0; i < newClauses_.size(); i++)
        delete newClauses_[i];
      newClauses_.clear();

      baseNumAtoms_ = gndPredHashArray_.size();
      cout << "Number of Baseatoms = " << baseNumAtoms_ << endl;
      cout << "Default => Cost\t" << "******\t" << " Clause Cnt\t" << endl;
      cout << "           " << defaultCost << "\t" << "******\t" << defaultCnt
           << "\t" << endl << endl;

        // Set base atoms as active in DB
      for (int i = 0; i < baseNumAtoms_; i++)
      {
        domain_->getDB()->setActiveStatus(gndPredHashArray_[i], true);
        activeAtoms_++;        
      }

        // Add the rest of the atoms in the blocks, but don't activate
      fillLazyBlocks();

        // Get the initial set of active clauses
      ignoreActivePreds = false;
      getActiveClauses(newClauses_, ignoreActivePreds);      
    } // End lazy version
      // Eager version: Use KBMC to produce the state
    else
    {
      unePreds_ = unknownQueries;
      knePreds_ = knownQueries;
      knePredValues_ = knownQueryValues;

        // MRF is built on known and unknown queries
      int size = 0;
      if (unknownQueries) size += unknownQueries->size();
      if (knownQueries) size += knownQueries->size();
      GroundPredicateHashArray* queries = new GroundPredicateHashArray(size);
      if (unknownQueries) queries->append(unknownQueries);
      if (knownQueries) queries->append(knownQueries);
      mrf_ = new MRF(queries, allPredGndingsAreQueries, domain_,
                     domain_->getDB(), mln_, markHardGndClauses,
                     trackParentClauseWts, -1);
        //delete to save space. Can be deleted because no more gndClauses are
        //appended to gndPreds beyond this point
      mrf_->deleteGndPredsGndClauseSets();
        //do not delete the intArrRep in gndPreds_;
      delete queries;

        // Blocks built in MRF
      blocks_ = mrf_->getBlocks();
      blockEvidence_ = mrf_->getBlockEvidence();
        
        // Put ground clauses in newClauses_
      newClauses_ = *(Array<GroundClause*>*)mrf_->getGndClauses();
        // Put ground preds in the hash array
      //const Array<GroundPredicate*>* gndPreds = mrf_->getGndPreds();
      const GroundPredicateHashArray* gndPreds = mrf_->getGndPreds();
      for (int i = 0; i < gndPreds->size(); i++)
        gndPredHashArray_.append((*gndPreds)[i]);
    
        // baseNumAtoms_ are all atoms in eager version
      baseNumAtoms_ = gndPredHashArray_.size();        
    } // End eager version
    
      // At this point, ground clauses are held in newClauses_
      // and ground predicates are held in gndPredHashArray_
      // for both versions
    
      // Add the clauses and preds and fill info arrays
    bool initial = true;
    addNewClauses(initial);
    
    cout << "Initial num. of clauses: " << getNumClauses() << endl;
  }

VariableState::~VariableState

(

)

[inline]

Destructor.

Blocks are deleted in lazy version; MRF is deleted in eager version.

Definition at line 263 of file variablestate.h.

References Array< Type >::size().

  {
    if (lazy_)
    {
        // Block information from lazy version is deleted
      for (int i = 0; i < blocks_->size(); i++)
        (*blocks_)[i].clearAndCompress();
      delete blocks_;
    
      delete blockEvidence_;  
    }
    else
    {
        // MRF from eager version is deleted
      if (mrf_) delete mrf_;
      //if (unePreds_) delete unePreds_;
      //if (knePreds_) delete knePreds_;
      //if (knePredValues_) delete knePredValues_;
    }    
  }

---

Member Function Documentation

void VariableState::addNewClauses

(

bool

initial

)

[inline]

New clauses are added to the state.

If not the initialization, then makecost and breakcost are updated for the new atoms.

Parameters:

initial

If true, this is the first time new clauses have been added.

Definition at line 292 of file variablestate.h.

References Array< Type >::append(), Array< Type >::clear(), Domain::getDB(), getNumAtoms(), getNumClauses(), Database::getValue(), Array< Type >::growToSize(), initMakeBreakCostWatch(), killClauses(), HashArray< Type, HashFn, EqualFn >::size(), and Array< Type >::size().

Referenced by activateAtom(), addOneAtomToEachBlock(), fillLazyBlocks(), and VariableState().

  {
    if (vsdebug)
      cout << "Adding " << newClauses_.size() << " new clauses.." << endl;

      // Store the old number of clauses and atoms
    int oldNumClauses = getNumClauses();
    int oldNumAtoms = getNumAtoms();

    gndClauses_->append(newClauses_);
    gndPreds_->growToSize(gndPredHashArray_.size());

    int numAtoms = getNumAtoms();
    int numClauses = getNumClauses();
      // If no new atoms or clauses have been added, then do nothing
    if (numAtoms == oldNumAtoms && numClauses == oldNumClauses) return;

    if (vsdebug) cout << "Clauses: " << numClauses << endl;

      // atomIdx starts at 1
    atom_.growToSize(numAtoms + 1, false);
    makeCost_.growToSize(numAtoms + 1, 0.0);
    breakCost_.growToSize(numAtoms + 1, 0.0);
    lowAtom_.growToSize(numAtoms + 1, false);
    fixedAtom_.growToSize(numAtoms + 1, 0);

      // Copy ground preds to gndPreds_ and set values in atom and lowAtom
    for (int i = oldNumAtoms; i < gndPredHashArray_.size(); i++)
    {
      (*gndPreds_)[i] = gndPredHashArray_[i];

      if (vsdebug)
      {
        cout << "New pred: ";
        (*gndPreds_)[i]->print(cout, domain_);
        cout << endl;
      }

      lowAtom_[i + 1] = atom_[i + 1] = 
        (domain_->getDB()->getValue((*gndPreds_)[i]) == TRUE) ? true : false;
    }
    newClauses_.clear();

    clause_.growToSize(numClauses);
    clauseCost_.growToSize(numClauses);
    falseClause_.growToSize(numClauses);
    whereFalse_.growToSize(numClauses);
    numTrueLits_.growToSize(numClauses);
    watch1_.growToSize(numClauses);
    watch2_.growToSize(numClauses);
    isSatisfied_.growToSize(numClauses, false);
    deadClause_.growToSize(numClauses, false);
    threshold_.growToSize(numClauses, false);

    occurence_.growToSize(2*numAtoms + 1);

    for (int i = oldNumClauses; i < numClauses; i++)
    {
      GroundClause* gndClause = (*gndClauses_)[i];

      if (vsdebug)
      {
        cout << "New clause: ";
        gndClause->print(cout, domain_, &gndPredHashArray_);
        cout << endl;
      }
      
        // Set thresholds for clause selection
      if (gndClause->isHardClause()) threshold_[i] = RAND_MAX;
      else
      {
        double w = gndClause->getWt();
        threshold_[i] = RAND_MAX*(1 - exp(-abs(w)));
        if (vsdebug)
        {
          cout << "Weight: " << w << endl;            
        }
      }
      if (vsdebug)
        cout << "Threshold: " << threshold_[i] << endl;            
      
      int numGndPreds = gndClause->getNumGroundPredicates();
      clause_[i].growToSize(numGndPreds);

      for (int j = 0; j < numGndPreds; j++) 
      {
          // idx in gndClause + 1 (negated if neg. literal)
        //int idx = gndClause->getGroundPredicateIndex(j);
        //assert(idx >= 0);
        //int lit = (gndClause->getGroundPredicateSense(j)) ?
        //          idx + 1 : -(idx + 1);
        int lit = gndClause->getGroundPredicateIndex(j);
        clause_[i][j] = lit;
        int litIdx = 2*abs(lit) - (lit > 0);
        occurence_[litIdx].append(i);
      }

        // Hard clause weight has been previously determined
      if (gndClause->isHardClause())
        clauseCost_[i] = hardWt_;
      else
        clauseCost_[i] = gndClause->getWt();
    }

    if (!initial)
    {
      //initNumSatLiterals(1, oldNumClauses);
      if (useThreshold_)
      {
        killClauses(oldNumClauses);
      }
      else
      {
        initMakeBreakCostWatch(oldNumClauses);
      }
    }
    if (vsdebug) cout << "Done adding new clauses.." << endl;
  }

void VariableState::initRandom

(

)

[inline]

Makes a random truth assigment to all (active) atoms.

Blocks are taken into account: exactly one atom in the block is set to true and the others are set to false.

Definition at line 432 of file variablestate.h.

References getBlockIndex(), init(), initBlocksRandom(), and setValueOfAtom().

Referenced by MaxWalkSat::init().

  {
      // Set one in each block to true randomly
    initBlocksRandom();

      // Random truth value for all not in blocks
    for (int i = 1; i <= baseNumAtoms_; i++)
    {
        // fixedAtom_[i] = -1: false, fixedAtom_[i] = 1: true
      if (fixedAtom_[i] != 0) setValueOfAtom(i, (fixedAtom_[i] == 1));
        // Blocks are initialized above
      if (getBlockIndex(i - 1) >= 0)
      {
        if (vsdebug) cout << "Atom " << i << " in block" << endl;
        continue;
      }
        // Not fixed and not in block
      else
      {
        if (vsdebug) cout << "Atom " << i << " not in block" << endl;
        setValueOfAtom(i, random() % 2);
      }
    }
    init();
  }

void VariableState::initMakeBreakCostWatch

(

const int &

startClause

)

[inline]

Initialize makeCost and breakCost and watch arrays based on the current variable assignment.

Parameters:

startClause

All clauses with index of this or greater are initialized.

Definition at line 515 of file variablestate.h.

References getClauseSize(), getNumClauses(), and isTrueLiteral().

Referenced by addNewClauses(), eliminateSoftClauses(), init(), killClauses(), and resetDeadClauses().

  {
    int theTrueLit = -1;
      // Initialize breakCost and makeCost in the following:
    for (int i = startClause; i < getNumClauses(); i++)
    {
        // Don't look at dead clauses
      if (deadClause_[i]) continue;
      int trueLit1 = 0;
      int trueLit2 = 0;
      long double cost = clauseCost_[i];
      numTrueLits_[i] = 0;
      for (int j = 0; j < getClauseSize(i); j++)
      {
        if (isTrueLiteral(clause_[i][j]))
        { // ij is true lit
          numTrueLits_[i]++;
          theTrueLit = abs(clause_[i][j]);
          if (!trueLit1) trueLit1 = theTrueLit;
          else if (trueLit1 && !trueLit2) trueLit2 = theTrueLit;
        }
      }

        // Unsatisfied positive-weighted clauses or
        // Satisfied negative-weighted clauses
      if ((numTrueLits_[i] == 0 && cost > 0) ||
          (numTrueLits_[i] > 0 && cost < 0))
      {
        whereFalse_[i] = numFalseClauses_;
        falseClause_[numFalseClauses_] = i;
        numFalseClauses_++;
        costOfFalseClauses_ += abs(cost);
        if (highestCost_ == abs(cost)) {eqHighest_ = true; numHighest_++;}

          // Unsat. pos. clause: increase makeCost_ of all atoms
        if (numTrueLits_[i] == 0)
          for (int j = 0; j < getClauseSize(i); j++)
          {
            makeCost_[abs(clause_[i][j])] += cost;
          }

          // Sat. neg. clause: increase makeCost_ if one true literal
        if (numTrueLits_[i] == 1)
        {
            // Subtract neg. cost
          makeCost_[theTrueLit] -= cost;
          watch1_[i] = theTrueLit;
        }
        else if (numTrueLits_[i] > 1)
        {
          watch1_[i] = trueLit1;
          watch2_[i] = trueLit2;
        }
      }
        // Pos. clauses satisfied by one true literal
      else if (numTrueLits_[i] == 1 && cost > 0)
      {
        breakCost_[theTrueLit] += cost;
        watch1_[i] = theTrueLit;
      }
        // Pos. clauses satisfied by 2 or more true literals
      else if (cost > 0)
      { /*if (numtruelit[i] == 2)*/
        watch1_[i] = trueLit1;
        watch2_[i] = trueLit2;
      }
        // Unsat. neg. clauses: increase breakCost of all atoms
      else if (numTrueLits_[i] == 0 && cost < 0)
      {
        for (int j = 0; j < getClauseSize(i); j++)
          breakCost_[abs(clause_[i][j])] -= cost;
      }
    } // for all clauses
  }

int VariableState::getIndexOfAtomInRandomFalseClause

(

)

[inline]

Returns the absolute index of a random atom in a random unsatisfied pos.

clause or the absolute index of a random true literal in a random satisfied clause.

Definition at line 617 of file variablestate.h.

References getClauseSize(), and getRandomTrueLitInClause().

Referenced by MaxWalkSat::pickRandom().

  {
    if (numFalseClauses_ == 0) return NOVALUE;
    int clauseIdx = falseClause_[random()%numFalseClauses_];
      // Pos. clause: return index of random atom
    if (clauseCost_[clauseIdx] > 0)
      return abs(clause_[clauseIdx][random()%getClauseSize(clauseIdx)]);
      // Neg. clause: find random true lit
    else
      return getRandomTrueLitInClause(clauseIdx);
  }

int VariableState::getRandomFalseClauseIndex

(

)

[inline]

Returns the index of a random unsatisfied pos.

clause or a random satisfied neg. clause.

Definition at line 633 of file variablestate.h.

Referenced by MaxWalkSat::pickBest(), and MaxWalkSat::pickTabu().

  {
    if (numFalseClauses_ == 0) return NOVALUE;
    return falseClause_[random()%numFalseClauses_];
  }

bool VariableState::getValueOfAtom

(

const int &

atomIdx

)

[inline]

Returns the truth value of an atom.

Index of atom whose truth value is returned.

Returns:

Truth value of atom.

Definition at line 663 of file variablestate.h.

Referenced by MaxWalkSat::calculateImprovement(), flipAtom(), and MaxWalkSat::pickRandom().

  {
    return atom_[atomIdx];
  }

bool VariableState::getValueOfLowAtom

(

const int &

atomIdx

)

[inline]

Returns the truth value of an atom in the best state.

Index of atom whose truth value is returned.

Returns:

Truth value of atom.

Definition at line 674 of file variablestate.h.

Referenced by UnitPropagation::getProbability(), SAT::getProbability(), UnitPropagation::printProbabilities(), SAT::printProbabilities(), UnitPropagation::printTruePreds(), SAT::printTruePreds(), and MCMC::saveLowStateToChain().

  {
    return lowAtom_[atomIdx];
  }

void VariableState::setValueOfAtom	(	const int &	atomIdx,
		const bool &	value
	)			[inline]

Sets the truth value of an atom.

The truth value is propagated to the database.

Parameters:

	atomIdx	Index of atom whose value is to be set.
	value	Truth value being set.

Definition at line 686 of file variablestate.h.

References activateAtom(), Domain::getDB(), isActive(), and Database::setValue().

Referenced by addOneAtomToEachBlock(), fixAtom(), flipAtomValue(), initBlocksRandom(), initRandom(), and setOthersInBlockToFalse().

  {
    if (vsdebug) cout << "Setting value of atom " << atomIdx 
                      << " to " << value << endl;
      // If atom already has this value, then do nothing
    if (atom_[atomIdx] == value) return;
      // Propagate assigment to DB
    GroundPredicate* p = gndPredHashArray_[atomIdx - 1];
    if (value)
    {
      domain_->getDB()->setValue(p, TRUE);
    }
    else
    {
      domain_->getDB()->setValue(p, FALSE);
    }
      // If not active, then activate it
    if (lazy_ && !isActive(atomIdx))
    {
      bool ignoreActivePreds = false;
      activateAtom(atomIdx, ignoreActivePreds);
    }
    atom_[atomIdx] = value;
  }

void VariableState::flipAtom

(

const int &

toFlip

)

[inline]

Flip the truth value of an atom and update info arrays.

Parameters:

toFlip

Index of atom to be flipped.

Definition at line 734 of file variablestate.h.

References addBreakCost(), addBreakCostToAtomsInClause(), addFalseClause(), addMakeCost(), addMakeCostToAtomsInClause(), decrementNumTrueLits(), flipAtomValue(), getClauseCost(), getOccurenceArray(), getTrueLiteralOtherThan(), getValueOfAtom(), getWatch1(), getWatch2(), incrementNumTrueLits(), removeFalseClause(), setWatch1(), setWatch2(), and Array< Type >::size().

Referenced by MaxWalkSat::flipAtom(), and getImprovementByFlipping().

  {
    bool toFlipValue = getValueOfAtom(toFlip);
    register int clauseIdx;
    int sign;
    int oppSign;
    int litIdx;
    if (toFlipValue)
      sign = 1;
    else
      sign = 0;
    oppSign = sign ^ 1;

    flipAtomValue(toFlip);
    
      // Update all clauses in which the atom occurs as a true literal
    litIdx = 2*toFlip - sign;
    Array<int>& posOccArray = getOccurenceArray(litIdx);
    for (int i = 0; i < posOccArray.size(); i++)
    {
      clauseIdx = posOccArray[i];
        // Don't look at dead clauses
      if (deadClause_[clauseIdx]) continue;
        // The true lit became a false lit
      int numTrueLits = decrementNumTrueLits(clauseIdx);
      long double cost = getClauseCost(clauseIdx);
      int watch1 = getWatch1(clauseIdx);
      int watch2 = getWatch2(clauseIdx);

        // 1. If last true lit was flipped, then we have to update
        // the makecost / breakcost info accordingly        
      if (numTrueLits == 0)
      {
          // Pos. clause
        if (cost > 0)
        {
            // Add this clause as false in the state
          addFalseClause(clauseIdx);
            // Decrease toFlip's breakcost (add neg. cost)
          addBreakCost(toFlip, -cost);
            // Increase makecost of all vars in clause (add pos. cost)
          addMakeCostToAtomsInClause(clauseIdx, cost);
        }
          // Neg. clause
        else
        {
          assert(cost < 0);
            // Remove this clause as false in the state
          removeFalseClause(clauseIdx);
            // Increase breakcost of all vars in clause (add pos. cost)
          addBreakCostToAtomsInClause(clauseIdx, -cost);        
            // Decrease toFlip's makecost (add neg. cost)
          addMakeCost(toFlip, cost);
        }
      }
        // 2. If there is now one true lit left, then move watch2
        // up to watch1 and increase the breakcost / makecost of watch1
      else if (numTrueLits == 1)
      {
        if (watch1 == toFlip)
        {
          assert(watch1 != watch2);
          setWatch1(clauseIdx, watch2);
          watch1 = getWatch1(clauseIdx);
        }

          // Pos. clause: Increase toFlip's breakcost (add pos. cost)
        if (cost > 0)
        {
          addBreakCost(watch1, cost);
        }
          // Neg. clause: Increase toFlip's makecost (add pos. cost)
        else
        {
          assert(cost < 0);
          addMakeCost(watch1, -cost);
        }
      }
        // 3. If there are 2 or more true lits left, then we have to
        // find a new true lit to watch if one was flipped
      else
      { /* numtruelit[clauseIdx] >= 2 */
          // If watch1[clauseIdx] has been flipped
        if (watch1 == toFlip)
        {
            // find a different true literal to watch
          int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
          setWatch1(clauseIdx, diffTrueLit);
        }
          // If watch2[clauseIdx] has been flipped
        else if (watch2 == toFlip)
        {
            // find a different true literal to watch
          int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
          setWatch2(clauseIdx, diffTrueLit);
        }
      }
    }
        
      // Update all clauses in which the atom occurs as a false literal
    litIdx = 2*toFlip - oppSign;
    Array<int>& negOccArray = getOccurenceArray(litIdx);
    for (int i = 0; i < negOccArray.size(); i++)
    {
      clauseIdx = negOccArray[i];
        // Don't look at dead clauses
      if (deadClause_[clauseIdx]) continue;
        // The false lit became a true lit
      int numTrueLits = incrementNumTrueLits(clauseIdx);
      long double cost = getClauseCost(clauseIdx);
      int watch1 = getWatch1(clauseIdx);

        // 1. If this is the only true lit, then we have to update
        // the makecost / breakcost info accordingly        
      if (numTrueLits == 1)
      {
          // Pos. clause
        if (cost > 0)
        {
            // Remove this clause as false in the state
          removeFalseClause(clauseIdx);
            // Increase toFlip's breakcost (add pos. cost)
          addBreakCost(toFlip, cost);        
            // Decrease makecost of all vars in clause (add neg. cost)
          addMakeCostToAtomsInClause(clauseIdx, -cost);
        }
          // Neg. clause
        else
        {
          assert(cost < 0);
            // Add this clause as false in the state
          addFalseClause(clauseIdx);
            // Decrease breakcost of all vars in clause (add neg. cost)
          addBreakCostToAtomsInClause(clauseIdx, cost);
            // Increase toFlip's makecost (add pos. cost)
          addMakeCost(toFlip, -cost);
        }
          // Watch this atom
        setWatch1(clauseIdx, toFlip);
      }
        // 2. If there are now exactly 2 true lits, then watch second atom
        // and update breakcost
      else
      if (numTrueLits == 2)
      {
        if (cost > 0)
        {
            // Pos. clause
            // Decrease breakcost of first atom being watched (add neg. cost)
          addBreakCost(watch1, -cost);
        }
        else
        {
            // Neg. clause
          assert(cost < 0);
            // Decrease makecost of first atom being watched (add neg. cost)
          addMakeCost(watch1, cost);
        }
        
          // Watch second atom
        setWatch2(clauseIdx, toFlip);
      }
    }
  }

void VariableState::flipAtomValue

(

const int &

atomIdx

)

[inline]

Flips the truth value of an atom.

If in lazy mode, the truth value is propagated to the database.

Definition at line 903 of file variablestate.h.

References setValueOfAtom().

Referenced by flipAtom(), and MaxWalkSat::reconstructLowState().

  {
    bool opposite = !atom_[atomIdx];
    setValueOfAtom(atomIdx, opposite);
  }

long double VariableState::getImprovementByFlipping

(

const int &

atomIdx

)

[inline]

Calculates the improvement achieved by flipping an atom.

This is the cost of clauses which flipping the atom makes good minus the cost of clauses which flipping the atom makes bad. In lazy mode, if the atom is not active, then the atom is activated and the makecost and breakcost are updated.

Parameters:

atomIdx

Index of atom to flip.

Returns:

Improvement achieved by flipping the atom.

Definition at line 920 of file variablestate.h.

References flipAtom(), and isActive().

Referenced by MaxWalkSat::calculateImprovement().

  {
    if (lazy_ && !isActive(atomIdx))
    {
        // First flip the atom to activate it, then flip it back
      flipAtom(atomIdx);
      flipAtom(atomIdx);
    }
    long double improvement = makeCost_[atomIdx] - breakCost_[atomIdx];
    return improvement;
  }

void VariableState::activateAtom	(	const int &	atomIdx,
		const bool &	ignoreActivePreds
	)			[inline]

If in lazy mode, an atom is activated and all clauses activated by this atom are added to the state.

If in eager mode, nothing happens.

Parameters:

atomIdx

Index of atom to be activated.

Definition at line 938 of file variablestate.h.

References addNewClauses(), getActiveClauses(), Domain::getDB(), isActive(), and Database::setActiveStatus().

Referenced by setValueOfAtom().

  {
      // Lazy version: if atom is not active, we need to activate clauses
      // and take their cost into account
    if (lazy_ && !isActive(atomIdx))
    {
      Predicate* p =
        gndPredHashArray_[atomIdx - 1]->createEquivalentPredicate(domain_);
      getActiveClauses(p, newClauses_, true, ignoreActivePreds);
        // Add the clauses and preds and fill info arrays
      bool initial = false;
      addNewClauses(initial);
        // Set active status in db
      domain_->getDB()->setActiveStatus(p, true);
      activeAtoms_++;
      delete p;
    }        
  }

bool VariableState::isActive

(

const int &

atomIdx

)

[inline]

Checks if an atom is active.

Parameters:

atomIdx

Index of atom to be checked.

Returns:

true, if atom is active, otherwise false.

Definition at line 963 of file variablestate.h.

References Database::getActiveStatus(), and Domain::getDB().

Referenced by activateAtom(), getImprovementByFlipping(), and setValueOfAtom().

  {
    return domain_->getDB()->getActiveStatus(gndPredHashArray_[atomIdx-1]);
  }

bool VariableState::isActive

(

const Predicate *

pred

)

[inline]

Checks if an atom is active.

Parameters:

pred

Predicate to be checked.

Returns:

true, if atom is active, otherwise false.

Definition at line 974 of file variablestate.h.

References Database::getActiveStatus(), and Domain::getDB().

  {
    return domain_->getDB()->getActiveStatus(pred);
  }

void VariableState::addBreakCostToAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Increases breakCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' breakCost is altered.
	cost	Cost to be added to atoms' breakCost.

Definition at line 1071 of file variablestate.h.

References getClauseSize().

Referenced by flipAtom().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      breakCost_[abs(lit)] += cost;
    }
  }

void VariableState::subtractBreakCostFromAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Decreases breakCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' breakCost is altered.
	cost	Cost to be subtracted from atoms' breakCost.

Definition at line 1088 of file variablestate.h.

References getClauseSize().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      breakCost_[abs(lit)] -= cost;
    }
  }

void VariableState::addMakeCost	(	const int &	atomIdx,
		const long double &	cost
	)			[inline]

Increases makeCost of an atom.

Parameters:

	atomIdx	Index of atom whose makeCost is altered.
	cost	Cost to be added to atom's makeCost.

Definition at line 1105 of file variablestate.h.

Referenced by flipAtom().

  {
    makeCost_[atomIdx] += cost;
  }

void VariableState::subtractMakeCost	(	const int &	atomIdx,
		const long double &	cost
	)			[inline]

Decreases makeCost of an atom.

Parameters:

	atomIdx	Index of atom whose makeCost is altered.
	cost	Cost to be subtracted from atom's makeCost.

Definition at line 1116 of file variablestate.h.

  {
    makeCost_[atomIdx] -= cost;
  }

void VariableState::addMakeCostToAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Increases makeCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' makeCost is altered.
	cost	Cost to be added to atoms' makeCost.

Definition at line 1127 of file variablestate.h.

References getClauseSize().

Referenced by flipAtom().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      makeCost_[abs(lit)] += cost;
    }
  }

void VariableState::subtractMakeCostFromAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Decreases makeCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' makeCost is altered.
	cost	Cost to be subtracted from atoms' makeCost.

Definition at line 1144 of file variablestate.h.

References getClauseSize().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      makeCost_[abs(lit)] -= cost;
    }
  }

const int VariableState::getTrueLiteralOtherThan	(	const int &	clauseIdx,
		const int &	atomIdx1,
		const int &	atomIdx2
	)			[inline]

Retrieves a true literal in a clause other than the two given.

Parameters:

	clauseIdx	Index of clause from which literal is retrieved.
	atomIdx1	Index of first atom excluded from search.
	atomIdx2	Index of second atom excluded from search.

Returns:

Index of atom found.

Definition at line 1164 of file variablestate.h.

References getClauseSize(), and isTrueLiteral().

Referenced by flipAtom().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      register int v = abs(lit);
      if (isTrueLiteral(lit) && v != atomIdx1 && v != atomIdx2)
        return v;
    }
      // If we're here, then no other true lit exists
    assert(false);
    return -1;
  }

const int VariableState::getRandomTrueLitInClause

(

const int &

clauseIdx

)

[inline]

Retrieves the index of a random true literal in a clause.

Parameters:

clauseIdx

Index of clause from which the literal is retrieved.

Returns:

Index of the atom retrieved.

Definition at line 1211 of file variablestate.h.

References getClauseSize(), and isTrueLiteral().

Referenced by getIndexOfAtomInRandomFalseClause(), and MaxWalkSat::pickBest().

  {
    assert(numTrueLits_[clauseIdx] > 0);
    int trueLit = random()%numTrueLits_[clauseIdx];
    int whichTrueLit = 0;
    for (int i = 0; i < getClauseSize(clauseIdx); i++)
    {
      int lit = clause_[clauseIdx][i];
      int atm = abs(lit);
        // True literal
      if (isTrueLiteral(lit))
        if (trueLit == whichTrueLit++)
          return atm;
    }
      // If we're here, then no other true lit exists
    assert(false);
    return -1;
  }

const int VariableState::getBlockIndex

(

const int &

atomIdx

)

[inline]

Returns the index of the block which the atom with index atomIdx is in.

If not in any, returns -1.

Definition at line 1294 of file variablestate.h.

References Array< Type >::size().

Referenced by MaxWalkSat::calculateImprovement(), SimulatedTempering::infer(), initRandom(), MCMC::performGibbsStep(), MaxWalkSat::pickRandom(), and MCMC::randomInitGndPredsTruthValues().

  {
    for (int i = 0; i < blocks_->size(); i++)
    {
      int blockIdx = (*blocks_)[i].find(atomIdx);
      if (blockIdx >= 0)
        return i;
    }
    return -1;
  }

void VariableState::makeUnitCosts

(

)

[inline]

Turns all costs into units.

Positive costs are converted to 1, negative costs are converted to -1

Definition at line 1340 of file variablestate.h.

References Array< Type >::size().

Referenced by MCSAT::init().

  {
    for (int i = 0; i < clauseCost_.size(); i++)
    {
      if (clauseCost_[i] > 0) clauseCost_[i] = 1.0;
      else
      {
        assert(clauseCost_[i] < 0);
        clauseCost_[i] = -1.0;
      }
    }
  }

void VariableState::getNumClauseGndings	(	Array< double > *const &	numGndings,
		bool	tv
	)			[inline]

Gets the number of (true or false) clause groundings in this state.

If eager, the first order clause frequencies in the mrf are used.

Parameters:

	numGndings	Array being filled with values
	clauseCnt
	tv

Definition at line 1421 of file variablestate.h.

References MLN::getNumClauses(), getNumTrueLits(), and Array< Type >::size().

Referenced by SimulatedTempering::infer(), MaxWalkSat::infer(), and MCMC::performGibbsStep().

  {
    // TODO: lazy version
    IntPairItr itr;
    IntPair *clauseFrequencies;
    
      // numGndings should have been initialized with non-negative values
    int clauseCnt = numGndings->size();
    assert(clauseCnt == mln_->getNumClauses());
    for (int clauseno = 0; clauseno < clauseCnt; clauseno++)
      assert ((*numGndings)[clauseno] >= 0);
    
    for (int i = 0; i < gndClauses_->size(); i++)
    {
      GroundClause *gndClause = (*gndClauses_)[i];
      int satLitcnt = getNumTrueLits(i);
      if (tv && satLitcnt == 0)
        continue;
      if (!tv && satLitcnt > 0)
        continue;

      clauseFrequencies = gndClause->getClauseFrequencies();
      for (itr = clauseFrequencies->begin();
           itr != clauseFrequencies->end(); itr++)
      {
        int clauseno = itr->first;
        int frequency = itr->second;
        (*numGndings)[clauseno] += frequency;
      }
    }
  }

void VariableState::getNumClauseGndings	(	double	numGndings[],
		int	clauseCnt,
		bool	tv
	)			[inline]

Gets the number of (true or false) clause groundings in this state.

If eager, the first order clause frequencies in the mrf are used.

Parameters:

	numGndings
	clauseCnt
	tv

Definition at line 1461 of file variablestate.h.

References getNumTrueLits(), and Array< Type >::size().

  {
    // TODO: lazy version
    IntPairItr itr;
    IntPair *clauseFrequencies;
    
    for (int clauseno = 0; clauseno < clauseCnt; clauseno++)
      numGndings[clauseno] = 0;
    
    for (int i = 0; i < gndClauses_->size(); i++)
    {
      GroundClause *gndClause = (*gndClauses_)[i];
      int satLitcnt = getNumTrueLits(i);
      if (tv && satLitcnt == 0)
        continue;
      if (!tv && satLitcnt > 0)
        continue;

      clauseFrequencies = gndClause->getClauseFrequencies();
      for (itr = clauseFrequencies->begin();
           itr != clauseFrequencies->end(); itr++)
      {
        int clauseno = itr->first;
        int frequency = itr->second;
        numGndings[clauseno] += frequency;
      }
    }
  }

void VariableState::getNumClauseGndingsWithUnknown	(	double	numGndings[],
		int	clauseCnt,
		bool	tv,
		const Array< bool > *const &	unknownPred
	)			[inline]

Gets the number of (true or false) clause groundings in this state.

If eager, the first order clause frequencies in the mrf are used.

Parameters:

	numGndings	Will hold the number of groundings for each first-order clause.
	clauseCnt	Number of first-order clauses whose groundings are being counted.
	tv	If true, true groundings are counted, otherwise false groundings.
	unknownPred	If pred is marked as unknown, it is ignored in the count

Definition at line 1501 of file variablestate.h.

References getNumAtoms(), isTrueLiteral(), and Array< Type >::size().

  {
    assert(unknownPred->size() == getNumAtoms());
    IntPairItr itr;
    IntPair *clauseFrequencies;
    
    for (int clauseno = 0; clauseno < clauseCnt; clauseno++)
      numGndings[clauseno] = 0;
    
    for (int i = 0; i < gndClauses_->size(); i++)
    {
      GroundClause *gndClause = (*gndClauses_)[i];
      int satLitcnt = 0;
      bool unknown = false;
      for (int j = 0; j < gndClause->getNumGroundPredicates(); j++)
      {
        int lit = gndClause->getGroundPredicateIndex(j);
        if ((*unknownPred)[abs(lit) - 1])
        {
          unknown = true;
          continue;
        }
        if (isTrueLiteral(lit)) satLitcnt++;
      }
      
      if (tv && satLitcnt == 0)
        continue;
      if (!tv && (satLitcnt > 0 || unknown))
        continue;

      clauseFrequencies = gndClause->getClauseFrequencies();
      for (itr = clauseFrequencies->begin();
           itr != clauseFrequencies->end(); itr++)
      {
        int clauseno = itr->first;
        int frequency = itr->second;
        numGndings[clauseno] += frequency;
      }
    }
  }

void VariableState::setOthersInBlockToFalse	(	const int &	atomIdx,
		const int &	blockIdx
	)			[inline]

Sets the truth values of all atoms in a block except for the one given.

Parameters:

	atomIdx	Index of atom in block exempt from being set to false.
	blockIdx	Index of block whose atoms are set to false.

Definition at line 1550 of file variablestate.h.

References setValueOfAtom(), and Array< Type >::size().

Referenced by addOneAtomToEachBlock(), and initBlocksRandom().

  {
    Array<int>& block = (*blocks_)[blockIdx];
    for (int i = 0; i < block.size(); i++)
    {
        // Atom not the one specified and not fixed
      if (i != atomIdx && fixedAtom_[block[i] + 1] == 0)
        setValueOfAtom(block[i] + 1, false);
    }
  }

void VariableState::fixAtom	(	const int &	atomIdx,
		const bool &	value
	)			[inline]

Fixes an atom to a truth value.

This means the atom can not change its truth values again. If the atom has already been fixed to the opposite value, then we have a contradiction and the program terminates.

Parameters:

	atomIdx	Index of atom to be fixed.
	value	Truth value to which the atom is fixed.

Definition at line 1571 of file variablestate.h.

References setValueOfAtom().

Referenced by UnitPropagation::infer().

  {
    assert(atomIdx > 0);
      // If already fixed to opp. sense, then contradiction
    if ((fixedAtom_[atomIdx] == 1 && value == false) ||
        (fixedAtom_[atomIdx] == -1 && value == true))
    {
      cout << "Contradiction: Tried to fix atom " << atomIdx <<
      " to true and false ... exiting." << endl;
      exit(0);
    }

    if (vsdebug)
    {
      cout << "Fixing ";
      (*gndPreds_)[atomIdx - 1]->print(cout, domain_);
      cout << " to " << value << endl;
    }
    
    setValueOfAtom(atomIdx, value);
    fixedAtom_[atomIdx] = (value) ? 1 : -1;
  }

Array<int>* VariableState::simplifyClauseFromFixedAtoms

(

const int &

clauseIdx

)

[inline]

Simplifies a clause using atoms which have been fixed.

If clause is satisfied from the fixed atoms, this is marked in isSatisfied_ and an empty array is returned. If clause is empty and not satisfied, then a contradiction has occured. Otherwise, the simplified clause is returned.

Returned array should be deleted.

Parameters:

clauseIdx

Index of the clause to be simplified

Returns:

Simplified clause

Definition at line 1605 of file variablestate.h.

References Array< Type >::append(), Array< Type >::clear(), and getClauseSize().

Referenced by UnitPropagation::infer().

  {
    Array<int>* returnArray = new Array<int>;
      // If already satisfied from fixed atoms, then return empty array
    if (isSatisfied_[clauseIdx]) return returnArray;

      // Keeps track of pos. clause being satisfied or 
      // neg. clause being unsatisfied due to fixed atoms
    bool isGood = (clauseCost_[clauseIdx] > 0) ? false : true;
      // Keeps track of all atoms being fixed to false in a pos. clause
    bool allFalseAtoms = (clauseCost_[clauseIdx] > 0) ? true : false;
      // Check each literal in clause
    for (int i = 0; i < getClauseSize(clauseIdx); i++)
    {
      int lit = clause_[clauseIdx][i];
      int fixedValue = fixedAtom_[abs(lit)];

      if (clauseCost_[clauseIdx] > 0)
      { // Pos. clause: check if clause is satisfied
        if ((fixedValue == 1 && lit > 0) ||
            (fixedValue == -1 && lit < 0))
        { // True fixed lit
          isGood = true;
          allFalseAtoms = false;
          returnArray->clear();
          break;
        }
        else if (fixedValue == 0)
        { // Lit not fixed
          allFalseAtoms = false;
          returnArray->append(lit);
        }
      }
      else
      { // Neg. clause:
        assert(clauseCost_[clauseIdx] < 0);
        if ((fixedValue == 1 && lit > 0) ||
            (fixedValue == -1 && lit < 0))
        { // True fixed lit
          cout << "Contradiction: Tried to fix atom " << abs(lit) <<
          " to true in a negative clause ... exiting." << endl;
          exit(0);
        }
        else
        { // False fixed lit or non-fixed lit
          returnArray->append(lit);
            // Non-fixed lit
          if (fixedValue == 0) isGood = false;          
        }
      }
    }
    if (allFalseAtoms)
    {
      cout << "Contradiction: All atoms in clause " << clauseIdx <<
      " fixed to false ... exiting." << endl;
      exit(0);
    }
    if (isGood) isSatisfied_[clauseIdx] = true;
    return returnArray;
  }

const bool VariableState::isDeadClause

(

const int &

clauseIdx

)

[inline]

Checks if a clause is dead.

Parameters:

clauseIdx

Index of clause being checked.

Returns:

True, if clause is dead, otherwise false.

Definition at line 1672 of file variablestate.h.

Referenced by UnitPropagation::infer().

  {
    return deadClause_[clauseIdx];
  }

void VariableState::killClauses

(

const int &

startClause

)

[inline]

Marks clauses as dead which were not good in the previous iteration of inference or are not picked according to a weighted coin flip.

Parameters:

startClause

All clauses with index of this or greater are looked at to be killed.

Definition at line 1701 of file variablestate.h.

References clauseGoodInPrevious(), getNumClauses(), and initMakeBreakCostWatch().

Referenced by addNewClauses().

  {
    for (int i = startClause; i < getNumClauses(); i++)
    {
      GroundClause* clause = (*gndClauses_)[i];
      if ((clauseGoodInPrevious(i)) &&
          (clause->isHardClause() || random() <= threshold_[i]))
      {
        if (vsdebug)
        {
          cout << "Keeping clause "<< i << " ";
          clause->print(cout, domain_, &gndPredHashArray_);
          cout << endl;
        }
        deadClause_[i] = false;
      }
      else
      {
        deadClause_[i] = true;
      }
    }
    initMakeBreakCostWatch(startClause);
  }

const bool VariableState::clauseGoodInPrevious

(

const int &

clauseIdx

)

[inline]

Checks if a clause was good in the previous iteration of inference, i.e.

if it is positive and satisfied or negative and unsatisfied.

Parameters:

clauseIdx

Index of clause being checked.

Returns:

true, if clause was good, otherwise false.

Definition at line 1733 of file variablestate.h.

Referenced by killClauses().

  {
    //GroundClause* clause = (*gndClauses_)[clauseIdx];
    int numSatLits = numTrueLits_[clauseIdx];
      // Num. of satisfied lits in previous iteration is stored in clause
    if ((numSatLits > 0 && clauseCost_[clauseIdx] > 0.0) ||
        (numSatLits == 0 && clauseCost_[clauseIdx] < 0.0))
      return true;
    else
      return false;
  }

void VariableState::printLowState

(

ostream &

out

)

[inline]

Prints the best state found to a stream.

Parameters:

out

Stream to which the state is printed.

Definition at line 1783 of file variablestate.h.

References getNumAtoms().

Referenced by MCSAT::init().

  {
    for (int i = 0; i < getNumAtoms(); i++)
    {
      (*gndPreds_)[i]->print(out, domain_);
      out << " " << lowAtom_[i + 1] << endl;
    }
  }

void VariableState::printGndPred	(	const int &	predIndex,
		ostream &	out
	)			[inline]

Prints a ground predicate to a stream.

Parameters:

	predIndex	Index of predicate to be printed.
	out	Stream to which predicate is printed.

Definition at line 1798 of file variablestate.h.

Referenced by UnitPropagation::printProbabilities(), SAT::printProbabilities(), MCMC::printProbabilities(), UnitPropagation::printTruePreds(), SAT::printTruePreds(), and MCMC::printTruePreds().

  {
    (*gndPreds_)[predIndex]->print(out, domain_);
  }

GroundPredicate* VariableState::getGndPred

(

const int &

index

)

[inline]

Gets a pointer to a GroundPredicate.

Parameters:

index

Index of the GroundPredicate to be retrieved.

Returns:

Pointer to the GroundPredicate

Definition at line 1811 of file variablestate.h.

Referenced by MCMC::getProbabilityOfPred(), MCMC::gndPredFlippedUpdates(), SimulatedTempering::infer(), MCSAT::infer(), GibbsSampler::infer(), and MCMC::performGibbsStep().

  {
    return (*gndPreds_)[index];
  }

GroundClause* VariableState::getGndClause

(

const int &

index

)

[inline]

Gets a pointer to a GroundClause.

Parameters:

index

Index of the GroundClause to be retrieved.

Returns:

Pointer to the GroundClause

Definition at line 1822 of file variablestate.h.

Referenced by MCMC::gndPredFlippedUpdates(), MCMC::initNumTrueLits(), and MCMC::updateWtsForGndPreds().

  {
    return (*gndClauses_)[index];
  }

const int VariableState::getGndPredIndex

(

GroundPredicate *const &

gndPred

)

[inline]

Gets the index of a GroundPredicate in this state.

Parameters:

gndPred

GroundPredicate whose index is being found.

Returns:

Index of the GroundPredicate, if found; otherwise -1.

Definition at line 1862 of file variablestate.h.

References Array< Type >::find().

Referenced by UnitPropagation::getProbability(), SAT::getProbability(), and MCMC::getProbability().

  {
    return gndPreds_->find(gndPred);
  }

void VariableState::getActiveClauses	(	Predicate *	inputPred,
		Array< GroundClause * > &	activeClauses,
		bool const &	active,
		bool const &	ignoreActivePreds
	)			[inline]

Gets 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.

Parameters:

	inputPred	Only clauses containing this Predicate are looked at. If NULL, then all active clauses are retrieved.
	activeClauses	New active clauses are put here.
	active	If true, active clauses are retrieved, otherwise inactive.
	ignoreActivePreds	If true, active preds are not taken into account. This results in the retrieval of all unsatisfied clauses.

Definition at line 1886 of file variablestate.h.

References Array< Type >::append(), HashArray< Type, HashFn, EqualFn >::append(), GroundClause::appendParentWtPtr(), GroundClause::appendToGndPreds(), Array< Type >::clear(), HashArray< Type, HashFn, EqualFn >::find(), MLN::findClauseIdx(), Clause::getActiveClauses(), MLN::getClause(), MLN::getClausesContainingPred(), Domain::getDB(), Database::getDeactivatedStatus(), Predicate::getId(), MLN::getNumClauses(), GroundClause::getWt(), Clause::getWt(), Clause::getWtPtr(), GroundClause::incrementClauseFrequency(), Clause::isHardClause(), GroundClause::print(), Clause::print(), GroundClause::setWt(), HashArray< Type, HashFn, EqualFn >::size(), and Array< Type >::size().

Referenced by activateAtom(), getActiveClauses(), and VariableState().

  {
    Clause *fclause;
    GroundClause* newClause;
    int clauseCnt;
    GroundClauseHashArray clauseHashArray;

    Array<GroundClause*>* newClauses = new Array<GroundClause*>; 
  
    const Array<IndexClause*>* indexClauses = NULL;
      
      // inputPred is null: all active clauses should be retrieved
    if (inputPred == NULL)
    {
      clauseCnt = mln_->getNumClauses();
    }
      // Otherwise, look at all first order clauses containing the pred
    else
    {
      if (domain_->getDB()->getDeactivatedStatus(inputPred)) return;
      int predId = inputPred->getId();
      indexClauses = mln_->getClausesContainingPred(predId);
      clauseCnt = indexClauses->size();
    }

      // Look at each first-order clause and get active groundings
    int clauseno = 0;
    while (clauseno < clauseCnt)
    {
      if (inputPred)
        fclause = (Clause *) (*indexClauses)[clauseno]->clause;           
      else
        fclause = (Clause *) mln_->getClause(clauseno);

      if (vsdebug)
      {
        cout << "Getting active clauses for FO clause: ";
        fclause->print(cout, domain_);
        cout << endl;
      }
      
      long double wt = fclause->getWt();
      const double* parentWtPtr = NULL;
      if (!fclause->isHardClause()) parentWtPtr = fclause->getWtPtr();
      const int clauseId = mln_->findClauseIdx(fclause);
      newClauses->clear();

      fclause->getActiveClauses(inputPred, domain_, newClauses,
                                &gndPredHashArray_, ignoreActivePreds);

      for (int i = 0; i < newClauses->size(); i++)
      {
        newClause = (*newClauses)[i];
        int pos = clauseHashArray.find(newClause);
          // If clause already present, then just add weight
        if (pos >= 0)
        {
          if (vsdebug)
          {
            cout << "Adding weight " << wt << " to clause ";
            clauseHashArray[pos]->print(cout, domain_, &gndPredHashArray_);
            cout << endl;
          }
          clauseHashArray[pos]->addWt(wt);
          if (parentWtPtr)
          {
            clauseHashArray[pos]->appendParentWtPtr(parentWtPtr);
            clauseHashArray[pos]->incrementClauseFrequency(clauseId, 1);
          }
          delete newClause;
          continue;
        }

          // If here, then clause is not yet present        
        newClause->setWt(wt);
        newClause->appendToGndPreds(&gndPredHashArray_);
        if (parentWtPtr)
        {
          newClause->appendParentWtPtr(parentWtPtr);
          newClause->incrementClauseFrequency(clauseId, 1);
          assert(newClause->getWt() == *parentWtPtr);
        }      

        if (vsdebug)
        {
          cout << "Appending clause ";
          newClause->print(cout, domain_, &gndPredHashArray_);
          cout << endl;
        }
        clauseHashArray.append(newClause);
      }
      clauseno++; 
    } //while (clauseno < clauseCnt)

    for (int i = 0; i < clauseHashArray.size(); i++)
    {
      newClause = clauseHashArray[i];
      activeClauses.append(newClause);
    }
    delete newClauses;
  }

void VariableState::getActiveClauses	(	Array< GroundClause * > &	allClauses,
		bool const &	ignoreActivePreds
	)			[inline]

Get all the active clauses in the database.

Parameters:

	allClauses	Active clauses are retrieved into this Array.
	ignoreActivePreds	If true, active preds are ignored; this means all unsatisfied clauses are retrieved.

Definition at line 1998 of file variablestate.h.

References getActiveClauses().

  {
    getActiveClauses(NULL, allClauses, true, ignoreActivePreds);
  }

---

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

• src/logic/variablestate.h

---