org.sat4j.specs

Interface ISolverService

All Known Implementing Classes:

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

Methods

Modifier and Type	Method and Description
IConstr	addAtMostOnTheFly(int[] literals, int degree) Add a new pseudo cardinality constraint sum literals <= degree in the solver.
IConstr	addClauseOnTheFly(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.
String	getLogPrefix()
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.
boolean	removeSubsumedConstr(IConstr c) Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to 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

addClauseOnTheFly

IConstr addClauseOnTheFly(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.

addAtMostOnTheFly

IConstr addAtMostOnTheFly(int[] literals,
                        int degree)

Add a new pseudo cardinality constraint sum literals <= degree in the solver. The constraint must be falsified under current assignment.

Parameters:

literals - a set of literals in Dimacs format.

degree - the maximal number of literals which can be satisfied.

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.

removeSubsumedConstr

boolean removeSubsumedConstr(IConstr c)

Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver. Unlike the removeConstr() method, learned clauses will NOT be cleared. That method is expected to be used to remove constraints used in the optimization process. In order to prevent a wrong from the user, the method will only work if the argument is the last constraint added to the solver. An illegal argument exception will be thrown in other cases.

Parameters:

c - a constraint returned by one of the add method. It must be the latest constr added to the solver.

Returns:

true if the constraint was successfully removed.

getLogPrefix

String getLogPrefix()

Returns:

the string used to prefix the output.

Since:

2.3.3