QRAT Proofs for QBF Preprocessing

Description

For the practical evaluation of quantified Boolean formulas (QBFs) an additional preprocessing step is beneficial in many cases. The application of a preprocessor, however, prevented the extraction of proofs for the original formula. Such proofs are required to independently validate correctness of the preprocessor’s rewritings and the solver’s result. To address this issue, we introduced the QRAT proof system. With QRAT it is possible to capture all state-of-the-art preprocessing techniques in a uniform manner and to check the result of a preprocessor efficiently.

Period	02 Feb 2017
Event title	Helmut Veith Memorial Workshop
Event type	Conference
Location	AustriaShow on map