- 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.
We prove that the decision problem for linear arithmetic over Z with just equality (no inequalities) is as hard as for standard linear integer arithmetic. To do so, we define and study the complexity of a quantified version of SAT that supports higher-order Boolean functions.
- S. Almagor, D. Chistikov, J. Ouaknine, J. Worrell. O-minimal invariants for discrete-time dynamical systems. ACM Transactions on Computational Logic (2022). Extended version of the ICALP’18 paper.
For while loops of the form “while x in S do x:=A*x” (where x is initialized to a rational vector, A is a rational matrix, and S is a nice set), minimal invariants look like truncated cones.
- D. Chistikov, O. Goulko, A. Kent, M. Paterson. Globe-hopping. Proceedings of the Royal Society A (2020).
We look at a probabilistic puzzle on the sphere which has applications to quantum information theory (Bell inequalities).
- 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?
- S. Almagor, D. Chistikov, J. Ouaknine, J. Worrell. O-minimal invariants for linear loops. ICALP 2018. [DROPS] Extended version in ACM Transactions on Computational Logic (2022).
- D. Chistikov, S. Kiefer, I. Marušić, M. Shirmohammadi, J. Worrell. Nonnegative matrix factorization reqires irrationality. SIAM Journal on Applied Algebra and Geometry (2017). Extended version of the SODA’17 paper.
We find a matrix for which the nonnegative rank over the reals and over the rationals are different.
- 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, S. Kiefer, I. Marušić, M. Shirmohammadi, J. Worrell. On rationality of nonnegative matrix factorization. SODA 2017.
We find a matrix for which the nonnegative rank over the reals and over the rationals are different. Consequently, state minimization of hidden Markov models may require irrational probabilities.
- D. Chistikov, S. Kiefer, I. Marušić, M. Shirmohammadi, J. Worrell. On restricted nonnegative matrix factorization.
There exists a pair of 3D polytopes with rational vertices, one inside the other, such that every intermediate polytope with 5 vertices must have a vertex with an irrational coordinate.
- 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).