Logic seminar

QBF Solving and Calculi, Overview

Mikolas Janota

CIIRC

Monday, 23. November 2020 - 15:30 to 17:00

Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284

Quantified Boolean Formulas (QBFs) enrich the SAT problem with quantifiers taking the problem from NP to PSPACE. Recent years have seen a number of novel approaches to QBF solving. At the same time, QBF calculi were developed to match the solvers. However, there are calculi with no solving counterparts.

In this talk I will overview the two prominent paradigms in QBF solving: conflict-driven and expansion-based. I will also discuss the connection between solving and the existing proof systems as well as challenges for future research.

In this talk I will overview the two prominent paradigms in QBF solving: conflict-driven and expansion-based. I will also discuss the connection between solving and the existing proof systems as well as challenges for future research.