Algorytm certyfikacji
W informatyce teoretycznej algorytm certyfikujący to algorytm, który wraz z rozwiązaniem problemu, który rozwiązuje, wyprowadza dowód, że rozwiązanie jest poprawne. Mówi się, że algorytm certyfikujący jest wydajny , jeśli łączny czas działania algorytmu i modułu sprawdzającego jest wolniejszy co najwyżej o stały współczynnik niż najlepszy znany algorytm niecertyfikujący dla tego samego problemu.
Dowód wygenerowany przez algorytm certyfikujący powinien być w pewnym sensie prostszy niż sam algorytm, w przeciwnym razie każdy algorytm można by uznać za certyfikujący (z jego wynikiem zweryfikowanym przez ponowne uruchomienie tego samego algorytmu). Czasami jest to sformalizowane poprzez wymaganie, aby weryfikacja dowodu zajmowała mniej czasu niż oryginalny algorytm, podczas gdy dla innych problemów (zwłaszcza tych, dla których rozwiązanie można znaleźć w czasie liniowym) prostota wyjściowego dowodu jest rozpatrywana w mniej formalny sposób sens. Na przykład ważność dowodu wyjściowego może być bardziej widoczna dla użytkowników niż poprawność algorytmu lub sprawdzanie dowodu może być bardziej podatne na formalną weryfikację .
Implementacje algorytmów certyfikujących, które obejmują również sprawdzanie dowodu generowanego przez algorytm, można uznać za bardziej niezawodne niż algorytmy niecertyfikujące. Za każdym razem, gdy algorytm jest uruchamiany, dzieje się jedna z trzech rzeczy: generuje poprawne dane wyjściowe (pożądany przypadek), wykrywa błąd w algorytmie lub jego implikację (niepożądane, ale generalnie lepsze niż kontynuowanie bez wykrycia błędu) lub zarówno algorytm, jak i moduł sprawdzający są wadliwe w sposób maskujący błąd i uniemożliwiający jego wykrycie (niepożądane, ale mało prawdopodobne, ponieważ zależy to od istnienia dwóch niezależnych błędów).
Przykłady
Wiele przykładów problemów z sprawdzalnymi algorytmami pochodzi z teorii grafów . Na przykład klasyczny algorytm sprawdzania, czy graf jest dwudzielny , po prostu zwraca wartość logiczną: prawda, jeśli wykres jest dwudzielny, w przeciwnym razie fałsz. W przeciwieństwie do tego, algorytm certyfikujący może generować 2-kolorowanie wykresu w przypadku, gdy jest on dwudzielny, lub cykl o nieparzystej długości, jeśli nie jest. Każdy graf jest dwudzielny wtedy i tylko wtedy, gdy może być dwukolorowy, a niedwudzielny wtedy i tylko wtedy, gdy zawiera nieparzysty cykl. Zarówno sprawdzenie, czy 2-kolorowanie jest prawidłowe, jak i sprawdzenie, czy dana sekwencja wierzchołków o nieparzystej długości jest cyklem, można przeprowadzić prościej niż testowanie dwudzielności.
Analogicznie, możliwe jest sprawdzenie, czy dany graf skierowany jest acykliczny, za pomocą algorytmu certyfikującego, który wyprowadza porządek topologiczny lub cykl skierowany. Możliwe jest sprawdzenie, czy graf nieskierowany jest grafem akordowym za pomocą algorytmu certyfikującego, który wyprowadza albo porządek eliminacji (uporządkowanie wszystkich wierzchołków w taki sposób, że dla każdego wierzchołka sąsiedzi, którzy są później w kolejności, tworzą klikę ) lub cykl bez akordów. I możliwe jest sprawdzenie, czy graf jest planarny , za pomocą algorytmu certyfikującego, który wyprowadza albo planarne osadzenie, albo podgraf Kuratowskiego .
Rozszerzony algorytm euklidesowy dla największego wspólnego dzielnika dwóch liczb całkowitych x i y jest poświadczający: wyprowadza trzy liczby całkowite g (dzielnik), a i b , takie że ax + by = g . To równanie może być prawdziwe tylko dla wielokrotności największego wspólnego dzielnika, więc sprawdzenie, czy g jest największym wspólnym dzielnikiem, można przeprowadzić, sprawdzając, czy g dzieli zarówno x , jak i y oraz czy to równanie jest poprawne.
Zobacz też
- Kontrola poczytalności , prosty test poprawności wyniku wyjściowego lub pośredniego, który nie musi być pełnym dowodem poprawności