  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.
