org.sat4j.minisat.constraints
Class ClausalDataStructureCBWL

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory
      org.sat4j.minisat.constraints.ClausalDataStructureCBWL

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory

public class ClausalDataStructureCBWL
extends AbstractDataStructureFactory

Author:

leberre Uses Counter Based data strcuture for the original clausal in the database and uses Watched Literals Data structure for learned clauses.

See Also:

Serialized Form

Constructor Summary

ClausalDataStructureCBWL()

Method Summary

Constr	createClause(IVecInt literals)
Constr	createUnregisteredClause(IVecInt literals)

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

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

Methods inherited from class java.lang.Object

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

Constructor Detail

ClausalDataStructureCBWL

public ClausalDataStructureCBWL()

Method Detail

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.

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)