[CATALÀ] En aquest projecte desenvolupem un SAT solver per a problemes de programació lineal entera, partint de l'algorisme de DPLL i extenent-lo per a que suporti variables enteres. Després afegim noves funcionalitats i comparem el resultat amb altres mètodes que resolen problemes d'aquest tipus.

[CASTELLÀ] En este proyecto hemos desarrollado un SAT solver para problemas de programación lineal entera, también llamada programación entera. La programación lineal entera (ILP) es un problema NP-difícil, a diferencia de su versión racional, cuya pertenencia a la clase P fue probada en la década de los 70. Tradicionalmente, los solvers de problemas ILP utilizan el algoritmo Simplex como uno de sus ingredientes principales. Simplex, introducido por Dantzig en 1947, resuelve instancias de programación lineal (racional). Funciona siguiendo una interpretación geométrica del problema: las restricciones de nen un poliedro convexo en el espacio, y la función objetivo especifica una dirección en la cual optimizar. El algoritmo recorre los vértices del poliedro hasta encontrar uno optimo, que puede no ser entero. Para que Simplex pueda resolver problemas de programación lineal entera, hay que usar técnicas adicionales como añadir nuevas restricciones (cutting planes) o usar métodos basados en branch and bound. Nuestro enfoque es diferente. Nuestro solver, Intsat, es un SAT solver en el cual las variables son enteras. Para desarrollarlo hemos extendido el algoritmo DPLL para que soporte variables enteras. En esta memoria explicaremos el procedimiento e implementación, y presentaremos resultados de la comparación entre intsat y otros programas como cutsat o cplex.

[ANGLÈS] In this project we have developed a SAT solver that solves integer programming problems. We have taken the DPLL algorithm and we have extended it to support integer variables. After that, we have added extra functionalities and we have compared it to other solvers that also solve ILP problems.