org.sat4j.specs
Interface IProblem

All Known Subinterfaces:

IOptimizationProblem, ISolver

All Known Implementing Classes:

MaxSatDecorator, Minimal4CardinalityModel, Minimal4InclusionModel, MinOneDecorator, ModelIterator, PBSolver, PBSolverCard, PBSolverClause, PBSolverWithImpliedClause, PseudoOptDecorator, SATRaceDecorator, SingleSolutionDetector, SolutionCounter, Solver, SolverDecorator, WeightedMaxSatDecorator

public interface IProblem

Access to the information related to a given problem instance.

Author:

leberre

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.
boolean	model(int var) Provide the truth value of a specific variable in the model.
int	nConstraints() To know the number of constraints currently available in the solver.
int	nVars() To know the number of variables used in the solver.

Method Detail

model

int[] model()

Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Returns:

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

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

isSatisfiable

boolean isSatisfiable()
                      throws TimeoutException

Check the satisfiability of the set of constraints contained inside the solver.

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException

isSatisfiable

boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException

Check the satisfiability of the set of constraints contained inside the solver.

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

nConstraints

int nConstraints()

To know the number of constraints currently available in the solver. (without taking into account learnt constraints).

Returns:

the number of contraints added to the solver

nVars

int nVars()

To know the number of variables used in the solver.

Returns:

the number of variables created using newVar().