Clause/term resolution and learning in the evaluation of quantified boolean formulas

被引：0

作者：

Giunchiglia, Enrico ^{[1
]}

Narizzano, Massimo ^{[1
]}

Tacchella, Armando ^{[1
]}

机构：

[1] DIST, Università di Genova, Viale Causa 13, 16145 Genova, Italy

来源：

Journal of Artificial Intelligence Research | 2006年 / 26卷

关键词：

Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures; the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution; and goes on until the empty clause is generated or satisfiability of the set of clauses is proven; e.g; because no new clauses can be generated. In this paper; we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting; the above outlined deduction process is known to be sound and complete if given a formula in CNF and if a form of resolution; called Qresolution; is used. We introduce Q-resolution on terms; to be used for formulas in disjunctive normal form. We show that the computation performed by most of the available procedures for QBFs -based on the Davis-Logemann-Loveland procedure (DLL) for propositional satisfiability- corresponds to a tree in which Q-resolution on terms and clauses alternate. This poses the theoretical bases for the introduction of learning; corresponding to recording Q-resolution formulas associated with the nodes of the tree. We discuss the problems related to the introduction of learning in DLL based procedures; and present solutions extending state-of-the-art proposals coming from the literature on propositional satisfiability. Finally; we show that our DLL based solver extended with learning; performs significantly better on benchmarks used in the 2003 QBF solvers comparative evaluation. © 2006 AI Access Foundation. All rights reserved;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

Journal article (JA)

引用

页码：371 / 416

共 50 条

[41] Partial Witnesses from Preprocessed Quantified Boolean Formulas
Seidl, Martina
Koenighofer, Robert
2014 DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION (DATE), 2014,
[42] Comparing different prenexing strategies for quantified Boolean formulas
Egly, U
Seidl, M
Tompits, H
Woltran, S
Zolda, M
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 214 - 228
[43] A Duality-Aware Calculus for Quantified Boolean Formulas
Fazekas, Katalin
Seidl, Martina
Biere, Armin
PROCEEDINGS OF 2016 18TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC), 2016, : 181 - 186
[44] Short proofs for some symmetric Quantified Boolean Formulas
Kauers, Manuel
Seidl, Martina
INFORMATION PROCESSING LETTERS, 2018, 140 : 4 - 7
[45] Learning Boolean formulas
Kearns, Michael, 1600, ACM, New York, NY, United States (41):
[46] On computing belief change operations using quantified Boolean formulas
Delgrande, JP
Schaub, T
Tompits, H
Woltran, S
JOURNAL OF LOGIC AND COMPUTATION, 2004, 14 (06) : 801 - 826
[47] Primal and Dual Encoding from Applications into Quantified Boolean Formulas
Van Gelder, Allen
PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING, CP 2013, 2013, 8124 : 694 - 707
[48] Solving dependency quantified Boolean formulas using quantifier localization
Ge-Ernst, Aile
Scholl, Christoph
Sic, Juraj
Wimmer, Ralf
THEORETICAL COMPUTER SCIENCE, 2022, 925 : 1 - 24
[49] Solving advanced reasoning tasks using quantified Boolean formulas
Egly, U
Eiter, T
Tompits, H
Woltran, S
SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000), 2000, : 417 - 422
[50] An upper bound for the circuit complexity of existentially quantified Boolean formulas
Buening, H. Kleine
Remshagen, A.
THEORETICAL COMPUTER SCIENCE, 2010, 411 (31-33) : 2864 - 2870

← 1 2 3 4 5 →