Politeness and Stable Infiniteness: Stronger Together

Ying Sheng; Yoni Zohar; Christophe Ringeissen; Andrew Reynolds; Clark Barrett; Cesare Tinelli

doi:10.1007/978-3-030-79876-5_9

Back

Politeness and Stable Infiniteness: Stronger Together

Conference proceeding

Open access

Peer reviewed

Politeness and Stable Infiniteness: Stronger Together

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett and Cesare Tinelli

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol.12699, pp.148-165

Lecture Notes in Computer Science

CADE 2021 - 28th International Conference on Automated Deduction

01/01/2021

DOI: 10.1007/978-3-030-79876-5_9

Files and links (1)

url

https://doi.org/10.1007/978-3-030-79876-5_9View

Published (Version of record) Open Access

Abstract

We make two contributions to the study of polite combination in satisfiability modulo theories. The first contribution is a separation between politeness and strong politeness, by presenting a polite theory that is not strongly polite. This result shows that proving strong politeness (which is often harder than proving politeness) is sometimes needed in order to use polite combination. The second contribution is an optimization to the polite combination method, obtained by borrowing from the Nelson-Oppen method. In its non-deterministic form, the Nelson-Oppen method is based on guessing arrangements over shared variables. In contrast, polite combination requires an arrangement over \emph{all} variables of the shared sort (not just the shared variables). We show that when using polite combination, if the other theory is stably infinite with respect to a shared sort, only the shared variables of that sort need be considered in arrangements, as in the Nelson-Oppen method. Reasoning about arrangements of variables is exponential in the worst case, so reducing the number of variables that are considered has the potential to improve performance significantly. We show preliminary evidence for this in practice by demonstrating a speed-up on a smart contract verification benchmark.

Computer Science

Logic in Computer Science

Details

Title: Subtitle: Politeness and Stable Infiniteness: Stronger Together
Creators: Ying Sheng - Stanford University
Yoni Zohar - Stanford University
Christophe Ringeissen - Université de Lorraine
Andrew Reynolds - University of Iowa
Clark Barrett - Stanford University
Cesare Tinelli - University of Iowa
Resource Type: Conference proceeding
Publication Details: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol.12699, pp.148-165
Conference: CADE 2021 - 28th International Conference on Automated Deduction
Series: Lecture Notes in Computer Science
DOI: 10.1007/978-3-030-79876-5_9
ISSN: 0302-9743
eISSN: 1611-3349
Publisher: Springer
Language: English
Date published: 01/01/2021
Academic Unit: Computer Science
Record Identifier: 9984259489502771

Metrics

9 Record Views

6 Times Cited - Web of Science