org.sat4j.opt
Class MinCostDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator
      org.sat4j.opt.MinCostDecorator

All Implemented Interfaces:

java.io.Serializable, IOptimizationProblem, IProblem, ISolver

public class MinCostDecorator
extends SolverDecorator
implements IOptimizationProblem

A decorator that computes minimal cost models. Please make sure that newVar(howmany) is called first to setup the decorator.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

MinCostDecorator(ISolver solver)

Method Summary

boolean	admitABetterSolution()
java.lang.Number	calculateObjective()
int	costOf(int var) to know the cost of a given var.
void	discard()
boolean	hasNoObjectiveFunction()
int[]	model() Provide a model (if any) for a satisfiable formula.
int	newVar() Create a new variable in the solver (and thus in the vocabulary).
int	newVar(int howmany) Setup the number of variables to use inside the solver.
boolean	nonOptimalMeansSatisfiable()
void	setCost(int var, int cost) to set the cost of a given var.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addClause, addPseudoBoolean, clearLearntClauses, decorated, findModel, findModel, getStat, getTimeout, isSatisfiable, isSatisfiable, model, nConstraints, nVars, printStat, printStat, removeConstr, reset, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, model, nConstraints, nVars

Constructor Detail

MinCostDecorator

public MinCostDecorator(ISolver solver)

Method Detail

newVar

public int newVar()

Description copied from interface: ISolver

Create a new variable in the solver (and thus in the vocabulary). WE STRONGLY ENCOURAGE TO PRECOMPUTE THE NUMBER OF VARIABLES NEEDED AND TO USE newVar(howmany) INSTEAD. IF YOU EXPERIENCE A PROBLEM OF EFFICIENCY WHEN READING/BUILDING YOUR SAT INSTANCE, PLEASE CHECK THAT YOU ARE NOT USING THAT METHOD.

Specified by:

newVar in interface ISolver

Overrides:

newVar in class SolverDecorator

Returns:

the number of variables available in the vocabulary, which is the identifier of the new variable.

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 ISolver

Overrides:

newVar in class SolverDecorator

Parameters:

howmany - the maximum number of variables in the solver.

Returns:

the total number of variables available in the solver (the highest variable number)

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

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Specified by:

hasNoObjectiveFunction in interface IOptimizationProblem

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Specified by:

nonOptimalMeansSatisfiable in interface IOptimizationProblem

calculateObjective

public java.lang.Number calculateObjective()

Specified by:

calculateObjective in interface IOptimizationProblem

discard

public void discard()
             throws ContradictionException

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException

model

public int[] model()

Description copied from interface: IProblem

Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator

Returns:

a model of the formula as an array of literals to satisfy.

See Also:

IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)