Demostración de reducibilidad entre problemas utilizando Dafny

Abstract

En este trabajo se pretende demostrar la reducibilidad polinómica entre problemas NP-completos utilizando un lenguaje formal. En particular se utiliza el lenguaje Dafny, que permite especificar y verificar programas que contienen instrucciones tanto imperativas como funcionales. Primero se hará una introducción al lenguaje de programación Dafny, la NPcompletitud, los problemas que se verán a lo largo del trabajo y la reducibilidad polinómica. A continuación se formalizan las definiciones de los problemas y se implementan métodos de verificación polinómicos que demuestran la pertenencia de los problemas al conjunto NP. Finalmente se definen las transformaciones polinómicas entre dichos problemas que permiten demostrar la reducibilidad polinómica entre ellos.The aim of this paper is to prove polynomial reducibility between NP-complete problems using a formal language. In particular, the Dafny language is used, which allows to specify and verify programs containing both imperative and functional instructions. First, an introduction to the Dafny programming language, NP-completeness, the problems that will be seen throughout the paper, and polynomial reducibility will be given. Then the definitions of the problems are formalized and polynomial verification methods that prove the membership of the problems to the NP-set are implemented. Finally, we define the polynomial transformations between these problems that allow us to prove polynomial reducibility between them.