一句话：提出将最优 CHC 求解的最优性检查归约到终止性分析，并用约束合成终止论证来实现。
本文研究最优 CHC 求解，即计算约束 Horn 子句的最大解和/或最小解，其动机包括最大规约推断等开放程序推理。已有优化方法通常迭代改进解，因此判定给定解是否最优是关键。作者从计算理论角度分析最优性检查问题，发现其与程序终止性分析密切相关：理论上澄清了现有方法的局限和另一方法的错误，实践上可将终止性分析技术用于 CHC 解的最优性检查。文中提出基于约束合成的终止性论证生成方法，实现工具并在编码最大规约合成问题的 CHC 上评估，取得有希望的结果。
Motivated by applications to open program reasoning such as maximal specification inference, this paper studiesoptimal CHC solving, a problem to compute maximal and/or minimal solutions of constrained Horn clauses (CHCs). This problem and its subproblems have been studied in the literature, and a major approach is to iteratively improve a solution of CHCs until it becomes optimal. So a key ingredient of optimization methods is the optimality checking of a given solution. We propose a novel optimality checking method, as well as an optimization method using the proposed optimality checker, based on a computational theoretical analysis of the optimality checking problem. The key observation is that the optimality checking problem is closely related to the termination analysis of programs, and this observation is useful both theoretically and practically. From a theoretical perspective, it clarifies a limitation of an existing method and incorrectness of another method in the literature. From a practical perspective, it allows us to apply techniques of termination analysis to the optimality checking of a solution of CHCs. We present an optimality checking method based on constraint-based synthesis of termination arguments, implemented our method, evaluated it on CHCs that encode maximal specification synthesis problems, and obtained promising results.