BM25 k3 query-term saturation is skipped for repeated SHOULD clauses when 2 <= minimumNumberShouldMatch < number of SHOULD clauses

#15818 (unreleased, 11.0.0) added an opt-in k3 to BM25Similarity, and #16243 to StableTflSimilarity: a term repeated n times in a query is weighted ((k3 + 1) * n) / (k3 + n) "instead of linear summing". The weight is applied in exactly one place, when BooleanQuery.rewrite merges duplicate clauses into one boosted clause. Duplicate SHOULD clauses are merged only when minimumNumberShouldMatch <= 1, a correct guard from LUCENE-7925 (2017), because merging changes how many clauses a document matches. So for 2 <= minimumNumberShouldMatch < number of SHOULD clauses the duplicates stay separate and add up linearly, while msm 0, 1 and msm = number of SHOULD clauses are saturated. One document "a b", SHOULD a, a, b, k3 = 8: 0.3661408 at msm 1 and 3, 0.39229372 at msm 2. Only scores change; the matching documents do not, and nothing throws. Main and branch_11x only; no release has k3. A small BooleanWeight change that leaves the rewrite alone fixes it.

1. The promise. BM25Similarity.java:44-46, @param k3: "Controls query-side term frequency saturation. When duplicate terms appear in a query, their boost is computed as ((k3 + 1) * qtf) / (k3 + qtf) instead of linear summing. A negative value disables saturation (linear behavior)." StableTflSimilarity.java:103-105 has the same words, and its class javadoc lists "query-side saturation for repeated query terms" (:50). The formula: BM25Similarity.java:125-136, StableTflSimilarity.java:153-164; the default constructor sets k3 = -1 (BM25Similarity.java:121-123).
2. The hook. Similarity#computeQueryTermWeight (Similarity.java:164-177, @lucene.experimental) "is used during query rewriting to compute the boost for duplicate query terms"; the default is linear.
3. Its only caller. deduplicateClauses (BooleanQuery.java:714-758) groups equal clauses of one occur and boosts the merged clause by similarity.computeQueryTermWeight(n) (:746); with explicit boosts it sums them linearly (:740-742). No other production code calls the hook.
4. The guard. The SHOULD dedup runs only when minimumNumberShouldMatch <= 1 (BooleanQuery.java:438-447, condition at :442). Merging a a into a^w would make a document with only a stop matching (a a b)~2, so the guard is right; the hunt's Z3 model shows that a guard of msm <= 2 breaks matching (counterexample: msm = 2, two equal SHOULD clauses).
5. The MUST path. MUST duplicates are merged unconditionally (BooleanQuery.java:449-455); when the number of SHOULD clauses equals msm, every SHOULD becomes MUST (:570-587). That is why msm = number of SHOULD clauses saturates again.
6. Result. For 2 <= msm < number of SHOULD clauses the rewrite leaves the duplicate SHOULD clauses apart (for the repro's query it returns the query unchanged; duplicate MUST clauses in the same query would still be merged), BooleanWeight creates one weight per clause with the same boost (BooleanWeight.java:49-62), and the duplicates add up linearly.
7. Before k3 the guard changed no score: merged (a^2) and unmerged (a a) duplicates both add up linearly. k3-free controls on 9.12.3, 10.5.2, the parent of #15818 and main give one score for msm 1, 2 and 3.

One document "a b", BM25Similarity(1.2f, 0.75f, true, 8f), each term scores s = 0.13076457:

With k3 disabled every row is 0.39229372. With five SHOULD clauses (alpha x3, bravo, charlie) msm 0, 1 and 5 are saturated (1.2603091) and msm 2, 3 and 4 linear (1.385843). StableTflSimilarity with k3 = 8 behaves the same (3.739564 at msm 1 and 3, 4.0066757 at msm 2, on the finder's six-document index).

• Who. Users of main or branch_11x (unreleased 11.0.0) that set BM25Similarity(k1, b, discountOverlaps, k3) or StableTflSimilarity(k1, c, k3) with k3 >= 0 as the searcher's similarity, and run a BooleanQuery with a repeated unboosted SHOULD clause and 2 <= msm < number of SHOULD clauses. The typical producer is a "minimum should match" option over user text with a repeated word: QueryBuilder.createMinShouldMatchQuery("body", "alpha alpha bravo", f) scores one document 0.8479051 at f = 0.5 (msm 1), 0.90846974 at f = 0.7 (msm 2) and 0.8479051 at f = 1.0. Query text with a repeated word is the case k3 is for (#15768: "duplicate terms in query strings see their scores boosted by their number of occurrences").
• Reach limit. The rewrite takes the weight from IndexSearcher#getSimilarity() (BooleanQuery.java:734, :746), so k3 has an effect only if that similarity applies it. BM25Similarity and StableTflSimilarity do. The stock PerFieldSimilarityWrapper does not override computeQueryTermWeight, so behind it the rewrite gives (body:a)^2.0, not ^1.8 (executed); a custom wrapper could override the hook and delegate (Similarity.java:175, public and not final). That gap may be a separate issue; it was not judged.
• Effect. Wrong scores, silently: the repeated term contributes n * s instead of w(n) * s, about 5-10% of the total in the small examples and a factor of 4.84 for a term repeated 50 times next to two other terms (2.1188598 at msm 1, 10.250274 at msm 2). Inside the window the repeated SHOULD term contributes exactly its k3-disabled amount. When those are the query's only duplicates (the repro and every example here), the whole score equals the k3-disabled score; duplicates that the rewrite still merges (MUST ones) stay saturated. k3 only ever lowers scores (w(n) <= n), so no score goes above Lucene's default. Which documents match does not change and nothing throws. No check showed two documents swapping rank: scores change, and with them possibly the ranking.
• Consistency. For one document and one query text the score is not monotone in msm: higher at msm 2 than at msm 1 or at msm 3.
• Sibling, not part of this claim. Duplicates split across occurs (+a a) are never merged: linear at msm 0, saturated at msm 1, because a single SHOULD clause with msm 1 becomes MUST and is merged. The recommended fix does not change that case.
• No release has k3, so a fix before 11.0.0 means no release ever ships the bug.

The similarity is set explicitly on the writer and the searcher, so the framework's random similarity does not apply; the framework still randomizes the codec, locale and time zone, which do not affect this one-document score (two seeds tried). ByteBuffersDirectory, a plain IndexSearcher, one thread. The query is built directly, without QueryBuilder, so no fraction arithmetic is involved.

Regression test: this same test; it passes with the recommended fix.

cp $REPRO/TestK3SaturationMinShouldMatch.java $LUCENE/lucene/core/src/test/org/apache/lucene/search/
cd $LUCENE && ./gradlew :lucene:core:test --tests TestK3SaturationMinShouldMatch -Ptests.seed=DEADBEEF -Ptests.asserts=true
# assertions off fails the same way: -Ptests.asserts=false

# gradle, stock 645d4fe14a20, -Ptests.seed=DEADBEEF -Ptests.asserts=true (stack trimmed; -Ptests.asserts=false identical)
> Task :lucene:core:test FAILED

TestK3SaturationMinShouldMatch > testDuplicateShouldTermSaturatedAtMinShouldMatch2 FAILED
    java.lang.AssertionError: score of 'a b' at msm=2 vs msm=1 expected:<0.3661408> but was:<0.39229372>
        at __randomizedtesting.SeedInfo.seed([DEADBEEF:E5635D477A7341F3]:0)
        at org.junit.Assert.assertEquals(Assert.java:577)
        at org.apache.lucene.search.TestK3SaturationMinShouldMatch.testDuplicateShouldTermSaturatedAtMinShouldMatch2(TestK3SaturationMinShouldMatch.java:57)

# each term scores s = 0.13076457 on this index: 1.8 s + s = 0.3661408 (saturated), 2 s + s = 0.39229372 (linear)

• The contract. The k3 @param on BM25Similarity (:44-46) and StableTflSimilarity (:103-105) has no msm condition. The #15818 description: "Saturation is applied in BooleanQuery.rewrite() through a new Similarity.computeQueryTermWeight(int qtf) method, which BM25Similarity overrides. This works transparently regardless of which query parser or programmatic API produced the query."
• The one documented exception is different. Explicit boosts are summed linearly: a code comment (BooleanQuery.java:740-742) and TestBooleanRewrites#testDeduplicateWithExplicitBoostsFallsBackToLinearSum (:1173). The upstream k3 tests use msm 0 only (:1137, :1153), and none of the #15818 review comments mentions minimumNumberShouldMatch.
• An existing upstream test expects the same. TestBooleanMinShouldMatch#testRandomQueries (:312-360), a randomized regression test (not API documentation), checks that adding a minimumNumberShouldMatch to a random query leaves the score of a document that still matches unchanged (assertSubsetOfSameScores, :363); its comment cites "(field:v field:v field:v) gets rewritten into field:v^3" (:398-399). As configured it cannot see k3: its searcher uses the framework's AssertingSimilarity(RandomSimilarity) (newSearcher, LuceneTestCaseParent.java:2638; SetupAndRestoreStaticEnv.java:230), and neither wrapper overrides computeQueryTermWeight (RandomSimilarity is a PerFieldSimilarityWrapper, RandomSimilarity.java:68), so the rewrite always uses the linear default; its BM25 entry also has k3 off (:123). Adding a k3 BM25 to RandomSimilarity would not exercise this bug. With BM25 k3 = 8 set on the searcher the same check finds 6 violations in 2,000 queries (0 with k3 off): 2 are this bug, 4 the +a a sibling.
• Precedent. #5368 / LUCENE-4300 ("BooleanQuery inconsistently applies coord() if it rewrites itself"): a score that depended on the rewrite shape, caught by the same invariant test, was fixed.

The strongest case for "intended": k3 is defined by its mechanism. The hook's javadoc says it is "used during query rewriting", the PR says "Saturation is applied in BooleanQuery.rewrite()", and the SHOULD merge carries a deliberate, tested guard: TestBooleanRewrites#testDeduplicateShouldClauses (:610) asserts that (foo:bar foo:bar foo:quux)~2 rewrites to itself (:634-642). In the #15818 review rmuir called the boost handling "a bit odd and difficult to understand" and said that processing qtf separately from the boost "would create a much more invasive change", and added "This approach could use some fresh eyes and thoughts before committing to it"; the merged implementation kept the rewrite-based design. The hook is experimental, and Lucene does not promise comparable scores across different queries.

Why it fails: the guard explains why the clauses cannot be merged, not why the weight is dropped. The user-facing @param and the PR promise saturation regardless of how the query was built. For one document and one query text the score is not monotone in msm, which no review comment mentions. And a way to apply the weight without changing matching exists (the recommended fix); testDeduplicateShouldClauses stays green with it. Upstream may still reasonably prefer a javadoc caveat; that is the maintainers' call.

Option A was built and run through gradle. Option B, the hunt's first fix, scores correctly but makes non-scoring rewrites loop forever, so it is rejected. C (a javadoc caveat) is the no-risk alternative; D would also cover the +a a sibling but needs its own design.

In the BooleanWeight constructor (BooleanWeight.java:49-62), when scores are needed and minimumNumberShouldMatch > 1, count the unboosted SHOULD occurrences of each query; a query that occurs n >= 2 times, and never with an explicit boost, gets each clause weight created with boost * computeQueryTermWeight(n) / n (+47/-1 lines, BooleanWeight.java only).

float clauseBoost = boost;
if (c.occur() == Occur.SHOULD) {
  // computeQueryTermWeight(n) / n for an unboosted query that occurs n >= 2 times, msm > 1
  clauseBoost *= duplicateShouldWeights.getOrDefault(c.query(), 1f);
}
Weight w = searcher.createWeight(
    c.query(), c.isScoring() ? scoreMode : ScoreMode.COMPLETE_NO_SCORES, clauseBoost);

Trade-offs

• Matching unchanged. The clauses and msm stay as they are, so exactly the same documents match. Equal clauses match the same documents, so a document matches all n occurrences or none, and the n split weights add up to the merged weight (up to float rounding).
• Rewrite unchanged. The rewrite is not touched, so count(), ConstantScoreQuery and FILTER rewrites converge exactly as on stock main; that is where option B fails.
• Same rules as the merge. Explicitly boosted duplicates stay linear, as in BooleanQuery.java:740-742; with k3 off the factor is 1; with msm <= 1 nothing changes, since the rewrite already merged.
• Scope. It does not change the +a a sibling (see option D).
• Cost. A few small hash collections per scoring BooleanWeight with msm > 1; no benchmark was run.

What the checks validated

Applied to a scratch worktree of 645d4fe14a20 and run through gradle with OpenJDK 25.0.3, seed DEADBEEF (2026-10-31):

• stock: the minimal test fails with assertions on and off; the intended-behaviour check's re-run of the upstream msm score test finds 6 violations with k3 = 8, 0 with k3 off;
• with the fix: the minimal test passes with assertions on and off; the finder's BM25 + StableTfl repro (assertions on and off), the independent reproduction's 5 tests and the intended-behaviour check's window test pass (standalone runner, same fix);
• validation-only checks: count(q) and count(new ConstantScoreQuery(q)) on (a a b)~2 return 2 and the scoring rewrite still returns the query unchanged; deep CheckHits.checkExplanations passes for msm 0-3; SHOULD a x3, b, c scores the same for msm 0-5; explicitly boosted duplicates stay linear; k3-off scores unchanged;
• the invariant re-run: 4 violations left, all msm 1 queries with the duplicate split across occurs or nesting (the +a a sibling), 0 with k3 off;
• TestBooleanQuery, TestBooleanRewrites, TestBooleanMinShouldMatch, TestBoolean2, TestBooleanScorer, TestBooleanOr, TestBM25Similarity, TestStableTflSimilarity, TestQueryRescorer, TestSimilarity: 147 tests, 0 failures;
• the whole core org.apache.lucene.search test package: 214 classes, 2,339 tests, 0 failures (49 skipped);
• checkGoogleJavaFormat, ecjLintMain and forbiddenApisMain for core pass; the worktree was removed afterwards;
• scope: this validates the normal search path, where IndexSearcher rewrites the query before it creates weights (IndexSearcher#createWeight assumes an already rewritten query, IndexSearcher.java:970-976); code that builds weights for unrewritten queries was not checked.

The hunt's first fix wraps each duplicate SHOULD clause in BoostQuery(q, computeQueryTermWeight(n) / n) during the rewrite when msm > 1. It fixes the scores and passed 99 upstream tests.

Trade-offs

BooleanQuery.rewriteNoScoring strips the boosts again (BooleanQuery.java:228-231, reached from ConstantScoreQuery.rewrite, ConstantScoreQuery.java:44-62), the scoring rewrite adds them back, and IndexSearcher.rewrite loops until it gets the same object back (IndexSearcher.java:871-878). With this patch IndexSearcher.count on an ordinary (a a b)~2 query never returns (20 s timeout; stock main returns). Any rewrite-time fix must keep non-scoring rewrites convergent.

Say in the k3 @param of both similarities and in Similarity#computeQueryTermWeight that saturation applies only where BooleanQuery merges duplicates (duplicate SHOULD clauses only when minimumNumberShouldMatch <= 1).

Trade-offs

No code risk, but the scores keep depending on msm, and the score expectation of TestBooleanMinShouldMatch stays false with k3 on the searcher. A maintainer could reasonably choose it. Not run.

Do option A's counting across SHOULD and MUST occurrences of the same query, which would also cover +a a.

Trade-offs

It has to interact with the MUST merge, which already turns +a +a into +a^1.8, and with explicit boosts, so it needs its own design and tests.

Method: semi-formal (the hunt's tier for a hypothesis formed during modelling and confirmed by execution). The hunt unit covered BooleanQuery rewrite and dispatch.

• Rewrite model. A Z3 model of 47 rewrite obligations; obligation R9 ("SHOULD dedup when msm <= 1" preserves matching) is proved, and its mutant R9m ("when msm <= 2") has the counterexample msm = 2 with two equal SHOULD clauses. While writing R9 the finder saw that the k3 weight is applied only inside this dedup.
• Score model. A second Z3 model: the msm 1 and msm 3 paths equal the documented k3 score (UNSAT for a difference), the msm 2 path differs (SAT), and with k3 disabled there is no difference.
• JUnit. A public-API test on the stock jar failed for BM25 and StableTfl with assertions on and off and did not compile on 10.5.2. The minimal repro above is that test cut to one document, one query shape and one assertion.

The solver's own output was not the first signal: the hypothesis came from reading the code while writing the obligation.