Graphical structure of unsatisfiable boolean formulae

Karve, Vaibhav

Permalink

https://hdl.handle.net/2142/110504 Copy

Description

Title

Graphical structure of unsatisfiable boolean formulae

Author(s)

Karve, Vaibhav

Issue Date

2021-04-21

Director of Research (if dissertation) or Advisor (if thesis)

Hirani, Anil N

Doctoral Committee Chair(s)

Dunfield, Nathan M

Committee Member(s)

• Baryshnikov, Yuliy
• Tserunyan, Anush

Department of Study

Mathematics

Discipline

Mathematics

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(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.

Graduation Semester

2021-05

Type of Resource

Thesis

Permalink

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

Copyright and License Information

Copyright 2021 Vaibhav Karve

Owning Collections