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

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

[legend]

List of all members.

Public Member Functions
boolean	flipSatisfies (GroundAtom gndAtom)
double	getDelta ()
double	getDeltaFormula (boolean trueFlip)
Vector< GroundAtom >	getGAsOfConstraint ()
Vector< Object >	greedySatisfy ()
void	handleFlip (GroundAtom gndAtom)
void	initState ()
boolean	isHard ()
String	toString ()
	WeightedClause (GroundLiteral[] lits, boolean hard)
Public Attributes
boolean	hard
Protected Attributes
Vector< GroundAtom >	gndAtoms
GroundLiteral[]	lits
HashSet< GroundAtom >	trueOnes
double	weight

---

Detailed Description

A class used by MaxWalkSAT to administrate the weighted clauses of the Markov Logic Network.

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

---

Constructor & Destructor Documentation

edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::WeightedClause	(	GroundLiteral[]	lits,
		boolean	hard
	)			[inline]

Constructor to instantiate an weighted clause.

Parameters:

	lits	Groundliterals contained by the weighted clause.
	hard	Represents whether the clause is part of a hard formula, so it must be satisfied

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

---

Member Function Documentation

boolean edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::flipSatisfies

(

GroundAtom

gndAtom

)

[inline, virtual]

Method returns if a flip of the groundatom would satisfies the weighted clause. Else it is still satisfied.

Parameters:

gndAtom

groundatom to be checked

Returns:

boolean value, true if the groundatom satisfies the clause, false if the clause ist still satisfied

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

double edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::getDelta

(

)

[inline, virtual]

Method returns the weight of the clause always as 1/count of clauses of the according formula

Returns:

deltacosts of the clause as double value

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

double edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::getDeltaFormula

(

boolean

trueFlip

)

[inline, virtual]

Method returns the weight of the according formula as the weight of the clause if it's flip changes the value of the formula (negative if satisfied, positive if changed to unsatisfied)

Parameters:

trueFlip

boolean value: true, if the flip changes the value of the clause true, else false

Returns:

deltacosts of the clause as double value

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

Vector<GroundAtom> edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::getGAsOfConstraint

(

)

[inline, virtual]

Methot returns all groundatoms of the according constraint.

Returns:

containing groundatoms

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

Vector<Object> edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::greedySatisfy

(

)

[inline, virtual]

Method calls the method pickAndFlipVar of MaxWaltSAT-class with the containing groundatoms as candidates (see there for details).

Returns:

returns the best groundatom(s) to satisfy the clause with related added weights

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::handleFlip

(

GroundAtom

gndAtom

)

[inline, virtual]

Method refreshs all states of the relating Objects (trueOnes, unsatisfiedConstraints, formula2satClause, unsatisfied sum and bottlenecks).

Parameters:

gndAtom

fliped groundatom

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

void edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::initState

(

)

[inline, virtual]

Sets the initial state of the weighted clause (trueOnes, bottelnecks and if necessary unsatisfied constraints).

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

boolean edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::isHard

(

)

[inline, virtual]

Method returns if a constraint is part of a hard formula (must be satisfied)

Returns:

true, if constraint is part of a hard formula, else not

Implements edu::tum::cs::logic::sat::weighted::MaxWalkSAT::Constraint.

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

String edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::toString

(

)

[inline]

Method returns a string-representation of the weighted clause

Returns:

string-representation of the weighted clause

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

---

Member Data Documentation

Vector<GroundAtom> edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::gndAtoms [protected]

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

boolean edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::hard

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

GroundLiteral [] edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::lits [protected]

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

HashSet<GroundAtom> edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::trueOnes [protected]

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

double edu::tum::cs::logic::sat::weighted::MaxWalkSAT::WeightedClause::weight [protected]

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

---

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

• logic/sat/weighted/MaxWalkSAT.java