edu::tum::cs::logic::sat::weighted::MaxWalkSAT Class Reference

Inheritance diagram for edu::tum::cs::logic::sat::weighted::MaxWalkSAT:

Classes
class	Constraint
class	WeightedClause
Public Member Functions
PossibleWorld	getBestState ()
double	getP ()
PossibleWorld	getState ()
int	getStep ()
	MaxWalkSAT (WeightedClausalKB kb, PossibleWorld state, WorldVariables vars, Database evidence) throws Exception
void	printBestState (PrintStream fr)
void	printunsCons ()
void	run ()
void	setDeltaCostCalcMethod (int deltaCostCalcMethod)
void	setMaxSteps (int steps)
void	setP (double p)
Public Attributes
int	step
Protected Member Functions
void	addBottleneck (GroundAtom ga, Constraint c)
void	addGAOccurrence (GroundAtom ga, Constraint c)
void	addUnsatisfiedConstraint (Constraint c)
double	deltaCost (GroundAtom gndAtom)
double	deltaCostConAndForm (GroundAtom gndAtom)
double	deltaCostFormula (GroundAtom gndAtom)
void	flipGndAtom (GroundAtom gndAtom)
void	initFormulaState ()
Vector< Object >	pickAndFlipVar (Collection< GroundAtom > candidates)
Constraint	randomlyChosen ()
void	SAMove ()
void	setState ()
void	unsatisfiedSum ()
void	walkSATMove ()
Protected Attributes
PossibleWorld	bestState
HashMap< Integer, Vector < Constraint > >	bottlenecks
HashMap< WeightedClause, Formula >	cl2Formula
HashMap < edu.tum.cs.logic.sat.weighted.WeightedClause, Formula >	clFormula
int	countUnsCon
int	deltaCostCalcMethod = 1
HashMap< Integer, Boolean >	evidence
EvidenceHandler	evidenceHandler
int	flips
HashMap< Formula, HashSet < WeightedClause > >	formula2clauses
HashMap< Formula, HashSet < WeightedClause > >	formula2satClause
HashMap< Formula, Double >	formula2weight
HashMap< Integer, Vector < Constraint > >	GAOccurrences
int	greedyMoves
int	lastMinStep
int	maxSteps = 1000
Vector< Integer >	nonEvidenceGndAtomIndices
double	p = 0.999
Random	rand
int	SAMoves
PossibleWorld	state
Vector< Constraint >	unsatisfiedConstraints
double	unsSum
double	unsSumBeta
WorldVariables	vars
final boolean	verbose = false
Package Attributes
double	minSum

Detailed Description

Implementation of a stochastic weighted Maximum-a-posteriori WalkSAT algorithm

Author:: wernicke

Definition at line 29 of file logic/sat/weighted/MaxWalkSAT.java.

Constructor & Destructor Documentation

edu::tum::cs::logic::sat::weighted::MaxWalkSAT::MaxWalkSAT	(	WeightedClausalKB	kb,
		PossibleWorld	state,
		WorldVariables	vars,
		Database	evidence
	)			throws Exception `[inline]`

Constructor to instantiate an object of MAPMaxWalkSAT

Parameters:

	kb	a knowledge base of weighted clauses, which can be instantiated by an Markov Random Field (MRF)
	state	a possible world containing all variables of the Markov Logic Network (MLN)
	vars	world variables of the MLN which is needed by the class
	evidence	an evidence database

Exceptions:

java.lang.Exception

Definition at line 71 of file logic/sat/weighted/MaxWalkSAT.java.

Member Function Documentation

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::addBottleneck	(	GroundAtom	ga,
		Constraint	c
	)			`[inline, protected]`

Method adds a groundatom into a vector of bottlenecks for a given constraint (bottlenecks(=groundatoms) are responsible for the negative change of value of a constraint)

Parameters:

	ga	groundatom to be added to the bottlenecks
	c	constraint for which the groundatom a is a bottleneck

Definition at line 134 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::addGAOccurrence	(	GroundAtom	ga,
		Constraint	c
	)			`[inline, protected]`

Method adds a groundatom into a vector of containing groundatom of a constraint

Parameters:

	ga	groundatom to be added to the occurence of a constraint
	c	constraint in which the groundatom occurs

Definition at line 148 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::addUnsatisfiedConstraint ( Constraint c ) [inline, protected]

Method adds a constraint into unsatisfiedConstraints (Vector<Constraint>)

Parameters:

c

constraint which should be added

Definition at line 125 of file logic/sat/weighted/MaxWalkSAT.java.

double edu::tum::cs::logic::sat::weighted::MaxWalkSAT::deltaCost ( GroundAtom gndAtom ) [inline, protected]

Calculation of the deltacosts per groundatom depending on the weight of the formula devided by its count of constraints. Returns a double value.

Parameters:

gndAtom

groundatom to calculate

Returns:: returns a double value of added weights

Definition at line 495 of file logic/sat/weighted/MaxWalkSAT.java.

double edu::tum::cs::logic::sat::weighted::MaxWalkSAT::deltaCostConAndForm ( GroundAtom gndAtom ) [inline, protected]

Calculation of deltacosts per groundatom. If the value of the formula would changed through flipping the groundatom then the complete weight are the deltacosts else the weight is devided by the count of the constraints of the formula and returned as the deltacosts. Returns a double value.

Parameters:

gndAtom

groundatom to calculate

Returns:: returns a double value of added weights

Definition at line 550 of file logic/sat/weighted/MaxWalkSAT.java.

double edu::tum::cs::logic::sat::weighted::MaxWalkSAT::deltaCostFormula ( GroundAtom gndAtom ) [inline, protected]

Calcualtion of deltacosts per groundatom. Only if the value of the complete formula would be changed through flipping. the groundatom the complete weight of the formula is the deltacost of the groundatom. Returns a double value.

Parameters:

gndAtom

groundatom to calculate

Returns:: returns a double value of added weights

Definition at line 520 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::flipGndAtom ( GroundAtom gndAtom ) [inline, protected]

Method flips the given groundatom and refreshs the unsatisfied sum, the state of the constraint and the satisfied clauses of the according formula

Parameters:

gndAtom

groundatom to flip

Definition at line 456 of file logic/sat/weighted/MaxWalkSAT.java.

PossibleWorld edu::tum::cs::logic::sat::weighted::MaxWalkSAT::getBestState ( ) [inline]

Method returns an actual state of the algorithm in form of a boolean[].

Returns:: boolean[] (part of a possible world)

Definition at line 583 of file logic/sat/weighted/MaxWalkSAT.java.

double edu::tum::cs::logic::sat::weighted::MaxWalkSAT::getP ( ) [inline]

gets the probability of a greedy move

Returns:: parameter p

Definition at line 607 of file logic/sat/weighted/MaxWalkSAT.java.

PossibleWorld edu::tum::cs::logic::sat::weighted::MaxWalkSAT::getState ( ) [inline]

Returns the actual state of the algorithm

Returns:: PossibleWorld (actual state)

Definition at line 265 of file logic/sat/weighted/MaxWalkSAT.java.

int edu::tum::cs::logic::sat::weighted::MaxWalkSAT::getStep ( ) [inline]

Method returns an actual count of steps

Returns:: count of steps as integer value

Definition at line 591 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::initFormulaState ( ) [inline, protected]

Initial mapping of formulas to HashSet of containing satisfied clauses

Definition at line 180 of file logic/sat/weighted/MaxWalkSAT.java.

Vector<Object> edu::tum::cs::logic::sat::weighted::MaxWalkSAT::pickAndFlipVar ( Collection< GroundAtom > candidates ) [inline, protected]

Chooses the "best" groundatom among the given candidates (in relation to the overall unsatisfied sum)

Parameters:

candidates

a collection of groundatoms from which one should be flipped

Returns:: returns a vector of one or two (in case of a block) groundatoms in combination with a double value as representation of the effects to the state

Definition at line 375 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::printBestState ( PrintStream fr ) [inline]

prints the best state found by the algorithm

Definition at line 272 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::printunsCons ( ) [inline]

Method prints all unsatisfied constraints in combination with an according formula and afterwards the unsatisfied sum on the console

Definition at line 571 of file logic/sat/weighted/MaxWalkSAT.java.

Constraint edu::tum::cs::logic::sat::weighted::MaxWalkSAT::randomlyChosen ( ) [inline, protected]

Method randomly chooses a constraint among the unsatisfied constraints and returns it

Returns:: randomly chosen unsatisfied constraint

Definition at line 564 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::run ( ) [inline]

Method starts and controls the activities of the algorithm. In this case there will be executed a walkSatMove (greedyMove) with a property of 95% else the SAMove (random Move) will be executed.

Definition at line 197 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::SAMove ( ) [inline, protected]

Randomly chooses and flips a possible groundatom

Reimplemented in edu::tum::cs::logic::sat::weighted::MaxWalkSATRoom.

Definition at line 332 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::setDeltaCostCalcMethod ( int deltaCostCalcMethod ) [inline]

With this method one can set the method the daltacosts of a goriundatom are calculated. Possible values are: 1 - Calculation of deltacosts: Always 1/Count of constraints of the according formula 2 - Calculation of deltacosts: Only if value of formula was changed (then complete weight of the formula are the deltacosts of the groundatom) 3 - see 2, if no change of the value of the according formula was made then see 1

Parameters:

deltaCostCalcMethod

1, 2 or 3 (see above for details)

Definition at line 618 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::setMaxSteps ( int steps ) [inline]

Definition at line 117 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::setP ( double p ) [inline]

sets the probability of a greedy move

Parameters:

p

Definition at line 599 of file logic/sat/weighted/MaxWalkSAT.java.

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::setState ( ) [inline, protected]