New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding

Loading...
Thumbnail Image

Date

2023-06-01

Authors

Poremba, Joseph
Day, Nancy A.
Vakili, Amirhossein

Advisor

Journal Title

Journal ISSN

Volume Title

Publisher

IEEE

Abstract

Symmetry in finite model finding problems of many-sorted first-order logic (MSFOL) can be exploited to reduce the number of interpretations considered during search, thereby improving solver performance for tools such as the Alloy Analyzer. We present a framework to soundly compose static symmetry breaking schemes for MSFOL: 1) one for functions with distinct sorts in the domain and range; 2) one for functions where the range sort appears in the domain; and 3) one for predicates. We provide a novel presentation of sort inference in the context of symmetry breaking that yields a new mathematical link between sorts and symmetries. We empirically investigate how our symmetry breaking approaches affect solving performance.

Description

© 2023 IEEE. J. Poremba, N. A. Day and A. Vakili, "New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding," in IEEE Transactions on Software Engineering, vol. 49, no. 6, pp. 3487-3503, 1 June 2023, doi: 10.1109/TSE.2023.3256939.

Keywords

finite model finding, symmetry breaking

LC Subject Headings

Citation