No Cover Image

Book chapter 571 views 76 downloads

Transforming Quantified Boolean Formulas Using Biclique Covers

Oliver Kullmann Orcid Logo, Ankit Shukla

Tools and Algorithms for the Construction and Analysis of Systems, Pages: 372 - 390

Swansea University Author: Oliver Kullmann Orcid Logo

  • 62220.pdf

    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)

Check full text

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-...

Full description

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!
first_indexed 2023-01-12T12:03:37Z
last_indexed 2023-01-13T19:23:32Z
id cronfa62220
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>62220</id><entry>2022-12-29</entry><title>Transforming Quantified Boolean Formulas Using Biclique Covers</title><swanseaauthors><author><sid>2b410f26f9324d6b06c2b98f67362d05</sid><ORCID>0000-0003-3021-0095</ORCID><firstname>Oliver</firstname><surname>Kullmann</surname><name>Oliver Kullmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2022-12-29</date><deptcode>SCS</deptcode><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.</abstract><type>Book chapter</type><journal>Tools and Algorithms for the Construction and Analysis of Systems</journal><volume/><journalNumber/><paginationStart>372</paginationStart><paginationEnd>390</paginationEnd><publisher>Springer Nature Switzerland</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783031308192</isbnPrint><isbnElectronic>9783031308208</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>QBF solving, DQBF. 2QCNF, biclique cover problem, conflict graph, preprocessing Horn clause-sets, minimal unsatisfiability</keywords><publishedDay>1</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-01-01</publishedDate><doi>10.1007/978-3-031-30820-8_23</doi><url>http://dx.doi.org/10.1007/978-3-031-30820-8_23</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm>Other</apcterm><funders>O. Kullmann—Supported by EPSRC grant EP/S015523/1.</funders><projectreference/><lastEdited>2023-06-01T12:08:01.5577342</lastEdited><Created>2022-12-29T10:52:52.9573384</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>1</order></author><author><firstname>Ankit</firstname><surname>Shukla</surname><order>2</order></author></authors><documents><document><filename>62220__27581__ff5631754ff84a4c87c96db85bdad2db.pdf</filename><originalFilename>62220.pdf</originalFilename><uploaded>2023-05-23T15:04:06.8539635</uploaded><type>Output</type><contentLength>1281716</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>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</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs><OutputDur><Id>149</Id><IsDataAvailableOnline>true</IsDataAvailableOnline><DataNotAvailableOnlineReasonId xsi:nil="true"/><DurUrl>to be added</DurUrl><IsDurRestrictions>false</IsDurRestrictions><DurRestrictionReasonId xsi:nil="true"/><DurEmbargoDate xsi:nil="true"/></OutputDur></OutputDurs></rfc1807>
spelling v2 62220 2022-12-29 Transforming Quantified Boolean Formulas Using Biclique Covers 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2022-12-29 SCS 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. Book chapter Tools and Algorithms for the Construction and Analysis of Systems 372 390 Springer Nature Switzerland Cham 9783031308192 9783031308208 0302-9743 1611-3349 QBF solving, DQBF. 2QCNF, biclique cover problem, conflict graph, preprocessing Horn clause-sets, minimal unsatisfiability 1 1 2023 2023-01-01 10.1007/978-3-031-30820-8_23 http://dx.doi.org/10.1007/978-3-031-30820-8_23 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University Other O. Kullmann—Supported by EPSRC grant EP/S015523/1. 2023-06-01T12:08:01.5577342 2022-12-29T10:52:52.9573384 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Oliver Kullmann 0000-0003-3021-0095 1 Ankit Shukla 2 62220__27581__ff5631754ff84a4c87c96db85bdad2db.pdf 62220.pdf 2023-05-23T15:04:06.8539635 Output 1281716 application/pdf Version of Record true 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 true eng http://creativecommons.org/licenses/by/4.0/ 149 true to be added false
title Transforming Quantified Boolean Formulas Using Biclique Covers
spellingShingle Transforming Quantified Boolean Formulas Using Biclique Covers
Oliver Kullmann
title_short Transforming Quantified Boolean Formulas Using Biclique Covers
title_full Transforming Quantified Boolean Formulas Using Biclique Covers
title_fullStr Transforming Quantified Boolean Formulas Using Biclique Covers
title_full_unstemmed Transforming Quantified Boolean Formulas Using Biclique Covers
title_sort Transforming Quantified Boolean Formulas Using Biclique Covers
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Oliver Kullmann
Ankit Shukla
format Book chapter
container_title Tools and Algorithms for the Construction and Analysis of Systems
container_start_page 372
publishDate 2023
institution Swansea University
isbn 9783031308192
9783031308208
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-031-30820-8_23
publisher Springer Nature Switzerland
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://dx.doi.org/10.1007/978-3-031-30820-8_23
document_store_str 1
active_str 0
description 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.
published_date 2023-01-01T12:08:00Z
_version_ 1767498245004591104
score 11.035634

Similar Items