org.sat4j

Interface ILauncherMode

All Superinterfaces:

SolutionFoundListener

public interface ILauncherMode
extends SolutionFoundListener

Allow to change the behavior of the launcher (either decision or optimization mode)

Since:

2.3.3

Author:

sroussel

Field Summary

Fields

Modifier and Type	Field and Description
static String	ANSWER_PREFIX
static String	CURRENT_OPTIMUM_VALUE_PREFIX
static ILauncherMode	DECISION The launcher is in decision mode: the answer is either SAT, UNSAT or UNKNOWN
static ILauncherMode	OPTIMIZATION The launcher is in optimization mode: the answer is either SAT, UPPER_BOUND, OPTIMUM_FOUND, UNSAT or UNKNOWN.
static String	SOLUTION_PREFIX

Fields inherited from interface org.sat4j.tools.SolutionFoundListener

VOID

Method Summary

Methods

Modifier and Type	Method and Description
void	displayResult(ISolver solver, IProblem problem, ILogAble logger, PrintWriter out, Reader reader, long beginTime, boolean displaySolutionLine) Output of the launcher when the solver stops
ExitCode	getCurrentExitCode() Allow the launcher to get the current status of the problem: SAT, UNSAT, UPPER_BOUND, etc.
void	setExitCode(ExitCode exitCode) Allow to set a specific exit code to the launcher (in case of trivial unsatisfiability for instance).
void	setIncomplete(boolean isIncomplete) Allows the launcher to specifically return an upper bound of the optimal solution in case of a time out (for maxsat competitions for instance).
void	solve(IProblem problem, Reader reader, ILogAble logger, PrintWriter out, long beginTime) Main solver call: one call for a decision problem, a loop for an optimization problem.

Methods inherited from interface org.sat4j.tools.SolutionFoundListener

onSolutionFound, onSolutionFound, onUnsatTermination

Field Detail

SOLUTION_PREFIX

static final String SOLUTION_PREFIX

See Also:

Constant Field Values

ANSWER_PREFIX

static final String ANSWER_PREFIX

See Also:

Constant Field Values

CURRENT_OPTIMUM_VALUE_PREFIX

static final String CURRENT_OPTIMUM_VALUE_PREFIX

See Also:

Constant Field Values

DECISION

static final ILauncherMode DECISION

The launcher is in decision mode: the answer is either SAT, UNSAT or UNKNOWN

OPTIMIZATION

static final ILauncherMode OPTIMIZATION

The launcher is in optimization mode: the answer is either SAT, UPPER_BOUND, OPTIMUM_FOUND, UNSAT or UNKNOWN. Using the incomplete property, the solver returns an upper bound of the optimal solution when a time out occurs.

Method Detail

displayResult

void displayResult(ISolver solver,
                 IProblem problem,
                 ILogAble logger,
                 PrintWriter out,
                 Reader reader,
                 long beginTime,
                 boolean displaySolutionLine)

Output of the launcher when the solver stops

Parameters:

solver - the solver that is launched by the launcher

problem - the problem that is solved

logger - the element that is able to log the result

out - the printwriter to associate to the solver

reader - the problem reader

beginTime - the time at which the solver was launched

displaySolutionLine - indicates whether the solution line shound be displayed or not (not recommended for large solutions)

solve

void solve(IProblem problem,
         Reader reader,
         ILogAble logger,
         PrintWriter out,
         long beginTime)

Main solver call: one call for a decision problem, a loop for an optimization problem.

Parameters:

problem - the problem to solve

logger - the element that is able to log the result

out - the printwriter to associate to the solver

beginTime - the time at which the solver starts

setIncomplete

void setIncomplete(boolean isIncomplete)

Allows the launcher to specifically return an upper bound of the optimal solution in case of a time out (for maxsat competitions for instance).

Parameters:

isIncomplete -

getCurrentExitCode

ExitCode getCurrentExitCode()

Allow the launcher to get the current status of the problem: SAT, UNSAT, UPPER_BOUND, etc.

Returns:

setExitCode

void setExitCode(ExitCode exitCode)

Allow to set a specific exit code to the launcher (in case of trivial unsatisfiability for instance).