FLINGO -- Instilling ASP Expressiveness into Linear Integer Constraints

Resumo Técnico de "flingo — Instilando Expressividade ASP em Restrições Lineares de Inteiros"

Declaração do Problema
A Programação de Resposta a Conjuntos de Restrições (CASP) é um paradigma híbrido projetado para lidar com computações numéricas que excedem a escalabilidade das ferramentas padrão de Programação de Resposta a Conjuntos (ASP). Enquanto o ASP padrão depende de uma fase de grounding seguida por resolução, o CASP delega restrições numéricas a um solver de backend (tipicamente seguindo princípios de Satisfatibilidade Modulo Teoria) para evitar a explosão de grounding causada por grandes domínios numéricos. No entanto, os solvers CASP atuais, como o clingcon, sofrem de uma lacuna significativa de modelagem: a especificação de átomos de restrição frequentemente se alinha aos requisitos operacionais do backend numérico, em vez das funcionalidades declarativas de alto nível do paradigma ASP.

Especificamente, quando atributos numéricos são representados como variáveis de restrição em sistemas existentes, várias funcionalidades centrais do ASP são perdidas ou tornam-se difíceis de expressar:

1. Indefinição: A capacidade de deixar atributos indefinidos (em oposição a atribuir um valor padrão).
2. Valores Padrão: A capacidade de declarar valores padrão que podem ser sobrescritos por exceções.
3. Atribuições Não Determinísticas: A capacidade de fazer escolhas não determinísticas sobre valores de atributos por meio de regras de escolha.
4. Agregações: A capacidade de usar agregados (por exemplo, somas, mínimos) sobre variáveis de restrição, particularmente quando essas variáveis podem estar indefinidas.

Abordagens existentes, como a lógica de Aqui-e-Ali com restrições (HTc), estabeleceram fundamentos semânticos para indefinição e agregados, mas careciam de uma definição abrangente de linguagem e implementação de ferramentas que integrasse totalmente essas funcionalidades em um fluxo de trabalho CASP padrão.

Metodologia
Os autores introduzem o flingo, um novo sistema e linguagem CASP que estende o clingo para incorporar a expressividade ASP supracitada diretamente em restrições lineares de inteiros. A metodologia fundamenta-se nos seguintes componentes:

1. Fundação Semântica (HTc): A semântica do flingo é formalizada usando a Lógica de Aqui-e-Ali com restrições (HTc). Esta estrutura permite uma distinção entre "Aqui" (conhecimento atual) e "Ali" (conhecimento potencial), permitindo a representação de variáveis indefinidas.

   • Indefinição: Variáveis inteiras são indefinidas por padrão. Uma variável só é definida se for "fundada" (derivada) através das regras do programa.
   • Agregados Estritos vs. Não Estritos: A linguagem distingue entre operações estritas (&sus) e não estritas (&sum).
     • &sus (Soma Estrita): Exige que todos os termos estejam definidos. Se qualquer variável estiver indefinida, o átomo de restrição avalia-se como falso.
     • &sum (Soma Não Estrita): Descarta termos indefinidos do cálculo (tratando-os como o elemento neutro, 0), imitando o comportamento padrão de agregados do ASP.
   • Termos Condicionais: O flingo suporta termos condicionais na forma s : l1, ..., ln, onde um termo de produto s é usado se a conjunção de literais se mantiver; caso contrário, é usado um termo padrão (dependente do contexto).

2. Sintaxe e Funcionalidades:

   • Átomos de Restrição: Suporta átomos &sum, &sus, &min, &max e &df (definido).
   • Regras de Atribuição: Introduz regras da forma &fun{t1; ...; tn} =: s :- l1, ..., lm, que definem a variável s com base nos termos t1...tn apenas quando as condições são atendidas e as variáveis de origem estão definidas.
   • Regras de Escolha para Inteiros: Suporta regras de escolha baseadas em intervalos (por exemplo, &in{s1..s2} =: x), permitindo atribuição não determinística de variáveis inteiras.

3. Implementação e Tradução:

   • O solver flingo é implementado como uma extensão do clingo usando sua interface de teoria.
   • Crucialmente, o flingo usa o clingcon como backend. Para alcançar isso, o sistema executa uma série de oito transformações de reescrita em tempo linear para traduzir programas flingo em programas clingcon padrão.
   • Esta tradução envolve:
     • Substituir termos condicionais por átomos proposicionais e regras auxiliares.
     • Converter operações &sum (não estritas) em operações &sus (estritas) combinadas com regras que lidam com variáveis indefinidas atribuindo-lhes um valor neutro (0) apenas quando necessário para o backend.
     • Codificar operações &min e &max usando &sus e átomos proposicionais auxiliares.
     • Garantir que variáveis indefinidas no flingo não resultem em múltiplos modelos estáveis no backend, manipulando explicitamente o estado "indefinido".

Principais Contribuições

1. Design de Linguagem: A introdução do flingo, uma linguagem que unifica as funcionalidades declarativas do ASP (padrões, indefinição, escolha, agregados) com a eficiência da resolução de restrições numéricas.
2. Formalização Semântica: Uma definição rigorosa da semântica do flingo baseada na HTc, abordando especificamente o tratamento de variáveis inteiras indefinidas e a distinção entre agregados estritos e não estritos.
3. Mecanismo de Tradução: Uma tradução comprovada da sintaxe flingo para o formato de entrada clingcon, demonstrando que a expressividade aprimorada pode ser realizada usando backends CASP de alto desempenho existentes.
4. Propriedades Teóricas: O artigo estabelece proposições mostrando a relação entre os modelos flingo e clingcon. Notavelmente, demonstra que o flingo permite raciocínio não monótono sobre variáveis inteiras (por exemplo, uma regra x = 1 :- &sus{y} = 1 produz um x indefinido se y estiver indefinido, enquanto adicionar o fato &sus{y} = 1 torna x definido), uma funcionalidade não possível no clingcon padrão.

Resultados e Avaliação
O artigo fornece exemplos ilustrativos para demonstrar a utilidade do flingo:

• Exemplo de Tarifas: Revisita um problema envolvendo tarifas padrão e exceções. O flingo permite uma codificação natural onde valores padrão são atribuídos, a menos que exceções específicas (por exemplo, aço) sejam definidas, e a receita tributária é calculada usando somas não estritas que ignoram tarifas indefinidas.
• Configuração de Bicicleta: Um problema de configuração envolvendo um quadro e uma bolsa opcional com cálculos de preço. O exemplo mostra como o flingo lida com componentes opcionais, intervalos de preço padrão e a agregação de preços, mantendo ao mesmo tempo a "aparência e sensação" do ASP padrão.
• Afirmação Empírica: Os autores afirmam que o flingo foi usado para modelar problemas de configuração na linguagem de configuração Coom. Nestes casos, o flingo supera significativamente o clingo (sem restrições) em problemas com atributos numéricos que apresentam grandes domínios.

Significado
O artigo afirma que o flingo preenche a lacuna entre a modelagem ASP de alto nível e os requisitos operacionais da resolução de restrições numéricas. Seu significado reside em:

• Preservar o Paradigma ASP: Permite que os usuários mantenham funcionalidades padrão de modelagem ASP (como padrões e agregados) mesmo ao trabalhar com restrições numéricas, evitando a necessidade de adaptar modelos às limitações do backend de restrições.
• Lidar com Indefinição: Suporta formalmente o conceito de variáveis indefinidas em um contexto de restrições, o que é crucial para modelar informações incompletas e padrões.
• Implementação Prática: Ao traduzir para o clingcon, aproveita a eficiência dos solvers CASP de última geração sem exigir uma arquitetura de solver completamente nova, tornando a abordagem imediatamente aplicável.

Os autores observam que, embora a implementação atual dependa da gramática de teoria do clingo, trabalhos futuros focarão no refinamento da linguagem de entrada e na otimização do processo de tradução para aprimorar ainda mais a escalabilidade. O sistema está disponível publicamente.