Skip to main content

Linear Arithmetic Satisfiability Via Strategy Improvement

Author(s): Farzan, Azadeh; Kincaid, Zachary

To refer to this page use:
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.
Publication Date: Jul-2016
Citation: Farzan, Azadeh, and Zachary Kincaid. "Linear Arithmetic Satisfiability Via Strategy Improvement." In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (2016): pp. 735-743.
ISSN: 1045-0823
Pages: 735 - 743
Type of Material: Conference Article
Journal/Proceeding Title: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.