一句话：为 core-guided OLL MaxSAT 求解器提出首个原生证明日志框架，形式化推理规则并实现可自动检验的最优性证书。
MaxSAT 求解器正日益成为软件工程工具的后端，但其结果一直缺乏可自动检验的最优性证书：SAT 求解器可输出 (不)可满足性的 DRAT 证明，而 MaxSAT 还必须额外证明不存在代价更低的解。现有方法要么只覆盖孤立的求解范式，要么把 MaxSAT 推理归约为重量级的伪布尔（pseudo-Boolean）证明，导致验证开销过大而不实用。本文提出首个针对 core-guided OLL 求解器的 MaxSAT 专用证明日志框架，为 core、clique、hardening、totalizer 更新与 bound 调整等推理形式化原生推理规则，并在 EvalMaxSAT 中实现人类可读日志与紧凑的二进制 DAG 日志两种形式。在 2024 年 MaxSAT 竞赛数据集上的评估证实了该认证流水线的实用性与可扩展性，为可信赖的求解器使用铺平了道路。
MaxSAT solvers are increasingly used as back-ends in software engineering tools. Yet their results have lacked automatically checkable certificates of optimality. While SAT solvers emit DRAT proofs of (un)satisfiability, MaxSAT must additionally prove that no lower-cost solution exists. Existing approaches either cover only isolated solving paradigms or re-duce MaxSAT reasoning to heavyweight pseudo-Boolean proofs, yielding impractical verification overhead.We present the first MaxSAT-specific proof-logging framework for core-guided OLL solvers. We formalize native inference rules for cores, cliques, hardenings, totalizer updates, and bound adjustments, and implement both a human-readable logger and a compact binary DAG logger in EvalMaxSAT. Evaluation on the 2024 MaxSAT competition dataset confirm the practicality and scalability of our certification pipeline, paving the way for trustworthy, solver use.
DOI 原文 ·
@inproceedings{paperbot9386,
title = {Efficient and Verifiable Proof Logging for MaxSAT Solving},
author = {Raoul Van Doren and Timos Antonopoulos and Ruzica Piskac},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00113}
}