一句话：提出 AlloyMax，将最大满足/优化目标引入 Alloy 关系规范，使 SAT 无法处理的最优解分析成为可能。
Alloy 是基于一阶关系逻辑的声明式建模语言，其基于 SAT 的约束分析已用于配置合成、缺陷发现、测试生成和安全分析等任务。这些场景中的部分分析需要寻找最优解，例如网络配置问题希望得到允许最多数据包的最宽松配置，而不仅是任意有效配置。由于 Alloy 依赖 SAT，它无法直接指定和分析此类优化问题。论文提出 AlloyMax，旨在将最大满足引入关系规范，使用户能够在 Alloy 中表达并求解这类最优解问题。摘要未给出具体实现与实验评估细节。
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.
@inproceedings{paperbot6398,
title = {AlloyMax: bringing maximum satisfaction to relational specifications},
author = {Changjian Zhang and Ryan Wagner and Pedro Orvalho and David Garlan and Vasco Manquinho and Ruben Martins and Eunsuk Kang},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3468587}
}