org.sat4j.tools
Class ModelIterator

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

public class ModelIterator
extends SolverDecorator

That class allows to iterate through all the models (implicants) of a formula.

 ISolver solver = new ModelIterator(SolverFactory.OneSolver());
 boolean unsat = true;
 while (solver.isSatisfiable()) {
     unsat = false;
     int[] model = solver.model();
     // do something with model
 }
 if (unsat) {
     // UNSAT case
 }
 

Author:
leberre
See Also:
Serialized Form

Constructor Summary
ModelIterator(ISolver solver)
           
 
Method Summary
 boolean isSatisfiable()
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(IVecInt assumps)
          Check the satisfiability of the set of constraints contained inside the solver.
 int[] model()
          Provide a model (if any) for a satisfiable formula.
 void reset()
          Clean up the internal state of the solver.
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addClause, addPseudoBoolean, clearLearntClauses, decorated, findModel, findModel, getStat, getTimeout, model, nConstraints, newVar, newVar, nVars, printStat, printStat, removeConstr, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, toString
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

ModelIterator

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

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Overrides:
isSatisfiable in class SolverDecorator
Returns:
true if the set of constraints is satisfiable, else false.
Throws:
TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Overrides:
isSatisfiable in class SolverDecorator
Parameters:
assumps - a set of literals (represented by usual non null integers in Dimacs format).
Returns:
true if the set of constraints is satisfiable when literals are satisfied, else false.
Throws:
TimeoutException

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 SolverDecorator


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