org.sat4j.specs

Interface IProblem

All Superinterfaces:

RandomAccessModel

All Known Subinterfaces:

ICDCL<D>, IGroupSolver, IOptimizationProblem, 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 IProblem
extends RandomAccessModel

Access to the information related to a given problem instance.

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
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.
int	nConstraints() To know the number of constraints currently available in the solver.
int	newVar(int howmany) Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany.
int	nVars() To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.
int[]	primeImplicant() Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.
boolean	primeImplicant(int p) Check if a given literal is part of the prime implicant computed by the primeImplicant() method.
void	printInfos(PrintWriter out) To print additional informations regarding the problem.
void	printInfos(PrintWriter out, String prefix) Deprecated.

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

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)

primeImplicant

int[] primeImplicant()

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

Returns:

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

Since:

2.3

primeImplicant

boolean primeImplicant(int p)

Check if a given literal is part of the prime implicant computed by the primeImplicant() method.

Parameters:

p - a literal in Dimacs format

Returns:

true iff p belongs to primeImplicant()

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

newVar

int newVar(int howmany)

Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany. That feature allows encodings to create additional variables with identifier starting at howmany+1.

Parameters:

howmany - number of variables to create

Returns:

the total number of variables available in the solver (the highest variable number)

See Also:

nVars()

nVars

int nVars()

To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.

Returns:

the number of variables created using newVar().

See Also:

newVar(int)

printInfos

@Deprecated
void printInfos(PrintWriter out,
                         String prefix)

Deprecated.

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

printInfos

void printInfos(PrintWriter out)

To print additional informations regarding the problem.

Parameters:

out - the place to print the information

Since:

2.3.3

See Also:

#setLogPrefix(String)