Konstantin Korovin (Manchester)
Solving Linear Arithmetic
by Reasoning-Based
Methods

Reasoning methods for propositional logic based on resolution and the Davis-Putnam-Logemann-Loveland procedure (DPLL) have enjoyed many success stories in solving large problems coming from real-life applications.
One of the challenges is whether we can go beyond and extend this technology to other domains such as arithmetic.

In our recent work we introduced two methods for solving systems of linear inequalities called conflict resolution and bound propagation which aim to address this challenge.
In particular, conflict resolution can be seen as a refinement of resolution and bound propagation is analogous to DPLL with constraint propagation, backjumping and lemma learning. There are non-trivial issues when considering arithmetic constraints such as termination, dynamic variable ordering and dealing with large coefficients.

In this talk I will overview our approach and related work.