Preprocessing extensions - #886
Open
quickbeam123 wants to merge 4 commits into
Open
Conversation
Pushes quantifiers inside rectified/NNF/flattened formulas just before Skolemization (old clausification pipeline only; no effect with newcnf), so Skolem functions get fewer arguments. Duplicated binders are renamed on the fly to keep formulas rectified, as Skolemization requires. Skipped for higher-order and polymorphic problems: SubstHelper cannot rename under lambdas, and FormulaVarIterator does not see type variables inside binder sorts. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…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>
…solution The -pels path now keeps the clause set not just forward-inter-subsumed but also subsumption-resolved, reusing the saturation machinery: the candidate retrieval ports ForwardSubsumptionAndResolution::perform to our single-index setting (units and multi-literal clauses share one tree), including the setSR/usePreviousSetUp handshake with SATSubsumptionAndResolution, the preference of subsumption over any found SR conclusion, and the unit shortcut that skips the SAT solver. Conclusions come out of checkSubsumptionResolution/getSubsumptionResolutionConclusion ready-made, carrying a FORWARD_SUBSUMPTION_RESOLUTION inference with both premises. Unlike a single FSAR::perform call, we chain the simplification to a fixpoint (subsumption + SR on the conclusion again, until subsumed away or fully reduced), which matches saturation's net effect where a replacement re-enters the forward simplification loop. Applied both to the input clauses during the initial pass and to every generated resolvent before it is counted against the growth budget. Note that the clauses S_P and S_~P of the predicate being eliminated can never subsume or SR-simplify a P-free resolvent (their P-literal has nothing to match), so checking resolvents before deleting those clauses is safe. SR deletions and replacements are logical consequences of the remaining set, so no model-repairing interference is needed (re-verified via FMB and --mode model_check on problems where SR fired). Backward subsumption and backward SR remain future work. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…soundness fix) Clauses can still carry duplicate literals when they reach predicate elimination (e.g., EqResWithDeletion turns p(X) | p(a) | X != a into p(a) | p(a)), while SATSubsumptionAndResolution relies on its premises being duplicate-free -- an invariant that saturation maintains by running duplicate literal removal on every new clause, and that PE's -pels path violated. With the invariant broken, subsumption resolution could produce unsound conclusions. Minimal example (satisfiable, but was refuted in release; in debug an assertion in loadProblem would fire instead): cnf(c1, axiom, p(X) | ~p(Y)). cnf(c2, axiom, p(X) | p(a) | X != a). After equality resolution, c2 becomes p(a) | p(a). Taking it as the main premise against the side premise c1, the positional SAT encoding certifies resolving away the copy at one position while the side's positive literal p(X) matches the copy at the other position; conclusion generation then removes the resolved literal by pointer identity -- killing both copies, since duplicates of a shared literal are the same pointer -- and "derives" the empty clause. (This also incorrectly refuted, e.g., the satisfiable NUM926_30 with -pel on -pels on.) The fix runs DuplicateLiteralRemovalISE on every clause PE takes in; besides restoring the invariant, this also makes the occurrence counting less conservative (p(a) | p(a) no longer counts as self-referential in p). Resolvents and SR conclusions were already duplicate-free by construction. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
For now adding miniscoping, to be experimented with