org.sat4j.minisat.core
Interface DataStructureFactory<L extends ILits>
- All Known Implementing Classes:
- AbstractCardinalityDataStructure, AbstractDataStructureFactory, AbstractPBClauseCardConstrDataStructure, AbstractPBDataStructureFactory, CardinalityDataStructure, CardinalityDataStructureYanMax, CardinalityDataStructureYanMin, ClausalDataStructureCB, ClausalDataStructureCBWL, ClausalDataStructureWL, MixedDataStructureDaniel, MixedDataStructureDanielCBWL, MixedDataStructureWithBinary, MixedDataStructureWithBinaryAndTernary, PBMaxCBClauseCardConstrDataStructure, PBMaxClauseAtLeastConstrDataStructure, PBMaxClauseCardConstrDataStructure, PBMaxDataStructure, PBMinClauseCardConstrDataStructure, PBMinDataStructure, PuebloPBMinClauseAtLeastConstrDataStructure, PuebloPBMinClauseCardConstrDataStructure, PuebloPBMinDataStructure
public interface DataStructureFactory<L extends ILits>
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
- Author:
- leberre
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
L 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
Copyright © 2007 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.