org.sat4j.minisat.constraints

Class MixedDataStructureSingleWL

java.lang.Object

org.sat4j.minisat.constraints.AbstractDataStructureFactory

org.sat4j.minisat.constraints.MixedDataStructureSingleWL

All Implemented Interfaces:

Serializable, DataStructureFactory

public class MixedDataStructureSingleWL
extends AbstractDataStructureFactory

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

Constructors

Constructor and Description
MixedDataStructureSingleWL()

Method Summary

Methods

Modifier and Type	Method and Description
Constr	createCardinalityConstraint(IVecInt literals, int degree) Create a cardinality constraint of the form sum li >= degree.
Constr	createClause(IVecInt literals)
protected ILits	createLits()
Constr	createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
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

MixedDataStructureSingleWL

public MixedDataStructureSingleWL()

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

createUnregisteredCardinalityConstraint

public Constr createUnregisteredCardinalityConstraint(IVecInt literals,
                                             int degree)

Specified by:

createUnregisteredCardinalityConstraint in interface DataStructureFactory

Overrides:

createUnregisteredCardinalityConstraint in class AbstractDataStructureFactory

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