Skip to main content Skip to navigation

Publications on arithmetic theories (logical theories of arithmetic)

  • M. Benedikt, D. Chistikov, A. Mansutti. The complexity of Presburger arithmetic with power or powers. ICALP 2023. [DROPS]

    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. [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.

  • 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?

  • 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, 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).