org.sat4j.tools

Class ModelIterator

java.lang.Object

org.sat4j.tools.SolverDecorator<ISolver>

org.sat4j.tools.ModelIterator

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel

Direct Known Subclasses:

ModelIteratorToSATAdapter

public class ModelIterator
extends SolverDecorator<ISolver>

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
 }
 

It is also possible to limit the number of models returned:

 ISolver solver = new ModelIterator(SolverFactory.OneSolver(), 10);
 

will return at most 10 models.

Author:

leberre

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
ModelIterator(ISolver solver) Create an iterator over the solutions available in solver.
ModelIterator(ISolver solver, long bound) Create an iterator over a limited number of solutions available in solver.

Method Summary

Methods

Modifier and Type	Method and Description
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.
long	numberOfModelsFoundSoFar() To know the number of models already found.
int[]	primeImplicant() Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.
void	reset() Clean up the internal state of the solver.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, toString, unsatExplanation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

ModelIterator

public ModelIterator(ISolver solver)

Create an iterator over the solutions available in solver. The iterator will look for one new model at each call to isSatisfiable() and will discard that model at each call to model().

Parameters:

solver - a solver containing the constraints to satisfy.

See Also:

isSatisfiable(), SolverDecorator.isSatisfiable(boolean), isSatisfiable(IVecInt), SolverDecorator.isSatisfiable(IVecInt, boolean), model()

ModelIterator

public ModelIterator(ISolver solver,
             long bound)

Create an iterator over a limited number of solutions available in solver. The iterator will look for one new model at each call to isSatisfiable() and will discard that model at each call to model(). At most bound calls to models() will be allowed before the method isSatisfiable() returns false.

Parameters:

solver - a solver containing the constraints to satisfy.

bound - the maximum number of models to return.

Since:

2.1

See Also:

isSatisfiable(), SolverDecorator.isSatisfiable(boolean), isSatisfiable(IVecInt), SolverDecorator.isSatisfiable(IVecInt, boolean), model()

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)

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<ISolver>

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<ISolver>

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. Note that such method should also be called when you no longer need the solver because the state of the solver may prevent the GC to proceed. There is a known issue for instance where failing to call reset() on a solver will keep timer threads alive and exhausts memory.

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<ISolver>

primeImplicant

public int[] primeImplicant()

Description copied from interface: IProblem

Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.

Specified by:

primeImplicant in interface IProblem

Overrides:

primeImplicant in class SolverDecorator<ISolver>

Returns:

a prime implicant of the formula as an array of literal, Dimacs format.

numberOfModelsFoundSoFar

public long numberOfModelsFoundSoFar()

To know the number of models already found.

Returns:

the number of models found so far.

Since:

2.3