org.sat4j.specs
Interface ISolver

All Superinterfaces:
IProblem, java.io.Serializable
All Known Implementing Classes:
AbstractSelectorVariablesDecorator, DimacsOutputSolver, DimacsStringSolver, GateTranslator, MaxSatDecorator, Minimal4CardinalityModel, Minimal4InclusionModel, MinOneDecorator, ModelIterator, OptToSatAdapter, SingleSolutionDetector, SolutionCounter, Solver, SolverDecorator

public interface ISolver
extends IProblem, java.io.Serializable

This interface contains all services provided by a SAT solver.

Author:
leberre

Method Summary
 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 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.
 void clearLearntClauses()
          Remove clauses learned during the solving process.
 void expireTimeout()
          Expire the timeout of the solver.
 java.util.Map<java.lang.String,java.lang.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.
 int newVar()
          Deprecated. 
 int newVar(int howmany)
          Create howmany variables in the solver (and thus in the vocabulary).
 void printStat(java.io.PrintStream out, java.lang.String prefix)
          Deprecated. 
 void printStat(java.io.PrintWriter out, java.lang.String prefix)
          Display statistics to the given output writer
 boolean removeConstr(IConstr c)
          Remove a constraint returned by one of the add method from 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 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.
 java.lang.String toString(java.lang.String prefix)
          Display a textual representation of the solver configuration.
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, nVars, printInfos
 

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.

newVar

int newVar(int howmany)
Create howmany variables in the solver (and thus in the vocabulary).

Parameters:
howmany - number of variables to create
Returns:
the total number of variables available in the solver (the highest variable number)

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:
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)

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.

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 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 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)

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 counflicts)

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)

expireTimeout

void expireTimeout()
Expire the timeout of the solver.


reset

void reset()
Clean up the internal state of the solver.


printStat

@Deprecated
void printStat(java.io.PrintStream out,
                          java.lang.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

void printStat(java.io.PrintWriter out,
               java.lang.String prefix)
Display statistics to the given output writer

Parameters:
out -
prefix - the prefix to put in front of each line
Since:
1.6

getStat

java.util.Map<java.lang.String,java.lang.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

java.lang.String toString(java.lang.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.



Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.