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

Vaibhav Karve, Anil N. Hirani

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)123-132
Number of pages10
JournalDiscrete Applied Mathematics
Volume283
DOIs
StatePublished - 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

Fingerprint Dive into the research topics of 'The complete set of minimal simple graphs that support unsatisfiable 2-CNFs'. Together they form a unique fingerprint.

  • Cite this