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

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

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