2016/04/05 by Oliver Kullmann, Kullmann, Oliver, Xishun Zhao +1 · 2 citations
Computer Science · Mathematics · #05B99 #05D99 #68R05 #Advanced Graph Theory Research #Combinatorics (math.CO) #Constraint Satisfaction and Optimization #Discrete Mathematics (cs.DM) #F.2.2 #FOS: Computer and information sciences #FOS: Mathematics #G.2.2 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #acm:05B99 #acm:05D99 #acm:68R05 #cs.DM #cs.LO #math.CO #msc:05B99 #msc:05D99 #msc:68R05
paper · pdf · doi:10.48550/arxiv.1604.01288
17 pages
arxiv created 2016/04/05 · openalex publication_date 2016/04/05 · arxiv updated 2016/04/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The topic of this paper is the Finiteness Conjecture for minimally unsatisfiable clause-sets (MUs), stating that for each fixed deficiency (number of clauses minus number of variables) there are only finitely many patterns, given a certain basic reduction (generalising unit-clause propagation). We focus our attention on hitting clause-sets (every two clauses have at least one clash), where the conjecture says that there are only finitely many isomorphism types. The Finiteness Conjecture is here known to hold for deficiency at most 2, and we now prove it for deficiency 3. An important tool is the notion of "(ir)reducible clause-sets": we show how to reduce the general question to the irreducible case, and then solve this case (for deficiency 3). This notion comes from number theory (Korec 1984, Berger et al 1990), and we rediscovered it in our studies.