ImplicationGraph

Undocumented in source.

struct ImplicationGraph {

alias Node = Tuple!(Literal, "literal", size_t, "dlevel");

Set!Node nodes;

Set!Node[Node] successors;

Set!Node[Node] predecessors;

Clause.ID[Node][Node] edges;

Literal[] decisionLiterals;

void initalize();

this(ImplicationGraph graph);

void removeLevel(size_t dlevel);

Node getNode(Literal lit);

Set!Node get1UIPCut();

void transformToConflictGraph(size_t level);

}

Constructors

this this(ImplicationGraph graph): 与えられた implication graph を deep copy するためのコンストラクタ

Members

Aliases

Node alias Node = Tuple!(Literal, "literal", size_t, "dlevel"): dlevel とは、decision level のことをさす。

Functions

get1UIPCut Set!Node get1UIPCut(): 1UIP cut を取得します。
getNode Node getNode(Literal lit): 与えられたリテラルを持つ頂点を取得します。
initalize void initalize(): Undocumented in source. Be warned that the author may not have intended to support it.
removeLevel void removeLevel(size_t dlevel): 与えられた decision level 以上の頂点やそれに繋がっている辺を削除します。
transformToConflictGraph void transformToConflictGraph(size_t level): implication graph を conflict graph の制約を満たすように変形します。この関数呼出後のグラフは以下の制約のすべてを満たしていることが保証されています。

Variables

decisionLiterals Literal[] decisionLiterals;: Undocumented in source.
edges Clause.ID[Node][Node] edges;: Undocumented in source.
nodes Set!Node nodes;: Undocumented in source.
predecessors Set!Node[Node] predecessors;: Undocumented in source.
successors Set!Node[Node] successors;: Undocumented in source.

Meta

Source

See Implementation

satd solvers cdcl aliases

CDCLSolverResult

classes

CDCLSolver

structs

ImplicationGraph

variables

LAMBDA