org.sat4j.minisat.core
Interface DataStructureFactory
- All Known Implementing Classes:
- AbstractCardinalityDataStructure, AbstractDataStructureFactory, AbstractPBDataStructureFactory, CardinalityDataStructure, CardinalityDataStructureYanMax, CardinalityDataStructureYanMin, ClausalDataStructureCB, ClausalDataStructureCBWL, ClausalDataStructureWL, MixedDataStructureDaniel, MixedDataStructureWithBinary, MixedDataStructureWithBinaryAndTernary, PBMaxDataStructure, PBMinDataStructure
public interface DataStructureFactory
- Author:
- leberre The aim of the factory is to provide a concrete
implementation of clauses, cardinality constraints and pseudo boolean
consraints.
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