{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/110504"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/110504","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Graphical structure of unsatisfiable boolean formulae","abstract":"The presented research is an introduction and analysis of a novel graph decision problem called GraphSAT. Using the tools of topology and graph theory, this new variant builds upon the classical logic and computer science problem of boolean satisfiability k-SAT. k-SAT asks if there exists a truth assignment that satisfies a given boolean formula. Our variant deals with multi-hypergraphs instead of boolean formulae and uses truth assignments on vertices instead of variables. This graph-theoretic picture helps us explore and exploit patterns in unsatisfiable instances of k-SAT, which in turn helps us identify minimal obstruction sets to graph satisfiability. Historically, k-SAT (for k≥3) was the first problem that was proven to be NP-complete, independently by Cook and Levin, making it central to the study of algorithms and computational complexity. We shed new light on k-SAT by analyzing GraphSAT. We demonstrate that 2-GraphSAT is in complexity class P and has a finite obstruction set containing four simple graphs. Further, our exploration of 3-GraphSAT gives rise to the local graph rewriting theorem, which leverages the fact that taking a union over all possible vertex-assignments preserves the satisfiability status of a graph. Using this theorem, we generate a list of graph reduction rules and an incomplete list of obstructions to satisfiability of looped-multi-hypergraphs. A part of this research, especially the search for unsatisfiable instances of GraphSAT, was carried out using computational tools. Hence, some results are aided by a Python package specifically written to carry out computations on multi-hypergraph instances and implement the local rewriting algorithm. These computational steps are included in the thesis in the form of code blocks to give a glimpse of the back-end.","abstract_html":"The presented research is an introduction and analysis of a novel graph decision problem called GraphSAT. Using the tools of topology and graph theory, this new variant builds upon the classical logic and computer science problem of boolean satisfiability k-SAT. k-SAT asks if there exists a truth assignment that satisfies a given boolean formula. Our variant deals with multi-hypergraphs instead of boolean formulae and uses truth assignments on vertices instead of variables. This graph-theoretic picture helps us explore and exploit patterns in unsatisfiable instances of k-SAT, which in turn helps us identify minimal obstruction sets to graph satisfiability. Historically, k-SAT (for k≥3) was the first problem that was proven to be NP-complete, independently by Cook and Levin, making it central to the study of algorithms and computational complexity. We shed new light on k-SAT by analyzing GraphSAT. We demonstrate that 2-GraphSAT is in complexity class P and has a finite obstruction set containing four simple graphs. Further, our exploration of 3-GraphSAT gives rise to the local graph rewriting theorem, which leverages the fact that taking a union over all possible vertex-assignments preserves the satisfiability status of a graph. Using this theorem, we generate a list of graph reduction rules and an incomplete list of obstructions to satisfiability of looped-multi-hypergraphs. A part of this research, especially the search for unsatisfiable instances of GraphSAT, was carried out using computational tools. Hence, some results are aided by a Python package specifically written to carry out computations on multi-hypergraph instances and implement the local rewriting algorithm. These computational steps are included in the thesis in the form of code blocks to give a glimpse of the back-end.","abstract_has_math":false,"creators":["Karve, Vaibhav"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Mathematics","degree_department":null,"school":null,"contributors":["Hirani, Anil N","Dunfield, Nathan M","Baryshnikov, Yuliy","Tserunyan, Anush"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2021,"date_issued":"2021-09-17T01:11:03Z","date_published":"2021-09-17T01:11:03Z","updated_at":"2026-07-22T22:24:50Z","subjects":["boolean satisfiability","satisfiability","graph theory","logic","graphs","hypergraphs","python","graphsat","kSAT","3SAT","NP-complete"],"languages":["en"],"rights":["Copyright 2021 Vaibhav Karve"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/110504","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Hirani, Anil N","Dunfield, Nathan M","Baryshnikov, Yuliy","Tserunyan, Anush"]},{"key":"dc:creator","label":"Author","values":["Karve, Vaibhav"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2021-09-17T01:11:03Z","2021-04-21","2021-05"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Mathematics"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["boolean satisfiability","satisfiability","graph theory","logic","graphs","hypergraphs","python","graphsat","kSAT","3SAT","NP-complete"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2021 Vaibhav Karve"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/110504"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["The presented research is an introduction and analysis of a novel graph decision problem called GraphSAT. Using the tools of topology and graph theory, this new variant builds upon the classical logic and computer science problem of boolean satisfiability k-SAT. k-SAT asks if there exists a truth assignment that satisfies a given boolean formula. Our variant deals with multi-hypergraphs instead of boolean formulae and uses truth assignments on vertices instead of variables. This graph-theoretic picture helps us explore and exploit patterns in unsatisfiable instances of k-SAT, which in turn helps us identify minimal obstruction sets to graph satisfiability. Historically, k-SAT (for k≥3) was the first problem that was proven to be NP-complete, independently by Cook and Levin, making it central to the study of algorithms and computational complexity. We shed new light on k-SAT by analyzing GraphSAT. We demonstrate that 2-GraphSAT is in complexity class P and has a finite obstruction set containing four simple graphs. Further, our exploration of 3-GraphSAT gives rise to the local graph rewriting theorem, which leverages the fact that taking a union over all possible vertex-assignments preserves the satisfiability status of a graph. Using this theorem, we generate a list of graph reduction rules and an incomplete list of obstructions to satisfiability of looped-multi-hypergraphs. A part of this research, especially the search for unsatisfiable instances of GraphSAT, was carried out using computational tools. Hence, some results are aided by a Python package specifically written to carry out computations on multi-hypergraph instances and implement the local rewriting algorithm. These computational steps are included in the thesis in the form of code blocks to give a glimpse of the back-end.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2021-09-16 without embargo terms","The student, Vaibhav Karve, accepted the attached license on 2021-04-19 at 12:29.","The student, Vaibhav Karve, submitted this Dissertation for approval on 2021-04-19 at 13:01.","This Dissertation was approved for publication on 2021-04-21 at 10:21.","DSpace SAF Submission Ingestion Package generated from Vireo submission #16409 on 2021-09-16 at 16:43:08","Made available in DSpace on 2021-09-17T01:11:03Z (GMT). No. of bitstreams: 4 KARVE-DISSERTATION-2021.pdf: 9548194 bytes, checksum: be505880f31211583e873c0772b17d49 (MD5) source_files_20210421.zip: 18063704 bytes, checksum: b930551d4c9551dadc4b0133be2b18fa (MD5) LICENSE.txt: 4210 bytes, checksum: fe2a663fa37ec3596b25bead87928c42 (MD5) PROQUEST_LICENSE.txt: 4556 bytes, checksum: 7713e547ad45e88896976607b80a7732 (MD5) Previous issue date: 2021-04-21"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Graphical structure of unsatisfiable boolean formulae"]}]}],"canonical_facts":{"dc:contributor":["Hirani, Anil N","Dunfield, Nathan M","Baryshnikov, Yuliy","Tserunyan, Anush"],"dc:creator":["Karve, Vaibhav"],"dc:date":["2021-09-17T01:11:03Z","2021-04-21","2021-05"],"dc:description":["The presented research is an introduction and analysis of a novel graph decision problem called GraphSAT. Using the tools of topology and graph theory, this new variant builds upon the classical logic and computer science problem of boolean satisfiability k-SAT. k-SAT asks if there exists a truth assignment that satisfies a given boolean formula. Our variant deals with multi-hypergraphs instead of boolean formulae and uses truth assignments on vertices instead of variables. This graph-theoretic picture helps us explore and exploit patterns in unsatisfiable instances of k-SAT, which in turn helps us identify minimal obstruction sets to graph satisfiability. Historically, k-SAT (for k≥3) was the first problem that was proven to be NP-complete, independently by Cook and Levin, making it central to the study of algorithms and computational complexity. We shed new light on k-SAT by analyzing GraphSAT. We demonstrate that 2-GraphSAT is in complexity class P and has a finite obstruction set containing four simple graphs. Further, our exploration of 3-GraphSAT gives rise to the local graph rewriting theorem, which leverages the fact that taking a union over all possible vertex-assignments preserves the satisfiability status of a graph. Using this theorem, we generate a list of graph reduction rules and an incomplete list of obstructions to satisfiability of looped-multi-hypergraphs. A part of this research, especially the search for unsatisfiable instances of GraphSAT, was carried out using computational tools. Hence, some results are aided by a Python package specifically written to carry out computations on multi-hypergraph instances and implement the local rewriting algorithm. These computational steps are included in the thesis in the form of code blocks to give a glimpse of the back-end.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2021-09-16 without embargo terms","The student, Vaibhav Karve, accepted the attached license on 2021-04-19 at 12:29.","The student, Vaibhav Karve, submitted this Dissertation for approval on 2021-04-19 at 13:01.","This Dissertation was approved for publication on 2021-04-21 at 10:21.","DSpace SAF Submission Ingestion Package generated from Vireo submission #16409 on 2021-09-16 at 16:43:08","Made available in DSpace on 2021-09-17T01:11:03Z (GMT). No. of bitstreams: 4 KARVE-DISSERTATION-2021.pdf: 9548194 bytes, checksum: be505880f31211583e873c0772b17d49 (MD5) source_files_20210421.zip: 18063704 bytes, checksum: b930551d4c9551dadc4b0133be2b18fa (MD5) LICENSE.txt: 4210 bytes, checksum: fe2a663fa37ec3596b25bead87928c42 (MD5) PROQUEST_LICENSE.txt: 4556 bytes, checksum: 7713e547ad45e88896976607b80a7732 (MD5) Previous issue date: 2021-04-21"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/110504"],"dc:language":["en"],"dc:rights":["Copyright 2021 Vaibhav Karve"],"dc:subject":["boolean satisfiability","satisfiability","graph theory","logic","graphs","hypergraphs","python","graphsat","kSAT","3SAT","NP-complete"],"dc:title":["Graphical structure of unsatisfiable boolean formulae"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Mathematics"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:50Z"}