Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović

TL;DR

A novel branch-and-bound algorithm for finding the shortest resolution proofs is proposed and a layer list representation of proofs that groups clauses by their level of indirection is introduced, thereby improving upon the state-of-the-art symmetry-breaking and informing the design of a novel workflow for proof minimization.

Abstract

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.

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

TL;DR

A novel branch-and-bound algorithm for finding the shortest resolution proofs is proposed and a layer list representation of proofs that groups clauses by their level of indirection is introduced, thereby improving upon the state-of-the-art symmetry-breaking and informing the design of a novel workflow for proof minimization.

Abstract

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.

Paper Structure

This paper contains 26 sections, 14 theorems, 21 equations, 16 figures, 8 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Propositional Satisfiability
  4. Resolution Proof System
  5. Related Work
  6. Proof Minimization
  7. Layer List Representation
  8. Branch-and-bound Search, High-level Description
  9. Subproblem Partitioning
  10. Frontier Pruning
  11. Pruning by Dominance
  12. Lower Bounding the Proof Length with UNSAT Clause Subsets
  13. Experimental Evaluation
  14. Algorithm Configuration
  15. Dataset Description
  16. ...and 11 more sections

Key Result

Theorem 1

The resolution rule is sound in the sense that any model satisfying clauses $A$ and $B$ also satisfies the resolvent clause $A \diamond B$, and is Robinson1965-jAcm in the sense that an empty clause can be derived from a formula if and only if it is UNSAT.

Figures (16)

  • Figure 1: CaDiCaL proof length comparison against the shortest proofs on random unsatisfiable 3-CNFs.
  • Figure 2: Two DAG encodings of the proof from Example \ref{['example:more-symmetries']} using the same vertices but different edges. Every row on both figures corresponds to one layer.
  • Figure 3: A subproblem compatible with the proof in Figure \ref{['fig:more-symmetries-dag-top']}; the second-to-last layer of the proof is a superset of the next set $\mathtt{Next}[\mathcal{P}]$ of the subproblem.
  • Figure 4: Subproblems that cover all the compatible proofs of the subproblem in Figure \ref{['fig:subproblem']}.
  • Figure 5: The frontier of the known set after deriving $\{ x, t \}$ in Figure \ref{['fig:branching-y']}; frontier clauses are highlighted with dark background and light text.
  • ...and 11 more figures

Theorems & Definitions (37)

  • Definition 1
  • Theorem 1
  • Definition 2
  • Example 1
  • Definition 3
  • Proposition 1
  • Example 2
  • Definition 4
  • Example 3
  • Definition 5
  • ...and 27 more