sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
复制标题
sQueezeBF：基于等价推理的 QBF 有效预处理器
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Massimo Narizzano
中科院分区：
文献类型：
--
作者：
E. Giunchiglia;Paolo Marin;Massimo Narizzano
在本文中，我们提出sQueezeBF，一个有效的预处理器QBF，结合各种技术，消除变量和/或冗余的条款。特别是sQueezeBF结合了（i）通过Q-解析的变量消除，（ii）通过等价替换的变量消除和（iii）通过等价重写的等价破坏。实验分析表明，sQueezeBF可以产生显着减少的条款和/或变量的数量-的点，一些实例直接解决sQueezeBF -它可以显着提高效率的一系列国家的最先进的QBF求解器-的点，一些实例不能解决没有sQueezeBF预处理。
In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination via Q-resolution, (ii) variable elimination via equivalence substitution and (iii) equivalence breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables - up to the point that some instances are solved directly by sQueezeBF - and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers - up to the point that some instances cannot be solved without sQueezeBF preprocessing.