Preprocessing for DQBF
Preprocessing for DQBF
复制标题
DQBF 的预处理
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Bernd Becker
中科院分区：
文献类型：
--
作者：
Ralf Wimmer;Karina Gitina;Jennifer Nist;Christopher H. Scholl;Bernd Becker
对于 SAT 和 QBF 公式，在将公式传递到实际求解算法之前，应用了许多技术来减少/修改公式的变量和子句的数量。众所周知，这些预处理技术通常可以将求解器的计算时间减少几个数量级。在本文中，我们将 SAT 和 QBF 问题的不同预处理技术推广到依赖量化布尔公式 (DQBF)，并描述它们需要如何适应 DQBF 求解器核心。我们证明了它们对于基于 CNF 和非 CNF 的 DQBF 算法的有效性。
For SAT and QBF formulas many techniques are applied in order to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. It is well known that these preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper we generalize different preprocessing techniques for SAT and QBF problems to dependency quantified Boolean formulas (DQBF) and describe how they need to be adapted to work with a DQBF solver core. We demonstrate their effectiveness both for CNF- and non-CNF-based DQBF algorithms.
DOI：
10.1007/s10817-008-9114-5
发表时间：
2009-01-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Samer, Marko;Szeider, Stefan
通讯作者：
Szeider, Stefan
通过量词消除求解 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