XSAT and NAE-SAT of linear CNF classes

Porschen, Stefan and Schmidt, Tatjana and Speckenmeyer, Ewald and Wotzlaw, Andreas (2011) XSAT and NAE-SAT of linear CNF classes.
Published in: Discrete Applied Mathematics Vol. 167. pp. 1-14. ISSN 0166-218X


XSAT and NAE-SAT are important variants of the propositional satisfiability problem (SAT). Both are studied here regarding their computational complexity of linear CNF formulas. 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 investigation of both variants for several monotone linear subclasses that are parameterized by the size of clauses or by the number of occurrences of variables. In particular cases of these parameter values we are able to verify the NP-completeness of XSAT respectively 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. We verify the same assertion for NAE-SAT relying on some well-known result; whereas we obtain NP-completeness for XSAT of exact linear formulas. The case of uniform clause size k remains open for the latter problem. However, we can provide its polynomial-time behavior for k at most 6.

Download: [img] PDF - Preprinted Version
Download (364kB) | Preview
Editorial actions: View Item View Item (Login required)
Deposit Information:
ZAIK Number: zaik2011-632
Depositing User: Archive Admin
Date Deposited: 21 Oct 2011 12:32
Last Modified: 24 Nov 2015 12:11
URI: http://e-archive.informatik.uni-koeln.de/id/eprint/632