VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

Johannes Schoisswohl; Laura Kovács; Konstantin Korovin

doi:10.29007/kg4v

VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

Johannes Schoisswohl, Laura Kovács, Konstantin Korovin

Formal Methods

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

2 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24)
Editors	N. Bjørner, M. Heule, A. Voronkov
Publisher	EasyChair
Pages	147–164
Volume	100
DOIs	https://doi.org/10.29007/kg4v
Publication status	Published - 26 May 2024

Publication series

Name	EPiC Series in Computing

Keywords

arithmetic
decision precedure
lira
quantifier elimination
smt
virtual substitution

Access to Document

10.29007/kg4vLicence: CC BY-NC-ND

LPAR_2024_pages_147-164Final published version, 597 KBLicence: CC BY-NC-ND

SCorCH: Secure Code for Capability Hardware
Reger, G. (PI), Cordeiro, L. (CoI), Korovin, K. (CoI), Mustafa, M. (CoI) & Olivier, P. (CoI)
1/07/20 → 31/12/23
Project: Research

Cite this

Schoisswohl, J., Kovács, L., & Korovin, K. (2024). VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24) (Vol. 100, pp. 147–164). (EPiC Series in Computing). EasyChair. https://doi.org/10.29007/kg4v

@inproceedings{05b9be03729b4047982acf51ec824220,

title = "VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic",

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{\textquoteright}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.",

keywords = "arithmetic, decision precedure, lira, quantifier elimination, smt, virtual substitution",

author = "Johannes Schoisswohl and Laura Kov{\'a}cs and Konstantin Korovin",

year = "2024",

month = may,

day = "26",

doi = "10.29007/kg4v",

language = "English",

volume = "100",

series = "EPiC Series in Computing",

publisher = "EasyChair",

pages = "147–164",

editor = "Bj{\o}rner, {N. } and { Heule}, {M. } and Voronkov, {A. }",

booktitle = "Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24)",

address = "United Kingdom",

}

VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. / Schoisswohl, Johannes; Kovács, Laura; Korovin, Konstantin.
Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24). ed. / N. Bjørner; M. Heule; A. Voronkov. Vol. 100 EasyChair, 2024. p. 147–164 (EPiC Series in Computing).

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

AU - Schoisswohl, Johannes

AU - Kovács, Laura

AU - Korovin, Konstantin

PY - 2024/5/26

Y1 - 2024/5/26

N2 - 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.

AB - 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.

KW - arithmetic

KW - decision precedure

KW - lira

KW - quantifier elimination

KW - smt

KW - virtual substitution

U2 - 10.29007/kg4v

DO - 10.29007/kg4v

M3 - Conference contribution

VL - 100

T3 - EPiC Series in Computing

SP - 147

EP - 164

BT - Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24)

A2 - Bjørner, N.

A2 - Heule, M.

A2 - Voronkov, A.

PB - EasyChair

ER -

VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Projects

SCorCH: Secure Code for Capability Hardware

Cite this