org.sat4j.tools
Class SolverDecorator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator
All Implemented Interfaces:
java.io.Serializable, IProblem, ISolver
Direct Known Subclasses:
AbstractSelectorVariablesDecorator, GateTranslator, MinCostDecorator, Minimal4CardinalityModel, Minimal4InclusionModel, MinOneDecorator, ModelIterator, PseudoOptDecorator, SingleSolutionDetector, SolutionCounter

public abstract class SolverDecorator
extends java.lang.Object
implements ISolver, java.io.Serializable

The aim of that class is to allow adding dynamic responsabilities to SAT solvers using the Decorator design pattern. The class is abstract because it does not makes sense to use it "as is".

Author:
leberre
See Also:
Serialized Form

Constructor Summary
SolverDecorator(ISolver solver)
           
 
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.
 IConstr addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
          Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
 void clearLearntClauses()
           
 ISolver decorated()
           
 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.
 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.
 boolean isSatisfiable()
          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.
 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()
          Create a new variable in the solver (and thus in the vocabulary).
 int newVar(int howmany)
          Create howmany variables in the solver (and thus in the vocabulary).
 int nVars()
          To know the number of variables used in the solver.
 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 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.
 java.lang.String toString(java.lang.String prefix)
          Display a textual representation of the solver configuration.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

SolverDecorator

public SolverDecorator(ISolver solver)
Method Detail

clearLearntClauses

public void clearLearntClauses()
Specified by:
clearLearntClauses in interface ISolver

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.

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

setExpectedNumberOfClauses

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

Specified by:
setExpectedNumberOfClauses in interface ISolver
Parameters:
nb - the expected number of clauses.

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

toString

public java.lang.String toString(java.lang.String prefix)
Description copied from interface: ISolver
Display a textual representation of the solver configuration.

Specified by:
toString in interface ISolver
Parameters:
prefix - the prefix to use on each line.
Returns:
a textual description of the solver internals.

printStat

@Deprecated
public void printStat(java.io.PrintStream out,
                                 java.lang.String prefix)
Deprecated. 

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(java.io.PrintWriter out,
                      java.lang.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

newVar

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

Specified by:
newVar in interface ISolver
Returns:
the number of variables available in the vocabulary, which is the identifier of the new variable.

newVar

public int newVar(int howmany)
Description copied from interface: ISolver
Create howmany variables in the solver (and thus in the vocabulary).

Specified by:
newVar in interface ISolver
Parameters:
howmany - number of variables to create
Returns:
the total number of variables available in the solver (the highest variable number)

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException
Description copied from interface: ISolver
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. (clasical Dimacs way of representing literals).

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

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)

addAtMost

public IConstr addAtMost(IVecInt literals,
                         int degree)
                  throws ContradictionException
Description copied from interface: ISolver
Create a cardinality constraint of the type "at most n of those literals must be satisfied"

Specified by:
addAtMost in interface ISolver
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:
ISolver.removeConstr(IConstr)

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                          int degree)
                   throws ContradictionException
Description copied from interface: ISolver
Create a cardinality constraint of the type "at least n of those literals must be satisfied"

Specified by:
addAtLeast in interface ISolver
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:
ISolver.removeConstr(IConstr)

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt literals,
                                IVec<java.math.BigInteger> coeffs,
                                boolean moreThan,
                                java.math.BigInteger degree)
                         throws ContradictionException
Description copied from interface: ISolver
Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Specified by:
addPseudoBoolean in interface ISolver
Parameters:
literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
moreThan - true if it is a constraint >= degree
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 the constraint is falsified after unit propagation
See Also:
ISolver.removeConstr(IConstr)

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)

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

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)

nConstraints

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

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

nVars

public int nVars()
Description copied from interface: IProblem
To know the number of variables used in the solver.

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

reset

public void reset()
Description copied from interface: ISolver
Clean up the internal state of the solver.

Specified by:
reset in interface ISolver

decorated

public ISolver decorated()

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 learnt clauses will be cleared.

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

getStat

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


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