org.sat4j.tools

Class ClausalCardinalitiesDecorator<T extends ISolver>

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.ClausalCardinalitiesDecorator<T>

Type Parameters:

T -

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel

public class ClausalCardinalitiesDecorator<T extends ISolver>
extends SolverDecorator<T>

A decorator for clausal cardinalities constraints.

Since:

2.3.1

Author:

stephanieroussel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
ClausalCardinalitiesDecorator(T solver)
ClausalCardinalitiesDecorator(T solver, EncodingStrategyAdapter encodingAd)

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addAtLeast(IVecInt literals, int k) Create a cardinality constraint of the type "at least n of those literals must be satisfied"
IConstr	addAtMost(IVecInt literals, int k) Create a cardinality constraint of the type "at most n of those literals must be satisfied"
IConstr	addExactly(IVecInt literals, int k) Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
String	toString()
String	toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addBlockingClause, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, unsatExplanation

Methods inherited from class java.lang.Object

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

Constructor Detail

ClausalCardinalitiesDecorator

public ClausalCardinalitiesDecorator(T solver)

ClausalCardinalitiesDecorator

public ClausalCardinalitiesDecorator(T solver,
                             EncodingStrategyAdapter encodingAd)

Method Detail

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                 int k)
                   throws ContradictionException

Description copied from interface: ISolver

Create a cardinality constraint of the type "at least n of those literals must be satisfied"

Specified by:

addAtLeast in interface ISolver

Overrides:

addAtLeast in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

k - the degree (n) of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if degree literals are not remaining unfalsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

addAtMost

public IConstr addAtMost(IVecInt literals,
                int k)
                  throws ContradictionException

Description copied from interface: ISolver

Create a cardinality constraint of the type "at most n of those literals must be satisfied"

Specified by:

addAtMost in interface ISolver

Overrides:

addAtMost in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.

k - the degree (n) of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if it contains more than degree satisfied literals after unit propagation

See Also:

ISolver.removeConstr(IConstr)

addExactly

public IConstr addExactly(IVecInt literals,
                 int k)
                   throws ContradictionException

Description copied from interface: ISolver

Create a cardinality constraint of the type "exactly n of those literals must be satisfied".

Specified by:

addExactly in interface ISolver

Overrides:

addExactly in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

k - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.

toString

public String toString()

Overrides:

toString in class SolverDecorator<T extends ISolver>

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Specified by:

toString in interface ISolver

Overrides:

toString in class SolverDecorator<T extends ISolver>

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.