Publications on geometric problems
- D. Chistikov, C. Haase, A. Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. LICS 2022.
[WRAP]
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.
[doi]
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.
[DROPS]
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.
- 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.
[doi]
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).
[WRAP]
[arXiv]
[doi]
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.
[DROPS]
[WRAP]
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.
[WRAP]
[arXiv]
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.
[WRAP]
[arXiv]
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.
[DROPS]
[pdf]
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.
[doi]
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.
ICALP’16.
[DROPS]
[arXiv]
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.
ICALP’16.
[DROPS]
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).