Marijn Heule, Armin Biere,
"Compositional Propositional Proofs"
: Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015, Serie Lecture Notes in Computer Science (LNCS), Vol. 9450, Springer, Seite(n) 444-459, 2015
Compositional Propositional Proofs
Sprache des Titels:
Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015
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.