Author name cluster

Ewald Speckenmeyer

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.

13 papers

1 author row

SAT Conference 2011 Conference Paper

A Satisfiability-Based Approach for Embedding Generalized Tanglegrams on Level Graphs

Ewald Speckenmeyer
Andreas Wotzlaw
Stefan Porschen

Abstract A tanglegram is a pair of trees on the same set of leaves with matching leaves in the two trees joined by an edge. Tanglegrams are widely used in computational biology to compare evolutionary histories of species. In this paper we present a formulation of two related combinatorial embedding problems concerning tanglegrams in terms of CNF-formulas. The first problem is known as planar embedding and the second as crossing minimization problem. We show that our satisfiability formulation of these problems can handle a much more general case with more than two, not necessarily binary or complete, trees defined on arbitrary sets of leaves and allowed to vary their layouts.

Details

SAT Conference 2010 Conference Paper

Complexity Results for Linear XSAT-Problems

Stefan Porschen
Tatjana Schmidt
Ewald Speckenmeyer

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 [14, 7]. 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 [9]. Concretely, we show that XSAT for this class is NP-complete, in contrast to SAT or NAE-SAT. This can also be 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.

Details

SAT Conference 2009 Conference Paper

On Some Aspects of Mixed Horn Formulas

Stefan Porschen
Tatjana Schmidt
Ewald Speckenmeyer

Abstract We consider various aspects of the Mixed Horn formula class (MHF). A formula F ∈ MHF consists of a 2-CNF part P and a Horn part H. We propose that MHF has a central relevance in CNF, because many prominent NP-complete problems, e. g. Feedback Vertex Set, Vertex Cover, Dominating Set and Hitting Set can easily be encoded as MHF. Furthermore we show that SAT for some interesting subclasses of MHF remains NP-complete. Finally we provide algorithms for two of these subclasses solving SAT in a better running time than \(O(2^{0. 5284n})=O((\sqrt[3]{3})^n)\) which is the best bound for MHF so far, over n variables. One of these subclasses consists of formulas, where the Horn part is negative monotone and the variable graph corresponding to the positive 2-CNF part P consists of disjoint triangles only. For this class we provide an algorithm and present the running times for the k -uniform cases, where k ∈ {3, 4, 5, 6}. Regarding the other subclass consisting of certain k -uniform linear mixed Horn formulas, we provide an algorithm solving SAT in time \(O((\sqrt[k]{k})^n)\), for k ≥ 4.

Details

SAT Conference 2008 Conference Paper

A CNF Class Generalizing Exact Linear Formulas

Stefan Porschen
Ewald Speckenmeyer

Abstract The fibre view on clause sets, previously introduced in [12], is used in the present paper to define and investigate subclasses of CNF that appear to be polynomial time solvable w. r. t. SAT. The most interesting of these classes is a generalization of exact linear formulas, namely formulas such that each pair of distinct clauses has all variables in common or exactly one. By definition, in an exact linear formula each pair of distinct clauses has exactly one variable in common. SAT-solving for exact linear formulas was shown to be easy in [14]. Here we provide an algorithm solving the decision and counting variants of SAT for the generalized class in polynomial time. Moreover we study some other structurally defined formula classes on the basis of the fibre view. We show that these classes have the property that their members all are satisfiable or all are unsatisfiable.

Details

SAT Conference 2007 Conference Paper

Algorithms for Variable-Weighted 2-SAT and Dual Problems

Stefan Porschen
Ewald Speckenmeyer

Abstract In this paper we study NP-hard variable-weighted satisfiability optimization problems for the class 2-CNF providing worst-case upper time bounds holding for arbitrary real-valued weights. Moreover, we consider the monotone dual class consisting of clause sets where all variables occur at most twice. We show that weighted SAT, XSAT and NAESAT optimization problems for this class are polynomial time solvable using appropriate reductions to specific polynomial time solvable graph problems.

Details

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 2004 Conference Paper

Worst Case Bounds for some NP-Complete Modified Horn-SAT Problems

Stefan Porschen
Ewald Speckenmeyer

We consider the satisfiability problem for CNF instances that contain a (hidden) Horn and a 2-CNF part, called mixed formulas. We show that SAT remains NP-complete for such instances and also that any SAT instance can be encoded in terms of a mixed formula in polynomial time. Further, we provide an exact deterministic algorithm showing that SAT for mixed formulas is solvable in time O(20.5284n ). Motivating for these investigations are level graph formulas which are mixed Horn formulas.

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

CSL Conference 1992 Conference Paper

Some Aspects of the Probabilistic Behavior of Variants of Resolution

Peter Heusch
Ewald Speckenmeyer

Abstract The SAT-Problem fot boolean formulas in conjunctive normal form often arises in the area of artificial intelligence, its solution is known as mechanical theorem proving. Most mechanical theorem provers perform this by using a variant of the resolution principle. The time and space complexity of resolution strongly depends on the class of formulas. Horn formulas, where each clause may contain at most one positive literal, represent the most important class where resolution proofs with polynomial length exist. A special sort of Horn formulas, where each clause contains exactly one positive literal, is called logic programs. In logic programs, clauses of length one are also known as facts, clauses of length greater than one are known as rules. We show that there are typically short resolution proofs under unit/Davis-Putnam resolution for some models of formulas, and we study the “density” of rules necessary in another model for deriving the empty clause with probability tending to one.

Details

CSL Conference 1990 Conference Paper

On the Average Time Complexity of Set Partitioning

Ewald Speckenmeyer
Rainer Kemp

Abstract The average running time of backtracking for solving the set-partitioning problem under two probability models, the constant set size model and the constant occurence model, will be studied. Results separating classes of instances with an exponential from such with a polynomial running time in the average will be shown.

Details

CSL Conference 1989 Conference Paper

Is Average Superlinear Speedup Possible?

Ewald Speckenmeyer

Abstract A mathematical model for analysing the speedup behaviour of a parallel k processor backtracking algorithm compared with sequential backtracking is studied. The essential parameter of a problem class, which is incorporated in the model, is the distribution of solutions in the corresponding backtracking trees. Under the model assumptions it is shown that in case of sufficiently unbalanced distributions superlinear speedups will occur in the average. Further a result is shown, indicating that in case of restricted classes of CNF-formulas unbalanced distributions of solutions actually occur.

Details

MFCS Conference 1988 Conference Paper

Classes of CNF-Formulas with Backtracking Trees of Exponential or Linear Average Order for Exact-Satisfiability

Ewald Speckenmeyer

Abstract We analyse the average case behaviour of a simple backtracking algorithm for determining all exact-satisfying truth assignments of CNF-formulas over n variables with r clauses of length s. A truth assignment exact-satisfies a formula, if in every clause exactly one literal is set to true. 1. For the class of formulas given by the parameters n, r, and s a formula computable in polynomial time is derived, by which the average number of nodes in backtracking trees can be determined under the uniform instance distribution. 2. In case where all clauses have length s =3, it is shown that the average number of nodes in backtracking trees is growing exponentially in n, if r =0( n ), and it is at most n, if r ≥ 37/40 n 2.

Details

CSL Conference 1988 Conference Paper

On the Average Case Complexity of Backtracking for the Exact-Satisfiability Problem

Ewald Speckenmeyer

Abstract We analyse the average case performance of a simple backtracking algorithm for determining all exact-satisfying truth assignments of boolean formulas in conjunctive normal form with r clauses over n variables. A truth assignment exact-satisfies a formula, if in each clause exactly one literal is set to true. We show: If formulas are chosen by generating clauses independently, where each variable occurs in a clause either unnegated with probability p or negated with probability q or none of both with probability 1-p-q (p, q>0, p+q≦1), then the average number of nodes in the backtracking trees of formulas from these classes is bounded by a constant, for all nεN, if r≧1n2/(pq) is chosen. (In case of p=q=1/3 the result holds for all r≧6.)

Details