org.sat4j.specs

Interface ISolver

All Superinterfaces:

IProblem, RandomAccessModel, Serializable

All Known Subinterfaces:

ICDCL<D>, IGroupSolver

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 ISolver
extends IProblem, Serializable

This interface contains all services provided by a SAT solver.

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
void	addAllClauses(IVec<IVecInt> clauses) Create clauses from a set of set of literals.
IConstr	addAtLeast(IVecInt literals, int degree) Create a cardinality constraint of the type "at least n of those literals must be satisfied"
IConstr	addAtMost(IVecInt literals, int degree) Create a cardinality constraint of the type "at most n of those literals must be satisfied"
IConstr	addBlockingClause(IVecInt literals) Add a clause in order to prevent an assignment to occur.
IConstr	addClause(IVecInt literals) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
IConstr	addExactly(IVecInt literals, int n) Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
void	clearLearntClauses() Remove clauses learned during the solving process.
void	expireTimeout() Expire the timeout of the solver.
String	getLogPrefix()
<S extends ISolverService> SearchListener<S>	getSearchListener() Get the current SearchListener.
ISolver	getSolvingEngine() Retrieve the real engine in case the engine is decorated by one or several decorator.
Map<String,Number>	getStat() To obtain a map of the available statistics from the solver.
int	getTimeout() Useful to check the internal timeout of the solver.
long	getTimeoutMs() Useful to check the internal timeout of the solver.
boolean	isDBSimplificationAllowed() Indicate whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.
boolean	isSolverKeptHot() Ask to the solver if it is in "hot" mode, meaning that the heuristics is not reset after call is isSatisfiable().
boolean	isVerbose() To know if the solver is in verbose mode (output allowed) or not.
int[]	modelWithInternalVariables() That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance).
int	newVar() Deprecated.
int	nextFreeVarId(boolean reserve) Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).
void	printStat(PrintStream out, String prefix) Deprecated.
void	printStat(PrintWriter out) Display statistics to the given output writer
void	printStat(PrintWriter out, String prefix) Deprecated. using the prefix does no longer makes sense because the solver owns it.
int	realNumberOfVariables() Retrieve the real number of variables used in the solver.
void	registerLiteral(int p) Tell the solver to consider that the literal is in the CNF.
boolean	removeConstr(IConstr c) Remove a constraint returned by one of the add method from 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	reset() Clean up the internal state of the solver.
void	setDBSimplificationAllowed(boolean status) Set whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.
void	setExpectedNumberOfClauses(int nb) To inform the solver of the expected number of clauses to read.
void	setKeepSolverHot(boolean keepHot) Changed the behavior of the SAT solver heuristics between successive calls.
void	setLogPrefix(String prefix) Set the prefix used to display information.
<S extends ISolverService> void	setSearchListener(SearchListener<S> sl) Allow the user to hook a listener to the solver to be notified of the main steps of the search process.
void	setTimeout(int t) To set the internal timeout of the solver.
void	setTimeoutMs(long t) To set the internal timeout of the solver.
void	setTimeoutOnConflicts(int count) To set the internal timeout of the solver.
void	setUnitClauseProvider(UnitClauseProvider ucp) Allow the solver to ask for unit clauses before each restarts.
void	setVerbose(boolean value) Set the verbosity of the solver
String	toString(String prefix) Display a textual representation of the solver configuration.
IVecInt	unsatExplanation() Retrieve an explanation of the inconsistency in terms of assumption literals.

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Method Detail

newVar

@Deprecated
int newVar()

Deprecated.

Create a new variable in the solver (and thus in the vocabulary). WE STRONGLY ENCOURAGE TO PRECOMPUTE THE NUMBER OF VARIABLES NEEDED AND TO USE newVar(howmany) INSTEAD. IF YOU EXPERIENCE A PROBLEM OF EFFICIENCY WHEN READING/BUILDING YOUR SAT INSTANCE, PLEASE CHECK THAT YOU ARE NOT USING THAT METHOD.

Returns:

the number of variables available in the vocabulary, which is the identifier of the new variable.

nextFreeVarId

int nextFreeVarId(boolean reserve)

Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number). Note that a previous call to newVar(max) will reserve in the solver the variable identifier from 1 to max, so nextFreeVarId() would return max+1, even if some variable identifiers smaller than max are not used. By default, the method will always answer by the maximum variable identifier used so far + 1. The number of variables reserved in the solver is accessible through the realNumberOfVariables() method.

Parameters:

reserve - if true, the maxVarId is updated in the solver, i.e. successive calls to nextFreeVarId(true) will return increasing variable id while successive calls to nextFreeVarId(false) will always answer the same.

Returns:

a variable identifier not in use in the constraints already inside the solver.

Since:

2.1

See Also:

realNumberOfVariables()

registerLiteral

void registerLiteral(int p)

Tell the solver to consider that the literal is in the CNF. Since model() only return the truth value of the literals that appear in the solver, it is sometimes required that the solver provides a default truth value for a given literal. This happens for instance for MaxSat.

Parameters:

p - the literal in Dimacs format that should appear in the model.

setExpectedNumberOfClauses

void setExpectedNumberOfClauses(int nb)

To inform the solver of the expected number of clauses to read. This is an optional method, that is called when the p cnf line is read in dimacs formatted input file. Note that this method is supposed to be called AFTER a call to newVar(int)

Parameters:

nb - the expected number of clauses.

Since:

1.6

See Also:

IProblem.newVar(int)

addClause

IConstr addClause(IVecInt literals)
                  throws ContradictionException

Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. (classical Dimacs way of representing literals).

Parameters:

literals - a set of literals

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if it contains only falsified literals after unit propagation

See Also:

removeConstr(IConstr)

addBlockingClause

IConstr addBlockingClause(IVecInt literals)
                          throws ContradictionException

Add a clause in order to prevent an assignment to occur. This happens usually when iterating over models for instance.

Parameters:

literals -

Returns:

Throws:

ContradictionException

Since:

2.1

removeConstr

boolean removeConstr(IConstr c)

Remove a constraint returned by one of the add method from the solver. All learned clauses will be cleared. Current implementation does not handle properly the case of unit clauses.

Parameters:

c - a constraint returned by one of the add method.

Returns:

true if the constraint was successfully removed.

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.

Since:

2.1

addAllClauses

void addAllClauses(IVec<IVecInt> clauses)
                   throws ContradictionException

Create clauses from a set of set of literals. This is convenient to create in a single call all the clauses (mandatory for the distributed version of the solver). It is mainly a loop to addClause().

Parameters:

clauses - a vector of set (VecInt) of literals in the dimacs format. The vector can be reused since the solver is not supposed to keep a reference to that vector.

Throws:

ContradictionException - iff the vector of literals is empty or if it contains only falsified literals after unit propagation

See Also:

addClause(IVecInt)

addAtMost

IConstr addAtMost(IVecInt literals,
                int degree)
                  throws ContradictionException

Create a cardinality constraint of the type "at most n of those literals must be satisfied"

Parameters:

literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree (n) of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if it contains more than degree satisfied literals after unit propagation

See Also:

removeConstr(IConstr)

addAtLeast

IConstr addAtLeast(IVecInt literals,
                 int degree)
                   throws ContradictionException

Create a cardinality constraint of the type "at least n of those literals must be satisfied"

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree (n) of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if degree literals are not remaining unfalsified after unit propagation

See Also:

removeConstr(IConstr)

addExactly

IConstr addExactly(IVecInt literals,
                 int n)
                   throws ContradictionException

Create a cardinality constraint of the type "exactly n of those literals must be satisfied".

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

n - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.

Since:

2.3.1

setTimeout

void setTimeout(int t)

To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver.

Parameters:

t - the timeout (in s)

setTimeoutOnConflicts

void setTimeoutOnConflicts(int count)

To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver. Here the timeout is given in number of conflicts. That way, the behavior of the solver should be the same across different architecture.

Parameters:

count - the timeout (in number of conflicts)

setTimeoutMs

void setTimeoutMs(long t)

To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver.

Parameters:

t - the timeout (in milliseconds)

getTimeout

int getTimeout()

Useful to check the internal timeout of the solver.

Returns:

the internal timeout of the solver (in seconds)

getTimeoutMs

long getTimeoutMs()

Useful to check the internal timeout of the solver.

Returns:

the internal timeout of the solver (in milliseconds)

Since:

2.1

expireTimeout

void expireTimeout()

Expire the timeout of the solver.

reset

void reset()

Clean up the internal state of the solver. Note that such method should also be called when you no longer need the solver because the state of the solver may prevent the GC to proceed. There is a known issue for instance where failing to call reset() on a solver will keep timer threads alive and exhausts memory.

printStat

@Deprecated
void printStat(PrintStream out,
                        String prefix)

Deprecated.

Display statistics to the given output stream Please use writers instead of stream.

Parameters:

out -

prefix - the prefix to put in front of each line

See Also:

printStat(PrintWriter, String)

printStat

@Deprecated
void printStat(PrintWriter out,
                        String prefix)

Deprecated. using the prefix does no longer makes sense because the solver owns it.

Display statistics to the given output writer

Parameters:

out -

prefix - the prefix to put in front of each line

Since:

1.6

printStat

void printStat(PrintWriter out)

Display statistics to the given output writer

Parameters:

out -

Since:

2.3.3

See Also:

setLogPrefix(String)

getStat

Map<String,Number> getStat()

To obtain a map of the available statistics from the solver. Note that some keys might be specific to some solvers.

Returns:

a Map with the name of the statistics as key.

toString

String toString(String prefix)

Display a textual representation of the solver configuration.

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.

clearLearntClauses

void clearLearntClauses()

Remove clauses learned during the solving process.

setDBSimplificationAllowed

void setDBSimplificationAllowed(boolean status)

Set whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables. Note that the solver should not be allowed to perform such simplification when constraint removal is planned.

isDBSimplificationAllowed

boolean isDBSimplificationAllowed()

Indicate whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables. Note that the solver should not be allowed to perform such simplification when constraint removal is planned.

setSearchListener

<S extends ISolverService> void setSearchListener(SearchListener<S> sl)

Allow the user to hook a listener to the solver to be notified of the main steps of the search process.

Parameters:

sl - a Search Listener.

Since:

2.1

setUnitClauseProvider

void setUnitClauseProvider(UnitClauseProvider ucp)

Allow the solver to ask for unit clauses before each restarts.

Parameters:

ucp - an object able to provide unit clauses.

Since:

2.3.4

getSearchListener

<S extends ISolverService> SearchListener<S> getSearchListener()

Get the current SearchListener.

Returns:

a Search Listener.

Since:

2.2

isVerbose

boolean isVerbose()

To know if the solver is in verbose mode (output allowed) or not.

Returns:

true if the solver is verbose.

Since:

2.2

setVerbose

void setVerbose(boolean value)

Set the verbosity of the solver

Parameters:

value - true to allow the solver to output messages on the console, false either.

Since:

2.2

setLogPrefix

void setLogPrefix(String prefix)

Set the prefix used to display information.

Parameters:

prefix - the prefix to be in front of each line of text

Since:

2.2

getLogPrefix

String getLogPrefix()

Returns:

the string used to prefix the output.

Since:

2.2

unsatExplanation

IVecInt unsatExplanation()

Retrieve an explanation of the inconsistency in terms of assumption literals. This is only application when isSatisfiable(assumps) is used. Note that !isSatisfiable(assumps)&&assumps.contains(unsatExplanation()) should hold.

Returns:

a subset of the assumptions used when calling isSatisfiable(assumps). Will return null if not applicable (i.e. no assumptions used).

Since:

2.2

See Also:

IProblem.isSatisfiable(IVecInt), IProblem.isSatisfiable(IVecInt, boolean)

modelWithInternalVariables

int[] modelWithInternalVariables()

That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance). If no variables are added in the solver, then Arrays.equals(model(),modelWithInternalVariables()). In case new variables are added to the solver, then the number of models returned by that method is greater of equal to the number of models returned by model() when using a ModelIterator.

Returns:

an array of literals, in Dimacs format, corresponding to a model of the formula over all the variables declared in the solver.

Since:

2.3.1

See Also:

IProblem.model(), ModelIterator

realNumberOfVariables

int realNumberOfVariables()

Retrieve the real number of variables used in the solver. In many cases, realNumberOfVariables()==nVars(). However, when working with SAT encodings or translation from MAXSAT to PMS, one can have realNumberOfVariables()>nVars(). Those additional variables are supposed to be created using the nextFreeVarId(boolean) method.

Returns:

the number of variables reserved in the solver.

Since:

2.3.1

See Also:

nextFreeVarId(boolean)

isSolverKeptHot

boolean isSolverKeptHot()

Ask to the solver if it is in "hot" mode, meaning that the heuristics is not reset after call is isSatisfiable(). This is only useful in case of repeated calls to the solver with same set of variables.

Returns:

true iff the solver keep the heuristics value unchanged across calls.

Since:

2.3.2

setKeepSolverHot

void setKeepSolverHot(boolean keepHot)

Changed the behavior of the SAT solver heuristics between successive calls. If the value is true, then the solver will be "hot" on reuse, i.e. the heuristics will not be reset. Else the heuristics will be reset.

Parameters:

keepHot - true to keep the heuristics values across calls, false either.

Since:

2.3.2

getSolvingEngine

ISolver getSolvingEngine()

Retrieve the real engine in case the engine is decorated by one or several decorator. This can be used for instance to setup the engine, which requires to bypass all the decorators. It is thus safe to downcast the ISolver to an ICDCL interface. We cannot directly return an ICDCL object because we are not on the same abstraction level here.

Returns:

the solver

Since:

2.3.3