Working paper 5 views
Simple minimally unsatisfiable subsets of 2-CNFs
Oliver Kullmann 
,
Edward Clewer
,
Edward Clewer
Pages: 1 - 18
Swansea University Author:
Oliver Kullmann
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...
| Published: |
arXiv.org
2026
|
|---|---|
| Online Access: |
https://arxiv.org/abs/2603.10944 |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa71622 |
| 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. |
|---|---|
| Keywords: |
minimal unsatisfiable subsets, polynomial time, 2-CNF, enumeration |
| College: |
Faculty of Science and Engineering |
| Start Page: |
1 |
| End Page: |
18 |