Hyper-binary resolution is actually quite straightforward, or at least appears to be. Let’s take the following example. The clauses in our database are the following:
-a V b
-a V c
-b V -c V g
-b V -c V d
-d V g
a to true, and see what happens. Immediately,
c get set to true through binary clauses. If we now propagate
g through the clause
-b V -c V g, we ought to do hyper-binary resolution straight away, and add the clause
-a V g — some call this lazy hyper-binary resolution. Good, one more binary clause!
But then… So now we have nothing to propagate using only binary clauses, we have to propagate using a long clause,
-b V -c V d. As good citizens, we also do (lazy) hyper-binary resolution, coming up with the clause
-a V d. Good, one more binary clause! One slight glitch now…
d propagates to
g, using a binary clause. But this means that setting
a can propagate to
-a V g, the first hyper-binary clause we added! So the first hyper-binary clause we added is in fact useless, it needs to be removed. If we applied transitive reduction, it would remove the first hyper-binary clause
-a V g automatically.
Let’s go a bit deeper here. How could we have avoided adding the first hyper-binary clause? The obvious answer is: we should have started with
-b V -c V d instead of
-b V -c V g. But how easy would have it been to know (i.e. calculate) that starting with that different long clause would have made our work easier? I am not sure it would have been easy to know. And of course the example above is very trivial. It could be made much-much more complicated:
g could have been reached with any number of hyper-binary resolutions from
d — so simple binary look-ahead would not have helped.
I am stuck here. Any ideas?