arXiv:2611.14783 · v1

A Multi-Prover Interactive Protocol for Certification of Resolution Refutations

首次提交 2026-11-11 06:13

版本更新 2026-11-11 06:13

雷达观测 2026-11-13 10:09

摘要

A resolution refutation of a SAT-formula $\varphi$ is an independently checkable certificate proving that $\varphi$ is unsatisfiable. However, the refutations of $\varphi$ can be exponentially larger than $\varphi$. So, a verifier needs worst-case exponential time in the size of $\varphi$ to check their correctness. We present ResCertify, an interactive probabilistic protocol in which the verifier interacts with multiple independent, untrusted provers (MIP) to check the refutation with very low probability of error. The verifier runs in linear time in the size of $\varphi$. The provers require time $\mathcal{O}(n \cdot |Φ|)$, where $Φ$ is the resolution refutation and $n$ is the number of variables of $\varphi$. If they can be trusted to act as a multilinear oracle on certain queries, a single prover suffices, and the runtime can be improved to $\mathcal{O}(|Φ|)$. Finally, while the focus of our work is theoretical, we also report on a proof-of-concept implementation of ResCertify.

作者备注：33 pages, 7 figures, extended version to CSL 2027 version