implication graph を conflict graph の制約を満たすように変形します。 この関数呼出後のグラフは以下の制約のすべてを満たしていることが保証されています。
1. Λ とただ一つの conflict variable を含んでいる。 2. 任意の頂点について、Λ への道が存在する。 3. Λ を除くすべての頂点 l について、それが decision literal であるか、または (l_1 or l_2 or ... or l_k or l) が既知の節として存在して、かつ not l_1, not l_2, ..., not l_k が predecessor としてグラフに存在する。
See Implementation
implication graph を conflict graph の制約を満たすように変形します。 この関数呼出後のグラフは以下の制約のすべてを満たしていることが保証されています。
1. Λ とただ一つの conflict variable を含んでいる。 2. 任意の頂点について、Λ への道が存在する。 3. Λ を除くすべての頂点 l について、それが decision literal であるか、または (l_1 or l_2 or ... or l_k or l) が既知の節として存在して、かつ not l_1, not l_2, ..., not l_k が predecessor としてグラフに存在する。