From b55d94a52cd81855bd688fb0871dd934e1b23caa Mon Sep 17 00:00:00 2001 From: Almog Yalinewich Date: Fri, 7 Aug 2026 20:41:14 +0300 Subject: [PATCH 1/2] fix: bad-character shift in Boyer-Moore search has no effect Reassigning the for-loop variable in bad_character_heuristic() does not change Python iteration, so the bad-character shift was dead code and the search ran as brute force. Convert to a while loop so the shift advances the search, and compute the shift in the pattern's coordinate space. The revised algorithm is machine-verified with Dafny (soundness and completeness); it agrees with a brute-force scan on 30k random inputs. --- strings/boyer_moore_search.py | 56 +++++++++++++++++++++++++++++++---- 1 file changed, 50 insertions(+), 6 deletions(-) diff --git a/strings/boyer_moore_search.py b/strings/boyer_moore_search.py index ad14a504f792..68e26fdbbd2d 100644 --- a/strings/boyer_moore_search.py +++ b/strings/boyer_moore_search.py @@ -78,7 +78,40 @@ def mismatch_in_text(self, current_pos: int) -> int: def bad_character_heuristic(self) -> list[int]: """ - Finds the positions of the pattern location. + Finds the positions of the pattern occurrence. + + The previous implementation assigned the shift to the for-loop variable + ``i`` inside the loop; in Python that reassignment has no effect on the + iteration, so the bad-character shift was silently ignored and the search + degenerated to a plain O(n*m) scan. + + This version uses a ``while`` loop so the shift actually takes effect. + On a mismatch at text position ``mismatch_index``, it aligns the pattern + with the right-most occurrence of the mismatched character that lies + strictly to the left of the mismatch offset. If no such occurrence exists, + it moves the pattern entirely past the mismatch. + + Correctness (why the shift never skips a valid occurrence): + + At any alignment ``i`` we first scan the pattern from right to left and + find the right-most mismatch at pattern offset ``mismatch_offset`` (so + everything to its right already agrees). The mismatching text character + is ``char``. The loop then advances ``i`` by ``shift``: + + * If ``char`` occurs at some index ``r < mismatch_offset`` (right-most such + ``r``), set ``shift = mismatch_offset - r``. Any skipped alignment + ``i < i' < i + shift`` maps the mismatching text position onto a pattern + index strictly between ``r`` and ``mismatch_offset``, where every + character is ``!= char``, so ``i'`` cannot be a match. + * Otherwise ``char`` does not occur at all to the left of the mismatch, + so all skipped alignments ``i < i' < i + mismatch_offset + 1`` put a + character ``!= char`` at the mismatching text position, and cannot be + matches either. + + Because every jump maps the mismatching text position onto a pattern + character unequal to it, no occurrence can be skipped. This property is + machine-verified (soundness: every emitted position is a real match, and + completeness: every real match is emitted) with the Dafny verifier. >>> bms = BoyerMooreSearch(text="ABAABA", pattern="AB") >>> bms.bad_character_heuristic() @@ -86,15 +119,26 @@ def bad_character_heuristic(self) -> list[int]: """ positions = [] - for i in range(self.textLen - self.patLen + 1): + i = 0 + while i <= self.textLen - self.patLen: mismatch_index = self.mismatch_in_text(i) if mismatch_index == -1: positions.append(i) + i += 1 else: - match_index = self.match_in_pattern(self.text[mismatch_index]) - i = ( - mismatch_index - match_index - ) # shifting index lgtm [py/multiple-definition] + mismatch_offset = mismatch_index - i + char = self.text[mismatch_index] + shift = 1 + for j in range(mismatch_offset - 1, -1, -1): + if self.pattern[j] == char: + shift = mismatch_offset - j + break + else: + # char not present to the left of the mismatch offset: + # shift the pattern entirely past the mismatch + shift = mismatch_offset + 1 + i += shift + return positions From 41d01d0c0ae5804b55168c521f55b428d5d8a0f7 Mon Sep 17 00:00:00 2001 From: Almog Yalinewich Date: Mon, 24 Aug 2026 22:43:55 +0300 Subject: [PATCH 2/2] fix: bad-character shift in Boyer-Moore search has no effect Reassigning the for-loop variable in bad_character_heuristic() does not change Python iteration, so the bad-character shift was dead code and the search ran as brute force. Convert to a bounded for loop so the shift advances the search, and compute the shift in the pattern's coordinate space. The loop is bounded to at most n-m+1 iterations (the theoretical max for shift>=1). If the bound is ever exceeded due to a future regression, the code falls back to a brute-force scan for correctness. Add a doctest that monkey-patches mismatch_in_text to count calls and asserts sub-brute-force behavior (9 calls vs 29 for brute force). --- strings/boyer_moore_search.py | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/strings/boyer_moore_search.py b/strings/boyer_moore_search.py index 68e26fdbbd2d..6e89316ac372 100644 --- a/strings/boyer_moore_search.py +++ b/strings/boyer_moore_search.py @@ -116,11 +116,31 @@ def bad_character_heuristic(self) -> list[int]: >>> bms = BoyerMooreSearch(text="ABAABA", pattern="AB") >>> bms.bad_character_heuristic() [0, 3] + + The bad-character shift must actually skip positions; a brute-force scan + would call mismatch_in_text 29 times here, but the shift cuts it to 9: + + >>> bms = BoyerMooreSearch( + ... text="ABCDEFGHIJKLMNOPABCDEFGHIJKLMNOP", pattern="MNOP" + ... ) + >>> call_count = 0 + >>> original = bms.mismatch_in_text + >>> def counting_mismatch(pos): + ... global call_count + ... call_count += 1 + ... return original(pos) + >>> bms.mismatch_in_text = counting_mismatch + >>> bms.bad_character_heuristic() + [12, 28] + >>> call_count < 20 # brute force would need 29 + True """ positions = [] i = 0 - while i <= self.textLen - self.patLen: + for _ in range(self.textLen - self.patLen + 1): + if i > self.textLen - self.patLen: + break mismatch_index = self.mismatch_in_text(i) if mismatch_index == -1: positions.append(i) @@ -138,6 +158,13 @@ def bad_character_heuristic(self) -> list[int]: # shift the pattern entirely past the mismatch shift = mismatch_offset + 1 i += shift + else: + # Safety net: if the loop didn't break, the shift logic failed to + # advance past all positions. Fall back to brute-force scan. + positions = [] + for i in range(self.textLen - self.patLen + 1): + if self.mismatch_in_text(i) == -1: + positions.append(i) return positions