[metis-users] Subsumption in Metis - a quick question (I hope)

[Joe Hurd]

Hi James,

> I have a quick question on the subsumption routine. As a part of the Subsume
> structure there appears to be a type of empty clauses (alongside unit and
> nonunit).

The subsumption code is a little baroque. When checking whether any
clause in Subsume.subsume subsumes a given clause cl (a.k.a. forward
subsumption) the following algorithm is used:

1. If there's an empty clause in Subsume.subsume, then return it.

2. Check whether any of the unit clauses in Subsume.subsume matches a
literal of cl.

3. The rest of the clauses in Subsume.subsume are stored with two of
their literals treated specially: one goes into a set fstLits; and
another goes into a set sndLits.

3a. Let C1 be the set of clauses in Subsume.subsume containing a
literal in fstLits that matches a literal in cl.

3b. Let C2 be the set of clauses in Subsume.subsume containing a
literal in sndLits that matches a literal in cl.

3c. Let C = C1 intersect C2 be the set of candidate subsumption
clauses in Subsume.subsume.

3d. For each clause in C, perform a full subsumption check with cl.
Return the first clause that succeeds.

> Since the empty clause presumably would normally terminate the
> program I am puzzled as to why it has its own part of the Subsume structure.

You are correct that in the normal operation of Metis the appearance
of an empty clause would signal a successful proof. However, I wanted
to write a generic forward subsumption data structure, and to do that
it's necessary to store empty clauses that are added and return them
as subsumption matches. The algorithm above just returns the first
clause that subsumes the given clause, but a previous version of the
code (lazily) returned all the subsuming clauses.

Cheers,

Joe