org.sat4j.minisat.constraints
Class MixedDataStructureDanielCBHT

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits>
      org.sat4j.minisat.constraints.MixedDataStructureDaniel
          org.sat4j.minisat.constraints.MixedDataStructureDanielCBHT

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory<ILits>

public class MixedDataStructureDanielCBHT
extends MixedDataStructureDaniel

See Also:

Serialized Form

Field Summary

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

learner, lits, solver

Constructor Summary

MixedDataStructureDanielCBHT()

Method Summary

Constr

createClause(IVecInt literals)

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

createCardinalityConstraint, createLits, createUnregisteredClause

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

conflictDetectedInAttachesFor, getAttachesFor, getVocabulary, learnConstraint, reset, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

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

Constructor Detail

MixedDataStructureDanielCBHT

public MixedDataStructureDanielCBHT()

Method Detail

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory<ILits>

Overrides:

createClause in class MixedDataStructureDaniel

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.