algorithm - この特別なCNFは何と呼ばれていますか？

Question

の式がCNFで与えられているブール充足可能性のインスタンスがあるとします。さらに、各句には正のリテラルまたは負のリテラルのみが含まれます。例えば：

(a || b) && (!a || !c || !d) && (b || d)

そのようなブール式には特別な名前がありますか？標準のCNF式と比較して、このタイプの式で充足可能性をテストするためのより速い方法はありますか？

Answer 1

すべての節が肯定的または否定的であるような CNF のクラス、つまり、同時に肯定的なリテラルと否定的なリテラルを含む節が存在しないような CNF のクラスは、たとえば Hans Kleine Buening の命題論理に関する著書で「モノトーン CNF」と呼ばれています。 . 単調な CNF に関する最近の論文は https://arxiv.org/abs/1603.07881です。 「単調な 3-Sat-4 は NP-完全です」標準的な手法で単調な 3-SAT を確認することは難しくありません (すべての句はいずれかです正または負、すべての句の長さは (最大で) 3) NP 完全であり、上記の論文では、すべての変数が最大 4 回発生する場合の NP 完全性を示すことで、これを改良しています。

Answer 2

これは、ブール充足可能性問題または単に SAT と呼ばれます。特殊な場合には多項式解が存在しますが ( 2SATを参照)、一般的な問題は NP 完全です (つまり、いわゆる高速解は存在しません)。