Skolem Functions for DQBF
Skolem Functions for DQBF
复制标题
DQBF 的 Skolem 函数
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
B. Becker
中科院分区：
文献类型：
--
作者：
K. Wimmer;Ralf Wimmer;Christoph Scholl;B. Becker
我们考虑计算 Skolem 函数以满足依赖量化布尔公式 (DQBF) 的问题。我们展示了如何从基于消除的 DQBF 求解器获得 Skolem 函数以及如何考虑预处理步骤。 Skolem 函数的大小通过使用 Craig 插值和重写技术的无关最小化来优化。使用我们的 DQBF 求解器 HQS 进行的实验表明，与单纯求解公式相比，我们能够以很少的开销有效地计算 Skolem 函数。
We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don’t-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
通过量词消除求解 DQBF
DOI：
10.7873/date.2015.0098
发表时间：
2015
期刊：
2015 Design, Automation & Test in Europe Conference & Exhibition (DATE)
影响因子：
--
作者：
K. Gitina;R. Wimmer;S. Reimer;M. Sauer;C. Scholl;B. Becker
通讯作者：
B. Becker