XSAT and NAE-SAT of linear CNF classes
XSAT and NAE-SAT of linear CNF classes
复制标题
DOI：
10.1016/j.dam.2013.10.030
复制
发表时间：
2014-04
期刊：
影响因子：
--
通讯作者：
Stefan Porschen;Tatjana Schmidt;Ewald Speckenmeyer;Andreas Wotzlaw
中科院分区：
文献类型：
--
作者：
Stefan Porschen;Tatjana Schmidt;Ewald Speckenmeyer;Andreas Wotzlaw
摘要XSAT和NAE-SAT是命题可满足性问题（SAT）的重要变种。XSAT包含所有CNF公式，可以通过将每个子句中的一个文字设置为1来满足，而NAE-SAT需要满足真值赋值，而不是在任何子句中将所有文字设置为相等。这两种变体在这里研究了线性CNF公式的计算复杂性，其子句允许最多有一个共同的变量。我们证明了这两个变种保持NP-完全的（单调）线性公式，得出的结论是，也双色的线性超图是NP-完全的。减少使用引起的复杂性调查的几个单调的线性子类的变量，参数化条款的大小，或变量的出现次数。对于这些参数的特定值，我们能够显示NP-完全的XSAT和NAE-SAT，虽然我们不能提供一个完整的治疗。最后，我们专注于精确的线性公式，其中条款相交成对，SAT是已知的多项式时间可解。在这里，我们证明了NP-完全的XSAT的精确线性公式。如果此外的条款需要统一的长度，我们表明，XSAT和NAE-SAT是可判定的多项式时间，什至持有他们的计数版本。
Abstract XSAT and NAE-SAT are important variants of the propositional satisfiability problem (SAT). XSAT contains all CNF formulas that can be satisfied by setting exactly one literal in each clause to 1, whereas NAE-SAT requires satisfying truth assignments not setting all literals equally in any clause. Both variants are studied here regarding their computational complexity of linear CNF formulas, whose clauses are allowed to have at most one variable in common. We prove that both variants remain NP-complete for (monotone) linear formulas, yielding the conclusion that also bicolorability of linear hypergraphs is NP-complete. The reduction used gives rise to the complexity investigations of several monotone linear subclasses of both variants that are parameterized by the size of clauses, or by the number of occurrences of variables. For particular values of those parameters, we are able to show the NP-completeness of XSAT and NAE-SAT, though we cannot provide a complete treatment. Finally, we focus on exact linear formulas, where clauses intersect pairwise, and for which SAT is known to be polynomial-time solvable. Here, we prove NP-completeness of XSAT for exact linear formulas. If in addition the clauses are required to be of uniform length, we show that both XSAT and NAE-SAT are decidable in polynomial time, what even holds for their counting versions.