VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version)

EasyChair Preprint no. 13150, version 2

Abstract

We 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: automated reasoning, Descision Procedure, LIA, linear arithmetic, LIRA, logic, LRA, Presburger arithmetic, quantifier elimination, SMT

@Booklet{EasyChair:13150,
  author = {Johannes Schoisswohl and Laura Kovács and Konstantin Korovin},
  title = {VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version)},
  howpublished = {EasyChair Preprint no. 13150},

  year = {EasyChair, 2024}}