Simple minimally unsatisfiable subsets of 2-CNFs
This work addresses computational complexity issues in automated reasoning and constraint satisfaction for researchers and practitioners, but it is incremental as it builds on prior classifications and results.
The paper tackles the problem of finding minimal unsatisfiable subsets (MUSs) in 2-CNF Boolean formulas, showing that recognizing 2-MUs can be done in linear time, while some special cases like MUSs with one or two unit-clauses are solvable in polynomial time, but general deficiency-1 MUSs remain NP-complete.
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.