通过定义提取的认证式 DQBF 求解
计算机科学中的逻辑
2021-06-07 v1
摘要
我们提出一种新的依赖量化布尔公式（DQBF）判定过程，该过程使用基于插值的定义提取，在反例引导归纳综合（CEGIS）循环中计算 Skolem 函数。在每次迭代中，使用 SAT 求解器测试一组候选 Skolem 函数的正确性，该求解器要么确定一个模型已被找到，要么返回全称变量的一个赋值作为反例。修复一个反例通常涉及更改具有不可比较依赖集的多个存在变量候选。我们的过程引入辅助变量——我们称之为仲裁变量——每个变量表示存在变量在其依赖集的特定赋值下的值。可能的修复被表示为关于这些变量的子句，并调用 SAT 求解器来寻找一个能处理所有先前所见反例的赋值。添加仲裁变量定义了 Skolem 函数在先前未定义赋值处的值，并可能在后续迭代中通过定义提取检测到 Skolem 函数。所提过程的一个关键特性是其天生可认证：对于真 DQBF，可以以最小开销返回模型。面向假公式的认证，我们证明可以在基于展开的 DQBF 证明系统中推导子句。在标准基准集上的实验评估中，一个实现能够匹配（并在某些情况下超越）最先进 DQBF 求解器的性能。此外，对于所有已求解的真实例，均可生成并验证模型。
引用
@article{arxiv.2106.02550,
title = {Certified DQBF Solving by Definition Extraction},
author = {Franz-Xaver Reichl and Friedrich Slivovsky and Stefan Szeider},
journal= {arXiv preprint arXiv:2106.02550},
year = {2021}
}