DSpace-CRIS at TU Wienhttps://repositum.tuwien.atThe reposiTUm digital repository system captures, stores, indexes, preserves, and distributes digital research material.Sat, 26 Nov 2022 13:16:00 GMT2022-11-26T13:16:00Z5081The Parameterized Complexity of Reasoning Problems Beyond NPhttp://hdl.handle.net/20.500.12708/55807Title: The Parameterized Complexity of Reasoning Problems Beyond NP
Authors: de Haan, Ronald; Szeider, Stefan
Abstract: Today's propositional satisfiability (SAT) solvers are extremely powerful and can be used as an efficient back-end for solving NP-complete problems. However, many fundamental problems in knowledge representation and reasoning are located at the second level of the Polynomial Hierarchy or even higher, and hence polynomial-time transformations to SAT are not possible, unless the hierarchy collapses. Recent research shows that in certain cases one can break through these complexity barriers by fixed-parameter tractable (fpt) reductions which exploit structural aspects of problem instances in terms of problem parameters.
In this paper we develop a general theoretical framework that supports the classification of parameterized problems on whether they admit such an fpt-reduction to SAT or not. We instantiate our theory by classifying the complexities of several case study problems, with respect to various natural parameters. These case studies include the consistency problem for disjunctive answer set programming and a robust version of constraint satisfaction.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/558072014-01-01T00:00:00ZParameterized Complexity Results for Agenda Safety in Judgment Aggregationhttp://hdl.handle.net/20.500.12708/55806Title: Parameterized Complexity Results for Agenda Safety in Judgment Aggregation
Authors: Endriss, Ulle; de Haan, Ronald; Szeider, Stefan
Abstract: Many problems arising in computational social choice are of high computational complexity, and some are located at higher levels of the Polynomial Hierarchy. We argue that a parameterized complexity analysis provides a lot of insight about the factors contributing to the complexity of these problems, and can lead to practically useful algorithms. As a case study, we consider the problem of agenda safety in judgment aggregation, consider several natural parameters for this problem, and determine the parameterized complexity for each of these. Our analysis is aimed at obtaining fixed-parameter tractable (fpt) algorithms that use a small number of calls to a SAT solver. We hope that this work may initiate a structured parameterized complexity investigation of problems arising in the field of computational social choice that are located at higher levels of the Polynomial Hierarchy. A by-product of our case study is the development of complexity-theoretic techniques to provide lower bounds on the number of SAT calls needed by fpt-algorithms to solve certain problems.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/558062014-01-01T00:00:00ZSubexponential Time Complexity of CSP with Global Constraintshttp://hdl.handle.net/20.500.12708/55810Title: Subexponential Time Complexity of CSP with Global Constraints
Authors: Kanj, Iyad; de Haan, Ronald; Szeider, Stefan
Abstract: Not all NP-complete problems share the same practical hardness with respect to exact computation. Whereas some NP-complete problems are amenable to efficient computational methods, others are yet to show any such sign. It becomes a major challenge to develop a theoretical framework that is more fine-grained than the theory of NP-completeness, and that can explain the distinction between the exact complexities of various NP-complete problems. This distinction is highly relevant for constraint satisfaction problems under natural restrictions, where various shades of hardness can be observed in practice.
Acknowledging the NP-hardness of such problems, one has to look beyond polynomial time computation. The theory of subexponential time complexity provides such a framework, and has been enjoying increasing popularity in complexity theory. Recently, a first analysis of the subexponential time complexity of classical CSPs (where all constraints are given extensionally as tables) was given.
In this paper, we extend this analysis to CSPs in which constraints are given intensionally in the form of global constraints. In particular, we consider CSPs that use the fundamental global constraints AllDifferent, AtLeastNValue, AtMost- NValue, and constraints that are specified by compressed tuples (cTable). We provide tight characterizations of the subexponential time complexity of the aforementioned problems with respect to several natural structural parameters.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/558102014-01-01T00:00:00ZModel Checking Existential Logic on Partially Ordered Setshttp://hdl.handle.net/20.500.12708/55811Title: Model Checking Existential Logic on Partially Ordered Sets
Authors: Bova, Simone; Ganian, Robert; Szeider, Stefan
Abstract: We study the problem of checking whether an existential sentence
(that is, a first-order sentence in prefix form built using existential
quantifiers and all Boolean connectives) is true in a finite partially
ordered set (in short, a poset). A poset is a reflexive, antisymmetric,
and transitive digraph. The problem encompasses the fundamental
embedding problem of finding an isomorphic copy of a poset as an
induced substructure of another poset.
Model checking existential logic is already NP-hard on a fixed
poset; thus we investigate structural properties of posets yielding
conditions for fixed-parameter tractability when the problem is
parameterized by the sentence. We identify width as a central
structural property (the width of a poset is the maximum size of a
subset of pairwise incomparable elements); our main algorithmic
result is that model checking existential logic on classes of finite
posets of bounded width is fixed-parameter tractable. We observe a
similar phenomenon in classical complexity, where we prove that
the isomorphism problem is polynomial-time tractable on classes
of posets of bounded width; this settles an open problem in order
theory.
We surround our main algorithmic result with complexity results
on less restricted, natural neighboring classes of finite posets,
establishing its tightness in this sense. We also relate our work
with (and demonstrate its independence of) fundamental fixedparameter
tractability results for model checking on digraphs of
bounded degree and bounded clique-width.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/558112014-01-01T00:00:00ZQuantified Conjunctive Queries on Partially Ordered Setshttp://hdl.handle.net/20.500.12708/55812Title: Quantified Conjunctive Queries on Partially Ordered Sets
Authors: Bova, Simone; Ganian, Robert; Szeider, Stefan
Abstract: We study the computational problem of checking whether
a quantified conjunctive query (a first-order sentence built using only
conjunction as Boolean connective) is true in a finite poset (a reflexive,
antisymmetric, and transitive directed graph). We prove that the
problem is already NP-hard on a certain fixed poset, and investigate
structural properties of posets yielding fixed-parameter tractability when
the problem is parameterized by the query. Our main algorithmic result is
that model checking quantified conjunctive queries on posets of bounded
width is fixed-parameter tractable (the width of a poset is the maximum
size of a subset of pairwise incomparable elements). We complement our
algorithmic result by complexity results with respect to classes of finite
posets in a hierarchy of natural poset invariants, establishing its tightness
in this sense.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/558122014-01-01T00:00:00ZFixed-Parameter Tractable Reductions to SAThttp://hdl.handle.net/20.500.12708/55808Title: Fixed-Parameter Tractable Reductions to SAT
Authors: de Haan, Ronald; Szeider, Stefan
Abstract: Today's SAT solvers have an enormous importance and impact in many practical settings. They are used as efficient back-end to solve many NP-complete problems. However, many computational problems are located at the second level of the Polynomial Hierarchy or even higher, and hence polynomial-time transformations to SAT are not possible, unless the hierarchy collapses. In certain cases one can break through these complexity barriers by fixed-parameter tractable (fpt) reductions which exploit structural aspects of problem instances in terms of problem parameters. Recent research established a general theoretical framework that supports the classification of parameterized problems on whether they admit such an fpt-reduction to SAT or not. We use this framework to analyze some problems that are related to Boolean satisfiability. We consider several natural parameterizations of these problems, and we identify for which of these an fpt-reduction to SAT is possible. The problems that we look at are related to minimizing an implicant of a DNF formula, minimizing a DNF formula, and satisfiability of quantified Boolean formulas.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/558082014-01-01T00:00:00ZThe Complexity of Width Minimization for Existential Positive Querieshttp://hdl.handle.net/20.500.12708/55813Title: The Complexity of Width Minimization for Existential Positive Queries
Authors: Bova, Simone; Chen, Hubie
Abstract: Existential positive queries are logical sentences built from conjunction, disjunction, and existential quantification, and are also known as select-project-join-union queries in database theory, where they are recognized as a basic and fundamental class of queries. It is known that the number of variables needed to express an existential positive query is the crucial parameter determining the complexity of evaluating it on a database, and is hence a natural measure from the perspective of query optimization and rewriting. In this article, we study the complexity of the natural decision problem associated to this measure, which we call the expressibility problem: Given an existential positive query and a number k, can the query be expressed using k (or fewer) variables? We precisely determine the complexity of the expressibility problem, showing that it is complete for the level Pi^p_2 of the polynomial hierarchy. Moreover, we prove that the expressibility problem is undecidable in positive logic (that is, existential positive logic plus universal quantification), thus establishing existential positive logic as a maximal syntactic fragment where expressibility is decidable.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/558132014-01-01T00:00:00ZSmall Unsatisfiable Subsets in Constraint Satisfactionhttp://hdl.handle.net/20.500.12708/55734Title: Small Unsatisfiable Subsets in Constraint Satisfaction
Authors: Kanj, Iyad; de Haan, Ronald; Szeider, Stefan
Abstract: The problem of finding small unsatisfiable subsets of a set of constraints is important for various applications in computer science and artificial intelligence. We study the problem of identifying whether a given instance to the constraint satisfaction problem (CSP) has an unsatisfiable subset of size at most k from a parameterized complexity point of view. We show that the problem of finding small unsatisfiable subsets of a CSP instance is harder than the corresponding problem for CNF formulas. Moreover, we show that the problem is not fixed-parameter tractable when restricting the problem to any maximal tractable Boolean constraint language (for which the problem is nontrivial). We show that the problem is hard even when the maximum number of occurrences of any variable is bounded by a constant, a restriction which leads to fixed-parameter tractability for the case of CNF formulas. Finally, we relate the problem of finding small unsatisfiable subsets to the problem of identifying variable assignments that are enforced already by a small number of constraints (backbones), or that are ruled out already by a small number of constraints (anti-backbones).
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/20.500.12708/557342014-01-01T00:00:00Z