Package org.processmining.plugins.InductiveMiner.mining.cuts.IMc.solve.single

Class SATSolveSingle

java.lang.Object

org.processmining.plugins.InductiveMiner.mining.cuts.IMc.solve.single.SATSolveSingle

Direct Known Subclasses:

SATSolveSingleLoop, SATSolveSingleParallel, SATSolveSingleSequence, SATSolveSingleXor

public abstract class SATSolveSingle
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
protected static class	SATSolveSingle.Edge
protected static class	SATSolveSingle.Node
protected static class	SATSolveSingle.Var

Field Summary

Fields

Modifier and Type	Field	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 Summary

Constructors

Constructor	Description
SATSolveSingle(CutFinderIMinInfo info)

Method Summary

Modifier and Type	Method	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)

Methods inherited from class java.lang.Object

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

Field Detail

varInt2var

protected java.util.Map<java.lang.Integer,SATSolveSingle.Var> varInt2var

solver

protected org.sat4j.pb.IPBSolver solver

node2var

protected java.util.Map<org.deckfour.xes.classification.XEventClass,SATSolveSingle.Node> node2var

nodes

protected org.deckfour.xes.classification.XEventClass[] nodes

countNodes

protected int countNodes

info

protected final CutFinderIMinInfo info

Constructor Detail

SATSolveSingle

public SATSolveSingle(CutFinderIMinInfo info)

Method Detail

solveSingle

public abstract SATResult solveSingle(int cutSize,
                                      double bestAverageTillNow)

compute

protected Pair<java.util.Set<org.deckfour.xes.classification.XEventClass>,java.util.Set<org.deckfour.xes.classification.XEventClass>> compute()
                                                                                                                                             throws org.sat4j.specs.TimeoutException

Throws:

org.sat4j.specs.TimeoutException

newEdgeVar

protected SATSolveSingle.Edge newEdgeVar(org.deckfour.xes.classification.XEventClass a,
                                         org.deckfour.xes.classification.XEventClass b)

newNodeVar

protected SATSolveSingle.Node newNodeVar(org.deckfour.xes.classification.XEventClass a)

debug

protected void debug(java.lang.String x)

addClause

protected void addClause(int... ints)
                  throws org.sat4j.specs.ContradictionException

Throws:

org.sat4j.specs.ContradictionException