Add predicate elimination as a new preprocessing step - #892
Open
quickbeam123 wants to merge 1 commit into
Open
Conversation
…default off)
Implements the technique of Khasidashvili and Korovin (SAT 2016): a predicate P
occurring at most once in every clause is eliminated by replacing S_P and S_~P
with all pairwise resolvents on P. On problems without equality and theories,
resolvents are computed with an mgu and non-unifiable pairs dropped; otherwise
the P-literals are (virtually) flattened, introducing argument disequalities
which are then simplified away by exhaustive equality substitution (this can
introduce equality into a problem previously without it). FMB forces the
equational mode, since its model reconstruction cannot rely on the
Herbrand-interpretation argument justifying the mgu variant.
Elimination steps are gated SAT-VE-style by growth limits on the estimated
clause count |S_P|*|S_~P| - |S_P| - |S_~P|: a per-step tolerance factor over
the current total (-pelst, default 1.05) and a global cap relative to the
original total (-peltl, default 2.0). Syntactic tautologies (complementary
pair, t != t, s = s) and duplicate literals are removed from generated
resolvents, and the actual surviving count feeds back into the budget.
The next predicate to eliminate is by default the one with the smallest
estimated growth (pure predicates thus go first, their clauses being simply
deleted); with -pelr the choice is uniformly random among the admissible
candidates (controlled by random_seed), since the process is not confluent.
With -pels, the clause set is kept forward-inter-subsumed throughout, using a
standalone LiteralSubstitutionTree index (unit literal, or the least matchable
one) plus SATSubsumptionAndResolution; backward subsumption is left as future
work.
Every elimination records a model-repairing definition
P(xs) <=> \/_{D \/ P(ts) in S_P} exists ys. (xs = ts /\ ~D)
via Problem::addEliminatedPredicate (addTrivialPredicate for pure ones), so
both the textual model updates output and FMB model restoration stay correct
(verified via --mode model_check).
Skipped for higher-order/polymorphic inputs (predicates could hide inside
terms, breaking the occurrence counting) and for color-annotated problems.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
quickbeam123
requested review from
MichaelRawson and
mezpusz
and removed request for
MichaelRawson
August 3, 2026 10:21
Collaborator
Author
|
The original commit message is preserved in the commit but describes more than what I eventually decided to keep. (I used interactive rebasing and "fixup" to hide my update commits, not sure if for the better.) A TPTP FOL discount comparison is now: Overall, I already reviewed this and as a separate module in preprocessing, this shouldn't cause any problems. |
mezpusz
reviewed
Aug 6, 2026
| $ins=Z > ins ~cat 0:1 | ||
| $ins=NZ > ins ~sgd 0.4,1 | ||
|
|
||
| # predicate_elimination |
Contributor
There was a problem hiding this comment.
Looking at the duplicate changes in multiple sampler files, do you think some kind of inclusion mechanism could be added to the sampler syntax? We could then move out the common parts to separate files.
Contributor
There was a problem hiding this comment.
That's a good idea. We now have a few different homebrew Vampire input files - do you know of some semi-standardised configuration language?
Contributor
|
This predicate elimination technique was implemented in very early versions
of Vampire, I think as early as in 1999. I am not claiming it is exactly
the same as when K&K published, but it was in the code. The elimination was
done for (1 x n) occurrences or (2 x 2) occurrences because in these two
cases the number of clauses does not increase (1 + n clauses are replaced
by n and 4 clauses replaced by 4.
There is a caveat though: you don't want to have definition introduction
during formula preprocessing following predicate definition elimination,
which effectively undoes the introduction.
A
…On Mon, 3 Aug 2026 at 12:15, Martin Suda ***@***.***> wrote:
Implements the technique of Khasidashvili and Korovin (SAT 2016): a
predicate P occurring at most once in every clause is eliminated by
replacing S_P and S_~P with all pairwise resolvents on P. On problems
without equality and theories, resolvents are computed with an mgu and
non-unifiable pairs dropped; otherwise the P-literals are (virtually)
flattened, introducing argument disequalities which are then simplified
away by exhaustive equality substitution (this can introduce equality into
a problem previously without it). FMB forces the equational mode, since its
model reconstruction cannot rely on the Herbrand-interpretation argument
justifying the mgu variant.
Elimination steps are gated SAT-VE-style by growth limits on the estimated
clause count |S_P|*|S_~P| - |S_P| - |S_~P|: a global cap relative to the
original total (-peltl, default 2.0). Syntactic tautologies (complementary
pair, s = s) and duplicate literals are removed from generated resolvents,
and the actual surviving count feeds back into the budget.
The next predicate to eliminate is by default the one with the smallest
estimated growth (pure predicates thus go first, their clauses being simply
deleted)
With -pels, the clause set is kept forward-inter-subsumed throughout,
using a standalone LiteralSubstitutionTree index (unit literal, or the
least matchable one) plus SATSubsumptionAndResolution; backward subsumption
is left as future work.
Every elimination records a model-repairing definition
P(xs) <=> /_{D / P(ts) in S_P} exists ys. (xs = ts /\ ~D)
via Problem::addEliminatedPredicate (addTrivialPredicate for pure ones),
so both the textual model updates output and FMB model restoration stay
correct (verified via --mode model_check).
Skipped for higher-order/polymorphic inputs (predicates could hide inside
terms, breaking the occurrence counting) and for color-annotated problems.
------------------------------
You can view, comment on, or merge this pull request online at:
#892
Commit Summary
- 119524f
<119524f>
Add predicate elimination as a new preprocessing step (option: -pel,
default off)
File Changes
(17 files <https://github.com/vprover/vampire/pull/892/files>)
- *M* Kernel/Inference.cpp
<https://github.com/vprover/vampire/pull/892/files#diff-7a0c538d026b495a9cbe1206aa0bbba871265593b78fc1d3a52d55fe498eb294>
(2)
- *M* Kernel/Inference.hpp
<https://github.com/vprover/vampire/pull/892/files#diff-f39bb9c583a00abd1bef6f2b36cc7619a868f458d3263cb869adb35d77243a78>
(2)
- *M* Makefile
<https://github.com/vprover/vampire/pull/892/files#diff-76ed074a9305c04054cdebb9e9aad2d818052b07091de1f20cad0bbac34ffb52>
(1)
- *M* Shell/Options.cpp
<https://github.com/vprover/vampire/pull/892/files#diff-1d9a8bda26b884ff0eb2beeb509c437de7f04fc3df40e704901fdd26864a6d8c>
(28)
- *M* Shell/Options.hpp
<https://github.com/vprover/vampire/pull/892/files#diff-7e16f1074b0fafe3d87a886793c87cd07002a361d5b1d8514cd50a1484a79701>
(6)
- *A* Shell/PredicateElimination.cpp
<https://github.com/vprover/vampire/pull/892/files#diff-a8d54d83b75bf96b02661c6a3d689fbe1b0c61e05fd781eec3153b5fb7da28a7>
(694)
- *A* Shell/PredicateElimination.hpp
<https://github.com/vprover/vampire/pull/892/files#diff-332139a4e2276e718fd25f24fcd052393ffffca758b4ffec14b94958a6c9580c>
(132)
- *M* Shell/Preprocess.cpp
<https://github.com/vprover/vampire/pull/892/files#diff-d2ed7f8ad3d8c7844410206bf29266eb04da6c010984f5e9476542d8ba9daa13>
(19)
- *M* Shell/Statistics.cpp
<https://github.com/vprover/vampire/pull/892/files#diff-9101858d03e79d08341f2fc45ca5a11dec594d22500a5bb60793725062bf20b0>
(6)
- *M* Shell/Statistics.hpp
<https://github.com/vprover/vampire/pull/892/files#diff-563a31ccb959ad26a9226c8cd46518c2e72a41bd2f1ab61b505ac6c208922026>
(9)
- *A* UnitTests/tPredicateElimination.cpp
<https://github.com/vprover/vampire/pull/892/files#diff-a52ad388c16723847a2be0531747b78def273df7391f3dcdf5a12a4e7ed7908d>
(374)
- *M* cmake/sources.cmake
<https://github.com/vprover/vampire/pull/892/files#diff-a56d5c701e96a485b37ee07f16c6ba1b8382825fa99731897e4d7fc8290bac5c>
(3)
- *M* samplers/samplerFNT.smp
<https://github.com/vprover/vampire/pull/892/files#diff-9f23b71a064f9b09e948449d2ee7107171713441ccf856023f9e4bf2b4ebbd93>
(9)
- *M* samplers/samplerFOL.smp
<https://github.com/vprover/vampire/pull/892/files#diff-f8bd0658b1a6c4d4d397959eaf14d70dde04710f45686b6e4d1048d3b8b77e58>
(9)
- *M* samplers/samplerHOL.smp
<https://github.com/vprover/vampire/pull/892/files#diff-2ec7c12e7f41dc78f3f54a6cb380a9aeec58ededfb0548fa93dd830bc3fee778>
(9)
- *M* samplers/samplerIND.smp
<https://github.com/vprover/vampire/pull/892/files#diff-dc218f474ed75736f1da8200c10da22b6d25d65893f7a672a8ccd0df581bf6b2>
(9)
- *M* samplers/samplerSMT.smp
<https://github.com/vprover/vampire/pull/892/files#diff-8fda531ec8de3d8dbabb79dd5b8ad22b9ad223b5ac2d123142a30f4159a6b955>
(9)
Patch Links:
- https://github.com/vprover/vampire/pull/892.patch
- https://github.com/vprover/vampire/pull/892.diff
—
Reply to this email directly, view it on GitHub
<#892?email_source=notifications&email_token=ABVY4BPPBLYJCVZOMRWLIP35IBQ57A5CNFSNUABEM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UF42DCOJTGM3TKNRWGOTHEZLBONXW5KTTOVRHGY3SNFRGKZFFMV3GK3TUVRTG633UMVZF6Y3MNFRWW>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABVY4BNADEJIRBFSJSQBCDD5IBQ57AVCNFSNUABEKJSXA33TNF2G64TZHMYTQMBWG44TCMB3JFZXG5LFHM2TANBYG4YTQMZYGOQXMAQ>
.
Triage notifications, keep track of coding agent tasks and review pull
requests on the go with GitHub Mobile for iOS
<https://github.com/notifications/mobile/ios/ABVY4BKGS3SRRUXZ4CCN3XT5IBQ57A5CNFSNUABEM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UF42DCOJTGM3TKNRWGOTHEZLBONXW5KTTOVRHGY3SNFRGKZFFMV3GK3TUVJTG633UMVZF62LPOM>
and Android
<https://github.com/notifications/mobile/android/ABVY4BID2G7MPMGRV3NCY5T5IBQ57A5CNFSNUABEM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UF42DCOJTGM3TKNRWGOTHEZLBONXW5KTTOVRHGY3SNFRGKZFFMV3GK3TUVZTG633UMVZF6YLOMRZG62LE>.
Download it today!
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements the technique of Khasidashvili and Korovin (SAT 2016): a predicate P occurring at most once in every clause is eliminated by replacing S_P and S_~P with all pairwise resolvents on P. On problems without equality and theories, resolvents are computed with an mgu and non-unifiable pairs dropped; otherwise the P-literals are (virtually) flattened, introducing argument disequalities which are then simplified away by exhaustive equality substitution (this can introduce equality into a problem previously without it). FMB forces the equational mode, since its model reconstruction cannot rely on the Herbrand-interpretation argument justifying the mgu variant.
Elimination steps are gated SAT-VE-style by growth limits on the estimated clause count |S_P|*|S_~P| - |S_P| - |S_~P|: a global cap relative to the original total (-peltl, default 2.0). Syntactic tautologies (complementary pair, s = s) and duplicate literals are removed from generated resolvents, and the actual surviving count feeds back into the budget.
The next predicate to eliminate is by default the one with the smallest estimated growth (pure predicates thus go first, their clauses being simply deleted)
With -pels, the clause set is kept forward-inter-subsumed throughout, using a standalone LiteralSubstitutionTree index (unit literal, or the least matchable one) plus SATSubsumptionAndResolution; backward subsumption is left as future work.
Every elimination records a model-repairing definition
P(xs) <=> /_{D / P(ts) in S_P} exists ys. (xs = ts /\ ~D)
via Problem::addEliminatedPredicate (addTrivialPredicate for pure ones), so both the textual model updates output and FMB model restoration stay correct (verified via --mode model_check).
Skipped for higher-order/polymorphic inputs (predicates could hide inside terms, breaking the occurrence counting) and for color-annotated problems.