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 条

[31] Quantifier Shifting for Quantified Boolean Formulas Revisited
Heisinger, Simone
Heisinger, Maximilian
Rebola-Pardo, Adrian
Seidl, Martina
AUTOMATED REASONING, IJCAR 2024, PT I, 2024, 14739 : 325 - 343
[32] A Model for Generating Random Quantified Boolean Formulas
Chen, Hubie
Interian, Yannet
19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, : 66 - 71
[33] Propositional PSPACE reasoning with boolean programs versus quantified Boolean formulas
Skelley, A
AUTOMATA , LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2004, 3142 : 1163 - 1175
[34] A symbolic search based approach for quantified Boolean formulas
Audemard, G
Saïs, L
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 : 16 - 30
[35] Expressing default abduction problems as quantified Boolean formulas
Tompits, H
AI COMMUNICATIONS, 2003, 16 (02) : 89 - 105
[36] A multi-engine solver for quantified Boolean formulas
Pulina, Luca
Tacchella, Armando
PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING - CP 2007, 2007, 4741 : 574 - 589
[37] Transforming Quantified Boolean Formulas Using Biclique Covers
Kullmann, Oliver
Shukla, Ankit
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023, 2023, 13994 : 372 - 390
[38] Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas
Egly, Uwe
Woltran, Stefan
COMPUTATIONAL MODELS OF ARGUMENT, 2006, 144 : 133 - 144
[39] Multiplication Complexity Optimization based on Quantified Boolean Formulas
Zhu, Jun
Pan, Hongyang
Chu, Zhufei
2024 INTERNATIONAL SYMPOSIUM OF ELECTRONICS DESIGN AUTOMATION, ISEDA 2024, 2024, : 332 - 336
[40] SAT based BDD solver for Quantified Boolean Formulas
Audemard, G
Saïs, L
ICTAI 2004: 16TH IEEE INTERNATIONALCONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2004, : 82 - 89

← 1 2 3 4 5 →