
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 NAE-SAT 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 decidable 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.
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 3 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
