org.sat4j.minisat.core
Class Solver<D extends DataStructureFactory>

java.lang.Object
  extended by org.sat4j.minisat.core.Solver<D>
All Implemented Interfaces:
Serializable, Learner, UnitPropagationListener, IProblem, ISolver

public class Solver<D extends DataStructureFactory>
extends Object
implements ISolver, UnitPropagationListener, Learner

The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Author:
leberre
See Also:
Serialized Form

Field Summary
protected  AssertingClauseGenerator analyzer
           
protected  D dsfactory
           
 org.sat4j.minisat.core.Solver.ISimplifier EXPENSIVE_SIMPLIFICATION
           
 org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy glucose
           
 org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy memory_based
           
static org.sat4j.minisat.core.Solver.ISimplifier NO_SIMPLIFICATION
           
protected  int rootLevel
          S?
 org.sat4j.minisat.core.Solver.ISimplifier SIMPLE_SIMPLIFICATION
           
protected  IVecInt trail
          affectation en ordre chronologique
protected  IVecInt trailLim
          indice des s?
protected  ILits voc
           
 
Constructor Summary
Solver(AssertingClauseGenerator acg, LearningStrategy<D> learner, D dsf, IOrder order, RestartStrategy restarter)
          creates a Solver without LearningListener.
Solver(AssertingClauseGenerator acg, LearningStrategy<D> learner, D dsf, SearchParams params, IOrder order, RestartStrategy restarter)
           
 
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 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.
protected  IConstr addConstr(Constr constr)
           
 void analyze(Constr confl, Pair results)
           
protected  void analyzeAtRootLevel(Constr conflict)
           
 IVecInt analyzeFinalConflictInTermsOfAssumptions(Constr confl, IVecInt assumps, int conflictingLiteral)
          Derive a subset of the assumptions causing the inconistency.
 boolean assume(int p)
           
protected  void cancelUntil(int level)
          Cancel several levels of assumptions
 void claBumpActivity(Constr confl)
          Propagate activity to a constraint
 void clearLearntClauses()
          Remove clauses learned during the solving process.
protected  void decayActivities()
           
 int decisionLevel()
           
protected  IVecInt dimacs2internal(IVecInt in)
           
 boolean enqueue(int p)
          Satisfait un litt?
 boolean enqueue(int p, Constr from)
          Put the literal on the queue of assignments to be done.
 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.
 DataStructureFactory getDSFactory()
           
 IConstr getIthConstr(int i)
          returns the ith constraint in the solver.
 String getLogPrefix()
           
 IOrder getOrder()
           
 IVecInt getOutLearnt()
           
 SearchListener getSearchListener()
          Get the current SearchListener.
 Map<String,Number> getStat()
          To obtain a map of the available statistics from the solver.
 SolverStats getStats()
           
 int getTimeout()
          Useful to check the internal timeout of the solver.
 long getTimeoutMs()
          Useful to check the internal timeout of the solver.
 ILits getVocabulary()
           
protected  void initStats(SolverStats myStats)
           
 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 isVerbose()
          To know if the solver is in verbose mode (output allowed) or not.
 void learn(Constr c)
           
 int[] model()
          Si un mod?
 boolean model(int var)
          Provide the truth value of a specific variable in the model.
protected  int nAssigns()
           
 int nConstraints()
          To know the number of constraints currently available in the solver.
 int newVar()
          Deprecated. 
 int newVar(int howmany)
          Create howmany variables in the solver (and thus in the vocabulary).
 int nextFreeVarId(boolean reserve)
          Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).
 int nVars()
          To know the number of variables used in the solver.
 void printInfos(PrintWriter out, String prefix)
          To print additional informations regarding the problem.
 void printLearntClausesInfos(PrintWriter out, String prefix)
           
 void printStat(PrintStream out, String prefix)
          Display statistics to the given output stream Please use writers instead of stream.
 void printStat(PrintWriter out, String prefix)
          Display statistics to the given output writer
 Constr propagate()
           
protected  void reduceDB()
           
 boolean removeConstr(IConstr co)
          Remove a constraint returned by one of the add method from the solver.
 boolean removeSubsumedConstr(IConstr co)
          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 setDataStructureFactory(D dsf)
          Change the internal representation of the constraints.
 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 setLearnedConstraintsDeletionStrategy(org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy lcds)
           
 void setLearner(LearningStrategy<D> learner)
           
 void setLogPrefix(String prefix)
          Set the prefix used to display information.
 void setOrder(IOrder h)
           
 void setRestartStrategy(RestartStrategy restarter)
           
 void setSearchListener(SearchListener sl)
          Allow the user to hook a listener to the solver to be notified of the main steps of the search process.
 void setSearchParams(SearchParams sp)
           
 void setSimplifier(org.sat4j.minisat.core.Solver.ISimplifier simp)
          Setup the reason simplification strategy.
 void setSimplifier(String simp)
          Setup the reason simplification strategy.
 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
 boolean simplifyDB()
           
 String toString()
           
 String toString(String prefix)
          Display a textual representation of the solver configuration.
protected  void undoOne()
           
 IVecInt unsatExplanation()
          Retrieve an explanation of the inconsistency in terms of assumption literals.
 void unset(int p)
          Unset a unit clause.
 void varBumpActivity(int p)
          Update the activity of a variable v.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

trail

protected final IVecInt trail
affectation en ordre chronologique


trailLim

protected final IVecInt trailLim
indice des s?parateurs des diff?rents niveau de d?cision dans trail


rootLevel

protected int rootLevel
S?pare les hypoth?ses incr?mentale et recherche


voc

protected ILits voc

analyzer

protected final AssertingClauseGenerator analyzer

dsfactory

protected D extends DataStructureFactory dsfactory

NO_SIMPLIFICATION

public static final org.sat4j.minisat.core.Solver.ISimplifier NO_SIMPLIFICATION

SIMPLE_SIMPLIFICATION

public final org.sat4j.minisat.core.Solver.ISimplifier SIMPLE_SIMPLIFICATION

EXPENSIVE_SIMPLIFICATION

public final org.sat4j.minisat.core.Solver.ISimplifier EXPENSIVE_SIMPLIFICATION

memory_based

public final org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy memory_based
Since:
2.1

glucose

public final org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy glucose
Since:
2.1
Constructor Detail

Solver

public Solver(AssertingClauseGenerator acg,
              LearningStrategy<D> learner,
              D dsf,
              IOrder order,
              RestartStrategy restarter)
creates a Solver without LearningListener. A learningListener must be added to the solver, else it won't backtrack!!! A data structure factory must be provided, else it won't work either.

Parameters:
acg - an asserting clause generator

Solver

public Solver(AssertingClauseGenerator acg,
              LearningStrategy<D> learner,
              D dsf,
              SearchParams params,
              IOrder order,
              RestartStrategy restarter)
Method Detail

dimacs2internal

protected IVecInt dimacs2internal(IVecInt in)

setDataStructureFactory

public final void setDataStructureFactory(D dsf)
Change the internal representation of the constraints. Note that the heuristics must be changed prior to calling that method.

Parameters:
dsf - the internal factory

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 -
Since:
2.2

setSearchListener

public void setSearchListener(SearchListener 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

getSearchListener

public SearchListener getSearchListener()
Description copied from interface: ISolver
Get the current SearchListener.

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

setLearner

public void setLearner(LearningStrategy<D> learner)
Since:
2.2

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)

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)

setSearchParams

public void setSearchParams(SearchParams sp)

setRestartStrategy

public void setRestartStrategy(RestartStrategy restarter)

expireTimeout

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

Specified by:
expireTimeout in interface ISolver

nAssigns

protected int nAssigns()

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

learn

public void learn(Constr c)
Specified by:
learn in interface Learner

decisionLevel

public final int decisionLevel()

newVar

@Deprecated
public int newVar()
Deprecated. 

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

removeConstr

public boolean removeConstr(IConstr co)
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:
co - a constraint returned by one of the add method.
Returns:
true if the constraint was successfully removed.

removeSubsumedConstr

public boolean removeSubsumedConstr(IConstr co)
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:
co - 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

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)

simplifyDB

public boolean simplifyDB()

model

public int[] model()
Si un mod?le est trouv?, ce vecteur contient le mod?le.

Specified by:
model in interface IProblem
Returns:
un mod?le de la formule.
See Also:
IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

enqueue

public boolean enqueue(int p)
Satisfait un litt?ral

Specified by:
enqueue in interface UnitPropagationListener
Parameters:
p - le litt?ral
Returns:
true si tout se passe bien, false si un conflit appara?t.

enqueue

public boolean enqueue(int p,
                       Constr from)
Put the literal on the queue of assignments to be done.

Specified by:
enqueue in interface UnitPropagationListener
Parameters:
p - the literal.
from - the reason to propagate that literal, else null
Returns:
true if the assignment can be made, false if a conflict is detected.

analyze

public void analyze(Constr confl,
                    Pair results)

analyzeFinalConflictInTermsOfAssumptions

public IVecInt analyzeFinalConflictInTermsOfAssumptions(Constr confl,
                                                        IVecInt assumps,
                                                        int conflictingLiteral)
Derive a subset of the assumptions causing the inconistency.

Parameters:
confl - the last conflict of the search, occuring at root level.
assumps - the set of assumption literals
conflictingLiteral - the literal detected conflicting while propagating assumptions.
Returns:
a subset of assumps causing the inconsistency.
Since:
2.2

setSimplifier

public void setSimplifier(String simp)
Setup the reason simplification strategy. By default, there is no reason simplification. NOTE THAT REASON SIMPLIFICATION DOES NOT WORK WITH SPECIFIC DATA STRUCTURE FOR HANDLING BOTH BINARY AND TERNARY CLAUSES.

Parameters:
simp - the name of the simplifier (one of NO_SIMPLIFICATION, SIMPLE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION).

setSimplifier

public void setSimplifier(org.sat4j.minisat.core.Solver.ISimplifier simp)
Setup the reason simplification strategy. By default, there is no reason simplification. NOTE THAT REASON SIMPLIFICATION IS ONLY ALLOWED FOR WL CLAUSAL data structures. USING REASON SIMPLIFICATION ON CB CLAUSES, CARDINALITY CONSTRAINTS OR PB CONSTRAINTS MIGHT RESULT IN INCORRECT RESULTS.

Parameters:
simp -

undoOne

protected void undoOne()

claBumpActivity

public void claBumpActivity(Constr confl)
Propagate activity to a constraint

Parameters:
confl - a constraint

varBumpActivity

public void varBumpActivity(int p)
Description copied from interface: VarActivityListener
Update the activity of a variable v.

Parameters:
p - a literal (v<<1 or v<<1^1)

propagate

public Constr propagate()
Returns:
null if not conflict is found, else a conflicting constraint.

assume

public boolean assume(int p)
Returns:
false ssi conflit imm?diat.

cancelUntil

protected void cancelUntil(int level)
Cancel several levels of assumptions

Parameters:
level -

analyzeAtRootLevel

protected void analyzeAtRootLevel(Constr conflict)

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

clearLearntClauses

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

Specified by:
clearLearntClauses in interface ISolver

reduceDB

protected void reduceDB()

decayActivities

protected void decayActivities()

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 iff the set of constraints is satisfiable, 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 iff 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

setLearnedConstraintsDeletionStrategy

public void setLearnedConstraintsDeletionStrategy(org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy lcds)
Parameters:
lcds -
Since:
2.1

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

printInfos

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

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

printLearntClausesInfos

public void printLearntClausesInfos(PrintWriter out,
                                    String prefix)
Since:
2.1

getStats

public SolverStats getStats()

initStats

protected void initStats(SolverStats myStats)
Parameters:
myStats -
Since:
2.2

getOrder

public IOrder getOrder()

setOrder

public void setOrder(IOrder h)

getVocabulary

public ILits getVocabulary()

reset

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

Specified by:
reset in interface ISolver

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

addConstr

protected IConstr addConstr(Constr constr)
Parameters:
constr - a constraint implementing the Constr interface.
Returns:
a reference to the constraint for external use.

getDSFactory

public DataStructureFactory getDSFactory()

getOutLearnt

public IVecInt getOutLearnt()

getIthConstr

public IConstr getIthConstr(int i)
returns the ith constraint in the solver.

Parameters:
i - the constraint number (begins at 0)
Returns:
the ith constraint

printStat

public void printStat(PrintStream out,
                      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 out,
                      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

toString

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

toString

public String toString()
Overrides:
toString in class Object

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

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. Note that this method is supposed to be called AFTER a call to newVar(int)

Specified by:
setExpectedNumberOfClauses in interface ISolver
Parameters:
nb - the expected number of clauses.
See Also:
ISolver.newVar(int)

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.

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.

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

nextFreeVarId

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

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

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

unset

public void unset(int p)
Description copied from interface: UnitPropagationListener
Unset a unit clause. The effect of such method is to unset all truth values on the stack until the given literal is found (that literal included).

Specified by:
unset in interface UnitPropagationListener
Since:
2.1

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)


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