public abstract class AbstractPBClauseCardConstrDataStructure extends AbstractPBDataStructureFactory
FOR_COMPETITION, NO_COMPETITION
learner, lits, solver
Modifier and Type | Method and Description |
---|---|
protected Constr |
constraintFactory(int[] literals,
java.math.BigInteger[] coefs,
java.math.BigInteger degree) |
protected Constr |
constructCard(IVecInt theLits,
int degree) |
protected Constr |
constructClause(IVecInt v) |
protected Constr |
constructLearntCard(IDataStructurePB dspb) |
protected Constr |
constructLearntCard(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
protected Constr |
constructLearntClause(IVecInt literals) |
protected Constr |
constructLearntPB(IDataStructurePB dspb) |
protected Constr |
constructLearntPB(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
protected Constr |
constructPB(int[] theLits,
java.math.BigInteger[] coefs,
java.math.BigInteger degree) |
Constr |
createClause(IVecInt literals) |
Constr |
createUnregisteredClause(IVecInt literals) |
protected Constr |
learntAtLeastConstraintFactory(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
protected Constr |
learntAtMostConstraintFactory(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
protected Constr |
learntConstraintFactory(IDataStructurePB dspb) |
static java.math.BigInteger |
sumOfCoefficients(java.math.BigInteger[] coefs) |
createAtLeastPBConstraint, createAtMostPBConstraint, createCardinalityConstraint, createLits, createPseudoBooleanConstraint, createUnregisteredAtLeastConstraint, createUnregisteredAtMostConstraint, createUnregisteredCardinalityConstraint, createUnregisteredPseudoBooleanConstraint, getNormalizer, setNormalizer, setNormalizer
conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener
public Constr createClause(IVecInt literals) throws ContradictionException
createClause
in interface DataStructureFactory
createClause
in class AbstractPBDataStructureFactory
literals
- a set of literals using Dimacs format (signed non null
integers).ContradictionException
- the constraint is trivially unsatisfiable.public Constr createUnregisteredClause(IVecInt literals)
createUnregisteredClause
in interface DataStructureFactory
createUnregisteredClause
in class AbstractPBDataStructureFactory
protected Constr constraintFactory(int[] literals, java.math.BigInteger[] coefs, java.math.BigInteger degree) throws ContradictionException
constraintFactory
in class AbstractPBDataStructureFactory
ContradictionException
protected Constr learntConstraintFactory(IDataStructurePB dspb)
learntConstraintFactory
in class AbstractPBDataStructureFactory
protected Constr learntAtLeastConstraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
learntAtLeastConstraintFactory
in class AbstractPBDataStructureFactory
protected Constr learntAtMostConstraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
learntAtMostConstraintFactory
in class AbstractPBDataStructureFactory
protected Constr constructCard(IVecInt theLits, int degree) throws ContradictionException
ContradictionException
protected Constr constructPB(int[] theLits, java.math.BigInteger[] coefs, java.math.BigInteger degree) throws ContradictionException
ContradictionException
protected Constr constructLearntCard(IDataStructurePB dspb)
protected Constr constructLearntCard(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected Constr constructLearntPB(IDataStructurePB dspb)
protected Constr constructLearntPB(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
public static final java.math.BigInteger sumOfCoefficients(java.math.BigInteger[] coefs)