org.sat4j.opt
Class MaxSatDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator
      org.sat4j.opt.AbstractSelectorVariablesDecorator
          org.sat4j.opt.MaxSatDecorator

All Implemented Interfaces:

java.io.Serializable, IOptimizationProblem, IProblem, ISolver

public class MaxSatDecorator
extends AbstractSelectorVariablesDecorator
implements IOptimizationProblem

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.opt.AbstractSelectorVariablesDecorator

nbnewvar, nborigvars, prevfullmodel

Constructor Summary

MaxSatDecorator(ISolver solver)

Method Summary

IConstr	addClause(IVecInt literals) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
java.lang.Number	calculateObjective()
void	discard()
boolean	hasNoObjectiveFunction()
boolean	nonOptimalMeansSatisfiable()
void	reset() Clean up the internal state of the solver.

Methods inherited from class org.sat4j.opt.AbstractSelectorVariablesDecorator

admitABetterSolution, model, newVar, setExpectedNumberOfClauses

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addPseudoBoolean, clearLearntClauses, decorated, findModel, findModel, getStat, getTimeout, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, printStat, printStat, removeConstr, setTimeout, setTimeoutMs, 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.IOptimizationProblem

admitABetterSolution

Methods inherited from interface org.sat4j.specs.IProblem

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

Constructor Detail

MaxSatDecorator

public MaxSatDecorator(ISolver solver)

Method Detail

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Description copied from interface: ISolver

Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. (clasical Dimacs way of representing literals).

Specified by:

addClause in interface ISolver

Overrides:

addClause in class SolverDecorator

Parameters:

literals - a set of literals

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 it contains only falsified literals after unit propagation

See Also:

ISolver.removeConstr(IConstr)

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver.

Specified by:

reset in interface ISolver

Overrides:

reset in class AbstractSelectorVariablesDecorator

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