org.sat4j.minisat.constraints
Class ClausalDataStructureWL

java.lang.Object
  extended by org.sat4j.minisat.constraints.AbstractDataStructureFactory
      extended by org.sat4j.minisat.constraints.ClausalDataStructureWL
All Implemented Interfaces:
Serializable, DataStructureFactory

public class ClausalDataStructureWL
extends AbstractDataStructureFactory

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
ClausalDataStructureWL()
           
 
Method Summary
 Constr createClause(IVecInt literals)
           
protected  ILits createLits()
           
 Constr createUnregisteredClause(IVecInt literals)
           
 
Methods inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory
conflictDetectedInWatchesFor, createCardinalityConstraint, 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

ClausalDataStructureWL

public ClausalDataStructureWL()
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)

createLits

protected ILits createLits()
Specified by:
createLits in class AbstractDataStructureFactory


Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.