- M. Benedikt, D. Chistikov, A. Mansutti. The complexity of Presburger arithmetic with power or powers. ICALP 2023.
Existence of solutions over N to systems of linear equations and constraints of the form y=2x can be decided in nondeterministic exponential time. Also, linear integer arithmetic extended with a predicate for powers of 2 can be decided in triply exponential time.
- D. Chistikov, C. Haase, A. Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. LICS 2022.
A decision procedure for Presburger arithmetic based on semilinear sets runs in triply exponential time. Also, the VC dimension of Presburger formulas is at most doubly exponential in their length.
- D. Chistikov, C. Haase, A. Mansutti. Quantifier elimination for counting extensions of Presburger arithmetic. FoSSaCS 2022.
We extend linear integer arithmetic with quantifiers of the form “there exists at least c values of x” and similar. It turns out such theories still support efficient quantifier elimination, even in bounded alternation depth.
- D. Chistikov, C. Haase, Z. Hadizadeh, A. Mansutti. Higher-order Boolean satisfiability. MFCS 2022.
The decision problem for linear arithmetic over Z with just equality (no inequalities) is as hard as for standard linear integer arithmetic. To prove this, we define and study the complexity of a quantified version of SAT that supports higher-order Boolean functions.
- D. Chistikov, C. Haase. On the power of ordering in linear arithmetic theories. ICALP 2020.
Given a formula of linear arithmetic, can we decide if the same set can be defined by another formula that uses just equality, without inequalities?
- D. Chistikov, R. Dimitrova, R. Majumdar. Approximate counting in SMT and value estimation for probabilistic programs. ACTA Informatica (2017). Special issue for TACAS’15.
Relying on ideas of Sipser and Stockmeyer, existing SMT solvers can do approximate model counting (discrete counting or volume estimation) for logical theories of arithmetic.
- D. Chistikov, C. Haase. On the complexity of quantified integer programming. ICALP 2017.
If some variables in integer programs are quantified universally instead of existentially, then the decision problem becomes complete for the k-th level of the polynomial hierarchy, assuming k quantifier blocks.
- D. Chistikov, C. Haase. The taming of the semi-linear set.
To measure how semilinear sets “grow” under Boolean operations, we keep track of the maximum norm of generators.
- D. Chistikov, R. Dimitrova, R. Majumdar. Approximate counting in SMT and value estimation for probabilistic programs. TACAS’15. Extended version in Acta Informatica (2017).