Modern software for propositional satisfiability problems gives a powerful automated reasoning toolkit, capable of outputting not only a satisfiable/unsatisfiable signal but also a justification of unsatisfiability in the form of resolution proof (or a more expressive proof), which is commonly used for verification purposes. Empirically, modern SAT solvers produce relatively short proofs, however, there are no inherent guarantees that these proofs cannot be significantly reduced. This paper proposes a novel branch-and-bound algorithm for finding the shortest resolution proofs; to this end, we introduce a layer list representation of proofs that groups clauses by their level of indirection. As we show, this representation breaks all permutational symmetries, thereby improving upon the state-of-the-art symmetry-breaking and informing the design of a novel workflow for proof minimization. In addition to that, we design pruning procedures that reason on proof length lower bound, clause subsumption, and dominance. Our experiments suggest that the proofs from state-of-the-art solvers could be shortened by 30-60% on the instances from SAT Competition 2002 and by 25-50% on small synthetic formulas. When treated as an algorithm for finding the shortest proof, our approach solves twice as many instances as the previous work based on SAT solving and reduces the time to optimality by orders of magnitude for the instances solved by both approaches.

翻译：现代命题可满足性问题软件提供了强大的自动推理工具包，不仅能够输出可满足/不可满足的判断信号，还能以归结证明（或更具表达力的证明）形式提供不可满足性的论证依据，这类证明通常用于验证目的。经验表明，现代SAT求解器生成的证明相对较短，但无法保证这些证明无法被进一步显著压缩。本文提出了一种新颖的分支定界算法，用于寻找最短的归结证明；为此，我们引入了一种按间接程度对子句进行分层的证明层表表示法。如我们所示，该表示法能够打破所有置换对称性，从而改进了现有最先进的对称性破缺技术，并为证明最小化的新型工作流程设计提供了依据。此外，我们设计了基于证明长度下界、子句包含关系和支配关系的剪枝程序。实验结果表明，在SAT Competition 2002的实例上，当前最先进求解器生成的证明可缩短30-60%；在小型合成公式上可缩短25-50%。若将本方法视为寻找最短证明的算法，其可求解的实例数量是基于SAT求解的先前工作的两倍，且在双方均可求解的实例上，将达到最优解的时间缩短了数个数量级。