org.sat4j.minisat.core
Interface DataStructureFactory<L extends ILits>
- All Known Implementing Classes:
- AbstractCardinalityDataStructure, AbstractDataStructureFactory, CardinalityDataStructure, ClausalDataStructureCB, ClausalDataStructureCBHT, ClausalDataStructureHT, MixedDataStructureDaniel, MixedDataStructureDanielCBHT, MixedDataStructureWithBinary, MixedDataStructureWithBinaryAndTernary
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
setUnitPropagationListener
void setUnitPropagationListener(UnitPropagationListener s)
setLearner
void setLearner(Learner l)
reset
void reset()
getVocabulary
L getVocabulary()
getAttachesFor
IVec<Propagatable> getAttachesFor(int p)
- Parameters:
p
-
- Returns:
- a vector containing all the objects to be notified of the
satisfaction of that literal.
conflictDetectedInAttachesFor
void conflictDetectedInAttachesFor(int p,
int i)
- Parameters:
p
- i
- the index of the conflicting constraint
Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.