org.sat4j.multicore
Class ManyCore<S extends ISolver>

java.lang.Object
  org.sat4j.multicore.ManyCore<S>

All Implemented Interfaces:

Serializable, IProblem, ISolver

Direct Known Subclasses:

ManyCorePB

public class ManyCore<S extends ISolver>
extends Object
implements ISolver

See Also:

Serialized Form

Field Summary

protected int	numberOfSolvers
protected List<S>	solvers

Constructor Summary

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

Method Summary

void	addAllClauses(IVec<IVecInt> clauses)
IConstr	addAtLeast(IVecInt literals, int degree)
IConstr	addAtMost(IVecInt literals, int degree)
IConstr	addBlockingClause(IVecInt literals)
IConstr	addClause(IVecInt literals)
void	clearLearntClauses()
void	expireTimeout()
int[]	findModel()
int[]	findModel(IVecInt assumps)
String	getLogPrefix()
SearchListener	getSearchListener()
Map<String,Number>	getStat()
int	getTimeout()
long	getTimeoutMs()
boolean	isDBSimplificationAllowed()
boolean	isSatisfiable()
boolean	isSatisfiable(boolean globalTimeout)
boolean	isSatisfiable(IVecInt assumps)
boolean	isSatisfiable(IVecInt assumps, boolean globalTimeout)
boolean	isVerbose()
int[]	model()
boolean	model(int var)
int	nConstraints()
int	newVar()
int	newVar(int howmany)
int	nextFreeVarId(boolean reserve)
int	nVars()
void	onFinishWithAnswer(boolean finished, boolean result, int index)
void	printInfos(PrintWriter out, String prefix)
void	printStat(PrintStream out, String prefix) Deprecated.
void	printStat(PrintWriter out, String prefix)
boolean	removeConstr(IConstr c)
boolean	removeSubsumedConstr(IConstr c)
void	reset()
void	setDBSimplificationAllowed(boolean status)
void	setExpectedNumberOfClauses(int nb)
void	setLogPrefix(String prefix)
void	setSearchListener(SearchListener sl)
void	setTimeout(int t)
void	setTimeoutMs(long t)
void	setTimeoutOnConflicts(int count)
void	setVerbose(boolean value)
String	toString(String prefix)
IVecInt	unsatExplanation()

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)

Method Detail

addAllClauses

public void addAllClauses(IVec<IVecInt> clauses)
                   throws ContradictionException

Specified by:

addAllClauses in interface ISolver

Throws:

ContradictionException

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                          int degree)
                   throws ContradictionException

Specified by:

addAtLeast in interface ISolver

Throws:

ContradictionException

addAtMost

public IConstr addAtMost(IVecInt literals,
                         int degree)
                  throws ContradictionException

Specified by:

addAtMost in interface ISolver

Throws:

ContradictionException

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Specified by:

addClause in interface ISolver

Throws:

ContradictionException

clearLearntClauses

public void clearLearntClauses()

Specified by:

clearLearntClauses in interface ISolver

expireTimeout

public void expireTimeout()

Specified by:

expireTimeout in interface ISolver

getStat

public Map<String,Number> getStat()

Specified by:

getStat in interface ISolver

getTimeout

public int getTimeout()

Specified by:

getTimeout in interface ISolver

getTimeoutMs

public long getTimeoutMs()

Specified by:

getTimeoutMs in interface ISolver

newVar

public int newVar()

Specified by:

newVar in interface ISolver

newVar

public int newVar(int howmany)

Specified by:

newVar in interface ISolver

printStat

@Deprecated
public void printStat(PrintStream out,
                                 String prefix)

Deprecated.

Specified by:

printStat in interface ISolver

printStat

public void printStat(PrintWriter out,
                      String prefix)

Specified by:

printStat in interface ISolver

removeConstr

public boolean removeConstr(IConstr c)

Specified by:

removeConstr in interface ISolver

reset

public void reset()

Specified by:

reset in interface ISolver

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)

Specified by:

setExpectedNumberOfClauses in interface ISolver

setTimeout

public void setTimeout(int t)

Specified by:

setTimeout in interface ISolver

setTimeoutMs

public void setTimeoutMs(long t)

Specified by:

setTimeoutMs in interface ISolver

setTimeoutOnConflicts

public void setTimeoutOnConflicts(int count)

Specified by:

setTimeoutOnConflicts in interface ISolver

toString

public String toString(String prefix)

Specified by:

toString in interface ISolver

findModel

public int[] findModel()
                throws TimeoutException

Specified by:

findModel in interface IProblem

Throws:

TimeoutException

findModel

public int[] findModel(IVecInt assumps)
                throws TimeoutException

Specified by:

findModel in interface IProblem

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps,
                             boolean globalTimeout)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(boolean globalTimeout)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Throws:

TimeoutException

model

public int[] model()

Specified by:

model in interface IProblem

model

public boolean model(int var)

Specified by:

model in interface IProblem

nConstraints

public int nConstraints()

Specified by:

nConstraints in interface IProblem

nVars

public int nVars()

Specified by:

nVars in interface IProblem

printInfos

public void printInfos(PrintWriter out,
                       String prefix)

Specified by:

printInfos in interface IProblem

onFinishWithAnswer

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

isDBSimplificationAllowed

public boolean isDBSimplificationAllowed()

Specified by:

isDBSimplificationAllowed in interface ISolver

setDBSimplificationAllowed

public void setDBSimplificationAllowed(boolean status)

Specified by:

setDBSimplificationAllowed in interface ISolver

setSearchListener

public void setSearchListener(SearchListener sl)

Specified by:

setSearchListener in interface ISolver

getSearchListener

public SearchListener getSearchListener()

Specified by:

getSearchListener in interface ISolver

Since:

2.2

nextFreeVarId

public int nextFreeVarId(boolean reserve)

Specified by:

nextFreeVarId in interface ISolver

addBlockingClause

public IConstr addBlockingClause(IVecInt literals)
                          throws ContradictionException

Specified by:

addBlockingClause in interface ISolver

Throws:

ContradictionException

removeSubsumedConstr

public boolean removeSubsumedConstr(IConstr c)

Specified by:

removeSubsumedConstr in interface ISolver

isVerbose

public boolean isVerbose()

Specified by:

isVerbose in interface ISolver

setVerbose

public void setVerbose(boolean value)

Specified by:

setVerbose in interface ISolver

setLogPrefix

public void setLogPrefix(String prefix)

Specified by:

setLogPrefix in interface ISolver

getLogPrefix

public String getLogPrefix()

Specified by:

getLogPrefix in interface ISolver

unsatExplanation

public IVecInt unsatExplanation()

Specified by:

unsatExplanation in interface ISolver