MaxWalkSat Class Reference

The MaxWalkSat algorithm. More...

#include <maxwalksat.h>

Inheritance diagram for MaxWalkSat:

List of all members.

Public Member Functions
	MaxWalkSat (VariableState *state, int seed, const bool &trackClauseTrueCnts, MaxWalksatParams *params)
	Constructor: user-set parameters are set.
	~MaxWalkSat ()
	Destructor (destructors from superclasses are called).
void	init ()
	Initializes the MaxWalkSat algorithm.
void	infer ()
	Performs the given number of MaxWalkSat inference tries.
const int	getHeuristic ()
void	setHeuristic (const int &heuristic)
int	getMaxSteps ()
void	setMaxSteps (const int &maxSteps)
void	setPrintInfo (const bool &printInfo)
const bool	getPrintInfo ()
Protected Member Functions
void	flipAtom (int toFlip)
	Flips the truth value of an atom and marks this iteration as the last time it was flipped.
int	pickRandom ()
	Pick a random atom in a random unsatisfied pos.
int	pickBest ()
	Pick the best atom (clauses made satisfied - clauses made unsatisfied) in a random unsatisfied clause.
int	pickTabu ()
	Pick an atom from a random unsatisfied clause based on the tabu heuristic.
int	pickSS ()
	Pick an atom according to the SampleSat heuristic.
long double	calculateImprovement (const int &atomIdx, Array< int > &canNotFlip, Array< int > &candidateBlockedVars, Array< int > &othersToFlip, int &blockIdx)
	Calculates the improvement (makecost - breakcost) by flipping an atom.
void	reconstructLowState ()
	Reconstructs the state with the lowest cost by flipping atoms back to their value in this state.

---

Detailed Description

The MaxWalkSat algorithm.

This code is based on the MaxWalkSat package of Kautz et al. and SampleSat by Wei et al.

Walksat is achieved by using unit weights (1 and -1) in the clauses in the state and setting the target cost to 0.

SampleSat is achieved by using unit weights (1 and -1) in the clauses in the state and setting the target cost to 0 and the heuristic to SS.

Definition at line 94 of file maxwalksat.h.

---

Member Function Documentation

void MaxWalkSat::init

(

)

[inline, virtual]

Initializes the MaxWalkSat algorithm.

A random assignment is given to the atoms and the state is initialized.

Implements Inference.

Definition at line 161 of file maxwalksat.h.

References SAT::changed_, VariableState::getNumAtoms(), Array< Type >::growToSize(), VariableState::initRandom(), Array< Type >::shrinkToSize(), Array< Type >::size(), and Inference::state_.

Referenced by infer(), SimulatedTempering::init(), MCSAT::init(), and GibbsSampler::init().

  {
      // Init changed array if using tabu
    if (heuristic_ == TABU || heuristic_ == SS)
    {
      int numAtoms = state_->getNumAtoms();
      if (changed_.size() != numAtoms + 1)
      {
        if (changed_.size() < numAtoms + 1)
          changed_.growToSize(numAtoms + 1);
        else
          changed_.shrinkToSize(numAtoms + 1);
      }
      for (int i = 1; i <= numAtoms; i++)
        changed_[i] = -(tabuLength_ + 1);
    }
    state_->initRandom();
  }

void MaxWalkSat::flipAtom

(

int

toFlip

)

[inline, protected]

Flips the truth value of an atom and marks this iteration as the last time it was flipped.

Parameters:

toFlip

Index of atom to flip.

Definition at line 333 of file maxwalksat.h.

References SAT::changed_, VariableState::flipAtom(), VariableState::getNumAtoms(), Array< Type >::growToSize(), SAT::numFlips_, and Inference::state_.

Referenced by infer().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::flipAtom" << endl;
    if (toFlip == NOVALUE)
      return;

      // Flip the atom in the state
    state_->flipAtom(toFlip, inBlock_);
      // Mark this flip as last time atom was changed if tabu is used
    if (heuristic_ == TABU || heuristic_ == SS)
    {
      changed_.growToSize(state_->getNumAtoms() + 1, -(tabuLength_ + 1));
      changed_[toFlip] = numFlips_;
    }
    
    if (lazyLowState_)
    {
        // Mark this variable as flipped since last low state. If already
        // present, then it has been flipped back to its value in the low
        // state and we can remove it.
      if (varsFlippedSinceLowState_.find(toFlip) !=
          varsFlippedSinceLowState_.end())
      {
        if (mwsdebug)
        {
          //cout << "Atom " << toFlip << " has been flipped since low state, "
          //     << "so removing it" << endl;
        }
        varsFlippedSinceLowState_.erase(toFlip);
      }
      else
      {
        if (mwsdebug)
        {
          //cout << "Atom " << toFlip << " not flipped since low state, "
          //     << "so adding it" << endl;
        }
        varsFlippedSinceLowState_.insert(toFlip);
      }
    }
    //if (mwsdebug) cout << "Leaving MaxWalkSat::flipAtom" << endl;
  }

int MaxWalkSat::pickRandom

(

)

[inline, protected]

Pick a random atom in a random unsatisfied pos.

clause or a random true literal in a random satsified neg. clause to flip.

Returns:

Index of atom picked.

Definition at line 382 of file maxwalksat.h.

References VariableState::activateAtom(), Domain::getBlockEvidence(), VariableState::getBlockIndex(), Domain::getBlockSize(), VariableState::getDomain(), VariableState::getImprovementByFlipping(), VariableState::getIndexOfAtomInRandomFalseClause(), VariableState::getIndexOfGroundPredicate(), Domain::getPredInBlock(), Domain::getRandomPredInBlock(), VariableState::getValueOfAtom(), and Inference::state_.

Referenced by MaxWalkSat(), and pickBest().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::pickRandom" << endl;
    assert(inBlock_ == -1);
    int atomIdx = state_->getIndexOfAtomInRandomFalseClause();
    if (atomIdx == NOVALUE) return NOVALUE;
    if (state_->getImprovementByFlipping(atomIdx) == -LDBL_MAX) return NOVALUE;

      // if false => fix atoms
    bool ignoreActivePreds = false;
    bool groundOnly = false;
    if (!state_->activateAtom(atomIdx, ignoreActivePreds, groundOnly))
      return NOVALUE;

      // If atom is in a block, then another one has to be picked
    int blockIdx = state_->getBlockIndex(atomIdx - 1);
    if (blockIdx >= 0)
    {
        // Atom is in a block
        // If evidence atom exists or in block of size 1, then can not flip
      if (state_->getDomain()->getBlockEvidence(blockIdx) ||
          state_->getDomain()->getBlockSize(blockIdx) == 1)
        return NOVALUE;
      else
      {
          //Dealing with atom in a block
        int blockSize = state_->getDomain()->getBlockSize(blockIdx);
          // 0->1: choose atom in block which is already 1
        if (state_->getValueOfAtom(atomIdx) == 0)
        {
          for (int i = 0; i < blockSize; i++)
          {
            const Predicate* pred =
              state_->getDomain()->getPredInBlock(i, blockIdx);
            GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);

            int idx = state_->getIndexOfGroundPredicate(gndPred);

            delete gndPred;
            delete pred;

              // Pred is in the state
            if (idx >= 0)
            {
              if (state_->getValueOfAtom(idx + 1) == 1)
              {
                inBlock_ = blockIdx;
                flipInBlock_ = idx + 1;
                return atomIdx;
              }
            }
          }
        }
          // 1->0: choose to flip the other randomly
        else
        {
          bool ok = false;
          while (!ok)
          {
            const Predicate* pred =
              state_->getDomain()->getRandomPredInBlock(blockIdx);
            GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);

            int idx = state_->getIndexOfGroundPredicate(gndPred);
            
            delete gndPred;
            delete pred;

            if (idx + 1 != atomIdx)
            {
              inBlock_ = blockIdx;
              flipInBlock_ = idx + 1;
              return atomIdx;
            }
          }
        }
      }
    }
    //if (mwsdebug) cout << "Leaving MaxWalkSat::pickRandom" << endl;
    return atomIdx;
  }

int MaxWalkSat::pickBest

(

)

[inline, protected]

Pick the best atom (clauses made satisfied - clauses made unsatisfied) in a random unsatisfied clause.

Returns:

Index of atom picked.

Definition at line 470 of file maxwalksat.h.

References VariableState::activateAtom(), Array< Type >::append(), calculateImprovement(), Array< Type >::clear(), Array< Type >::find(), VariableState::getAtomInClause(), VariableState::getClauseCost(), VariableState::getClauseSize(), VariableState::getRandomFalseClauseIndex(), Array< Type >::growToSize(), VariableState::isFixedAtom(), pickRandom(), and Inference::state_.

Referenced by MaxWalkSat().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::pickBest" << endl;
      // With prob. do a noisy pick
    bool noisyPick = (numerator_ > 0 && random()%denominator_ < numerator_); 
    if (noisyPick)
      return pickRandom();

    assert(inBlock_ == -1);
      // Clause to fix picked at random    
    int toFix = state_->getRandomFalseClauseIndex();
    if (toFix == NOVALUE) return NOVALUE;

    if (mwsdebug) cout << "Looking to fix clause " << toFix << endl;

    int clauseSize = state_->getClauseSize(toFix);
    long double cost = state_->getClauseCost(toFix);

    long double improvement;
      // Arrays to hold information on candidate flips
    Array<Array<int> > canNotFlip;
      // If var in candidateBlockedVars is chosen, then
      // corresponding var in othersToFlip is flipped as well
    Array<Array<int> > candidateBlockedVars;
    Array<Array<int> > othersToFlip;
    Array<int> blockIdx;

    canNotFlip.growToSize(clauseSize);
    candidateBlockedVars.growToSize(clauseSize);
    othersToFlip.growToSize(clauseSize);
    blockIdx.growToSize(clauseSize);

      // Holds the best atoms so far
    Array<int> best;
      // How many are tied for best
    register int numbest = 0;
      // Best value so far
    long double bestvalue = -LDBL_MAX;

      // Look at each atom and pick best ones
    for (int i = 0; i < clauseSize; i++)
    {
      register int lit = state_->getAtomInClause(i, toFix);
        // Neg. clause: Only look at true literals
      if (cost < 0 && !state_->isTrueLiteral(lit)) continue;
        // var is the index of the atom
      register int var = abs(lit);

      if (state_->isFixedAtom(var)) continue;
      bool ignoreActivePreds = false;
      bool groundOnly = false;
          if (!state_->activateAtom(var, ignoreActivePreds, groundOnly))
        return NOVALUE;

      improvement = calculateImprovement(var, canNotFlip[i],
                                         candidateBlockedVars[i],
                                         othersToFlip[i], blockIdx[i]);
      if (mwsdebug)
        cout << "Improvement of var " << var << " is: " << improvement << endl;

      if (improvement > -LDBL_MAX && improvement >= bestvalue)
      { // Tied or better than previous best
        if (improvement > bestvalue)
        {
          numbest = 0;
          best.clear();
        }
        bestvalue = improvement;
        best.append(i);
        numbest++;
      }
    }

      // If only false literals in a neg. clause, then numbest is 0
    if (numbest == 0) return NOVALUE;
      // Choose one of the best at random
      // (default if none of the following 2 cases occur)
    int toFlip = best[random()%numbest];

      // Exactly one best atom
    if (numbest == 1)
      toFlip = best[0];
    int toFlipAtom = abs(state_->getAtomInClause(toFlip, toFix));

    if (blockIdx[toFlip] > -1)
    {
        // If atom can not be flipped, then null flip
      if (canNotFlip[toFlip].contains(toFlipAtom))
        toFlipAtom = NOVALUE;
      else
      { // If toFlip is in block, then set other to flip
        int idx = candidateBlockedVars[toFlip].find(toFlipAtom);
        if (idx >= 0)
        {
          inBlock_ = blockIdx[toFlip];
          flipInBlock_ = othersToFlip[toFlip][idx];
        }
      }
    }
    
    //if (mwsdebug) cout << "Leaving MaxWalkSat::pickBest" << endl;
    return toFlipAtom;
  }

int MaxWalkSat::pickTabu

(

)

[inline, protected]

Pick an atom from a random unsatisfied clause based on the tabu heuristic.

Returns:

Index of atom picked.

Definition at line 579 of file maxwalksat.h.

References VariableState::activateAtom(), Array< Type >::append(), calculateImprovement(), SAT::changed_, Array< Type >::clear(), Array< Type >::find(), VariableState::getAtomInClause(), VariableState::getClauseCost(), VariableState::getClauseSize(), VariableState::getRandomFalseClauseIndex(), Array< Type >::growToSize(), VariableState::isFixedAtom(), SAT::numFlips_, and Inference::state_.

Referenced by MaxWalkSat(), and pickSS().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::pickTabu" << endl;
    assert(inBlock_ == -1);
      // Clause to fix picked at random    
    int toFix = state_->getRandomFalseClauseIndex();
    if (toFix == NOVALUE)
    {
      //if (mwsdebug) cout << "Leaving MaxWalkSat::pickTabu (NOVALUE)" << endl;      
      return NOVALUE;
    }
    if (mwsdebug) cout << "Looking to fix clause " << toFix << endl;

    int clauseSize = state_->getClauseSize(toFix);
    long double cost = state_->getClauseCost(toFix);

    long double improvement;
      // Arrays to hold information on candidate flips
    Array<Array<int> > canNotFlip;
      // If var in candidateBlockedVars is chosen, then
      // corresponding var in othersToFlip is flipped as well
    Array<Array<int> > candidateBlockedVars;
    Array<Array<int> > othersToFlip;
    Array<int> blockIdx;

    canNotFlip.growToSize(clauseSize);
    candidateBlockedVars.growToSize(clauseSize);
    othersToFlip.growToSize(clauseSize);
    blockIdx.growToSize(clauseSize);

      // Holds the best atoms so far
    Array<int> best;
      // How many are tied for best
    register int numbest = 0;
      // Best value so far
    long double bestvalue = -LDBL_MAX;

      // With prob. do a noisy pick
    bool noisyPick = (numerator_ > 0 && random()%denominator_ < numerator_); 

      // if random move, exclude illegitimate ones and place others in a lottery
    if (noisyPick)
    {
      for (int i = 0; i < clauseSize; i++)
      {       
        register int lit = state_->getAtomInClause(i, toFix);
          // Neg. clause: Only look at true literals
        if (cost < 0 && !state_->isTrueLiteral(lit)) continue;
          // var is the index of the atom
        register int var = abs(lit);

        if (state_->isFixedAtom(var)) continue;
        bool ignoreActivePreds = false;
        bool groundOnly = false;
        if (!state_->activateAtom(var, ignoreActivePreds, groundOnly))
          return NOVALUE;

          // We don't need improvement, but this function fills the block arrays
        calculateImprovement(var, canNotFlip[i],
                             candidateBlockedVars[i],
                             othersToFlip[i], blockIdx[i]);

        best.append(i);
        numbest++;
      }
    }
      // greedy: pick the best value
    else for (int i = 0; i < clauseSize; i++)
    {
      register int lit = state_->getAtomInClause(i, toFix);
        // Neg. clause: Only look at true literals
      if (cost < 0 && !state_->isTrueLiteral(lit)) continue;
        // var is the index of the atom
      register int var = abs(lit);
      
      if (state_->isFixedAtom(var)) continue;
      bool ignoreActivePreds = false;
      bool groundOnly = false;
      if (!state_->activateAtom(var, ignoreActivePreds, groundOnly))
        return NOVALUE;

      improvement = calculateImprovement(var, canNotFlip[i],
                                         candidateBlockedVars[i],
                                         othersToFlip[i], blockIdx[i]);
      if (mwsdebug)
        cout << "Improvement of var " << var << " is: " << improvement << endl;

        // TABU: If pos. improvement, then always add it to best
      if (improvement > 0 && improvement >= bestvalue)
      { // Tied or better than previous best
        if (improvement > bestvalue)
        {
          numbest = 0;
          best.clear();
        }
        bestvalue = improvement;
        best.append(i);
        numbest++;
      }
      else if (improvement > -LDBL_MAX && 
               tabuLength_ < numFlips_ - changed_[var])
      {
        if (improvement >= bestvalue)
        { // Tied or better than previous best
          if (improvement > bestvalue)
          {
            numbest = 0;
            best.clear();
          }
          bestvalue = improvement;
          best.append(i);
          numbest++;
        }
      }
    }

    if (numbest == 0) 
    {
      //if (mwsdebug) cout << "Leaving MaxWalkSat::pickTabu (NOVALUE)" << endl;
      return NOVALUE;
    }

    int toFlip = NOVALUE;
      // Exactly one best atom
    if (numbest == 1)
      toFlip = best[0];
    else
      // Choose one of the best at random
      toFlip = best[random()%numbest];
    int toFlipAtom = abs(state_->getAtomInClause(toFlip, toFix));

    if (blockIdx[toFlip] > -1)
    {
        // If atom can not be flipped, then null flip
      if (canNotFlip[toFlip].contains(toFlipAtom))
        toFlipAtom = NOVALUE;
      else
      { // If toFlip is in block, then set other to flip
        int idx = candidateBlockedVars[toFlip].find(toFlipAtom);
        if (idx >= 0)
        {
          inBlock_ = blockIdx[toFlip];
          flipInBlock_ = othersToFlip[toFlip][idx];
        }
      }
    }

    //if (mwsdebug) cout << "Leaving MaxWalkSat::pickTabu" << endl;
    return toFlipAtom;
  }

int MaxWalkSat::pickSS

(

)

[inline, protected]

Pick an atom according to the SampleSat heuristic.

This means sometimes sim. annealing, sometimes MaxWalkSat.

Returns:

Index of atom picked.

Definition at line 736 of file maxwalksat.h.

References VariableState::activateAtom(), calculateImprovement(), Array< Type >::contains(), Array< Type >::find(), VariableState::getCostOfFalseClauses(), VariableState::getIndexOfRandomAtom(), VariableState::isFixedAtom(), pickTabu(), VariableState::setActive(), Inference::state_, and SAT::targetCost_.

Referenced by MaxWalkSat().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::pickSS" << endl;
    assert(inBlock_ == -1);
    Array<int> canNotFlip;
      // If var in candidateBlockedVars is chosen, then
      // corresponding var in othersToFlip is flipped as well
    Array<int> candidateBlockedVars;
    Array<int> othersToFlip;
    int blockIdx;
    
    long double costOfFalseClauses = state_->getCostOfFalseClauses();

      // If we have already reached a solution or if in an SA step,
      // then perform SA
      // Add 0.0001 to targetCost_ because of double precision error
      // This needs to be fixed
    if (costOfFalseClauses <= targetCost_ + 0.0001 ||
        (!lateSa_ && random() % 100 < saRatio_ ))
    {
        // Choose a random atom to flip
      int toFlip = state_->getIndexOfRandomAtom();
      if (toFlip == NOVALUE) return NOVALUE;

      if (state_->isFixedAtom(toFlip)) return NOVALUE;
      bool ignoreActivePreds = false;
        // SA step: we don't want to activate
      bool groundOnly = true;
          if (!state_->activateAtom(toFlip, ignoreActivePreds, groundOnly))
        return NOVALUE;
      long double improvement = calculateImprovement(toFlip, canNotFlip,
                                                     candidateBlockedVars,
                                                     othersToFlip, blockIdx);
      if (mwsdebug) cout << "Total improvement: " << improvement << endl;

        // If pos. or no improvement, then the atom will be flipped
        // Or neg. improvement: According to temp. flip atom anyway
      if (improvement > -LDBL_MAX && 
          ((improvement >= 0) ||
          (random() <= exp(improvement/(saTemp_/100.0)) * RAND_MAX)))
      {
          // If atom can not be flipped, then null flip
        if (canNotFlip.contains(toFlip)) toFlip = NOVALUE;
        else
        { // If toflip is in block, then set other to flip
          int idx = candidateBlockedVars.find(toFlip);
          if (idx >= 0)
          {
            inBlock_ = blockIdx;
            flipInBlock_ = othersToFlip[idx];
          }
        }
        
          // SA
        if (toFlip != NOVALUE)
        {
          state_->setActive(toFlip);
        }
        return toFlip;
      }
      else
      {
        return NOVALUE;
      }
    }
      // Not in a solution or SA step: perform normal MWS step
    else
    {
      return pickTabu();
    }
  }

long double MaxWalkSat::calculateImprovement	(	const int &	atomIdx,
		Array< int > &	canNotFlip,
		Array< int > &	candidateBlockedVars,
		Array< int > &	othersToFlip,
		int &	blockIdx
	)			[inline, protected]

Calculates the improvement (makecost - breakcost) by flipping an atom.

If the atom is in a block, then its index is saved in candidateBlockedVars and the index of another atom chosen to be flipped in the block is appended to othersToFlip. If the atom is in a block with evidence, then its index is appended to canNotFlip.

Parameters:

	atomIdx	Index of atom for which the improvement is calculated.
	canNotFlip	Holds indices of atoms which can not be flipped due to evidence in a block.
	candidateBlockedVars	If dealing with an atom in a block, then its index is appended here.
	othersToFlip	If dealing with an atom in a block, then the index of the other atom chosen to be flipped is appended here.
	blockIdx	Index of block if atom with atomIdx is in a block. Otherwise, -1.

Definition at line 826 of file maxwalksat.h.

References Array< Type >::append(), Domain::getBlockEvidence(), VariableState::getBlockIndex(), Domain::getBlockSize(), VariableState::getDomain(), VariableState::getImprovementByFlipping(), VariableState::getIndexOfGroundPredicate(), Domain::getPredInBlock(), Domain::getRandomPredInBlock(), VariableState::getValueOfAtom(), and Inference::state_.

Referenced by pickBest(), pickSS(), and pickTabu().

  {
    blockIdx = state_->getBlockIndex(atomIdx - 1);
    if (blockIdx == -1)
    {
        // Atom not in a block
      return state_->getImprovementByFlipping(atomIdx);
    }
    else
    {
        // Atom is in a block
        // If evidence atom exists or in block of size 1, then can not flip
      if (state_->getDomain()->getBlockEvidence(blockIdx) ||
          state_->getDomain()->getBlockSize(blockIdx) == 1)
      {
        canNotFlip.append(atomIdx);
        return -LDBL_MAX;
      }
      else
      {
          // Dealing with atom in a block
        int blockSize = state_->getDomain()->getBlockSize(blockIdx);
        int chosen = -1;
        int otherToFlip = -1;

          // 0->1: choose atom in block which is already 1
        if (state_->getValueOfAtom(atomIdx) == 0)
        {
          for (int i = 0; i < blockSize; i++)
          {
            const Predicate* pred =
              state_->getDomain()->getPredInBlock(i, blockIdx);
            GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);

            int idx = state_->getIndexOfGroundPredicate(gndPred);

            delete gndPred;
            delete pred;

              // Pred is in the state
            if (idx >= 0)
            {
              if (state_->getValueOfAtom(idx + 1) == 1)
              {
                chosen = idx + 1;
                break;
              }
            }
          }
        }
          // 1->0: choose to flip the other randomly
          // TODO: choose to flip the other with best improvement
        else
        {
          bool ok = false;
          while (!ok)
          {
            const Predicate* pred =
              state_->getDomain()->getRandomPredInBlock(blockIdx);
            GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);

            int idx = state_->getIndexOfGroundPredicate(gndPred);
            if (idx == -1)
            {
              delete gndPred;
              delete pred;
              continue;
              // TODO: Other atom not yet in state (lazy) - must activate it              
            }
            chosen = idx + 1;
            
            delete gndPred;
            delete pred;

            if (chosen != atomIdx)
              ok = true;
          }
        }

        assert(chosen >= 0);
        candidateBlockedVars.append(atomIdx);
        otherToFlip = chosen;
        othersToFlip.append(otherToFlip);
        return (state_->getImprovementByFlipping(atomIdx) +
                state_->getImprovementByFlipping(otherToFlip));
      }
    }
  }

---

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

• src/infer/maxwalksat.h

---