The Connectivity of Boolean Satisfiability: Computational and Structural Dichotomies

TL;DR

This paper explores the structural and computational properties of solution spaces in Boolean satisfiability problems, establishing clear dichotomies that distinguish between tractable and intractable cases based on graph connectivity and structure.

Contribution

It introduces new dichotomy theorems for the complexity of connectivity questions and characterizes the structural properties of solution subgraphs in Boolean satisfiability.

Findings

Intractable cases are PSPACE-complete with exponential diameter solutions.

Tractable cases have polynomial-time algorithms for connectivity and linear diameter.

Structural properties of solution subgraphs differ significantly between tractable and intractable cases.

Abstract

Boolean satisfiability problems are an important benchmark for questions about complexity, algorithms, heuristics and threshold phenomena. Recent work on heuristics, and the satisfiability threshold has centered around the structure and connectivity of the solution space. Motivated by this work, we study structural and connectivity-related properties of the space of solutions of Boolean satisfiability problems and establish various dichotomies in Schaefer's framework. On the structural side, we obtain dichotomies for the kinds of subgraphs of the hypercube that can be induced by the solutions of Boolean formulas, as well as for the diameter of the connected components of the solution space. On the computational side, we establish dichotomy theorems for the complexity of the connectivity and st-connectivity questions for the graph of solutions of Boolean formulas. Our results assert that the intractable side of the computational dichotomies is PSPACE-complete, while the tractable side - which includes but is not limited to all problems with polynomial time algorithms for satisfiability - is in P for the st-connectivity question, and in coNP for the connectivity question. The diameter of components can be exponential for the PSPACE-complete cases, whereas in all other cases it is linear; thus, small diameter and tractability of the connectivity problems are remarkably aligned. The crux of our results is an expressibility theorem showing that in the tractable cases, the subgraphs induced by the solution space possess certain good structural properties, whereas in the intractable cases, the subgraphs can be arbitrary.