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 条
[41]   OMEGA(N LOG N) LOWER BOUNDS ON LENGTH OF BOOLEAN-FORMULAS [J].
FISCHER, MJ ;
MEYER, AR ;
PATERSON, MS .
SIAM JOURNAL ON COMPUTING, 1982, 11 (03) :416-427
[42]   A Model for Generating Random Quantified Boolean Formulas [J].
Chen, Hubie ;
Interian, Yannet .
19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, :66-71
[43]   A dichotomy theorem for learning quantified boolean formulas [J].
Dalmau, V .
MACHINE LEARNING, 1999, 35 (03) :207-224
[44]   SIZE-DEPTH TRADEOFF IN NON-MONOTONE BOOLEAN-FORMULAS [J].
COMMENTZWALTER, B ;
SATTLER, J .
ACTA INFORMATICA, 1980, 14 (03) :257-269
[45]   AMPLIFICATION OF BOUNDED DEPTH MONOTONE READ-ONCE BOOLEAN-FORMULAS [J].
GU, QP ;
MARUOKA, A .
SIAM JOURNAL ON COMPUTING, 1991, 20 (01) :41-55
[46]   BOUNDS ON THE REALIZATION COMPLEXITY OF BOOLEAN-FORMULAS BY TREE CIRCUITS OF TUNABLE MODULES [J].
ARTYUKHOV, VL ;
KOPEIKIN, GA ;
SHALYTO, AA .
AUTOMATION AND REMOTE CONTROL, 1981, 42 (11) :1532-1538
[47]   Propositional PSPACE reasoning with boolean programs versus quantified Boolean formulas [J].
Skelley, A .
AUTOMATA , LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2004, 3142 :1163-1175
[48]   A symbolic search based approach for quantified Boolean formulas [J].
Audemard, G ;
Saïs, L .
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 :16-30
[49]   Expressing default abduction problems as quantified Boolean formulas [J].
Tompits, H .
AI COMMUNICATIONS, 2003, 16 (02) :89-105
[50]   A multi-engine solver for quantified Boolean formulas [J].
Pulina, Luca ;
Tacchella, Armando .
PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING - CP 2007, 2007, 4741 :574-589
12345