Files in this item

FilesDescriptionFormat

application/pdf

application/pdfKARVE-DISSERTATION-2021.pdf (10MB)
(no description provided)PDF

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)

Item Statistics