Several effective preprocessing techniques for Boolean formulas with and without quantifiers use unit propagation to simplify the formula. Among these techniques are vivification, unit propagation look-ahead (UPLA), and the identification of redundant clauses as so-called quantified resolution asymmetric tautologies (QRAT). For quantified Boolean formulas (QBFs), these techniques have been extended to allow the application of universal reduction during unit propagation, which makes the techniques more effective. In this paper, we prove that the generalization of QBF to dependency quantified Boolean formulas (DQBFs) also allows the application of universal reduction during these preprocessing techniques.

翻译：针对含与不含量词的布尔公式，多种有效的预处理技术均采用子句传播以简化公式。这些技术包括活化技术、子句传播前瞻（UPLA）以及识别冗余子句的所谓量词消解非对称重言式（QRAT）。对于量词布尔公式（QBF），上述技术已扩展至允许在子句传播过程中应用全称归约，从而提升技术有效性。本文证明，将QBF推广至依赖量词布尔公式（DQBF）时，这些预处理技术同样允许在子句传播中应用全称归约。