Moving Definition Variables in Quantified Boolean Formulas
Moving Definition Variables in Quantified Boolean Formulas
复制标题
在量化布尔公式中移动定义变量
DOI：
10.1007/978-3-030-99524-9_26
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Bryant, Randal E.
中科院分区：
文献类型：
--
作者：
Reeves, Joseph E.;Heule, Marijn J.;Bryant, Randal E.
在带有定义变量的量化布尔公式中增加问题变量，可以实现子句形式的紧凑表示。一般来说，这些定义变量被放置在最里面的量词级别。为了恢复一些结构信息，我们引入了一种预处理技术，将定义变量移动到最接近定义它们的变量的量词级别。我们表达了QRAT证明系统中的运动，以允许独立的证明检查员进行验证。我们在QBFEVAL'20竞争基准上评估了定义变量的运动。运动显著提高了比赛的顶级求解器的性能。与单独使用Bloqqer相比，将变量移动与预处理器Bloqer相结合可以提高求解器的性能。
Augmenting problem variables in a quantified Boolean formula with definition variables enables a compact representation in clausal form. Generally these definition variables are placed in the innermost quantifier level. To restore some structural information, we introduce a preprocessing technique that moves definition variables to the quantifier level closest to the variables that define them. We express the movement in the QRAT proof system to allow verification by independent proof checkers. We evaluated definition variable movement on the QBFEVAL’20 competition benchmarks. Movement significantly improved performance for the competition’s top solvers. Combining variable movement with the preprocessorBloqqerimproves solver performance compared to usingBloqqeralone.
登录
查看更多内容
在检查子句证明时进行修剪
DOI：
10.1109/fmcad.2013.6679408
发表时间：
2013
期刊：
2013 Formal Methods in Computer-Aided Design
影响因子：
--
作者：
Marijn J. H. Heule;W. Hunt;Nathan Wetzler
通讯作者：
Nathan Wetzler
QBFRelay、QRATPre 和 DepQBF：增量预处理满足基于搜索的 QBF 求解
DOI：
--
发表时间：
2019
期刊：
Journal on Satisfiability, Boolean Modeling and Computation
影响因子：
--
作者：
Florian Lonsing
通讯作者：
Florian Lonsing
SAT 求解中门结构的识别和利用
DOI：
--
发表时间：
2020
期刊：
影响因子：
--
作者：
M. Iser
通讯作者：
M. Iser
DOI：
10.1007/s10817-019-09516-0
发表时间：
2020-03-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Heule, Marijn J. H.;Kiesl, Benjamin;Biere, Armin
通讯作者：
Biere, Armin
DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Basler G
通讯作者：
Basler G