Algoritmos certificadores e verificadores - Marinho, Anne Rose Alves Federici. (UFRJ, 2015)
[PT]Algoritmos certificadores são algoritmos que retornam não apenas a solução para o problema que se prestam a resolver, mas também um certificado, direta e eficientemente verificável, de que tal solução é correta. Nesta dissertação, argumentamos a favor do emprego de algoritmos certificadores para a solução computacional de problemas em geral, em detrimento a algoritmos clássicos, não-certificadores. O ponto central é que os primeiros estão protegidos contra possíveis — e, certamente, comuns — erros introduzidos inadvertidamente pelo programador, ao passo que os últimos, nesses casos, apresentariam respostas imprevisíveis, provavelmente incorretas e com efeitos indesejados. O objetivo desta pesquisa foi estudar o emprego de algoritmos certificadores, divulgando a técnica e estimulando seu uso. Foram considerados (analisados e implementados) quatro problemas: o problema do reconhecimento de grafos bipartidos e o do emparelhamento de cardinalidade máxima, ambos já descritos na literatura de algoritmos certificadores; o problema da seleção dos k menores elementos de uma lista (k-selection); e o problema do reconhecimento de grafos de disco unitário. Esses dois últimos problemas fogem intencionalmente do padrão do algoritmo certificador que provê um certificado que pode ser verificado de forma muita simples e eficiente, pois, no primeiro caso, o certificado é a própria saída do algoritmo, que se presta imediatamente à verificação (como ocorre, na prática, em muitas situações), e no segundo caso, a verificação não é formalmente eficiente (por demandar tempo exponencial), mas pode ser computacionalmente viável para instâncias pequenas, permitindo, por exemplo, ser usada em provas computacionais para teoremas.[EN]Certifying algorithms are those which return not only the solution to the problem they mean to solve, but also a correctness certificate, whose verification can be tackled in an efficient and straightforward way. In this dissertation, we argue for the use of certifying algorithms, rather than their classic, non-certifying counterparts, whenever possible. The central idea is that the former are shielded against implementation errors inadvertently introduced by the programmer, whereas the latter, in these cases, would helplessly present unforeseeable, incorrect outputs, probably with undesirable consequences. After a brief account of the theory of certifying algorithms, we look into three problems illustrative examples, highlighting the necessary care one should devote to the completeness of the verification phase. The goal of this research was to study the applicability of certifying algorithms, disclosing the technique and stimulating its use. We have considered (analysed and implemented) four problems: the recognition of bipartite graphs and the maximum-cardinality matching problem, both already tackled in the literature of certifying algorithms; the k-selection problem; and the recognition of unit disk graphs. The two latter problems intentionally deviate a little from the standard pattern of the certifying algorithm which provides a certificate that can be verified in a very simple and efficient way. In the first case, no certificate is actually called for, since the very output of the classic algorithm can be verified right away (as is the case in many practical situations); in the second case, even though the verification step cannot be undertaken in a formally efficient way (demanding exponential time), it can be computationally feasible for small instances, which shall make it suitable for theorem proofing.