Search Results

Documents authored by Mansutti, Alessio

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.132
Integer Linear-Exponential Programming in NP by Quantifier Elimination

Authors: Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms 2^x and remainder terms (x mod 2^y). Our result implies that the existential theory of the structure (ℕ,0,1,+,2^(⋅),V_2(⋅,⋅), ≤) has an NP-complete satisfiability problem, thus improving upon a recent EXPSPACE upper bound. This theory extends the existential fragment of Presburger arithmetic with the exponentiation function x ↦ 2^x and the binary predicate V_2(x,y) that is true whenever y ≥ 1 is the largest power of 2 dividing x. Our procedure for solving linear-exponential systems uses the method of quantifier elimination. As a by-product, we modify the classical Gaussian variable elimination into a non-deterministic polynomial-time procedure for integer linear programming (or: existential Presburger arithmetic).
Cite as

Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak. Integer Linear-Exponential Programming in NP by Quantifier Elimination. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 132:1-132:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2024.132,
  author =	{Chistikov, Dmitry and Mansutti, Alessio and Starchak, Mikhail R.},
  title =	{{Integer Linear-Exponential Programming in NP by Quantifier Elimination}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{132:1--132:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.132},
  URN =		{urn:nbn:de:0030-drops-202758},
  doi =		{10.4230/LIPIcs.ICALP.2024.132},
  annote =	{Keywords: decision procedures, integer programming, quantifier elimination}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.52
On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)

Authors: Christoph Haase, Alessio Mansutti, and Amaury Pouly

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
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.
Cite as

Christoph Haase, Alessio Mansutti, and Amaury Pouly. On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.MFCS.2023.52,
  author =	{Haase, Christoph and Mansutti, Alessio and Pouly, Amaury},
  title =	{{On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{52:1--52:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.52},
  URN =		{urn:nbn:de:0030-drops-185869},
  doi =		{10.4230/LIPIcs.MFCS.2023.52},
  annote =	{Keywords: first-order theories, arithmetic theories, fixed-parameter tractability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.112
The Complexity of Presburger Arithmetic with Power or Powers

Authors: Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We investigate expansions of Presburger arithmetic (Pa), i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function that takes a number to the power of 2, or a predicate 2^ℕ for the powers of 2. The latter theory, denoted Pa(2^ℕ(·)), was introduced by Büchi as a first attempt at characterizing the sets of tuples of numbers that can be expressed using finite automata; Büchi’s method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as Pa(λx.2^|x|), was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by Büchi, Semenov’s method is also non-elementary. And in fact, the theory with the power function has a non-elementary lower bound. In this paper, we show that while Semenov’s and Büchi’s approaches yield non-elementary blow-ups for Pa(2^ℕ(·)), the theory is in fact decidable in triply exponential time, similarly to the best known quantifier-elimination algorithm for Pa. We also provide a NExpTime upper bound for the existential fragment of Pa(λx.2^|x|), a step towards a finer-grained analysis of its complexity. Both these results are established by analyzing a single parameterized satisfiability algorithm for Pa(λx.2^|x|), which can be specialized to either the setting of Pa(2^ℕ(·)) or the existential theory of Pa(λx.2^|x|). Besides the new upper bounds for the existential theory of Pa(λx.2^|x|) and Pa(2^ℕ(·)), we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.
Cite as

Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The Complexity of Presburger Arithmetic with Power or Powers. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 112:1-112:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICALP.2023.112,
  author =	{Benedikt, Michael and Chistikov, Dmitry and Mansutti, Alessio},
  title =	{{The Complexity of Presburger Arithmetic with Power or Powers}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{112:1--112:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.112},
  URN =		{urn:nbn:de:0030-drops-181641},
  doi =		{10.4230/LIPIcs.ICALP.2023.112},
  annote =	{Keywords: arithmetic theories, exponentiation, decision procedures}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.33
Higher-Order Quantified Boolean Satisfiability

Authors: Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
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.
Cite as

Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti. Higher-Order Quantified Boolean Satisfiability. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.MFCS.2022.33,
  author =	{Chistikov, Dmitry and Haase, Christoph and Hadizadeh, Zahra and Mansutti, Alessio},
  title =	{{Higher-Order Quantified Boolean Satisfiability}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.33},
  URN =		{urn:nbn:de:0030-drops-168313},
  doi =		{10.4230/LIPIcs.MFCS.2022.33},
  annote =	{Keywords: Boolean satisfiability problem, higher-order Boolean functions, weak k-EXP hierarchies, non-elementary complexity, Presburger arithmetic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.55
On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes

Authors: Christoph Haase and Alessio Mansutti

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
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.
Cite as

Christoph Haase and Alessio Mansutti. On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 55:1-55:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.MFCS.2021.55,
  author =	{Haase, Christoph and Mansutti, Alessio},
  title =	{{On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{55:1--55:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.55},
  URN =		{urn:nbn:de:0030-drops-144953},
  doi =		{10.4230/LIPIcs.MFCS.2021.55},
  annote =	{Keywords: linear arithmetic, B\"{u}chi arithmetic, p-adic numbers, automatic structures}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.19
Internal Calculi for Separation Logics

Authors: Stéphane Demri, Etienne Lozes, and Alessio Mansutti

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic SL(∗, -*). We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem.
Cite as

Stéphane Demri, Etienne Lozes, and Alessio Mansutti. Internal Calculi for Separation Logics. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{demri_et_al:LIPIcs.CSL.2020.19,
  author =	{Demri, St\'{e}phane and Lozes, Etienne and Mansutti, Alessio},
  title =	{{Internal Calculi for Separation Logics}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.19},
  URN =		{urn:nbn:de:0030-drops-116625},
  doi =		{10.4230/LIPIcs.CSL.2020.19},
  annote =	{Keywords: Separation logic, internal calculus, adjunct/quantifier elimination}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.42
Extending Propositional Separation Logic for Robustness Properties

Authors: Alessio Mansutti

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.
Cite as

Alessio Mansutti. Extending Propositional Separation Logic for Robustness Properties. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{mansutti:LIPIcs.FSTTCS.2018.42,
  author =	{Mansutti, Alessio},
  title =	{{Extending Propositional Separation Logic for Robustness Properties}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{42:1--42:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.42},
  URN =		{urn:nbn:de:0030-drops-99418},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.42},
  annote =	{Keywords: Separation logic, decision problems, reachability, logics on trees, interval temporal logic, adjuncts and quantifiers elimination}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact