Satisfiability of Acyclic and Almost Acyclic CNF Formulas

TL;DR

This paper identifies a polynomial-time solvable class of CNF formulas based on {eta}-acyclic hypergraphs and explores the complexity of nearly {eta}-acyclic formulas, revealing new hardness results and class comparisons.

Contribution

It introduces a new polynomial-time solvable class of CNF formulas using a special Davis-Putnam resolution and analyzes the complexity of formulas close to this class.

Findings

SAT for {eta}-acyclic formulas is polynomial-time solvable.

Testing membership in the extended class is NP-complete.

SAT parameterized by clique-width is W[1]-hard.

Abstract

We show that the Satisfiability (SAT) problem for CNF formulas with {\beta}-acyclic hypergraphs can be solved in polynomial time by using a special type of Davis-Putnam resolution in which each resolvent is a subset of a parent clause. We extend this class to CNF formulas for which this type of Davis-Putnam resolution still applies and show that testing membership in this class is NP-complete. We compare the class of {\beta}-acyclic formulas and this superclass with a number of known polynomial formula classes. We then study the parameterized complexity of SAT for "almost" {\beta}-acyclic instances, using as parameter the formula's distance from being {\beta}-acyclic. As distance we use the size of a smallest strong backdoor set and the {\beta}-hypertree width. As a by-product we obtain the W[1]-hardness of SAT parameterized by the (undirected) clique-width of the incidence graph, which disproves a conjecture by Fischer, Makowsky, and Ravve.