HMaxWalkSat Class Reference

The HMaxWalkSat algorithm. More...

#include <hmaxwalksat.h>

Inheritance diagram for HMaxWalkSat:

SAT Inference List of all members.

Public Member Functions

 HMaxWalkSat (HVariableState *state, int seed, const bool &trackClauseTrueCnts, MaxWalksatParams *params)
 Constructor: user-set parameters are set.
 ~HMaxWalkSat ()
 Destructor (destructors from superclasses are called).
void SetMaxSeconds (double maxSeconds)
void SetNoisePra (int numerator, int denominator)
void SetSAInterval (int saInterval)
void init ()
 Initializes the HMaxWalkSat algorithm.
double getTargetCost ()
void setSATempDownRatio (double saTempDownRatio)
void infer ()
 Performs the given number of HMaxWalkSat inference tries.
const int getHeuristic ()
void setHeuristic (const int &heuristic)
virtual const Array< double > * getClauseTrueCnts ()
virtual const Array< double > * getClauseTrueCntsCont ()
double collapseDepthConstraint (double th)

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 pickHMCS ()
 Pick the atom idx according to hybrid WalkSAT strategy.
void checkAr (const Array< int > &ar)
int pickHMWS ()
int pickSA ()
int pickSS ()
 Pick an atom according to the SampleSat heuristic.
long double calculateImprovementDisHMCS (const int &atomIdx)
 Calculates the improvement (makecost - breakcost) by flipping an atom.
long double calculateImprovementDisHMWS (int atomIdx)
void reconstructLowState ()
 Reconstructs the state with the lowest cost by flipping atoms back to their value in this state.

Classes

struct  FlipDisVarIdxCont

Detailed Description

The HMaxWalkSat algorithm.

This code is based on the HMaxWalkSat 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 97 of file hmaxwalksat.h.

Member Function Documentation

void HMaxWalkSat::init (  )  [inline, virtual]

Initializes the HMaxWalkSat algorithm.

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

Implements Inference.

Definition at line 175 of file hmaxwalksat.h.

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

Referenced by infer(), and HMCSAT::init().

00176         {
00177                 if (heuristic_ == TABU || heuristic_ == SS || heuristic_ == HMWS)
00178                 {
00179                         int numAtoms = hstate_->getNumAtoms();
00180                         if (changed_.size() != numAtoms + 1)
00181                         {
00182                                 if (int(changed_.size()) < numAtoms + 1) {
00183                                         changed_.growToSize(numAtoms + 1);
00184                                 } else {
00185                                         changed_.shrinkToSize(numAtoms + 1);
00186                                 }
00187                         }
00188                         for(int i = 1; i <= numAtoms; ++i)
00189                                 changed_[i] = -(tabuLength_ + 1);
00190                 }
00191 
00192                 // Random initialize the variables 
00193                 hstate_->initRandom();          
00194                 //reinitialize the SATemp here
00195                 saTemp_ = saTempInit_;
00196         }

void HMaxWalkSat::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 503 of file hmaxwalksat.h.

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

Referenced by infer(), and pickHMCS().

00504         {
00505                 //if (hmwsdebug) cout << "Entering HMaxWalkSat::flipAtom" << endl;
00506                 if (toFlip == NOVALUE)
00507                         return;
00508 
00509                 // Flip the atom in the state
00510                 hstate_->flipAtom(toFlip, -1);
00511                 // Mark this flip as last time atom was changed if tabu is used
00512                 if (heuristic_ == TABU || heuristic_ == SS || heuristic_ == HMWS)
00513                 {
00514                         changed_[toFlip] = numFlips_;
00515                         changed_.growToSize(hstate_->getNumAtoms() + 1, -(tabuLength_ + 1));
00516                 }
00517 
00518                 if (lazyLowState_)
00519                 {
00520                         // Mark this variable as flipped since last low state. If already
00521                         // present, then it has been flipped back to its value in the low
00522                         // state and we can remove it.
00523                         if (varsFlippedSinceLowState_.find(toFlip) !=
00524                                 varsFlippedSinceLowState_.end())
00525                         {
00526                                 varsFlippedSinceLowState_.erase(toFlip);
00527                         }
00528                         else
00529                         {
00530                                 varsFlippedSinceLowState_.insert(toFlip);
00531                         }
00532                 }
00533       if (hmwsdebug) cout << "Leaving HMaxWalkSat::flipAtom" << endl;
00534         }

int HMaxWalkSat::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 542 of file hmaxwalksat.h.

Referenced by HMaxWalkSat().

00543         {
00544                 return 0;
00545         }

int HMaxWalkSat::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 553 of file hmaxwalksat.h.

Referenced by HMaxWalkSat().

00554         {
00555                 return 0;
00556         }

int HMaxWalkSat::pickHMCS (  )  [inline, protected]

Pick the atom idx according to hybrid WalkSAT strategy.

Returns:
Index of atom picked.

Definition at line 563 of file hmaxwalksat.h.

References Array< Type >::append(), HVariableState::atom_, calculateImprovementDisHMCS(), SAT::changed_, HVariableState::clauseCost_, Array< Type >::clear(), flipAtom(), HVariableState::getAtomInClause(), HVariableState::getClauseCost(), HVariableState::getClauseSize(), HVariableState::GetImprovementBySolvingHybridConstraintToContVar(), HVariableState::getRandomFalseClauseIndexHMCS(), HVariableState::getValueOfAtom(), Inference::hstate_, HVariableState::HybridClauseContPartValue(), HVariableState::HybridClauseValue(), HVariableState::hybridConjunctionDisjunction_, HVariableState::hybridConstraints_, HVariableState::hybridContClause_, HVariableState::hybridDisClause_, HVariableState::hybridWts_, HVariableState::isSatisfied(), SAT::numFlips_, HVariableState::printDisClause(), HVariableState::printHybridConstraint(), Array< Type >::size(), HVariableState::SolveConstraintAndRandomSample(), HVariableState::SolveHybridConstraintToContVarSample(), HVariableState::UpdateHybridClauseInfoByContAtom(), and HVariableState::UpdateHybridClauseInfoByDisAtom().

Referenced by HMaxWalkSat(), and pickSS().

00564         {
00565                 if (wjhmwsdebug)
00566                 {
00567                         cout << "HMCS" << endl;
00568                 }
00569 
00570                 assert(!inBlock_);
00571                 // Clause to fix picked at random
00572                 // need to be changed to deal with hybrid case
00573                 bool noisyPick = (numerator_ > 0 && random() % denominator_ < numerator_); 
00574                 // Pick a clause.
00575                 // For H-MCSAT, the picked clause is either a false discrete clause, or a hybrid one not satisfying the inequality constraint.
00576                 // For HMWS, the picked clause is either a false discrete clause or a hybrid one.
00577                 int toFix = hstate_->getRandomFalseClauseIndexHMCS();  // HMCS version.
00578                 if (toFix ==     NOVALUE) // No false clause.
00579                 {
00580                         return NOVALUE;
00581                 }
00582                 else if (toFix > 0) //discrete clause, clause idx = toFix - 1;
00583                 {
00584                         toFix --;
00585                         if (wjhmwsdebug)
00586                         {
00587                                 cout << "Pick false dis clause: " << toFix << ", "; hstate_->printDisClause(toFix, cout); cout << "Cost: " << hstate_->clauseCost_[toFix] << endl;
00588                         }
00589                         long double improvement;
00590                         int clauseSize = hstate_->getClauseSize(toFix);
00591                         long double cost = hstate_->getClauseCost(toFix);
00592                         // Holds the best atoms so far
00593                         Array<int> best;
00594                         // How many are tied for best
00595                         register int numbest = 0;
00596                         // Best value so far
00597                         long double bestvalue = -LDBL_MAX;
00598                         // With prob. do a noisy pick, prob = denominator / numerator.
00599                         // if random move, exclude illegitimate ones and place others in a lottery
00600                         if (noisyPick)
00601                         {
00602                                 for (int i = 0; i < clauseSize; ++i)
00603                                 {       
00604                                         register int lit = hstate_->getAtomInClause(i, toFix);
00605                                         // Neg. clause: Only look at true literals
00606                                         if (cost < 0 && !hstate_->isTrueLiteral(lit)) continue;
00607                                         best.append(abs(lit));
00608                                         numbest++;
00609                                 }
00610                         }  // Noisy pick ends.
00611                         else  // Greedy: pick the best value
00612                         {
00613                                 for (int i = 0; i < clauseSize; ++i)
00614                                 {
00615                                         register int lit = hstate_->getAtomInClause(i, toFix);
00616                                         // Neg. clause: Only look at true literals
00617                                         if (cost < 0 && !hstate_->isTrueLiteral(lit)) continue;
00618                                         // var is the index of the atom
00619                                         register int var = abs(lit);
00620                                         improvement = calculateImprovementDisHMCS(var);
00621                                         if (mwsdebug) {
00622                                                 cout << "Improvement of var " << var << " is: " << improvement << endl;
00623                                         }
00624 
00625                                         // TABU: If pos. improvement, then always add it to best
00626                                         if (improvement > 0 && improvement >= bestvalue)
00627                                         { // Tied or better than previous best
00628                                                 if (improvement > bestvalue)
00629                                                 {
00630                                                         numbest = 0;
00631                                                         best.clear();
00632                                                 }
00633                                                 bestvalue = improvement;
00634                                                 best.append(var);
00635                                                 numbest++;
00636                                         } else if (improvement > -LDBL_MAX && tabuLength_ < numFlips_ - changed_[var]) {
00637                                                 if (improvement >= bestvalue)
00638                                                 { // Tied or better than previous best
00639                                                         if (improvement > bestvalue)
00640                                                         {
00641                                                                 numbest = 0;
00642                                                                 best.clear();
00643                                                         }
00644                                                         bestvalue = improvement;
00645                                                         best.append(var);
00646                                                         numbest++;
00647                                                 }
00648                                         }
00649                                 }
00650                         }
00651 
00652                         if (numbest == 0) 
00653                         {
00654                                 if (wjhmwsdebug) cout << "Leaving MaxWalkSat::pickHMCS (NOVALUE)" << endl;
00655                                 return NOVALUE;
00656                         }
00657                         int toFlip = NOVALUE;
00658                         // Exactly one best atom
00659                         if (numbest == 1) {
00660                                 toFlip = best[0];
00661                         } else {
00662                                 // Choose one of the best at random
00663                                 toFlip = best[random()% best.size()];
00664                         }
00665 
00666                         if (wjhmwsdebug) 
00667                         {
00668                                 cout << "Improvement:" << bestvalue << endl;
00669                         }
00670                         return toFlip;
00671                 }  // Discrete clause
00672                 else  // Hybrid clause, clause idx = - (toFix + 1); toFix < 0
00673                 {
00674                         toFix++;
00675                         int contClauseIdx = -toFix;
00676                         // If the weight of the hybrid constraint is 0, then we skip the current pick.
00677                         if (hstate_->hybridWts_[contClauseIdx] == 0) return NOVALUE;
00678 
00679                         if (wjhmwsdebug) {
00680                                 cout << "Pick false hybrid clause: " << contClauseIdx << ", constraint:"; hstate_->printHybridConstraint(contClauseIdx, cout);
00681                         }
00682                         int contVarNum = hstate_->hybridContClause_[contClauseIdx].size();
00683                         int disVarNum = hstate_->hybridDisClause_[contClauseIdx].size();
00684                         int totalVarNum = contVarNum + disVarNum;
00685                         if (noisyPick)  // Random pick and then flip, p = numerator_/denominator_;
00686                         {
00687                                 set<int> pickedContVars;
00688                                 int inIdx = random() % totalVarNum;
00689                                 if (inIdx < contVarNum)  // Continuous variable
00690                                 {
00691                                         int contAtomIdx = hstate_->hybridContClause_[contClauseIdx][inIdx];
00692                                         // Solve the constraint in regarding with the chosen continuous variable.
00693                                         // Then compute the improvement in term of #false clause reduction.
00694                                         pickedContValue_ = hstate_->SolveHybridConstraintToContVarSample(contClauseIdx, inIdx);
00695                                         if (pickedContValue_ == FLIPDIS) {
00696                                                 // Generate a random solution to the discrete part of the hybrid clause, so that making it true.
00697                                                 Array<bool> solution;
00698                                                 GetClauseRandomSolution(hstate_->hybridDisClause_[contClauseIdx].size(), true, hstate_->hybridConjunctionDisjunction_[contClauseIdx], &solution);
00699                                                 // Update each discrete variable.
00700                                                 for (int i = 0; i < solution.size(); ++i) {
00701                                                         int atomIdx = hstate_->hybridDisClause_[contClauseIdx][i];
00702                                                         if (solution[i] != hstate_->getValueOfAtom(atomIdx)) {
00703                                                                 flipAtom(atomIdx);
00704                                                                 bool atomValue = hstate_->getValueOfAtom(atomIdx);
00705                                                                 hstate_->UpdateHybridClauseInfoByDisAtom(atomIdx, atomValue);
00706                                                         }
00707                                                 }
00708                                                 // Then check if the continuous part's value satisfies the constraint or not.
00709                                                 double cont_part_value = hstate_->HybridClauseContPartValue(contClauseIdx);
00710                                                 if (cont_part_value < hstate_->hybridConstraints_[contClauseIdx].vThreshold_)                                           {
00711                                                         // If not, solve the continuous part for the given variable, set both solutions and update status.
00712                                                         double cont_var_value = hstate_->SolveConstraintAndRandomSample(contClauseIdx, inIdx);
00713                                                         if (cont_var_value == UNSOLVABLE)
00714                                                                 return NOVALUE;
00715                                                         else {
00716                                                                 // Update by the continuous variable.
00717                                                                 hstate_->UpdateHybridClauseInfoByContAtom(contAtomIdx, cont_var_value);
00718                                                         }
00719                                                 }
00720         
00721                                                 // Return the status that no action needs to be performed.
00722                                                 return NOVALUE;
00723                                         }  // FLIP_DIS ends
00724 
00725                                         return -contAtomIdx;
00726                                 }
00727                                 else  // discrete variable
00728                                 {
00729                                         // Check if flipping this discrete variable could satisfy this constraint.
00730                                         // If so, return it, if not, do nothing.
00731                                         int atomIdx = abs(hstate_->hybridDisClause_[contClauseIdx][inIdx - contVarNum]);
00732                                         hstate_->atom_[atomIdx] = !hstate_->atom_[atomIdx];
00733                                         double hybrid_clause_val = hstate_->HybridClauseValue(contClauseIdx);
00734                                         hstate_->atom_[atomIdx] = !hstate_->atom_[atomIdx];
00735                                         if (hstate_->isSatisfied(hstate_->hybridConstraints_[contClauseIdx], hybrid_clause_val)) {
00736                                                 return atomIdx;
00737                                         } else {
00738                                                 return NOVALUE;
00739                                         }
00740                                 }
00741                         }  // Noisy pick
00742                         else //greedy try to flip every variable and find the one get biggest improvement
00743                         {
00744                                 long double bestvalue = -LDBL_MAX;
00745                                 Array<int> best;
00746                                 int numbest = 0;
00747                                 map<int, double> pickedContValues;
00748                                 for (int i = 0; i < contVarNum; ++i) {
00749                                         int contAtomIdx = hstate_->hybridContClause_[contClauseIdx][i];
00750                                         // Solve the constraint in regarding with the chosen continuous variable.
00751                                         // Then compute the improvement in term of #false clause reduction.
00752                                         double cont_var_val = 0;
00753                                         double improvement =
00754                                                         hstate_->GetImprovementBySolvingHybridConstraintToContVar(contClauseIdx, i, cont_var_val);
00755                                         // Tied or better than previous best
00756                                         if (improvement != CANNOTSATCURRENT && improvement >= bestvalue) {
00757                                                 if (improvement > bestvalue) {
00758                                                         numbest = 0;
00759                                                         best.clear();
00760                                                 }
00761                                                 bestvalue = improvement;
00762                                                 best.append(-contAtomIdx);
00763                                                 numbest++;
00764                                                 pickedContValues[-contAtomIdx] = cont_var_val;
00765                                         }
00766                                 }
00767 
00768                                 for (int i = 0; i < disVarNum; ++i) {
00769                                         int disAtomIdx = hstate_->hybridDisClause_[contClauseIdx][i];
00770                                         double improvement = calculateImprovementDisHMCS(disAtomIdx);
00771 
00772                                         if (improvement >= bestvalue)
00773                                         { // Tied or better than previous best
00774                                                 if (improvement > bestvalue)
00775                                                 {
00776                                                         numbest = 0;
00777                                                         best.clear();
00778                                                 }
00779                                                 bestvalue = improvement;
00780                                                 best.append(disAtomIdx);
00781                                                 numbest++;
00782                                         }
00783                                 }
00784 
00785                                 int atomIdx = NOVALUE;
00786                                 // Exactly one best atom
00787                                 if (numbest == 1)
00788                                         atomIdx = best[0];
00789                                 else
00790                                         // Choose one of the best at random
00791                                         atomIdx = best[random()%numbest];
00792 
00793                                 if (atomIdx < 0)  // Picked variable is a continuous variable.
00794                                 {
00795                                         pickedContValue_ = pickedContValues[atomIdx];
00796                                 }
00797                                 return atomIdx;
00798                         }  // Greedy
00799                 }  // Hybrid clause.
00800                 return NOVALUE;
00801         }

int HMaxWalkSat::pickSS (  )  [inline, protected]

Pick an atom according to the SampleSat heuristic.

This means sometimes sim. annealing, sometimes HMaxWalkSat.

Returns:
Index of atom picked.

Definition at line 1116 of file hmaxwalksat.h.

References calculateImprovementDisHMCS(), HVariableState::getCostOfTotalFalseConstraints(), HVariableState::GetImprovementByMovingContVar(), HVariableState::getIndexOfRandomAtom(), Inference::hstate_, pickHMCS(), HVariableState::printContAtom(), HVariableState::printDisAtom(), and SAT::targetCost_.

Referenced by HMaxWalkSat().

01117         {
01118                 long double costOfFalseClauses = hstate_->getCostOfTotalFalseConstraints();
01119                 // If we have already reached a solution or if in an SA step,
01120                 // then perform SA
01121                 if (costOfFalseClauses <= targetCost_ + SMALLVALUE || (random() % 100 < saRatio_ && !lateSa_))
01122                 {
01123                         if (wjhmwsdebug)
01124                         {
01125                                 cout << "SASTEP" << endl;
01126                         }
01127                         // Choose a random atom to flip
01128                         int toFlip = hstate_->getIndexOfRandomAtom(); //change to hybrid, pos, discrete, neg, continuous
01129                         if (toFlip > 0)  // Discrete atom.
01130                         {
01131                                 if (wjhmwsdebug)
01132                                 {
01133                                         cout << "Choose to flip dis atom " << toFlip << ":";hstate_->printDisAtom(toFlip, cout);
01134                                 }
01135                                 long double improvement = calculateImprovementDisHMCS(toFlip); 
01136 
01137                                 if (wjhmwsdebug)
01138                                 {
01139                                         cout << "By flipping, improvement is " << improvement << endl;
01140                                 }
01141 
01142                                 // If pos. or no improvement, then the atom will be flipped
01143                                 // Or neg. improvement: According to temp. flip atom anyway
01144                                 if ((improvement >= 0) || (random() <= exp(improvement/(saTemp_/100.0)) * RAND_MAX))
01145                                 {
01146                                         return toFlip;
01147                                 }
01148                                 else
01149                                 {
01150                                         return NOVALUE;
01151                                 }
01152                         }
01153                         else  // Continuous variable.
01154                         {
01155                                 //generate the new value for the continuous variable according to the proposal distribution
01156                                 int contAtomIdx = -toFlip;
01157                                 double vContAtomFlipped;                                
01158                                 long double improvement = hstate_->GetImprovementByMovingContVar(contAtomIdx, vContAtomFlipped); 
01159                                 
01160                                 if (wjhmwsdebug)
01161                                 {
01162                                         cout << "Choose to move cont atom " << contAtomIdx << ":";hstate_->printContAtom(contAtomIdx, cout);
01163                                         cout << " To " << vContAtomFlipped << ", improvement is " << improvement << endl;
01164                                 }
01165 
01166                                 if ((improvement >= 0) ||
01167                                         (random() <= exp(improvement/(saTemp_/100.0)) * RAND_MAX))
01168                                 {       
01169                                         pickedContValue_ = vContAtomFlipped; //the value picked.
01170                                         return toFlip; //neg, indicate cont variable.
01171                                 }         
01172                                 else
01173                                 {
01174                                         return NOVALUE;
01175                                 }
01176                         }       
01177                 }
01178                 // Not in a solution or SA step: perform Hybrid WalkSAT step
01179                 else
01180                 {
01181                         return pickHMCS();  // TODO: juewang
01182                 }
01183         }

long double HMaxWalkSat::calculateImprovementDisHMCS ( const int &  atomIdx  )  [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 1200 of file hmaxwalksat.h.

References HVariableState::getImprovementByFlippingDisHMCS(), and Inference::hstate_.

Referenced by pickHMCS(), and pickSS().

01201         {
01202                 return hstate_->getImprovementByFlippingDisHMCS(atomIdx);
01203         }

The documentation for this class was generated from the following file:
Generated on Sun Jun 7 11:55:25 2009 for Alchemy by  doxygen 1.5.1