org.sat4j.tools

Class ModelIteratorToSATAdapter

java.lang.Object

org.sat4j.tools.SolverDecorator<ISolver>

org.sat4j.tools.ModelIterator

org.sat4j.tools.ModelIteratorToSATAdapter

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel

public class ModelIteratorToSATAdapter
extends ModelIterator

This class allow to use the ModelIterator class as a solver.

Author:

lonca

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
ModelIteratorToSATAdapter(ISolver solver, long bound, SolutionFoundListener sfl)
ModelIteratorToSATAdapter(ISolver solver, SolutionFoundListener sfl)

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.

Methods inherited from class org.sat4j.tools.ModelIterator

numberOfModelsFoundSoFar, primeImplicant, reset

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

ModelIteratorToSATAdapter

public ModelIteratorToSATAdapter(ISolver solver,
                         SolutionFoundListener sfl)

ModelIteratorToSATAdapter

public ModelIteratorToSATAdapter(ISolver solver,
                         long bound,
                         SolutionFoundListener sfl)

Method Detail

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 ModelIterator

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 ModelIterator

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

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 ModelIterator

Returns:

a model of the formula as an array of literals to satisfy.

See Also:

IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)