How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization

要約

命題充足可能性問題用の最新のソフトウェアは、充足可能/充足不能信号だけでなく、検証目的で一般的に使用される解決証明 (またはより表現力豊かな証明) の形式で充足不可能性の正当化も出力できる、強力な自動推論ツールキットを提供します。
。
経験的に、最新の SAT ソルバーは比較的短い証明を生成しますが、これらの証明を大幅に短縮できないという本質的な保証はありません。
この論文では、最短解像度の証明を見つけるための新しい分岐限定アルゴリズムを提案します。
この目的のために、間接性のレベルによって節をグループ化する証明のレイヤー リスト表現を導入します。
私たちが示すように、この表現はすべての順列対称性を破り、それによって最先端の対称性の破りを改善し、証明の最小化のための新しいワークフローの設計に情報を与えます。
それに加えて、証明長の下限、節包含、および優越性に基づいて推論する枝刈り手順を設計します。
私たちの実験では、最先端のソルバーによる証明は、SAT Competition 2002 のインスタンスでは 30 ～ 60%、小さな合成公式では 25 ～ 50% 短縮できることが示唆されています。
最短の証明を見つけるためのアルゴリズムとして扱われる場合、私たちのアプローチは SAT 解決に基づく以前の研究の 2 倍のインスタンスを解決し、両方のアプローチで解決されたインスタンスの最適化までの時間を桁違いに短縮します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google