Descripción del proyecto
ESTA PROPUESTA PRETENDE MEJORAR LOS RESOLUTORES DE PROGRAMACION CON RESTRICCIONES, TALES COMO LOS RESOLUTORES DE SAT Y MAXSAT, PARA PROBLEMAS COMBINATORIOS INDUSTRIALES/REALES, LOS PROBLEMAS COMBINATORIOS SE DAN DE FORMA NATURAL EN MUCHOS DOMINIOS: PLANIFICACION, VERIFICACION DE SOFTWARE Y HARDWARE, COMPILACION DE CONOCIMIENTO, MODELADO PROBABILISTICO, BIOINFORMATICA, SISTEMAS DE ENERGIA, CIUDADES INTELIGENTES, REDES SOCIALES, SOSTENIBILIDAD COMPUTACIONAL, ETC,EN LA ULTIMA DECADA SE HAN REALIZADO GRANDES AVANCES EN LA RESOLUCION DE PROBLEMAS COMBINATORIOS INDUSTRIALES GRACIAS LA APLICACION DE TECNICAS DE PROGRAMACION CON RESTRICCIONES, TALES COMO LOS RESOLUTORES DE SATISFACTIBILIDAD (SAT), SIN EMBARGO, APENAS HEMOS ARAÑADO LA PUNTA DEL ICEBERG, DESDE UN PUNTO DE VISTA TEORICO, SABEMOS QUE HAY SISTEMAS MAS POTENTES QUE EL QUE SUBYACE EN LOS RESOLUTORES DE SAT (RESOLUCION), POR LO TANTO, UN CLARO RETO PARA LA PROXIMA DECADA ES HACER PRACTICOS ESTOS SISTEMAS DE DEMOSTRACION MAS POTENTES, PERMITIENDO QUE LOS RESOLUTORES DE SAT EVOLUCIONEN AL SIGUIENTE NIVEL, EN PARTICULAR, PRIMERO ESTUDIAREMOS VERSIONES RESTRINGIDAS DE SISTEMAS COMO RESOLUCION EXTENDIDA Y REDUNDANCIA DE PROPAGACION QUE YA HAN RECIBIDO ATENCION ES ESTE SENTIDO, ADEMAS, CUALQUIER AVANCE EN LOS RESOLUTORES DE SAT PROVOCARA UNA MEJORA DE LOS RESOLUTORES DE MAXSAT (LA VERSION DE OPTIMIZACION DE SAT) Y EN OTROS TECNICAS QUE UTILIZAN LA TECNOLOGIA DE SAT COMO POR EJEMPLO LA SATISFACTIBILIDAD MODULO TEORIAS,LA CREENCIA COMUN EN LA COMUNIDAD DE SAT ES QUE LOS RESOLUTORES DE SAT MODERNOS SON TAN EFICIENTES GRACIAS A SU AUN NO BIEN COMPRENDIDA CAPACIDAD DE EXPLOTAR LA ESTRUCTURA SUBYACENTE EN LOS PROBLEMAS DEL MUNDO REAL, POR LO TANTO, LA EVOLUCION DE LOS RESOLUTORES DE SAT NO SE MATERIALIZARA A NO SER QUE PODAMOS AUTOMATIZAR LA IDENTIFICACION Y EXPLOTACION DE ESTA ESTRUCTURA, PARA TAL FIN, ESTUDIAREMOS MAS A FONDO COMO DESCUBRIR Y EXPLOTAR TANTO LA ESTRUCTURA DE LOS PROBLEMAS REALES, COMO LA ESTRUCTURA DE LA DEMOSTRACION QUE LOS RESOLUTORES DE SAT CONSTRUYEN, A TRAVES DE LA APLICACION DE TECNICAS DE RAZONAMIENTO AUTOMATICO, EN PARTICULAR, ESTUDIAREMOS COMO COMBINAR APRENDIZAJE PROFUNDO Y APRENDIZAJE POR REFUERZO, ANALISIS DE REDES COMPLEJAS Y SISTEMAS DE DEMOSTRACION MAS POTENTES, CREANDO UN TODAVIA NO EXPLORADA SINERGIA ENTRE APRENDIZAJE AUTOMATICA Y PROGRAMACION CON RESTRICCIONES,CUALQUIER NUEVA TECNICA DESARROLLADA EN LA TEMATICA DE ESTA PROPUESTA PODRIA TENER INMEDIATAMENTE UN IMPACTO RELEVANTE, TANTO EN LA COMUNIDAD DE CIENCIAS DE LA COMPUTACION, COMO EN LA INDUSTRIA, FINALMENTE, ESTA PROPUESTA TRABAJA EN DOS RETOS BIEN CONOCIDOS EN LA COMUNIDAD DE SAT, EN HENRY A, KAUTZ, BART SELMAN: TEN CHALLENGES REDUX: RECENT PROGRESS IN PROPOSITIONAL REASONING AND SEARCH, CP 2003: 1-18, PODEMOS ENCONTRAR:RETO 8: CARACTERIZAR LAS PROPIEDADES COMPUTACIONALES DE DIFERENTES CODIFICACIONES DE PROBLEMAS DEL MUNDO REAL Y/O DAR PRINCIPIOS GENERALES QUE SE DEN EN UN RANGO DE DOMINIOS,RETO 3: DEMOSTRAR QUE UN SISTEMA DE DEMOSTRACION PROPOSICIONAL MAS POTENTE QUE RESOLUCION PUEDE SER PRACTICO PARA LA RESOLUCION DEL PROBLEMA DE LA SATISFACTIBILIDAD, SATISFACCION DE RESTRICCIONES\LOGICA PROPOSICIONAL\SISTEMAS DE DEMOSTRACION\COMPLEJIDAD DE DEMOSTRACIONES