Arrow Research search

Author name cluster

Christoph Haase

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.

15 papers
2 author rows

Possible papers

15

SODA Conference 2024 Conference Paper

Integer Programming with GCD Constraints

  • Rémy Défossez
  • Christoph Haase
  • Alessio Mansutti
  • Guillermo A. Pérez

We study the non-linear extension of integer programming with greatest common divisor constraints of the form gcd( f, g) ~ d, where f and g are linear polynomials, d is a positive integer, and ~ is a relation among ≤, = ≠, = and ≥. We show that the feasibility problem for these systems is in NP, and that an optimal solution minimizing a linear objective function, if it exists, has polynomial bit length. To show these results, we identify an expressive fragment of the existential theory of the integers with addition and divisibility that admits solutions of polynomial bit length. It was shown by Lipshitz [Trans. Am. Math. Soc. , 235, pp. 271-283, 1978] that this theory adheres to a local-to-global principle in the following sense: a formula Φ is equi-satisfiable with a formula Ψ in this theory such that Ψ has a solution if and only if Ψ has a solution modulo every prime p. We show that in our fragment, only a polynomial number of primes of polynomial bit length need to be considered, and that the solutions modulo prime numbers can be combined to yield a solution to Φ of polynomial bit length. As a technical by-product, we establish a Chinese-remainder-type theorem for systems of congruences and non-congruences showing that solution sizes do not depend on the magnitude of the moduli of non-congruences.

KR Conference 2023 Conference Paper

Computing All Facts Entailed By An LTL Specification

  • Przemysław Andrzej Wałęga
  • Michał Zawidzki
  • Christoph Haase

We study the problem of efficiently computing all (usually infinitely many) facts which are entailed by a specification written in linear temporal logic (LTL)-a standard formalism for specifying and verifying properties of computations in reactive systems. This problem can be seen as a generalisation of the standard entailment checking, but whose output provides a much wider understanding of the system’s behaviour. We show that in full LTL the problem can be solved in doubly exponential time, whereas for Horn fragments of LTL, which can be seen as temporal logic programs, the problem can be solved in exponential or only quadratic time, depending on the allowed temporal operators in the input formula. Moreover, we show that all these bounds are optimal. We also implement and experimentally compare two techniques for solving the problem: an automata-based algorithm for full LTL and a materialisation-based algorithm for Horn fragments. The obtained results suggest practical usefulness of our approach.

MFCS Conference 2023 Conference Paper

On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)

  • Christoph Haase
  • Alessio Mansutti
  • Amaury Pouly

This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1-31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time.

MFCS Conference 2022 Conference Paper

Higher-Order Quantified Boolean Satisfiability

  • Dmitry Chistikov 0001
  • Christoph Haase
  • Zahra Hadizadeh
  • Alessio Mansutti

The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXP. While, in theory, iterating this approach yields complete problems for k-NEXP for all k > 0, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds. The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higher-order Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k, d), k ≥ 0, d ≥ 1, in which variables are interpreted as Boolean functions of order at most k and there are d quantifier alternations between functions of order exactly k. We show that the unbounded HOSAT problem is TOWER-complete, and that HOSAT(k, d) is complete for the weak k-EXP hierarchy with d alternations for fixed k, d ≥ 1 and d odd. We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic.

Highlights Conference 2021 Conference Abstract

A guided tour through Presburger arithmetic and friends, Part I

  • Christoph Haase

The goal of this tutorial is to give a comprehensive overview over Presburger arithmetic, the first-order theory of the natural numbers with addition and order. To this end, I will present some classical and very recent results that representatively illustrate the many facets of Presburger arithmetic. I will also offer to the audience some concrete technical tools that come in handy when working on lower-level aspects of Presburger arithmetic. The tutorial will consist of three one-hour parts. Part one is concerned with the decidability of Presburger arithmetic, which can be shown by appealing to three algorithmic frameworks: quantifier elimination, generator-based methods and automata-based methods. Each of these frameworks comes with their own advantages and disadvantages, e. g. for showing complexity results or the decidability of extensions of Presburger arithmetic. Besides establishing some complexity results, I will illustrate how choosing the right framework enables one to smoothly show decidability of extensions of Presburger arithmetic with counting quantifiers, Kleene star and restricted divisibility predicates.

Highlights Conference 2021 Conference Abstract

A guided tour through Presburger arithmetic and friends, Part II

  • Christoph Haase

In the second part, I will focus on lower bounds for Presburger arithmetic and some of its extensions. I will review classical constructions such as the Fischer-Rabin trick and also give some of the main ideas underlying a recent breakthrough showing the intractability of so-called short formulas of Presburger arithmetic.

Highlights Conference 2021 Conference Abstract

A guided tour through Presburger arithmetic and friends, Part III

  • Christoph Haase

The third part of the tutorial will see a discussion of the decidability proof of existential Presburger arithmetic extended with full divisibility predicates as well as counting solutions of formulas of parametric Presburger arithmetic. Time permitting, I will discuss concrete applications of those extensions in model theory, automata theory and compiler optimisation.

MFCS Conference 2021 Conference Paper

On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes

  • Christoph Haase
  • Alessio Mansutti

Given an existential formula Φ of linear arithmetic over p-adic integers together with valuation constraints, we study the p-universality problem which consists of deciding whether Φ is satisfiable for all primes p, and the analogous problem for the closely related existential theory of Büchi arithmetic. Our main result is a coNEXP upper bound for both problems, together with a matching lower bound for existential Büchi arithmetic. On a technical level, our results are obtained from analysing properties of a certain class of p-automata, finite-state automata whose languages encode sets of tuples of natural numbers.

TCS Journal 2018 Journal Article

Context-free commutative grammars with integer counters and resets

  • Dmitry Chistikov
  • Christoph Haase
  • Simon Halfon

We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this class of commutative grammars enjoys semi-linear reachability sets. We also show that the inclusion problem is, in general, coNEXP-complete and already Π 2 P -complete for grammars with only one non-terminal symbol. Showing the lower bound for the latter result requires us to develop a novel Π 2 P -complete variant of the classic subset sum problem.

MFCS Conference 2017 Conference Paper

Counting Problems for Parikh Images

  • Christoph Haase
  • Stefan Kiefer
  • Markus Lohrey

Given finite-state automata (or context-free grammars) A, B over the same alphabet and a Parikh vector p, we study the complexity of deciding whether the number of words in the language of A with Parikh image p is greater than the number of such words in the language of B. Recently, this problem turned out to be tightly related to the cost problem for weighted Markov chains. We classify the complexity according to whether A and B are deterministic, the size of the alphabet, and the encoding of p (binary or unary).

Highlights Conference 2017 Conference Abstract

On the complexity of quantified integer programming

  • Dmitry Chistikov
  • Christoph Haase

Quantified integer programming is the the problem of deciding assertions of the form "Q x_k … forall x_2 exists x_1: A x geq c" where vectors of variables x_k, …, x_1 form the vector x, all variables are interpreted over N (alternatively, over Z), and A and c are a matrix and vector over Z of appropriate sizes. We show that quantified integer programming with alternation depth k is complete for the k-th level of the polynomial hierarchy. Abstract available in PDF.

Highlights Conference 2016 Conference Abstract

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

  • with Stefan Göller
  • Christoph Haase
  • Ranko Lazic

I propose to present recent and ongoing work on Branching Vector Addition System (BVASS), that extend Vector Addition Systems with special branching transitions like in tree automata. When performing a branching step, the counter values are distributed non-deterministically between two successor processes. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. Our recent result is that the reachability, coverability and boundedness problems are polynomial-time complete for BVASS in dimension one. Regarding the reachability problem, this is the first decidability result in a subclass of BVASS known so far. This is joint work with Stefan G\”oller, Christoph Haase and Ranko Lazi\’c, to be published at ICALP’16 under the same name and also available here: http: //arxiv. org/abs/1602. 05547

Highlights Conference 2014 Conference Abstract

Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy

  • Christoph Haase

I will show that for any fixed i > 0, validity in Presburger arithmetic with i + 1 quantifier alternations beginning with an existential quantifier is complete for the i -th level of the weak EXP hierarchy, an analogue to the polynomial-time hierarchy residing between NEXP and EXPSPACE.

MFCS Conference 2013 Conference Paper

Reachability in Register Machines with Polynomial Updates

  • Alain Finkel
  • Stefan Göller
  • Christoph Haase

Abstract This paper introduces a class of register machines whose registers can be updated by polynomial functions when a transition is taken, and the domain of the registers can be constrained by linear constraints. This model strictly generalises a variety of known formalisms such as various classes of Vector Addition Systems with States. Our main result is that reachability in our class is PSPACE -complete when restricted to one register. We moreover give a classification of the complexity of reachability according to the type of polynomials allowed and the geometry induced by the range-constraining formula.

ECAI Conference 2008 Conference Paper

Complexity of Subsumption in the [Escr ][Lscr ] Family of Description Logics: Acyclic and Cyclic TBoxes

  • Christoph Haase
  • Carsten Lutz

We perform an exhaustive study of the complexity of subsumption in the ℰ ℒ family of lightweight description logics w. r. t. acyclic and cyclic TBoxes. It turns out that there are interesting members of this family for which subsumption w. r. t. cyclic TBoxes is tractable, whereas it is EXPTIME-complete w. r. t. general TBoxes. For other extensions that are intractable w. r. t. general TBoxes, we establish intractability already for acyclic and cyclic TBoxes.

v2026.09.13