Arrow Research search

Author name cluster

Bert Randerath

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers
2 author rows

Possible papers

5

SAT Conference 2006 Conference Paper

On Linear CNF Formulas

  • Stefan Porschen
  • Ewald Speckenmeyer
  • Bert Randerath

Abstract In the present paper we introduce the class of linear CNF formulas generalizing the notion of linear hypergraphs. Clauses of a linear formula intersect in at most one variable. We show that SAT for the general class of linear formulas remains NP-complete. Moreover we show that the subclass of exactly linear formulas is always satisfiable. We further consider the class of uniform linear formulas and investigate conditions for the formula graph to be complete. We define a formula hierarchy such that one can construct a 3-uniform linear formula belonging to the i th level such that the clause-variable density is of Ω(2. 5 i − − 1 ) ∩ O (3. 2 i − − 1 ). Finally, we introduce the subclasses LCNF ≥ k of linear formulas having only clauses of length at least k, and show that SAT remains NP-complete for LCNF ≥ 3.

Details

SAT Conference 2003 Conference Paper

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

  • Stefan Porschen
  • Bert Randerath
  • Ewald Speckenmeyer

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.

Details