1-in-k周六的完整分辨率规则

Question

在CNF SAT中，每个条款（A或B或C或...）必须至少包含一个真正的文字。解决方案规则适用于那些完全一对相反文字的条款。

（a或b或c）和（！a或d或e）=>（b或c或d或e）

我说，这条规则是完整的，从某种意义上说：如果公式不可或缺，我可以通过详尽地应用规则（在硬实例上，指数倍数），直到产生一个空子子句。如果公式具有唯一的解决方案，则可以应用规则，直到生成每个单位子句。

1-in-k sat是一个np-complety variant，每个子句（a，b，c，....）= 1的恰好一个变量是真的。给出了一对具有对面文字的条款，没有共同的文字，我也可以产生第三个：

（a，b，c）= 1和（！a，d，e）= 1=>（b，c，d，e）= 1

问题：这条规则是否完全用于不可履行且唯一可满足的1-in-kformulas？

Answer 1

您正在处理分辨率，好像它是纯粹的语法规则。它与传统的CNF子句有那种方式，因为这与推理的底层规则相对应。但是，CNF子句具有额外的一个文字的额外限制不再对应于可以有效地应用的分辨率规则。

boolean表达式 $（a \ lor b）\ land（\ lnot {a} \ lor \ lnot {b}）\ land（\ lnot {a} \ lor b）$ 与 1-in-k-sat 公式不挑离，但天真地应用分辨率规则生成 $ a= false，b= true$ 作为（错误）解决方案。