org.sat4j.minisat.constraints
Class MixedDataStructureDanielHT

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

public class MixedDataStructureDanielHT
extends AbstractDataStructureFactory

Uses specific data structure for cardinality constraints.

Since:
2.1
Author:
leberre
See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory
learner, lits, solver
 
Constructor Summary
MixedDataStructureDanielHT()
           
 
Method Summary
 Constr createCardinalityConstraint(IVecInt literals, int degree)
          Create a cardinality constraint of the form sum li >= degree.
 Constr createClause(IVecInt literals)
           
protected  ILits createLits()
           
 Constr createUnregisteredClause(IVecInt literals)
           
 
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

MixedDataStructureDanielHT

public MixedDataStructureDanielHT()
Method Detail

createCardinalityConstraint

public Constr createCardinalityConstraint(IVecInt literals,
                                          int degree)
                                   throws ContradictionException
Description copied from interface: DataStructureFactory
Create a cardinality constraint of the form sum li >= degree.

Specified by:
createCardinalityConstraint in interface DataStructureFactory
Overrides:
createCardinalityConstraint in class AbstractDataStructureFactory
Parameters:
literals - a set of literals.
degree - the degree of the cardinality constraint.
Returns:
a constraint stating that at least degree literals are satisfied.
Throws:
ContradictionException

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 © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.