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)
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)
	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 95 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 151 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 286 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);
      // Mark this flip as last time atom was changed if tabu is used
    if (heuristic_ == TABU || heuristic_ == SS)
    {
      changed_[toFlip] = numFlips_;
      changed_.growToSize(state_->getNumAtoms(), -(tabuLength_ + 1));
    }
    
    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 335 of file maxwalksat.h.

References VariableState::getBlockArray(), VariableState::getBlockIndex(), VariableState::getBlockSize(), VariableState::getIndexOfAtomInRandomFalseClause(), VariableState::getValueOfAtom(), VariableState::isBlockEvidence(), Array< Type >::size(), and Inference::state_.

Referenced by MaxWalkSat().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::pickRandom" << endl;
    assert(!inBlock_);
    int atomIdx = state_->getIndexOfAtomInRandomFalseClause();
    assert(atomIdx > 0);

      // 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_->isBlockEvidence(blockIdx) ||
          state_->getBlockSize(blockIdx) == 1)
        return NOVALUE;
      else
      {
          //Dealing with atom in a block
        Array<int>& block = state_->getBlockArray(blockIdx);
          // 0->1: choose atom in block which is already 1
        if (state_->getValueOfAtom(atomIdx) == 0)
        {
          for (int i = 0; i < block.size(); i++)
          {
            if (state_->getValueOfAtom(block[i] + 1) == 1)
            {
              inBlock_ = true;
              flipInBlock_ = block[i] + 1;
              return atomIdx;
            }
          }
        }
          // 1->0: choose to flip the other randomly
          // TODO: choose to flip the other with best improvement
        else
        {
          bool ok = false;
          while (!ok)
          {
            int chosen = random() % block.size();
            if (block[chosen] + 1 != atomIdx)
            {
              inBlock_ = true;
              flipInBlock_ = block[chosen] + 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 396 of file maxwalksat.h.

References Array< Type >::append(), calculateImprovement(), Array< Type >::clear(), Array< Type >::contains(), Array< Type >::find(), VariableState::getAtomInClause(), VariableState::getClauseCost(), VariableState::getClauseSize(), VariableState::getRandomAtomInClause(), VariableState::getRandomFalseClauseIndex(), VariableState::getRandomTrueLitInClause(), and Inference::state_.

Referenced by MaxWalkSat().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::pickBest" << endl;
    assert(!inBlock_);
      // Clause to fix picked at random    
    int toFix = state_->getRandomFalseClauseIndex();
    if (toFix == NOVALUE) return NOVALUE;

    long double improvement;

    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 clauseSize = state_->getClauseSize(toFix);
    long double cost = state_->getClauseCost(toFix);
      // 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_); 

      // 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);

      improvement = calculateImprovement(var, canNotFlip,
                                         candidateBlockedVars,
                                         othersToFlip);

      if (improvement >= bestvalue)
      { // Tied or better than previous best
        if (improvement > bestvalue)
        {
          numbest = 0;
          best.clear();
        }
        bestvalue = improvement;
        best.append(var);
        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];

      // 1. If no improvement by best,
      // then with prob. choose a random atom
    if (bestvalue <= 0 && noisyPick)
    {
      if (cost > 0)
        toFlip = abs(state_->getRandomAtomInClause(toFix));
      else
        toFlip = state_->getRandomTrueLitInClause(toFix);
    }
      // 2. Exactly one best atom
    else if (numbest == 1)
      toFlip = best[0];

      // 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_ = true;
        flipInBlock_ = othersToFlip[idx];
      }
    }

    //if (mwsdebug) cout << "Leaving MaxWalkSat::pickBest" << endl;
    return toFlip;
  }

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 489 of file maxwalksat.h.

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

Referenced by MaxWalkSat(), and pickSS().

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

    long double improvement;
    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 clauseSize = state_->getClauseSize(toFix);
    long double cost = state_->getClauseCost(toFix);

      // 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_); 

    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);

      improvement = calculateImprovement(var, canNotFlip, candidateBlockedVars,
                                         othersToFlip);

        // 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(var);
        numbest++;
      }
      else if (tabuLength_ < numFlips_ - changed_[var])
      {
        if (noisyPick && bestvalue <= 0)
        { 
          best.append(var);
          numbest++;
        }
        else if (improvement >= bestvalue)
        { // Tied or better than previous best
          if (improvement > bestvalue)
          {
            numbest = 0;
            best.clear();
          }
          bestvalue = improvement;
          best.append(var);
          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];


      // 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_ = true;
        flipInBlock_ = othersToFlip[idx];
      }
    }

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

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 602 of file maxwalksat.h.

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

Referenced by MaxWalkSat().

  {
    //if (mwsdebug) cout << "Entering MaxWalkSat::pickSS" << endl;
    assert(!inBlock_);
    Array<int> canNotFlip;
      // If var in candidateBlockedVars is chosen, then
      // corresponding var in othersToFlip is flipped as well
    Array<int> candidateBlockedVars;
    Array<int> othersToFlip;
    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 ||
        (random() % 100 < saRatio_ && !lateSa_))
    {
        // Choose a random atom to flip
      int toFlip = state_->getIndexOfRandomAtom();
      if (toFlip == NOVALUE) return NOVALUE;
      long double improvement = calculateImprovement(toFlip, canNotFlip,
                                                     candidateBlockedVars,
                                                     othersToFlip);

        // If pos. or no improvement, then the atom will be flipped
        // Or neg. improvement: According to temp. flip atom anyway
      if ((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_ = true;
            flipInBlock_ = othersToFlip[idx];
          }
        }
        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
	)			[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.

Definition at line 673 of file maxwalksat.h.

References Array< Type >::append(), VariableState::getBlockArray(), VariableState::getBlockIndex(), VariableState::getBlockSize(), VariableState::getImprovementByFlipping(), VariableState::getValueOfAtom(), VariableState::isBlockEvidence(), Array< Type >::size(), and Inference::state_.

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

  {
    int 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_->isBlockEvidence(blockIdx) ||
          state_->getBlockSize(blockIdx) == 1)
      {
        canNotFlip.append(atomIdx);
        return -LDBL_MAX;
      }
      else
      {
          //Dealing with atom in a block
        Array<int>& block = state_->getBlockArray(blockIdx);
        int chosen = -1;
        int otherToFlip = -1;

          // 0->1: choose atom in block which is already 1
        if (state_->getValueOfAtom(atomIdx) == 0)
        {
          if (mwsdebug)
          {
            cout << "0->1 atom " << atomIdx << endl;
            for (int i = 0; i < block.size(); i++)
            {
              cout << "Atom in block " << block[i] + 1 << " ";
              cout << state_->getValueOfAtom(block[i] + 1) << endl;
            }
          }
          
          for (int i = 0; i < block.size(); i++)
          {
            if (state_->getValueOfAtom(block[i] + 1) == 1)
            {
              chosen = i;
              break;
            }
          }
        }
          // 1->0: choose to flip the other randomly
          // TODO: choose to flip the other with best improvement
        else
        {
          if (mwsdebug)
          {
            cout << "1->0 atom " << atomIdx << endl;
            for (int i = 0; i < block.size(); i++)
            {
              cout << "Atom in block " << block[i] + 1 << " ";
              cout << state_->getValueOfAtom(block[i] + 1) << endl;
            }
          }
          bool ok = false;
          while (!ok)
          {
            chosen = random() % block.size();
            if (block[chosen] + 1 != atomIdx)
              ok = true;
          }
        }
    
        assert(chosen >= 0);
        candidateBlockedVars.append(atomIdx);
        otherToFlip = block[chosen] + 1;
        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

---