分割による解像度保護圧縮

数理論理学において、分割による証明圧縮は、分解証明の後処理として動作するアルゴリズムである。これは、スコット・コットンが論文「分解証明を最小化するための2つの手法」で提案したものである。^{[ 1 ]}

分割アルゴリズムは、以下の観察に基づいています。

充足不能性の証明が与えられた場合${\displaystyle \pi }$そして変数${\displaystyle x}$証明を再構成（分割）するのは簡単です。${\displaystyle x}$そして証明${\displaystyle \neg x}$そして、これら2つの証明を（追加の分解ステップによって）組み合わせることで、元の証明よりも小さな証明が得られる可能性がある。

証明で分割を適用することに注意${\displaystyle \pi }$変数を使用する${\displaystyle x}$異なる変数を使用したアルゴリズムの後続の適用を無効にするものではない${\displaystyle y}$^{実際、コットン[ 1 ]}が提案した方法は、一連の証明を生成する。$\displaystyle \pi _{1}\pi _{2}\ldots }$それぞれの証明$\displaystyle \pi _{i+1}}$は、分割を適用した結果です。$\displaystyle \pi _{i}}$数列の構築中に、証明が$\displaystyle \pi _{j}}$たまたま大きすぎる、$\displaystyle \pi _{j+1}}$は、${\displaystyle \{\pi _{1},\pi _{2},\ldots ,\pi _{j}\}}$。

圧縮/時間比を向上させるには、変数選択のヒューリスティックが望ましい。この目的のために、Cotton ^{[ 1 ] は}、解決ステップの「加算性」（前件あり）を定義している。${\displaystyle p}$そして${\displaystyle n}$そして、レゾルベント${\displaystyle r}$):

${\displaystyle \operatorname {add} (r):=\max(|r|-\max(|p|,|n|),0)}$

次に、各変数について${\displaystyle v}$、スコアは、すべての解決ステップの加算性を合計して計算されます。${\displaystyle \pi }$ピボット付き${\displaystyle v}$これらの解決ステップの数とともに。このようにして計算された各スコアを次のように表します。${\displaystyle add(v,\pi )}$各変数は、そのスコアに比例した確率で選択される。

${\displaystyle p(v)={\frac {\operatorname {add} (v,\pi _{i})}{\sum _{x}{\operatorname {add} (x,\pi _{i})}}}}$

不充足性の証明を分割する${\displaystyle \pi }$証明において$\displaystyle \pi _{x}}$の${\displaystyle x}$そして証明$\displaystyle \pi _{\neg x}}$の${\displaystyle \neg x}$コットン^{[ 1 ]}は次のように提案している。

させて${\displaystyle l}$リテラルと${\displaystyle p\oplus _{x}n}$節の解決項を表す${\displaystyle p}$そして${\displaystyle n}$どこ${\displaystyle x\in p}$そして${\displaystyle \neg x\in n}$次に、マップを定義します。$\displaystyle \pi _{l}}$解決DAGのノードで${\displaystyle \pi }$:

${\displaystyle \pi _{l}(c):={\begin{cases}c,&{\text{cが入力の場合}}\\\pi _{l}(p),&{\text{c=p\oplus _{x}nかつ}}(l=xまたは}}x\notin \pi _{l}(p))\\\pi _{l}(n),&{\text{c=p\oplus _{x}nかつ}}(l=\neg xまたは}}\neg x\notin \pi _{l}(n))\\\pi _{l}(p)\oplus _{x}\pi _{l}(p),&{\text{x\in \pi _{l}(p)かつ}}\neg x\in \pi _{l}(n)\end{cases}}}$

また、${\displaystyle o}$空節である${\displaystyle \pi }$。 それから、$\displaystyle \pi _{x}}$そして$\displaystyle \pi _{\neg x}}$計算によって得られる${\displaystyle \pi _{x}(o)}$そして${\displaystyle \pi _{\neg x}(o)}$、 それぞれ。