ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework

Abstract

In recent years, automated reasoning is increasingly relying on parallelization techniques such as Divide-and-Conquer approaches to improve performance. In this context, generating certificates for independently verifying solver results is challenging, since decomposition into subtasks complicates the use of existing proof techniques. Nevertheless, certificates are essential for ensuring correctness and trust in automated reasoning tools. In this paper, we present ParaProofa, the—to the best of our knowledge—first certifying parallel framework for quantified Boolean formulas (QBF). To this end, we extend ParaQooba, a Cube-and-Conquer-based parallel QBF solver to emit proofs of the subproblems that were solved to obtain the value of the input QBF. ParaProofa constructs a complete proof for the result of the input QBF which can be independently checked.