La programación de conjuntos de respuestas ( ASP ) es una forma de programación declarativa orientada a problemas de búsqueda difíciles (principalmente NP-hard ) . Se basa en la semántica del modelo estable (conjunto de respuestas) de la programación lógica . En ASP, los problemas de búsqueda se reducen a computar modelos estables y los solucionadores de conjuntos de respuestas (programas para generar modelos estables) se utilizan para realizar la búsqueda. El proceso computacional empleado en el diseño de muchos solucionadores de conjuntos de respuestas es una mejora del algoritmo DPLL y, en principio, siempre termina (a diferencia de la evaluación de consultas de Prolog , que puede conducir a un bucle infinito).
En un sentido más general, ASP incluye todas las aplicaciones de conjuntos de respuestas a la representación del conocimiento [1] [2] y el uso de la evaluación de consultas al estilo Prolog para resolver problemas que surgen en estas aplicaciones.
Historia
El método de planificación propuesto en 1993 por Dimopoulos, Nebel y Köhler [3] es un ejemplo temprano de programación de conjuntos de respuestas. Su enfoque se basa en la relación entre planes y modelos estables. [4] Soininen y Niemelä [5] aplicaron lo que ahora se conoce como programación de conjuntos de respuestas al problema de la configuración del producto . El uso de solucionadores de conjuntos de respuestas para la búsqueda fue identificado como un nuevo paradigma de programación por Marek y Truszczyński en un artículo que apareció en una perspectiva de 25 años sobre el paradigma de programación lógica publicado en 1999 [6] y en [Niemelä 1999]. [7] De hecho, Lifschitz [8] propuso por primera vez la nueva terminología de "conjunto de respuestas" en lugar de "modelo estable" en un artículo que aparece en el mismo volumen retrospectivo que el artículo de Marek-Truszczynski.
Respuesta establecer lenguaje de programación AnsProlog
Lparse es el nombre del programa que se creó originalmente como una herramienta de conexión a tierra (front-end) para los smodels de solucionador de conjuntos de respuestas . El lenguaje que acepta Lparse ahora se llama comúnmente AnsProlog, [9] abreviatura de Answer Set Programming in Logic . [10] En la actualidad se utiliza de la misma manera en muchos otros solucionadores del conjunto de respuestas, incluyendo Assat , broche , cmodels , GNT , nomore ++ y pbmodels . ( dlv es una excepción; la sintaxis de los programas ASP escritos para dlv es algo diferente).
Un programa AnsProlog consta de reglas de la forma
< cabeza > : - < cuerpo > .
El símbolo :-
("si") se elimina si está vacío; tales reglas se llaman hechos . El tipo más simple de reglas Lparse son las reglas con restricciones .
Otra construcción útil incluida en este lenguaje es la elección . Por ejemplo, la regla de elección
{ p , q , r }.
dice: elige arbitrariamente cuál de los átomos para incluir en el modelo estable. El programa Lparse que contiene esta regla de elección y ninguna otra regla tiene 8 modelos estables: subconjuntos arbitrarios de. La definición de modelo estable se generalizó a programas con reglas de elección. [11] Las reglas de elección pueden tratarse también como abreviaturas de fórmulas proposicionales bajo la semántica del modelo estable . [12] Por ejemplo, la regla de elección anterior se puede ver como una forma abreviada de la conjunción de tres fórmulas del " medio excluido ":
El lenguaje de Lparse también nos permite escribir reglas de elección "restringidas", como
1 { p , q , r } 2.
Esta regla dice: elige al menos 1 de los átomos , pero no más de 2. El significado de esta regla bajo la semántica del modelo estable está representado por la fórmula proposicional
Los límites de cardinalidad también se pueden usar en el cuerpo de una regla, por ejemplo:
: - 2 { p , q , r }.
Agregar esta restricción a un programa Lparse elimina los modelos estables que contienen al menos 2 de los átomos . El significado de esta regla se puede representar mediante la fórmula proposicional
Las variables (en mayúsculas, como en Prolog ) se utilizan en Lparse para abreviar colecciones de reglas que siguen el mismo patrón, y también para abreviar colecciones de átomos dentro de la misma regla. Por ejemplo, el programa Lparse
p ( a ). p ( b ). p ( c ). q ( X ) : - p ( X ), X ! = a .
tiene el mismo significado que
p ( a ). p ( b ). p ( c ). q ( b ). q ( c ).
El programa
p ( a ). p ( b ). p ( c ). { q ( X ): - p ( X )} 2.
es una abreviatura de
p ( a ). p ( b ). p ( c ). { q ( a ), q ( b ), q ( c )} 2.
Un rango tiene la forma:
( inicio .. fin )
donde el inicio y el final son expresiones aritméticas de valor constante. Un rango es un atajo de notación que se usa principalmente para definir dominios numéricos de una manera compatible. Por ejemplo, el hecho
a ( 1..3 ).
es un atajo para
a ( 1 ). a ( 2 ). a ( 3 ).
Los rangos también se pueden usar en cuerpos de reglas con la misma semántica.
Un literal condicional tiene la forma:
p ( X ) : q ( X )
Si la extensión de q es {q (a1), q (a2), ..., q (aN)}, la condición anterior es semánticamente equivalente a escribir {p (a1), p (a2), ..., p (aN)} en lugar de la condición. Por ejemplo,
q ( 1..2 ). a : - 1 { p ( X ) : q ( X )}.
es una abreviatura de
q ( 1 ). q ( 2 ). a : - 1 { p ( 1 ), p ( 2 )}.
Generando modelos estables
Para encontrar un modelo estable del programa Lparse almacenado en un archivo ${filename}
usamos el comando
% lparse $ { nombre de archivo } | smodels
La opción 0 indica a los smodels que busquen todos los modelos estables del programa. Por ejemplo, si el archivo test
contiene las reglas
1 { p , q , r } 2. s : - no p .
entonces el comando produce la salida
prueba % lparse | smodels 0 Respuesta: 1 Modelo estable: qp Respuesta: 2 Modelo estable: p Respuesta: 3 Modelo estable: rp Respuesta: 4 Modelo estable: qs Respuesta: 5 Modelo estable: rs Respuesta: 6 Modelo estable: rqs
Ejemplos de programas ASP
Coloración gráfica
Un - coloración de un gráfico es una función tal que por cada par de vértices adyacentes . Nos gustaría usar ASP para encontrar un-colorear un gráfico determinado (o determinar que no existe).
Esto se puede lograr usando el siguiente programa Lparse:
c ( 1 .. n ). 1 { color ( X , I ) : c ( I )} 1 : - v ( X ). : - color ( X , I ), color ( Y , I ), e ( X , Y ), c ( I ).
La línea 1 define los números ser colores. De acuerdo con la regla de elección de la línea 2, un color único debe asignarse a cada vértice . La restricción en la Línea 3 prohíbe asignar el mismo color a los vértices y si hay un borde que los conecta.
Si combinamos este archivo con una definición de , como
v (1 .. 100 ). % 1, ..., 100 son vértices e ( 1 , 55 ). % hay una ventaja de 1 a 55 . . .
y ejecutar smodels en él, con el valor numérico de especificado en la línea de comando, luego los átomos de la forma en la salida de smodels representará un -color de .
El programa de este ejemplo ilustra la organización de "generar y probar" que a menudo se encuentra en programas ASP simples. La regla de elección describe un conjunto de "soluciones potenciales", un superconjunto simple del conjunto de soluciones para el problema de búsqueda dado. Le sigue una restricción, que elimina todas las posibles soluciones que no son aceptables. Sin embargo, el proceso de búsqueda empleado por smodels y otros solucionadores de conjuntos de respuestas no se basa en prueba y error .
Gran camarilla
Una camarilla en un gráfico es un conjunto de vértices adyacentes por pares. El siguiente programa Lparse encuentra una camarilla de tamaño en un gráfico dado, o determina que no existe:
n { en ( X ) : v ( X )}.: - en ( X ), en ( Y ), v ( X ), v ( Y ), X ! = Y , no e ( X , Y ), no e ( Y , X ).
Este es otro ejemplo de la organización de generar y probar. La regla de elección en la línea 1 "genera" todos los conjuntos que constan devértices. La restricción en la Línea 2 "elimina" los conjuntos que no son camarillas.
Ciclo hamiltoniano
Un ciclo hamiltoniano en un gráfico dirigido es un ciclo que pasa por cada vértice del gráfico exactamente una vez. El siguiente programa Lparse se puede utilizar para encontrar un ciclo hamiltoniano en un gráfico dirigido dado, si existe; asumimos que 0 es uno de los vértices.
{ en ( X , Y )} : - e ( X , Y ).: - 2 { en ( X , Y ) : e ( X , Y )}, v ( X ).: - 2 { en ( X , Y ) : e ( X , Y )}, v ( Y ).r ( X ) : - en ( 0 , X ), v ( X ).r ( Y ) : - r ( X ), en ( X , Y ), e ( X , Y ).: - no r ( X ), v ( X ).
La regla de elección en la Línea 1 "genera" todos los subconjuntos del conjunto de aristas. Las tres restricciones "eliminan" los subconjuntos que no son ciclos hamiltonianos. El último de ellos usa el predicado auxiliar (" es alcanzable desde 0 ") para prohibir los vértices que no satisfagan esta condición. Este predicado se define de forma recursiva en las líneas 6 y 7.
Este programa es un ejemplo de la organización más general de "generar, definir y probar": incluye la definición de un predicado auxiliar que nos ayuda a eliminar todas las posibles soluciones "malas".
Análisis de dependencias
En el procesamiento del lenguaje natural , el análisis basado en dependencias se puede formular como un problema ASP. [13] El siguiente código analiza la oración latina "Puella pulchra in villa linguam latinam discit", "la niña bonita está aprendiendo latín en la villa". El árbol de sintaxis se expresa mediante los predicados de arco que representan las dependencias entre las palabras de la oración. La estructura calculada es un árbol enraizado ordenado linealmente.
% ********** frase de entrada ********** palabra ( 1 , puella ). palabra ( 2 , pulchra ). palabra ( 3 , en ). palabra ( 4 , villa ). palabra ( 5 , linguam ). palabra ( 6 , latinam ). palabra ( 7 , discit ). % ********** léxico ********** 1 { nodo ( X , attr ( pulcher , a , fem , nom , sg )); nodo ( X , attr ( pulcher , a , fem , abl , sg )) } 1 : - palabra ( X , pulchra ). nodo ( X , attr ( latinus , a , fem , acc , sg )) : - palabra ( X , latinam ). 1 { nodo ( X , attr ( puella , n , fem , nom , sg )); nodo ( X , attr ( puella , n , fem , abl , sg )) } 1 : - palabra ( X , puella ). 1 { nodo ( X , attr ( villa , n , fem , nom , sg )); nodo ( X , attr ( villa , n , fem , abl , sg )) } 1 : - palabra ( X , villa ). nodo ( X , attr ( linguam , n , fem , acc , sg )) : - palabra ( X , linguam ). nodo ( X , attr ( discere , v , pres , 3 , sg )) : - palabra ( X , discit ). nodo ( X , attr ( in , p )) : - palabra ( X , in ). % ********** reglas sintácticas ********** 0 { arc ( X , Y , subj ) } 1 : - nodo ( X , attr ( _ , v , _ , 3 , sg )), nodo ( Y , attr ( _ , n , _ , nom , sg )). 0 { arc ( X , Y , dobj ) } 1 : - nodo ( X , attr ( _ , v , _ , 3 , sg )), node ( Y , attr ( _ , n , _ , acc , sg )). 0 { arc ( X , Y , attr ) } 1 : - nodo ( X , attr ( _ , n , Gender , Case , Number )), node ( Y , attr ( _ , a , Gender , Case , Number )). 0 { arc ( X , Y , prep ) } 1 : - nodo ( X , atributo ( _ , p )), nodo ( Y , atributo ( _ , n , _ , abl , _ )), X < Y . 0 { arc ( X , Y , adv ) } 1 : - nodo ( X , atributo ( _ , v , _ , _ , _ )), nodo ( Y , atributo ( _ , p )), no hoja ( Y ). % ********** garantizando la estructura de árbol del gráfico ********** 1 { root ( X ) : node ( X , _ ) } 1 .: - arc ( X , Z , _ ), arco ( Y , Z , _ ), X ! = Y . : - arco ( X , Y , L1 ), arco ( X , Y , L2 ), L1 ! = L2 . camino ( X , Y ) : - arco ( X , Y , _ ). ruta ( X , Z ) : - arco ( X , Y , _ ), ruta ( Y , Z ). : - ruta ( X , X ). : - raíz ( X ), nodo ( Y , _ ), X ! = Y , no ruta ( X , Y ). hoja ( X ) : - nodo ( X , _ ), no arco ( X , _ , _ ).
Estandarización lingüística y competencia ASP
El grupo de trabajo de estandarización de ASP elaboró una especificación de lenguaje estándar, denominada ASP-Core-2, [14] hacia la cual convergen los sistemas ASP recientes. ASP-Core-2 es el lenguaje de referencia para el Concurso de programación de conjuntos de respuestas, en el que los solucionadores de ASP se comparan periódicamente con una serie de problemas de referencia.
Comparación de implementaciones
Los primeros sistemas, como Smodels, usaban el retroceso para encontrar soluciones. A medida que evolucionó la teoría y la práctica de los solucionadores de SAT booleanos , se construyeron varios solucionadores de ASP sobre los solucionadores de SAT, incluidos ASSAT y Cmodels. Estos convirtieron la fórmula ASP en proposiciones SAT, aplicaron el solucionador SAT y luego volvieron a convertir las soluciones a la forma ASP. Los sistemas más recientes, como Clasp, utilizan un enfoque híbrido, utilizando algoritmos basados en conflictos inspirados en SAT, sin conversión completa a una forma lógica booleana. Estos enfoques permiten mejoras significativas del rendimiento, a menudo en un orden de magnitud, con respecto a los algoritmos de retroceso anteriores.
El proyecto Potassco actúa como un paraguas para muchos de los sistemas siguientes, incluidos los de cierre , sistemas de puesta a tierra ( gringo ), sistemas incrementales ( iclingo ), solucionadores de restricciones ( clingcon ), lenguaje de acción para compiladores ASP ( coala ), implementaciones MPI distribuidas ( claspar ) , y muchos otros.
La mayoría de los sistemas admiten variables, pero solo indirectamente, forzando la conexión a tierra, utilizando un sistema de conexión a tierra como Lparse o gringo como interfaz. La necesidad de conexión a tierra puede provocar una explosión combinatoria de cláusulas; por lo tanto, los sistemas que realizan la puesta a tierra sobre la marcha podrían tener una ventaja.
Las implementaciones basadas en consultas de la programación de conjuntos de respuestas, como el sistema Galliwasp, [15] s (ASP) [16] ys (CASP) [17] evitan la conexión a tierra mediante el uso de una combinación de resolución y coinducción .
Plataforma | Características | Mecánica | ||||||
---|---|---|---|---|---|---|---|---|
Nombre | SO | Licencia | Variables | Símbolos de función | Conjuntos explícitos | Listas explícitas | Soporte disyuntivo (reglas de elección) | |
ASPeRiX | Linux | GPL | sí | No | puesta a tierra sobre la marcha | |||
ASSAT | Solaris | Freeware | Basado en solucionador SAT | |||||
Solucionador de conjuntos de respuestas de cierre | Linux , macOS , Windows | Licencia MIT | Si, en Clingo | sí | No | No | sí | incremental, inspirado en el solucionador de SAT (no bueno, impulsado por conflictos) |
Cmodelos | Linux , Solaris | GPL | Requiere puesta a tierra | sí | incremental, inspirado en el solucionador de SAT (no bueno, impulsado por conflictos) | |||
diff-SAT | Linux , macOS , Windows ( máquina virtual Java ) | Licencia MIT | Requiere puesta a tierra | sí | Inspirado en SAT-solver (no bueno, impulsado por conflictos). Apoya la resolución de problemas probabilísticos y el muestreo de conjuntos de respuestas. | |||
DLV | Linux , macOS , Windows [18] | gratis para uso educativo académico y no comercial, y para organizaciones sin fines de lucro [18] | sí | sí | No | No | sí | no compatible con Lparse |
Complejo DLV | Linux , macOS , Windows | GPL | sí | sí | sí | sí | construido sobre DLV - no compatible con Lparse | |
GnT | Linux | GPL | Requiere puesta a tierra | sí | construido sobre smodels | |||
Jekejeke | Linux , macOS , Windows ( máquina virtual Java ) | Propiedad | sí | sí | sí | Variante DPLL a través del encadenamiento directo seguro | ||
más ++ | Linux | GPL | literal combinado + basado en reglas | |||||
Ornitorrinco | Linux , Solaris , Windows | GPL | distribuidos, multiproceso nomore ++, smodels | |||||
Pbmodels | Linux | ? | basado en solucionador pseudo-booleano | |||||
Smodels | Linux , macOS , Windows | GPL | Requiere puesta a tierra | No | No | No | No | |
Smodels-cc | Linux | ? | Requiere puesta a tierra | Basado en solucionador SAT; smodels con cláusulas de conflicto | ||||
Sorber | Linux | ? | Basado en solucionador SAT |
Ver también
- Lógica predeterminada
- Programación lógica
- Lógica no monótona
- Prólogo
- Semántica de modelo estable
Referencias
- ^ Baral, Chitta (2003). Representación del conocimiento, razonamiento y resolución declarativa de problemas . Prensa de la Universidad de Cambridge. ISBN 978-0-521-81802-5.
- ^ Gelfond, Michael (2008). "Conjuntos de respuestas" . En van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (eds.). Manual de representación del conocimiento . Elsevier. págs. 285–316. ISBN 978-0-08-055702-1. como PDF Archivado el 3 de marzo de 2016 en la Wayback Machine.
- ^ Dimopoulos, Y .; Nebel, B .; Köhler, J. (1997). "Codificación de problemas de planificación en programas lógicos no monótonos". En Steel, Sam; Alami, Rachid (eds.). Avances recientes en la planificación de la IA: 4ª Conferencia Europea de Planificación, ECP'97, Toulouse, Francia, 24 al 26 de septiembre de 1997, Actas . Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence. 1348 . Saltador. págs. 273-285. ISBN 978-3-540-63912-1. como Postscript
- ^ Subrahmanian, VS; Zaniolo, C. (1995). "Relacionar modelos estables y dominios de planificación de IA" . En Sterling, Leon (ed.). Programación lógica: Actas de la Duodécima Conferencia Internacional sobre Programación Lógica . Prensa del MIT. págs. 233–247. ISBN 978-0-262-69177-2. como Postscript
- ^ Soininen, T .; Niemelä, I. (1998), Formalización del conocimiento de configuración usando reglas con elecciones (Postscript) , Laboratorio de Ciencias del Procesamiento de la Información, Universidad Tecnológica de Helsinki
- ^ Marek, V .; Truszczyński, M. (1999). "Modelos estables y paradigma de programación lógica alternativa". En Apt, Krzysztof R. (ed.). El paradigma de la programación lógica: una perspectiva de 25 años (PDF) . Saltador. págs. 169-181. arXiv : cs / 9809032 . ISBN 978-3-540-65463-6.
- ^ Niemelä, I. (1999). "Programas lógicos con semántica de modelo estable como paradigma de programación de restricciones" (Postscript, gzip) . Anales de Matemáticas e Inteligencia Artificial . 25 (3/4): 241-273. doi : 10.1023 / A: 1018930122475 .
- ^ Lifschitz, V. (1999). "Lenguajes de acción, conjuntos de respuestas y planificación". Cite journal requiere
|journal=
( ayuda )En Apt 1999 , págs. 357–374 - ^ Crick, Tom (2009). Superoptimización: generación de código demostrablemente óptima mediante la programación de conjuntos de respuestas (PDF) (Ph.D.). Universidad de Bath. Expediente 20352. Archivado desde el original (PDF) el 4 de marzo de 2016 . Consultado el 27 de mayo de 2011 .
- ^ Rogelio Dávila. "AnsProlog, una descripción general" (PowerPoint) .
- ^ Niemelä, I .; Simons, P .; Soinenen, T. (2000). "Semántica de modelo estable de reglas de restricción de peso" . En Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald (eds.). Programación lógica y razonamiento no monótono: 5ª Conferencia Internacional, LPNMR '99, El Paso, Texas, EE. UU., Actas del 2 al 4 de diciembre de 1999 . Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence. 1730 . Saltador. págs. 317–331. ISBN 978-3-540-66749-0. como Postscript
- ^ Ferraris, P .; Lifschitz, V. (enero de 2005). "Restricciones de peso como expresiones anidadas". Teoría y práctica de la programación lógica . 5 (1–2): 45–74. arXiv : cs / 0312045 . doi : 10.1017 / S1471068403001923 . como Postscript
- ^ "Análisis de dependencias" . Archivado desde el original el 15 de abril de 2015 . Consultado el 15 de abril de 2015 .
- ^ "Especificación del idioma de entrada ASP-Core-2" (PDF) . Consultado el 14 de mayo de 2018 .
- ^ Marple, Kyle .; Gupta, Gopal. (2012). "Galliwasp: un solucionador de conjuntos de respuestas dirigidas a objetivos". En Albert, Elvira (ed.). Síntesis y transformación del programa basado en la lógica, 22º Simposio Internacional, LOPSTR 2012, Lovaina, Bélgica, 18 al 20 de septiembre de 2012, artículos seleccionados revisados . Saltador. págs. 122-136.
- ^ Marple, K .; Salazar, E .; Gupta, G. (2017). "Computación de modelos estables de programas lógicos normales sin puesta a tierra". CoRR . abs / 1709.00501. [1]
- ^ Arias, J .; Carro, M .; Salazar, E .; Marple, K .; Gupta, G. (2018). "Programación del conjunto de respuesta de restricción sin conexión a tierra". Teoría y práctica de la programación lógica . 18 (3–4): 337–354.
- ^ a b "Página de empresa del sistema DLV" . DLVSYSTEM srl . Consultado el 16 de noviembre de 2011 .
enlaces externos
- Especificación de idioma de entrada ASP-Core-2 2.03c
- Primera competencia del sistema ASP
- Segunda Competición ASP
- Tercera Competencia ASP
- Cuarta Competición ASP
- Ornitorrinco
- Una variedad de solucionadores de conjuntos de respuestas empaquetados para Debian / Ubuntu
- Solucionador de conjuntos de respuestas de cierre