含意グラフ

数学論理学とグラフ理論において、含意グラフは、頂点集合Vと有向辺集合Eで構成される歪対称の有向グラフ G = ( V , E )です。 V内の各頂点はブールリテラルの真理値を表し、頂点uから頂点vへの各有向辺は「リテラルuが真であればリテラルvも真である」という物質的含意を表します。 含意グラフは、もともと複雑なブール式を分析するために使用されていました。

連言正規形の2 満足可能性インスタンスは、その選言のそれぞれを 1 組の含意に置き換えることによって、含意グラフに変換できます。たとえば、ステートメントは のペアとして書き直すことができます。インスタンスが満足可能であるのは、リテラルとその否定が、その含意グラフの同じ強連結成分に属していない場合のみです。この特徴付けは、2 満足可能性インスタンスを線形時間で解決するために使用できます。^[1]${\displaystyle (x_{0}\lor x_{1})}$${\displaystyle (\neg x_{0}\rightarrow x_{1}),(\neg x_{1}\rightarrow x_{0})}$

CDCL SATソルバーでは、単位伝播は、決定リテラルからすべての暗黙のリテラルを導出するすべての可能な方法をキャプチャする含意グラフと自然に関連付けられ、^[2]それが節学習に使用されます。