Lagrangian-Based Duality for Quantified SMT Algorithms

Abstract

Lagrangian-based duality, traditionally applied in optimization, has recently been generalized to serve as the basis for a unifying framework for primal-dual search algorithms in the context of program verification and automated reasoning. In this paper, we analyze Quantified Satisfiability Modulo Theories (QSMT) algorithms using this framework. Interestingly, our Lagrangian-based analysis reveals that three recently proposed algorithms for quantified linear real arithmetic (LRA) share a common structure, and that their main differences lie in the approach to a certain problem—model-based projection for Lagrangian-based duality, traditionally applied in optimization, has recently been generalized to serve as the basis for a unifying framework for primal-dual search algorithms in the context of program verification and automated reasoning. In this paper, we analyze Quantified Satisfiability Modulo Theories (QSMT) algorithms using this framework. Interestingly, our Lagrangian-based analysis reveals that three recently proposed algorithms for quantified linear real arithmetic (LRA) share a common structure, and that their main differences lie in the approach to a certain problem—model-based projection for ∃∀-formulas. Moreover, in the course of this Lagrangian-based analysis, we identify an issue with the progress property of one of the algorithms, propose a way to fix the issue, and experimentally demonstrate that the proposed fix improves performance. ∃∀-formulas. Moreover, in the course of this Lagrangian-based analysis, we identify an issue with the progress property of one of the algorithms, propose a way to fix the issue, and experimentally demonstrate that the proposed fix improves performance.