org.sat4j.minisat.core
Interface DataStructureFactory

All Known Subinterfaces:

PBDataStructureFactory

All Known Implementing Classes:

AbstractCardinalityDataStructure, AbstractDataStructureFactory, AbstractPBClauseCardConstrDataStructure, AbstractPBDataStructureFactory, CardinalityDataStructure, CardinalityDataStructureYanMax, CardinalityDataStructureYanMin, ClausalDataStructureWL, CompetMinHTmixedClauseCardConstrDataStructureFactory, CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBLongMixedHTClauseCardConstrDataStructure, CompetResolutionPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBMixedHTClauseCardConstrDataStructure, CompetResolutionPBMixedWLClauseCardConstrDataStructure, MixedDataStructureDanielHT, MixedDataStructureDanielWL, MixedDataStructureSingleWL, PBLongMaxClauseCardConstrDataStructure, PBLongMinClauseCardConstrDataStructure, PBMaxClauseAtLeastConstrDataStructure, PBMaxClauseCardConstrDataStructure, PBMaxDataStructure, PBMinClauseCardConstrDataStructure, PBMinDataStructure, PuebloPBMinClauseAtLeastConstrDataStructure, PuebloPBMinClauseCardConstrDataStructure, PuebloPBMinDataStructure

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) Create a cardinality constraint of the form sum li >= 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.

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

Create a cardinality constraint of the form sum li >= degree.

Parameters:

literals - a set of literals.

degree - the degree of the cardinality constraint.

Returns:

a constraint stating that at least degree literals are satisfied.

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