[mezpusz]

We don't generally want to spend too much time computing HOL unifiers in a single generating inference. This was only controlled so far by a bound on the depth of the unification tree, but it also makes sense to cap the weight of the unifiers too, delaying the really problematic ones. This PR adds the functionality to stop computing unification constraints that are too big, given by a bound set by a new option. Of course this is only done when we are already in a non-zero unification depth, otherwise we are not making progress with the unification.

The result are not super exciting but definitely show improvement with the semi-randomly chosen default value 1000. In particular, we solve the previously unsolved NUM021^1 which is known to be a hard unification problem.

TPTP HOL Discount:

run 0 unsat: 2127 (0) sat: 1 (0) cputime: 10411.47 s instructions: 49410866 Mi memory: 241397.18 MB
run 1 unsat: 2128 (1) sat: 1 (0) cputime: 10402.21 s instructions: 49382231 Mi memory: 232456.09 MB

TPTP HOL Otter:

run 0 unsat: 2109 (0) sat: 1 (0) cputime: 10729.34 s instructions: 49906193 Mi memory: 333578.71 MB
run 1 unsat: 2113 (4) sat: 1 (0) cputime: 10698.48 s instructions: 49855248 Mi memory: 319983.25 MB

[MichaelRawson]

Haven't looked at the code at all yet. But would it make sense to limit only by (total?) weight, rather than weight + depth? Imagine there are only finitely many unifiers with a given weight.

[mezpusz]

Haven't looked at the code at all yet. But would it make sense to limit only by (total?) weight, rather than weight + depth? Imagine there are only finitely many unifiers with a given weight.

Good idea, but not sure it would work in all cases, we might get into some looping, since the problem is not decidable, right?

[MichaelRawson]

I'm thinking of this in the same way that both selecting clauses only by age and selecting only by weight are complete: there are only finitely many clauses with a given weight.

Back to HOL unification. I imagine that deeper in the unification tree you have to (eventually) create something with a larger weight. Or perhaps the weight function can be adapted to take this into account?

Either way, just an idea. Will get back to reviewing code. :)

[mezpusz]

You're right, but for using the weight like that you will need some kind of subsumption to avoid doing the same thing over and over. Which might be actually an excellent idea to try on matthew-22-21! For master, we could probably implement subsumption of unification pairs only locally for a given term index query call. 🤔

[MichaelRawson]

And nice and easy to review it was, too. :)

[mezpusz]

We can also postpone this if it feels like there should be some more generally worked out solution.