El investigador Alessio Mansutti es de Udine, una ciudad del noreste de Italia, nos cuenta que es una ciudad maravillosa para vivir y que desde allí se puede llegar al mar Adriático o a los Alpes en una hora. Realizó sus estudios de licenciatura y máster en su ciudad natal, su doctorado en la École Normale Supérieure Paris-Saclay y, antes de incorporarse a IMDEA Software, fue investigador postdoctoral en la Universidad de Oxford.
Le preguntamos en qué momento decidió estudiar una carrera científica y nos dijo que no estaba seguro de haber hecho esta elección conscientemente: “Me sentí atraído por la ciencia desde niño. Por lo que recuerdo, durante la escuela primaria mis principales aficiones eran el baloncesto y hacer experimentos científicos. En aquella época, una editorial muy conocida en Italia empezó varias series de revistas quincenales de ciencia para niños (una de astronomía, otra sobre el cuerpo humano, etc.). Yo tenía casi todos los volúmenes de todas las series. Hacía todos los experimentos de estos volúmenes con mi padre, y él tenía un acuerdo con mi profesor de matemáticas para rehacer los mejores en mi clase”. A partir de ese momento, su fascinación por los temas científicos no hizo más que crecer.
En cuanto a cómo acabó haciendo el doctorado, “fue un accidente muy agradable”, dice. De hecho, había decidido lo contrario, no hacer el doctorado y ya había empezado a hacer entrevistas para algunas empresas (esto fue un poco antes de terminar su máster). Según Alessio: “Al día siguiente del Viva de mi máster recibí un correo electrónico de Angelo Montanari (uno de mis profesores universitarios en Udine) sobre la posibilidad de hacer un doctorado en París. Stéphane Demri, que más tarde se convertiría en mi director de doctorado, me invitó a pasar allí una semana. Me gustaron mucho el laboratorio y Stéphane, así que tiré mi lista de “pros y contras del doctorado” y decidí trasladarme a Francia”.
“Trabajo en lógica computacional, y actualmente sobre todo en algoritmos para teorías aritméticas. Las teorías aritméticas son lenguajes para especificar enunciados sobre números. Los algoritmos para este tipo de enunciados pueden clasificarse principalmente en cuatro grupos: algoritmos que determinan si un enunciado es verdadero o falso, algoritmos que devuelven algunas (o todas) las soluciones para las que un enunciado es verdadero, algoritmos que cuentan el número de soluciones y algoritmos que encuentran una solución óptima que satisface un enunciado determinado”, señala Mansutti.
Para Alessio, las teorías aritméticas son esenciales en varias áreas de la informática y la matemática computacional. Aporta tres ejemplos de por qué son tan importantes:
Los algoritmos para teorías aritméticas se utilizan dentro de las herramientas de Satisfiability Modulo Theories (SMT). Se trata de herramientas que hoy en día se utilizan ampliamente en la industria, en particular para la verificación y depuración de sistemas de software y hardware. Las teorías aritméticas también se utilizan en los compiladores, tanto para la comprobación de tipos como para la optimización del código.
La sociedad depende en gran medida de la resolución de problemas de optimización y planificación: los aeropuertos necesitan programar vuelos, las rutas de transporte de mercancías necesitan optimizarse, etc. Todos estos problemas de optimización y planificación pueden codificarse en teorías aritméticas y luego resolverse utilizando herramientas para estas teorías.
Recientemente, varias afirmaciones matemáticas de las que sólo se sospechaba que eran verdaderas se han demostrado utilizando solucionadores para teorías aritméticas. Para ello sólo es necesario encontrar una forma inteligente de codificar el enunciado del problema en el lenguaje de la aritmética y dejar que el solucionador se ejecute hasta su finalización. Actualmente, estos enunciados matemáticos no tienen un impacto práctico en las industrias (podrían tenerlo en el futuro), pero en todo caso, demuestran cómo los solucionadores son hoy en día capaces de encontrar soluciones a problemas que ni siquiera los expertos son capaces de resolver.
