Talks
Spring 2021

On CDCL vs. Resolution in QBF

Thursday, June 16th, 2022, 2:00 pm3:00 pm

Add to Calendar

Speaker: 

Olaf Beyersdorff (Friedrich-Schiller University of Jena)

Location: 

Calvin Lab Room 116

The quantified version QCDCL of CDCL is one of the main approaches to solve quantified Boolean formulas (QBF). While CDCL is known to be tightly captured by propositional resolution, we show that QCDCL and Q-Resolution are exponentially incomparable. We also explore different versions of QCDCL and compare their strength. Technically we use develop lower bound techniques that are effective for QBF resolution systems as well as for QCDCL. The talk is based on a series of papers with Benjamin Böhm and Tomas Peitl, which appeared at ITCS’21, SAT’21, SAT’22, IJCAI’22.

AttachmentSize
PDF icon Slides607.57 KB