Przykłady algorytmów i dowodów, które wydają się poprawne, ale nie są

W moim wstępie do kursu programowania dowiadujemy się o metodzie inicjalizacji, konserwacji i terminacji, aby udowodnić, że algorytm działa zgodnie z oczekiwaniami. Musieliśmy jednak tylko udowodnić, że algorytm, o którym wiadomo, że jest poprawny, jest poprawny. Nigdy nie byliśmy proszeni o wykazanie, że algorytm jest nieprawidłowy.

Czy są jakieś klasyczne przykłady algorytmów, które wyglądają poprawnie, ale nie są? Szukam przypadków, w których podejście inicjalizacji-konserwacji-zakończenia wychwytuje coś, czego intuicja na pierwszy rzut oka nie ma.

ds.algorithms proofs

— Marin
źródło

Prawdopodobnie interesujące: cs.stackexchange.com/q/29475/755

— DW

Głosowanie, ponieważ uważam, że jest to bardzo ważne pytanie pedagogiczne. Jest nieco poza zakresem cstheory, ale nie znam lepszej platformy do tego, i istnieje wiele instruktorów algorytmów w społeczności cstheory. Większość kursów projektowania algorytmów naraża studentów tylko na poprawianie istniejących algorytmów oraz na problemy, które można łatwo rozwiązać za pomocą znanych technik. To wzmacnia wrażenie, tak atrakcyjne dla studentów, że można bezpiecznie zaufać intuicyjnemu odczuciu, że pozornie prawdopodobny algorytm ma rację. Dobry kurs projektowania algorytmów powinien być odwrotny!

— Neal Young

Chciałbym mieć taką kolekcję.

— Chandra Chekuri

Lokalne maksimum 2D

wejście: 2-wymiarowa tablica $n \times n$ $A$

wyjście: lokalne maksimum - para taka, że nie ma sąsiedniej komórki w tablicy, która zawiera ściśle większą wartość. $(i,j)$ $A[i,j]$

(Sąsiednie komórki to te spośród które są obecne w tablicy.) Na przykład, jeśli jest $A[i, j+1], A[i, j-1], A[i-1, j], A[i+1, j]$ $A$

\begin{array}{cccc} 0 & 1 & 3 & 4 \\ 3 & 2 & 3 & 1 \\ 2 & 5 & 0 & 1 \\ 4 & 0 & 1 & 3 \end{array}

$\begin{array}{cccc} 0&1&3&\mathbf{4}\\ \mathbf{3}&2&\mathbf{3}&1\\ 2&\mathbf{5}&0&1\\ \mathbf{4}&0&1&\mathbf{3}\end{array}$

następnie każda pogrubiona komórka jest lokalnym maksimum. Każda niepusta tablica ma co najmniej jedno maksimum lokalne.

Algorytm. Istnieje algorytm czasu : wystarczy sprawdzić każdą komórkę. Oto pomysł na szybszy, rekurencyjny algorytm. $O(n^2)$

Biorąc pod uwagę , zdefiniuj krzyż aby składał się z komórek w środkowej kolumnie i komórek w środkowym rzędzie. Najpierw sprawdź każdą komórkę w , aby zobaczyć, czy komórka jest lokalnym maksimum w . Jeśli tak, zwróć taką komórkę. W przeciwnym razie niech będzie komórką w o maksymalnej wartości. Ponieważ nie jest lokalnym maksimum, musi mieć sąsiednią komórkę o większej wartości. $A$ $X$ $X$ $A$ $(i, j)$ $X$ $(i, j)$ $(i', j')$

Partycja (tablica minus komórki w ) na cztery ćwiartki - górny lewy, prawy górny, dolny lewy i dolny prawy ćwiartki - w sposób naturalny. Sąsiednia komórka o większej wartości musi znajdować się w jednej z tych ćwiartek. Nazwij ten kwadrant . $A \setminus X$ $A$ $X$ $(i', j')$ $A'$

Lemat. Quadrant zawiera lokalne maksimum . $A'$ $A$

Dowód. Rozważ rozpoczęcie od komórki . Jeśli nie jest to lokalne maksimum, przejdź do sąsiada o większej wartości. Można to powtarzać do momentu dotarcia do komórki, która jest lokalnym maksimum. Ta ostatnia komórka musi znajdować się w , ponieważ jest ze wszystkich stron ograniczona przez komórki, których wartości są mniejsze niż wartość komórki . To dowodzi lematu. $(i', j')$ $A'$ $A'$ $(i', j')$ $\diamond$

Algorytm nazywa się rekurencyjnie na podgrupaaby znaleźć lokalne maksimum, a następnie zwraca tę komórkę. $\frac{n}{2}\times\frac{n}{2}$ $A'$ $(i, j)$

Czas przebiegu dla macierzy spełnia , więc . $T(n)$ $n\times n$ $T(n) = T(n/2) + O(n)$ $T(n) = O(n)$

W ten sposób udowodniliśmy następujące twierdzenie:

Twierdzenie. Istnieje algorytm czasu do znajdowania maksimum lokalnego w tablicy . $O(n)$ $n\times n$

A może my?

— Neal Young
źródło

W pierwszym czytaniu jedynym błędem, jaki zauważyłem, było rozwiązanie problemu powtarzalności. Czy to jedyny błąd?

— Radu GRIGore

Nawrót jest prawidłowy. Algorytm nie jest!

— Neal Young

Ach, tak, popełniłem głupi błąd z nawrotem. Widzę problem: maksimum, które udowodniłeś, nie jest (koniecznie) tym, co znajdziesz. A to, co znajdziesz, ignoruje X.

— Radu GRIGore

(\begin{matrix} 2 & 1 & 4 & 3 & 3 & 0 & 0 \\ 1 & 0 & 1 & 2 & 3 & 0 & 0 \\ 0 & 1 & 0 & 2 & 3 & 0 & 0 \\ 2 & 2 & 2 & 2 & 2 & 2 & 2 \\ 3 & 3 & 3 & 2 & 3 & 3 & 3 \\ 0 & 0 & 3 & 2 & 3 & 0 & 0 \\ 0 & 0 & 3 & 2 & 3 & 0 & 0 \end{matrix})

$\begin{pmatrix}2&1&4&3&3&0&0\\1&0&1&2&3&0&0\\0&{\color{red}1}&0&2&3&0&0\\2&2&2&2&2&2&2\\3&3&3&2&3&3&3\\0&0&3&2&3&0&0\\0&0&3&2&3&0&0\end{pmatrix}$

A^{'}

$A'$

A

$A$