Graphical structure of unsatisfiable boolean formulae

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Mathematics

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2021

Author dc:creator

• Karve, Vaibhav

Contributors dc:contributor

• Hirani, Anil N
• Dunfield, Nathan M
• Baryshnikov, Yuliy
• Tserunyan, Anush

• boolean satisfiability
• satisfiability
• graph theory
• logic
• graphs
• hypergraphs
• python
• graphsat
• kSAT
• 3SAT
• NP-complete

Statement dc:rights

• Copyright 2021 Vaibhav Karve

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/110504

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/110504