{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreicncplqmmatqirovpwd3emcmfhfkrk7okk4fujnjwcwmq4vnyqdlm",
    "uri": "at://did:plc:4rgrdigiftglskeax4wvmsev/app.bsky.feed.post/3mgvtzve3ckm2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2603.10944v1",
  "publishedAt": "2026-03-12T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Oliver Kullmann",
    "Edward Clewer"
  ],
  "textContent": "**Authors:** Oliver Kullmann, Edward Clewer\n\nWe 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.",
  "title": "Simple minimally unsatisfiable subsets of 2-CNFs"
}