在 DQBF 预处理中使用单元传播与全称约简
计算机科学中的逻辑
2023-03-28 v1
摘要
若干针对带量词与不带量词的布尔公式的有效预处理技术使用单元传播来简化公式。这些技术包括活化（vivification）、单元传播前瞻（UPLA），以及将冗余子句识别为所谓的量化分辨非对称重言式（QRAT）。对于量化布尔公式（QBFs），这些技术已被扩展以允许在单元传播期间应用全称约简，从而使技术更加有效。在本文中，我们证明将 QBF 推广到依赖量化布尔公式（DQBFs）同样允许在这些预处理技术中应用全称约简。
引用
@article{arxiv.2303.14446,
title = {Using Unit Propagation with Universal Reduction in DQBF Preprocessing},
author = {Ralf Wimmer and Ming-Yi Hu},
journal= {arXiv preprint arXiv:2303.14446},
year = {2023}
}