org.sat4j.specs
Interface ISolverService

All Known Implementing Classes:

PBSolver, PBSolverCautious, PBSolverClause, PBSolverCP, PBSolverResCP, PBSolverResolution, PBSolverWithImpliedClause, Solver

public interface ISolverService

The aim on that interface is to allow power users to communicate with the SAT solver using Dimacs format. That way, there is no need to know the internals of the solver.

Since:

2.3.2

Author:

leberre

Method Summary

void	addClause(int[] literals) Add a new clause in the SAT solver.
void	backtrack(int[] reason) Ask the SAT solver to backtrack.
int	currentDecisionLevel() To access the current decision level
IVec<? extends IConstr>	getLearnedConstraints() Read-Only access to the list of constraints learned and not deleted so far in the solver.
int[]	getLiteralsPropagatedAt(int decisionLevel) To access the literals propagated at a specific decision level.
double[]	getVariableHeuristics() Read-Only access to the value of the heuristics for each variable.
int	nVars() Read-Only access to the number of variables declared in the solver.
void	stop() Ask the SAT solver to stop the search.
void	suggestNextLiteralToBranchOn(int l) Suggests to the SAT solver to branch next on the given literal.
Lbool	truthValue(int literal) To access the truth value of a specific literal under current assignment.

Method Detail

stop

void stop()

Ask the SAT solver to stop the search.

backtrack

void backtrack(int[] reason)

Ask the SAT solver to backtrack. It is mandatory to provide a reason for backtracking, in terms of literals (which should be falsified under current assignment). The reason is not added to the clauses of the solver: only the result of the analysis is stored in the learned clauses. Note that these clauses may be removed latter.

Parameters:

reason - a set of literals, in Dimacs format, currently falsified, i.e. for (int l : reason) assert truthValue(l) == Lbool.FALSE

addClause

void addClause(int[] literals)

Add a new clause in the SAT solver. The new clause may contain new variables. The clause may be falsified, in that case, the difference with backtrack() is that the new clause is appended to the solver as a regular clause. Thus it will not be removed by aggressive clause deletion. The clause may be assertive at a given decision level. In that case, the solver should backtrack to the proper decision level. In other cases, the search should simply proceed.

Parameters:

literals - a set of literals in Dimacs format.

truthValue

Lbool truthValue(int literal)

To access the truth value of a specific literal under current assignment.

Parameters:

literal - a Dimacs literal, i.e. a non-zero integer.

Returns:

true or false if the literal is assigned, else undefined.

currentDecisionLevel

int currentDecisionLevel()

To access the current decision level

getLiteralsPropagatedAt

int[] getLiteralsPropagatedAt(int decisionLevel)

To access the literals propagated at a specific decision level.

Parameters:

decisionLevel - a decision level between 0 and #currentDecisionLevel()

suggestNextLiteralToBranchOn

void suggestNextLiteralToBranchOn(int l)

Suggests to the SAT solver to branch next on the given literal.

Parameters:

l - a literal in Dimacs format.

getVariableHeuristics

double[] getVariableHeuristics()

Read-Only access to the value of the heuristics for each variable. Note that for efficiency reason, the real array storing the value of the heuristics is returned. DO NOT CHANGE THE VALUES IN THAT ARRAY.

Returns:

the value of the heuristics for each variable (using Dimacs index).

getLearnedConstraints

IVec<? extends IConstr> getLearnedConstraints()

Read-Only access to the list of constraints learned and not deleted so far in the solver. Note that for efficiency reason, the real list of constraints managed by the solver is returned. DO NOT MODIFY THAT LIST NOR ITS CONSTRAINTS.

Returns:

the constraints learned and kept so far by the solver.

nVars

int nVars()

Read-Only access to the number of variables declared in the solver.

Returns:

the maximum variable id (Dimacs format) reserved in the solver.