org.sat4j.specs

Interface RandomAccessModel

All Known Subinterfaces:

ICDCL<D>, IGroupSolver, IOptimizationProblem, IProblem, ISolver

All Known Implementing Classes:

AbstractClauseSelectorSolver, AbstractMinimalModel, AbstractOutputSolver, AbstractSelectorVariablesDecorator, ClausalCardinalitiesDecorator, DimacsOutputSolver, DimacsStringSolver, FullClauseSelectorSolver, GateTranslator, GroupClauseSelectorSolver, HighLevelXplain, LexicoDecorator, ManyCore, MaxSatDecorator, Minimal4CardinalityModel, Minimal4InclusionModel, MinOneDecorator, ModelIterator, ModelIteratorToSATAdapter, NegationDecorator, OptToSatAdapter, SingleSolutionDetector, SolutionCounter, Solver, SolverDecorator, StatisticsSolver, Xplain

public interface RandomAccessModel

That interface allows to efficiently retrieve the truth value of a given variable in the solver.

Author:

daniel

Method Summary

Methods

Modifier and Type	Method and Description
boolean	model(int var) Provide the truth value of a specific variable in the model.

Method Detail

model

boolean model(int var)

Provide the truth value of a specific variable in the model. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Parameters:

var - the variable id in Dimacs format

Returns:

the truth value of that variable in the model

Since:

1.6

See Also:

#model()