AlloyMax: bringing maximum satisfaction to relational specifications

Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an optimal solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most permissive (i.e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems.

We propose Alloy Max , an extension of Alloy with a capability to express and analyze problems with optimal solutions. Alloy Max introduces (1) a small addition of language constructs that can be used to specify a wide range of problems that involve optimality and (2) a new analysis engine that leverages a Maximum Satisfiability (MaxSAT ) solver to generate optimal solutions. To enable this new type of analysis, we show how a specification in a first-order relational logic can be translated into an input format of MaxSAT solvers-namely, a Boolean formula in weighted conjunctive normal form (WCNF). We demonstrate the applicability and scalability of Alloy Max on a benchmark of problems. To our knowledge, Alloy Max is the first approach to enable analysis with optimality in a relational modeling language, and we believe that Alloy Max has the potential to bring a wide range of new applications to Alloy.