cross over gadget

3 SATを平面 3 SATにするためのガジェット

辺は端点に節を、もう一方の端点に変数を持つため、考慮すべき交点は1種類のみ。

https://scrapbox.io/files/649d8538f11dc8001c431b78.png

この青線が何を表すのかはよくわからない。変数の値の伝搬？

not を赤線で図示

https://scrapbox.io/files/649d87aaf24f86001b7642c3.png

この図自体は Wikipedia より

cross over gadget の構成・証明

赤黒線のある方の図に則って示す

1. $ a,b の組み合わせを $ \alpha,\beta,\gamma,\deltaで表す

$ \alpha\Leftrightarrow{a_2}\land{b_2}

$ \beta\Leftrightarrow{a_2}\land\lnot{b_1}

$ \gamma\Leftrightarrow\lnot{a_1}\land\lnot{b_1}

$ \delta\Leftrightarrow\lnot{a_1}\land{b_2}

2. $ \alpha,\beta,\gamma,\deltaのうち 1 つのみが必ず True になる

$ (\alpha\lor\beta\lor\gamma\lor\delta)

$ \lnot(\alpha\land\beta)

$ \lnot(\beta\land\gamma)

$ \lnot(\gamma\land\delta)

$ \lnot(\delta\land\alpha)

$ \lnot(\alpha\land\gamma)は上記の式のみから以下のように導けるので書かない

同様に$ \lnot(\beta\land\delta)も導けるので書かない

$ (\alpha,\gamma)=(\mathrm{True},\mathrm{True})とする

$ \alpha\Leftrightarrow{a_2}\land{b_2}から$ (a_1,b_1)=(\mathrm{False},\mathrm{False}) が導ける

$ \gamma\Leftrightarrow\lnot{a_1}\land\lnot{b_1}から$ (a_2,b_2)=(\mathrm{True},\mathrm{True}) が導ける

$ \beta\Leftrightarrow{a_2}\land\lnot{b_1}から$ \beta=\mathrm{True}が導ける

$ \lnot(\alpha\land\beta)が$ \mathrm{False}になるので式全体が$ \mathrm{False}になる。

よって、充足可能にするには$ \lnot(\alpha\land\gamma)を満たす必要がある

3. これらの式を CNF に起こす

$ (\alpha\lor\lnot{a_2}\lor\lnot{b_2})\land(\lnot\alpha\lor{a_2})\land(\lnot\alpha\lor{b_2})

$ (\beta\lor\lnot{a_2}\lor{b_1})\land(\lnot\beta\lor{a_2})\land(\lnot\beta\lor\lnot{b_1})

$ (\gamma\lor{a_1}\lor{b_1})\land(\lnot\gamma\lor\lnot{a_1})\land(\lnot\gamma\lor\lnot{b_1})

$ (\delta\lor{a_1}\lor\lnot{b_2})\land(\lnot\delta\lor\lnot{a_1})\land(\lnot\delta\lor{b_2})

$ (\alpha\lor\beta\lor\lnot\xi)\land(\xi\lor\gamma\lor\delta)

$ (\lnot\alpha\lor\lnot\beta)\land(\lnot\beta\lor\lnot\gamma)

$ (\lnot\gamma\lor\lnot\delta)\land(\lnot\delta\lor\lnot\alpha)

3SATの節と変数の関係をグリッド上に表現できるため、交点を cross over gadget で置き換える

https://scrapbox.io/files/649d860b76feef001ce9bd03.png

1-in-3 SAT バージョン

https://gyazo.com/42c5fa23fe99997072e31f9ae6aae49b

https://gyazo.com/33f230f62bc14e5faf5a81560e677c5e