Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Artikel
Titel:
Lecture Notes in Computer Science: QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Beteiligte:
Bonacina, Maria Paola;
Graham-Lengrand, Stéphane;
Vauthier, Christophe
Erschienen:
Springer Nature Switzerland, 2023
Erschienen in:
Lecture Notes in Computer Science (2023), Seite 78-95
Sprache:
Englisch
DOI:
10.1007/978-3-031-38499-8_5
ISBN:
9783031384998;
9783031384981
ISSN:
0302-9743;
1611-3349
Entstehung:
Anmerkungen:
Beschreibung:
AbstractThis paper presents and proves totally correct a new algorithm, called$$\textsf{QSMA}$$QSMA, for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of$$\textsf{QSMA}$$QSMAimplemented in YicesQS is described and shown to preserve total correctness. A report on the performance of YicesQS at the 2022 SMT competition is included. YicesQS ran in the$$\textsf{LIA}$$LIA,$$\textsf{NIA}$$NIA,$$\textsf{LRA}$$LRA,$$\textsf{NRA}$$NRA, and$$\textsf{BV}$$BVcategories and ranked second for the “largest contribution” award (single queries). It was the only solver to solve all$$\textsf{LRA}$$LRAinstances, where it was about two orders of magnitude faster than the second best solver (Z3).