IMSc Webinar

Hard QBFs for Merge Resolution

Gaurav Sood

IMSc

Webinar: join at https://meet.google.com/oba-tuhi-yza The most successful SAT solvers are based on the proof system Resolution. Because of this success, Resolution has been adapted to get a variety of proof systems for Quantified Boolean Formulas (QBF). We study one such QBF proof system, called Merge Resolution; and prove the first non-trivial lower bounds for it. This is joint work with Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, and Tomáš Peitl.