org.sat4j.maxsat

Class MinCostDecorator

java.lang.Object

org.sat4j.tools.SolverDecorator<IPBSolver>

org.sat4j.pb.PBSolverDecorator

org.sat4j.maxsat.MinCostDecorator

All Implemented Interfaces:

Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

public class MinCostDecorator
extends PBSolverDecorator
implements IOptimizationProblem

A decorator that computes minimal cost models. That problem is also known as binate covering problem. Please make sure that newVar(howmany) is called first to setup the decorator.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
MinCostDecorator(IPBSolver solver)

Method Summary

Methods

Modifier and Type	Method and Description
boolean	admitABetterSolution()
boolean	admitABetterSolution(IVecInt assumps)
Number	calculateObjective()
int	costOf(int var) to know the cost of a given var.
void	discard()
void	discardCurrentSolution()
void	forceObjectiveValueTo(Number forcedValue)
Number	getObjectiveValue()
boolean	hasNoObjectiveFunction()
boolean	isOptimal()
int[]	model()
int	newVar()
int	newVar(int howmany) Setup the number of variables to use inside the solver.
boolean	nonOptimalMeansSatisfiable()
void	reset()
void	setCost(int var, int cost) to set the cost of a given var.
void	setTimeoutForFindingBetterSolution(int seconds)

Methods inherited from class org.sat4j.pb.PBSolverDecorator

addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction

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, model, modelWithInternalVariables, nConstraints, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, 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.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, nConstraints, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

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, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, toString, unsatExplanation

Constructor Detail

MinCostDecorator

public MinCostDecorator(IPBSolver solver)

Method Detail

newVar

public int newVar()

Specified by:

newVar in interface ISolver

Overrides:

newVar in class SolverDecorator<IPBSolver>

newVar

public int newVar(int howmany)

Setup the number of variables to use inside the solver. It is mandatory to call that method before setting the cost of the variables.

Specified by:

newVar in interface IProblem

Overrides:

newVar in class SolverDecorator<IPBSolver>

Parameters:

howmany - the maximum number of variables in the solver.

costOf

public int costOf(int var)

to know the cost of a given var.

Parameters:

var - a variable in dimacs format

Returns:

the cost of that variable when assigned to true

setCost

public void setCost(int var,
           int cost)

to set the cost of a given var.

Parameters:

var - a variable in dimacs format

cost - the cost of var when assigned to true

admitABetterSolution

public boolean admitABetterSolution()
                             throws TimeoutException

Specified by:

admitABetterSolution in interface IOptimizationProblem

Throws:

TimeoutException

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

Specified by:

admitABetterSolution in interface IOptimizationProblem

Throws:

TimeoutException

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Specified by:

hasNoObjectiveFunction in interface IOptimizationProblem

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Specified by:

nonOptimalMeansSatisfiable in interface IOptimizationProblem

calculateObjective

public Number calculateObjective()

Specified by:

calculateObjective in interface IOptimizationProblem

discardCurrentSolution

public void discardCurrentSolution()
                            throws ContradictionException

Specified by:

discardCurrentSolution in interface IOptimizationProblem

Throws:

ContradictionException

reset

public void reset()

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<IPBSolver>

model

public int[] model()

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

getObjectiveValue

public Number getObjectiveValue()

Specified by:

getObjectiveValue in interface IOptimizationProblem

discard

public void discard()
             throws ContradictionException

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException

Specified by:

forceObjectiveValueTo in interface IOptimizationProblem

Throws:

ContradictionException

isOptimal

public boolean isOptimal()

Specified by:

isOptimal in interface IOptimizationProblem

setTimeoutForFindingBetterSolution

public void setTimeoutForFindingBetterSolution(int seconds)

Specified by:

setTimeoutForFindingBetterSolution in interface IOptimizationProblem