Lógica, Computación e IA

En la clase de hoy del curso de Razonamiento automático se han presentado los principales patrones de inducción en Isabelle: en la primera parte se ha presentado los patrones de de mostración por casos y por inducción y en la segunda parte se han presentado otros patrones (eliminación de disyunción, negación, contradicción y equivalencias).

La primera parte de la clase se ha basado en la siguiente teoría Isabelle
Leer el resto de esta entrada »

En la clase de hoy del curso de Razonamiento automático se ha estudiado:

• la transformación de la formas a formas normales prenexas, formas de Skolem y forma clausal,
• las interprestaciones de Herbrand,
• el teorema de Herbrand y
• el procedimiento de semidecisión basado en el teorema de Herbrand.

Las transparencias de la clase son las páginas 52 a 90 del tema 1.

En la clase de hoy del curso de Razonamiento automático se ha presentado la semántica de la lógica de primer orden.

Hemos empezado viendo ejemplos para ver de qué depende la verdad de una fórmula: del universo, de la interpretación de los símbolos constantes y de la asignación a las variables libres.

A partir de estos ejemplos, se introduce los conceptos de

• estructura (formadas por un universo junto con la interpretación de las constantes, funciones y relaciones),
• asignación a las variables en una estructura () e
• interpretación (formada por una estructura junto con una asignación)

A continuación, se definen los siguientes conceptos:

• valor de un término en una interpretación (),
• valor de ua fórmula en una interpretación (),
• realización de una fórmula (),
• satisfacibilidad de una fórmula en una interpretación,
• validez de una fórmula en una estructura (),
• modelo de una fórmula (),
• satisfacibilidad de una fórmula,
• validez de una fórmula (),
• realización de un conjunto de fórmulas (),
• consistencia de un conjunto de fórmulas,
• modelo de un conjunto de fórmulas (),
• consecuencia lógica (),
• equivalencia lógica (),

También se ha estudiados las relaciones entre los anteriores conceptos.

Las transparencias de la clase son las páginas 23 a 51 del tema 1.

Sudoku es un pasatiempo que se popularizó en Japón en 1986, y se dio a conocer en el ámbito internacional en 2005. El objetivo es rellenar una cuadrícula de 9 × 9 celdas (81 casillas) dividida en subcuadrículas de 3 × 3 (llamadas “cajas” o “regiones”) con las cifras del 1 al 9 partiendo de algunos
números ya dispuestos en algunas de las celdas. No se debe repetir ninguna cifra en una misma fila, columna o region. Un sudoku está bien planteado si la solución es única.

Un ejemplo de sudoku bien planteado es el siguiente:

En este ejemplo, la casilla destacada se encuentra en la fila 3, la columna 3 y la caja 1. Su valor no puede ser

• 1, 5, 6 ni 8: pues dichos valores ya se encuentran en la misma fila
• 3 ni 9: pues dichos valores ya se encuentran en la misma columna
• 4 ni 7: pues dichos valores ya se encuentran en la misma región

A partir de esta información se puede deducir que el valor de dicha casilla tiene que ser 2

El objetivo de este trabajo es implementar un programa CLIPS que resuelva un Sudoku de forma deductiva, es decir, deduciendo el valor de una casilla a partir de reglas que analicen los posibles valores de las casillas relacionadas.

Para ello se proporciona un fichero ejemplos.txt que contiene 100 Sudokus bien planteados con el siguiente formato:


# Sudoku 23
94---6-2-
-7---5-4-
68-1--5--
1-947---3
8-----7--
---2---5-
---89---1
--37--6--
---------


Donde la primera línea tiene que comenzar con # y contiene una descripción del pasatiempo (procedencia, tipología o dificultad) y las restantes 9 líneas se corresponden con las filas del Sudoku, donde un número indica un valor inicial para una casilla y el símbolo - indica que la casilla correspondiente está vacía.

También se proporciona un fichero base sudoku en el que se definen los siguientes constructores:

• Una plantilla celda para almacenar la información sobre las celdas del tablero:

  (deftemplate celda
    (slot fila)
    (slot columna)
    (slot caja)
    (slot valor
      (default 0))
    (multislot rango
      (default (create$ 1 2 3 4 5 6 7 8 9))))
  

  • Los campos fila, columna y caja sirven para almacenar los números de fila, columna y caja en las que se encuentra la celda.
  • El campo valor sirve para almacenar el valor deducido para la celda
  • El campo rango sirve para almacenar los posibles valores que pueden aparecer en la celda
• Una regla inicializa-valores para generar las representaciones de todas las celdas de un Sudoku vacío

  (defrule inicializa-valores
    (declare (salience 50))
    =>
    (assert (lee-ejemplo))
    (loop-for-count (?i 1 9)
      (loop-for-count (?j 1 9)
        (assert (celda (fila ?i)
                (columna ?j)
                (caja (caja ?i ?j)))))))
  

  • La función caja calcula el número de caja de una celda situada en la fila ?i y la columna ?j
  • La regla tiene prioridad 50 ((declare (salience 50))) para asegurar que es la primera en ser ejecutada
• Las reglas sudoku-numero y asigna-valor-inicial que junto con la función lee-sudoku sirven para cargar un ejemplo desde el fichero ejemplos.txt

  (deffunction lee-sudoku (?n)
    (open "ejemplos.txt" data "r")
    (loop-for-count (?i 1 (- ?n 1))
  		  (loop-for-count (?j 1 11) (readline data)))
    (readline data)
    (loop-for-count
     (?i 1 9)
     (bind ?fila (readline data))
      (loop-for-count
      (?j 1 9)
      (bind ?v (sub-string ?j ?j ?fila))
      (if (not (eq ?v "-"))
  	then (assert (valor-inicial ?i ?j
                                      (nth 1 (explode$ ?v)))))))
    (close data))
  

  (defrule sudoku-numero
    (declare (salience 50))
    ?h <- (lee-ejemplo)
    =>
    (retract ?h)
    (printout t "Que problema quieres resolver (1-100): ")
    (lee-sudoku (read)))
  

  (defrule asigna-valor-inicial
    (declare (salience 50))
    ?h1 <- (celda (fila ?i) (columna ?j))
    ?h2 <- (valor-inicial ?i ?j ?v)
    =>
    (retract ?h2)
    (modify ?h1 (rango ?v) (valor ?v)))
  

  • Las reglas tiene prioridad 50 ((declare (salience 50))) para asegurar que se ejecutan antes que las reglas de deducción
  • La regla sudoku-numero es la primera en ejecutarse y sólo lo hace cuando la regla de inicialización ya ha actuado.
  • La regla sudoku-numero evalúa una llamada a la función lee-sudoku que carga todos los datos del sudoku que se ha escogido como ejemplo
  • La regla asigna-valor-inicial actualiza la información de las celdas que toman un valor fijo en el planteamiento inicial del problema
• Las reglas imprime-sudoku e imprime-celda que sirven para imprimir en pantalla el estado actual del Sudoku

  (defrule imprime-sudoku
    (declare (salience 50))
    ?h <- (imprime)
    =>
    (printout t "+---+---+---+" t "|")
    (retract ?h)
    (assert (imprime 1 1)))
  

  (defrule imprime-celda
    (declare (salience 50))
    ?h <- (imprime ?i ?j)
    (celda (fila ?i) (columna ?j) (valor ?v))
    =>
    (retract ?h)
    (if (= ?v 0)
        then (printout t " ")
      else (printout t ?v))
    (if (= (mod ?j 3) 0)
        then (printout t "|"))
    (if (= (mod ?j 9) 0)
        then (printout t t))
    (if (and (= (mod ?i 3) 0) (= (mod ?j 9) 0))
        then (printout t "+---+---+---+" t))
    (if (and (= (mod ?j 9) 0) (not (= ?i 9)))
        then (printout t "|")
      (assert (imprime (+ ?i 1) 1))
      else (assert (imprime ?i (+ ?j 1)))))
  

  • Las reglas tiene prioridad 50 ((declare (salience 50))) para asegurar que se ejecutan antes que las reglas de deducción
  • La regla imprime-sudoku es la primera en ejecutarse y sólo lo hace cuando se añade el hecho (imprime)
  • La regla imprime-celda imprime una celda del tablero y fuerza a que se repita la ejecución con la celda siguiente
• La regla presenta-sudoku-inicial que sirve para presentar en pantalla la situación inicial del Sudoku que se haya cargado desde el fichero ejemplos.txt

  (defrule presenta-sudoku-inicial
    (declare (salience 40))
    (not (valor-inicial ? ? ?))
    =>
    (assert (imprime)))
  

  • La regla tiene prioridad 40 ((declare (salience 40))) para asegurar que se ejecuta después de las reglas de inicialización y lectura de pero antes que las reglas de deducción
  • Para comenzar el proceso de impresión en pantalla del estado del Sudoku basta con añadir el hecho (imprime)

Objetivos del trabajo

El trabajo consiste en desarrollar un conjunto de reglas para resolver un Sudoku de forma deductiva, es decir, determinando el valor de una celda o eliminando posibles valores de su rango. Estas reglas no deben tener prioridad asociada (salvo causa debidamente justificada).

En la página web http://www.sudoku.org.uk/SolvingSudoku.asp se puede encontrar una descripción detallada de diversas reglas deductivas para resolver un Sudoku. En el trabajo se pide implementar las siguientes reglas deductivas allí mencionadas: naked pairs, naked triples, hidden pairs, hidden triples, pointing pairs (intersection removal, box reduction, line reduction), x-wing, sword-fish, y-wing, xyz-wing y wxyz-wing.

El sistema de producción resultante debe ser capaz de resolver correctamente los 100 problemas propuestos en el fichero ejemplos.txt.

Criterios de evaluación

Los criterios de evaluación serán los siguientes:

• El número y la corrección de las reglas deductivas implementadas
• Claridad y buen estilo de programación CLIPS
• Documentación del trabajo

En la clase de hoy del curso de Razonamiento automático se ha comenzado el estudio de la lógica de primer orden.

En primer lugar hemos visto cómo se puede usar la lógica de primer orden para la representación de conocimiento. Como ejemplo hemos visto la representación del mundo de los bloques y su uso en problemas de planificación.

Basándonos en los ejemplos anteriores hemos introducido la sintaxis de la lógica de primer orden, resaltando la naturaleza recursiva de las definiciones.

Las transparencias de la clase son las 23 primeras del tema 1.