New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding
Loading...
Date
2023-06-01
Authors
Poremba, Joseph
Day, Nancy A.
Vakili, Amirhossein
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