public abstract class AbstractPBDataStructureFactory extends AbstractDataStructureFactory implements PBDataStructureFactory
Modifier and Type | Field and Description |
---|---|
static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer |
FOR_COMPETITION |
static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer |
NO_COMPETITION |
learner, lits, solver
Constructor and Description |
---|
AbstractPBDataStructureFactory() |
Modifier and Type | Method and Description |
---|---|
protected abstract Constr |
constraintFactory(int[] literals,
java.math.BigInteger[] coefs,
java.math.BigInteger degree) |
Constr |
createAtLeastPBConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
Constr |
createAtMostPBConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
Constr |
createCardinalityConstraint(IVecInt literals,
int degree)
Create a cardinality constraint of the form sum li >= degree.
|
Constr |
createClause(IVecInt literals) |
protected ILits |
createLits() |
Constr |
createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree) |
Constr |
createUnregisteredAtLeastConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
Constr |
createUnregisteredAtMostConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
Constr |
createUnregisteredCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
createUnregisteredClause(IVecInt literals) |
Constr |
createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb) |
protected org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer |
getNormalizer() |
protected abstract Constr |
learntAtLeastConstraintFactory(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
protected abstract Constr |
learntAtMostConstraintFactory(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree) |
protected abstract Constr |
learntConstraintFactory(IDataStructurePB dspb) |
void |
setNormalizer(org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer normalizer) |
void |
setNormalizer(java.lang.String simp) |
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 static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer FOR_COMPETITION
public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer NO_COMPETITION
protected org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer getNormalizer()
public void setNormalizer(java.lang.String simp)
public void setNormalizer(org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer normalizer)
public Constr createClause(IVecInt literals) throws ContradictionException
createClause
in interface DataStructureFactory
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
public Constr createCardinalityConstraint(IVecInt literals, int degree) throws ContradictionException
DataStructureFactory
createCardinalityConstraint
in interface DataStructureFactory
createCardinalityConstraint
in class AbstractDataStructureFactory
literals
- a set of literals.degree
- the degree of the cardinality constraint.ContradictionException
public Constr createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree) throws ContradictionException
createPseudoBooleanConstraint
in interface PBDataStructureFactory
ContradictionException
public Constr createAtMostPBConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree) throws ContradictionException
createAtMostPBConstraint
in interface PBDataStructureFactory
ContradictionException
public Constr createAtLeastPBConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree) throws ContradictionException
createAtLeastPBConstraint
in interface PBDataStructureFactory
ContradictionException
public Constr createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)
createUnregisteredPseudoBooleanConstraint
in interface PBDataStructureFactory
public Constr createUnregisteredAtLeastConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
createUnregisteredAtLeastConstraint
in interface PBDataStructureFactory
public Constr createUnregisteredAtMostConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
createUnregisteredAtMostConstraint
in interface PBDataStructureFactory
protected abstract Constr constraintFactory(int[] literals, java.math.BigInteger[] coefs, java.math.BigInteger degree) throws ContradictionException
ContradictionException
protected abstract Constr learntConstraintFactory(IDataStructurePB dspb)
protected abstract Constr learntAtLeastConstraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected abstract Constr learntAtMostConstraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected ILits createLits()
createLits
in class AbstractDataStructureFactory
public Constr createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
createUnregisteredCardinalityConstraint
in interface DataStructureFactory
createUnregisteredCardinalityConstraint
in class AbstractDataStructureFactory