相关论文: Short Presburger arithmetic is hard

Exactly solving first-order constraints (i.e., first-order formulas over a certain predefined structure) can be a very hard, or even undecidable problem. In continuous structures like the real numbers it is promising to compute approximate…

This paper considers the computational hardness of computing expected outcomes and deciding almost-sure termination of probabilistic programs. We show that deciding almost-sure termination and deciding whether the expected outcome of a…

We present a first-order theory of sequences with integer elements, Presburger arithmetic, and regular constraints, which can model significant properties of data structures such as arrays and lists. We give a decision procedure for the…

We prove several decidability and undecidability results for the satisfiability and validity problems for languages that can express solutions to word equations with length constraints. The atomic formulas over this language are equality…

We study the complexity of satisfiability problems in probabilistic and causal reasoning. Given random variables $X_1, X_2,\ldots$ over finite domains, the basic terms are probabilities of propositional formulas over atomic events $X_i =…

We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation logic with various forms of Presburger arithmetic…

We examine the complexity of basic regular operations on languages represented by Boolean and alternating finite automata. We get tight upper bounds m+n and m+n+1 for union, intersection, and difference, 2^m+n and 2^m+n+1 for concatenation,…

We investigate the class of regular-ordered word equations. In such equations, each variable occurs at most once in each side and the order of the variables occurring in both sides is the preserved (the variables can be, however, separated…

Many problems in Computer Science can be abstracted to the following question: given a set of objects and rules respectively, which new objects can be produced? In the paper, we consider a succinct version of the question: given a set of…

Propositional satisfiability (SAT) is one of the most fundamental problems in computer science. Its worst-case hardness lies at the core of computational complexity theory, for example in the form of NP-hardness and the (Strong) Exponential…

Satisfiability of word equations is an important problem in the intersection of formal languages and algebra: Given two sequences consisting of letters and variables we are to decide whether there is a substitution for the variables that…

We identify a fragment of Presburger arithmetic enriched with free function symbols and cardinality constraints for interpreted sets, which is amenable to automated analysis. We establish decidability and complexity results for such a…

Motivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyond ${\bf NP\neq co NP}$. These conjectures formally connect computational complexity with the difficulty of…

The Boolean satisfiability problem (SAT) is a well-known example of monotonic reasoning, of intense practical interest due to fast solvers, complemented by rigorous fine-grained complexity results. However, for non-monotonic reasoning,…

We continue the investigation of polynomial-time sparsification for NP-complete Boolean Constraint Satisfaction Problems (CSPs). The goal in sparsification is to reduce the number of constraints in a problem instance without changing the…

All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is…

Presburger Arithmetic $\mathop{\mathbf{PrA}}\nolimits$ is the true theory of natural numbers with addition. We consider linear orderings interpretable in Presburger Arithmetic and establish various necessary and sufficient conditions for…

In various applications the search for certificates for certain properties (e.g., stability of dynamical systems, program termination) can be formulated as a quantified constraint solving problem with quantifier prefix exists-forall. In…

It is well known that sparse approximation problem is \textsf{NP}-hard under general dictionaries. Several algorithms have been devised and analyzed in the past decade under various assumptions on the \emph{coherence} $\mu$ of the…

Short integer linear programs are programs with a relatively small number of constraints. We show how recent improvements on the running-times of solvers for such programs can be used to obtain fast pseudo-polynomial time algorithms for…