arXiv subjects

Alessio Mansutti

Publications and source records attributed to Alessio Mansutti.

At least 19 recordsLinked to original sources

arXiv2026

Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis

Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate representation between syntax and classical denotational semantics, which treats programs as operators. Abstract compilation is then understood as the act of abstracting such operators. We develop higher-order abstract domains for functions, operators, and programs themselves, in which composition is the key novel primitive, together with a categorical framework for constructing sound, precise, and modular abstract compilers. We instantiate this framework in the context of recurrence-based static cost analysis, developing solver-independent, optimal recurrence extraction techniques for recursive programs over algebraic data types, that support general function unknowns and catamorphic metrics, a broad class of size metrics beyond traditional approaches.

cs.PL↗

arXiv2026

Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners

We present the theory underpinning a complexity analysis tool (under development) that aims at automating tedious parts of the analysis of complex algorithms originating from the field of automated reasoning. Examples are given by super-exponential quantifier elimination procedures in real and integer arithmetics. Our tool implements the following pipeline. * Together with the algorithm to be analysed, the user (expert, e.g. the algorithm designer) can provide key metrics to track, and lemmas to improve the analysis. In pen-and-paper proofs, these correspond to the "non-tedious" and "creative" parts of the complexity analysis, that require human ingenuity. * The second step consists in the extraction of (generalised) recurrence equations. Here, we rely on a novel higher-order abstract interpretation technique, built on the concept of operator semantics. It enables (optimal) abstract compilation of symbolic programs to different kinds of purely numerical recursive representations, such as recurrence equations on interval-valued functions or numerical logic programs. * Finally, our tool solves the recurrence equations. We propose to go beyond the direct usage of computer algebra systems (CAS), and use pre/postfixpoint-based techniques to discover and verify candidate bounds on the solution. This approach makes use, in turn, of recent progress in SMT solvers, and can also be improved by techniques originating in termination analysis research.

cs.LO↗

arXiv2026

How (and when) can you fit examples to logic-based hypothesis classes over infinite structures?

We study fitting problems, sometimes called ``training problems'', where we have a finite sample consisting of inputs and outputs, and we want to know whether there is a function in a certain class that could produce these outputs, exactly or approximately, on the given inputs. We focus on the computational and descriptive complexity of fitting for logically-defined classes in common decidable structures, like the real ordered field and Presburger arithmetic, and also for broader classes defined via combinatorial or model-theoretic properties. We isolate the complexity of these fitting problems, with particular attention to cases where we can use queries in a natural query language over the sample to determine whether a sample is fittable.

cs.LO↗

arXiv2026

MCSAT Modulo Transcendental Arithmetics

We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and trigonometric ones. The framework extends the Model Constructive Satisfiability calculus (MCSAT), and leverages procedures for NRA and methods from real analysis. At its core, our procedure abstracts the input formula to NRA, and lets MCSAT and an NRA plugin incrementally build a partial model of the abstracted formula. A Transcendental Real Arithmetic plugin, acting as an intermediary between MCSAT and the NRA plugin, ensures the consistency of the partial model and is responsible for refining the abstracted formula. We implemented our procedure in the Yices2 SMT solver for the sine and exponential functions, and conducted an extensive empirical evaluation that shows that our prototype outperforms state-of-the-art solvers on both SAT and UNSAT instances.

cs.LO↗

arXiv2025

Optimization Modulo Integer Linear-Exponential Programs

This paper presents the first study of the complexity of the optimization problem for integer linear-exponential programs which extend classical integer linear programs with the exponential function $x \mapsto 2^x$ and the remainder function ${(x,y) \mapsto (x \bmod 2^y)}$. The problem of deciding if such a program has a solution was recently shown to be NP-complete in [Chistikov et al., ICALP'24]. The optimization problem instead asks for a solution that maximizes (or minimizes) a linear-exponential objective function, subject to the constraints of an integer linear-exponential program. We establish the following results: 1. If an optimal solution exists, then one of them can be succinctly represented as an integer linear-exponential straight-line program (ILESLP): an arithmetic circuit whose gates always output an integer value (by construction) and implement the operations of addition, exponentiation, and multiplication by rational numbers. 2. There is an algorithm that runs in polynomial time, given access to an integer factoring oracle, which determines whether an ILESLP encodes a solution to an integer linear-exponential program. This algorithm can also be used to compare the values taken by the objective function on two given solutions. Building on these results, we place the optimization problem for integer linear-exponential programs within an extension of the optimization class $\text{NPO}$ that lies within $\text{FNP}^{\text{NP}}$. In essence, this extension forgoes determining the optimal solution via binary search.

cs.LO↗

arXiv2025

One-Parametric Presburger Arithmetic has Quantifier Elimination

We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function $x \mapsto t \cdot x$, where $t$ is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al., Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions $x \mapsto \lfloor{\frac{x}{f(t)}}\rfloor$, one for each integer polynomial $f$. Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring $\mathbb{Z}[t]$ of univariate polynomials. The second is reminiscent of the so-called "base $t$ division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size.

cs.LO↗

arXiv2025

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

This paper investigates $\exists\mathbb{R}(r^{\mathbb{Z}})$, that is the extension of the existential theory of the reals by an additional unary predicate $r^{\mathbb{Z}}$ for the integer powers of a fixed computable real number $r > 0$. If all we have access to is a Turing machine computing $r$, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when: 1. $r$ is known to be transcendental, or 2. $r$ is a root of some given integer polynomial (that is, $r$ is algebraic). In other words, knowing the algebraicity of $r$ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that $r$ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of $\exists\mathbb{R}(r^{\mathbb{Z}})$ is 1. in NEXPTIME if $r$ is a natural number, 2. in EXPSPACE if $r$ is an algebraic number, and 3. in 3EXP if $r$ belongs to a family of transcendental numbers including $\pi$ and Euler's $e$. As a by-product of our results, we are able to remove the appeal to Schanuel's conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS'23]: when the base of the entropic risk is Euler's $e$ and the aversion factor is a fixed algebraic number, the problem is in EXP.

cs.LO↗

arXiv2024

On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories

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. We give two further examples of instantiations of our framework, showing polynomial-time decidability of the fixed negation fragments of weak linear real arithmetic and of the restriction of Presburger arithmetic in which each inequality contains at most one variable.

cs.LO↗

arXiv2024

Integer Linear-Exponential Programming in NP by Quantifier Elimination

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 \bmod 2^y)}$. Our result implies that the existential theory of the structure $(\mathbb{N},0,1,+,2^{(\cdot)},V_2(\cdot,\cdot),\leq)$ 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 \mapsto 2^x$ and the binary predicate $V_2(x,y)$ that is true whenever $y \geq 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).

cs.LO↗

arXiv2024

Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)

This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages (Ln)_{n>=1} such that Ln can be expressed with a pure future formula of size O(n), but it requires formulae of size 2^Ω(n) to be captured with past formulae. As a by-product, such a succinctness result shows the optimality of the pastification algorithm proposed in [Artale et al., KR, 2023]. We show that, in the considered case, succinctness cannot be proven by relying on the classical automata-based method introduced in [Markey, Bull. EATCS, 2003]. In place of this method, we devise and apply a combinatorial proof system whose deduction trees represent LTL formulae. The system can be seen as a proof-centric (one-player) view on the games used by Adler and Immerman to study the succinctness of CTL.

cs.LO↗

arXiv2023

Integer Programming with GCD Constraints

We study the non-linear extension of integer programming with greatest common divisor constraints of the form $\gcd(f,g) \sim d$, where $f$ and $g$ are linear polynomials, $d$ is a positive integer, and $\sim$ is a relation among $\leq, =, \neq$ and $\geq$. 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.

cs.LO↗

arXiv2023

The complexity of Presburger arithmetic with power or powers

We investigate expansions of Presburger arithmetic, 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 for the powers of $2$. The latter theory, denoted $\mathrm{PresPower}$, was introduced by B\"uchi as a first attempt at characterizing the sets of tuples of numbers that can be expressed using finite automata; B\"uchi's method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as $\mathrm{PresExp}$, was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by B\"uchi, 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\"uchi's approaches yield non-elementary blow-ups for $\mathrm{PresPower}$, the theory is in fact decidable in triply exponential time, similarly to the best known quantifier-elimination algorithm for Presburger arithmetic. We also provide a $\mathrm{NExpTime}$ upper bound for the existential fragment of $\mathrm{PresExp}$, a step towards a finer-grained analysis of its complexity. Both these results are established by analyzing a single parameterized satisfiability algorithm for $\mathrm{PresExp}$, which can be specialized to either the setting of $\mathrm{PresPower}$ or the existential theory of $\mathrm{PresExp}$. Besides the new upper bounds for the existential theory of $\mathrm{PresExp}$ and $\mathrm{PresPower}$, we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.

cs.LO↗

arXiv2021

Notes on kAExp(pol) problems for deterministic machines

The complexity of several logics, such as Presburger arithmetic, dependence logics and ambient logics, can only be characterised in terms of alternating Turing machines. Despite quite natural, the presence of alternation can sometimes cause neat ideas to be obfuscated inside heavy technical machinery. In these notes, we propose two problems on deterministic machines that can be used to prove lower bounds with respect to the computational class $k$AExp$_{\text{pol}}$, that is the class of all problems solvable by an alternating Turing machine running in $k$ exponential time and performing a polynomial amount of alternations, with respect to the input size. The first problem, called $k$AExp$_{\text{pol}}$-prenex TM problem, is a problem about deterministic Turing machines. The second problem, called the $k$-exp alternating multi-tiling problem, is analogous to the first one, but on tiling systems. Both problems are natural extensions of the TM alternation problem and the alternating multi-tiling problem proved AExp$_{\text{pol}}$-complete by L. Bozzelli, A. Molinari, A. Montanari and A. Peron in [GandALF, pp. 31-45, 2017]. The proofs presented in these notes follow the elegant exposition in A. Molinari's PhD thesis to extend these results from the case $k = 1$ to the case of arbitrary $k$.

cs.LO↗

arXiv2021

A Complete Axiomatisation for Quantifier-Free Separation Logic

We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-style axiomatisation for quantifier-free separation logic. The calculus is divided in three parts: the axiomatisation of core formulae where Boolean combinations of core formulae capture the expressivity of the whole logic, axioms and inference rules to simulate a bottom-up elimination of separating connectives, and finally structural axioms and inference rules from propositional calculus and Boolean BI with the magic wand.

cs.LO↗

arXiv2021

Presburger arithmetic with threshold counting quantifiers is easy

We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier $\exists^{\ge c} y$ that determines whether the number of different $y$ satisfying some formula is at least $c \in \mathbb N$, where $c$ is given in binary. Using a standard quantifier elimination procedure for Presburger arithmetic, the resulting theory is easily seen to be decidable in 4ExpTime. Our main contribution is to develop a novel quantifier-elimination procedure for a more general counting quantifier that decides this theory in 3ExpTime, meaning that it is no harder to decide than standard Presburger arithmetic. As a side result, we obtain an improved quantifier elimination procedure for Presburger arithmetic with counting quantifiers as studied by Schweikardt [ACM Trans. Comput. Log., 6(3), pp. 634-671, 2005], and a 3ExpTime quantifier-elimination procedure for Presburger arithmetic extended with a generalised modulo counting quantifier.

cs.LO↗

arXiv2021

The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic

The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic.

cs.LO↗

arXiv2020

Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)

We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(*) contains the separating conjunction * from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(*) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(*) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete. As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.

cs.LO↗

arXiv2019

Internal Calculi for Separation Logics

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. 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.

cs.LO↗