Files in this item
Files | Description | Format |
---|---|---|
application/pdf ![]() | (no description provided) |
Description
Title: | Graphical structure of unsatisfiable boolean formulae |
Author(s): | Karve, Vaibhav |
Director of Research: | Hirani, Anil N |
Doctoral Committee Chair(s): | Dunfield, Nathan M |
Doctoral Committee Member(s): | Baryshnikov, Yuliy; Tserunyan, Anush |
Department / Program: | Mathematics |
Discipline: | Mathematics |
Degree Granting Institution: | University of Illinois at Urbana-Champaign |
Degree: | Ph.D. |
Genre: | Dissertation |
Subject(s): | boolean satisfiability
satisfiability graph theory logic graphs hypergraphs python graphsat kSAT 3SAT NP-complete |
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. |
Issue Date: | 2021-04-21 |
Type: | Thesis |
URI: | http://hdl.handle.net/2142/110504 |
Rights Information: | Copyright 2021 Vaibhav Karve |
Date Available in IDEALS: | 2021-09-17 |
Date Deposited: | 2021-05 |
This item appears in the following Collection(s)
-
Dissertations and Theses - Mathematics
-
Graduate Dissertations and Theses at Illinois
Graduate Theses and Dissertations at Illinois