Certifierande algoritm

Inom teoretisk datavetenskap är en certifierande algoritm en algoritm som, tillsammans med en lösning på problemet den löser, ger ett bevis på att lösningen är korrekt. En certifieringsalgoritm sägs vara effektiv om den kombinerade körtiden för algoritmen och en provkontroll är långsammare med högst en konstant faktor än den mest kända icke-certifierande algoritmen för samma problem.

Beviset som produceras av en certifierande algoritm borde i någon mening vara enklare än själva algoritmen, för annars kan vilken algoritm som helst anses vara certifierande (med dess utdata verifierad genom att köra samma algoritm igen). Ibland formaliseras detta genom att kräva att en verifiering av beviset tar kortare tid än den ursprungliga algoritmen, medan för andra problem (särskilt de för vilka lösningen kan hittas i linjär tid) anses enkelheten för utdatabeviset i ett mindre formellt känsla. Till exempel kan giltigheten av utdatabeviset vara mer uppenbart för mänskliga användare än algoritmens korrekthet, eller så kan en kontrollör för beviset vara mer mottaglig för formell verifiering .

Implementeringar av certifierande algoritmer som även inkluderar en kontrollör för beviset som genereras av algoritmen kan anses vara mer tillförlitliga än icke-certifierande algoritmer. För, närhelst algoritmen körs, händer en av tre saker: den producerar en korrekt utdata (det önskade fallet), den upptäcker en bugg i algoritmen eller dess implikation (oönskat, men i allmänhet att föredra framför att fortsätta utan att upptäcka felet), eller både algoritmen och kontrollen är felaktiga på ett sätt som maskerar buggen och förhindrar att den upptäcks (oönskat, men osannolikt eftersom det beror på att det finns två oberoende buggar).

Exempel

Många exempel på problem med kontrollerbara algoritmer kommer från grafteorin . Till exempel skulle en klassisk algoritm för att testa om en graf är tvådelad helt enkelt mata ut ett booleskt värde: sant om grafen är tvådelad, annars falskt. Däremot kan en certifieringsalgoritm mata ut en 2-färgning av grafen om den är tvådelad, eller en cykel med udda längd om den inte är det. Varje graf är tvådelad om och endast om den kan vara 2-färgad, och icke-tvådelad om och endast om den innehåller en udda cykel. Både att kontrollera om en 2-färgning är giltig och att kontrollera om en given sekvens med udda längder av hörn är en cykel kan utföras enklare än att testa bipartiteness.

Analogt är det möjligt att testa om en given riktad graf är acyklisk genom en certifierande algoritm som matar ut antingen en topologisk ordning eller en riktad cykel. Det är möjligt att testa om en oriktad graf är en ackordsgraf genom en certifieringsalgoritm som matar ut antingen en elimineringsordning (en ordning av alla hörn så att, för varje hörn, de grannar som är senare i ordningen bildar en klick ) eller en ackordlös cykel. Och det är möjligt att testa om en graf är plan med en certifierande algoritm som matar ut antingen en plan inbäddning eller en Kuratowski-subgraf .

Den utökade euklidiska algoritmen för den största gemensamma divisorn av två heltal x och y är certifierande: den matar ut tre heltal g (divisorn), a , och b , så att ax + by = g . Denna ekvation kan bara vara sann för multipler av den största gemensamma divisorn, så att testa att g är den största gemensamma divisorn kan utföras genom att kontrollera att g delar både x och y och att denna ekvation är korrekt.

Se även

• Sanitetskontroll , ett enkelt test av korrektheten av en utdata eller mellanresultat som inte krävs för att vara ett fullständigt bevis på korrekthet