org.sat4j.minisat.constraints
Class ClausalDataStructureCBWL
java.lang.Object
org.sat4j.minisat.constraints.AbstractDataStructureFactory
org.sat4j.minisat.constraints.ClausalDataStructureCBWL
- All Implemented Interfaces:
- 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
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
ClausalDataStructureCBWL
public ClausalDataStructureCBWL()
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.