# The complete set of minimal simple graphs that support unsatisfiable 2-CNFs

## TL;DR

This paper characterizes exactly which simple graphs can support unsatisfiable reduced 2-CNF formulas, identifying four small graphs as key topological minors that determine satisfiability.

## Contribution

It provides a complete characterization of graphs supporting unsatisfiable 2-CNF sentences using topological minors, extending understanding of the structure of such formulas.

## Key findings

- A reduced 2-CNF is supported on a simple graph if and only if it contains one of four specific minors.
- All satisfiable 2-CNF formulas supported on a graph exclude subdivisions of these four minors.
- The characterization leverages topological minors, not minors, and discusses limitations of the Robertson-Seymour theorem.

## Abstract

A propositional logic sentence in conjunctive normal form that has clauses of length two (a 2-CNF) can be associated with a multigraph in which the vertices correspond to the variables and edges to clauses. We first show that every such sentence that has been reduced, that is, which is unchanged under application of certain tautologies, is equisatisfiable to a 2-CNF whose associated multigraph is, in fact, a simple graph. Our main result is a complete characterization of graphs that can support unsatisfiable 2-CNF sentences. We show that a simple graph can support an unsatisfiable reduced 2-CNF sentence if and only if it contains any one of four specific small graphs as a topological minor. Equivalently, all reduced 2-CNF sentences supported on a given simple graph are satisfiable if and only if all subdivisions of those four graphs are forbidden as subgraphs of of the original graph. We conclude with a discussion of why the Robertson-Seymour graph minor theorem does not apply in our approach.