Alchemy: HVariableState Class Reference

All inference algorithms should have a HVariableState 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 HVariableState 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.

Constructor & Destructor Documentation

HVariableState::HVariableState	(	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 HVariableState.

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 141 of file hvariablestate.h.

References addNewClauses(), HashArray< Type, HashFn, EqualFn >::append(), bInitFromEvi_, bMaxOnly_, Array< Type >::clear(), Domain::computeNumNonEvidAtoms(), costHybridFalseConstraint_, costOfTotalFalseConstraints_, MRF::deleteGndPredsGndClauseSets(), getActiveClauses(), Domain::getDB(), MRF::getGndClauses(), MRF::getGndPreds(), getNumClauses(), Domain::getNumNonEvidenceAtoms(), gndClauses_, gndPredHashArray_, gndPreds_, hybridClauseNum_, hybridFalseConstraintNum_, hybridFormulaNum_, initBlocksRandom(), knePreds_, knePredValues_, lowBadAll_, lowBadHybrid_, lowCost_, lowCostAll_, lowCostHybrid_, newClauses_, Timer::printTime(), Database::setActiveStatus(), Database::setPerformingInference(), HashArray< Type, HashFn, EqualFn >::size(), Array< Type >::size(), Timer::time(), totalFalseConstraintNum_, unePreds_, weightSumCont_, and weightSumDis_.

00149         {
00150       stillActivating_ = true;
00151     Timer timer;
00152     double startTime = timer.time();
00153 
00154                 if (hvsdebug)
00155                 {
00156                         cout << "from hybrid vs" << endl;
00157                 }
00158                 this->mln_ = (MLN*)mln;
00159                 this->domain_ = (Domain*)domain;
00160                 this->lazy_ = lazy;
00161 
00162                 // Instantiate information
00163                 bInitFromEvi_ = false;
00164                 baseNumAtoms_ = 0;
00165                 activeAtoms_ = 0;
00166                 numFalseClauses_ = 0;
00167                 costOfFalseClauses_ = 0.0;
00168                 weightSumDis_ = 0.0;
00169                 weightSumCont_ = 0.0;
00170                 costOfTotalFalseConstraints_ = 0.0;
00171                 totalFalseConstraintNum_ = 0;
00172                 costHybridFalseConstraint_ = 0.0;
00173                 hybridFalseConstraintNum_ = 0;
00174                 lowCost_ = LDBL_MAX;
00175                 lowBad_ = INT_MAX;
00176                 lowCostAll_ = LDBL_MAX;
00177                 lowBadAll_ = INT_MAX;
00178                 lowCostHybrid_ = LDBL_MAX;
00179                 lowBadHybrid_ = INT_MAX;
00180 
00182                 //WJ
00184                 hybridClauseNum_ = 0;
00185                 hybridFormulaNum_ = 0;
00186 
00187                 // Clauses and preds are stored in gndClauses_ and gndPreds_
00188                 gndClauses_ = new Array<GroundClause*>;
00189                 gndPreds_ = new Array<GroundPredicate*>;
00190                 bMaxOnly_ = false;
00191 
00192                 // Set the hard clause weight
00193                 setHardClauseWeight();
00194 
00195                 // Lazy version: Produce state with initial active atoms and clauses
00196                 if (lazy_)
00197                 {
00198         // Set number of non-evidence atoms from domain
00199       domain_->computeNumNonEvidAtoms();
00200       numNonEvAtoms_ = domain_->getNumNonEvidenceAtoms();
00201                         // Unknown preds are treated as false
00202                         domain_->getDB()->setPerformingInference(true);
00203                         clauseLimit_ = INT_MAX;
00204                         noApprox_ = false;
00205                         haveDeactivated_ = false;
00206 
00208                         // Get initial set of active atoms (atoms in unsat. clauses)
00209                         // Assumption is: all atoms are initially false except those in blocks
00210                         // One atom in each block is set to true and activated
00211       initBlocksRandom();
00212 
00213       //bool ignoreActivePreds = false;
00214       bool ignoreActivePreds = true;
00215       cout << "Getting initial active atoms ... " << endl;
00216                         getActiveClauses(newClauses_, ignoreActivePreds);
00217       cout << "done." << endl;
00218                         int defaultCnt = newClauses_.size();
00219                         long double defaultCost = 0;
00220 
00221                         for (int i = 0; i < defaultCnt; i++)
00222                         {
00223                                 if (newClauses_[i]->isHardClause())
00224                                         defaultCost += hardWt_;
00225                                 else
00226                                         defaultCost += abs(newClauses_[i]->getWt());
00227                         }
00228 
00229                         // Clear ground clauses in the ground preds
00230                         for (int i = 0; i < gndPredHashArray_.size(); i++)
00231                                 gndPredHashArray_[i]->removeGndClauses();
00232 
00233                         // Delete new clauses
00234                         for (int i = 0; i < newClauses_.size(); i++)
00235                                 delete newClauses_[i];
00236                         newClauses_.clear();
00237 
00238                         baseNumAtoms_ = gndPredHashArray_.size();
00239       cout << "Number of Baseatoms = " << baseNumAtoms_ << endl;
00240                         cout << "Default => Cost\t" << "******\t" << " Clause Cnt\t" << endl;
00241                         cout << "           " << defaultCost << "\t" << "******\t" << defaultCnt
00242                                 << "\t" << endl << endl;
00243 
00244                         // Set base atoms as active in DB
00245                         for (int i = 0; i < baseNumAtoms_; i++)
00246                         {
00247                                 domain_->getDB()->setActiveStatus(gndPredHashArray_[i], true);
00248                                 activeAtoms_++;        
00249                         }
00250 
00251                         // Get the initial set of active clauses
00252                         ignoreActivePreds = false;
00253       cout << "Getting initial active clauses ... ";
00254                         getActiveClauses(newClauses_, ignoreActivePreds);      
00255       cout << "done." << endl;
00256                 } // End lazy version
00257                 // Eager version: Use KBMC to produce the state
00258                 else
00259                 {
00260                         unePreds_ = unknownQueries;
00261                         knePreds_ = knownQueries;
00262                         knePredValues_ = knownQueryValues;
00263                         // MRF is built on known and unknown queries
00264                         int size = 0;
00265                         if (unknownQueries) size += unknownQueries->size();
00266                         if (knownQueries) size += knownQueries->size();
00267                         GroundPredicateHashArray* queries = new GroundPredicateHashArray(size);
00268                         if (unknownQueries) queries->append(unknownQueries);
00269                         if (knownQueries) queries->append(knownQueries);
00270                         //markHardGndClauses = true;
00271                         mrf_ = new MRF(queries, allPredGndingsAreQueries, domain_,
00272                                 domain_->getDB(), mln_, true,
00273                                 trackParentClauseWts, -1);
00274                         //delete to save space. Can be deleted because no more gndClauses are
00275                         //appended to gndPreds beyond this point
00276 
00277                         mrf_->deleteGndPredsGndClauseSets();
00278 
00279                         //do not delete the intArrRep in gndPreds_;
00280                         delete queries;
00281 
00282                         // Put ground clauses in newClauses_
00283                         newClauses_ = *(Array<GroundClause*>*)mrf_->getGndClauses();
00284 
00285                         // Put ground preds in the hash array
00286                         //const Array<GroundPredicate*>* gndPreds = mrf_->getGndPreds();
00287                         const GroundPredicateHashArray* gndPreds = mrf_->getGndPreds();
00288                         for (int i = 0; i < gndPreds->size(); i++)
00289                                 gndPredHashArray_.append((*gndPreds)[i]);
00290 
00291                         // baseNumAtoms_ are all atoms in eager version
00292                         baseNumAtoms_ = gndPredHashArray_.size();        
00293                 } // End eager version
00294 
00295                 // At this point, ground clauses are held in newClauses_
00296                 // and ground predicates are held in gndPredHashArray_
00297                 // for both versions
00298 
00299                 // Add the clauses and preds and fill info arrays
00300                 bool initial = true;
00301                 addNewClauses(initial);         
00302     
00303         cout << "[VS] ";
00304         Timer::printTime(cout,timer.time()-startTime);
00305         cout << endl;
00306         cout << ">>> DONE: Initial num. of clauses: " << getNumClauses() << endl;
00307         }

HVariableState::~HVariableState ( ) [inline]

Destructor.

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

Definition at line 313 of file hvariablestate.h.

References contsolvers_, gndClauses_, gndPredHashArray_, Array< Type >::size(), and HashArray< Type, HashFn, EqualFn >::size().

00314         {
00315       if (lazy_)
00316       {
00317         if (gndClauses_)
00318           for (int i = 0; i < gndClauses_->size(); i++)
00319             delete (*gndClauses_)[i];
00320 
00321         for (int i = 0; i < gndPredHashArray_.size(); i++)
00322         {
00323           gndPredHashArray_[i]->removeGndClauses();
00324           delete gndPredHashArray_[i];
00325                 }
00326       }
00327       else
00328       {
00329                         // MRF from eager version is deleted
00330         if (mrf_)
00331         {
00332           delete mrf_;
00333           mrf_ = NULL;
00334         }
00335                         //if (unePreds_) delete unePreds_;
00336                         //if (knePreds_) delete knePreds_;
00337                         //if (knePredValues_) delete knePredValues_;
00338                         for (int i = 0; i < contsolvers_.size(); i++)
00339                         {
00340                                 delete contsolvers_[i];
00341                         }
00342                 }    
00343         }

Member Function Documentation

void HVariableState::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 352 of file hvariablestate.h.

References ADD_CLAUSE_INITIAL, ADD_CLAUSE_REGULAR, and newClauses_.

Referenced by activateAtom(), fixAtom(), HVariableState(), and initBlocksRandom().

00353   {
00354     if (initial) addNewClauses(ADD_CLAUSE_INITIAL, newClauses_);
00355     else addNewClauses(ADD_CLAUSE_REGULAR, newClauses_);
00356   }

void HVariableState::addNewClauses	(	int	addType,
		Array< GroundClause * > &	clauses
	)			`[inline]`

Adds new clauses to the state.

Parameters:

	addType	How the clauses are being added (see ADD_CLAUSE_*)
	clauses	Array of ground clauses to be added to the state.

Definition at line 364 of file hvariablestate.h.

References ADD_CLAUSE_DEAD, ADD_CLAUSE_REGULAR, ADD_CLAUSE_SAT, Array< Type >::append(), atom_, breakCost_, clause_, clauseCost_, Array< Type >::clear(), deadClause_, falseClause_, falseClauseLow_, fixedAtom_, Domain::getDB(), getNumAtoms(), getNumClauses(), Database::getValue(), gndClauses_, gndPredHashArray_, gndPreds_, Array< Type >::growToSize(), initMakeBreakCostWatch(), isSatisfied_, killClauses(), lowAtom_, makeCost_, MODE_HARD, MODE_SAMPLESAT, numTrueLits_, occurence_, HashArray< Type, HashFn, EqualFn >::size(), Array< Type >::size(), threshold_, useThreshold_, watch1_, watch2_, and whereFalse_.

00365   {
00366     if (hvsdebug)
00367       cout << "Adding " << clauses.size() << " new clauses.." << endl;
00368 
00369       // Must be in mc-sat to add dead or sat
00370     if (!useThreshold_ &&
00371         (addType == ADD_CLAUSE_DEAD || addType == ADD_CLAUSE_SAT))
00372     {
00373       cout << ">>> [ERR] add_dead/sat but useThreshold_ is false" << endl;
00374       exit(0);
00375     }
00376 
00377       // Store the old number of clauses and atoms
00378     int oldNumClauses = getNumClauses();
00379     int oldNumAtoms = getNumAtoms();
00380 
00381       //gndClauses_->append(clauses);
00382     for (int i = 0; i < clauses.size(); i++)
00383     {
00384       gndClauses_->append(clauses[i]);
00385       clauses[i]->appendToGndPreds(&gndPredHashArray_);
00386     }
00387 
00388     gndPreds_->growToSize(gndPredHashArray_.size());
00389 
00390     int numAtoms = getNumAtoms();
00391     int numClauses = getNumClauses();
00392       // If no new atoms or clauses have been added, then do nothing
00393     if (numAtoms == oldNumAtoms && numClauses == oldNumClauses) return;
00394 
00395     if (hvsdebug) cout << "Clauses: " << numClauses << endl;
00396       // atomIdx starts at 1
00397     atom_.growToSize(numAtoms + 1, false);
00398 
00399     makeCost_.growToSize(numAtoms + 1, 0.0);
00400     breakCost_.growToSize(numAtoms + 1, 0.0);
00401     lowAtom_.growToSize(numAtoms + 1, false);
00402     fixedAtom_.growToSize(numAtoms + 1, 0);
00403 
00404       // Copy ground preds to gndPreds_ and set values in atom and lowAtom
00405     for (int i = oldNumAtoms; i < gndPredHashArray_.size(); i++)
00406     {
00407       (*gndPreds_)[i] = gndPredHashArray_[i];
00408 
00409       if (hvsdebug)
00410       {
00411         cout << "New pred " << i + 1 << ": ";
00412         (*gndPreds_)[i]->print(cout, domain_);
00413         cout << endl;
00414       }
00415 
00416       lowAtom_[i + 1] = atom_[i + 1] = 
00417         (domain_->getDB()->getValue((*gndPreds_)[i]) == TRUE) ? true : false;
00418     }
00419     clauses.clear();
00420 
00421     clause_.growToSize(numClauses);
00422     clauseCost_.growToSize(numClauses);
00423     falseClause_.growToSize(numClauses);
00424     whereFalse_.growToSize(numClauses);
00425     numTrueLits_.growToSize(numClauses);
00426     falseClauseLow_.growToSize(numClauses);
00427     watch1_.growToSize(numClauses);
00428     watch2_.growToSize(numClauses);
00429     isSatisfied_.growToSize(numClauses, false);
00430     deadClause_.growToSize(numClauses, false);
00431     threshold_.growToSize(numClauses, false);  
00432     occurence_.growToSize(2*numAtoms + 1);
00433 
00434     for (int i = oldNumClauses; i < numClauses; i++)
00435     {
00436       GroundClause* gndClause = (*gndClauses_)[i];
00437 
00438       if (hvsdebug)
00439       {
00440         cout << "New clause " << i << ": ";
00441         gndClause->print(cout, domain_, &gndPredHashArray_);
00442         cout << endl;
00443       }
00444 
00445         // Set thresholds for clause selection
00446       if (gndClause->isHardClause()) threshold_[i] = RAND_MAX;
00447       else
00448       {
00449         double w = gndClause->getWt();
00450         threshold_[i] = RAND_MAX*(1 - exp(-abs(w)));
00451         if (hvsdebug)
00452         {
00453           cout << "Weight: " << w << endl;            
00454         }
00455       }
00456       if (hvsdebug)
00457         cout << "Threshold: " << threshold_[i] << endl;            
00458 
00459       int numGndPreds = gndClause->getNumGroundPredicates();
00460       clause_[i].growToSize(numGndPreds);
00461       for (int j = 0; j < numGndPreds; j++) 
00462       {
00463         int lit = gndClause->getGroundPredicateIndex(j);
00464         clause_[i][j] = lit;
00465         int litIdx = 2*abs(lit) - (lit > 0);
00466         occurence_[litIdx].append(i);
00467       }
00468 
00469         // Hard clause weight has been previously determined
00470       if (inferenceMode_==MODE_SAMPLESAT)
00471       {
00472         if (gndClause->getWt()>0) clauseCost_[i] = 1;
00473         else clauseCost_[i] = -1;
00474       }
00475       else if (gndClause->isHardClause())
00476         clauseCost_[i] = hardWt_;
00477       else
00478         clauseCost_[i] = gndClause->getWt();
00479 
00480         // filter hard clauses
00481       if (inferenceMode_ == MODE_HARD && !gndClause->isHardClause())
00482       {
00483           // mark dead
00484         deadClause_[i] = true;
00485       }
00486     }
00487 
00488     if (addType == ADD_CLAUSE_DEAD)
00489     {
00490         // set to dead: no need for initMakeBreakCost, won't impact anyone
00491       for (int i = oldNumClauses; i < numClauses; i++)
00492       {
00493         deadClause_[i] = true;
00494       }
00495     }
00496     else if (addType == ADD_CLAUSE_SAT)
00497     {
00498         // set to dead: no need for initMakeBreakCost, won't impact anyone
00499       for (int i = oldNumClauses; i < numClauses; i++)
00500       {
00501         isSatisfied_[i]=true;
00502       }
00503     }
00504     else if (addType == ADD_CLAUSE_REGULAR)
00505     {
00506       if (useThreshold_)
00507         killClauses(oldNumClauses);
00508       else
00509         initMakeBreakCostWatch(oldNumClauses);
00510     }
00511 
00512     if (hvsdebug) 
00513       cout << "Done adding new clauses.." << endl;
00514   }

void HVariableState::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. For continous variables, we assign an arbitrary value

Definition at line 710 of file hvariablestate.h.

References atom_, atomEvi_, bInitFromEvi_, contAtomNum_, contAtoms_, contAtomsEvi_, Array< Type >::copyFrom(), init(), initContinuousVariableRandom(), printContAtom(), printDisAtom(), and setValueOfAtom().

Referenced by HMaxWalkSat::init().

00711         {
00712                 // Initialize variable assignment values
00713                 if (!bInitFromEvi_) // Random initialization rather than initialize from evidence.
00714                 {
00715                         // Random truth value for discrete variables.
00716                         for (int i = 1; i <= baseNumAtoms_; i++)
00717                         {
00718                                 if (hvsdebug) cout << "Atom " << i << " not in block" << endl;
00719                                 setValueOfAtom(i, random() % 2, false, -1);
00720                         }
00721 
00722                         // Random initialize continuous variables.
00723                         initContinuousVariableRandom();
00724 
00725                         if (hvsdebug)
00726                         {
00727                                 cout << "Randomly initializing dis&cont variables to:" << endl;
00728                                 for(int i = 0; i < baseNumAtoms_; i++)
00729                                 {
00730                                         printDisAtom(i+1, cout);
00731                                 }
00732 
00733                                 for(int i = 0; i < contAtomNum_; i++)
00734                                 {
00735                                         printContAtom(i+1, cout);
00736                                 }
00737                         }
00738                 }
00739                 else
00740                 {
00741                         atom_.copyFrom(atomEvi_);
00742                         contAtoms_.copyFrom(contAtomsEvi_);
00743                 }
00744 
00745                 // Initialize other state information.
00746                 init();
00747         }

void HVariableState::initMakeBreakCostWatch ( ) [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 887 of file hvariablestate.h.

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

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

00888         {
00889                 if (hvsdebug)
00890                 {
00891                         cout << "entering intiMakeBreakCostWatch()" << endl;
00892                 }
00893                 assert(makeCost_.size() == breakCost_.size());
00894                 // Reset make and break cost to 0
00895                 for (int i = 0; i < makeCost_.size(); i++)
00896                 {
00897                         makeCost_[i] = breakCost_[i] = 0.0;
00898                 }
00899                 initMakeBreakCostWatch(0);
00900                 if (hvsdebug)
00901                 {
00902                         cout << "leaving intiMakeBreakCostWatch()" << endl;
00903                 }
00904         }

int HVariableState::getIndexOfAtomInRandomFalseClause ( ) [inline]

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

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

Definition at line 1041 of file hvariablestate.h.

References clause_, clauseCost_, falseClause_, getClauseSize(), and getRandomTrueLitInClause().

01042         {
01043                 if (numFalseClauses_ == 0) return NOVALUE;
01044                 int clauseIdx = falseClause_[random()%numFalseClauses_];
01045                 // Pos. clause: return index of random atom
01046                 if (clauseCost_[clauseIdx] > 0)
01047                         return abs(clause_[clauseIdx][random()%getClauseSize(clauseIdx)]);
01048                 // Neg. clause: find random true lit
01049                 else
01050                         return getRandomTrueLitInClause(clauseIdx);
01051         }

int HVariableState::getRandomFalseClauseIndex ( ) [inline]

Returns the index of a random unsatisfied pos.

clause or a random satisfied neg. clause.

Definition at line 1057 of file hvariablestate.h.

References falseClause_.

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

bool HVariableState::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 1097 of file hvariablestate.h.

References atom_.

Referenced by flipAtom(), getImprovementInWeightSumByFlipping(), HMaxWalkSat::infer(), HMaxWalkSat::pickHMCS(), updateMakeBreakCostAfterFlip(), and updateSatisfiedClauses().

01098         {
01099                 return atom_[atomIdx];
01100         }

bool HVariableState::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 1108 of file hvariablestate.h.

References lowAtom_.

01109         {
01110                 return lowAtom_[atomIdx];
01111         }

void HVariableState::setValueOfAtom	(	const int &	atomIdx,
		const bool &	value,
		const bool &	activate,
		const int &	blockIdx
	)			`[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.
	activate	If true, atom is activated if not active.
	blockIdx	Indicates which block the atom being flipped is in. If not in one, this is -1.

Definition at line 1157 of file hvariablestate.h.

References activateAtom(), atom_, Domain::getDB(), gndPredHashArray_, isActive(), Predicate::printWithStrVar(), Domain::setTruePredInBlock(), and Database::setValue().

Referenced by activateAtom(), fixAtom(), flipAtomValue(), getImprovementInWeightSumByFlipping(), initBlocksRandom(), initRandom(), setOthersInBlockToFalse(), UpdateHybridClauseInfoByDisAtom(), and UpdateHybridClauseWeightSumByDisAtom().

01159   {
01160       // If atom already has this value, then do nothing
01161     if (atom_[atomIdx] == value) return;
01162     if (hvsdebug) cout << "Setting value of atom " << atomIdx 
01163                       << " to " << value << endl;
01164       // Propagate assignment to DB
01165     GroundPredicate* p = gndPredHashArray_[atomIdx - 1];
01166     if (value)
01167       domain_->getDB()->setValue(p, TRUE);
01168     else
01169       domain_->getDB()->setValue(p, FALSE);
01170 
01171       // If not active, then activate it
01172     if (activate && lazy_ && !isActive(atomIdx))
01173     {
01174       bool ignoreActivePreds = false;
01175       bool groundOnly = false;
01176       activateAtom(atomIdx, ignoreActivePreds, groundOnly);
01177     }
01178     atom_[atomIdx] = value;
01179 
01180       // If in block and setting to true, tell the domain
01181     if (blockIdx > -1 && value)
01182     {
01183       Predicate* pred = p->createEquivalentPredicate(domain_);
01184       domain_->setTruePredInBlock(blockIdx, pred);
01185       if (hvsdebug)
01186       {
01187         cout << "Set true pred in block " << blockIdx << " to ";
01188         pred->printWithStrVar(cout, domain_);
01189         cout << endl;
01190       }
01191     }
01192   }

void HVariableState::flipAtom	(	const int &	toFlip,
		const int &	blockIdx
	)			`[inline]`

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

Parameters:

	toFlip	Index of atom to be flipped.
	blockIdx	Index of block in which atom is, or -1 if not in one.

Definition at line 1218 of file hvariablestate.h.

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

Referenced by HMaxWalkSat::flipAtom().

01219   {
01220     bool toFlipValue = getValueOfAtom(toFlip);
01221     register int clauseIdx;
01222     int sign;
01223     int oppSign;
01224     int litIdx;
01225     if (toFlipValue)
01226       sign = 1;
01227     else
01228       sign = 0;
01229     oppSign = sign ^ 1;
01230 
01231     flipAtomValue(toFlip, blockIdx);
01232 
01233       // Update all clauses in which the atom occurs as a true literal
01234     litIdx = 2*toFlip - sign;
01235     Array<int>& posOccArray = getOccurenceArray(litIdx);
01236     for (int i = 0; i < posOccArray.size(); i++)
01237     {
01238       clauseIdx = posOccArray[i];
01239         // Don't look at dead clauses
01240       if (deadClause_[clauseIdx]) continue;
01241         // The true lit became a false lit
01242       int numTrueLits = decrementNumTrueLits(clauseIdx);
01243       long double cost = getClauseCost(clauseIdx);
01244       int watch1 = getWatch1(clauseIdx);
01245       int watch2 = getWatch2(clauseIdx);
01246 
01247         // 1. If last true lit was flipped, then we have to update
01248         // the makecost / breakcost info accordingly        
01249       if (numTrueLits == 0)
01250       {
01251         weightSumDis_ -= clauseCost_[clauseIdx];
01252           // Pos. clause
01253         if (cost > 0)
01254         {
01255             // Add this clause as false in the state
01256           addFalseClause(clauseIdx);
01257             // Decrease toFlip's breakcost (add neg. cost)
01258           addBreakCost(toFlip, -cost);
01259             // Increase makecost of all vars in clause (add pos. cost)
01260           addMakeCostToAtomsInClause(clauseIdx, cost);
01261         }
01262           // Neg. clause
01263         else
01264         {
01265           assert(cost < 0);
01266             // Remove this clause as false in the state
01267           removeFalseClause(clauseIdx);
01268             // Increase breakcost of all vars in clause (add pos. cost)
01269           addBreakCostToAtomsInClause(clauseIdx, -cost);
01270             // Decrease toFlip's makecost (add neg. cost)
01271           addMakeCost(toFlip, cost);
01272         }
01273       }
01274         // 2. If there is now one true lit left, then move watch2
01275         // up to watch1 and increase the breakcost / makecost of watch1
01276       else if (numTrueLits == 1)
01277       {
01278         if (watch1 == toFlip)
01279                                 {
01280                                         assert(watch1 != watch2);
01281                                         setWatch1(clauseIdx, watch2);
01282                                         watch1 = getWatch1(clauseIdx);
01283                                 }
01284 
01285                                 // Pos. clause: Increase toFlip's breakcost (add pos. cost)
01286                                 if (cost > 0)
01287                                 {
01288                                         addBreakCost(watch1, cost);
01289                                 }
01290                                 // Neg. clause: Increase toFlip's makecost (add pos. cost)
01291                                 else
01292                                 {
01293                                         assert(cost < 0);
01294                                         addMakeCost(watch1, -cost);
01295                                 }
01296                         }
01297                         // 3. If there are 2 or more true lits left, then we have to
01298                         // find a new true lit to watch if one was flipped
01299                         else
01300                         { /* numtruelit[clauseIdx] >= 2 */
01301                                 // If watch1[clauseIdx] has been flipped
01302                                 if (watch1 == toFlip)
01303                                 {
01304                                         // find a different true literal to watch
01305                                         int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
01306                                         setWatch1(clauseIdx, diffTrueLit);
01307                                 }
01308                                 // If watch2[clauseIdx] has been flipped
01309                                 else if (watch2 == toFlip)
01310                                 {
01311                                         // find a different true literal to watch
01312                                         int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
01313                                         setWatch2(clauseIdx, diffTrueLit);
01314                                 }
01315                         }
01316                 }
01317 
01318                 // Update all clauses in which the atom occurs as a false literal
01319                 litIdx = 2*toFlip - oppSign;
01320                 Array<int>& negOccArray = getOccurenceArray(litIdx);
01321                 for (int i = 0; i < negOccArray.size(); i++)
01322                 {
01323                         clauseIdx = negOccArray[i];
01324                         // Don't look at dead clauses
01325                         if (deadClause_[clauseIdx]) continue;
01326                         // The false lit became a true lit
01327                         int numTrueLits = incrementNumTrueLits(clauseIdx);
01328                         long double cost = getClauseCost(clauseIdx);
01329                         int watch1 = getWatch1(clauseIdx);
01330 
01331                         // 1. If this is the only true lit, then we have to update
01332                         // the makecost / breakcost info accordingly        
01333                         if (numTrueLits == 1)
01334                         {
01335                                 weightSumDis_ += clauseCost_[clauseIdx];
01336                                 // Pos. clause
01337                                 if (cost > 0)
01338                                 {
01339                                         // Remove this clause as false in the state
01340                                         removeFalseClause(clauseIdx);
01341                                         // Increase toFlip's breakcost (add pos. cost)
01342                                         addBreakCost(toFlip, cost);        
01343                                         // Decrease makecost of all vars in clause (add neg. cost)
01344                                         addMakeCostToAtomsInClause(clauseIdx, -cost);
01345                                 }
01346                                 // Neg. clause
01347                                 else
01348                                 {
01349                                         assert(cost < 0);
01350                                         // Add this clause as false in the state
01351                                         addFalseClause(clauseIdx);
01352                                         // Decrease breakcost of all vars in clause (add neg. cost)
01353                                         addBreakCostToAtomsInClause(clauseIdx, cost);
01354                                         // Increase toFlip's makecost (add pos. cost)
01355                                         addMakeCost(toFlip, -cost);
01356                                 }
01357                                 // Watch this atom
01358                                 setWatch1(clauseIdx, toFlip);
01359                         }
01360                         // 2. If there are now exactly 2 true lits, then watch second atom
01361                         // and update breakcost
01362                         else if (numTrueLits == 2)
01363                                 {
01364                                         if (cost > 0)
01365                                         {
01366                                                 // Pos. clause
01367                                                 // Decrease breakcost of first atom being watched (add neg. cost)
01368                                                 addBreakCost(watch1, -cost);
01369                                         }
01370                                         else
01371                                         {
01372                                                 // Neg. clause
01373                                                 assert(cost < 0);
01374                                                 // Decrease makecost of first atom being watched (add neg. cost)
01375                                                 addMakeCost(watch1, cost);
01376                                         }
01377 
01378                                         // Watch second atom
01379                                         setWatch2(clauseIdx, toFlip);
01380                                 }
01381                 }
01382         }

void HVariableState::flipAtomValue	(	const int &	atomIdx,
		const int &	blockIdx
	)			`[inline]`

Flips the truth value of an atom.

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

Parameters:

	atomIdx	Index of atom to be flipped.
	blockIdx	Index of block in which the atom is in, or -1 if not in one.

Definition at line 1403 of file hvariablestate.h.

References atom_, and setValueOfAtom().

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

01404   {
01405     bool opposite = !atom_[atomIdx];
01406     bool activate = true;
01407     setValueOfAtom(atomIdx, opposite, activate, blockIdx);
01408   }

bool HVariableState::activateAtom	(	const int &	atomIdx,
		const bool &	ignoreActivePreds,
		const bool &	groundOnly
	)			`[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.
	ignoreActivePreds	If true, active atoms are ignored when getting active clauses (just gets unsatisfied clauses).
	groundOnly	If true, atom itself is not activated, just its active clauses are retrieved.

Definition at line 1447 of file hvariablestate.h.

References ADD_CLAUSE_DEAD, ADD_CLAUSE_REGULAR, ADD_CLAUSE_SAT, addNewClauses(), Array< Type >::append(), atom_, Array< Type >::clear(), fixAtom(), getActiveClauses(), Database::getActiveStatus(), Domain::getDB(), gndPredHashArray_, isActive(), Database::setActiveStatus(), setValueOfAtom(), Array< Type >::size(), updateMakeBreakCostAfterFlip(), and useThreshold_.

Referenced by setValueOfAtom().

01449   {
01450     /***
01451      * . [IF MCSAT] 
01452      * - check neg-wt clauses
01453      * . if alive, fix
01454      * . else mark dead
01455      * - if not fixed, add all pos-wt, killClauses
01456      * - else add dead
01457      * . [ELSE] add all
01458      ***/
01459     if (lazy_ && !isActive(atomIdx))
01460     {
01461       if (hvsdebug)
01462       {
01463         cout << "\tActivating ";
01464         gndPredHashArray_[atomIdx-1]->print(cout,domain_);
01465         cout << " " <<
01466         domain_->getDB()->getActiveStatus(gndPredHashArray_[atomIdx-1]) << endl;
01467       }
01468 
01469         // Set atom to true first, see if avoid getting clauses already active
01470       bool needToFlipBack = false;
01471       if (!atom_[atomIdx])
01472       {
01473         bool activate = false;
01474         setValueOfAtom(atomIdx, true, activate, -1);
01475         updateMakeBreakCostAfterFlip(atomIdx);
01476         needToFlipBack = true;
01477       } 
01478 
01479         // gather active clauses
01480       Predicate* p =
01481         gndPredHashArray_[atomIdx - 1]->createEquivalentPredicate(domain_);
01482 
01483       bool isFixed = false;
01484       Array<GroundClause*> unsatClauses;
01485       Array<GroundClause*> deadClauses;
01486       Array<GroundClause*> toAddClauses;
01487 
01488         // Using newClauses_ causes problem since it's shared across the board
01489       getActiveClauses(p, unsatClauses, true, ignoreActivePreds);
01490 
01491         // if MC-SAT: check neg-wt or unit clauses and see if can fix         
01492       if (useThreshold_)
01493       {
01494           // first append deadClauses, then pos-wt
01495         for (int ni = 0; ni < unsatClauses.size(); ni++)
01496         {
01497           GroundClause* c = unsatClauses[ni];
01498           if (c->getWt() < 0)
01499           {  // Neg. weighted clause
01500               // since newClauses_ excludes clauses in memory, c must be
01501               // goodInPrevious
01502             double threshold = RAND_MAX*(1 - exp(c->getWt()));
01503             if (random() <= threshold)
01504             {
01505                 // fix
01506               isFixed = true;
01507 
01508                 // append dead and fixed clauses first, so fixed atoms do not
01509                 // activate them unnecessarily
01510               if (deadClauses.size() > 0)
01511                 addNewClauses(ADD_CLAUSE_DEAD, deadClauses);
01512 
01513               Array<GroundClause*> fixedClauses;
01514               fixedClauses.append(c);
01515               addNewClauses(ADD_CLAUSE_SAT, fixedClauses);
01516 
01517                 // --- fix the atoms
01518               for (int pi = 0; pi < c->getNumGroundPredicates(); pi++)
01519               {
01520                 int lit = c->getGroundPredicateIndex(pi);
01521                 fixAtom(abs(lit), (lit < 0));
01522               }
01523 
01524                 // - can quit now
01525               break;
01526             }
01527             else
01528             {
01529                 // dead
01530               deadClauses.append(c);
01531             }
01532           }
01533           else if (c->getNumGroundPredicates() == 1)
01534           {  // Unit clause
01535             double threshold = RAND_MAX*(1 - exp(-c->getWt()));
01536             if (random() <= threshold)
01537             {
01538                 // fix
01539               isFixed = true;
01540 
01541                 // append dead and fixed clauses first, so fixed atoms do not
01542                 // activate them unnecessarily
01543               if (deadClauses.size() > 0)
01544                 addNewClauses(ADD_CLAUSE_DEAD, deadClauses);
01545 
01546               Array<GroundClause*> fixedClauses;
01547               fixedClauses.append(c);
01548               addNewClauses(ADD_CLAUSE_SAT, fixedClauses);
01549 
01550                 // --- fix the atoms
01551               int lit = c->getGroundPredicateIndex(0);
01552               fixAtom(abs(lit), (lit > 0)); // this is positive wt
01553 
01554                 // - can quit now
01555               break;
01556             }
01557             else
01558             {
01559                 // dead
01560               deadClauses.append(c);
01561             }
01562           }
01563           else toAddClauses.append(c);
01564         }
01565       }
01566 
01567         // Add the clauses and preds and fill info arrays
01568       if (!isFixed)
01569       {
01570         if (deadClauses.size() > 0)
01571           addNewClauses(ADD_CLAUSE_DEAD, deadClauses);
01572 
01573         if (useThreshold_)
01574           addNewClauses(ADD_CLAUSE_REGULAR, toAddClauses);
01575         else // lazy-sat
01576           addNewClauses(ADD_CLAUSE_REGULAR, unsatClauses);
01577 
01578           // To avoid append already-active: if not fixed, might need to
01579           // flip back
01580         if (needToFlipBack)
01581         {
01582           bool activate = false;
01583           setValueOfAtom(atomIdx, false, activate, -1);
01584           updateMakeBreakCostAfterFlip(atomIdx);
01585         }
01586 
01587         if (!groundOnly)
01588         {
01589             // Set active status in db
01590           domain_->getDB()->setActiveStatus(p, true);
01591           activeAtoms_++;
01592         }
01593       }
01594 
01595       delete p;
01596       unsatClauses.clear();
01597       deadClauses.clear();
01598       toAddClauses.clear();
01599 
01600       return !isFixed; // if !isFixed, then activated
01601     }
01602     return true;
01603   }

void HVariableState::updateSatisfiedClauses ( const int & toFix ) [inline]

Updates isSatisfiedClause after an atom is fixed.

ASSUME: fixed val already applied, and updateMakeBreakCost called

Parameters:

toFix

Index of atom fixed

Definition at line 1636 of file hvariablestate.h.

References deadClause_, getClauseCost(), getOccurenceArray(), getValueOfAtom(), isSatisfied_, and Array< Type >::size().

Referenced by fixAtom().

01637   {
01638       // Already flipped
01639     bool toFlipValue = getValueOfAtom(toFix);
01640       
01641     register int clauseIdx;
01642     int sign;
01643     int litIdx;
01644     if (toFlipValue)
01645       sign = 1;
01646     else
01647       sign = 0;
01648 
01649       // Set isSatisfied: all clauses in which the atom occurs as a true literal
01650     litIdx = 2*toFix - sign;
01651     Array<int>& posOccArray = getOccurenceArray(litIdx);
01652     for (int i = 0; i < posOccArray.size(); i++)
01653     {
01654       clauseIdx = posOccArray[i];
01655         // Don't look at dead clauses
01656         // ignore already sat
01657       if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;
01658 
01659       if (getClauseCost(clauseIdx) < 0) 
01660       {
01661         cout << "ERR: in MC-SAT, active neg-wt clause (" << clauseIdx
01662              << ") is sat by fixed "<<endl;
01663         exit(0);
01664       }
01665       isSatisfied_[clauseIdx] = true;  
01666     }
01667   }

void HVariableState::updateMakeBreakCostAfterFlip ( const int & toFlip ) [inline]

Updates cost after flip.

Assume: already activated and flipped. Called by flipAtom and fixAtom (if fixed to the opposite val)

Definition at line 1674 of file hvariablestate.h.

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

Referenced by activateAtom(), and fixAtom().

01675   {   
01676       // Already flipped
01677     bool toFlipValue = !getValueOfAtom(toFlip);
01678 
01679     register int clauseIdx;
01680     int sign;
01681     int oppSign;
01682     int litIdx;
01683     if (toFlipValue)
01684       sign = 1;
01685     else
01686       sign = 0;
01687     oppSign = sign ^ 1;
01688 
01689       // Update all clauses in which the atom occurs as a true literal
01690     litIdx = 2*toFlip - sign;
01691     Array<int>& posOccArray = getOccurenceArray(litIdx);
01692 
01693     for (int i = 0; i < posOccArray.size(); i++)
01694     {
01695       clauseIdx = posOccArray[i];
01696         // Don't look at dead clauses and sat clauses
01697       if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;
01698 
01699         // The true lit became a false lit
01700       int numTrueLits = decrementNumTrueLits(clauseIdx);
01701       long double cost = getClauseCost(clauseIdx);
01702       int watch1 = getWatch1(clauseIdx);
01703       int watch2 = getWatch2(clauseIdx);
01704 
01705         // 1. If last true lit was flipped, then we have to update
01706         // the makecost / breakcost info accordingly        
01707       if (numTrueLits == 0)
01708       {
01709           // Pos. clause
01710         if (cost >= 0)
01711         {
01712             // Add this clause as false in the state
01713           addFalseClause(clauseIdx);
01714             // Decrease toFlip's breakcost (add neg. cost)
01715           addBreakCost(toFlip, -cost);
01716             // Increase makecost of all vars in clause (add pos. cost)
01717           addMakeCostToAtomsInClause(clauseIdx, cost);
01718         }
01719           // Neg. clause
01720         else
01721         {
01722           assert(cost < 0);
01723             // Remove this clause as false in the state
01724           removeFalseClause(clauseIdx);
01725             // Increase breakcost of all vars in clause (add pos. cost)
01726           addBreakCostToAtomsInClause(clauseIdx, -cost);        
01727             // Decrease toFlip's makecost (add neg. cost)
01728           addMakeCost(toFlip, cost);
01729         }
01730       }
01731         // 2. If there is now one true lit left, then move watch2
01732         // up to watch1 and increase the breakcost / makecost of watch1
01733       else if (numTrueLits == 1)
01734       {
01735         if (watch1 == toFlip)
01736         {
01737           assert(watch1 != watch2);
01738           setWatch1(clauseIdx, watch2);
01739           watch1 = getWatch1(clauseIdx);
01740         }
01741           // Pos. clause: Increase toFlip's breakcost (add pos. cost)
01742         if (cost >= 0)
01743         {
01744           addBreakCost(watch1, cost);
01745         }
01746             // Neg. clause: Increase toFlip's makecost (add pos. cost)
01747         else
01748         {
01749           assert(cost < 0);
01750           addMakeCost(watch1, -cost);
01751         }
01752       }
01753         // 3. If there are 2 or more true lits left, then we have to
01754         // find a new true lit to watch if one was flipped
01755       else
01756       {
01757           /* numtruelit[clauseIdx] >= 2 */
01758           // If watch1[clauseIdx] has been flipped
01759         if (watch1 == toFlip)
01760         {
01761             // find a different true literal to watch
01762           int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
01763           setWatch1(clauseIdx, diffTrueLit);
01764         }
01765           // If watch2[clauseIdx] has been flipped
01766         else if (watch2 == toFlip)
01767         {
01768             // find a different true literal to watch
01769           int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
01770           setWatch2(clauseIdx, diffTrueLit);
01771         }
01772       }
01773     }
01774 
01775       // Update all clauses in which the atom occurs as a false literal
01776     litIdx = 2*toFlip - oppSign;
01777     Array<int>& negOccArray = getOccurenceArray(litIdx);
01778     for (int i = 0; i < negOccArray.size(); i++)
01779     {
01780       clauseIdx = negOccArray[i];
01781         // Don't look at dead clauses or satisfied clauses
01782       if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;
01783 
01784         // The false lit became a true lit
01785       int numTrueLits = incrementNumTrueLits(clauseIdx);
01786       long double cost = getClauseCost(clauseIdx);
01787       int watch1 = getWatch1(clauseIdx);
01788 
01789         // 1. If this is the only true lit, then we have to update
01790         // the makecost / breakcost info accordingly        
01791       if (numTrueLits == 1)
01792       {
01793           // Pos. clause
01794         if (cost >= 0)
01795         {
01796             // Remove this clause as false in the state
01797           removeFalseClause(clauseIdx);
01798             // Increase toFlip's breakcost (add pos. cost)
01799           addBreakCost(toFlip, cost);        
01800             // Decrease makecost of all vars in clause (add neg. cost)
01801           addMakeCostToAtomsInClause(clauseIdx, -cost);
01802         }
01803           // Neg. clause
01804         else
01805         {
01806           assert(cost < 0);
01807             // Add this clause as false in the state
01808           addFalseClause(clauseIdx);
01809             // Decrease breakcost of all vars in clause (add neg. cost)
01810           addBreakCostToAtomsInClause(clauseIdx, cost);
01811             // Increase toFlip's makecost (add pos. cost)
01812           addMakeCost(toFlip, -cost);
01813         }
01814           // Watch this atom
01815         setWatch1(clauseIdx, toFlip);
01816       }
01817         // 2. If there are now exactly 2 true lits, then watch second atom
01818         // and update breakcost
01819       else if (numTrueLits == 2)
01820       {
01821         if (cost >= 0)
01822         {
01823             // Pos. clause
01824             // Decrease breakcost of first atom being watched (add neg. cost)
01825           addBreakCost(watch1, -cost);
01826         }
01827         else
01828         {
01829             // Neg. clause
01830           assert(cost < 0);
01831             // Decrease makecost of first atom being watched (add neg. cost)
01832           addMakeCost(watch1, cost);
01833         }
01834           // Watch second atom
01835         setWatch2(clauseIdx, toFlip);
01836       }
01837     }
01838   }

bool HVariableState::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 1846 of file hvariablestate.h.

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

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

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

bool HVariableState::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 1857 of file hvariablestate.h.

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

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

void HVariableState::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 1933 of file hvariablestate.h.

References breakCost_, clause_, and getClauseSize().

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

01935         {
01936                 register int size = getClauseSize(clauseIdx);
01937                 for (int i = 0; i < size; i++)
01938                 {
01939                         register int lit = clause_[clauseIdx][i];
01940                         breakCost_[abs(lit)] += cost;
01941                 }
01942         }

void HVariableState::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 1950 of file hvariablestate.h.

References breakCost_, clause_, and getClauseSize().

01952         {
01953                 register int size = getClauseSize(clauseIdx);
01954                 for (int i = 0; i < size; i++)
01955                 {
01956                         register int lit = clause_[clauseIdx][i];
01957                         breakCost_[abs(lit)] -= cost;
01958                 }
01959         }

void HVariableState::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 1967 of file hvariablestate.h.

References makeCost_.

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

01968         {
01969                 makeCost_[atomIdx] += cost;
01970         }

void HVariableState::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 1978 of file hvariablestate.h.

References makeCost_.

01979         {
01980                 makeCost_[atomIdx] -= cost;
01981         }

void HVariableState::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 1989 of file hvariablestate.h.

References clause_, getClauseSize(), and makeCost_.

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

01991         {
01992                 register int size = getClauseSize(clauseIdx);
01993                 for (int i = 0; i < size; i++)
01994                 {
01995                         register int lit = clause_[clauseIdx][i];
01996                         makeCost_[abs(lit)] += cost;
01997                 }
01998         }

void HVariableState::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 2006 of file hvariablestate.h.

References clause_, getClauseSize(), and makeCost_.

02008         {
02009                 register int size = getClauseSize(clauseIdx);
02010                 for (int i = 0; i < size; i++)
02011                 {
02012                         register int lit = clause_[clauseIdx][i];
02013                         makeCost_[abs(lit)] -= cost;
02014                 }
02015         }

const int HVariableState::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 2026 of file hvariablestate.h.

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

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

02029         {
02030                 register int size = getClauseSize(clauseIdx);
02031                 for (int i = 0; i < size; i++)
02032                 {
02033                         register int lit = clause_[clauseIdx][i];
02034                         register int v = abs(lit);
02035                         if (isTrueLiteral(lit) && v != atomIdx1 && v != atomIdx2)
02036                                 return v;
02037                 }
02038                 // If we're here, then no other true lit exists
02039                 assert(false);
02040                 return -1;
02041         }

const int HVariableState::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 2073 of file hvariablestate.h.

References clause_, getClauseSize(), isTrueLiteral(), and numTrueLits_.

Referenced by getIndexOfAtomInRandomFalseClause().

02074         {
02075                 assert(numTrueLits_[clauseIdx] > 0);
02076                 int trueLit = random()%numTrueLits_[clauseIdx];
02077                 int whichTrueLit = 0;
02078                 for (int i = 0; i < getClauseSize(clauseIdx); i++)
02079                 {
02080                         int lit = clause_[clauseIdx][i];
02081                         int atm = abs(lit);
02082                         // True literal
02083                         if (isTrueLiteral(lit))
02084                                 if (trueLit == whichTrueLit++)
02085                                         return atm;
02086                 }
02087                 // If we're here, then no other true lit exists
02088                 assert(false);
02089                 return -1;
02090         }

const int HVariableState::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 2137 of file hvariablestate.h.

References Array< Type >::size().

Referenced by fixAtom().

02138         {
02139                 for (int i = 0; i < blocks_->size(); i++)
02140                 {
02141                         int blockIdx = (*blocks_)[i].find(atomIdx);
02142                         if (blockIdx >= 0)
02143                                 return i;
02144                 }
02145                 return -1;
02146         }

void HVariableState::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. If lazy, the f.o. clause frequencies computed when activating are used.

Parameters:

	numGndings	Array being filled with values.
	clauseCnt	Number of first-order clauses (size of numGndings)
	tv	If true, number of true groundings are retrieved, otherwise false groundings are retrieved.

Definition at line 2266 of file hvariablestate.h.

References MLN::getClause(), MLN::getNumClauses(), Domain::getNumNonEvidGroundings(), gndClauses_, isTrueLiteral(), and Array< Type >::size().

Referenced by HMaxWalkSat::getClauseTrueCnts(), and HMaxWalkSat::infer().

02267   {
02268       // If lazy, then all groundings of pos. clauses not materialized in this
02269       // state are true (non-materialized groundings of neg. clauses are false),
02270       // so if tv is false and clause is pos. (or tv is true and clause is
02271       // neg.), then eager and lazy counts are equivalent. If tv is
02272       // true and clause is pos. (or tv is false and clause is neg.), then we
02273       // need to keep track of true *and* false groundings and
02274       // then subtract from total groundings of the f.o. clause.
02275       
02276       // This holds the false groundings when tv is true and lazy.
02277     Array<double> lazyFalseGndings(numGndings->size(), 0);
02278     Array<double> lazyTrueGndings(numGndings->size(), 0);
02279 
02280     IntBoolPairItr itr;
02281     IntBoolPair *clauseFrequencies;
02282     
02283       // numGndings should have been initialized with non-negative values
02284     int clauseCnt = numGndings->size();
02285     assert(clauseCnt == mln_->getNumClauses());
02286     for (int clauseno = 0; clauseno < clauseCnt; clauseno++)
02287       assert ((*numGndings)[clauseno] >= 0);
02288     
02289     for (int i = 0; i < gndClauses_->size(); i++)
02290     {
02291       GroundClause *gndClause = (*gndClauses_)[i];
02292       int satLitcnt = 0;
02293       for (int j = 0; j < gndClause->getNumGroundPredicates(); j++)
02294       {
02295         int lit = gndClause->getGroundPredicateIndex(j);
02296         if (isTrueLiteral(lit)) satLitcnt++;
02297       }
02298 
02299       clauseFrequencies = gndClause->getClauseFrequencies();
02300       for (itr = clauseFrequencies->begin();
02301            itr != clauseFrequencies->end(); itr++)
02302       {
02303         int clauseno = itr->first;
02304         int frequency = itr->second.first;
02305         bool invertWt = itr->second.second;
02306           // If flipped unit clause, then we want opposite kind of grounding
02307         if (invertWt)
02308         {
02309             // Want true and is true => don't count it
02310           if (tv && satLitcnt > 0)
02311           {
02312               // Lazy: We need to keep track of false groundings also
02313             if (lazy_) lazyFalseGndings[clauseno] += frequency;
02314             continue;
02315           }
02316             // Want false and is false => don't count it
02317           if (!tv && satLitcnt == 0)
02318           {
02319               // Lazy: We need to keep track of false groundings also
02320             if (lazy_) lazyTrueGndings[clauseno] += frequency;
02321             continue;
02322           }
02323         }
02324         else
02325         {
02326             // Want true and is false => don't count it
02327           if (tv && satLitcnt == 0)
02328           {
02329               // Lazy: We need to keep track of false groundings also
02330             if (lazy_) lazyFalseGndings[clauseno] += frequency;
02331             continue;
02332           }
02333             // Want false and is true => don't count it
02334           if (!tv && satLitcnt > 0)
02335           {
02336               // Lazy: We need to keep track of false groundings also
02337             if (lazy_) lazyTrueGndings[clauseno] += frequency;
02338             continue;
02339           }
02340         }
02341         (*numGndings)[clauseno] += frequency;
02342       }
02343     }
02344     
02345       // Getting true counts in lazy: we have to add the remaining groundings
02346       // not materialized (they are by definition true groundings if clause is
02347       // positive, or false groundings if clause is negative)
02348     if (lazy_)
02349     {
02350       for (int c = 0; c < mln_->getNumClauses(); c++)
02351       {
02352         const Clause* clause = mln_->getClause(c);
02353           // Getting true counts and positive clause
02354         if (tv && clause->getWt() >= 0)
02355         {
02356           double totalGndings = domain_->getNumNonEvidGroundings(c);
02357           assert(totalGndings >= (*numGndings)[c] + lazyFalseGndings[c]);
02358           double remainingTrueGndings = totalGndings - lazyFalseGndings[c] -
02359                                         (*numGndings)[c];
02360           (*numGndings)[c] += remainingTrueGndings;
02361         }
02362           // Getting false counts and negative clause
02363         else if (!tv && clause->getWt() < 0)
02364         {
02365           double totalGndings = domain_->getNumNonEvidGroundings(c);
02366           assert(totalGndings >= (*numGndings)[c] + lazyTrueGndings[c]);
02367           double remainingFalseGndings = totalGndings - lazyTrueGndings[c] -
02368                                         (*numGndings)[c];
02369           (*numGndings)[c] += remainingFalseGndings;
02370         }
02371       }
02372     }
02373 
02374   }

void HVariableState::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	Absolute index of atom in block exempt from being set to false.
	blockIdx	Index of block whose atoms are set to false.

Definition at line 2383 of file hvariablestate.h.

References HashArray< Type, HashFn, EqualFn >::find(), fixedAtom_, Domain::getBlockSize(), Domain::getPredInBlock(), gndPredHashArray_, GroundPredicate::print(), and setValueOfAtom().

Referenced by initBlocksRandom().

02384   {
02385     if (hvsdebug)
02386     {
02387       cout << "Set all in block " << blockIdx << " to false except "
02388            << atomIdx << endl;
02389     }
02390     int blockSize = domain_->getBlockSize(blockIdx);
02391     for (int i = 0; i < blockSize; i++)
02392     {
02393       const Predicate* pred = domain_->getPredInBlock(i, blockIdx);
02394       GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);      
02395       int idx = gndPredHashArray_.find(gndPred);
02396 
02397       if (hvsdebug)
02398       {
02399         cout << "Gnd pred in block ";
02400         gndPred->print(cout, domain_);
02401         cout << " (idx " << idx << ")" << endl;
02402       }
02403 
02404       delete gndPred;
02405       delete pred;
02406       
02407         // Pred already present: check that it's not fixed
02408       if (idx >= 0)
02409       {
02410           // Atom not the one specified and not fixed
02411         if (idx != atomIdx && fixedAtom_[idx + 1] == 0)
02412         {
02413           if (hvsdebug)
02414             cout << "Set " << idx + 1 << " to false" << endl;
02415 
02416           bool activate = true;
02417           setValueOfAtom(idx + 1, false, activate, -1);
02418         }
02419       }
02420     }
02421   }

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

Fixes an atom to a truth value.

This means the atom can not change its truth value 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 2451 of file hvariablestate.h.

References ADD_CLAUSE_REGULAR, addNewClauses(), atom_, HashArray< Type, HashFn, EqualFn >::find(), fixedAtom_, getActiveClauses(), getBlockIndex(), Domain::getBlockSize(), Domain::getDB(), Domain::getPredInBlock(), gndPredHashArray_, isActive(), Database::setActiveStatus(), setValueOfAtom(), updateMakeBreakCostAfterFlip(), updateSatisfiedClauses(), and useThreshold_.

Referenced by activateAtom().

02452   {
02453     assert(atomIdx > 0);
02454     if (hvsdebug)
02455     {
02456       cout << "Fixing ";
02457       (*gndPreds_)[atomIdx - 1]->print(cout, domain_);
02458       cout << " to " << value << endl;    
02459     }
02460 
02461       // Must be in mc-sat
02462     if (!useThreshold_)
02463     {
02464       cout << ">>> [ERR] useThreshold_ is false" << endl;
02465       exit(0);
02466     }
02467 
02468       // If already fixed to opp. sense, then contradiction
02469     if ((fixedAtom_[atomIdx] == 1 && value == false) ||
02470         (fixedAtom_[atomIdx] == -1 && value == true))
02471     {
02472       cout << "Contradiction: Tried to fix atom " << atomIdx <<
02473       " to true and false ... exiting." << endl;
02474       exit(0);
02475     }
02476 
02477       // already fixed
02478     if (fixedAtom_[atomIdx] != 0) return;
02479 
02480     fixedAtom_[atomIdx] = (value) ? 1 : -1; 
02481     if (atom_[atomIdx] != value) 
02482     {
02483       bool activate = false;
02484       int blockIdx =  getBlockIndex(atomIdx - 1);
02485       setValueOfAtom(atomIdx, value, activate, blockIdx);
02486       updateMakeBreakCostAfterFlip(atomIdx);
02487     }
02488     
02489       // update isSat
02490     updateSatisfiedClauses(atomIdx);
02491 
02492       // If in a block and fixing to true, fix all others to false
02493     if (value)
02494     {
02495       int blockIdx = getBlockIndex(atomIdx - 1);
02496       if (blockIdx > -1)
02497       {
02498         int blockSize = domain_->getBlockSize(blockIdx);
02499         for (int i = 0; i < blockSize; i++)
02500         {
02501           const Predicate* pred = domain_->getPredInBlock(i, blockIdx);
02502           GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);      
02503           int idx = gndPredHashArray_.find(gndPred);
02504           delete gndPred;
02505           delete pred;
02506       
02507             // Pred already present: check that it's not fixed
02508           if (idx >= 0)
02509           {
02510               // Atom not the one specified
02511             if (idx != (atomIdx - 1))
02512             {
02513                 // If already fixed to true, then contradiction
02514               if (fixedAtom_[idx + 1] == 1)
02515               {
02516                 cout << "Contradiction: Tried to fix atom " << idx + 1 <<
02517                 " to true and false ... exiting." << endl;
02518                 exit(0);
02519               }
02520                 // already fixed
02521               if (fixedAtom_[idx + 1] == -1) continue;
02522               if (hvsdebug)
02523               {
02524                 cout << "Fixing ";
02525                 (*gndPreds_)[idx]->print(cout, domain_);
02526                 cout << " to 0" << endl;
02527               }
02528               fixedAtom_[idx + 1] = -1; 
02529               if (atom_[idx + 1] != false) 
02530               {
02531                 bool activate = false;
02532                 setValueOfAtom(idx + 1, value, activate, blockIdx);
02533                 updateMakeBreakCostAfterFlip(idx + 1);
02534               }
02535                 // update isSat
02536               updateSatisfiedClauses(idx + 1);
02537             }
02538           }
02539         }
02540       }
02541     }
02542 
02543       // activate clauses falsified
02544       // need to updateMakeBreakCost for new clauses only, which aren't sat
02545     if (lazy_ && !isActive(atomIdx) && value)
02546     {
02547         // if inactive fixed to true, need to activate falsified
02548         // inactive clauses gather active clauses
02549       Predicate* p =
02550         gndPredHashArray_[atomIdx - 1]->createEquivalentPredicate(domain_);
02551         
02552       bool ignoreActivePreds = false; // only get currently unsat ones
02553       Array<GroundClause*> unsatClauses;
02554       getActiveClauses(p, unsatClauses, true, ignoreActivePreds);       
02555         
02556         // filter out clauses already added (can also add directly, but
02557         // will elicit warning)
02558       addNewClauses(ADD_CLAUSE_REGULAR, unsatClauses);
02559 
02560         // Set active status in db
02561       domain_->getDB()->setActiveStatus(p, true);
02562       activeAtoms_++;
02563 
02564       delete p;
02565     }
02566   }

Array<int>* HVariableState::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 2613 of file hvariablestate.h.

References Array< Type >::append(), clause_, clauseCost_, Array< Type >::clear(), fixedAtom_, getClauseSize(), and isSatisfied_.

02614         {
02615                 Array<int>* returnArray = new Array<int>;
02616                 // If already satisfied from fixed atoms, then return empty array
02617                 if (isSatisfied_[clauseIdx]) return returnArray;
02618 
02619                 // Keeps track of pos. clause being satisfied or 
02620                 // neg. clause being unsatisfied due to fixed atoms
02621                 bool isGood = (clauseCost_[clauseIdx] > 0) ? false : true;
02622                 // Keeps track of all atoms being fixed to false in a pos. clause
02623                 bool allFalseAtoms = (clauseCost_[clauseIdx] > 0) ? true : false;
02624                 // Check each literal in clause
02625                 for (int i = 0; i < getClauseSize(clauseIdx); i++)
02626                 {
02627                         int lit = clause_[clauseIdx][i];
02628                         int fixedValue = fixedAtom_[abs(lit)];
02629 
02630                         if (clauseCost_[clauseIdx] > 0)
02631                         { // Pos. clause: check if clause is satisfied
02632                                 if ((fixedValue == 1 && lit > 0) ||
02633                                         (fixedValue == -1 && lit < 0))
02634                                 { // True fixed lit
02635                                         isGood = true;
02636                                         allFalseAtoms = false;
02637                                         returnArray->clear();
02638                                         break;
02639                                 }
02640                                 else if (fixedValue == 0)
02641                                 { // Lit not fixed
02642                                         allFalseAtoms = false;
02643                                         returnArray->append(lit);
02644                                 }
02645                         }
02646                         else
02647                         { // Neg. clause:
02648                                 assert(clauseCost_[clauseIdx] < 0);
02649                                 if ((fixedValue == 1 && lit > 0) ||
02650                                         (fixedValue == -1 && lit < 0))
02651                                 { // True fixed lit
02652                                         cout << "Contradiction: Tried to fix atom " << abs(lit) <<
02653                                                 " to true in a negative clause ... exiting." << endl;
02654                                         exit(0);
02655                                 }
02656                                 else
02657                                 { // False fixed lit or non-fixed lit
02658                                         returnArray->append(lit);
02659                                         // Non-fixed lit
02660                                         if (fixedValue == 0) isGood = false;          
02661                                 }
02662                         }
02663                 }
02664                 if (allFalseAtoms)
02665                 {
02666                         cout << "Contradiction: All atoms in clause " << clauseIdx <<
02667                                 " fixed to false ... exiting." << endl;
02668                         exit(0);
02669                 }
02670                 if (isGood) isSatisfied_[clauseIdx] = true;
02671                 return returnArray;
02672         }

const bool HVariableState::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 2680 of file hvariablestate.h.

References deadClause_.

02681         {
02682                 return deadClause_[clauseIdx];
02683         }

void HVariableState::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 2725 of file hvariablestate.h.

References clauseGoodInPrevious(), deadClause_, getNumClauses(), gndClauses_, gndPredHashArray_, initMakeBreakCostWatch(), initMakeBreakCostWatchCont(), and threshold_.

Referenced by addNewClauses().

02726         {
02727                 for (int i = startClause; i < getNumClauses(); i++)
02728                 {
02729                         GroundClause* clause = (*gndClauses_)[i];
02730                         if ((clauseGoodInPrevious(i)) &&
02731                                 (clause->isHardClause() || random() <= threshold_[i]))
02732                         {
02733                                 if (hvsdebug)
02734                                 {
02735                                         cout << "Keeping clause "<< i << " ";
02736                                         clause->print(cout, domain_, &gndPredHashArray_);
02737                                         cout << endl;
02738                                 }
02739                                 deadClause_[i] = false;
02740                         }
02741                         else
02742                         {
02743                                 deadClause_[i] = true;
02744                         }
02745                 }
02746 
02747                 if(startClause == 0)
02748                 {
02749                         initMakeBreakCostWatch();
02750                 }
02751                 else
02752                 {
02753                         initMakeBreakCostWatch(startClause);
02754                 }
02755 
02756                 initMakeBreakCostWatchCont();
02757         }

const bool HVariableState::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 2767 of file hvariablestate.h.

References clauseCost_, and numTrueLits_.

Referenced by killClauses().

02768         {
02769                 //GroundClause* clause = (*gndClauses_)[clauseIdx];
02770                 int numSatLits = numTrueLits_[clauseIdx];
02771                 // Num. of satisfied lits in previous iteration is stored in clause
02772                 if ((numSatLits > 0 && clauseCost_[clauseIdx] > 0.0) ||
02773                         (numSatLits == 0 && clauseCost_[clauseIdx] < 0.0))
02774                         return true;
02775                 else
02776                         return false;
02777         }

void HVariableState::printLowState ( ostream & out ) [inline]

Prints the best state found to a stream.

Parameters:

out

Stream to which the state is printed.

Definition at line 2825 of file hvariablestate.h.

References getNumAtoms(), gndPreds_, and lowAtom_.

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

02826         {
02827                 for (int i = 0; i < getNumAtoms(); i++)
02828                 {
02829                         (*gndPreds_)[i]->print(out, domain_);
02830                         out << " " << lowAtom_[i + 1] << endl;
02831                 }
02832         }

void HVariableState::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 2841 of file hvariablestate.h.

Referenced by MCMC::printTruePredsH().

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

GroundPredicate* HVariableState::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 2854 of file hvariablestate.h.

References gndPreds_.

Referenced by MCMC::getProbabilityOfPredH(), and HMCSAT::infer().

02855         {
02856                 return (*gndPreds_)[index];
02857         }

GroundClause* HVariableState::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 2865 of file hvariablestate.h.

References gndClauses_.

Referenced by printDisClause(), printFalseClauses(), and MCMC::updateWtsForGndPredsH().

02866         {
02867                 return (*gndClauses_)[index];
02868         }

const int HVariableState::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 2907 of file hvariablestate.h.

References Array< Type >::find(), and gndPreds_.

Referenced by MCMC::getProbabilityH().

02908         {
02909                 return gndPreds_->find(gndPred);
02910         }

void HVariableState::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 2929 of file hvariablestate.h.

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

Referenced by activateAtom(), fixAtom(), getActiveClauses(), and HVariableState().

02933   {
02934     Timer timer;
02935     double currTime;
02936 
02937     Clause *fclause;
02938     GroundClause* newClause;
02939     int clauseCnt;
02940     GroundClauseHashArray clauseHashArray;
02941 
02942     Array<GroundClause*>* newClauses = new Array<GroundClause*>; 
02943   
02944     const Array<IndexClause*>* indexClauses = NULL;
02945       
02946       // inputPred is null: all active clauses should be retrieved
02947     if (inputPred == NULL)
02948     {
02949       clauseCnt = mln_->getNumClauses();
02950     }
02951       // Otherwise, look at all first order clauses containing the pred
02952     else
02953     {
02954       if (domain_->getDB()->getDeactivatedStatus(inputPred)) return;
02955       int predId = inputPred->getId();
02956       indexClauses = mln_->getClausesContainingPred(predId);
02957       clauseCnt = indexClauses->size();
02958     }
02959 
02960       // Look at each first-order clause and get active groundings
02961     int clauseno = 0;
02962 
02963     while (clauseno < clauseCnt)
02964     {
02965       if (inputPred)
02966         fclause = (Clause *) (*indexClauses)[clauseno]->clause;           
02967       else
02968         fclause = (Clause *) mln_->getClause(clauseno);
02969 
02970       if (hvsdebug)
02971       {
02972         cout << "Getting active clauses for FO clause: ";
02973         fclause->print(cout, domain_);
02974         cout << endl;
02975       }
02976 
02977       currTime = timer.time();
02978 
02979       const double* parentWtPtr = NULL;
02980       if (!fclause->isHardClause()) parentWtPtr = fclause->getWtPtr();
02981       const int clauseId = mln_->findClauseIdx(fclause);
02982       newClauses->clear();
02983 
02984       if (stillActivating_)
02985         stillActivating_ = fclause->getActiveClauses(inputPred, domain_,
02986                                                      newClauses,
02987                                                      &gndPredHashArray_,
02988                                                      ignoreActivePreds);
02989 
02990       for (int i = 0; i < newClauses->size(); i++)
02991       {
02992         long double wt = fclause->getWt();
02993         newClause = (*newClauses)[i];
02994 
02995           // If already active, ignore; assume all gndClauses_ are active
02996         if (gndClauses_->find(newClause) >= 0)
02997         {
02998           delete newClause;
02999           continue;
03000         }
03001 
03002         bool invertWt = false;
03003           // We want to normalize soft unit clauses to all be positives
03004         if (!fclause->isHardClause() &&
03005             newClause->getNumGroundPredicates() == 1 &&
03006             !newClause->getGroundPredicateSense(0))
03007         {
03008           newClause->setGroundPredicateSense(0, true);
03009           newClause->setWt(-newClause->getWt());
03010           wt = -wt;
03011           invertWt = true;
03012           int addToIndex = gndClauses_->find(newClause);
03013           if (addToIndex >= 0)
03014           {
03015             (*gndClauses_)[addToIndex]->addWt(wt);
03016             if (parentWtPtr)
03017               (*gndClauses_)[addToIndex]->incrementClauseFrequency(clauseId, 1,
03018                                                                    invertWt);
03019             delete newClause;
03020             continue;
03021           }
03022         }
03023         
03024         int pos = clauseHashArray.find(newClause);
03025           // If clause already present, then just add weight
03026         if (pos >= 0)
03027         {
03028             // Check if already added from this f.o. clause. If so, don't add
03029             // again
03030           if (clauseHashArray[pos]->getClauseFrequency(clauseId) > 0)
03031           {
03032             delete newClause;
03033             continue;
03034           }
03035           if (hvsdebug)
03036           {
03037             cout << "Adding weight " << wt << " to clause ";
03038             clauseHashArray[pos]->print(cout, domain_, &gndPredHashArray_);
03039             cout << endl;
03040           }
03041           clauseHashArray[pos]->addWt(wt);
03042           if (parentWtPtr)
03043             clauseHashArray[pos]->incrementClauseFrequency(clauseId, 1,
03044                                                            invertWt);
03045           delete newClause;
03046           continue;
03047         }
03048 
03049           // If here, then clause is not yet present        
03050         newClause->setWt(wt);
03051         if (parentWtPtr)
03052           newClause->incrementClauseFrequency(clauseId, 1, invertWt);
03053 
03054         if (hvsdebug)
03055         {
03056           cout << "Appending clause ";
03057           newClause->print(cout, domain_, &gndPredHashArray_);
03058           cout << endl;
03059         }
03060         clauseHashArray.append(newClause);
03061       }
03062       clauseno++; 
03063 
03064     } //while (clauseno < clauseCnt)
03065 
03066     for (int i = 0; i < clauseHashArray.size(); i++)
03067     {
03068       newClause = clauseHashArray[i];
03069       activeClauses.append(newClause);
03070     }
03071 
03072     newClauses->clear();
03073     delete newClauses;
03074 
03075     clauseHashArray.clear();
03076   }

void HVariableState::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 3085 of file hvariablestate.h.

References getActiveClauses().

03087         {
03088                 getActiveClauses(NULL, allClauses, true, ignoreActivePreds);
03089         }

int HVariableState::getIndexOfRandomAtom ( ) [inline]

Returns the absolutionute index of a random atom.

could be discrete or continuous. If the picked atom is discrete, the return value is its index in the atom_ variable. If the picked atom is continuous, the return value is -1 * index.

Definition at line 3322 of file hvariablestate.h.

References getNumAtoms(), and totalAtomNum_.

Referenced by HMaxWalkSat::pickSA(), and HMaxWalkSat::pickSS().

03323         {
03324                 assert(totalAtomNum_ > 0);
03325                 int discreteNumAtoms = getNumAtoms();
03326                 int idx = random()%totalAtomNum_;
03327                 if (idx < discreteNumAtoms)
03328                 {
03329                         return (idx + 1);
03330                 }
03331                 else
03332                 {
03333                         return -(idx - discreteNumAtoms + 1);
03334                 }
03335         }

int HVariableState::getRandomToFixClauseIdx ( ) [inline]

Returns the index of a clause that has the potential to be optimized, i.e., a false discrete clause or a hybird clause (we assume each hybrid clause is optimizable at any time.

) Used in hybrid MaxWalkSAT. If the picked clause is discrete, the return value is its index. If the picked atom is continuous, the return value is -1 * index.

Definition at line 3342 of file hvariablestate.h.

References falseClause_, and hybridClauseNum_.

03343         {
03344                 int idx = random() % (numFalseClauses_ + hybridClauseNum_);
03345 
03346                 if (idx < numFalseClauses_)
03347                         return falseClause_[idx];
03348                 else return -(idx - numFalseClauses_);
03349         }

long double HVariableState::getImprovementByFlippingDisHMCS ( 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.

Parameters:

atomIdx

Index of atom to flip.

Returns:: Improvement achieved by flipping the atom.

Definition at line 3583 of file hvariablestate.h.

References breakCost_, getDisImproveInHybridByFlippingMCSAT(), and makeCost_.

Referenced by HMaxWalkSat::calculateImprovementDisHMCS().

03583         {
03584                 if (hvsdebug) {
03585                         cout << "Entering HVariableState::getImprovementByFlippingDisHMCS" << endl;
03586                 }
03587                 assert(atomIdx > 0);
03588                 // This is the improvement from discrete clauses
03589                 long double improvementDis = makeCost_[atomIdx] - breakCost_[atomIdx];
03590                 double improvementHybrid = getDisImproveInHybridByFlippingMCSAT(atomIdx);
03591                 if (hvsdebug) {
03592                         cout << "Leaving HVariableState::getImprovementByFlippingDisHMCS" << endl;
03593                 }
03594                 return improvementDis + improvementHybrid;
03595         }
03596

void HVariableState::makeUnitCosts ( ) [inline]

Turns all costs into units.

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

Definition at line 3891 of file hvariablestate.h.

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

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

03891         {
03892                 for (int i = 0; i < clauseCost_.size(); i++)
03893                 {
03894                         // All hard clauses would have weight 1.0 .
03895                         if (clauseCost_[i] > 0) clauseCost_[i] = 1.0;
03896                         else {
03897                                 assert(clauseCost_[i] < 0);
03898                                 clauseCost_[i] = -1.0;
03899                         }
03900                 }
03901 
03902                 for(int i = 0; i < hybridClauseCost_.size(); i++)
03903                 {
03904                         if (hybridClauseCost_[i] > 0) hybridClauseCost_[i] = 1.0;
03905                         else
03906                         {
03907                                 assert(hybridClauseCost_[i] < 0);
03908                                 hybridClauseCost_[i] = -1.0;
03909                         }
03910                 }
03911         }
03912

void HVariableState::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 4457 of file hvariablestate.h.

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

04459   {
04460     // TODO: lazy version
04461     assert(unknownPred->size() == getNumAtoms());
04462     IntBoolPairItr itr;
04463     IntBoolPair *clauseFrequencies;
04464     
04465     for (int clauseno = 0; clauseno < clauseCnt; clauseno++)
04466       numGndings[clauseno] = 0;
04467     
04468     for (int i = 0; i < gndClauses_->size(); i++)
04469     {
04470       GroundClause *gndClause = (*gndClauses_)[i];
04471       int satLitcnt = 0;
04472       bool unknown = false;
04473       for (int j = 0; j < gndClause->getNumGroundPredicates(); j++)
04474       {
04475         int lit = gndClause->getGroundPredicateIndex(j);
04476         if ((*unknownPred)[abs(lit) - 1])
04477         {
04478           unknown = true;
04479           continue;
04480         }
04481         if (isTrueLiteral(lit)) satLitcnt++;
04482       }
04483 
04484       clauseFrequencies = gndClause->getClauseFrequencies();
04485       for (itr = clauseFrequencies->begin();
04486            itr != clauseFrequencies->end(); itr++)
04487       {
04488         int clauseno = itr->first;
04489         int frequency = itr->second.first;
04490         bool invertWt = itr->second.second;
04491           // If flipped unit clause, then we want opposite kind of grounding
04492         if (invertWt)
04493         {
04494             // Want true and is true or unknown => don't count it
04495           if (tv && (satLitcnt > 0 || unknown))
04496             continue;
04497             // Want false and is false => don't count it
04498           if (!tv && satLitcnt == 0)
04499             continue;
04500         }
04501         else
04502         {
04503             // Want true and is false => don't count it
04504           if (tv && satLitcnt == 0)
04505             continue;
04506             // Want false and is true => don't count it
04507           if (!tv && (satLitcnt > 0 || unknown))
04508             continue;
04509         }
04510         numGndings[clauseno] += frequency;
04511       }
04512     }
04513   }
04514

HVariableState Class Reference

Public Member Functions

Public Attributes

Static Public Attributes

Classes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation


Public Member Functions
	HVariableState (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 HVariableState.
	~HVariableState ()
	Destructor.
void	addNewClauses (bool initial)
	New clauses are added to the state.
void	addNewClauses (int addType, Array< GroundClause * > &clauses)
	Adds new clauses to the state.
void	init ()
	Information about the state is reset and initialized.
void	initLowState ()
void	setInitFromEvi (bool bInitFromEvi)
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 ()
	Initialize makeCost and breakCost and watch arrays based on the current variable assignment.
void	printDisAtom (int atomIdx, ostream &os)
void	printDisClause (int i, ostream &os)
void	initMakeBreakCostWatch (const int &startClause)
int	getNumAtoms ()
int	getNumClauses ()
int	getNumDeadClauses ()
int	getIndexOfAtomInRandomFalseClause ()
	Returns the absolutionute index of a random atom in a random unsatisfied pos.
int	getRandomFalseClauseIndex ()
	Returns the index of a random unsatisfied pos.
int	getNumFalseClauses ()
	Returns the number of the unsatisfied positive and satisfied negative clauses.
long double	getCostOfFalseClauses ()
	Returns the cost of the unsatisfied positive and satisfied negative clauses.
const double	getMaxClauseWeight ()
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, const bool &activate, const int &blockIdx)
	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, const int &blockIdx)
	Flip the truth value of an atom and update info arrays.
void	flipAtomValue (const int &atomIdx, const int &blockIdx)
	Flips the truth value of an atom.
bool	activateAtom (const int &atomIdx, const bool &ignoreActivePreds, const bool &groundOnly)
	If in lazy mode, an atom is activated and all clauses activated by this atom are added to the state.
void	setInferenceMode (int mode)
	Set the inference mode currently being used.
void	updateSatisfiedClauses (const int &toFix)
	Updates isSatisfiedClause after an atom is fixed.
void	updateMakeBreakCostAfterFlip (const int &toFlip)
	Updates cost after flip.
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	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 absolutionute index of the nth atom in a clause.
const int	getRandomAtomInClause (const int &clauseIdx)
	Retrieves the absolutionute 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 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	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	saveLowState ()
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	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	updateNumTrueLits ()
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	resetDeadClausesAndInitMake ()
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	initLazyBlocks ()
	Initializes the block structures for the lazy version.
void	printHybridConstraint (int i, ostream &os)
void	WriteGndPredIdxMap (const char *gnd_pred_map_file)
void	initMakeBreakCostWatchCont ()
int	getNumContAtoms ()
int	getIndexOfRandomAtom ()
	Returns the absolutionute index of a random atom.
int	getRandomToFixClauseIdx ()
	Returns the index of a clause that has the potential to be optimized, i.e., a false discrete clause or a hybird clause (we assume each hybrid clause is optimizable at any time.
double	getCostOfTotalFalseConstraints ()
double	getCostOfAllClauses (double &discost, double &hybridcost)
void	UpdateHybridClauseWeightSumByContAtom (const int &atomIdx, const double &atomValue)
void	UpdateHybridClauseWeightSumByDisAtom (const int &atomIdx, bool atomValue)
void	UpdateHybridClauseInfoByContAtom (const int &atomIdx, const double &atomValue)
void	UpdateHybridClauseInfoByDisAtom (const int &atomIdx, const bool &atomValue)
void	UpdateHybridClause (const int &contClauseIdx)
long double	getImprovementRandomMoveCont (const int &atomIdx, const double &atomValue)
long double	getImprovementInWeightSumByFlipping (const int &atomIdx)
double	SolveConstraintAndRandomSample (const int &contClauseIdx, const int &inIdx)
long double	getImprovementByFlippingDisHMCS (const int &atomIdx)
	Calculates the improvement achieved by flipping an atom.
double	getDisImproveInHybridByFlippingMCSAT (const int &atomIdx)
double	SolveHybridConstraintToContVarSample (int contClauseIdx, int inIdx, int maxIter=100)
double	GetImprovementBySolvingHybridConstraintToContVar (const int &contClauseIdx, const int &inIdx, double &cont_var_val)
bool	isConstraintSolvableByCont (const int &contClauseIdx)
int	getRandomFalseClauseIndexHMCS ()
double	GetImprovementByMovingContVar (const int &atomIdx, double &vContAtomFlipped)
void	addFalseHybridConstraint (const int &contClauseIdx)
void	removeFalseHybridConstraint (const int &contClauseIdx)
void	UpdateHybridConstraintTh ()
void	addFalseClause (const int &clauseIdx)
void	removeFalseClause (const int &clauseIdx)
	Unmarks a clause as false in the state.
void	makeUnitCosts ()
	Turns all costs into units.
void	optimizeIndividualNumTerm ()
double	ReduceClauseAndOptimize (const Array< int > &contVarIdx, Array< double > &assign)
double	ReduceClauseAndOptimize (const int &contVarIdx, double *assign)
double	OptimizeHybridClauseToContVar (int clause_idx, int cont_var_inIdx)
long double	getImprovementByFlippingDisHMWS (const int &atomIdx)
double	getDisImproveInHybridByFlippingHMWS (const int &atomIdx)
int	getRandomFalseClauseIndexHMWS ()
double	getContVarValueByRandomMove (const int &atomIdx)
Array< int > &	getContDisOccurenceArray (const int &idx)
Array< int > &	getContContOccurenceArray (const int &idx)
const double	getMaxClauseWeightTotal ()
	Marks a clause as false in the state.
const long double	getLowCostAll ()
	Returns the cost of bad clauses in the optimum state.
const int	getLowBadAll ()
	Returns the number of bad clauses in the optimum state.
const long double	getLowCostCont ()
const int	getLowBadCont ()
	Returns the number of bad clauses in the optimum state.
void	printFalseClauses (ostream &os)
void	saveLowToCurrentAll ()
void	saveLowToCurrentDis ()
void	saveLowToCurrentCont ()
void	saveLowStateAll ()
void	saveLowStateCont ()
void	saveCurrentAsLastAssignment ()
	Save current assignment as an optimum state.
void	saveLastAsCurrentAssignment ()
void	updateCost ()
void	getContClauseGndings (Array< double > *const &numGndings)
void	getContClauseGndingsWithUnknown (double numGndings[], int contClauseCnt, const Array< bool > *const &unknownPred)
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	printLowStateCont (ostream &os)
	Gets the number of (true or false) clause groundings in this state.
void	printLowStateAll (ostream &os)
void	recordAtomMakeDisClauseFalse (int clauseIdx, Array< int > *record)
void	recordAtomMakeDisClauseTrue (int clauseIdx, Array< int > *record)
double	HybridClauseValueNonWt (int contClauseIdx)
double	HybridClauseValue (int contClauseIdx, bool &dis, double &cont)
double	HybridClauseValue (int contClauseIdx)
double	HybridClauseContPartValue (int contClauseIdx)
bool	HybridClauseDisPartValue (int contClauseIdx)
PolyNomial &	GetHybridClausePolynomial (int contClauseIdx)
bool	isSatisfied (int iContClauseIdx)
bool	isSatisfied (const HybridConstraint &cst, double currentValue)
bool	CheckIfLBFGSCacheSatisfied (int contClauseIdx)
bool	isSatisfied (const HybridConstraint &cst)
void	LoadDisPartAtoms (const string &str, Array< int > &arDis, map< string, int > &gndPredCont, const int &clauseIdx)
void	LoadContPartAtoms (const string &str, Array< int > &arDis)
void	printContAtom (int conAtomIdx, ostream &os)
void	printContAtoms (ostream &os)
void	PrintDisAtoms (ostream &os)
void	PrintContPartMLN (ostream &os)
void	printContOccurrence (ostream &os)
void	buildContOccurrence ()
void	setDisVarValueFromEvi ()
void	setContVarValueFromEvi ()
void	LoadDisEviValuesFromRst (const char *szDisEvi)
void	LoadDisEviValues (const char *szDisEvi)
void	LoadContEviValues (const char *szContEvi)
void	LoadContGroundedMLN (const char *szContFile)
int	getNumContFormulas ()
void	initRange ()
double	randomSampleRange (const DoubleRange &r)
double	computeMaxValue (PolyNomial &pl, int contClauseIdx, int i)
void	setProposalStdev (const char *szStdev)
void	proceedOneStepAndCache (int contClauseIdx, PolyNomial &pl)
bool	SolveContByLBFGS (int contClauseIdx, int maxIter)
void	initContinuousVariableRandom ()
Public Attributes
Array< GroundPredicate * > *	gndPreds_
Array< GroundClause * > *	gndClauses_
GroundPredicateHashArray *	unePreds_
GroundPredicateHashArray *	knePreds_
Array< TruthValue > *	knePredValues_
Array< GroundClause * >	newClauses_
Array< GroundPredicate * >	newPreds_
GroundPredicateHashArray	gndPredHashArray_
Array< Array< int > >	clause_
Array< long double >	clauseCost_
Array< int >	falseClause_
Array< int >	falseClauseLow_
Array< int >	whereFalse_
Array< int >	numTrueLits_
Array< int >	watch1_
Array< int >	watch2_
Array< bool >	isSatisfied_
Array< bool >	deadClause_
bool	useThreshold_
Array< long double >	threshold_
Array< Array< int > >	occurence_
Array< long double >	makeCost_
Array< long double >	breakCost_
Array< int >	fixedAtom_
Array< bool >	lowAtom_
long double	lowCost_
Array< bool >	atom_
bool	bInitFromEvi_
Array< bool >	atomEvi_
Array< bool >	atomsLast_
Array< LBFGSP * >	contsolvers_
Array< HybridConstraint >	hybridConstraints_
Array< PolyNomial >	hybridPls_
Array< double >	hybridWts_
map< int, double >	contOptimum_
map< int, Array< double > >	contOptimumAssignment_
Array< double >	contAtomsLast_
Array< double >	contAtoms_
Array< double >	contAtomsBackup_
Array< double >	contAtomsEvi_
Array< double >	contAtomsLow_
double	lowCostHybrid_
int	lowBadHybrid_
Array< Array< int > >	hybridDisClause_
Array< Array< int > >	hybridContClause_
Array< Array< int > >	hybridDisOccurrence_
Array< Array< int > >	hybridContOccurrence_
Array< DoubleRange >	contAtomRange_
Array< bool >	hybridConjunctionDisjunction_
Array< double >	hybridClauseCost_
Array< int >	hybridGndClauseToFormulaMap_
Array< Array< int > >	hybridFormulaGndClauseIdx_
int	hybridFormulaNum_
int	hybridClauseNum_
int	contAtomNum_
int	totalAtomNum_
int	totalFalseConstraintNum_
int	hybridFalseConstraintNum_
Array< int >	hybridFalseClause_
Array< int >	hybridFalseClauseLow_
Array< int >	hybridWhereFalse_
Array< double >	hybridClauseValue_
Array< bool >	hybridClauseDisValue_
map< string,int >	gndPredCont_
map< int, string >	gndPredReverseCont_
double	costOfTotalFalseConstraints_
int	lowBadAll_
double	lowCostAll_
double	costHybridFalseConstraint_
bool	bMaxOnly_
Array< double >	proposalStdev_
map< string, int >	gndPredDis_
double	weightSumDis_
double	weightSumCont_
Array< Array< double > >	lbfgsCache_
Array< double >	hmwsContOptimal_
Array< bool >	hmwsDisOptimal_
string	strHybridDis_
Static Public Attributes
static const int	MODE_MWS = 0
static const int	MODE_HARD = 1
static const int	MODE_SAMPLESAT = 2
static const int	ADD_CLAUSE_INITIAL = 0
static const int	ADD_CLAUSE_REGULAR = 1
static const int	ADD_CLAUSE_DEAD = 2
static const int	ADD_CLAUSE_SAT = 3
Classes
struct	HybridConstraint
	Fills the blocks with the predicates in the domain blocks. More...