Unsatisfiable hitting clause-sets with three more clauses than variables

TL;DR

This paper proves the Finiteness Conjecture for minimally unsatisfiable hitting clause-sets with a deficiency of 3, extending known results from deficiency 2 using the concept of irreducible clause-sets.

Contribution

It introduces the reduction to irreducible clause-sets and proves the conjecture for the case of deficiency 3, advancing understanding of clause-set structures.

Findings

Finiteness conjecture holds for deficiency 3 in hitting clause-sets.

Reduction to irreducible clause-sets simplifies the problem.

Established methods from number theory are applied to clause-set analysis.

Abstract

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.