abstract

We investigate the computational complexity of the exact satisfiability problem (XSAT) restricted to certain subclasses of linear CNF formulas. These classes are defined through restricting the number of occurrences of variables and are therefore interesting because the complexity status does not follow from Schaefer's theorem [schaefer,tusa]. Specifically we prove that XSAT remains NP-complete for linear formulas which are monotone and all variables occur exactly l times. We also present some complexity results for exact linear formulas left open in [sofsem09]. Concretely, we show that XSAT for this class is NP-complete, in contrast to SAT or NSAT. This can be also established when clauses have length at least k, for fixed integer k ≥ 3. However, the XSAT-complexity for exact linear formulas with clause length exactly k remains open, but we provide its polynomial-time behaviour at least for every positive integer k ≤ 6.