On some SAT-variants over linear formulas

Abstract

We investigate the computational complexity of some prominent variants of the propositional satisfiability problem (SAT), namely not-all-equal SAT (NAE-SAT) and exact SAT (XSAT) restricted to the class of linear conjunctive normal form (CNF) formulas. Clauses of a linear formula pairwise have at most one variable in common. We prove that NAE-SAT and XSAT both remain NP-complete when restricted to linear formulas. Since the corresponding reduction is not valid when input formulas are not allowed to have 2-clauses, we also prove that NAESAT and XSAT still behave NP-complete on formulas only containing clauses of length at least k, for each fixed integer k = 3. Moreover, NP-completeness proofs for NAE-SAT and XSAT restricted to monotone linear formulas are presented. We also discuss the length restricted monotone linear formula classes regarding NP-completeness where a difficulty arises for NAE-SAT, when all clauses are k-uniform, for k = 4. Finally, we show that NAE-SAT is polynomial-time dec ble on exact linear formulas, where each pair of distinct clauses has exactly one variable in common. And, we give some hints regarding the complexity of XSAT on the exact linear class. © Springer-Verlag Berlin Heidelberg 2009.