org.sat4j.tools
Class ClausalCardinalitiesDecorator<T extends ISolver>

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<T>
      extended by org.sat4j.tools.ClausalCardinalitiesDecorator<T>
Type Parameters:
T -
All Implemented Interfaces:
Serializable, IProblem, ISolver

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
ClausalCardinalitiesDecorator(T solver)
           
ClausalCardinalitiesDecorator(T solver, EncodingStrategyAdapter encodingAd)
           
 
Method Summary
 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, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, 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.


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.