Book chapter 571 views 76 downloads
Transforming Quantified Boolean Formulas Using Biclique Covers
,
Ankit Shukla
Tools and Algorithms for the Construction and Analysis of Systems, Pages: 372 - 390
Swansea University Author:
Oliver Kullmann
-
PDF | Version of Record
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter’s Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder
Download (1.22MB)
DOI (Published version): 10.1007/978-3-031-30820-8_23
Abstract
We introduce the global conflict graph of DQCNFs (dependency quantified conjunctive normal forms), recording clashes between clauses on such universal variables on which all existential variables depend (called “global variables”). The biclique covers of this graph correspond to the eligible clause-...
| Published in: | Tools and Algorithms for the Construction and Analysis of Systems |
|---|---|
| ISBN: | 9783031308192 9783031308208 |
| ISSN: | 0302-9743 1611-3349 |
| Published: |
Cham
Springer Nature Switzerland
2023
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa62220 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
We introduce the global conflict graph of DQCNFs (dependency quantified conjunctive normal forms), recording clashes between clauses on such universal variables on which all existential variables depend (called “global variables”). The biclique covers of this graph correspond to the eligible clause-slices of the DQCNF which consider only the global variables. We show that all such slices yield satisfiability-equivalent variations. This opens the possibility to realise this slice using as few global variables as possible. We give basic theoretical results and first supporting experimental data. |
|---|---|
| Keywords: |
QBF solving, DQBF. 2QCNF, biclique cover problem, conflict graph, preprocessing Horn clause-sets, minimal unsatisfiability |
| College: |
Faculty of Science and Engineering |
| Funders: |
O. Kullmann—Supported by EPSRC grant EP/S015523/1. |
| Start Page: |
372 |
| End Page: |
390 |