org.sat4j.tools
Class AbstractOutputSolver

java.lang.Object
  extended by org.sat4j.tools.AbstractOutputSolver
All Implemented Interfaces:
Serializable, IProblem, ISolver
Direct Known Subclasses:
DimacsOutputSolver, DimacsStringSolver

public abstract class AbstractOutputSolver
extends Object
implements ISolver

See Also:
Serialized Form

Field Summary
protected  boolean firstConstr
           
protected  boolean fixedNbClauses
           
protected  int nbclauses
           
protected  int nbvars
           
 
Constructor Summary
AbstractOutputSolver()
           
 
Method Summary
 void addAllClauses(IVec<IVecInt> clauses)
          Create clauses from a set of set of literals.
 IConstr addBlockingClause(IVecInt literals)
          Add a clause in order to prevent an assignment to occur.
 void clearLearntClauses()
          Remove clauses learned during the solving process.
 void expireTimeout()
          Expire the timeout of the solver.
 int[] findModel()
          Look for a model satisfying all the clauses available in the problem.
 int[] findModel(IVecInt assumps)
          Look for a model satisfying all the clauses available in the problem.
 String getLogPrefix()
           
<S extends ISolverService>
SearchListener<S>
getSearchListener()
          Get the current SearchListener.
 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 isSatisfiable()
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(boolean global)
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(IVecInt assumps)
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(IVecInt assumps, boolean global)
          Check the satisfiability of the set of constraints contained inside the solver.
 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[] model()
          Provide a model (if any) for a satisfiable formula.
 boolean model(int var)
          Provide the truth value of a specific variable in the model.
 int nConstraints()
          To know the number of constraints currently available in the solver.
 int newVar(int howmany)
          Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany.
 int nVars()
          To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.
 int[] primeImplicant()
          Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.
 void printInfos(PrintWriter output, String prefix)
          To print additional informations regarding the problem.
 void printStat(PrintStream output, String prefix)
          Display statistics to the given output stream Please use writers instead of stream.
 void printStat(PrintWriter output, 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.
 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 setDBSimplificationAllowed(boolean status)
          Set whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.
 void setKeepSolverHot(boolean value)
          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 setVerbose(boolean value)
          Set the verbosity of the solver
 IVecInt unsatExplanation()
          Retrieve an explanation of the inconsistency in terms of assumption literals.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.sat4j.specs.ISolver
addAtLeast, addAtMost, addClause, addExactly, modelWithInternalVariables, newVar, nextFreeVarId, realNumberOfVariables, registerLiteral, reset, setExpectedNumberOfClauses, toString
 
Methods inherited from interface org.sat4j.specs.IProblem
primeImplicant
 

Field Detail

nbvars

protected int nbvars

nbclauses

protected int nbclauses

fixedNbClauses

protected boolean fixedNbClauses

firstConstr

protected boolean firstConstr
Constructor Detail

AbstractOutputSolver

public AbstractOutputSolver()
Method Detail

removeConstr

public boolean removeConstr(IConstr c)
Description copied from interface: ISolver
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.

Specified by:
removeConstr in interface ISolver
Parameters:
c - a constraint returned by one of the add method.
Returns:
true if the constraint was successfully removed.

addAllClauses

public void addAllClauses(IVec<IVecInt> clauses)
                   throws ContradictionException
Description copied from interface: ISolver
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().

Specified by:
addAllClauses in interface ISolver
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:
ISolver.addClause(IVecInt)

setTimeout

public void setTimeout(int t)
Description copied from interface: ISolver
To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver.

Specified by:
setTimeout in interface ISolver
Parameters:
t - the timeout (in s)

setTimeoutMs

public void setTimeoutMs(long t)
Description copied from interface: ISolver
To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver.

Specified by:
setTimeoutMs in interface ISolver
Parameters:
t - the timeout (in milliseconds)

getTimeout

public int getTimeout()
Description copied from interface: ISolver
Useful to check the internal timeout of the solver.

Specified by:
getTimeout in interface ISolver
Returns:
the internal timeout of the solver (in seconds)

getTimeoutMs

public long getTimeoutMs()
Description copied from interface: ISolver
Useful to check the internal timeout of the solver.

Specified by:
getTimeoutMs in interface ISolver
Returns:
the internal timeout of the solver (in milliseconds)
Since:
2.1

expireTimeout

public void expireTimeout()
Description copied from interface: ISolver
Expire the timeout of the solver.

Specified by:
expireTimeout in interface ISolver

isSatisfiable

public boolean isSatisfiable(IVecInt assumps,
                             boolean global)
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Parameters:
assumps - a set of literals (represented by usual non null integers in Dimacs format).
global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
Returns:
true if the set of constraints is satisfiable when literals are satisfied, else false.
Throws:
TimeoutException

isSatisfiable

public boolean isSatisfiable(boolean global)
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Parameters:
global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
Returns:
true if the set of constraints is satisfiable, else false.
Throws:
TimeoutException

printInfos

public void printInfos(PrintWriter output,
                       String prefix)
Description copied from interface: IProblem
To print additional informations regarding the problem.

Specified by:
printInfos in interface IProblem
Parameters:
output - the place to print the information
prefix - the prefix to put in front of each line

setTimeoutOnConflicts

public void setTimeoutOnConflicts(int count)
Description copied from interface: ISolver
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.

Specified by:
setTimeoutOnConflicts in interface ISolver
Parameters:
count - the timeout (in number of counflicts)

isDBSimplificationAllowed

public boolean isDBSimplificationAllowed()
Description copied from interface: ISolver
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.

Specified by:
isDBSimplificationAllowed in interface ISolver

setDBSimplificationAllowed

public void setDBSimplificationAllowed(boolean status)
Description copied from interface: ISolver
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.

Specified by:
setDBSimplificationAllowed in interface ISolver

printStat

public void printStat(PrintStream output,
                      String prefix)
Description copied from interface: ISolver
Display statistics to the given output stream Please use writers instead of stream.

Specified by:
printStat in interface ISolver
prefix - the prefix to put in front of each line
See Also:
ISolver.printStat(PrintWriter, String)

printStat

public void printStat(PrintWriter output,
                      String prefix)
Description copied from interface: ISolver
Display statistics to the given output writer

Specified by:
printStat in interface ISolver
prefix - the prefix to put in front of each line

getStat

public Map<String,Number> getStat()
Description copied from interface: ISolver
To obtain a map of the available statistics from the solver. Note that some keys might be specific to some solvers.

Specified by:
getStat in interface ISolver
Returns:
a Map with the name of the statistics as key.

clearLearntClauses

public void clearLearntClauses()
Description copied from interface: ISolver
Remove clauses learned during the solving process.

Specified by:
clearLearntClauses in interface ISolver

model

public int[] model()
Description copied from interface: IProblem
Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:
model in interface IProblem
Returns:
a model of the formula as an array of literals to satisfy.
See Also:
IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

model

public boolean model(int var)
Description copied from interface: IProblem
Provide the truth value of a specific variable in the model. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:
model in interface IProblem
Parameters:
var - the variable id in Dimacs format
Returns:
the truth value of that variable in the model
See Also:
IProblem.model()

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Returns:
true if the set of constraints is satisfiable, else false.
Throws:
TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Parameters:
assumps - a set of literals (represented by usual non null integers in Dimacs format).
Returns:
true if the set of constraints is satisfiable when literals are satisfied, else false.
Throws:
TimeoutException

findModel

public int[] findModel()
                throws TimeoutException
Description copied from interface: IProblem
Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable() and model() methods, as shown in the pseudo-code: if (isSatisfiable()) { return model(); } return null;

Specified by:
findModel in interface IProblem
Returns:
a model of the formula as an array of literals to satisfy, or null if no model is found
Throws:
TimeoutException - if a model cannot be found within the given timeout.

findModel

public int[] findModel(IVecInt assumps)
                throws TimeoutException
Description copied from interface: IProblem
Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable(IVecInt) and model() methods, as shown in the pseudo-code: if (isSatisfiable(assumpt)) { return model(); } return null;

Specified by:
findModel in interface IProblem
Returns:
a model of the formula as an array of literals to satisfy, or null if no model is found
Throws:
TimeoutException - if a model cannot be found within the given timeout.

removeSubsumedConstr

public boolean removeSubsumedConstr(IConstr c)
Description copied from interface: ISolver
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.

Specified by:
removeSubsumedConstr in interface ISolver
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

addBlockingClause

public IConstr addBlockingClause(IVecInt literals)
                          throws ContradictionException
Description copied from interface: ISolver
Add a clause in order to prevent an assignment to occur. This happens usually when iterating over models for instance.

Specified by:
addBlockingClause in interface ISolver
Returns:
Throws:
ContradictionException
Since:
2.1

getSearchListener

public <S extends ISolverService> SearchListener<S> getSearchListener()
Description copied from interface: ISolver
Get the current SearchListener.

Specified by:
getSearchListener in interface ISolver
Returns:
a Search Listener.
Since:
2.2

setSearchListener

public <S extends ISolverService> void setSearchListener(SearchListener<S> sl)
Description copied from interface: ISolver
Allow the user to hook a listener to the solver to be notified of the main steps of the search process.

Specified by:
setSearchListener in interface ISolver
Parameters:
sl - a Search Listener.
Since:
2.1

isVerbose

public boolean isVerbose()
Description copied from interface: ISolver
To know if the solver is in verbose mode (output allowed) or not.

Specified by:
isVerbose in interface ISolver
Returns:
true if the solver is verbose.
Since:
2.2

setVerbose

public void setVerbose(boolean value)
Description copied from interface: ISolver
Set the verbosity of the solver

Specified by:
setVerbose in interface ISolver
Parameters:
value - true to allow the solver to output messages on the console, false either.
Since:
2.2

setLogPrefix

public void setLogPrefix(String prefix)
Description copied from interface: ISolver
Set the prefix used to display information.

Specified by:
setLogPrefix in interface ISolver
Parameters:
prefix - the prefix to be in front of each line of text
Since:
2.2

getLogPrefix

public String getLogPrefix()
Specified by:
getLogPrefix in interface ISolver
Returns:
the string used to prefix the output.
Since:
2.2

unsatExplanation

public IVecInt unsatExplanation()
Description copied from interface: ISolver
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.

Specified by:
unsatExplanation in interface ISolver
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)

primeImplicant

public int[] primeImplicant()
Description copied from interface: IProblem
Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.

Specified by:
primeImplicant in interface IProblem
Returns:
a prime implicant of the formula as an array of literal, Dimacs format.

nConstraints

public int nConstraints()
Description copied from interface: IProblem
To know the number of constraints currently available in the solver. (without taking into account learned constraints).

Specified by:
nConstraints in interface IProblem
Returns:
the number of constraints added to the solver

newVar

public int newVar(int howmany)
Description copied from interface: IProblem
Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany. That feature allows encodings to create additional variables with identifier starting at howmany+1.

Specified by:
newVar in interface IProblem
Parameters:
howmany - number of variables to create
Returns:
the total number of variables available in the solver (the highest variable number)
See Also:
IProblem.nVars()

nVars

public int nVars()
Description copied from interface: IProblem
To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.

Specified by:
nVars in interface IProblem
Returns:
the number of variables created using newVar().
See Also:
IProblem.newVar(int)

isSolverKeptHot

public boolean isSolverKeptHot()
Description copied from interface: ISolver
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.

Specified by:
isSolverKeptHot in interface ISolver
Returns:
true iff the solver keep the heuristics value unchanged across calls.

setKeepSolverHot

public void setKeepSolverHot(boolean value)
Description copied from interface: ISolver
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.

Specified by:
setKeepSolverHot in interface ISolver
Parameters:
value - true to keep the heuristics values across calls, false either.


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