FLINGO -- Instilling ASP Expressiveness into Linear Integer Constraints

Resumen Técnico de "flingo — Inculcando la Expresividad de ASP en Restricciones Enteras Lineales"

Enunciado del Problema
La Programación de Conjuntos de Respuesta con Restricciones (CASP) es un paradigma híbrido diseñado para manejar cálculos numéricos que exceden la escalabilidad de las herramientas estándar de Programación de Conjuntos de Respuesta (ASP). Mientras que el ASP estándar se basa en una fase de instanciación seguida de resolución, el CASP delega las restricciones numéricas a un solver de backend (generalmente siguiendo principios de Satisfacción Modulo Teoría) para evitar la explosión de instanciación causada por dominios numéricos grandes. Sin embargo, los solvers CASP actuales, como clingcon, sufren una brecha significativa en la modelación: la especificación de átomos de restricción a menudo se alinea con los requisitos operativos del backend numérico en lugar de las características declarativas de alto nivel del paradigma ASP.

Específicamente, cuando los atributos numéricos se representan como variables de restricción en sistemas existentes, varias características centrales del ASP se pierden o se vuelven difíciles de expresar:

1. Indefinición: La capacidad de dejar atributos indefinidos (en lugar de asignar un valor por defecto).
2. Valores por Defecto: La capacidad de declarar valores por defecto que pueden ser sobrescritos por excepciones.
3. Asignaciones No Deterministas: La capacidad de hacer elecciones no deterministas sobre los valores de los atributos mediante reglas de elección.
4. Agregados: La capacidad de usar agregados (por ejemplo, sumas, mínimos) sobre variables de restricción, particularmente cuando esas variables podrían estar indefinidas.

Los enfoques existentes, como la lógica de Aquí-y-Ahí con restricciones (HTc), han sentado las bases semánticas para la indefinición y los agregados, pero carecían de una definición de lenguaje completa y una implementación de herramientas que integrara plenamente estas características en un flujo de trabajo CASP estándar.

Metodología
Los autores introducen flingo, un nuevo sistema y lenguaje CASP que extiende clingo para incorporar la expresividad de ASP mencionada anteriormente directamente en restricciones enteras lineales. La metodología se fundamenta en los siguientes componentes:

1. Fundamento Semántico (HTc): La semántica de flingo se formaliza utilizando la Lógica de Aquí-y-Ahí con restricciones (HTc). Este marco permite distinguir entre "Aquí" (conocimiento actual) y "Ahí" (conocimiento potencial), permitiendo la representación de variables indefinidas.

   • Indefinición: Las variables enteras son indefinidas por defecto. Una variable solo está definida si está "fundada" (derivada) a través de las reglas del programa.
   • Agregados Estrictos vs. No Estrictos: El lenguaje distingue entre operaciones estrictas (&sus) y no estrictas (&sum).
     • &sus (Suma Estricta): Requiere que todos los términos estén definidos. Si alguna variable está indefinida, el átomo de restricción se evalúa como falso.
     • &sum (Suma No Estricta): Descarta los términos indefinidos del cálculo (tratándolos como el elemento neutro, 0), imitando el comportamiento de agregado estándar de ASP.
   • Términos Condicionales: flingo soporta términos condicionales de la forma s : l1, ..., ln, donde un término producto s se usa si la conjunción de literales se cumple; de lo contrario, se usa un término por defecto (dependiente del contexto).

2. Sintaxis y Características:

   • Átomos de Restricción: Soporta átomos &sum, &sus, &min, &max y &df (definido).
   • Reglas de Asignación: Introduce reglas de la forma &fun{t1; ...; tn} =: s :- l1, ..., lm, que definen la variable s basándose en los términos t1...tn solo cuando se cumplen las condiciones y las variables fuente están definidas.
   • Reglas de Elección para Enteros: Soporta reglas de elección basadas en rangos (por ejemplo, &in{s1..s2} =: x) que permiten la asignación no determinista de variables enteras.

3. Implementación y Traducción:

   • El solver flingo se implementa como una extensión de clingo utilizando su interfaz de teoría.
   • Crucialmente, flingo utiliza clingcon como backend. Para lograr esto, el sistema realiza una serie de ocho transformaciones de reescritura de tiempo lineal para traducir programas flingo a programas clingcon estándar.
   • Esta traducción implica:
     • Reemplazar términos condicionales con átomos proposicionales y reglas auxiliares.
     • Convertir operaciones &sum (no estrictas) en operaciones &sus (estrictas) combinadas con reglas que manejan variables indefinidas asignándoles un valor neutro (0) solo cuando es necesario para el backend.
     • Codificar operaciones &min y &max utilizando &sus y átomos proposicionales auxiliares.
     • Asegurar que las variables indefinidas en flingo no resulten en múltiples modelos estables en el backend manejando explícitamente el estado "indefinido".

Contribuciones Clave

1. Diseño de Lenguaje: La introducción de flingo, un lenguaje que unifica las características declarativas del ASP (valores por defecto, indefinición, elección, agregados) con la eficiencia de la resolución de restricciones numéricas.
2. Formalización Semántica: Una definición rigurosa de la semántica de flingo basada en HTc, abordando específicamente el manejo de variables enteras indefinidas y la distinción entre agregados estrictos y no estrictos.
3. Mecanismo de Traducción: Una traducción probada desde la sintaxis de flingo al formato de entrada de clingcon, demostrando que la expresividad mejorada puede realizarse utilizando backends CASP de alto rendimiento existentes.
4. Propiedades Teóricas: El artículo establece proposiciones que muestran la relación entre los modelos de flingo y clingcon. Notablemente, demuestra que flingo permite un razonamiento no monótono sobre variables enteras (por ejemplo, una regla x = 1 :- &sus{y} = 1 produce un x indefinido si y está indefinido, mientras que añadir el hecho &sus{y} = 1 hace que x esté definido), una característica no posible en clingcon estándar.

Resultados y Evaluación
El artículo proporciona ejemplos ilustrativos para demostrar la utilidad de flingo:

• Ejemplo de Tarifas: Revisa un problema que involucra tarifas por defecto y excepciones. flingo permite una codificación natural donde se asignan valores por defecto a menos que se definan excepciones específicas (por ejemplo, acero), y los ingresos fiscales se calculan usando sumas no estrictas que ignoran tarifas indefinidas.
• Configuración de Bicicletas: Un problema de configuración que involucra un cuadro y una bolsa opcional con cálculos de precio. El ejemplo muestra cómo flingo maneja componentes opcionales, rangos de precios por defecto y la agregación de precios, manteniendo al mismo tiempo la "apariencia y sensación" del ASP estándar.
• Afirmación Empírica: Los autores declaran que flingo se ha utilizado para modelar problemas de configuración en el lenguaje de configuración Coom. En estos casos, flingo supera significativamente a clingo (sin restricciones) en problemas con atributos numéricos que presentan dominios grandes.

Significado
El artículo afirma que flingo cierra la brecha entre la modelación ASP de alto nivel y los requisitos operativos de la resolución de restricciones numéricas. Su significado radica en:

• Preservar el Paradigma ASP: Permite a los usuarios retener características de modelación ASP estándar (como valores por defecto y agregados) incluso al trabajar con restricciones numéricas, evitando la necesidad de adaptar modelos a las limitaciones del backend de restricciones.
• Manejo de Indefinición: Soporta formalmente el concepto de variables indefinidas en un entorno de restricciones, lo cual es crucial para modelar información incompleta y valores por defecto.
• Implementación Práctica: Al traducir a clingcon, aprovecha la eficiencia de solvers CASP de última generación sin requerir una arquitectura de solver completamente nueva, haciendo que el enfoque sea inmediatamente aplicable.

Los autores señalan que, si bien la implementación actual depende de la gramática de teoría de clingo, el trabajo futuro se centrará en refinar el lenguaje de entrada y optimizar el proceso de traducción para mejorar aún más la escalabilidad. El sistema está disponible públicamente.