org.sat4j.pb.tools
Class DependencyHelper<T,C>

java.lang.Object
  extended by 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
static INegator BASIC_NEGATION
           
static INegator NO_NEGATION
           
 
Constructor Summary
DependencyHelper(IPBSolver solver)
           
DependencyHelper(IPBSolver solver, boolean explanationEnabled)
           
DependencyHelper(IPBSolver solver, boolean explanationEnabled, boolean canonicalOptFunctionEnabled)
           
 
Method Summary
 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
 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


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