Linear Arithmetic: Geometry, Algorithms, and Logic

Logic and Computation Courses

Linear Arithmetic: Geometry, Algorithms, and Logic,
Dmitry Chistikov (University of Warwick, UK) and Christoph Haase (University of Oxford, UK)

Week 1, 14:00 – 15:30, Room 224, Floor 1

Theories of linear arithmetic over R, Q, Z, and N are at the core of computational logic. Arising as generalizations of their existential conjunctive fragments-linear programming and integer programming-they occur in many contexts in computer science both in theory and practice. Reducing domain-specific constraints to a linear arithmetic theory is a standard and powerful problem-solving technique. Arithmetic theories are a fascinating object to study, as they lie at the interface of geometry, algorithmics, and logic.

This course is an introduction to the theories of linear arithmetic, such as the first order linear theory of the reals and Presburger arithmetic, its analogue over the natural numbers. We will first explore the geometry of linear constraints over R and Z, defining convex polytopes and convex polyhedra, as well as so-called hybrid linear sets, their discrete analogue. Subsequently, we will cover classic algorithmic techniques for linear programming (simplex and polynomial-time algorithms) and integer programming (branch-and-bound and rounding techniques) and decision procedures for Presburger arithmetic, such as quantifier elimination and automata-based techniques. Finally, we will discuss the expressive power and computational complexity of linear arithmetic theories.

Syllabus

1. Introduction to linear arithmetic. Geometry of linear arithmetic (slides).
2. Linear programming (slides).
3. Integer programming (slides).
4. Theories of linear arithmetic: decision procedures (slides).
5. Theories of linear arithmetic: expressive power (slides).

Prerequisites

We assume basic knowledge of the following:

• Linear algebra
• Algorithms
• Logic or discrete mathematics
• Computational complexity (desirable, but not required)

References

General references:

• Niels Lauritzen. Lectures on convex sets (link). 2009.
• Andreas Paffenholz. Polyhedral geometry and linear optimization. Lecture notes, summer semester 2010 (link).
• Jesús A. De Loera. Actually doing it: Polyhedral computation and its applications (link). 2010.
• Jean Gallier and Jocelyn Quaintance. Aspects of convex geometry, polyhedra, linear programming, shellings, Voronoi diagrams, Delaunay triangulations (link). 2017.
• R. Tyrrell Rockafellar. Convex analysis (link). Princeton University Press. 1972.
• Alexander Schrijver. Theory of linear and integer programming (google link). John Wiley & Sons. 1986.

References specific to individual lectures:

• For Lectures 2 & 3: Michel X. Goemans. Lecture notes on the ellipsoid algorithm. MIT course 18.453 Combinatorial Optimization (link). 2017.
• For Lecture 3: David P. Williamson and David B. Shmoys. The design of approximation algorithms (link). Cambridge University Press. 2010. Chapter 1.
• For Lectures 3 & 4: Christoph Haase. A survival guide to Presburger arithmtic (link). ACM SIGLOG News. 2018.
• For Lecture 5: Dexter C. Kozen. Theory of Computation (google link). Springer, London. 2006. Lecture 23.