Message passing for quantified Boolean formulas

TL;DR

This paper presents two message passing algorithms for quantified Boolean formulas, improving unsatisfiability proofs and guiding branching heuristics, leading to significant efficiency gains and solving previously unsolved benchmarks.

Contribution

Introduction of message passing heuristics for QBF that prove unsatisfiability and enhance solver efficiency, with demonstrated empirical improvements.

Findings

Robust exponential efficiency gain on random QBFs

Successfully solved previously unsolved benchmarks

Insights into message passing applications in small systems

Abstract

We introduce two types of message passing algorithms for quantified Boolean formulas (QBF). The first type is a message passing based heuristics that can prove unsatisfiability of the QBF by assigning the universal variables in such a way that the remaining formula is unsatisfiable. In the second type, we use message passing to guide branching heuristics of a Davis-Putnam Logemann-Loveland (DPLL) complete solver. Numerical experiments show that on random QBFs our branching heuristics gives robust exponential efficiency gain with respect to the state-of-art solvers. We also manage to solve some previously unsolved benchmarks from the QBFLIB library. Apart from this our study sheds light on using message passing in small systems and as subroutines in complete solvers.