org.sat4j.pb.constraints
Class CompetResolutionPBMixedHTClauseCardConstrDataStructure

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

All Implemented Interfaces:

Serializable, DataStructureFactory, PBDataStructureFactory

public class CompetResolutionPBMixedHTClauseCardConstrDataStructure
extends PBMaxClauseCardConstrDataStructure

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

CompetResolutionPBMixedHTClauseCardConstrDataStructure()

Method Summary

protected Constr	constructCard(IVecInt theLits, int degree)
protected Constr	constructClause(IVecInt v)
protected Constr	constructLearntCard(IDataStructurePB dspb)
protected Constr	constructLearntClause(IVecInt resLits)
Constr	createClause(IVecInt literals)

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

constructLearntPB, constructPB

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

CompetResolutionPBMixedHTClauseCardConstrDataStructure

public CompetResolutionPBMixedHTClauseCardConstrDataStructure()

Method Detail

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory

Overrides:

createClause in class PuebloPBMinClauseCardConstrDataStructure

Throws:

ContradictionException

constructClause

protected Constr constructClause(IVecInt v)

Overrides:

constructClause in class PuebloPBMinClauseCardConstrDataStructure

constructLearntClause

protected Constr constructLearntClause(IVecInt resLits)

Overrides:

constructLearntClause in class PuebloPBMinClauseCardConstrDataStructure

constructCard

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

Overrides:

constructCard in class PuebloPBMinClauseCardConstrDataStructure

Throws:

ContradictionException

constructLearntCard

protected Constr constructLearntCard(IDataStructurePB dspb)

Overrides:

constructLearntCard in class PuebloPBMinClauseCardConstrDataStructure