Descripción del proyecto
LOS PROBLEMAS COMBINATORIOS APARECEN POR DOQUIER EN LA VIDA COTIDIANA, SIENDO DE ESPECIAL RELEVANCIA EN EL AMBITO INDUSTRIAL (PROGRAMACION DE TAREAS INDUSTRIALES), EMPRESARIAL (PROGRAMACION DE TURNOS DE TRABAJO), ACADEMICO (PROGRAMACION DE HORARIOS), MEDICO (OPTIMIZACION DE CADENAS DE TRASPLANTE RENAL DE DONANTE VIVO), ETC, LA RESOLUCION DE ESTOS PROBLEMAS POR MEDIOS HUMANOS SUPONE GRAN ESFUERZO, Y A MENUDO LA SOLUCION OBTENIDA ESTA LEJOS DE SER OPTIMA, DEL MISMO MODO, LA MODIFICACION DE UNA SOLUCION DEBIDO A CAMBIOS IMPREVISTOS ACOSTUMBRA A TENER UN ELEVADO COSTE, POR ELLO, EL DISPONER DE METODOS COMPUTACIONALES PARA SU RESOLUCION AUTOMATICA O SEMI-AUTOMATICA SUPONE UN RETO DE GRAN INTERES SOCIAL Y ECONOMICO,COMO CONTINUACION DEL PROYECTO HELO (REF, TIN2012-33042) EN ESTE PROYECTO NOS PROPONEMOS AHONDAR EN LA APLICACION DE LA TECNOLOGIA SAT Y SMT A LOS PROBLEMAS DE PROGRAMACION (SCHEDULING) Y PLANIFICACION (PLANNING) DE TAREAS, CON ESPECIAL HINCAPIE EN LOS PROBLEMAS DE PLANIFICACION NUMERICA, POR PROBLEMAS DE PLANIFICACION NUMERICA NOS REFERIMOS A PROBLEMAS DE PLANIFICACION CON UNA MEZCLA DE VARIABLES BOOLEANAS Y NUMERICAS, REPRESENTANDO ESTAS ULTIMAS CONCEPTOS COMO DISTANCIAS, CONSUMOS, CAPACIDADES, ETC,LA MEJORA DEL MODELO DE "CAJA NEGRA", ES DECIR, EL USO DE MOTORES DE CALCULO DE AMBITO GENERAL, ESTA LIMITADA A LA MEJORA DE LAS CODIFICACIONES DE LOS PROBLEMAS AL FORMALISMO LOGICO USADO, ESTO SIGNIFICA QUE PARA IR MAS ALLA EN LA MEJORA DEL RENDIMIENTO DE LAS HERRAMIENTAS BASADAS EN LA LOGICA (SOLUCIONADORES SAT, SMT, ETC,) EN CIERTOS PROBLEMAS, PUEDE SER NECESARIO ABORDAR LA MODIFICACION DE DETERMINADOS MECANISMOS DE CALCULO INTERNOS, ES DECIR, OBSERVAR EL COMPORTAMIENTO DE ESTAS HERRAMIENTAS SEGUN LO QUE LLAMARIAMOS UN MODELO DE "CAJA DE CRISTAL" Y, A PARTIR DE AHI, ADAPTAR LOS MECANISMOS PARA FAVORECER DETERMINADAS FAMILIAS DE PROBLEMAS, EN ESTE PROYECTO PRETENDEMOS ABORDAR TANTO ASPECTOS DE REFORMULACION COMO DE MODIFICACION DE LOS MECANISMOS INTERNOS DE CALCULO DE LOS SOLUCIONADORES SAT Y SMT PARA RESOLVER PROBLEMAS COMBINATORIOS, COMO NOVEDAD, ABORDAREMOS LA ADAPTACION DE SOLUCIONADORES SAT Y SMT PARA PROBLEMAS DE PROGRAMACION Y PLANIFICACION DE TAREAS, EN EL PROYECTO ANTERIOR ESTE ASPECTO SE CONSIDERO TENTATIVAMENTE, Y SOLAMENTE PARA PROBLEMAS DE PROGRAMACION, EN EL SENTIDO DE DISEÑAR SOLUCIONADORES PARA TEORIAS ESPECIFICAS, AQUI PRETENDEMOS DARLE UN ENFOQUE UN TANTO DIFERENTE, Y MAS GENERAL, CONSISTENTE EN MODIFICAR LOS MECANISMOS INTERNOS, DADO QUE LOS SOLUCIONADORES SAT Y SMT, AUN BASANDOSE EN METODOS EXACTOS Y COMPLETOS, UTILIZAN HEURISTICAS PARA, POR EJEMPLO, ESCOGER LA SIGUIENTE VARIABLE SOBRE LA CUAL DECIDIR, QUE CLAUSULAS APRENDER DE LOS CONFLICTOS, CON QUE FRECUENCIA LLAMAR A UN DETERMINADO MODULO DE DECISION, ETC,, PENSAMOS QUE INCIDIR EN ESTOS ASPECTOS PUEDE CONLLEVAR SIGNIFICATIVAS MEJORAS EN EL RENDIMIENTO PARA DETERMINADAS FAMILIAS DE PROBLEMAS, ES DE SUPONER QUE LOS SOLUCIONADORES SMT, DISEÑADOS EN PRIMERA INSTANCIA PARA RESOLVER PROBLEMAS INDUSTRIALES DE VERIFICACION, PUEDEN SER MEJORADOS PARA PROBLEMAS DE PROGRAMACION Y PLANIFICACION DE TAREAS, DADA SU PARTICULAR ESTRUCTURA, COMO RESULTADO ESPERAMOS OBTENER SOLUCIONADORES EXACTOS Y COMPLETOS, QUE SEAN COMPETITIVOS CON SOLUCIONADORES BASADOS EN METODOS HEURISTICOS, PARA PROBLEMAS COMBINATORIOS DE GRAN INTERES COMO EL DE LA OPTIMIZACION DE CADENAS DE TRASPLANTE RENAL DE DONANTE VIVO, SAT\SMT\PROBLEMAS DE SATISFACCIÓN DE RESTRICCION\PROGRAMACIÓN Y PLANIFICACIÓN DE TAREAS\APLICACIONES