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.|
|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.|
|Pages:||735 - 743|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.