DependencyHelper (SAT4J pseudo 2.3.3 API)

java.lang.Object
- org.sat4j.pb.tools.DependencyHelper<T,C>

Type Parameters:
T - The class of the objects to map into boolean variables.
C - The class of the object to map to each constraint.

Direct Known Subclasses:

LexicoHelper
```
public class DependencyHelper<T,C>
extends Object
```
Helper class intended to make life easier to people to feed a sat solver programmatically.

Author:

daniel

Field Summary

Fields
Modifier and Type Field and Description

static INegator BASIC_NEGATION

static INegator NO_NEGATION

Fields
Modifier and Type	Field and Description
`static INegator`	`BASIC_NEGATION`
`static INegator`	`NO_NEGATION`

Constructor Summary

Constructors
Constructor and Description
`DependencyHelper(IPBSolver solver)`
`DependencyHelper(IPBSolver solver, boolean explanationEnabled)`
`DependencyHelper(IPBSolver solver, boolean explanationEnabled, boolean canonicalOptFunctionEnabled)`

Method Summary

Methods
Modifier and Type	Method and Description
`void`	`addToObjectiveFunction(T thing, BigInteger weight)` Add a weighted literal to the objective function.
`void`	`addToObjectiveFunction(T thing, int weight)` Add a weighted literal to the objective function.
`void`	`and(C name, T thing, T... otherThings)` Create a constraint of the form thing <=> (thing1 and thing 2 ... and thingn)
`void`	`atLeast(C name, BigInteger degree, WeightedObject<T>... wobj)` Create a PB constraint of the form `w1.l1 + w2.l2 + ... wn.ln >= degree` where wi are position integers and li are domain objects.
`void`	`atLeast(C name, int i, T... things)` Create a constraint stating that at most i domain object should be set to true.
`void`	`atMost(C name, BigInteger degree, WeightedObject<T>... wobj)` Create a PB constraint of the form `w1.l1 + w2.l2 + ... wn.ln <= degree` where wi are position integers and li are domain objects.
`void`	`atMost(C name, int i, T... things)` Create a constraint stating that at most i domain object should be set to true.
`void`	`atMost(C name, int degree, WeightedObject<T>... wobj)`
`ImplicationNamer<T,C>`	`atMost(int i, T... things)` Create a constraint stating that at most i domain object should be set to true.
`void`	`clause(C name, T... things)` Create a clause (thing1 or thing 2 ... or thingn)
`void`	`discard(IVec<T> things)`
`void`	`discardSolutionsWithObjectiveValueGreaterThan(long value)`
`DisjunctionRHS<T,C>`	`disjunction(T... lhs)`
`Collection<T>`	`getASolution()` Retrieve a collection of objects satisfying the constraints.
`boolean`	`getBooleanValueFor(T t)` Retrieve the boolean value associated with a domain object in the solution found by the solver.
`protected int`	`getIntValue(T thing)` Translate a domain object into a dimacs variable.
`protected int`	`getIntValue(T thing, boolean create)` Translate a domain object into a dimacs variable.
`Map<Integer,T>`	`getMappingToDomain()`
`int`	`getNumberOfConstraints()`
`int`	`getNumberOfVariables()`
`String`	`getObjectiveFunction()`
`IVec<T>`	`getSolution()` Retrieve the solution found.
`BigInteger`	`getSolutionCost()`
`IPBSolver`	`getSolver()`
`void`	`halfOr(C name, T thing, T... otherThings)` Create a constraint of the form thing <= (thing1 or thing 2 ... or thingn)
`boolean`	`hasASolution()`
`boolean`	`hasASolution(Collection<T> assumps)`
`boolean`	`hasASolution(IVec<T> assumps)`
`void`	`iff(C name, T thing, T... otherThings)` Create a constraint using equivalency chains thing <=> (thing1 <=> thing2 <=> ... <=> thingn)
`void`	`ifThenElse(C name, T thing, T conditionThing, T thenThing, T elseThing)` Create a constraint of the form thing <=> (if conditionThing then thenThing else elseThing)
`ImplicationRHS<T,C>`	`implication(T... lhs)` Create a logical implication of the form lhs -> rhs
`void`	`impliedBy(Collection<T> assumptions, Collection<T> satisfied, Collection<T> falsified)` Compute the objects implied by the assumptions.
`Object`	`not(T thing)`
`void`	`or(C name, T thing, T... otherThings)` Create a constraint of the form thing <=> (thing1 or thing 2 ... or thingn)
`void`	`reset()` Reset the state of the helper (mapping, objective function, etc).
`void`	`setFalse(T thing, C name)` Add a constraint to set the value of a domain object to false.
`void`	`setNegator(INegator negator)`
`void`	`setObjectiveFunction(WeightedObject<T>... wobj)` Add an objective function to ask for a solution that minimize the objective function.
`void`	`setTrue(T thing, C name)` Add a constraint to set the value of a domain object to true.
`void`	`stopExplanation()` Stop the explanation computation.
`void`	`stopSolver()` Stop the SAT solver that is looking for a solution.
`Set<C>`	`why()` Explain the reason of the inconsistency of the set of constraints.
`Set<C>`	`why(T thing)` Explain a domain object has been set to true in a solution.
`Set<C>`	`whyNot(T thing)` Explain a domain object has been set to false in a solution.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - NO_NEGATION
```
public static final INegator NO_NEGATION
```
  - BASIC_NEGATION
```
public static final INegator BASIC_NEGATION
```
- Constructor Detail
  - DependencyHelper
```
public DependencyHelper(IPBSolver solver)
```
    Parameters:
    solver - the solver to be used to solve the problem.
  - DependencyHelper
```
public DependencyHelper(IPBSolver solver,
                boolean explanationEnabled)
```
    Parameters:
    solver - the solver to be used to solve the problem.
    explanationEnabled - if true, will add one new variable per constraint to allow the solver to compute an explanation in case of failure. Default is true. Usually, this is set to false when one wants to check the encoding produced by the helper.
  - DependencyHelper
```
public DependencyHelper(IPBSolver solver,
                boolean explanationEnabled,
                boolean canonicalOptFunctionEnabled)
```
    Parameters:
    solver - the solver to be used to solve the problem.
    explanationEnabled - if true, will add one new variable per constraint to allow the solver to compute an explanation in case of failure. Default is true. Usually, this is set to false when one wants to check the encoding produced by the helper.
    canonicalOptFunctionEnabled - when set to true, the objective function sum up all the coefficients for a given literal. The default is true. It is useful to set it to false when checking the encoding produced by the helper.
    Since:
    
    2.2
- Method Detail
  - setNegator
```
public void setNegator(INegator negator)
```
  - getIntValue
```
protected int getIntValue(T thing)
```
    Translate a domain object into a dimacs variable.
    
    Parameters:
    thing - a domain object
    
    Returns:
    the dimacs variable (an integer) representing that domain object.
  - getIntValue
```
protected int getIntValue(T thing,
              boolean create)
```
    Translate a domain object into a dimacs variable.
    
    Parameters:
    thing - a domain object
    create - to allow or not the solver to create a new id if the object in unknown. If set to false, the method will throw an IllegalArgumentException if the object is unknown.
    
    Returns:
    the dimacs variable (an integer) representing that domain object.
  - getSolution
```
public IVec<T> getSolution()
```
    Retrieve the solution found. Note that this method returns a Sat4j specific data structure (IVec). People willing to retrieve a more common data structure should use getASolution() instead. THAT METHOD IS EXPECTED TO BE CALLED IF hasASolution() RETURNS TRUE.
    
    Returns:
    the domain object that must be satisfied to satisfy the constraints entered in the solver.
    See Also:
    #hasASolution()}, #getASolution()}
  - getASolution
```
public Collection<T> getASolution()
```
    Retrieve a collection of objects satisfying the constraints. It behaves basically the same as getSolution() but returns a common Collection instead of a Sat4j specific IVec. THAT METHOD IS EXPECTED TO BE CALLED IF hasASolution() RETURNS TRUE.
    
    Returns:
    the domain object that must be satisfied to satisfy the constraints entered in the solver.
    Since:
    
    2.3.1
    
    See Also:
    #hasASolution()}, #getSolution()}
  - getSolutionCost
```
public BigInteger getSolutionCost()
```
  - getBooleanValueFor
```
public boolean getBooleanValueFor(T t)
```
    Retrieve the boolean value associated with a domain object in the solution found by the solver. THAT METHOD IS EXPECTED TO BE CALLED IF hasASolution() RETURNS TRUE.
    
    Parameters:
    t - a domain object
    
    Returns:
    true iff the domain object has been set to true in the current solution.
    
    Throws:
    
    IllegalArgumentException - If the argument of the method is unknown to the solver.
  - hasASolution
```
public boolean hasASolution()
                     throws TimeoutException
```
    Returns:
    true if the set of constraints entered inside the solver can be satisfied.
    
    Throws:
    
    TimeoutException
  - hasASolution
```
public boolean hasASolution(IVec<T> assumps)
                     throws TimeoutException
```
    Returns:
    true if the set of constraints entered inside the solver can be satisfied.
    
    Throws:
    
    TimeoutException
  - hasASolution
```
public boolean hasASolution(Collection<T> assumps)
                     throws TimeoutException
```
    Returns:
    true if the set of constraints entered inside the solver can be satisfied.
    
    Throws:
    
    TimeoutException
  - why
```
public Set<C> why()
           throws TimeoutException
```
    Explain the reason of the inconsistency of the set of constraints. THAT METHOD IS EXPECTED TO BE CALLED IF hasASolution() RETURNS FALSE.
    
    Returns:
    a set of objects used to "name" each constraint entered in the solver.
    
    Throws:
    
    TimeoutException
    See Also:
    #hasASolution()}
  - why
```
public Set<C> why(T thing)
           throws TimeoutException
```
    Explain a domain object has been set to true in a solution.
    
    Returns:
    a set of objects used to "name" each constraint entered in the solver.
    
    Throws:
    
    TimeoutException
    See Also:
    #hasASolution()}
  - whyNot
```
public Set<C> whyNot(T thing)
              throws TimeoutException
```
    Explain a domain object has been set to false in a solution.
    
    Returns:
    a set of objects used to "name" each constraint entered in the solver.
    
    Throws:
    
    TimeoutException
    See Also:
    #hasASolution()}
  - setTrue
```
public void setTrue(T thing,
           C name)
             throws ContradictionException
```
    Add a constraint to set the value of a domain object to true.
    
    Parameters:
    thing - the domain object
    name - the name of the constraint, to be used in an explanation if needed.
    
    Throws:
    
    ContradictionException - if the set of constraints appears to be trivially inconsistent.
  - setFalse
```
public void setFalse(T thing,
            C name)
              throws ContradictionException
```
    Add a constraint to set the value of a domain object to false.
    
    Parameters:
    thing - the domain object
    name - the name of the constraint, to be used in an explanation if needed.
    
    Throws:
    
    ContradictionException - if the set of constraints appears to be trivially inconsistent.
  - implication
```
public ImplicationRHS<T,C> implication(T... lhs)
```
    Create a logical implication of the form lhs -> rhs
    
    Parameters:
    lhs - some domain objects. They form a conjunction in the left hand side of the implication.
    
    Returns:
    the right hand side of the implication.
  - disjunction
```
public DisjunctionRHS<T,C> disjunction(T... lhs)
```
  - atLeast
```
public void atLeast(C name,
           int i,
           T... things)
             throws ContradictionException
```
    Create a constraint stating that at most i domain object should be set to true.
    
    Parameters:
    i - the maximum number of domain object to set to true.
    things - the domain objects.
    
    Throws:
    
    ContradictionException
  - atMost
```
public ImplicationNamer<T,C> atMost(int i,
                           T... things)
                             throws ContradictionException
```
    Create a constraint stating that at most i domain object should be set to true.
    
    Parameters:
    i - the maximum number of domain object to set to true.
    things - the domain objects.
    
    Returns:
    an object used to name the constraint. The constraint MUST BE NAMED.
    
    Throws:
    
    ContradictionException
  - atMost
```
public void atMost(C name,
          int i,
          T... things)
            throws ContradictionException
```
    Create a constraint stating that at most i domain object should be set to true.
    
    Parameters:
    i - the maximum number of domain object to set to true.
    things - the domain objects.
    
    Throws:
    
    ContradictionException
  - clause
```
public void clause(C name,
          T... things)
            throws ContradictionException
```
    Create a clause (thing1 or thing 2 ... or thingn)
    
    Parameters:
    name -
    things -
    
    Throws:
    
    ContradictionException
  - iff
```
public void iff(C name,
       T thing,
       T... otherThings)
         throws ContradictionException
```
    Create a constraint using equivalency chains thing <=> (thing1 <=> thing2 <=> ... <=> thingn)
    
    Parameters:
    thing - a domain object
    things - other domain objects.
    
    Throws:
    
    ContradictionException
  - and
```
public void and(C name,
       T thing,
       T... otherThings)
         throws ContradictionException
```
    Create a constraint of the form thing <=> (thing1 and thing 2 ... and thingn)
    
    Parameters:
    name -
    thing -
    otherThings -
    
    Throws:
    
    ContradictionException
  - or
```
public void or(C name,
      T thing,
      T... otherThings)
        throws ContradictionException
```
    Create a constraint of the form thing <=> (thing1 or thing 2 ... or thingn)
    
    Parameters:
    name -
    thing -
    otherThings -
    
    Throws:
    
    ContradictionException
  - halfOr
```
public void halfOr(C name,
          T thing,
          T... otherThings)
            throws ContradictionException
```
    Create a constraint of the form thing <= (thing1 or thing 2 ... or thingn)
    
    Parameters:
    name -
    thing -
    otherThings -
    
    Throws:
    
    ContradictionException
  - ifThenElse
```
public void ifThenElse(C name,
              T thing,
              T conditionThing,
              T thenThing,
              T elseThing)
                throws ContradictionException
```
    Create a constraint of the form thing <=> (if conditionThing then thenThing else elseThing)
    
    Parameters:
    name -
    thing -
    otherThings -
    
    Throws:
    
    ContradictionException
  - setObjectiveFunction
```
public void setObjectiveFunction(WeightedObject<T>... wobj)
```
    Add an objective function to ask for a solution that minimize the objective function.
    
    Parameters:
    wobj - a set of weighted objects (pairs of domain object and BigInteger).
  - addToObjectiveFunction
```
public void addToObjectiveFunction(T thing,
                          int weight)
```
    Add a weighted literal to the objective function.
    
    Parameters:
    thing -
    weight -
  - addToObjectiveFunction
```
public void addToObjectiveFunction(T thing,
                          BigInteger weight)
```
    Add a weighted literal to the objective function.
    
    Parameters:
    thing -
    weight -
  - atLeast
```
public void atLeast(C name,
           BigInteger degree,
           WeightedObject<T>... wobj)
             throws ContradictionException
```
    Create a PB constraint of the form w1.l1 + w2.l2 + ... wn.ln >= degree where wi are position integers and li are domain objects.
    
    Parameters:
    degree -
    wobj -
    
    Throws:
    
    ContradictionException
  - atMost
```
public void atMost(C name,
          BigInteger degree,
          WeightedObject<T>... wobj)
            throws ContradictionException
```
    Create a PB constraint of the form w1.l1 + w2.l2 + ... wn.ln <= degree where wi are position integers and li are domain objects.
    
    Parameters:
    degree -
    wobj -
    
    Throws:
    
    ContradictionException
  - atMost
```
public void atMost(C name,
          int degree,
          WeightedObject<T>... wobj)
            throws ContradictionException
```
    Throws:
    
    ContradictionException
  - stopSolver
```
public void stopSolver()
```
    Stop the SAT solver that is looking for a solution. The solver will throw a TimeoutException.
  - stopExplanation
```
public void stopExplanation()
```
    Stop the explanation computation. A TimeoutException will be thrown by the explanation algorithm.
  - discard
```
public void discard(IVec<T> things)
             throws ContradictionException
```
    Throws:
    
    ContradictionException
  - discardSolutionsWithObjectiveValueGreaterThan
```
public void discardSolutionsWithObjectiveValueGreaterThan(long value)
                                                   throws ContradictionException
```
    Throws:
    
    ContradictionException
  - getObjectiveFunction
```
public String getObjectiveFunction()
```
  - getNumberOfVariables
```
public int getNumberOfVariables()
```
  - getNumberOfConstraints
```
public int getNumberOfConstraints()
```
  - getMappingToDomain
```
public Map<Integer,T> getMappingToDomain()
```
  - not
```
public Object not(T thing)
```
  - getSolver
```
public IPBSolver getSolver()
```
    Returns:
    the IPBSolver enclosed in the helper.
    Since:
    
    2.2
  - reset
```
public void reset()
```
    Reset the state of the helper (mapping, objective function, etc).
    
    Since:
    
    2.3.1
  - impliedBy
```
public void impliedBy(Collection<T> assumptions,
             Collection<T> satisfied,
             Collection<T> falsified)
               throws TimeoutException
```
    Compute the objects implied by the assumptions.
    
    Parameters:
    assumptions - already satisfied objects (e.g. user choices)
    satisfied - the objects that are always satisfied under assumptions (includes the objects from assumptions)
    falsified - the objects that are always falsified under assumptions.
    
    Throws:
    
    TimeoutException
    Since:
    
    2.3.3

Class DependencyHelper<T,C>

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

NO_NEGATION

BASIC_NEGATION

Constructor Detail

DependencyHelper

DependencyHelper

DependencyHelper

Method Detail

setNegator

getIntValue

getIntValue

getSolution

getASolution

getSolutionCost

getBooleanValueFor

hasASolution

hasASolution

hasASolution

why

why

whyNot

setTrue

setFalse

implication

disjunction

atLeast

atMost

atMost

clause

iff

and

or

halfOr

ifThenElse

setObjectiveFunction

addToObjectiveFunction

addToObjectiveFunction

atLeast

atMost

atMost

stopSolver

stopExplanation

discard

discardSolutionsWithObjectiveValueGreaterThan

getObjectiveFunction

getNumberOfVariables

getNumberOfConstraints

getMappingToDomain

not

getSolver

reset

impliedBy