“Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers” by Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, and Clark Barrett. In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 84-88.
With the increasing availability of parallel computing power, there is a growing focus on parallelizing algorithms for important automated reasoning problems such as Boolean satisfiability (SAT). Divide-and-Conquer (D&C) is a popular parallel SAT solving paradigm that partitions SAT instances into independent sub-problems which are then solved in parallel. For unsatisfiable instances, state-of-the-art D&C solvers generate DRAT refutations for each sub-problem. However, they do not generate a single refutation for the original instance. To close this gap, we present Proof-Stitch, a procedure for combining refutations of different sub-problems into a single refutation for the original instance. We prove the correctness of the procedure and propose optimizations to reduce the size and checking time of the combined refutations by invoking existing trimming tools in the proof-combination process. We also provide an extensible implementation of the proposed technique. Experiments on instances from last year's SAT competition show that the optimized refutations are checkable up to seven times faster than unoptimized refutations.
BibTeX entry:
@inproceedings{NCW+22,
author = {Abhishek Nair and Saranyu Chattopadhyay and Haoze Wu and Alex
Ozdemir and Clark Barrett},
editor = {Alberto Griggio and Neha Rungta},
title = {Proof-Stitch: Proof Combination for Divide-and-Conquer {SAT}
Solvers},
booktitle = {Proceedings of the {\it 22^{nd}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '22)},
pages = {84--88},
publisher = {TU Wien Academic Press},
month = oct,
year = {2022},
doi = {10.34727/2022/isbn.978-3-85448-053-2_14},
url = {http://theory.stanford.edu/~barrett/pubs/NCW+22.pdf}
}
(This webpage was created with bibtex2web.)