Linear Time Algorithms for Some Not-All-Equal Satisfiability Problems

Abstract In this paper we consider the problem Not-All-Equal satisfiability (NAESAT) for propositional formulas in conjunctive normal form (CNF). It asks whether there is a (satisfying) model for the input formula in no clause assigning truth value 1 to all its literals. NAESAT is NP-complete in general as well as restricted to formulas with either only negated or unnegated variables. After having pointed out that SAT and NAESAT in the unrestricted case are equivalent from the point of view of computational complexity, we propose linear time algorithms deciding NAESAT for restricted classes of CNF formulas. First we show that a NAESAT model (if existing) can be computed in linear time for formulas in which each variable occurs at most twice. Moreover we prove that this computation is in NC and hence can also be solved in parallel efficiently. Secondly, we show that NAESAT can be decided in linear time for monotone formulas in which each clause has length exactly k and each variable occurs exactly k times. Hence, bicolorability of k -uniform, k -regular hypergraphs is decidable in linear time.

Authors

• Stefan Porschen
• Bert Randerath
• Ewald Speckenmeyer

Keywords

No keywords are indexed for this paper.