Small demodulation improvement

[mezpusz]

Equations such as the following
f(x,f(y,z)) = f(z,f(y,x))
give two identical ways to demodulate, but we index both variants.

Since these equations are by definition incomparable as well, it can hurt
the performance of demodulation a bit as such demodulators are tried twice
in the unsuccessful case.

Experiments show a slight improvement over TPTP-v8.1.2 with -sa discount -t 10:
avg time: 5.13053s (old), 5.11622s (new)
solved: 10852 (old), 10865 (new)

[MichaelRawson]

Nice. Seems like a slam-dunk to me, @quickbeam123.

give two identical ways to demodulate, but we index both variants

Are there any other cases where this idea happens? I couldn't come up with any single-equation cases off the top of my head.

[mezpusz]

It could also happen in superposition, generating two variants of the same clause, but I haven't really looked at that case...

[easychair]

I am suspicious, results are too good because I cannot imagine 1. That many problems contain such demodulators 2. Even if they do, 13 more problems would be solved 3. With 0.02s average improvement we solve 13 more problems. What is avg, by the way? average over what? It would be good if someone checks what is going on. A

…

On Mon, 12 Feb 2024 at 17:30, Márton Hajdu ***@***.***> wrote: Equations such as the following f(x,f(y,z)) = f(z,f(y,x)) give two identical ways to demodulate, but we index both variants. Since these equations are by definition incomparable as well, it can hurt the performance of demodulation a bit as such demodulators are tried twice in the unsuccessful case. Experiments show a slight improvement with avg time: 5.13053s (old), 5.11622s (new) solved: 10852 (old), 10865 (new) ------------------------------ You can view, comment on, or merge this pull request online at: #522 Commit Summary - c28aec4 <c28aec4> Do not use both sides of equations for demodulation which are their own variants oriented reversed File Changes (1 file <https://github.com/vprover/vampire/pull/522/files>) - *M* Kernel/EqHelper.cpp <https://github.com/vprover/vampire/pull/522/files#diff-6a77dea4f9bb860fe1532d8e5bdcacd03df29fee6823dbba6c648f7acdd018a1> (6) Patch Links: - https://github.com/vprover/vampire/pull/522.patch - https://github.com/vprover/vampire/pull/522.diff — Reply to this email directly, view it on GitHub <#522>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BI7UYZRIGDZYIF2M7TYTJGS5AVCNFSM6AAAAABDFDUWOGVHI2DSMVQWIX3LMV43ASLTON2WKOZSGEZTANRRGYZDCOA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[selig]

For a -sa discount -t 10 experiment, an increase of 15 problems feels like some could fall into standard variability.

I'd be tempted to repeat to see how much falls into variability and whether the same 15 are gained then look at those to confirm they come from this option.

However, the code change seems a net positive without the results; do less work = good.

[mezpusz]

Yes, I agree that the experiment was far from thorough, I mainly wanted to see that we don't lose proofs and that the proofs are the same (although I think there could be small changes in the proof search due to a code tree or substitution tree being organized in a slightly different way with and without a certain demodulator being indexed).

There are hundreds of benchmarks with e.g. AC-axioms where this makes a difference, but overall in the 25257 benchmarks this averages out.

Let me know if more details are needed.

[quickbeam123]

I will run my own experiments anyway, will let you know!

[quickbeam123]

I see around 5 problem improvement on average under shuffling:

8764.7 -> 8769.6

with discount10 and 1000 Mi instruction limit.

Although I still didn't properly work out statistics, I would guess the probability that this makes things worse is actually quite low! ;)