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:

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

protected Constr	constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
protected Constr	constructCard(IVecInt theLits, int degree)
protected Constr	constructClause(IVecInt v)
protected Constr	constructLearntCard(IDataStructurePB dspb)
protected Constr	constructLearntClause(IVecInt literals)
protected Constr	constructLearntPB(IDataStructurePB dspb)
protected Constr	constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	createClause(IVecInt literals)
Constr	createUnregisteredClause(IVecInt literals)
protected Constr	learntConstraintFactory(IDataStructurePB dspb)

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

createCardinalityConstraint, createLits, createPseudoBooleanConstraint, 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,
                                   BigInteger[] coefs,
                                   BigInteger degree)
                            throws ContradictionException

Specified by:

constraintFactory in class AbstractPBDataStructureFactory

Throws:

ContradictionException

learntConstraintFactory

protected Constr learntConstraintFactory(IDataStructurePB dspb)

Specified by:

learntConstraintFactory 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,
                             BigInteger[] coefs,
                             BigInteger degree)
                      throws ContradictionException

Throws:

ContradictionException

constructLearntClause

protected Constr constructLearntClause(IVecInt literals)

constructLearntCard

protected Constr constructLearntCard(IDataStructurePB dspb)

constructLearntPB

protected Constr constructLearntPB(IDataStructurePB dspb)