Existence of solutions over N to systems of linear equations and constraints of the form y=2^x 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.

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.

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 relative to alternation depth.

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.

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?

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.

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.

To measure how semilinear sets “grow” under Boolean operations, we keep track of the maximum norm of generators.