org.sat4j.minisat.core
Interface DataStructureFactory

All Known Implementing Classes:

AbstractCardinalityDataStructure, AbstractDataStructureFactory, AbstractPBClauseCardConstrDataStructure, AbstractPBDataStructureFactory, CardinalityDataStructure, CardinalityDataStructureYanMax, CardinalityDataStructureYanMin, ClausalDataStructureCB, ClausalDataStructureCBWL, ClausalDataStructureWL, MixedDataStructureDaniel, MixedDataStructureWithBinary, MixedDataStructureWithBinaryAndTernary, PBMaxCBClauseCardConstrDataStructure, PBMaxClauseAtLeastConstrDataStructure, PBMaxClauseCardConstrDataStructure, PBMaxDataStructure, PBMinClauseCardConstrDataStructure, PBMinDataStructure, PuebloPBMinClauseAtLeastConstrDataStructure, PuebloPBMinClauseCardConstrDataStructure, PuebloPBMinDataStructure

public interface DataStructureFactory

Author:

leberre The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.

Method Summary

void	conflictDetectedInWatchesFor(int p, int i)
Constr	createCardinalityConstraint(IVecInt literals, int degree)
Constr	createClause(IVecInt literals)
Constr	createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	createUnregisteredClause(IVecInt literals)
Constr	createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
ILits	getVocabulary()
IVec<Propagatable>	getWatchesFor(int p)
void	learnConstraint(Constr constr)
void	reset()
void	setLearner(Learner l)
void	setUnitPropagationListener(UnitPropagationListener s)

Method Detail

createClause

Constr createClause(IVecInt literals)
                    throws ContradictionException

Parameters:

literals - a set of literals using Dimacs format (signed non null integers).

Returns:

null if the constraint is a tautology.

Throws:

ContradictionException - the constraint is trivially unsatisfiable.

java.lang.UnsupportedOperationException - there is no concrete implementation for that constraint.

createUnregisteredClause

Constr createUnregisteredClause(IVecInt literals)

learnConstraint

void learnConstraint(Constr constr)

createCardinalityConstraint

Constr createCardinalityConstraint(IVecInt literals,
                                   int degree)
                                   throws ContradictionException

Throws:

ContradictionException

createPseudoBooleanConstraint

Constr createPseudoBooleanConstraint(IVecInt literals,
                                     IVec<java.math.BigInteger> coefs,
                                     boolean moreThan,
                                     java.math.BigInteger degree)
                                     throws ContradictionException

Throws:

ContradictionException

createUnregisteredPseudoBooleanConstraint

Constr createUnregisteredPseudoBooleanConstraint(IVecInt literals,
                                                 IVec<java.math.BigInteger> coefs,
                                                 java.math.BigInteger degree)

setUnitPropagationListener

void setUnitPropagationListener(UnitPropagationListener s)

setLearner

void setLearner(Learner l)

reset

void reset()

getVocabulary

ILits getVocabulary()

getWatchesFor

IVec<Propagatable> getWatchesFor(int p)

Parameters:

p -

Returns:

a vector containing all the objects to be notified of the satisfaction of that literal.

conflictDetectedInWatchesFor

void conflictDetectedInWatchesFor(int p,
                                  int i)

Parameters:

p -

i - the index of the conflicting constraint