org.sat4j.minisat.constraints
Class MixedDataStructureDanielCBWL

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

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory<ILits>

public class MixedDataStructureDanielCBWL
extends MixedDataStructureDaniel

See Also:

Serialized Form

Field Summary

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

learner, lits, solver

Constructor Summary

MixedDataStructureDanielCBWL()

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

conflictDetectedInWatchesFor, createPseudoBooleanConstraint, 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

MixedDataStructureDanielCBWL

public MixedDataStructureDanielCBWL()

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.