org.sat4j.specs
Interface IProblem

All Known Subinterfaces:
IOptimizationProblem, ISolver
All Known Implementing Classes:
AbstractSelectorVariablesDecorator, DimacsOutputSolver, DimacsStringSolver, GateTranslator, MaxSatDecorator, Minimal4CardinalityModel, Minimal4InclusionModel, MinOneDecorator, ModelIterator, OptToSatAdapter, SingleSolutionDetector, SolutionCounter, Solver, SolverDecorator

public interface IProblem

Access to the information related to a given problem instance.

Author:
leberre

Method Summary
 int[] findModel()
          Look for a model satisfying all the clauses available in the problem.
 int[] findModel(IVecInt assumps)
          Look for a model satisfying all the clauses available in the problem.
 boolean isSatisfiable()
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(boolean globalTimeout)
          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.
 boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
          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.
 void printInfos(java.io.PrintWriter out, java.lang.String prefix)
          To print additional informations regarding the problem.
 

Method Detail

model

int[] model()
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.

Returns:
a model of the formula as an array of literals to satisfy.
See Also:
isSatisfiable(), isSatisfiable(IVecInt)

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()

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,
                      boolean globalTimeout)
                      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).
globalTimeout - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
Returns:
true if the set of constraints is satisfiable when literals are satisfied, else false.
Throws:
TimeoutException

isSatisfiable

boolean isSatisfiable(boolean globalTimeout)
                      throws TimeoutException
Check the satisfiability of the set of constraints contained inside the solver.

Parameters:
globalTimeout - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
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

findModel

int[] findModel()
                throws TimeoutException
Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable() and model() methods, as shown in the pseudo-code: if (isSatisfiable()) { return model(); } return null;

Returns:
a model of the formula as an array of literals to satisfy, or null if no model is found
Throws:
TimeoutException - if a model cannot be found within the given timeout.
Since:
1.7

findModel

int[] findModel(IVecInt assumps)
                throws TimeoutException
Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable(IVecInt) and model() methods, as shown in the pseudo-code: if (isSatisfiable(assumpt)) { return model(); } return null;

Returns:
a model of the formula as an array of literals to satisfy, or null if no model is found
Throws:
TimeoutException - if a model cannot be found within the given timeout.
Since:
1.7

nConstraints

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

Returns:
the number of constraints 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().

printInfos

void printInfos(java.io.PrintWriter out,
                java.lang.String prefix)
To print additional informations regarding the problem.

Parameters:
out - the place to print the information
prefix - the prefix to put in front of each line


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