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.

public class DependencyHelper<T,C>
extends java.lang.Object

Helper class intended to make life easier to people to feed a sat solver programmatically.

Author:

daniel

Field Summary

boolean	explanationEnabled
INegator<T>	NO_NEGATION

Constructor Summary

DependencyHelper(IPBSolver solver)

DependencyHelper(IPBSolver solver, boolean explanationEnabled)

Method Summary

void	addToObjectiveFunction(T thing, java.math.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)
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)
DisjunctionRHS<T,C>	disjunction(T... lhs)
boolean	getBooleanValueFor(T t) Retrieve the boolean value associated with a domain object in the solution found by the solver.
int	getNumberOfConstraints()
int	getNumberOfVariables()
java.lang.String	getObjectiveFunction()
IVec<T>	getSolution() Retrieve the solution found.
java.math.BigInteger	getSolutionCost()
boolean	hasASolution()
boolean	hasASolution(java.util.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	or(C name, T thing, T... otherThings) Create a constraint of the form thing <=> (thing1 or thing 2 ... or thingn)
void	setFalse(T thing, C name) Add a constraint to set the value of a domain object to false.
void	setNegator(INegator<T> 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.
java.util.Set<C>	why() Explain the reason of the inconsistency of the set of constraints.
java.util.Set<C>	why(T thing) Explain a domain object has been set to true in a solution.
java.util.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 final INegator<T> NO_NEGATION

explanationEnabled

public boolean explanationEnabled

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)

Method Detail

setNegator

public void setNegator(INegator<T> negator)

getSolution

public IVec<T> getSolution()

Retrieve the solution found. 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()}

getSolutionCost

public java.math.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.

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(java.util.Collection<T> assumps)
                     throws TimeoutException

Returns:

true if the set of constraints entered inside the solver can be satisfied.

Throws:

TimeoutException

why

public java.util.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 java.util.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 java.util.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)

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

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

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,
                                   java.math.BigInteger weight)

Add a weighted literal to the objective function.

Parameters:

thing -

weight -

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

getObjectiveFunction

public java.lang.String getObjectiveFunction()

getNumberOfVariables

public int getNumberOfVariables()

getNumberOfConstraints

public int getNumberOfConstraints()