org.sat4j.multicore
Class ManyCore

java.lang.Object
  org.sat4j.multicore.ManyCore

All Implemented Interfaces:

java.io.Serializable, IProblem, ISolver

public class ManyCore
extends java.lang.Object
implements ISolver

See Also:

Serialized Form

Constructor Summary

ManyCore(ASolverFactory<? extends ISolver> factory, java.lang.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)
java.util.Map<java.lang.String,java.lang.Number>	getStat()
int	getTimeout()
long	getTimeoutMs()
boolean	isDBSimplificationAllowed()
boolean	isSatisfiable()
boolean	isSatisfiable(boolean globalTimeout)
boolean	isSatisfiable(IVecInt assumps)
boolean	isSatisfiable(IVecInt assumps, boolean globalTimeout)
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(java.io.PrintWriter out, java.lang.String prefix)
void	printStat(java.io.PrintStream out, java.lang.String prefix) Deprecated.
void	printStat(java.io.PrintWriter out, java.lang.String prefix)
boolean	removeConstr(IConstr c)
boolean	removeSubsumedConstr(IConstr c)
void	reset()
void	setDBSimplificationAllowed(boolean status)
void	setExpectedNumberOfClauses(int nb)
void	setSearchListener(SearchListener sl)
void	setTimeout(int t)
void	setTimeoutMs(long t)
void	setTimeoutOnConflicts(int count)
java.lang.String	toString(java.lang.String prefix)

Methods inherited from class java.lang.Object

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

Constructor Detail

ManyCore

public ManyCore(ASolverFactory<? extends ISolver> factory,
                java.lang.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 java.util.Map<java.lang.String,java.lang.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(java.io.PrintStream out,
                                 java.lang.String prefix)

Deprecated.

Specified by:

printStat in interface ISolver

printStat

public void printStat(java.io.PrintWriter out,
                      java.lang.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 java.lang.String toString(java.lang.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(java.io.PrintWriter out,
                       java.lang.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

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