Proxima Charla del DC: Viernes 3/6/11- 14 hs. José Castaño - DC-FCEyN - UBA: Modelos de automata y satisfacibilidad computacional
El uso de técnicas de modelos formales con mayor poder expresivo que los lenguajes libres de contexto, pueden aportar enfoques no explorados para solucionar problemas conocidos que podrian redundar en ventajas comparativas. Dichas ventajas podrán ser cuantificadas contra bancos de prueba específicos del problema.
En particular, el modelado de problemas que requieren mayor poder expresivo, se puede realizar por construcción de un autómaton ad hoc, o por reconocimiento, es decir existe un autómaton que reconoce el lenguaje que modela este clase de problemas. En particular el problema de satisfacibilidad proposicional puede abordarse utilizando estas dos técnicas.
En el método ad-hoc se parte del hecho que los automatas de estados finitos tienen un poder expresivo suficiente para modelar el problema de satisfacibilidad proposicional. A partir de una formula en CNF se puede construir un automata de estados finitos que genera el conjunto (posiblemente vacio) de valuaciones que satisfacen la formula. Si dicha construcción no se realiza adecuadamente el costo computacional puede ser prohibitivo, ya que como es sabido el problema de intersección de automata es PSPACE-completo. A fin de realizar un proceso eficiente, deben utilizarse distintas heurísticas al modo que se utilizan distintas heurísticas en un algoritmo de búsqueda como DPLL.
En el método de uso de autómata como reconocimiento de un lenguaje, es necesario utilizar un modelo de autómata con mayor poder expresivo que el de autómata de pila ("pushdown automata"), ya que el tipo de lenguaje que puede codificar el problema de satisfacibilidad proposicional corresponde a un lenguaje con multiples dependencias cruzadas. En este caso hablaremos de un caso particular del problema de satisfacilibilidad.
Ambos abordajes están relacionados ya que un modelo de automata que reconoce este tipo de dependencias debe construir una estructura de datos que "controle" el reconocimiento.
El problema central es, al igual que un algoritmo como DPLL, cómo recortar el espacio de búsqueda.
