Domenico Cantone

TCS Journal 2026 Journal Article

Quantum algorithms for longest common and palindromic substrings in the circuit model

• Domenico Cantone
• Simone Faro
• Arianna Pavone
• Caterina Viola

The Longest Common Substring (LCS) and Longest Palindromic Substring (LPS) problems are fundamental challenges in string processing, traditionally solved in linear time using classical computation through suffix trees. Recent breakthroughs by Le Gall and Seddighin [1] introduced sublinear quantum query algorithms, while Akmal and Jin [2] further improved the LCS complexity to O ˜ ( n 2 / 3 ). While these results are remarkable in the quantum query model, their practical implementation on real quantum hardware remains elusive. In this paper, we bridge this gap by presenting the first O ˜ ( n ) quantum algorithms for both LCS and LPS in the circuit model of computation. Our circuits are explicitly constructed and analyzed in terms of size and depth, achieving polylogarithmic overheads while preserving the O ˜ ( n ) depth bound. This provides, for the first time, concrete circuit-level blueprints and resource estimates for quantum solutions to LCS and LPS.

TCS Journal 2023 Journal Article

A decidable theory involving addition of differentiable real functions

• Gabriele Buriola
• Domenico Cantone
• Gianluca Cincotti
• Eugenio G. Omodeo
• Gaetano T. Spartà

This paper enriches a pre-existing decision algorithm, which in turn augmented a fragment of Tarski's elementary algebra with one-argument real functions endowed with a continuous first derivative. In its present (still quantifier-free) version, our decidable language embodies the addition of functions and multiplication of functions by scalars; the issue we address is the one of satisfiability. As regards real numbers, individual variables and constructs designating the basic arithmetic operations are available, along with comparison relators. As regards functions, we have variables of another sort, out of which compound terms are formed by means of constructs designating addition and differentiation. An array of predicates designates various relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: function comparisons, strict and non-strict monotonicity / convexity / concavity, comparisons between the derivative of a function and a real-valued term. Our decision method consists in preprocessing the given formula into an equi-satisfiable quantifier-free formula of the elementary algebra of real numbers, whose satisfiability can then be checked by means of Tarski's decision method. No direct reference to functions will appear in the target formula, each function variable having been superseded by a collection of stub real variables; hence, in order to prove that the proposed translation is satisfiability-preserving, we must figure out a flexible-enough family of interpolating C 1 functions that can accommodate a model for the source formula whenever the target formula turns out to be satisfiable. With respect to the results announced in earlier papers of the same stream, a significant effort went into designing the family of interpolating functions so that it could meet the new constraints stemming from the presence of function addition (along with differentiation) among the constructs of our fragment of mathematical analysis.

TCS Journal 2023 Journal Article

Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages

• Domenico Cantone
• Pietro Maugeri
• Eugenio G. Omodeo

We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubic-time satisfiability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator ∪ and the logical relators = and ≠. It can be seen that the dual language involving the Boolean operator ∩ and, again, the relators = and ≠, also admits a cubic-time satisfiability decision test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satisfiability test can be used to treat the relators ⊆ and ⊈, and the predicates ‘ Image 1 ’ and ‘ Image 2 ’, meaning ‘the argument is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘ Image 3 ’ and ‘ Image 4 ’. Those richer languages are ‘polynomial maximal’, in the sense that each language strictly containing either of them and whose formulae are conjunctions of literals has an NP-hard satisfiability problem. A generalized version of the two said satisfiability tests can treat the relator ⊄, though at the price of a worsening of the algorithmic complexity (from cubic to quintic time).

GandALF Workshop 2021 Workshop Paper

On the Convexity of a Fragment of Pure Set Theory with Applications within a Nelson-Oppen Framework

• Domenico Cantone
• Andrea De Domenico
• Pietro Maugeri

The Satisfiability Modulo Theories (SMT) issue concerns the satisfiability of formulae from multiple background theories, usually expressed in the language of first-order predicate logic with equality. SMT solvers are often based on variants of the Nelson-Oppen combination method, a solver for the quantifier-free fragment of the combination of theories with disjoint signatures, via cooperation among their decision procedures. When each of the theories to be combined by the Nelson-Oppen method is convex (that is, any conjunction of its literals can imply a disjunction of equalities only when it implies at least one of the equalities) and decidable in polynomial time, the running time of the combination procedure is guaranteed to be polynomial in the size of the input formula. In this paper, we prove the convexity of a fragment of Zermelo-Fraenkel set theory, called Multi-Level Syllogistic, most of whose polynomially decidable fragments we have recently characterized.

TCS Journal 2020 Journal Article

Complexity assessments for decidable fragments of set theory. II: A taxonomy for ‘small’ languages involving membership

• Domenico Cantone
• Pietro Maugeri
• Eugenio G. Omodeo

We carry on a long-standing investigation aimed at identifying fragments of set theory that are potentially useful in automated verification with proof-checkers, such as ÆtnaNova, based on the set-theoretic formalism. This note provides a complete taxonomy of the polynomial and the NP-complete fragments consisting of all conjunctions that involve, besides variables intended to range over the von Neumann set-universe, a collection of constructs drawn from the Boolean set operators ∪, ∩, ∖ and the membership relators ∈ and ∉. This is done in sight of combining the aforementioned taxonomy with one recently put together for analogous fragments involving, in place of the relators ∈ and ∉, the Boolean relators ⊆, = and the predicates ‘ ⋅ = ∅ ’ and ‘ Disj ( ⋅, ⋅ ) ’ (respectively meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’), along with their opposites ‘ ⊈, ≠, ⋅ ≠ ∅ ’ and ‘ ¬ Disj ( ⋅, ⋅ ) ’.

I&C Journal 2018 Journal Article

Games, automata, logics and formal verification (GandALF 2016)

• Domenico Cantone
• Giorgio Delzanno

GandALF Workshop 2017 Workshop Paper

The Satisfiability Problem for Boolean Set Theory with a Choice Correspondence

• Domenico Cantone
• Alfio Giarlotta
• Stephen Watson

Given a set U of alternatives, a choice (correspondence) on U is a contractive map c defined on a family Omega of nonempty subsets of U. Semantically, a choice c associates to each menu A in Omega a nonempty subset c(A) of A comprising all elements of A that are deemed selectable by an agent. A choice on U is total if its domain is the powerset of U minus the empty set, and partial otherwise. According to the theory of revealed preferences, a choice is rationalizable if it can be retrieved from a binary relation on U by taking all maximal elements of each menu. It is well-known that rationalizable choices are characterized by the satisfaction of suitable axioms of consistency, which codify logical rules of selection within menus. For instance, WARP (Weak Axiom of Revealed Preference) characterizes choices rationalizable by a transitive relation. Here we study the satisfiability problem for unquantified formulae of an elementary fragment of set theory involving a choice function symbol c, the Boolean set operators and the singleton, the equality and inclusion predicates, and the propositional connectives. In particular, we consider the cases in which the interpretation of c satisfies any combination of two specific axioms of consistency, whose conjunction is equivalent to WARP. In two cases we prove that the related satisfiability problem is NP-complete, whereas in the remaining cases we obtain NP-completeness under the additional assumption that the number of choice terms is constant.

TCS Journal 2014 Journal Article

A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions

• Domenico Cantone
• Cristiano Longo

In this paper we address the decision problem for a two-sorted fragment of set theory with restricted quantification which extends the language studied in [4] with pair-related quantifiers and constructs. We also show that the decision problem for our language has a nondeterministic exponential-time complexity. However, in the restricted case of formulae whose quantifier prefixes have length bounded by a constant, the decision problem becomes NP-complete. In spite of such restriction, several useful set-theoretic constructs, mostly related to maps, are still expressible. We also argue that our restricted language has applications to knowledge representation, with particular reference to metamodeling issues. Finally, we compare our proposed language with two similar languages in terms of their expressivity and present some undecidable extensions of it, involving any of the domain, range, image, and map composition operators.

I&C Journal 2014 Journal Article

Formative processes with applications to the decision problem in set theory: II. Powerset and singleton operators, finiteness predicate

• Domenico Cantone
• Pietro Ursino

In this paper we solve the satisfiability problem for the quantifier-free fragment of set theory MLSSPF involving in addition to the basic Boolean set operators of union, intersection, and difference, also the powerset and singleton operators, and a finiteness predicate. The more restricted fragment obtained by dropping the finiteness predicate has been shown to have a solvable satisfiability problem in a previous paper, by establishing for it a small model property. We exploit the latter decision result for dealing also with the finiteness predicate (and therefore with the infiniteness predicate too) and prove a small witness-model property for MLSSPF, asserting that any model for a satisfiable formula Φ with m distinct variables of the fragment of our interest admits a finite representation bounded by c ( m ), where c is a suitable computable function. Since such candidate representations are finitely many, their number does not exceed a known bound, and it can be recognized algorithmically whether they indeed represent a(n infinite) model for the input formula, the decidability of the satisfiability problem for MLSSPF follows.

TCS Journal 2013 Journal Article

Efficient string-matching allowing for non-overlapping inversions

• Domenico Cantone
• Salvatore Cristofaro
• Simone Faro

Inversions are a class of chromosomal mutations, widely regarded as one of the major mechanisms for reorganizing the genome. In this paper we present a new algorithm for the approximate string matching problem allowing for non-overlapping inversions which runs in O ( n m ) worst-case time and O ( m 2 ) space, for a character sequence of size n and pattern of size m. This improves upon a previous O ( n m 2 ) -time algorithm. In addition we present a variant of our algorithm with the same complexity in the worst case, but with a O ( n ) time complexity in the average case.

TCS Journal 2013 Journal Article

Further analysis of the remedian algorithm

• Domenico Cantone
• Micha Hofri

We present an analysis of the remedian, an efficient, known algorithm, for the approximate median selection problem, that is easy to implement. The algorithm can be used for data in an array, as well as for streaming data. In an array it performs in-place, recursively dividing the candidate values into sets of size b, from which exact medians are selected for the next phase. On streaming data it performs a filter operation, requiring, by the time n items are processed, the storage of log b n candidate entries. The contribution of the article is a precise characterization, combinatorial and asymptotic, of the accuracy of the algorithm, showing explicitly the role of the critical design parameter b. In addition, we compute the time and space costs of the algorithm, and present experimental illustrations of its accuracy.

I&C Journal 2012 Journal Article

A compact representation of nondeterministic (suffix) automata for the bit-parallel approach

• Domenico Cantone
• Simone Faro
• Emanuele Giaquinta

We present a novel technique, suitable for bit-parallelism, for representing both the nondeterministic automaton and the nondeterministic suffix automaton of a given string in a more compact way. Our approach is based on a particular factorization of strings which on the average allows to pack in a machine word of w bits automata state configurations for strings of length greater than w. We adapted the Shift-And and BNDM algorithms using our encoding and compared them with the original algorithms. Experimental results show that the new variants are generally faster for long patterns.

GandALF Workshop 2012 Workshop Paper

A decidable quantified fragment of set theory with ordered pairs and some undecidable extensions

• Domenico Cantone
• Cristiano Longo

In this paper we address the decision problem for a fragment of set theory with restricted quantification which extends the language studied in [4] with pair related quantifiers and constructs, in view of possible applications in the field of knowledge representation. We will also show that the decision problem for our language has a non-deterministic exponential time complexity. However, for the restricted case of formulae whose quantifier prefixes have length bounded by a constant, the decision problem becomes NP-complete. We also observe that in spite of such restriction, several useful set-theoretic constructs, mostly related to maps, are expressible. Finally, we present some undecidable extensions of our language, involving any of the operators domain, range, image, and map composition. [4] Michael Breban, Alfredo Ferro, Eugenio G. Omodeo and Jacob T. Schwartz (1981): Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Communications on Pure and Applied Mathematics 34, pp. 177-195

CSL Conference 2011 Conference Paper

A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics

• Domenico Cantone
• Cristiano Longo
• Marianna Nicolosi Asmundo

We present a decision procedure for a quantified fragment of set theory involving ordered pairs and some operators to manipulate them. When our decision procedure is applied to formulae in this fragment whose quantifier prefixes have length bounded by a fixed constant, it runs in nondeterministic polynomial-time. Related to this fragment, we also introduce a description logic which provides an unusually large set of constructs, such as, for instance, Boolean constructs among roles. The set-theoretic nature of the description logics semantics yields a straightforward reduction of the knowledge base consistency problem to the satisfiability problem for formulae of our fragment with quantifier prefixes of length at most 2, from which the NP-completeness of reasoning in this novel description logic follows. Finally, we extend this reduction to cope also with SWRL rules.

I&C Journal 2002 Journal Article

Formative Processes with Applications to the Decision Problem in Set Theory

• Domenico Cantone
• Pietro Ursino
• Eugenio G. Omodeo

This paper introduces formative processes, composed by transitive partitions. Given a family F of sets, a formative process ending in the Venn partition Σ of F is shown to exist. Sufficient criteria are also singled out for a transitive partition to model (via a function from set variables to unions of sets in the partition) all set-literals modeled by Σ. On the basis of such criteria a procedure is designed that mimics a given formative process by another where sets have finite rank bounded by C(|Σ|), with C a specific computable function. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satisfiability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described (which is able to exhibit a set-solution when the answer is affirmative) can be extended to solve the satisfiability problem for broader fragments of set theory.

CSL Conference 1991 Conference Paper

Decision Problems for Tarski and Presburger Arithmetics Extended With Sets

• Domenico Cantone
• Vincenzo Cutello
• Jacob T. Schwartz

CSL Conference 1990 Conference Paper

Set-Theoretic Reductions of Hilbert's Tenth Problem

• Domenico Cantone
• Vincenzo Cutello
• Alberto Policriti

IJCAI Conference 1989 Conference Paper

On the Decidability of Formulae Involving Continuous and Closed Functions

• Domenico Cantone
• Eugenio G. Omodeo