org.sat4j.minisat.constraints
Class MixedDataStructureDanielCBWL

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory
      org.sat4j.minisat.constraints.MixedDataStructureDanielWL
          org.sat4j.minisat.constraints.MixedDataStructureDanielCBWL

All Implemented Interfaces:

Serializable, DataStructureFactory

public class MixedDataStructureDanielCBWL
extends MixedDataStructureDanielWL

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.MixedDataStructureDanielWL

createCardinalityConstraint, createLits, createUnregisteredClause

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

Constructor Detail

MixedDataStructureDanielCBWL

public MixedDataStructureDanielCBWL()

Method Detail

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory

Overrides:

createClause in class MixedDataStructureDanielWL

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.