SATクイズ?: FをCNF、Cを節、xをリテラルとして、 x∈Cかつ任意の(¬x)∈D∈FであるようなDについてF⊨C∪(D∖(¬x))であるとき、 Fが充足可能ならばF∪{C}もそうであることを示せ。

出典: https://arxiv.org/abs/1605.00723