edu::tum::cs::logic::sat::SampleSAT Class Reference

Inheritance diagram for edu::tum::cs::logic::sat::SampleSAT:

Classes
class	Clause
class	Constraint
Public Member Functions
void	enableUnitPropagation ()
String	getAlgorithmName ()
ParameterHandler	getParameterHandler ()
PossibleWorld	getState ()
void	initConstraints (Iterable<?extends edu.tum.cs.logic.sat.Clause > kb) throws Exception
void	run () throws Exception
	SampleSAT (PossibleWorld state, WorldVariables vars, Iterable<?extends AbstractVariable > db) throws Exception
	SampleSAT (Iterable<?extends edu.tum.cs.logic.sat.Clause > kb, PossibleWorld state, WorldVariables vars, Iterable<?extends AbstractVariable > db) throws Exception
void	setDebugMode (boolean active)
void	setPSampleSAT (double p)
void	setPWalkSAT (double p)
Static Public Member Functions
static void	main (String[] args) throws Exception
Protected Member Functions
void	addBottleneck (GroundAtom a, Constraint c)
void	addGAOccurrence (GroundAtom a, Constraint c)
void	addUnsatisfiedConstraint (Constraint c)
void	checkIntegrity () throws Exception
int	deltaCost (GroundAtom gndAtom)
void	flipGndAtom (GroundAtom gndAtom)
void	makeMove ()
void	pickAndFlipVar (Iterable< GroundAtom > candidates)
boolean	pickSecondAtRandomAndFlip (GroundAtom gndAtom)
void	removeClause (Clause c)
void	SAMove ()
void	setRandomState ()
void	unitPropagation ()
void	walkSATMove ()
Protected Attributes
HashMap< Integer, Vector < Constraint > >	bottlenecks
Vector< Constraint >	constraints
boolean	debug = false
HashMap< Integer, Boolean >	evidence
EvidenceHandler	evidenceHandler
HashMap< Integer, Vector < Constraint > >	GAOccurrences
ParameterHandler	paramHandler
double	pSampleSAT = 0.9
double	pWalkSAT = 0.5
Random	rand
PossibleWorld	state
Vector< Constraint >	unsatisfiedConstraints
boolean	useUnitPropagation = false
WorldVariables	vars
Package Attributes
Iterable<?extends edu.tum.cs.logic.sat.Clause >	kb

Detailed Description

Implementation of the stochastic SAT sampling algorithm SampleSAT by Wei et al. It near-uniformly samples a solution from the set of solutions

Author:: jain

Definition at line 31 of file SampleSAT.java.

Constructor & Destructor Documentation

edu::tum::cs::logic::sat::SampleSAT::SampleSAT	(	Iterable<?extends edu.tum.cs.logic.sat.Clause >	kb,
		PossibleWorld	state,
		WorldVariables	vars,
		Iterable<?extends AbstractVariable >	db
	)			throws Exception `[inline]`

Parameters:

	kb	a collection of clauses to satisfy (such as a ClausalKB)
	state	a possible world to write to (can be arbitrarily initialized, as it is completely reinitialized)
	vars	the set of variables the SAT problem is defined on
	db	an evidence database indicating truth values of evidence atoms (which are to be respected by the algorithm); the state is initialized to respect it and the respective variables are never touched again

Exceptions:

Exception

Definition at line 64 of file SampleSAT.java.

edu::tum::cs::logic::sat::SampleSAT::SampleSAT	(	PossibleWorld	state,
		WorldVariables	vars,
		Iterable<?extends AbstractVariable >	db
	)			throws Exception `[inline]`

initializes the sampler without a set of constraints

Parameters:

	state	a possible world to write to (can be arbitrarily initialized, as it is completely reinitialized)
	vars	the set of variables the SAT problem is defined on
	db	an evidence database indicating truth values of evidence atoms (which are to be respected by the algorithm); the state is initialized to respect it and the respective variables are never touched again

Exceptions:

Exception

Definition at line 88 of file SampleSAT.java.

Member Function Documentation

void edu::tum::cs::logic::sat::SampleSAT::addBottleneck	(	GroundAtom	a,
		Constraint	c
	)			`[inline, protected]`

Definition at line 193 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::addGAOccurrence	(	GroundAtom	a,
		Constraint	c
	)			`[inline, protected]`

Definition at line 202 of file SampleSAT.java.

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

Definition at line 189 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::checkIntegrity ( ) throws Exception [inline, protected]

checks the integrity of internal data structures

Exceptions:

Exception

Definition at line 253 of file SampleSAT.java.

int edu::tum::cs::logic::sat::SampleSAT::deltaCost ( GroundAtom gndAtom ) [inline, protected]

Definition at line 448 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::enableUnitPropagation ( ) [inline]

enables unit propagation when initializing the set of constraints

Definition at line 99 of file SampleSAT.java.

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

Definition at line 430 of file SampleSAT.java.

String edu::tum::cs::logic::sat::SampleSAT::getAlgorithmName ( ) [inline]

Definition at line 634 of file SampleSAT.java.

ParameterHandler edu::tum::cs::logic::sat::SampleSAT::getParameterHandler ( ) [inline]

Implements edu::tum::cs::inference::IParameterHandler.

Definition at line 630 of file SampleSAT.java.

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

Definition at line 296 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::initConstraints ( Iterable<?extends edu.tum.cs.logic.sat.Clause > kb ) throws Exception [inline]

prepares this sampler for a new set of constraints. NOTE: This method only needs to be called explicitly when switching to a new set of constraints or when using the construction method without the KB

Parameters:

kb

Exceptions:

Exception

Definition at line 108 of file SampleSAT.java.

static void edu::tum::cs::logic::sat::SampleSAT::main ( String[] args ) throws Exception [inline, static]

Definition at line 597 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::makeMove ( ) [inline, protected]

Reimplemented in edu::tum::cs::logic::sat::WalkSAT.

Definition at line 307 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::pickAndFlipVar ( Iterable< GroundAtom > candidates ) [inline, protected]

Definition at line 377 of file SampleSAT.java.

boolean edu::tum::cs::logic::sat::SampleSAT::pickSecondAtRandomAndFlip ( GroundAtom gndAtom ) [inline, protected]

attempts to flip the variable that is given, choosing an appropriate second variable (at random where applicable) if the variable is in a block

Parameters:

gndAtom

Returns:: true if the variable could be flipped

Definition at line 348 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::removeClause ( Clause c ) [inline, protected]

Definition at line 182 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::run ( ) throws Exception [inline]

solves the SAT problem by first initializing the state randomly (respecting the evidence, however) and then performing greedy and SA moves (as determined by parameter p)

Exceptions:

Exception

Definition at line 215 of file SampleSAT.java.

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

Definition at line 329 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::setDebugMode ( boolean active ) [inline]

Definition at line 92 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::setPSampleSAT ( double p ) [inline]

sets the probability of a random walk (WalkSAT-style) move

Parameters:

p

Definition at line 467 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::setPWalkSAT ( double p ) [inline]

sets the probability of a random move (rather than a greedy move) in WalkSAT moves

Parameters:

p

Definition at line 475 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::setRandomState ( ) [inline, protected]

sets a random state for non-evidence atoms

Reimplemented in edu::tum::cs::srl::bayesnets::inference::SATIS::SampleSATPriors.

Definition at line 303 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::unitPropagation ( ) [inline, protected]

performs unit propagation on clauses to simplify the set of constraints

Definition at line 135 of file SampleSAT.java.

void edu::tum::cs::logic::sat::SampleSAT::walkSATMove ( ) [inline, protected]

Definition at line 318 of file SampleSAT.java.

Member Data Documentation

HashMap<Integer,Vector<Constraint> > edu::tum::cs::logic::sat::SampleSAT::bottlenecks [protected]

Definition at line 32 of file SampleSAT.java.

Vector<Constraint> edu::tum::cs::logic::sat::SampleSAT::constraints [protected]

Definition at line 36 of file SampleSAT.java.

boolean edu::tum::cs::logic::sat::SampleSAT::debug = false [protected]

Definition at line 39 of file SampleSAT.java.

HashMap<Integer,Boolean> edu::tum::cs::logic::sat::SampleSAT::evidence [protected]

Definition at line 41 of file SampleSAT.java.

EvidenceHandler edu::tum::cs::logic::sat::SampleSAT::evidenceHandler [protected]

Definition at line 40 of file SampleSAT.java.

HashMap<Integer,Vector<Constraint> > edu::tum::cs::logic::sat::SampleSAT::GAOccurrences [protected]

Definition at line 33 of file SampleSAT.java.

Iterable<? extends edu.tum.cs.logic.sat.Clause> edu::tum::cs::logic::sat::SampleSAT::kb [package]

Definition at line 43 of file SampleSAT.java.

ParameterHandler edu::tum::cs::logic::sat::SampleSAT::paramHandler [protected]

Definition at line 44 of file SampleSAT.java.

double edu::tum::cs::logic::sat::SampleSAT::pSampleSAT = 0.9 [protected]

SampleSAT's p parameter: probability of performing a random walk (WalkSAT-style) move rather than a simulated annealing-style move

Definition at line 48 of file SampleSAT.java.

double edu::tum::cs::logic::sat::SampleSAT::pWalkSAT = 0.5 [protected]

WalkSAT's p parameter: random walk parameter, probability of non-greedy move (random flip in unsatisfied clause) rather than greedy (locally optimal) move. According to the WalkSAT paper, optimal values were always between 0.5 and 0.6

Definition at line 54 of file SampleSAT.java.

Random edu::tum::cs::logic::sat::SampleSAT::rand [protected]

Definition at line 37 of file SampleSAT.java.

PossibleWorld edu::tum::cs::logic::sat::SampleSAT::state [protected]

Definition at line 34 of file SampleSAT.java.

Vector<Constraint> edu::tum::cs::logic::sat::SampleSAT::unsatisfiedConstraints [protected]

Definition at line 35 of file SampleSAT.java.

boolean edu::tum::cs::logic::sat::SampleSAT::useUnitPropagation = false [protected]

Definition at line 42 of file SampleSAT.java.

WorldVariables edu::tum::cs::logic::sat::SampleSAT::vars [protected]

Definition at line 38 of file SampleSAT.java.

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