org.sat4j.helper
Class MappingHelper<T>

java.lang.Object
  org.sat4j.helper.MappingHelper<T>

Type Parameters:

T - The class of the objects to map into boolean variables.

public class MappingHelper<T>
extends java.lang.Object

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

Author:

daniel

Constructor Summary

MappingHelper(ISolver solver)

Method Summary

void	addAtLeast(java.util.Collection<T> x, int degree) Easy way to enter in the solver that at least degree x[i] must be satisfied.
void	addAtLeast(T[] x, int degree) Easy way to enter in the solver that at least degree x[i] must be satisfied.
void	addAtMost(java.util.Collection<T> x, int degree) Easy way to enter in the solver that at most degree x[i] must be satisfied.
void	addAtMost(T[] x, int degree) Easy way to enter in the solver that at most degree x[i] must be satisfied.
void	addConflict(java.util.Collection<T> things) Easy way to mean that a set of things are incompatible, i.e. they cannot altogether be satisfied.
void	addConflict(T... things) Easy way to mean that a set of things are incompatible, i.e. they cannot altogether be satisfied.
void	addExactlyOneOf(T... ts)
void	addImplication(T x, java.util.Collection<T> y) Easy way to feed the solver with implications.
void	addImplication(T x, T[] y) Easy way to feed the solver with a clause.
void	addImplies(java.util.Collection<T> x, T y) Easy way to feed the solver with implications.
void	addImplies(T[] x, T y) Easy way to feed the solver with implications.
void	addImplies(T x, java.util.Collection<T> y) Easy way to feed the solver with implications.
void	addImplies(T x, T y) Easy way to feed the solver with implications.
void	addImplies(T x, T[] y) Easy way to feed the solver with implications.
void	addImpliesEquivalence(T x, T y, T z) Add a constraint x -> (y <-> z).
boolean	getBooleanValueFor(T t)
IVec<T>	getSolution()
boolean	hasASolution()
void	setFalse(T... things)
void	setTrue(T... things)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

MappingHelper

public MappingHelper(ISolver solver)

Method Detail

getSolution

public IVec<T> getSolution()

getBooleanValueFor

public boolean getBooleanValueFor(T t)

hasASolution

public boolean hasASolution()
                     throws TimeoutException

Throws:

TimeoutException

addImplies

public void addImplies(T x,
                       T y)
                throws ContradictionException

Easy way to feed the solver with implications.

Parameters:

x - a thing.

y - a thing implied by x.

Throws:

ContradictionException

addImplies

public void addImplies(T[] x,
                       T y)
                throws ContradictionException

Easy way to feed the solver with implications.

Parameters:

x - an array of things such that x[i] -> y for all i.

y - a thing implied by all the x[i].

Throws:

ContradictionException

addImplies

public void addImplies(java.util.Collection<T> x,
                       T y)
                throws ContradictionException

Easy way to feed the solver with implications.

Parameters:

x - a collection of things such that x[i] -> y for all i.

y - a thing implied by all the x[i].

Throws:

ContradictionException

addImplies

public void addImplies(T x,
                       T[] y)
                throws ContradictionException

Easy way to feed the solver with implications.

Parameters:

x - a thing such that x -> y[i] for all i

y - an array of things implied by x.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addImplies

public void addImplies(T x,
                       java.util.Collection<T> y)
                throws ContradictionException

Easy way to feed the solver with implications.

Parameters:

x - a thing such that x -> y[i] for all i

y - a collection of things implied by x.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addImplication

public void addImplication(T x,
                           T[] y)
                    throws ContradictionException

Easy way to feed the solver with a clause.

Parameters:

x - a thing such that x -> y[1] ... y[n]

y - an array of things whose disjunction is implied by x.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addImplication

public void addImplication(T x,
                           java.util.Collection<T> y)
                    throws ContradictionException

Easy way to feed the solver with implications.

Parameters:

x - a thing such that x -> y[1] ... y[n]

y - a collection of things whose disjunction is implied by x.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addAtLeast

public void addAtLeast(T[] x,
                       int degree)
                throws ContradictionException

Easy way to enter in the solver that at least degree x[i] must be satisfied.

Parameters:

x - an array of things.

degree - the minimal number of elements in x that must be satisfied.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addAtLeast

public void addAtLeast(java.util.Collection<T> x,
                       int degree)
                throws ContradictionException

Easy way to enter in the solver that at least degree x[i] must be satisfied.

Parameters:

x - an array of things.

degree - the minimal number of elements in x that must be satisfied.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addAtMost

public void addAtMost(T[] x,
                      int degree)
               throws ContradictionException

Easy way to enter in the solver that at most degree x[i] must be satisfied.

Parameters:

x - an array of things.

degree - the maximal number of elements in x that must be satisfied.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addAtMost

public void addAtMost(java.util.Collection<T> x,
                      int degree)
               throws ContradictionException

Easy way to enter in the solver that at most degree x[i] must be satisfied.

Parameters:

x - an array of things.

degree - the maximal number of elements in x that must be satisfied.

Throws:

ContradictionException - if a trivial inconsistency is detected.

addExactlyOneOf

public void addExactlyOneOf(T... ts)
                     throws ContradictionException

Throws:

ContradictionException

addImpliesEquivalence

public void addImpliesEquivalence(T x,
                                  T y,
                                  T z)
                           throws ContradictionException

Add a constraint x -> (y <-> z).

Parameters:

x -

y -

z -

Throws:

ContradictionException

addConflict

public void addConflict(java.util.Collection<T> things)
                 throws ContradictionException

Easy way to mean that a set of things are incompatible, i.e. they cannot altogether be satisfied.

Throws:

ContradictionException

addConflict

public void addConflict(T... things)
                 throws ContradictionException

Easy way to mean that a set of things are incompatible, i.e. they cannot altogether be satisfied.

Throws:

ContradictionException

setTrue

public void setTrue(T... things)
             throws ContradictionException

Throws:

ContradictionException

setFalse

public void setFalse(T... things)
              throws ContradictionException

Throws:

ContradictionException