Quantifier Shifting for Quantified Boolean Formulas Revisited

被引：1
作者：
Heisinger, Simone [1 ]
Heisinger, Maximilian [1 ]
Rebola-Pardo, Adrian [1 ,2 ]
Seidl, Martina [1 ]
机构：
[1] JKU Linz, Inst Symbol Artificial Intelligence, Linz, Austria
[2] TU Vienna, Inst Log & Computat, Vienna, Austria
来源：
AUTOMATED REASONING, IJCAR 2024, PT I | 2024年 / 14739卷
关键词：
Quantified Boolean Formulas; Prenexing; Normal Form Transformation; QBF; SOLVER;
D O I：
10.1007/978-3-031-63498-7_20
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Modern solvers for quantified Boolean formulas (QBFs) process formulas in prenex form, which divides each QBF into two parts: the quantifier prefix and the propositional matrix. While this representation does not cover the full language of QBF, every non-prenex formula can be transformed to an equivalent formula in prenex form. This transformation offers several degrees of freedom and blurs structural information that might be useful for the solvers. In a case study conducted 20 years back, it has been shown that the applied transformation strategy heavily impacts solving time. We revisit this work and investigate how sensitive recent QBF solvers perform w.r.t. various prenexing strategies.
引用
收藏
页码：325 / 343
页数：19
相关论文
共 31 条
[1]  
Beyersdorff O, 2021, FRONT ARTIF INTEL AP, P1177, DOI 10.3233/FAIA201015
[2]   Reasons for Hardness in QBF Proof Systems [J].
Beyersdorff, Olaf ;
Hinde, Luke ;
Pich, Jan .
ACM TRANSACTIONS ON COMPUTATION THEORY, 2020, 12 (02)
[3]  
Biere A, 2011, LECT NOTES ARTIF INT, V6803, P101, DOI 10.1007/978-3-642-22438-6_10
[4]  
Charwat G., 2016, SAT, P27
[5]  
Charwat G., 2016, BDD-based dynamic programming on tree decompositions
[6]  
Egly U, 2004, LECT NOTES COMPUT SC, V2919, P214
[7]  
Egly U, 2006, FRONT ARTIF INTEL AP, V141, P477
[8]  
Goultiaeva A, 2010, LECT NOTES COMPUT SC, V6175, P333, DOI 10.1007/978-3-642-14186-7_29
[9]   Solving QBF by Abstraction [J].
Hecking-Harbusch, Jesko ;
Tentrup, Leander .
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (277) :88-102
[10]  
Heisinger M., 2024, LNCS, V14739, P315, DOI [10.1007/978-3- 031- 63498- 7_19, DOI 10.1007/978-3-031-63498-7_19]
1234