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 条

[21] On Unordered BDDs and Quantified Boolean Formulas
Janota, Mikolas
PROGRESS IN ARTIFICIAL INTELLIGENCE, PT II, 2019, 11805 : 501 - 507
[22] Equivalence models for quantified Boolean formulas
Büning, HK
Zhao, XS
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2005, 3542 : 224 - 234
[23] Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas
Pulina, Luca
Tacchella, Armando
FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2009, 5749 : 350 - 365
[24] Looking algebraically at tractable quantified Boolean formulas
Chen, HB
Dalmau, V
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2005, 3542 : 71 - 79
[25] Computing Smallest MUSes of Quantified Boolean Formulas
Niskanen, Andreas
Mustonen, Jere
Berg, Jeremias
Jarvisalo, Matti
LOGIC PROGRAMMING AND NONMONOTONIC REASONING, LPNMR 2022, 2022, 13416 : 301 - 314
[26] Abstract Solvers for Quantified Boolean Formulas and their Applications
Brochenin, Remi
Maratea, Marco
AI*IA 2015: ADVANCES IN ARTIFICIAL INTELLIGENCE, 2015, 9336 : 205 - 217
[27] A Structural Approach to Reasoning with Quantified Boolean Formulas
Pulina, Luca
Tacchella, Armando
21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, : 596 - 602
[28] Extracting Certificates from Quantified Boolean Formulas
Benedetti, Marco
19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, : 47 - 53
[29] Moving Definition Variables in Quantified Boolean Formulas
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
[30] QuBIS: An (In)complete Solver for Quantified Boolean Formulas
Pulina, Luca
Tacchella, Armando
MICAI 2008: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2008, 5317 : 34 - 43

← 1 2 3 4 5 →