New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding
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.
Collections
Cite this version of the work
Joseph Poremba, Nancy A. Day, Amirhossein Vakili
(2023).
New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding. UWSpace.
http://hdl.handle.net/10012/19627
Other formats