org.sat4j.pb.core
Interface PBDataStructureFactory

All Superinterfaces:

DataStructureFactory

All Known Implementing Classes:

AbstractPBClauseCardConstrDataStructure, AbstractPBDataStructureFactory, CompetMinHTmixedClauseCardConstrDataStructureFactory, CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBLongMixedHTClauseCardConstrDataStructure, CompetResolutionPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBMixedHTClauseCardConstrDataStructure, CompetResolutionPBMixedWLClauseCardConstrDataStructure, PBLongMaxClauseCardConstrDataStructure, PBLongMinClauseCardConstrDataStructure, PBMaxClauseAtLeastConstrDataStructure, PBMaxClauseCardConstrDataStructure, PBMaxDataStructure, PBMinClauseCardConstrDataStructure, PBMinDataStructure, PuebloPBMinClauseAtLeastConstrDataStructure, PuebloPBMinClauseCardConstrDataStructure, PuebloPBMinDataStructure

public interface PBDataStructureFactory
extends DataStructureFactory

Method Summary

Constr	createPseudoBooleanConstraint(IVecInt literals, IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
Constr	createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)

Methods inherited from interface org.sat4j.minisat.core.DataStructureFactory

conflictDetectedInWatchesFor, createCardinalityConstraint, createClause, createUnregisteredClause, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener

Method Detail

createPseudoBooleanConstraint

Constr createPseudoBooleanConstraint(IVecInt literals,
                                     IVec<BigInteger> coefs,
                                     boolean moreThan,
                                     BigInteger degree)
                                     throws ContradictionException

Throws:

ContradictionException

createUnregisteredPseudoBooleanConstraint

Constr createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)