Skip to content

Add predicate elimination as a new preprocessing step - #892

Merged
quickbeam123 merged 5 commits into
masterfrom
predicate_elimination
Aug 11, 2026
Merged

Add predicate elimination as a new preprocessing step#892
quickbeam123 merged 5 commits into
masterfrom
predicate_elimination

Conversation

@quickbeam123

@quickbeam123quickbeam123 commented Aug 3, 2026

Copy link
Copy Markdown
Collaborator

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.

@quickbeam123@claude
Add predicate elimination as a new preprocessing step (option: -pel, …
119524f
…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
quickbeam123 requested review from MichaelRawson and mezpusz and removed request for MichaelRawsonAugust 3, 2026 10:21
@quickbeam123

quickbeam123 commented Aug 3, 2026•
edited
Loading

Copy link
Copy Markdown
CollaboratorAuthor

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:

Sort by SAT
1025 ['problemsSTD_pel10964_dis10_i10K.pkl']
1073 ['problemsSTD_pel10964_dis10_pel_i10K.pkl']
Sort by UNS
8406 ['problemsSTD_pel10964_dis10_i10K.pkl']
8591 ['problemsSTD_pel10964_dis10_pel_i10K.pkl']
Total 1108 / 8826
Num only-by (UNS):
problemsSTD_pel10964_dis10_i10K.pkl 235
problemsSTD_pel10964_dis10_pel_i10K.pkl 420
Greedy cover (UNS):
# problemsSTD_pel10964_dis10_pel_i10K.pkl contributes 8591 total 8591
# problemsSTD_pel10964_dis10_i10K.pkl contributes 235 total 8406
Total 8826

Overall, I already reviewed this and as a separate module in preprocessing, this shouldn't cause any problems.

mezpusz
mezpusz reviewed Aug 6, 2026
View reviewed changes
Comment threadsamplers/samplerFNT.smp
@easychair

easychair commented Aug 6, 2026 via email

Copy link
Copy Markdown
Contributor

mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.cpp
mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.hpp Outdated
mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.hpp
mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.hpp Outdated
mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.hpp Outdated
mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.cpp Outdated
mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.cpp Outdated
mezpusz
mezpusz reviewed Aug 10, 2026
View reviewed changes
Comment threadShell/PredicateElimination.hpp
@quickbeam123
Marton's suggestions 1
550c4b0
@quickbeam123
Back PredicateElimination's forward subsumption by ClauseCodeTree
b34a196
Replace the hand-written port of ForwardSubsumptionAndResolution (a
LiteralSubstitutionTree keyed by the least matchable literal, a two-pass
generalization scan, and a SATSubsumptionAndResolution instance) with the
ClauseCodeTree path that SaturationAlgorithm uses under -cts. The code tree
indexes whole clauses and performs the multi-literal matching itself, so the
index-key bookkeeping (_indexedKey), the two passes and the SAT solver all go
away; forwardSubsumedOrResolved becomes a ClauseMatcher loop modelled on
CodeTreeForwardSubsumptionAndResolution::perform. PredicateElimination no
longer depends on SATSubsumption/ at all.
higherOrder is fixed to false: Preprocess does not run predicate elimination
on higher-order or polymorphic problems.
Also drop input tautologies (in addition to the duplicate literals we already
removed): the code tree's multi-literal matching assumes no clause carries two
equal or opposite literals, an invariant maintained in saturation by running
these very simplifications on every new clause.
Two behavioural notes:
- subsumption is no longer globally preferred over subsumption resolution --
ClauseMatcher returns whichever it reaches first -- but forwardSimplify
still iterates to a fixpoint, so the resulting clause set rarely differs;
- the empty clause has nothing to match on and is passed through, mirroring
the guard indexInsert already had.
On a sample of 80 TPTP problems clausified with -pel on -pels on, predicate
elimination ran out of time on 16 problems before and only 3 after.
@easychair

easychair commented Aug 10, 2026 via email

Copy link
Copy Markdown
Contributor

MichaelRawson
MichaelRawson approved these changes Aug 11, 2026
View reviewed changes

@MichaelRawsonMichaelRawson left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cool! I wondered if something similar could be achieved during saturation by literal selection - but it's not the same thing at all.

Comment threadShell/Preprocess.cpp
Comment threadShell/PredicateElimination.cpp
Comment threadShell/PredicateElimination.cpp
@quickbeam123
quickbeam123 merged commit 7f90db0 into masterAug 11, 2026
1 check passed
@quickbeam123
quickbeam123 deleted the predicate_elimination branch August 11, 2026 13:09
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MichaelRawsonMichaelRawsonMichaelRawson approved these changes
@mezpuszmezpuszmezpusz approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@quickbeam123@easychair@MichaelRawson@mezpusz