# On failed literal probing

Apparently, there have been quite some work done on failed literal probing, although I don’t think they have all been put into a common package yet.

The idea is quite simple in its purest form: try to set variable `v1` to `true` and see if that fails. If it does, variable `v1` must be `false`. If it doesn’t fail, try the other way around: set it to `false` and if that fails, it must be `true`.

There are a couple of tricks we can add, however. For example, if both `v1` and `!v1` set variable `v10` to value `X` (where `X` can be either `true` or `false`), then set `v10` to `X`. The reasoning here is simple: `v1` must be set, so whatever both `v1` and `!v1` imply, it must be set, too. So we can safely set `v10` to `X`.

A more interesting thinking is the following. If `v1` sets `v20` to `true`, but `!v1` sets `v20` to `false`, then `v1 = v20`. So, we can replace `v20` with `v1`. One less variable to worry about!

There are even more tricks, however. If setting `v1` to `true` and `false` both shorten a longer XOR to a 2-long XOR “`v40 + v50 = false`“, this 2-long XOR can be learnt: `v40` can be replaced with `v50`.

And more tricks. If there is a 2-long clause `v1 or v2 = true`, then we can do all of the above, but with `v1` and `v2` this time. Since either `v1` or `v2` must be `true`, all the above ideas still work. In all previous ideas all we used was the fact that either `v1` or `!v1` must be true. This is still the case: either `v1` or `v2` must be true. This, by the way, is called 1-recursive learning. (note: the fourth paragraphs changes a bit, but we still learn a 2-long xor).

And now something new. I have been thinking about trying to re-use old learnt clauses. They really code down sometimes quite important facts about the problem. What if we tried to re-use them? After all, keeping them in memory is really cheap: the only problem with them is that doing regular propagation with them takes a lot of time, thus slowing down the solver. But what if we only used them to do failed literal probing? I just launched a test on the Grid’5000 cluster to find out. Fingers crossed…