org.sat4j.minisat.core
Interface DataStructureFactory

All Known Implementing Classes:

AbstractCardinalityDataStructure, AbstractDataStructureFactory, CardinalityDataStructure, CardinalityDataStructureYanMax, CardinalityDataStructureYanMin, ClausalDataStructureCB, ClausalDataStructureCBWL, ClausalDataStructureWL, MixedDataStructureDanielCBWL, MixedDataStructureDanielHT, MixedDataStructureDanielWL

public interface DataStructureFactory

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

Author:

leberre

Method Summary

void	conflictDetectedInWatchesFor(int p, int i)
Constr	createCardinalityConstraint(IVecInt literals, int degree)
Constr	createClause(IVecInt literals)
Constr	createUnregisteredClause(IVecInt literals)
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

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