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

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

Constructors

Constructor and Description
PuebloPBMinClauseCardConstrDataStructure()

Method Summary

Methods

Modifier and Type	Method and Description
Constr	createClause(IVecInt literals)

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

constraintFactory, constructCard, constructClause, constructLearntCard, constructLearntCard, constructLearntClause, constructLearntPB, constructLearntPB, constructPB, createUnregisteredClause, learntAtLeastConstraintFactory, learntAtMostConstraintFactory, learntConstraintFactory, sumOfCoefficients

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

createAtLeastPBConstraint, createAtMostPBConstraint, createCardinalityConstraint, createLits, createPseudoBooleanConstraint, createUnregisteredAtLeastConstraint, createUnregisteredAtMostConstraint, createUnregisteredCardinalityConstraint, 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 AbstractPBClauseCardConstrDataStructure

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.