org.sat4j.pb.tools
Class LexicoDecoratorPB

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<T>
      extended by org.sat4j.tools.LexicoDecorator<IPBSolver>
          extended by org.sat4j.pb.tools.LexicoDecoratorPB
All Implemented Interfaces:
Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver

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
LexicoDecoratorPB(IPBSolver solver)
           
 
Method Summary
 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)
           
protected  IConstr discardSolutionsForOptimizing()
           
protected  Number evaluate()
           
protected  void fixCriterionValue()
           
 ObjectiveFunction getObjectiveFunction()
          Retrieve the objective function from the solver.
protected  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, hasNoObjectiveFunction, isOptimal, model, model, nonOptimalMeansSatisfiable
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, 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, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, 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, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos
 

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
Specified by:
admitABetterSolution in interface IOptimizationProblem
Overrides:
admitABetterSolution in class LexicoDecorator<IPBSolver>
Throws:
TimeoutException

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>

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

protected 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.


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