Alladi Ramakrishnan Hall

A study of QBF Merge Resolution and MaxSAT Resolution

Gaurav Sood

IMSc

We study two proof systems: (i) Merge Resolution for Quantified Boolean Formulas (QBFs), and (ii) MaxSAT Resolution for certifying unsatisfiability.

Merge Resolution (M-Res) was proposed as a proof system for QBFs by Beyersdorff et al. The main motivation was to overcome the limitations of another QBF proof system called LD-Q-Res. We show that M-Res has advantages over all standard resolution-based proof systems, it has disadvantages over some proof systems. Finally, and more crucially, we show that it is an unnatural proof system (i.e. not closed under restrictions). We believe this may make building good QBF solvers based on M-Res difficult.

MaxSAT Resolution (MaxRes) was proposed as a proof system for MaxSAT by Larrosa et al. and Bonet et al. We compare it with standard proof systems. We show that it has advantages over tree-like resolution. In devising a lower bound technique specific to MaxRes, we define a new semialgebraic proof system called the SubCubeSums proof system. We show that SubCubeSums lower bounds translate to MaxRes lower bounds. We then give a lower bound technique for it via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums.

(pre-synopsis seminar)