org.sat4j.pb.constraints

Class AbstractPBDataStructureFactory

java.lang.Object

org.sat4j.minisat.constraints.AbstractDataStructureFactory

org.sat4j.pb.constraints.AbstractPBDataStructureFactory

All Implemented Interfaces:

Serializable, DataStructureFactory, PBDataStructureFactory

Direct Known Subclasses:

AbstractPBClauseCardConstrDataStructure, PBMaxDataStructure, PBMinDataStructure, PuebloPBMinDataStructure

public abstract class AbstractPBDataStructureFactory
extends AbstractDataStructureFactory
implements PBDataStructureFactory

Author:

leberre To change the template for this generated type comment go to Window>Preferences>Java>Code Generation>Code and Comments

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer	FOR_COMPETITION
static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer	NO_COMPETITION

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

learner, lits, solver

Constructor Summary

Constructors

Constructor and Description
AbstractPBDataStructureFactory()

Method Summary

Methods

Modifier and Type	Method and Description
protected abstract Constr	constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
Constr	createAtLeastPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	createAtMostPBConstraint(IVecInt literals, IVec<BigInteger> coefs, 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<BigInteger> coefs, boolean moreThan, BigInteger degree)
Constr	createUnregisteredAtLeastConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	createUnregisteredAtMostConstraint(IVecInt literals, IVec<BigInteger> coefs, 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<BigInteger> coefs, BigInteger degree)
protected abstract Constr	learntAtMostConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected abstract Constr	learntConstraintFactory(IDataStructurePB dspb)
void	setNormalizer(org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer normalizer)
void	setNormalizer(String simp)

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

Field Detail

FOR_COMPETITION

public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer FOR_COMPETITION

NO_COMPETITION

public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer NO_COMPETITION

Constructor Detail

AbstractPBDataStructureFactory

public AbstractPBDataStructureFactory()

Method Detail

getNormalizer

protected org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer getNormalizer()

setNormalizer

public void setNormalizer(String simp)

setNormalizer

public void setNormalizer(org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer normalizer)

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory

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

createCardinalityConstraint

public Constr createCardinalityConstraint(IVecInt literals,
                                 int degree)
                                   throws ContradictionException

Description copied from interface: DataStructureFactory

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

Specified by:

createCardinalityConstraint in interface DataStructureFactory

Overrides:

createCardinalityConstraint in class AbstractDataStructureFactory

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

createPseudoBooleanConstraint

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

Specified by:

createPseudoBooleanConstraint in interface PBDataStructureFactory

Throws:

ContradictionException

createAtMostPBConstraint

public Constr createAtMostPBConstraint(IVecInt literals,
                              IVec<BigInteger> coefs,
                              BigInteger degree)
                                throws ContradictionException

Specified by:

createAtMostPBConstraint in interface PBDataStructureFactory

Throws:

ContradictionException

createAtLeastPBConstraint

public Constr createAtLeastPBConstraint(IVecInt literals,
                               IVec<BigInteger> coefs,
                               BigInteger degree)
                                 throws ContradictionException

Specified by:

createAtLeastPBConstraint in interface PBDataStructureFactory

Throws:

ContradictionException

createUnregisteredPseudoBooleanConstraint

public Constr createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)

Specified by:

createUnregisteredPseudoBooleanConstraint in interface PBDataStructureFactory

createUnregisteredAtLeastConstraint

public Constr createUnregisteredAtLeastConstraint(IVecInt literals,
                                         IVec<BigInteger> coefs,
                                         BigInteger degree)

Specified by:

createUnregisteredAtLeastConstraint in interface PBDataStructureFactory

createUnregisteredAtMostConstraint

public Constr createUnregisteredAtMostConstraint(IVecInt literals,
                                        IVec<BigInteger> coefs,
                                        BigInteger degree)

Specified by:

createUnregisteredAtMostConstraint in interface PBDataStructureFactory

constraintFactory

protected abstract Constr constraintFactory(int[] literals,
                       BigInteger[] coefs,
                       BigInteger degree)
                                     throws ContradictionException

Throws:

ContradictionException

learntConstraintFactory

protected abstract Constr learntConstraintFactory(IDataStructurePB dspb)

learntAtLeastConstraintFactory

protected abstract Constr learntAtLeastConstraintFactory(IVecInt literals,
                                    IVec<BigInteger> coefs,
                                    BigInteger degree)

learntAtMostConstraintFactory

protected abstract Constr learntAtMostConstraintFactory(IVecInt literals,
                                   IVec<BigInteger> coefs,
                                   BigInteger degree)

createLits

protected ILits createLits()

Specified by:

createLits in class AbstractDataStructureFactory

createUnregisteredCardinalityConstraint

public Constr createUnregisteredCardinalityConstraint(IVecInt literals,
                                             int degree)

Specified by:

createUnregisteredCardinalityConstraint in interface DataStructureFactory

Overrides:

createUnregisteredCardinalityConstraint in class AbstractDataStructureFactory