首次为多目标最大可满足性提供可验证的证明机制，确保求解结果可信。
Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
- 利用VeriPB预序关系构造多目标优化解的验证证明
- 在不修改格式的前提下实现非支配解集的帕累托最优认证
- 实测表明证明生成开销合理，适用于主流求解器
由于自动化推理广泛应用于正确系统的设计与分析，推理引擎的结果必须可靠。对于布尔可满足性（SAT）求解器——以及近期基于SAT的最大可满足性（MaxSAT）求解器——通过集成证明日志实现可信性，使求解器能够生成机器可验证的证明以确认推理步骤的正确性。本文首次为多目标最大可满足性（MO-MaxSAT）优化技术引入基于VeriPB证明格式的证明日志。尽管VeriPB不直接支持多目标问题，我们详述如何利用其预序关系，为计算非支配解集中每个元素的帕累托最优解提供证书，且无需扩展VeriPB格式或证明检查器。通过将VeriPB证明日志集成到最先进的多目标MaxSAT求解器中，我们实证表明该证明机制在多目标最大可满足性上具有可扩展性，且开销合理。
原文摘要 · Abstract (English)
Due to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For Boolean satisfiability (SAT) solvers - and more recently SAT-based maximum satisfiability (MaxSAT) solvers - trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed. In this work, we enable for the first time proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. Although VeriPB does not offer direct support for multi-objective problems, we detail how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto-optimality, without extending the VeriPB format or the proof checker. By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。