public abstract class SATSolveSingle
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
protected static class |
SATSolveSingle.Edge |
protected static class |
SATSolveSingle.Node |
protected static class |
SATSolveSingle.Var |
Modifier and Type | Field and Description |
---|---|
protected int |
countNodes |
protected CutFinderIMinInfo |
info |
protected java.util.Map<org.deckfour.xes.classification.XEventClass,SATSolveSingle.Node> |
node2var |
protected org.deckfour.xes.classification.XEventClass[] |
nodes |
protected org.sat4j.pb.IPBSolver |
solver |
protected java.util.Map<java.lang.Integer,SATSolveSingle.Var> |
varInt2var |
Constructor and Description |
---|
SATSolveSingle(CutFinderIMinInfo info) |
Modifier and Type | Method and Description |
---|---|
protected void |
addClause(int... ints) |
protected Pair<java.util.Set<org.deckfour.xes.classification.XEventClass>,java.util.Set<org.deckfour.xes.classification.XEventClass>> |
compute() |
protected void |
debug(java.lang.String x) |
protected SATSolveSingle.Edge |
newEdgeVar(org.deckfour.xes.classification.XEventClass a,
org.deckfour.xes.classification.XEventClass b) |
protected SATSolveSingle.Node |
newNodeVar(org.deckfour.xes.classification.XEventClass a) |
abstract SATResult |
solveSingle(int cutSize,
double bestAverageTillNow) |
protected java.util.Map<java.lang.Integer,SATSolveSingle.Var> varInt2var
protected org.sat4j.pb.IPBSolver solver
protected java.util.Map<org.deckfour.xes.classification.XEventClass,SATSolveSingle.Node> node2var
protected org.deckfour.xes.classification.XEventClass[] nodes
protected int countNodes
protected final CutFinderIMinInfo info
public SATSolveSingle(CutFinderIMinInfo info)
public abstract SATResult solveSingle(int cutSize, double bestAverageTillNow)
protected Pair<java.util.Set<org.deckfour.xes.classification.XEventClass>,java.util.Set<org.deckfour.xes.classification.XEventClass>> compute() throws org.sat4j.specs.TimeoutException
org.sat4j.specs.TimeoutException
protected SATSolveSingle.Edge newEdgeVar(org.deckfour.xes.classification.XEventClass a, org.deckfour.xes.classification.XEventClass b)
protected SATSolveSingle.Node newNodeVar(org.deckfour.xes.classification.XEventClass a)
protected void debug(java.lang.String x)
protected void addClause(int... ints) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.ContradictionException