Defensa Tesis Licenciatura Diego Rubinstein

• Título: Resolución en paralelo para lógicas híbridas
• Director: Daniel Gorín
• Jurados: Santiago Figueira y Fernando Schapachnik
• Resumen:

Desde el surgimiento de las primeras computadoras electrónicas se ha asistido a un incremento sostenido en la velocidad de cómputo de los procesadores. Esta tendencia histórica se ha detenido en los últimos años y no se esperan avances significativos en el corto plazo. La carrera actual es por agregar más unidades de procesamiento en un mismo chip y el desafío está ahora en cómo aprovechar esta forma de procesamiento paralelo para acelerar cómputos.

En este trabajo investigamos el problema de cómo paralelizar un algoritmo para el problema de satisfacibilidad en lógicas híbridas de forma de aprovechar la ejecución en arquitecturas de multiprocesador. El algoritmo está basado en un cálculo similar al de resolución para lógica clásica; se trata, por lo tanto, de un algoritmo de saturación con estrategias de eliminación de redundancia. Proponemos una estrategia concreta de paralelización que implementamos como una extensión al prototipo HyLoRes, realizamos pruebas de performance y reportamos resultados preliminares.