Linear arithmetic satisfiability via strategy improvement

Azadeh Farzan, Zachary Kincaid

Research output: Contribution to journalConference articlepeer-review

5 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)735-743
Number of pages9
JournalIJCAI International Joint Conference on Artificial Intelligence
Volume2016-January
StatePublished - Jan 1 2016
Event25th International Joint Conference on Artificial Intelligence, IJCAI 2016 - New York, United States
Duration: Jul 9 2016Jul 15 2016

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Linear arithmetic satisfiability via strategy improvement'. Together they form a unique fingerprint.

Cite this