org.sat4j.multicore
Class ManyCore

java.lang.Object
  extended by 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


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