Archivo de la categoría: Otter

Una experiencia programando en Otter.

Este programa lo conocí durante mi formación académica dentro de una asignatura donde veíamos sistemas de razonamiento automático. Siempre he pensado que el conocer diversos lenguajes de programación y sistemas o programas te dan la posibilidad de afrontar un mismo problema desde diversos puntos de vista y que lo que aprendes con lenguajes funcionales te puede ser útil del mismo modo que lo que te aportan los lenguajes imperativos, no me gusta hablar de que algo es mejor o peor, son maneras diferentes de afrontar problemas y te permiten afrontar los problemas con una batería más amplia, más completa de soluciones.

En este caso trataré el sistema Otter. Para aquellos que no lo conozcan decir que Otter es un demostrador automático para la Lógica de Primer Orden con Igualdad, es un demostrador automático por refutación, esto es, busca una contradicción en un conjunto de fórmulas, dando como resultado una prueba en forma de secuencia de fórmulas indicando como se obtienen a partir de las anteriores o de las de partida.  El programa, el manual y algunos ejemplos los podéis encontrar en el siguiente enlace Otter, está en inglés y pertenece a William McCune su desarrollador; también podemos encontrar recursos en este otro enlace Otter altenativo, que también está en inglés; pudiéndose encontrar versiones tanto para Linux como para Windows. Como curiosidad decir que el nombre del sistema Otter en español quiere decir nutria y es este animal el que encontraremos en el segundo de los enlaces como imagen del programa, aunque Otter es un acronimo de Organized Techniques for Theorem-proving and Effective Research.

El problema sobre el que trabajamos para encontrar la solución es un puzle al que denominamos el atasco. Dicho puzle lo podemos encontrar en El Profesor Layton y la Villa Misteriosa siendo el puzle denominado el aparcamiento; aunque es una versión más compleja que el que mostraré, es igualmente resoluble con este sistema sólo habría que implementarlo adecuadamente.

La idea del puzle es que tenemos una serie de piezas en un tablero y queremos sacar en concreto una de ellas por una zona concreta del tablero y solo pudiendo hacer desplazamientos horizontales o verticales de las piezas.

otter1En los casos solucionados siempre se busca llevar la pieza cero al hueco en la esquina inferior derecha del tablero, es algo que todos podemos hacer manualmente, pero que conforme aumentamos el tamaño del tablero y el número de piezas puede llevarnos cierto tiempo.

La complejidad de la solución reside en encontrar una manera de representar el problema correctamente de manera que podamos identificar los movimientos que hay que hacer para llegar a la solución. Toda la representación y las soluciones con una explicación detallada a las variaciones que se ven en la siguiente galería se pueden encontrar en el siguiente archivo solución atasco.

Con respecto a las soluciones hay que tener en cuenta que el sistema busca la solución que menos pasos da para llevar la pieza al objetivo, lo que no quiere decir que tarde poco en encontrarla de hecho hubo una solución que tarda unos veinte minutos para estas dimensiones, hace una busqueda exhaustiva realizando poda para no volver a situaciones repetidas pero aún así en los casos en que el sistema requiere realizar muchos movimientos tardará algo más de lo que uno quisiera, pero lo dicho a cambio tienes la solución con mínimos movimientos.

Anuncios