Blocked literals are universal

Abstract

We recently introduced a new proof system for Quantified Boolean Formulas (QBF), called QRAT, that opened up a variety of new preprocessing techniques. This paper presents a concept that follows from the QRAT proof system: blocked literals. Blocked literals are redundant universal literals that can be removed or added to clauses. We show that blocked literal elimination (BLE) and blocked literal addition are not confluent.We implemented BLE in the state-of-the-art preprocessor bloqqer. Our experimental results illustrate that the BLE extension improves solver performance on the 2014 QBF evaluation benchmarks.