## Abstract

A propositional logic sentence in conjunctive normal form that has clauses of length at most two (a 2-CNF) can be associated with a multigraph in which the vertices correspond to the variables and edges to clauses. We show that every 2-CNF that has been reduced under the 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 the original graph.

Original language | English (US) |
---|---|

Pages (from-to) | 123-132 |

Number of pages | 10 |

Journal | Discrete Applied Mathematics |

Volume | 283 |

DOIs | |

State | Published - Sep 15 2020 |

## Keywords

- Boolean satisfiability
- Conjunctive normal form
- Edge contraction
- Graph minors
- Propositional logic
- Subdivision
- Topological minors

## ASJC Scopus subject areas

- Discrete Mathematics and Combinatorics
- Applied Mathematics