- Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer:
The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments.
Electronic Notes in Theoretical Computer Science, 2008 (to appear).
To appear.
Show abstract
In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal
Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators
used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This
paper systematically studies the model-checking problem for LTL formulae over restricted sets of propositional
and temporal operators. For almost all combinations of temporal and propositional operators, we
determine whether the model-checking problem is tractable (in P) or intractable (NP-hard). We then focus
on the tractable cases, showing that they all are NL-complete or even logspace solvable. This leads to a
surprising gap in complexity between tractable and intractable cases. It is worth noting that our analysis
covers an infinite set of problems, since there are infinitely many sets of propositional operators.
- Eric Brelsford, Piotr Faliszewski, Edith Hemaspaandra, Henning Schnoor, Ilka Schnoor:
Approximability of Manipulating Elections.
In Proceedings of AAAI Conference on Artificial Intelligence, pp. 44-49.
AAAI Press,
2008.
Show abstract
In this paper, we set up a framework to study approximation of manipulation, control, and bribery in elections. We show existence of approximation algorithms (even fully polynomial time approximation schemes) as well as obtain inapproximability results.
- Nadia Creignou, Henning Schnoor, Ilka Schnoor:
Non-uniform Boolean Constraint Satisfaction Problems with Cardinality Constraint.
In Proceedings of Computer Science Logic, Volume 5213 of Lecture Notes in Computer Science, pp. 109-123.
Springer,
2008.
Show abstract
We study the computational complexity of Boolean constraint satisfaction problems with cardinality constraint. A Galois connection between clones and co-clones has received a lot of attention in the context of complexity considerations for constraint satisfaction problems. This connection fails when considering constraint satisfaction problems that support in addition a cardinality constraint. We prove that a similar Galois connection, involving a weaker closure operator and partial polymorphisms, can be applied to such problems. Thus, we establish dichotomies for the decision as well as for the counting problems in Schaefer’s framework.
- Henning Schnoor, Ilka Schnoor:
Partial Polymorphisms and Constraint Satisfaction Problems.
In Complexity of Constraints, Volume 5250 of Lecture Notes in Computer Science, pp. 229-254.
Springer,
2008.
Show abstract
The Galois connection between clones and and co-clones has
received a lot of attention in the context of complexity considerations for
constraint satisfaction problems. However, it fails if we are interested in
a reduction giving equivalence instead of only satisfiability-equivalence.
We show how a similar Galois connection involving weaker closure operators
can be applied for these problems. As an example of the usefulness
of our construction, we show how to obtain very short proofs of complexity
classifications in this context.
- Michael Elberfeld, Ilka Schnoor, Till Tantau:
Influence of Tree Topology Restrictions on the Complexity of Haplotyping with Missing Data.
Technical report SIIM-TR-A-08-05,
Schriftenreihe der Institute für Informatik/Mathematik der Universität zu Lübeck,
2008.
Show PDF | Show abstract
Haplotyping, also known as haplotype phase prediction, is the
problem of predicting likely haplotypes based on genotype data. One
fast haplotyping method is based on an evolutionary model where a
<i>perfect phylogenetic tree</i> is sought that explains the
observed data. Unfortunately, when data entries are missing, as is
often the case in real laboratory data, the resulting formal problem
IPPH, which stands for incomplete perfect phylogeny
haplotyping, is NP-complete and no theoretical results are known
concerning its approximability, fixed-parameter tractability or
exact algorithms for it. Even radically simplified versions, such as
the restriction to phylogenetic trees consisting of just two directed
paths from a given root, are still NP-complete, but here, at least,
a fixed-parameter algorithm is known. We generalize this algorithm
to arbitrary tree topologies and present the first
theoretical analysis of an algorithm that works on arbitrary
instances of the original IPPH problem. At the same time we
also show that restricting the tree topology does not always make
finding phylogenies easier: while the incomplete directed perfect phylogeny
problem is well-known to be solvable in polynomial time, we show
that the same problem restricted to path topologies is NP-complete.
- Michael Bauland, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer:
The Complexity of Generalized Satisfiability for Linear Temporal Logic.
In Proceedings of FOSSACS, Volume 4423 of Lecture Notes in Computer Science, pp. 46-62.
Springer,
2007.
Show abstract
In a seminal paper from 1985, Sistla and Clarke showed that
satis?ability for Linear Temporal Logic (LTL) is either NP-complete or
PSPACE-complete, depending on the set of temporal operators used. If,
in contrast, the set of propositional operators is restricted, the complexity
may decrease. This paper undertakes a systematic study of satis?ability for LTL formulae over restricted sets of propositional and temporal
operators. Since every propositional operator corresponds to a Boolean
function, there exist in?nitely many propositional operators. In order to
systematically cover all possible sets of them, we use Post’s lattice. With
its help, we determine the computational complexity of LTL satis?ability for all combinations of temporal operators and all but two classes of
propositional functions. Each of these in?nitely many problems is shown
to be either PSPACE-complete, NP-complete, or in P.
- Phillipe Chapdelaine,, Miki Hermann, Ilka Schnoor:
Complexity of Default Logic on Generalized Conjunctive Queries.
In Proceedings of LPNMR, Volume 4483 of Lecture Notes in Artificial Intelligence, pp. 58-70.
Springer,
2007.
Show abstract
Reiter’s default logic formalizes nonmonotonic reasoning using default assumptions. The semantics of a given instance of default logic is based
on a ?xpoint equation de?ning an extension. Three different reasoning problems
arise in the context of default logic, namely the existence of an extension, the
presence of a given formula in an extension, and the occurrence of a formula in
all extensions. Since the end of 1980s, several complexity results have been pub-
lished concerning these default reasoning problems for different syntactic classes
of formulas. We derive in this paper a complete classi?cation of default logic rea-
soning problems by means of universal algebra tools using Post’s clone lattice. In
particular we prove a trichotomy theorem for the existence of an extension, clas-
sifying this problem to be either polynomial, NP-complete, or ?2 P-complete,
depending on the set of underlying Boolean connectives. We also prove similar
trichotomy theorems for the two other algorithmic problems in connection with
default logic reasoning.
- Henning Schnoor, Ilka Schnoor:
Enumerating All Solutions for Constraint Satisfaction Problems.
In Proceedings of STACS, Volume 4393 of Lecture Notes in Computer Science, pp. 694-705.
Springer,
2007.
Show abstract
We examine the problem to enumerate, for a given constraint
formula, its set of satisfying assignments. We prove that the tools known
from the Boolean case do not su?ce in general, and provide a template
for a new class of algorithms. For the three-element case, we achieve a
?rst step towards a dichotomy theorem for the enumeration problem.