org.sat4j.pb.constraints

Class AbstractPBClauseCardConstrDataStructure

java.lang.Object

org.sat4j.minisat.constraints.AbstractDataStructureFactory

org.sat4j.pb.constraints.AbstractPBDataStructureFactory

org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory, PBDataStructureFactory

Direct Known Subclasses:

CompetMinHTmixedClauseCardConstrDataStructureFactory, CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBLongMixedHTClauseCardConstrDataStructure, CompetResolutionPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBMixedHTClauseCardConstrDataStructure, CompetResolutionPBMixedWLClauseCardConstrDataStructure, PBLongMaxClauseCardConstrDataStructure, PBLongMinClauseCardConstrDataStructure, PBMaxClauseAtLeastConstrDataStructure, PBMaxClauseCardConstrDataStructure, PBMinClauseCardConstrDataStructure, PuebloPBMinClauseAtLeastConstrDataStructure, PuebloPBMinClauseCardConstrDataStructure

public abstract class AbstractPBClauseCardConstrDataStructure
extends AbstractPBDataStructureFactory

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

FOR_COMPETITION, NO_COMPETITION

Fields inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory

learner, lits, solver

Method Summary

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)

Methods inherited from class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

createAtLeastPBConstraint, createAtMostPBConstraint, createCardinalityConstraint, createLits, createPseudoBooleanConstraint, createUnregisteredAtLeastConstraint, createUnregisteredAtMostConstraint, createUnregisteredCardinalityConstraint, createUnregisteredPseudoBooleanConstraint, getNormalizer, setNormalizer, setNormalizer

Methods inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory

conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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

conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener

Method Detail

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory

Overrides:

createClause in class AbstractPBDataStructureFactory

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.

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)

Specified by:

createUnregisteredClause in interface DataStructureFactory

Overrides:

createUnregisteredClause in class AbstractPBDataStructureFactory

constraintFactory

protected Constr constraintFactory(int[] literals,
                                   java.math.BigInteger[] coefs,
                                   java.math.BigInteger degree)
                            throws ContradictionException

Specified by:

constraintFactory in class AbstractPBDataStructureFactory

Throws:

ContradictionException

learntConstraintFactory

protected Constr learntConstraintFactory(IDataStructurePB dspb)

Specified by:

learntConstraintFactory in class AbstractPBDataStructureFactory

learntAtLeastConstraintFactory

protected Constr learntAtLeastConstraintFactory(IVecInt literals,
                                                IVec<java.math.BigInteger> coefs,
                                                java.math.BigInteger degree)

Specified by:

learntAtLeastConstraintFactory in class AbstractPBDataStructureFactory

learntAtMostConstraintFactory

protected Constr learntAtMostConstraintFactory(IVecInt literals,
                                               IVec<java.math.BigInteger> coefs,
                                               java.math.BigInteger degree)

Specified by:

learntAtMostConstraintFactory in class AbstractPBDataStructureFactory

constructClause

protected Constr constructClause(IVecInt v)

constructCard

protected Constr constructCard(IVecInt theLits,
                               int degree)
                        throws ContradictionException

Throws:

ContradictionException

constructPB

protected Constr constructPB(int[] theLits,
                             java.math.BigInteger[] coefs,
                             java.math.BigInteger degree)
                      throws ContradictionException

Throws:

ContradictionException

constructLearntClause

protected Constr constructLearntClause(IVecInt literals)

constructLearntCard

protected Constr constructLearntCard(IDataStructurePB dspb)

constructLearntCard

protected Constr constructLearntCard(IVecInt literals,
                                     IVec<java.math.BigInteger> coefs,
                                     java.math.BigInteger degree)

constructLearntPB

protected Constr constructLearntPB(IDataStructurePB dspb)

constructLearntPB

protected Constr constructLearntPB(IVecInt literals,
                                   IVec<java.math.BigInteger> coefs,
                                   java.math.BigInteger degree)

sumOfCoefficients

public static final java.math.BigInteger sumOfCoefficients(java.math.BigInteger[] coefs)