org.sat4j.pb.constraints
Class PuebloPBMinClauseCardConstrDataStructure

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory
      org.sat4j.pb.constraints.AbstractPBDataStructureFactory
          org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
              org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

All Implemented Interfaces:

Serializable, DataStructureFactory, PBDataStructureFactory

Direct Known Subclasses:

PBMaxClauseCardConstrDataStructure, PBMinClauseCardConstrDataStructure, PuebloPBMinClauseAtLeastConstrDataStructure

public class PuebloPBMinClauseCardConstrDataStructure
extends AbstractPBClauseCardConstrDataStructure

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

Constructor Summary

PuebloPBMinClauseCardConstrDataStructure()

Method Summary

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)

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

constraintFactory, learntConstraintFactory

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

createCardinalityConstraint, createLits, createPseudoBooleanConstraint, createUnregisteredClause, 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

Constructor Detail

PuebloPBMinClauseCardConstrDataStructure

public PuebloPBMinClauseCardConstrDataStructure()

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.

constructClause

protected Constr constructClause(IVecInt v)

Specified by:

constructClause in class AbstractPBClauseCardConstrDataStructure

constructCard

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

Specified by:

constructCard in class AbstractPBClauseCardConstrDataStructure

Throws:

ContradictionException

constructPB

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

Specified by:

constructPB in class AbstractPBClauseCardConstrDataStructure

Throws:

ContradictionException

constructLearntClause

protected Constr constructLearntClause(IVecInt literals)

Specified by:

constructLearntClause in class AbstractPBClauseCardConstrDataStructure

constructLearntCard

protected Constr constructLearntCard(IDataStructurePB dspb)

Specified by:

constructLearntCard in class AbstractPBClauseCardConstrDataStructure

constructLearntPB

protected Constr constructLearntPB(IDataStructurePB dspb)

Specified by:

constructLearntPB in class AbstractPBClauseCardConstrDataStructure