Simple minimally unsatisfiable subsets of 2-CNFs

TL;DR

This paper investigates minimal unsatisfiable subsets of 2-CNF formulas, providing recognition algorithms, complexity results, and polynomial-time methods for specific MUS types, advancing understanding of their computational landscape.

Contribution

It introduces a linear-time recognition procedure for 2-MUs, extends NP-completeness results, and offers polynomial algorithms for MUSs with unit-clauses, deepening the analysis of 2-CNF MUS complexity.

Findings

Linear-time recognition of 2-MUs

NP-completeness of deficiency-1 MUS decision

Polynomial-time algorithms for MUSs with unit-clauses

Abstract

We present a study of minimal unsatisfiable subsets (MUSs) of 2-CNF Boolean formulas, building on the Abbasizanjani-Kullmann classification of minimally unsatisfiable 2-CNFs (2-MUs). We start by giving a linear-time procedure for recognising 2-MUs. Then we study the problem of finding one simple MUS. On the one hand we extend the results by Kleine Buening et al, which showed NP-completeness of the decision, whether a deficiency-1 MUS exists. On the other hand we show that deciding/finding an MUS containing one or two unit-clauses (which are special deficiency-1 MUSs) can be done in polynomial time. Finally we present an incremental polynomial time algorithm for some special type of MUSs, namely those MUSs containing at least one unit-clause. We conclude by discussing the main open problem, developing a deeper understanding of the landscape of easy/hard MUSs of 2-CNFs.