Closed quickbeam123 closed 1 month ago
Hi, I don't think we need this rule. We made experiments in the past - it does not help to solve new problems.
Uwe's talk was about "let's apply the standard construction and see what we obtain" - anybody understanding the construction would come up with the same results in 30 minutes.
Cheers, Andrei
On Fri, 19 Jul 2024 at 08:03, Martin Suda @.***> wrote:
I hacked this up during Uwe's talk at IJCAR.
Not sure if we want it, but it's a small change and seems to help (for UNS) a tiny bit:
Sort by UNS 7567 ['problemsSTD_rel_erds7706_dis5_sims-off_i5000.pkl'] 7577 ['problemsSTD_rel_erds7706_dis5_i5000.pkl'] 7585 ['problemsSTD_rel_erds7706_dis5_erd-simplif_i5000.pkl']
(coincidentally, the change improvement is in a similar ballpark to what we lose if we turn off simultaneous superposition).
For SAT, we consider erd=simplif an incomplete strategy, so we get:
Sort by SAT 517 ['problemsSTD_rel_erds7706_dis5_erd-simplif_i5000.pkl'] 986 ['problemsSTD_rel_erds7706_dis5_i5000.pkl'] 986 ['problemsSTD_rel_erds7706_dis5_sims-off_i5000.pkl']
You can view, comment on, or merge this pull request online at:
https://github.com/vprover/vampire/pull/581 Commit Summary
- cc2bb5e https://github.com/vprover/vampire/pull/581/commits/cc2bb5e6d5129a2d42afe00a3a28e271437c4a4c equalityResolutionWithDeletion as a simplifier
- c81807d https://github.com/vprover/vampire/pull/581/commits/c81807d0f14b637db7710390d185906924e1101b update the samplers too
File Changes
(9 files https://github.com/vprover/vampire/pull/581/files)
- M Saturation/SaturationAlgorithm.cpp https://github.com/vprover/vampire/pull/581/files#diff-b1a3fd77b0b97bfa20ffebeb433c7968f6feab0666418ae0a119f8b7ce7f3915 (5)
- M Shell/EqResWithDeletion.hpp https://github.com/vprover/vampire/pull/581/files#diff-e195169ec9e0c2ea121566afd292013ff037ee3c6dcbcde40fba280cb028a4d2 (8)
- M Shell/Options.cpp https://github.com/vprover/vampire/pull/581/files#diff-1d9a8bda26b884ff0eb2beeb509c437de7f04fc3df40e704901fdd26864a6d8c (12)
- M Shell/Options.hpp https://github.com/vprover/vampire/pull/581/files#diff-7e16f1074b0fafe3d87a886793c87cd07002a361d5b1d8514cd50a1484a79701 (10)
- M Shell/Preprocess.cpp https://github.com/vprover/vampire/pull/581/files#diff-d2ed7f8ad3d8c7844410206bf29266eb04da6c010984f5e9476542d8ba9daa13 (3)
- M samplers/samplerFOL.txt https://github.com/vprover/vampire/pull/581/files#diff-6d413557e2d2d15e59454106caa0b611d7f6dbe1281e22b57a5a0e7387277b00 (2)
- M samplers/samplerIND.txt https://github.com/vprover/vampire/pull/581/files#diff-5f1f56910544063409783e97fd4d51846f6b8e2af66938ee2570c7601fcc592d (2)
- M samplers/samplerSMT.txt https://github.com/vprover/vampire/pull/581/files#diff-6498c517f938bf3144a6ff7c1ab540249d7d81c54bb6ddeb4ab11365e351fdcb (2)
- M samplers/samplerUEQ.txt https://github.com/vprover/vampire/pull/581/files#diff-7ad25e02c8f698bee956a4f9a47afa7692416c918780ab161d8ad1dfa4d5e84b (2)
Patch Links:
— Reply to this email directly, view it on GitHub https://github.com/vprover/vampire/pull/581, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVY4BOSN3YV6OJEMCNRFHTZNC25XAVCNFSM6AAAAABLEAPDS2VHI2DSMVQWIX3LMV43ASLTON2WKOZSGQYTQMRRG4ZTCNQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>
Fair point, Andrei! Let's put this to ice.
I hacked this up during Uwe's talk at IJCAR.
Not sure if we want it, but it's a small change and seems to help (for UNS) a tiny bit:
(coincidentally, the change improvement is in a similar ballpark to what we lose if we turn off simultaneous superposition).
For SAT, we consider erd=simplif an incomplete strategy, so we get: