Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR18-025 | 1st February 2018 18:55

More on Size and Width in QBF Resolution


Authors: Olaf Beyersdorff, Judith Clymo
Publication: 5th February 2018 17:40
Downloads: 596


In their influential paper `Short proofs are narrow -- resolution made simple', Ben-Sasson and Wigderson introduced a crucial tool for proving lower bounds on the lengths of proofs in the resolution calculus. Over a decade later their technique for showing lower bounds on the size of proofs, by examining the width of all possible proofs, remains one of the most effective lower bound techniques in propositional proof complexity.

We continue the investigation into the application of this technique to proof systems for quantified Boolean formulas. We demonstrate a relationship between the size of proofs in level-ordered Q-Resolution and the width of proofs in Q-Resolution. In general, however, the picture is not positive, and for most stronger systems based on Q-Resolution, the size-width relation fails.

ISSN 1433-8092 | Imprint