ブール回路理論における演算
ツェイチン 変換 (別名 ツェイチン変換)は、任意の 組み合わせ論理 回路を入力として受け取り 、 等充足可能な ブール式を 連言正規形 (CNF) で生成します。式の長さは回路のサイズに比例します。回路出力を「真」にする入力ベクトルは、式を満たす 割り当てと 1 対 1 で対応しています。これにより、任意の回路 (任意の式を含む) の 回路充足可能性 の問題が、3-CNF 式の 充足可能性の問題に簡略化されます。これは、ロシアの科学者 グリゴリー・ツェイチン によって発見されました 。
モチベーション 単純なアプローチでは、回路をブール式として記述し、 ド・モルガンの法則 と 分配法則 を使用してCNF に変換します。ただし、これにより方程式のサイズが指数関数的に増加する可能性があります。Tseytin 変換は、入力回路のサイズに対して線形に増加する数式を出力します。
アプローチ 出力方程式は、定数 1 を式に等しく設定したものです。この式はサブ式の結合であり、各サブ式が満たされると、入力回路内の 1 つのゲートが適切に動作することが保証されます。したがって、出力式全体が満たされると、入力回路全体が適切に動作することが保証されます。
各ゲートには、その出力を表す新しい変数が導入されます。入力と出力を関連付ける小さな事前計算済みの CNF 式が (「and」演算を介して) 出力式に追加されます。これらのゲートへの入力は、元のリテラルまたはサブゲートの出力を表す導入された変数のいずれかになることに注意してください。
出力式には入力よりも多くの変数が含まれますが、それでも等 充足可能 であり、元の入力方程式が充足可能な場合にのみ充足可能となります。変数の充足可能な割り当てが見つかった場合、導入された変数の割り当ては単純に破棄できます。
最終節には、最終ゲートの出力変数という単一のリテラルが追加されます。このリテラルが補完されると、この節が満たされると出力式が false に強制され、そうでない場合は式が true に強制されます。
例 次の式を考えてみましょう 。
ϕ
{\displaystyle \phi}
ϕ := （ （ p ∨ q ） ∧ r ） → （ ¬ s ）
{\displaystyle \phi :=((p\lor q)\land r)\to (\neg s)}
すべてのサブ式を考慮します（単純な変数を除く）。
¬ s
p ∨ q
（ p ∨ q ） ∧ r
（ （ p ∨ q ） ∧ r ） → （ ¬ s ）
{\displaystyle {\begin{aligned}&\neg s\\&p\lor q\\&(p\lor q)\land r\\&((p\lor q)\land r)\to (\neg s)\end{整列}}}
各サブ数式に新しい変数を導入します。
x
1
↔ ¬ s
x
2
↔ p ∨ q
x
3
↔
x
2
∧ r
x
4
↔
x
3
→
x
1
{\displaystyle {\begin{aligned}x_{1}&\leftrightarrow \neg s\\x_{2}&\leftrightarrow p\lor q\\x_{3}&\leftrightarrow x_{2}\land r\\x_{4}&\leftrightarrow x_{3}\to x_{1}\end{aligned}}}
すべての置換と の置換を結合します 。
ϕ
{\displaystyle \phi}
T （ ϕ ） :=
x
4
∧ （
x
4
↔
x
3
→
x
1
） ∧ （
x
3
↔
x
2
∧ r ） ∧ （
x
2
↔ p ∨ q ） ∧ （
x
1
↔ ¬ s ）
{\displaystyle T(\phi ):=x_{4}\land (x_{4}\leftrightarrow x_{3}\to x_{1})\land (x_{3}\leftrightarrow x_{2}\land r)\land (x_{2}\leftrightarrow p\lor q)\land (x_{1}\leftrightarrow \neg s)}
すべての置換はCNFに変換できます。例：
x
2
↔ p ∨ q
≡ （
x
2
→ （ p ∨ q ） ） ∧ （ （ p ∨ q ） →
x
2
）
≡ （ ¬
x
2
∨ p ∨ q ） ∧ （ ¬ （ p ∨ q ） ∨
x
2
）
≡ （ ¬
x
2
∨ p ∨ q ） ∧ （ （ ¬ p ∧ ¬ q ） ∨
x
2
）
≡ （ ¬
x
2
∨ p ∨ q ） ∧ （ ¬ p ∨
x
2
） ∧ （ ¬ q ∨
x
2
）
{\displaystyle {\begin{aligned}x_{2}\leftrightarrow p\lor q&\equiv (x_{2}\to (p\lor q))\land ((p\lor q)\to x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg (p\lor q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land ((\neg p\land \neg q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg p\lor x_{2})\land (\neg q\lor x_{2})\end{aligned}}}
ゲートサブ式 さまざまなロジック ゲートに対して作成できる可能性のあるサブ式の一部を示します。演算式では、C は出力として機能します。CNF サブ式では、C は新しいブール変数として機能します。各演算では、CNF サブ式は、C がすべての可能な入力値に対するブール演算の契約に準拠している場合にのみ true になります。
シンプルな組み合わせロジック 次の回路は、少なくとも入力の一部が true の場合に true を返しますが、一度に 2 つを超える入力が true になることはありません。この回路は、方程式 y = x1 · x2 + x1 · x2 + x2 · x3 を実装します。ゲートの出力ごとに変数が導入され、それぞれが赤でマークされています。
x 2 を入力とするインバータの出力には、2 つの変数が導入されていることに注意してください。これは冗長ですが、結果の式の等充足可能性には影響しません。次に、各ゲートを適切な CNF サブ式に置き換えます。
最終的な出力変数は gate8 なので、この回路の出力が真であることを強制するために、最後の単純な節 (gate8) が追加されます。これらの式を組み合わせると、SAT の最終的なインスタンスは次のようになります。
(ゲート1 ∨ x1) ∧ ( ゲート1 ∨ x1 ) ∧ ( ゲート2 ∨ ゲート1) ∧ ( ゲート2 ∨ x2) ∧ ( x2 ∨ ゲート 2 ∨ ゲート 1 ) ∧ (ゲート 3 ∨ x2) ∧ ( ゲート 3 ∨ x2 ) ∧ ( ゲート 4 ∨ x1) ∧ ( ゲート 4 ∨ ゲート 3) ∧ (ゲート 3 ∨ ゲート 4 ∨ x1 ) ∧ (ゲート 5 ∨ x2) ∧ ( ゲート5 ∨ x2 ) ∧ ( ゲート6 ∨ ゲート5) ∧ ( ゲート6 ∨ x3) ∧ ( x3 ∨ ゲート 6 ∨ ゲート 5 ) ∧ (ゲート 7 ∨ ゲート 2 ) ∧ (ゲート 7 ∨ ゲート 4 ) ∧ (ゲート2 ∨ ゲート7 ∨ ゲート4) ∧ (ゲート8 ∨ ゲート6 ) ∧ (ゲート8 ∨ ゲート7 ) ∧ (ゲート6 ∨ ゲート8 ∨ ゲート7) ∧ (ゲート8) = 1 これらの変数の適切な割り当ての例は次のようになります。
導入された変数の値は通常は破棄されますが、元の回路のロジック パスをトレースするために使用できます。ここでは、 確かに元の回路が true を出力するための基準を満たしています。別の答えを見つけるには、節 (x1 ∨ x2 ∨ x3 ) を追加して、SAT ソルバーを再度実行します。
（ x 1 、 x 2 、 x 3 ） = （ 0 、 0 、 1 ）
{\displaystyle (x1,x2,x3)=(0,0,1)}
導出 選択されたゲートに対する CNF サブ式の 1 つの可能な導出を示します。
ORゲート 2 つの入力A と B と 1 つの出力 C を持つ OR ゲートは、 次の条件を満たします。
出力 Cが真であれば、その入力 A または B の少なくとも1つは 真である。 出力 C が偽の場合、その入力 A と B は 両方とも偽になります。 これら 2 つの条件は、次の 2 つの意味の結合として表現できます。
（ Ｃ → （ あ ∨ B ） ） ∧ （
Ｃ ¯
→ （
あ ¯
∧
B ¯
） ）
{\displaystyle (C\rightarrow (A\vee B))\wedge ({\overline {C}}\rightarrow ({\overline {A}}\wedge {\overline {B}}))}
含意を、接続詞、選言、否定のみを含む同等の表現に置き換えると、次の式が得られます。
（
Ｃ ¯
∨ （ あ ∨ B ） ） ∧ （ Ｃ ∨ （
あ ¯
∧
B ¯
） ） 、
{\displaystyle ({\overline {C}}\vee (A\vee B))\wedge (C\vee ({\overline {A}}\wedge {\overline {B}})),}
これはすでにほぼ 連言標準形 になっている。右端の節を2回分配すると、
（
Ｃ ¯
∨ あ ∨ B ） ∧ （ （ Ｃ ∨
あ ¯
） ∧ （ Ｃ ∨
B ¯
） ） 、
{\displaystyle ({\overline {C}}\vee A\vee B)\wedge ((C\vee {\overline {A}})\wedge (C\vee {\overline {B}})),}
そして、連言の結合性を適用すると、CNF式が得られる。
（
Ｃ ¯
∨ あ ∨ B ） ∧ （ Ｃ ∨
あ ¯
） ∧ （ Ｃ ∨
B ¯
）
{\displaystyle ({\overline {C}}\vee A\vee B)\wedge (C\vee {\overline {A}})\wedge (C\vee {\overline {B}})}
NOTゲート NOT ゲートは、入力と出力が互いに反対の場合に正常に動作しています。つまり、
出力Cが真の場合、入力Aは偽である 出力Cが偽の場合、入力Aは真である これらの条件を満たす必要がある式として表します。
（ Ｃ →
あ ¯
） ∧ （
Ｃ ¯
→ あ ）
{\displaystyle (C\rightarrow {\overline {A}})\wedge ({\overline {C}}\rightarrow A)}
、
(
C
¯
∨
A
¯
)
∧
(
C
∨
A
)
{\displaystyle ({\overline {C}}\vee {\overline {A}})\wedge (C\vee A)}
NORゲート NOR ゲートは、次の条件が満たされている場合に正常に動作しています。
出力Cが真であれば、AもBも真ではない 出力Cが偽の場合、少なくともAとBのどちらかが真である これらの条件を満たす必要がある式として表します。
(
C
→
(
A
∨
B
)
¯
)
∧
(
C
¯
→
(
A
∨
B
)
)
{\displaystyle (C\rightarrow {\overline {(A\vee B)}})\wedge ({\overline {C}}\rightarrow (A\vee B))}
、、、、、
(
C
¯
∨
(
A
¯
∧
B
¯
)
)
¯
¯
∧
(
C
∨
A
∨
B
)
)
{\displaystyle {\overline {\overline {({\overline {C}}\vee ({\overline {A}}\wedge {\overline {B}}))}}}\wedge (C\vee A\vee B))}
(
C
∧
(
A
∨
B
)
)
¯
∧
(
C
∨
A
∨
B
)
)
{\displaystyle {\overline {(C\wedge (A\vee B))}}\wedge (C\vee A\vee B))}
(
A
∧
C
)
∨
(
B
∧
C
)
¯
∧
(
C
∨
A
∨
B
)
)
{\displaystyle {\overline {(A\wedge C)\vee (B\wedge C)}}\wedge (C\vee A\vee B))}
(
A
¯
∨
C
¯
)
∧
(
B
¯
∨
C
¯
)
∧
(
C
∨
A
∨
B
)
)
{\displaystyle ({\overline {A}}\vee {\overline {C}})\wedge ({\overline {B}}\vee {\overline {C}})\wedge (C\vee A\vee B))}
参考文献 GS Tseytin : 命題計算における導出の複雑さについて。Slisenko, AO (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics, pp. 115–125. Steklov Mathematical Institute (1970)。ロシア語からの翻訳: Zapiski Nauchnykh Seminarov LOMI 8 (1968)、pp. 234–259。 GS Tseytin: 命題計算における導出の複雑さについて。1966 年 9 月に開催されたレニングラード数理論理学セミナーで発表。 
