# On hyper-binary resolution

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```

Let’s set `a` to true, and see what happens. Immediately, `b` and `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 `g` without `-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?