---
title: "Linear Arithmetic Satisfiability via Strategy Improvement"
authors:
  - "Azadeh Farzan"
  - "Zachary Kincaid"
doi: ""
url: "https://ijcai.org/proceedings/2016/110"
pdf: "https://ijcai.org/proceedings/2016/0110.pdf"
venue: "Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence"
year: 2016
pages: "735-742"
track: ""
keywords:
---

# Linear Arithmetic Satisfiability via Strategy Improvement

Azadeh Farzan, Zachary Kincaid

*Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence*, pages 735-742.

## Abstract

Satisfiability-checking of formulas in the theory of linear rational arithmetic (LRA) has broad applications including program verification and synthesis. Satisfiability Modulo Theories (SMT) solvers are effective at checking satisfiability of the ground fragment of LRA, but applying them to quantified formulas requires a costly quantifier elimination step. This article presents a novel decision procedure for LRA that leverages SMT solvers for the ground fragment of LRA, but avoids explicit quantifier elimination. The intuition behind the algorithm stems from an interpretation of a quantified formula as a game between two players, whose goals are to prove that the formula is either satisfiable or not. The algorithm synthesizes a winning strategy for one of the players by iteratively improving candidate strategies for both. Experimental results demonstrate that the proposed procedure is competitive with existing solvers.