[Todos] Charla del DC - José Castaño - Modelos de automata y satisfacibilidad computacional.

[Esteban Feuerstein]

Cuándo: 3/6/2011. 14:00 hs 
Dónde: Laboratorio Epsilon
Con qué: ¡Con sandwichitos!
 
Orador:  José Castaño - Depto. de Computación - FCEyN - UBA
Título: Modelos de automata y satisfacibilidad computacional

Resumen: 
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.