# Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers

## TL;DR

This paper introduces a scalable method for distributed SAT solvers to produce proofs of unsatisfiability, enabling their use in critical applications.

## Contribution

A novel distributed algorithm for composing linear unsatisfiability proofs from multiple sequential solvers is introduced.

## Key findings

- A sequential algorithm for proof composition is described and validated.
- A distributed proof composition algorithm is shown to be more scalable and general than prior approaches.
- Empirical results show proof composition and checking can occur within around 3× the solving time.

## Abstract

Distributed clause-sharing SAT solvers can solve challenging problems hundreds of times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which limits their use in critical applications. In this work, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. We first describe a simple sequential algorithm and then present a fully distributed algorithm for proof composition, which is substantially more scalable and general than prior works. Our empirical evaluation with over 1500 solver threads shows that our distributed approach allows proof composition and checking within around 3\documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$$\times $$\end{document}× its own (highly competitive) solving time.