Public Member Functions
boolean	checkMinimalityHS ()
int	compute (int maxHSSize, int maxNumMinHS)
int	computeMore (int newMaxHSSize, int newMaxNumMinHS)
ArrayList	getConflictsAsAss ()
ArrayList	getMinHS ()
ArrayList	getMinHSAsIntLists ()
boolean	hitsAllConflictSets ()
	MinHittingSets (boolean conflictsAreMinimal, ArrayList conflictSets)
	MinHittingSets (boolean conflictsAreMinimal, ABTheoremProver tp)
Static Public Attributes
static final int	CS_ALL_MIN_DIAGS_COMPUTED = 1
static final int	CS_MAX_HS_SIZE_REACHED = 2
static final int	CS_MAX_NUM_MIN_HS_REACHED = 3
Protected Member Functions
void	attemptPrune (HSNode node)
SortedIntList	callTheoremProver (SortedIntList edgeLabels)
boolean	canClose (HSNode node)
void	computeLabel (HSNode node)
int	computeNumUnprunedChildren (HSNode node)
void	expandNode (HSNode node, LinkedList newNodes, int lastLevel)
boolean	nodeInvariant (HSNode node)
void	processLastLevel (int lastLevel, LinkedList lastLevelNodes, LinkedList newLevelNodes, boolean expandNodes)
void	prune (HSNode node, HSNode prunedParent)
void	relabel (HSNode node, HSNode newNode)
int	searchRefutingCS (SortedIntList edgeLabel)
Protected Attributes
ArrayList	assumptions = null
HSNode	attemptedPruneNode = null
SortedIntList	components = null
int	computationState = -1
ArrayList	computedMinHS = new ArrayList()
boolean	computeIncr
boolean	conflictsAreMinimal
ArrayList	conflictSets = null
ArrayList	levels = new ArrayList()
int	maxHSSize
int	maxNumMinHS
HSNode	rootNode = null
ABTheoremProver	theoremProver = null
Static Protected Attributes
static final int	CS_COMPUTING = 0

Detailed Description

This class encapsulates Reiter's Hitting Set algorithm.

There are 2 possibilities: 1) the conflict sets are provided by the user of this class, i.e. no more calls to the TP are performed by methods of this class. 2) the conflict sets are computed incrementally while creating the HS-DAG, i.e. an instance of ABTheoremProver must be provided by the user of this class.

Definition at line 47 of file MinHittingSets.java.

Constructor & Destructor Documentation

hittingsetalg.MinHittingSets.MinHittingSets	(	boolean	conflictsAreMinimal,
		ArrayList	conflictSets
	)		`[inline]`

Conctructor of MinHittingSets, receiving a list of conflict sets.

The constructor initializes the object instance. In order to compute the hitting sets, call compute(). Note that an instance of MinHittingSets which is created by this constructor does not allow to compute the hitting sets incrementally!

Parameters:

conflictsAreMinimal	If true, then all provided conflicts are minimal. As a consequence, the computationally expensive "Pruning" rule is not required.
conflictSets	A list of SortedIntList objects, where a SortedIntList is a linked list containing integers representing components.

Definition at line 113 of file MinHittingSets.java.

hittingsetalg.MinHittingSets.MinHittingSets	(	boolean	conflictsAreMinimal,
		ABTheoremProver	tp
	)		`[inline]`

Conctructor of MinHittingSets, receiving a theorem prover.

The constructor initializes the object instance. A subsequent call to compute() will compute the min. hitting sets incrementally. If conflictsAreMinimal is true, then the algorithm relies on the theorem prover to compute only minmal conflicts.

Definition at line 130 of file MinHittingSets.java.

Member Function Documentation

void hittingsetalg.MinHittingSets.attemptPrune ( HSNode node ) [inline, protected]

Definition at line 530 of file MinHittingSets.java.

SortedIntList hittingsetalg.MinHittingSets.callTheoremProver ( SortedIntList edgeLabels ) [inline, protected]

Definition at line 356 of file MinHittingSets.java.

boolean hittingsetalg.MinHittingSets.canClose ( HSNode node ) [inline, protected]

Definition at line 766 of file MinHittingSets.java.

boolean hittingsetalg.MinHittingSets.checkMinimalityHS ( ) [inline]

Definition at line 888 of file MinHittingSets.java.

int hittingsetalg.MinHittingSets.compute	(	int	maxHSSize,
		int	maxNumMinHS
	)		`[inline]`

Definition at line 260 of file MinHittingSets.java.

void hittingsetalg.MinHittingSets.computeLabel ( HSNode node ) [inline, protected]

Definition at line 677 of file MinHittingSets.java.

int hittingsetalg.MinHittingSets.computeMore	(	int	newMaxHSSize,
		int	newMaxNumMinHS
	)		`[inline]`

Definition at line 305 of file MinHittingSets.java.

int hittingsetalg.MinHittingSets.computeNumUnprunedChildren ( HSNode node ) [inline, protected]

Definition at line 517 of file MinHittingSets.java.

void hittingsetalg.MinHittingSets.expandNode	(	HSNode	node,
		LinkedList	newNodes,
		int	lastLevel
	)		`[inline, protected]`

Definition at line 833 of file MinHittingSets.java.

ArrayList hittingsetalg.MinHittingSets.getConflictsAsAss ( ) [inline]

Definition at line 227 of file MinHittingSets.java.

ArrayList hittingsetalg.MinHittingSets.getMinHS ( ) [inline]

Returns the computed min. hitting sets.

The return value is an ArrayList of ArrayList of Assumption. IMPORTANT: this method can be used only if a theorem prover is used, i.e., if the conflict sets are computed dynamically! If no TP is used, then getMinHSAsIntegers() must be used!

Definition at line 165 of file MinHittingSets.java.

ArrayList hittingsetalg.MinHittingSets.getMinHSAsIntLists ( ) [inline]

Definition at line 204 of file MinHittingSets.java.

boolean hittingsetalg.MinHittingSets.hitsAllConflictSets ( ) [inline]

Definition at line 911 of file MinHittingSets.java.

boolean hittingsetalg.MinHittingSets.nodeInvariant ( HSNode node ) [inline, protected]

Definition at line 934 of file MinHittingSets.java.

void hittingsetalg.MinHittingSets.processLastLevel	(	int	lastLevel,
		LinkedList	lastLevelNodes,
		LinkedList	newLevelNodes,
		boolean	expandNodes
	)		`[inline, protected]`