Randomized preprocessing - #895
Open
quickbeam123 wants to merge 8 commits 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>
… log-uniformly from [nm/2, 2*nm] Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ndividual definition eliminations Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…a candidate inequality (a pass with all candidates skipped ends the per-clause fixpoint) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ered blocking (the dropped candidate is never re-enqueued, so the clause can only still get blocked via one of its other literals) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…andidate predicate (marking it never-to-be-reconsidered, so it stays in the problem for good) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
quickbeam123
requested review from
MichaelRawson and
mezpusz
and removed request for
MichaelRawson
August 4, 2026 15:36
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
1 participant
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.
randomized_preprocessingmakes selected preprocessing steps "leaky": under a coin toss, some of their operations are randomly skipped, producing a mixture of half-completed (but still sound) results as a source of noise injection and a data augmentation technique.This PR stands of top of on the predicate-elimination one.