org.sat4j.pb.tools

Class LexicoDecoratorPB

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.LexicoDecorator<IPBSolver>

org.sat4j.pb.tools.LexicoDecoratorPB

All Implemented Interfaces:

Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

public class LexicoDecoratorPB
extends LexicoDecorator<IPBSolver>
implements IPBSolver

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.tools.LexicoDecorator

criteria, currentCriterion, prevboolmodel, prevfullmodel

Constructor Summary

Constructors

Constructor and Description
LexicoDecoratorPB(IPBSolver solver)

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	addAtLeast(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo boolean constraint of the type "at most".
IConstr	addAtMost(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo boolean constraint of the type "at most".
void	addCriterion(IVecInt literals)
void	addCriterion(IVecInt literals, IVec<BigInteger> coefs)
IConstr	addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	addExactly(IVecInt literals, IVecInt coeffs, int weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"
boolean	admitABetterSolution(IVecInt assumps) Look for a solution of the optimization problem when some literals are satisfied.
protected IConstr	discardSolutionsForOptimizing()
protected Number	evaluate()
protected Number	evaluate(int criterion)
protected void	fixCriterionValue()
ObjectiveFunction	getObjectiveFunction() Retrieve the objective function from the solver.
int	numberOfCriteria()
void	setObjectiveFunction(ObjectiveFunction obj) Provide an objective function to the solver.

Methods inherited from class org.sat4j.tools.LexicoDecorator

admitABetterSolution, calculateObjective, discard, discardCurrentSolution, forceObjectiveValueTo, getObjectiveValue, getObjectiveValue, hasNoObjectiveFunction, isOptimal, model, model, nonOptimalMeansSatisfiable, setTimeoutForFindingBetterSolution

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, toString, unsatExplanation

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Constructor Detail

LexicoDecoratorPB

public LexicoDecoratorPB(IPBSolver solver)

Method Detail

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt lits,
                       IVec<BigInteger> coeffs,
                       boolean moreThan,
                       BigInteger d)
                         throws ContradictionException

Description copied from interface: IPBSolver

Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"

Specified by:

addPseudoBoolean in interface IPBSolver

Parameters:

lits - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

moreThan - true if it is a constraint >= degree, false if it is a constraint <= degree

d - the degree of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if the constraint is falsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction obj)

Description copied from interface: IPBSolver

Provide an objective function to the solver.

Specified by:

setObjectiveFunction in interface IPBSolver

Parameters:

obj - the objective function

getObjectiveFunction

public ObjectiveFunction getObjectiveFunction()

Description copied from interface: IPBSolver

Retrieve the objective function from the solver.

Specified by:

getObjectiveFunction in interface IPBSolver

Returns:

the objective function

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

Description copied from interface: IOptimizationProblem

Look for a solution of the optimization problem when some literals are satisfied.

Specified by:

admitABetterSolution in interface IOptimizationProblem

Overrides:

admitABetterSolution in class LexicoDecorator<IPBSolver>

Parameters:

assumps - a set of literals in Dimacs format.

Returns:

true if a better solution than current one can be found.

Throws:

TimeoutException - if the solver cannot answer in reasonable time.

See Also:

ISolver.setTimeout(int)

addCriterion

public void addCriterion(IVecInt literals)

Overrides:

addCriterion in class LexicoDecorator<IPBSolver>

addCriterion

public void addCriterion(IVecInt literals,
                IVec<BigInteger> coefs)

evaluate

protected Number evaluate()

Overrides:

evaluate in class LexicoDecorator<IPBSolver>

evaluate

protected Number evaluate(int criterion)

Overrides:

evaluate in class LexicoDecorator<IPBSolver>

fixCriterionValue

protected void fixCriterionValue()
                          throws ContradictionException

Overrides:

fixCriterionValue in class LexicoDecorator<IPBSolver>

Throws:

ContradictionException

discardSolutionsForOptimizing

protected IConstr discardSolutionsForOptimizing()
                                         throws ContradictionException

Overrides:

discardSolutionsForOptimizing in class LexicoDecorator<IPBSolver>

Throws:

ContradictionException

numberOfCriteria

public int numberOfCriteria()

Overrides:

numberOfCriteria in class LexicoDecorator<IPBSolver>

addAtMost

public IConstr addAtMost(IVecInt literals,
                IVecInt coeffs,
                int degree)
                  throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo boolean constraint of the type "at most".

Specified by:

addAtMost in interface IPBSolver

Parameters:

literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addAtMost

public IConstr addAtMost(IVecInt literals,
                IVec<BigInteger> coeffs,
                BigInteger degree)
                  throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo boolean constraint of the type "at most".

Specified by:

addAtMost in interface IPBSolver

Parameters:

literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                 IVecInt coeffs,
                 int degree)
                   throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "at least".

Specified by:

addAtLeast in interface IPBSolver

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                 IVec<BigInteger> coeffs,
                 BigInteger degree)
                   throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "at least".

Specified by:

addAtLeast in interface IPBSolver

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree of the pseudo-boolean constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addExactly

public IConstr addExactly(IVecInt literals,
                 IVecInt coeffs,
                 int weight)
                   throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "subset sum".

Specified by:

addExactly in interface IPBSolver

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

weight - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.

addExactly

public IConstr addExactly(IVecInt literals,
                 IVec<BigInteger> coeffs,
                 BigInteger weight)
                   throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "subset sum".

Specified by:

addExactly in interface IPBSolver

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

weight - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.