org.sat4j.minisat.constraints
Class CardinalityDataStructure

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits>
      org.sat4j.minisat.constraints.AbstractCardinalityDataStructure
          org.sat4j.minisat.constraints.CardinalityDataStructure

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory<ILits>

public class CardinalityDataStructure
extends AbstractCardinalityDataStructure

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 inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory

learner, lits, solver

Constructor Summary

CardinalityDataStructure()

Method Summary

Constr	createCardinalityConstraint(IVecInt literals, int degree)
Constr	createClause(IVecInt literals)
Constr	createUnregisteredClause(IVecInt literals)

Methods inherited from class org.sat4j.minisat.constraints.AbstractCardinalityDataStructure

coefficientsEqualToOne, createLits, createPseudoBooleanConstraint

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

conflictDetectedInWatchesFor, createUnregisteredPseudoBooleanConstraint, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

CardinalityDataStructure

public CardinalityDataStructure()

Method Detail

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

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.

createCardinalityConstraint

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

Specified by:

createCardinalityConstraint in interface DataStructureFactory<ILits>

Overrides:

createCardinalityConstraint in class AbstractDataStructureFactory<ILits>

Throws:

ContradictionException