No Cover Image

Working paper 5 views

Simple minimally unsatisfiable subsets of 2-CNFs

Oliver Kullmann Orcid Logo, Edward Clewer

Pages: 1 - 18

Swansea University Author: Oliver Kullmann Orcid Logo

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...

Full description

Published: arXiv.org 2026
Online Access: https://arxiv.org/abs/2603.10944
URI: https://cronfa.swan.ac.uk/Record/cronfa71622
first_indexed 2026-03-12T18:06:30Z
last_indexed 2026-03-13T05:25:17Z
id cronfa71622
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2026-03-12T18:06:28.3571380</datestamp><bib-version>v2</bib-version><id>71622</id><entry>2026-03-12</entry><title>Simple minimally unsatisfiable subsets of 2-CNFs</title><swanseaauthors><author><sid>2b410f26f9324d6b06c2b98f67362d05</sid><ORCID>0000-0003-3021-0095</ORCID><firstname>Oliver</firstname><surname>Kullmann</surname><name>Oliver Kullmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2026-03-12</date><deptcode>MACS</deptcode><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.</abstract><type>Working paper</type><journal/><volume/><journalNumber/><paginationStart>1</paginationStart><paginationEnd>18</paginationEnd><publisher>arXiv.org</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>minimal unsatisfiable subsets, polynomial time, 2-CNF, enumeration</keywords><publishedDay>12</publishedDay><publishedMonth>3</publishedMonth><publishedYear>2026</publishedYear><publishedDate>2026-03-12</publishedDate><doi/><url>https://arxiv.org/abs/2603.10944</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm>Not Required</apcterm><funders/><projectreference/><lastEdited>2026-03-12T18:06:28.3571380</lastEdited><Created>2026-03-12T17:55:42.6037205</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2"/></path><authors><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>1</order></author><author><firstname>Edward</firstname><surname>Clewer</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2026-03-12T18:06:28.3571380 v2 71622 2026-03-12 Simple minimally unsatisfiable subsets of 2-CNFs 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2026-03-12 MACS 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. Working paper 1 18 arXiv.org minimal unsatisfiable subsets, polynomial time, 2-CNF, enumeration 12 3 2026 2026-03-12 https://arxiv.org/abs/2603.10944 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Not Required 2026-03-12T18:06:28.3571380 2026-03-12T17:55:42.6037205 Faculty of Science and Engineering Oliver Kullmann 0000-0003-3021-0095 1 Edward Clewer 2
title Simple minimally unsatisfiable subsets of 2-CNFs
spellingShingle Simple minimally unsatisfiable subsets of 2-CNFs
Oliver Kullmann
title_short Simple minimally unsatisfiable subsets of 2-CNFs
title_full Simple minimally unsatisfiable subsets of 2-CNFs
title_fullStr Simple minimally unsatisfiable subsets of 2-CNFs
title_full_unstemmed Simple minimally unsatisfiable subsets of 2-CNFs
title_sort Simple minimally unsatisfiable subsets of 2-CNFs
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Oliver Kullmann
Edward Clewer
format Working paper
container_start_page 1
publishDate 2026
institution Swansea University
publisher arXiv.org
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
url https://arxiv.org/abs/2603.10944
document_store_str 0
active_str 0
description 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.
published_date 2026-03-12T05:22:32Z
_version_ 1859704221787488256
score 11.099424

Similar Items