期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2020
卷号：2020
页码：1-26
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：Dependency quantified Boolean formulas (DQBF) describe an NEXPTIME-complete generalisation of QBF, which in turn generalises SAT. DQBF solving is an emerging field with further applications in, among others, incomplete circuit design. QRAT is a recently proposed proof system for quantified Boolean formulas (QBF), which simulates the full suite of QBF preprocessing techniques and thus forms a uniform proof checking format for solver verification. In this work, we study QRAT in the more general DQBF context, obtaining a sound and complete refutational DQBF proof system that we call DQRAT. We show that DQRAT can simulate the full suite of dedicated DQBF preprocessing techniques, except those relying on defined variables, which we cover with the introduction of a new form of prefix modification. Our work enables generalisations of further QBF preprocessing techniques (e.g. blocked literal elimination) that were not previously considered for DQBF.
