org.sat4j.maxsat
Class MinCostDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator<org.sat4j.pb.IPBSolver>
      org.sat4j.pb.PBSolverDecorator
          org.sat4j.maxsat.MinCostDecorator

All Implemented Interfaces:

java.io.Serializable, org.sat4j.pb.IPBSolver, org.sat4j.specs.IOptimizationProblem, org.sat4j.specs.IProblem, org.sat4j.specs.ISolver

public class MinCostDecorator
extends org.sat4j.pb.PBSolverDecorator
implements org.sat4j.specs.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

MinCostDecorator(org.sat4j.pb.IPBSolver 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()
int	newVar()
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.pb.PBSolverDecorator

addPseudoBoolean, getExplanation, setListOfVariablesForExplanation, setObjectiveFunction

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, nVars, printInfos, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sat4j.specs.IProblem

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

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addClause, clearLearntClauses, expireTimeout, getStat, getTimeout, isDBSimplificationAllowed, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString

Constructor Detail

MinCostDecorator

public MinCostDecorator(org.sat4j.pb.IPBSolver solver)

Method Detail

newVar

public int newVar()

Specified by:

newVar in interface org.sat4j.specs.ISolver

Overrides:

newVar in class org.sat4j.tools.SolverDecorator<org.sat4j.pb.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 org.sat4j.specs.ISolver

Overrides:

newVar in class org.sat4j.tools.SolverDecorator<org.sat4j.pb.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 org.sat4j.specs.TimeoutException

Specified by:

admitABetterSolution in interface org.sat4j.specs.IOptimizationProblem

Throws:

org.sat4j.specs.TimeoutException

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Specified by:

hasNoObjectiveFunction in interface org.sat4j.specs.IOptimizationProblem

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Specified by:

nonOptimalMeansSatisfiable in interface org.sat4j.specs.IOptimizationProblem

calculateObjective

public java.lang.Number calculateObjective()

Specified by:

calculateObjective in interface org.sat4j.specs.IOptimizationProblem

discard

public void discard()
             throws org.sat4j.specs.ContradictionException

Specified by:

discard in interface org.sat4j.specs.IOptimizationProblem

Throws:

org.sat4j.specs.ContradictionException

model

public int[] model()

Specified by:

model in interface org.sat4j.specs.IProblem

Overrides:

model in class org.sat4j.tools.SolverDecorator<org.sat4j.pb.IPBSolver>