org.sat4j.opt
Class MaxSatDecorator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator
      extended by org.sat4j.opt.AbstractSelectorVariablesDecorator
          extended by 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


Copyright © 2007 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.