TRUEを利用した UnSAT
from SAT の色んなガジェット
TRUEガジェットを利用した UnSAT
TRUEガジェットの図の赤い変数が同じ節に存在してしまうため
? このガジェットは大きすぎる。もっと小さい UnSAT は無いか
大きすぎるのも問題だが、TRUEガジェットを利用して$ =に帰着して UnSAT 判定ができるので解析上の旨味がない
とりあえず、こうすれば UnSAT は作れますよという程度の例
https://scrapbox.io/files/649f84b64e1fc4001cc174e2.png
正平面2上界1-in-3 SAT版
上の図とはちょっと違う構造
https://gyazo.com/e700d6028621bc4035cd10eb55fef2e7