org.sat4j.tools
Class Minimal4InclusionModel

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<ISolver>
      extended by org.sat4j.tools.Minimal4InclusionModel
All Implemented Interfaces:
java.io.Serializable, IProblem, ISolver

public class Minimal4InclusionModel
extends SolverDecorator<ISolver>

Computes models with a minimal subset (with respect to set inclusion) of negative literals. This is done be adding a clause containing the negation of the negative literals appearing in the model found (which prevents any interpretation containing that subset of negative literals to be a model of the formula). Computes only one model minimal for inclusion, since there is currently no way to save the state of the solver.

Author:
leberre
See Also:
ISolver.addClause(IVecInt), Serialized Form

Constructor Summary
Minimal4InclusionModel(ISolver solver)
           
 
Method Summary
 int[] model()
          Provide a model (if any) for a satisfiable formula.
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, newVar, 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
 

Constructor Detail

Minimal4InclusionModel

public Minimal4InclusionModel(ISolver solver)
Parameters:
solver -
Method Detail

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<ISolver>
Returns:
a model of the formula as an array of literals to satisfy.
See Also:
IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)


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