RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS

被引：214
作者：
BUNING, HK [1 ]
KARPINSKI, M [1 ]
FLOGEL, A [1 ]
机构：
[1] UNIV BONN, INST INFORMAT, D-53012 BONN, GERMANY
来源：
INFORMATION AND COMPUTATION | 1995年 / 117卷 / 01期
关键词：
D O I：
10.1006/inco.1995.1025
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A complete and sound resolution operation directly applicable to the quantified Boolean formulas is presented. If we restrict the resolution to unit resolution, then the completeness and soundness for extended quantified Horn formulas is shown. We prove that the truth of a quantified Horn formula can be decided in O(rn) time, where n is the length of the formula and r is the number of universal variables, whereas in contrast the evaluation problem for extended quantified Horn formulas is coNP-complete for formulas with prefix For All There Exists. Further, we show that the resolution is exponential for extended quantified Horn formulas. (C) 1995 Academic Press, Inc.
引用
收藏
页码：12 / 18
页数：7
相关论文
共 50 条
[31]   RANDOM BOOLEAN-FORMULAS REPRESENTING ANY BOOLEAN FUNCTION WITH ASYMPTOTICALLY EQUAL PROBABILITY [J].
SAVICKY, P .
LECTURE NOTES IN COMPUTER SCIENCE, 1988, 324 :512-517
[32]   Computing Smallest MUSes of Quantified Boolean Formulas [J].
Niskanen, Andreas ;
Mustonen, Jere ;
Berg, Jeremias ;
Jarvisalo, Matti .
LOGIC PROGRAMMING AND NONMONOTONIC REASONING, LPNMR 2022, 2022, 13416 :301-314
[33]   A Dichotomy Theorem for Learning Quantified Boolean Formulas [J].
Víictor Dalmau .
Machine Learning, 1999, 35 :207-224
[34]   Looking algebraically at tractable quantified Boolean formulas [J].
Chen, HB ;
Dalmau, V .
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2005, 3542 :71-79
[35]   Abstract Solvers for Quantified Boolean Formulas and their Applications [J].
Brochenin, Remi ;
Maratea, Marco .
AI*IA 2015: ADVANCES IN ARTIFICIAL INTELLIGENCE, 2015, 9336 :205-217
[36]   A Structural Approach to Reasoning with Quantified Boolean Formulas [J].
Pulina, Luca ;
Tacchella, Armando .
21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, :596-602
[37]   Extracting Certificates from Quantified Boolean Formulas [J].
Benedetti, Marco .
19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, :47-53
[38]   Moving Definition Variables in Quantified Boolean Formulas [J].
Reeves, Joseph E. ;
Heule, Marijn J. H. ;
Bryant, Randal E. .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 :462-479
[39]   QuBIS: An (In)complete Solver for Quantified Boolean Formulas [J].
Pulina, Luca ;
Tacchella, Armando .
MICAI 2008: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2008, 5317 :34-43
[40]   Quantifier Shifting for Quantified Boolean Formulas Revisited [J].
Heisinger, Simone ;
Heisinger, Maximilian ;
Rebola-Pardo, Adrian ;
Seidl, Martina .
AUTOMATED REASONING, IJCAR 2024, PT I, 2024, 14739 :325-343
12345