@inproceedings{594fb5028cb74805812c1943cda4416c,
title = "Compositional Propositional Proofs",
abstract = "Many hard-combinatorial problems have only be solved by SAT solvers in a massively parallel setting. This reduces the trust one has in the final result as errors might occur during parallel SAT solving or during partitioning of the original problem. We present a new framework to produce clausal proofs for cube-and-conquer, arguably the most effective parallel SAT solving paradigm for hard-combinatorial problems. The framework also provides an elegant approach to parallelize the validation of clausal proofs efficiently, both in terms of run time and memory usage. We evaluate the presented approach on some hard-combinatorial problems and validate constructed clausal proofs in parallel.",
author = "Marijn Heule and Armin Biere",
year = "2015",
doi = "10.1007/978-3-662-48899-7\_31",
language = "English",
isbn = "9783662488980",
volume = "9450",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "444--459",
editor = "Andrei Voronkov and Ansgar Fehnker and Martin Davis and Annabelle McIver",
booktitle = "Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015",
}