org.sat4j.tools

Class ManyCore<S extends ISolver>

java.lang.Object

org.sat4j.tools.SearchListenerAdapter<ISolverService>

org.sat4j.tools.ManyCore<S>

Type Parameters:

S - the type of the solver (ISolver of IPBSolver)

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel, SearchListener<ISolverService>, UnitClauseProvider, OutcomeListener

public class ManyCore<S extends ISolver>
extends SearchListenerAdapter<ISolverService>
implements ISolver, OutcomeListener, UnitClauseProvider

A class allowing to run several solvers in parallel. Note that each solver will have its own copy of the CNF, so it is not a memory efficient implementation. There is no sharing of information yet between the solvers.

Author:

leberre

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
protected int	numberOfSolvers
protected List<S>	solvers

Fields inherited from interface org.sat4j.specs.UnitClauseProvider

VOID

Constructor Summary

Constructors

Constructor and Description
ManyCore(ASolverFactory<S> factory, String... solverNames)
ManyCore(S... solverObjects)
ManyCore(String[] names, S... solverObjects) Create a parallel solver from a list of solvers and a list of names.

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.
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()
<I extends ISolverService> SearchListener<I>	getSearchListener() Get the current SearchListener.
List<S>	getSolvers()
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	isSatisfiable() Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(boolean globalTimeout) 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 globalTimeout) 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.
void	learnUnit(int p) learn a new unit clause (a literal)
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[]	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	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) 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	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 as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.
void	onFinishWithAnswer(boolean finished, boolean result, int index)
int[]	primeImplicant() Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.
boolean	primeImplicant(int p) Check if a given literal is part of the prime implicant computed by the IProblem.primeImplicant() method.
void	printInfos(PrintWriter out) To print additional informations regarding the problem.
void	printInfos(PrintWriter out, String prefix) To print additional informations regarding the problem.
void	printStat(PrintStream out, String prefix) Deprecated.
void	printStat(PrintWriter out) Display statistics to the given output writer
void	printStat(PrintWriter out, String prefix) Display statistics to the given output writer
void	provideUnitClauses(UnitPropagationListener upl)
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 value) Changed the behavior of the SAT solver heuristics between successive calls.
void	setLogPrefix(String prefix) Set the prefix used to display information.
<I extends ISolverService> void	setSearchListener(SearchListener<I> 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 class org.sat4j.tools.SearchListenerAdapter

adding, assuming, backjump, backtracking, beginLoop, cleaning, conflictFound, conflictFound, delete, end, init, learn, propagating, restarting, solutionFound, start

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

solvers

protected final List<S extends ISolver> solvers

numberOfSolvers

protected final int numberOfSolvers

Constructor Detail

ManyCore

public ManyCore(ASolverFactory<S> factory,
        String... solverNames)

ManyCore

public ManyCore(String[] names,
        S... solverObjects)

Create a parallel solver from a list of solvers and a list of names.

Parameters:

names - a String to describe each solver in the messages.

solverObjects - the solvers

ManyCore

public ManyCore(S... solverObjects)

Method Detail

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)

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

ISolver.removeConstr(IConstr)

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

ISolver.removeConstr(IConstr)

addExactly

public IConstr addExactly(IVecInt literals,
                 int n)
                   throws ContradictionException

Description copied from interface: ISolver

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

Specified by:

addExactly 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.

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.

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)

clearLearntClauses

public void clearLearntClauses()

Description copied from interface: ISolver

Remove clauses learned during the solving process.

Specified by:

clearLearntClauses in interface ISolver

expireTimeout

public void expireTimeout()

Description copied from interface: ISolver

Expire the timeout of the solver.

Specified by:

expireTimeout in interface ISolver

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.

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)

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

printStat

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

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.

reset

public void reset()

Description copied from interface: ISolver

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.

Specified by:

reset in interface ISolver

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:

IProblem.newVar(int)

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

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.

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.

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,
                    boolean globalTimeout)
                      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).

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

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

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

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

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 RandomAccessModel

Parameters:

var - the variable id in Dimacs format

Returns:

the truth value of that variable in the model

See Also:

#model()

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

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)

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

onFinishWithAnswer

public void onFinishWithAnswer(boolean finished,
                      boolean result,
                      int index)

Specified by:

onFinishWithAnswer in interface OutcomeListener

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

setSearchListener

public <I extends ISolverService> void setSearchListener(SearchListener<I> 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.

getSearchListener

public <I extends ISolverService> SearchListener<I> getSearchListener()

Description copied from interface: ISolver

Get the current SearchListener.

Specified by:

getSearchListener in interface ISolver

Returns:

a Search Listener.

Since:

2.2

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. The number of variables reserved in the solver is accessible through the ISolver.realNumberOfVariables() method.

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.

See Also:

ISolver.realNumberOfVariables()

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

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.

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.

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.

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

getLogPrefix

public String getLogPrefix()

Specified by:

getLogPrefix in interface ISolver

Returns:

the string used to prefix the output.

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

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.

primeImplicant

public boolean primeImplicant(int p)

Description copied from interface: IProblem

Check if a given literal is part of the prime implicant computed by the IProblem.primeImplicant() method.

Specified by:

primeImplicant in interface IProblem

Parameters:

p - a literal in Dimacs format

Returns:

true iff p belongs to IProblem.primeImplicant()

Since:

2.3.2

getSolvers

public List<S> getSolvers()

modelWithInternalVariables

public int[] modelWithInternalVariables()

Description copied from interface: ISolver

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.

Specified by:

modelWithInternalVariables in interface ISolver

Returns:

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

See Also:

IProblem.model(), ModelIterator

realNumberOfVariables

public int realNumberOfVariables()

Description copied from interface: ISolver

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 ISolver.nextFreeVarId(boolean) method.

Specified by:

realNumberOfVariables in interface ISolver

Returns:

the number of variables reserved in the solver.

See Also:

ISolver.nextFreeVarId(boolean)

registerLiteral

public void registerLiteral(int p)

Description copied from interface: ISolver

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.

Specified by:

registerLiteral in interface ISolver

Parameters:

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

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.

getSolvingEngine

public ISolver getSolvingEngine()

Description copied from interface: ISolver

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.

Specified by:

getSolvingEngine in interface ISolver

Returns:

the solver

printStat

public void printStat(PrintWriter out)

Description copied from interface: ISolver

Display statistics to the given output writer

Specified by:

printStat in interface ISolver

Since:

2.3.3

See Also:

ISolver.setLogPrefix(String)

printInfos

public void printInfos(PrintWriter out)

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

Since:

2.3.3

See Also:

#setLogPrefix(String)

learnUnit

public void learnUnit(int p)

Description copied from interface: SearchListener

learn a new unit clause (a literal)

Specified by:

learnUnit in interface SearchListener<ISolverService>

Overrides:

learnUnit in class SearchListenerAdapter<ISolverService>

Parameters:

p - a literal in Dimacs format.

provideUnitClauses

public void provideUnitClauses(UnitPropagationListener upl)

Specified by:

provideUnitClauses in interface UnitClauseProvider

setUnitClauseProvider

public void setUnitClauseProvider(UnitClauseProvider ucp)

Description copied from interface: ISolver

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

Specified by:

setUnitClauseProvider in interface ISolver

Parameters:

ucp - an object able to provide unit clauses.