org.kahina.logic.sat.data.cnf

Class CnfSatInstance

java.lang.Object

org.kahina.core.data.KahinaObject

org.kahina.logic.sat.data.KahinaSatInstance

org.kahina.logic.sat.data.cnf.CnfSatInstance

All Implemented Interfaces:

java.io.Serializable

Direct Known Subclasses:

GroupCnfSatInstance, MUCMetaInstance

public class CnfSatInstance
extends KahinaSatInstance

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
protected java.util.List<java.lang.Integer>	clauseIDs
protected java.util.Map<java.lang.Integer,java.util.List<java.lang.Integer>>	clauseStore
protected int	maxVarID
protected boolean	needsRebuild
protected java.util.Map<java.lang.Integer,java.util.List<java.lang.Integer>>	occurrenceMap
protected java.util.Map<java.lang.Integer,java.lang.Integer>	reverseConversionTable

Fields inherited from class org.kahina.logic.sat.data.KahinaSatInstance

symbolTable

Fields inherited from class org.kahina.core.data.KahinaObject

needsUpdate

Constructor Summary

Constructors

Constructor and Description
CnfSatInstance()

Method Summary

Methods

Modifier and Type	Method and Description
int	addClause(java.util.List<java.lang.Integer> clause)
void	announceAddedClauses()
void	announceChangedClauses()
void	applyAssignmentDestructively(PartialAssignment assignment)
void	applyDontCareFilter(ClauseFilter filter)
void	computeOccurrenceMap()
CnfSatInstance	copy()
void	deleteVariablesDestructively(java.util.Set<java.lang.Integer> removedVars)
java.util.List<java.lang.Integer>	deriveUnitsByPropagation(java.util.List<java.lang.Integer> toPropagate)
void	discardOccurrenceMap()
PartialAssignment	extractMaxAutarkyDestructively()
java.util.Map<java.lang.String,java.lang.Integer>	generateClauseToIndexMap()
java.util.List<java.lang.Integer>	getClause(int clauseIndex)
java.util.List<java.lang.Integer>	getClauseByID(int clauseID)
int	getCountOccourrence(int variable) Counts the occurrence of a variable within the instance
int	getHighestVar() precondition: removeID must not be executed if this function is used.
int	getNumVariables()
int	getSize()
java.util.List<java.lang.Integer>	getSubsumedClauseIndices(java.util.List<java.lang.Integer> clause) Finds the clauses subsumed by some clause.
protected int	idxToId(int clauseIndex)
boolean	isDontCareClause(int clauseIndex)
boolean	needsRebuild()
boolean	needsUpdate() States whether a view of this object needs to be updated.
java.lang.String	printAllClauses()
void	reduceToLeanKernel()
void	removeClauseID(int clauseID) Removes the clause with the given internal ID.
void	removeClauseIndex(int clauseIndex) Removes the clause at the given index (not an internal ID!).
CnfSatInstance	selectClauses(java.util.Collection<java.lang.Integer> clauseIndices) Extracts a subinstance of the this instance defined by clause indices.
void	setSubsumptionCheck(boolean check)

Methods inherited from class org.kahina.logic.sat.data.KahinaSatInstance

getSymbolForLiteral, setSymbolMapping

Methods inherited from class org.kahina.core.data.KahinaObject

requireUpdate

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

maxVarID

protected int maxVarID

clauseIDs

protected java.util.List<java.lang.Integer> clauseIDs

reverseConversionTable

protected java.util.Map<java.lang.Integer,java.lang.Integer> reverseConversionTable

clauseStore

protected java.util.Map<java.lang.Integer,java.util.List<java.lang.Integer>> clauseStore

occurrenceMap

protected java.util.Map<java.lang.Integer,java.util.List<java.lang.Integer>> occurrenceMap

needsRebuild

protected boolean needsRebuild

Constructor Detail

CnfSatInstance

public CnfSatInstance()

Method Detail

copy

public CnfSatInstance copy()

setSubsumptionCheck

public void setSubsumptionCheck(boolean check)

addClause

public int addClause(java.util.List<java.lang.Integer> clause)

idxToId

protected int idxToId(int clauseIndex)

removeClauseID

public void removeClauseID(int clauseID)

Removes the clause with the given internal ID.

Parameters:

clauseID - the ID of the clause to be removed.

getCountOccourrence

public int getCountOccourrence(int variable)

Counts the occurrence of a variable within the instance

Parameters:

variable - the variableID

Returns:

in how many clauses this variable appears.

removeClauseIndex

public void removeClauseIndex(int clauseIndex)

Removes the clause at the given index (not an internal ID!).

Parameters:

clauseIndex - the index of the clause to be removed.

getSubsumedClauseIndices

public java.util.List<java.lang.Integer> getSubsumedClauseIndices(java.util.List<java.lang.Integer> clause)

Finds the clauses subsumed by some clause.

Parameters:

clause - the clause to check for subsumption against the clauses in this CNF

Returns:

null if the new clause is subsumed, a list of indices of subsumed clauses otherwise

getSize

public int getSize()

Returns:

number of Clauses

computeOccurrenceMap

public void computeOccurrenceMap()

discardOccurrenceMap

public void discardOccurrenceMap()

isDontCareClause

public boolean isDontCareClause(int clauseIndex)

applyDontCareFilter

public void applyDontCareFilter(ClauseFilter filter)

getClause

public java.util.List<java.lang.Integer> getClause(int clauseIndex)

selectClauses

public CnfSatInstance selectClauses(java.util.Collection<java.lang.Integer> clauseIndices)

Extracts a subinstance of the this instance defined by clause indices. The clauses are not copied, but pointers to clauses are shared, i.e. modifying clauses in the subinstance will corrupt this instance! For a safely modifiable version, use copy() on the result.

Parameters:

clauseIndices - a list of 1-based clause indices in this instance

Returns:

a new sat instance containing the clauses at the selected indices

deriveUnitsByPropagation

public java.util.List<java.lang.Integer> deriveUnitsByPropagation(java.util.List<java.lang.Integer> toPropagate)

getHighestVar

public int getHighestVar()

precondition: removeID must not be executed if this function is used.

Returns:

deleteVariablesDestructively

public void deleteVariablesDestructively(java.util.Set<java.lang.Integer> removedVars)

applyAssignmentDestructively

public void applyAssignmentDestructively(PartialAssignment assignment)

reduceToLeanKernel

public void reduceToLeanKernel()

extractMaxAutarkyDestructively

public PartialAssignment extractMaxAutarkyDestructively()

generateClauseToIndexMap

public java.util.Map<java.lang.String,java.lang.Integer> generateClauseToIndexMap()

announceChangedClauses

public void announceChangedClauses()

announceAddedClauses

public void announceAddedClauses()

needsUpdate

public boolean needsUpdate()

Description copied from class: KahinaObject

States whether a view of this object needs to be updated.

Overrides:

needsUpdate in class KahinaObject

Returns:

whether the object was changed since the last call to needsUpdate()

needsRebuild

public boolean needsRebuild()

printAllClauses

public java.lang.String printAllClauses()

getClauseByID

public java.util.List<java.lang.Integer> getClauseByID(int clauseID)

getNumVariables

public int getNumVariables()