E-Thesis 435 views 879 downloads
The combinatorics of minimal unsatisfiability: connecting to graph theory / HODA ABBASIZANJANI
Swansea University Author: HODA ABBASIZANJANI
DOI (Published version): 10.23889/SUthesis.57815
Abstract
Minimally Unsatisfiable CNFs (MUs) are unsatisfiable CNFs where removing any clause destroys unsatisfiability. MUs are the building blocks of unsatisfia-bility, and our understanding of them can be very helpful in answering various algorithmic and structural questions relating to unsatisfiability. In thi...
| Published: |
Swansea
2021
|
|---|---|
| Institution: | Swansea University |
| Degree level: | Doctoral |
| Degree name: | Ph.D |
| Supervisor: | Kullmann, Oliver ; Beckmann, Arnold |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa57815 |
| first_indexed |
2021-09-08T15:38:54Z |
|---|---|
| last_indexed |
2021-09-09T03:21:19Z |
| id |
cronfa57815 |
| recordtype |
RisThesis |
| fullrecord |
<?xml version="1.0"?><rfc1807><datestamp>2021-09-08T16:58:00.1015746</datestamp><bib-version>v2</bib-version><id>57815</id><entry>2021-09-08</entry><title>The combinatorics of minimal unsatisfiability: connecting to graph theory</title><swanseaauthors><author><sid>678d753c3d556c287deb03888b279f7e</sid><firstname>HODA</firstname><surname>ABBASIZANJANI</surname><name>HODA ABBASIZANJANI</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2021-09-08</date><abstract>Minimally Unsatisfiable CNFs (MUs) are unsatisfiable CNFs where removing any clause destroys unsatisfiability. MUs are the building blocks of unsatisfia-bility, and our understanding of them can be very helpful in answering various algorithmic and structural questions relating to unsatisfiability. In this thesis we study MUs from a combinatorial point of view, with the aim of extending the understanding of the structure of MUs. We show that some important classes of MUs are very closely related to known classes of digraphs, and using arguments from logic and graph theory we characterise these MUs.Two main concepts in this thesis are isomorphism of CNFs and the implica-tion digraph of 2-CNFs (at most two literals per disjunction). Isomorphism of CNFs involves renaming the variables, and flipping the literals. The implication digraph of a 2-CNF F has both arcs (¬a → b) and (¬b → a) for every binary clause (a ∨ b) in F .In the first part we introduce a novel connection between MUs and Minimal Strong Digraphs (MSDs), strongly connected digraphs, where removing any arc destroys the strong connectedness. We introduce the new class DFM of special MUs, which are in close correspondence to MSDs. The known relation between 2-CNFs and implication digraphs is used, but in a simpler and more direct way, namely that we have a canonical choice of one of the two arcs. As an application of this new framework we provide short and intuitive new proofs for two im-portant but isolated characterisations for nonsingular MUs (every literal occurs at least twice), both with ingenious but complicated proofs: Characterising 2-MUs (minimally unsatisfiable 2-CNFs), and characterising MUs with deficiency 2 (two more clauses than variables).In the second part, we provide a fundamental addition to the study of 2-CNFs which have efficient algorithms for many interesting problems, namely that we provide a full classification of 2-MUs and a polytime isomorphism de-cision of this class. We show that implication digraphs of 2-MUs are “Weak Double Cycles” (WDCs), big cycles of small cycles (with possible overlaps). Combining logical and graph-theoretical methods, we prove that WDCs have at most one skew-symmetry (a self-inverse fixed-point free anti-symmetry, re-versing the direction of arcs). It follows that the isomorphisms between 2-MUs are exactly the isomorphisms between their implication digraphs (since digraphs with given skew-symmetry are the same as 2-CNFs). This reduces the classifi-cation of 2-MUs to the classification of a nice class of digraphs.Finally in the outlook we discuss further applications, including an alter-native framework for enumerating some special Minimally Unsatisfiable Sub-clause-sets (MUSs).</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>8</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2021</publishedYear><publishedDate>2021-09-08</publishedDate><doi>10.23889/SUthesis.57815</doi><url/><notes>ORCiD identifier https://orcid.org/0000-0002-9575-4758</notes><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Kullmann, Oliver ; Beckmann, Arnold</supervisor><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><apcterm/><lastEdited>2021-09-08T16:58:00.1015746</lastEdited><Created>2021-09-08T16:37:00.5004882</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>HODA</firstname><surname>ABBASIZANJANI</surname><order>1</order></author></authors><documents><document><filename>57815__20794__e99b8a0d9d2347ae9e0044f9a6c4b934.pdf</filename><originalFilename>Abbasizanjani_Hoda_PhD_Thesis_Final_Redacted_Signature.pdf</originalFilename><uploaded>2021-09-08T16:55:51.4490598</uploaded><type>Output</type><contentLength>1080880</contentLength><contentType>application/pdf</contentType><version>E-Thesis – open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The author, Hoda Abbasizanjani, 2021.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807> |
| spelling |
2021-09-08T16:58:00.1015746 v2 57815 2021-09-08 The combinatorics of minimal unsatisfiability: connecting to graph theory 678d753c3d556c287deb03888b279f7e HODA ABBASIZANJANI HODA ABBASIZANJANI true false 2021-09-08 Minimally Unsatisfiable CNFs (MUs) are unsatisfiable CNFs where removing any clause destroys unsatisfiability. MUs are the building blocks of unsatisfia-bility, and our understanding of them can be very helpful in answering various algorithmic and structural questions relating to unsatisfiability. In this thesis we study MUs from a combinatorial point of view, with the aim of extending the understanding of the structure of MUs. We show that some important classes of MUs are very closely related to known classes of digraphs, and using arguments from logic and graph theory we characterise these MUs.Two main concepts in this thesis are isomorphism of CNFs and the implica-tion digraph of 2-CNFs (at most two literals per disjunction). Isomorphism of CNFs involves renaming the variables, and flipping the literals. The implication digraph of a 2-CNF F has both arcs (¬a → b) and (¬b → a) for every binary clause (a ∨ b) in F .In the first part we introduce a novel connection between MUs and Minimal Strong Digraphs (MSDs), strongly connected digraphs, where removing any arc destroys the strong connectedness. We introduce the new class DFM of special MUs, which are in close correspondence to MSDs. The known relation between 2-CNFs and implication digraphs is used, but in a simpler and more direct way, namely that we have a canonical choice of one of the two arcs. As an application of this new framework we provide short and intuitive new proofs for two im-portant but isolated characterisations for nonsingular MUs (every literal occurs at least twice), both with ingenious but complicated proofs: Characterising 2-MUs (minimally unsatisfiable 2-CNFs), and characterising MUs with deficiency 2 (two more clauses than variables).In the second part, we provide a fundamental addition to the study of 2-CNFs which have efficient algorithms for many interesting problems, namely that we provide a full classification of 2-MUs and a polytime isomorphism de-cision of this class. We show that implication digraphs of 2-MUs are “Weak Double Cycles” (WDCs), big cycles of small cycles (with possible overlaps). Combining logical and graph-theoretical methods, we prove that WDCs have at most one skew-symmetry (a self-inverse fixed-point free anti-symmetry, re-versing the direction of arcs). It follows that the isomorphisms between 2-MUs are exactly the isomorphisms between their implication digraphs (since digraphs with given skew-symmetry are the same as 2-CNFs). This reduces the classifi-cation of 2-MUs to the classification of a nice class of digraphs.Finally in the outlook we discuss further applications, including an alter-native framework for enumerating some special Minimally Unsatisfiable Sub-clause-sets (MUSs). E-Thesis Swansea 8 9 2021 2021-09-08 10.23889/SUthesis.57815 ORCiD identifier https://orcid.org/0000-0002-9575-4758 COLLEGE NANME COLLEGE CODE Swansea University Kullmann, Oliver ; Beckmann, Arnold Doctoral Ph.D 2021-09-08T16:58:00.1015746 2021-09-08T16:37:00.5004882 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science HODA ABBASIZANJANI 1 57815__20794__e99b8a0d9d2347ae9e0044f9a6c4b934.pdf Abbasizanjani_Hoda_PhD_Thesis_Final_Redacted_Signature.pdf 2021-09-08T16:55:51.4490598 Output 1080880 application/pdf E-Thesis – open access true Copyright: The author, Hoda Abbasizanjani, 2021. true eng |
| title |
The combinatorics of minimal unsatisfiability: connecting to graph theory |
| spellingShingle |
The combinatorics of minimal unsatisfiability: connecting to graph theory HODA ABBASIZANJANI |
| title_short |
The combinatorics of minimal unsatisfiability: connecting to graph theory |
| title_full |
The combinatorics of minimal unsatisfiability: connecting to graph theory |
| title_fullStr |
The combinatorics of minimal unsatisfiability: connecting to graph theory |
| title_full_unstemmed |
The combinatorics of minimal unsatisfiability: connecting to graph theory |
| title_sort |
The combinatorics of minimal unsatisfiability: connecting to graph theory |
| author_id_str_mv |
678d753c3d556c287deb03888b279f7e |
| author_id_fullname_str_mv |
678d753c3d556c287deb03888b279f7e_***_HODA ABBASIZANJANI |
| author |
HODA ABBASIZANJANI |
| author2 |
HODA ABBASIZANJANI |
| format |
E-Thesis |
| publishDate |
2021 |
| institution |
Swansea University |
| doi_str_mv |
10.23889/SUthesis.57815 |
| 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 |
| document_store_str |
1 |
| active_str |
0 |
| description |
Minimally Unsatisfiable CNFs (MUs) are unsatisfiable CNFs where removing any clause destroys unsatisfiability. MUs are the building blocks of unsatisfia-bility, and our understanding of them can be very helpful in answering various algorithmic and structural questions relating to unsatisfiability. In this thesis we study MUs from a combinatorial point of view, with the aim of extending the understanding of the structure of MUs. We show that some important classes of MUs are very closely related to known classes of digraphs, and using arguments from logic and graph theory we characterise these MUs.Two main concepts in this thesis are isomorphism of CNFs and the implica-tion digraph of 2-CNFs (at most two literals per disjunction). Isomorphism of CNFs involves renaming the variables, and flipping the literals. The implication digraph of a 2-CNF F has both arcs (¬a → b) and (¬b → a) for every binary clause (a ∨ b) in F .In the first part we introduce a novel connection between MUs and Minimal Strong Digraphs (MSDs), strongly connected digraphs, where removing any arc destroys the strong connectedness. We introduce the new class DFM of special MUs, which are in close correspondence to MSDs. The known relation between 2-CNFs and implication digraphs is used, but in a simpler and more direct way, namely that we have a canonical choice of one of the two arcs. As an application of this new framework we provide short and intuitive new proofs for two im-portant but isolated characterisations for nonsingular MUs (every literal occurs at least twice), both with ingenious but complicated proofs: Characterising 2-MUs (minimally unsatisfiable 2-CNFs), and characterising MUs with deficiency 2 (two more clauses than variables).In the second part, we provide a fundamental addition to the study of 2-CNFs which have efficient algorithms for many interesting problems, namely that we provide a full classification of 2-MUs and a polytime isomorphism de-cision of this class. We show that implication digraphs of 2-MUs are “Weak Double Cycles” (WDCs), big cycles of small cycles (with possible overlaps). Combining logical and graph-theoretical methods, we prove that WDCs have at most one skew-symmetry (a self-inverse fixed-point free anti-symmetry, re-versing the direction of arcs). It follows that the isomorphisms between 2-MUs are exactly the isomorphisms between their implication digraphs (since digraphs with given skew-symmetry are the same as 2-CNFs). This reduces the classifi-cation of 2-MUs to the classification of a nice class of digraphs.Finally in the outlook we discuss further applications, including an alter-native framework for enumerating some special Minimally Unsatisfiable Sub-clause-sets (MUSs). |
| published_date |
2021-09-08T04:58:29Z |
| _version_ |
1860880469272297472 |
| score |
11.100184 |