org.sat4j.maxsat
Class WeightedMaxSatDecorator

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

All Implemented Interfaces:

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

public class WeightedMaxSatDecorator
extends org.sat4j.pb.PBSolverDecorator
implements org.sat4j.specs.IOptimizationProblem

A decorator for solving weighted MAX SAT problems. The first value of the list of literals in the addClause() method contains the weight of the clause.

Author:

daniel

See Also:

Serialized Form

Field Summary

protected int	nbnewvar
protected int	nborigvars
protected int[]	prevfullmodel
protected int	top

Constructor Summary

WeightedMaxSatDecorator(org.sat4j.pb.IPBSolver solver)

Method Summary

org.sat4j.specs.IConstr	addClause(org.sat4j.specs.IVecInt literals)
boolean	admitABetterSolution()
java.lang.Number	calculateObjective()
void	discard()
boolean	hasNoObjectiveFunction()
int[]	model()
int	newVar(int howmany)
boolean	nonOptimalMeansSatisfiable()
void	reset()
void	setExpectedNumberOfClauses(int nb)
void	setTopWeight(int top)

Methods inherited from class org.sat4j.pb.PBSolverDecorator

addPseudoBoolean, getExplanation, setListOfVariablesForExplanation, setObjectiveFunction

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, printInfos, printStat, printStat, removeConstr, setDBSimplificationAllowed, 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, clearLearntClauses, expireTimeout, getStat, getTimeout, isDBSimplificationAllowed, newVar, printStat, printStat, removeConstr, setDBSimplificationAllowed, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString

Field Detail

nborigvars

protected int nborigvars

nbnewvar

protected int nbnewvar

prevfullmodel

protected int[] prevfullmodel

top

protected int top

Constructor Detail

WeightedMaxSatDecorator

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

Method Detail

newVar

public int newVar(int howmany)

Specified by:

newVar in interface org.sat4j.specs.ISolver

Overrides:

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

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)

Specified by:

setExpectedNumberOfClauses in interface org.sat4j.specs.ISolver

Overrides:

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

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>

setTopWeight

public void setTopWeight(int top)

addClause

public org.sat4j.specs.IConstr addClause(org.sat4j.specs.IVecInt literals)
                                  throws org.sat4j.specs.ContradictionException

Specified by:

addClause in interface org.sat4j.specs.ISolver

Overrides:

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

Throws:

org.sat4j.specs.ContradictionException

admitABetterSolution

public boolean admitABetterSolution()
                             throws org.sat4j.specs.TimeoutException

Specified by:

admitABetterSolution in interface org.sat4j.specs.IOptimizationProblem

Throws:

org.sat4j.specs.TimeoutException

reset

public void reset()

Specified by:

reset in interface org.sat4j.specs.ISolver

Overrides:

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

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