Abstraction-Based Algorithm for 2QBF

被引：0

作者：

Janota, Mikolas ^{[2
]}

Marques-Silva, Joao ^{[1
,2
]}

机构：

[1] Univ Coll Dublin, Dublin, Ireland

[2] INESC ID, Lisbon, Portugal

来源：

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2011 | 2011年 / 6695卷

关键词：

MODEL CHECKING; REFINEMENT;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Quantified Boolean Formulas (QBFs) enable standard representation of PSPACE problems. In particular, formulas with two quantifier levels (2QBFs) enable representing problems in the second level of the polynomial hierarchy (Pi(P)(2), Sigma(P)(2)). This paper proposes an algorithm for solving 2QBF satisfiability by counterexample guided abstraction refinement (CEGAR). This represents an alternative approach to 2QBF satisfiability and, by extension, to solving decision problems in the second level of polynomial hierarchy. In addition, the paper presents a comparison of a prototype implementing the presented algorithm to state of the art QBF solvers, showing that a larger set of instances is solved.

引用

页码：230 / 244

页数：15

共 50 条

[1] 2QBF: Challenges and Solutions
Balabanov, Valeriy
Jiang, Jie-Hong Roland
Scholl, Christoph
Mishchenko, Alan
Brayton, Robert K.
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016, 2016, 9710 : 453 - 469
[2] Understanding and Extending Incremental Determinization for 2QBF
Rabe, Markus N.
Tentrup, Leander
Rasmussen, Cameron
Seshia, Sanjit A.
COMPUTER AIDED VERIFICATION, CAV 2018, PT II, 2018, 10982 : 256 - 274
[3] A Generator of Hard 2QBF Formulas and ASP Programs
Amendola, Giovanni
Ricca, Francesco
Truszczynski, Miroslaw
SIXTEENTH INTERNATIONAL CONFERENCE ON PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2018, : 52 - 56
[4] ABSTRACTION-BASED REUSE REPOSITORIES
CAMPBELL, GH
AIAA COMPUTERS IN AEROSPACE VII CONFERENCE, PTS 1 AND 2: A COLLECTION OF PAPERS, 1989, : 368 - 373
[5] Single-solver algorithms for 2QBF (Poster presentation)
Bayless, Sam
Hu, Alan J.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2012, 7317 LNCS : 487 - 488
[6] ABSTRACTION-BASED SOFTWARE-DEVELOPMENT
HAGER, J
COMMUNICATIONS OF THE ACM, 1986, 29 (11) : 1027 - 1027
[7] Data Cleaning: An Abstraction-based Approach
Koshley, Dileep Kumar
Halder, Raju
2015 INTERNATIONAL CONFERENCE ON ADVANCES IN COMPUTING, COMMUNICATIONS AND INFORMATICS (ICACCI), 2015, : 713 - 719
[8] Resilient Abstraction-Based Controller Design
Samuel, Stanly
Mallik, Kaushik
Schmuck, Anne-Kathrin
Neider, Daniel
2020 59TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2020, : 2123 - 2129
[9] Abstraction-based Action Ordering in Planning
Fox, Maria
Long, Derek
Porteous, Julie
19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, : 1220 - 1225
[10] Abstraction-Based Performance Verification of NoCs
Holcomb, Daniel
Brady, Bryan
Seshia, Sanjit
PROCEEDINGS OF THE 48TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2011, : 492 - 497

← 1 2 3 4 5 →