We consider multicommodity flows in undirected graphs. An instance consists of an edgecapacitated graph \(G\), called the supply graph, and a set of source-sink pairs with associated demands (commodities), defining a demand graph \(H\). An instance is said to be feasible if there exists a flow that routes all demands while respecting the edge capacities. In many applications, it is further required that the entire demand of each commodity be routed along a single path; this is known as the unsplittable multicommodity flow problem. We study conditions under which the existence of a feasible (splittable) flow implies the existence of an unsplittable flow that does not significantly violate edge capacities.

Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the K<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">odkod</small> library as a back-end for finite model finding. K<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">odkod</small> translates the model to a SAT problem; however, this method can often handle only problems of fairly low-size sets and is inherently finite. We present P<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortus</small>, a method for translating Alloy into an equivalent many-sorted first-order logic problem (MSFOL). Once in MSFOL, the problem can be evaluated by an SMT-based finite model finding method implemented in the F<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortress</small> library, creating an alternative back-end for the A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">lloy</small> A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">nalyzer</small>. F<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortress</small> converts the MSFOL finite model finding problem into the logic of uninterpreted functions with equality (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers. We compare the performance of P<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortus</small> with K<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">odkod</small> on a corpus of 63 Alloy models written by experts. Our method is fully integrated into the A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">lloy</small> A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">nalyzer</small>.

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 many-sorted finite model finding. Then, we introduce and prove the correctness of three 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.