Download PDFOpen PDF in browserCurrent versionVIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version)EasyChair Preprint 13150, version 158 pages•Date: April 30, 2024AbstractWe introduce Virtual Integer-Real Arithmetic Substitution (Viras), a quantifier elimination procedure for deciding quantified linear mixed integer-real arithmetic problems. Viras combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that Viras gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve. Keyphrases: Descision Procedure, LIA, LIRA, LRA, Presburger arithmetic, SMT, automated reasoning, linear arithmetic, logic, quantifier elimination
|