org.sat4j.minisat.constraints
Class ClausalDataStructureCBHT

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

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory<ILits>

public class ClausalDataStructureCBHT
extends AbstractDataStructureFactory<ILits>

Uses Counter Based data strudture for the original clausal in the database and uses Head Tail Data structure for learned clauses.

Author:

leberre

See Also:

Serialized Form

Field Summary

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

learner, lits, solver

Constructor Summary

ClausalDataStructureCBHT()

Method Summary

Constr	createClause(IVecInt literals)
protected ILits	createLits()
Constr	createUnregisteredClause(IVecInt literals)

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

conflictDetectedInAttachesFor, createCardinalityConstraint, getAttachesFor, getVocabulary, learnConstraint, reset, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

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

Constructor Detail

ClausalDataStructureCBHT

public ClausalDataStructureCBHT()

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<ILits>