FLINGO -- Instilling ASP Expressiveness into Linear Integer Constraints

Résumé technique de « flingo — Instiller l'expressivité d'ASP dans les contraintes entières linéaires »

Énoncé du problème
La Programmation par Réponse d'Ensemble de Contraintes (CASP) est un paradigme hybride conçu pour gérer des calculs numériques qui dépassent l'évolutivité des outils standards de Programmation par Réponse d'Ensemble (ASP). Alors que l'ASP standard repose sur une phase de mise au sol suivie d'une résolution, le CASP délègue les contraintes numériques à un solveur backend (généralement suivant les principes de la Satisfiabilité Modulo Théorie) pour éviter l'explosion de la mise au sol causée par de grands domaines numériques. Cependant, les solveurs CASP actuels, tels que clingcon, souffrent d'un écart de modélisation significatif : la spécification des atomes de contrainte correspond souvent aux exigences opérationnelles du backend numérique plutôt qu'aux fonctionnalités déclaratives de haut niveau du paradigme ASP.

Plus précisément, lorsque les attributs numériques sont représentés comme des variables de contrainte dans les systèmes existants, plusieurs fonctionnalités fondamentales de l'ASP sont perdues ou deviennent difficiles à exprimer :

1. Indéfini : La capacité de laisser des attributs indéfinis (par opposition à l'attribution d'une valeur par défaut).
2. Valeurs par défaut : La capacité de déclarer des valeurs par défaut qui peuvent être écrasées par des exceptions.
3. Assignations non déterministes : La capacité de faire des choix non déterministes concernant les valeurs d'attributs via des règles de choix.
4. Agrégats : La capacité d'utiliser des agrégats (par exemple, sommes, minimums) sur des variables de contrainte, en particulier lorsque ces variables peuvent être indéfinies.

Les approches existantes, telles que la logique du Ici-et-Là avec contraintes (HTc), ont posé des fondements sémantiques pour l'indéfini et les agrégats, mais manquaient d'une définition de langage complète et d'une implémentation d'outil qui intègre pleinement ces fonctionnalités dans un flux de travail CASP standard.

Méthodologie
Les auteurs introduisent flingo, un nouveau système et langage CASP qui étend clingo pour incorporer l'expressivité ASP susmentionnée directement dans les contraintes entières linéaires. La méthodologie repose sur les composants suivants :

1. Fondement sémantique (HTc) : La sémantique de flingo est formalisée à l'aide de la logique du Ici-et-Là avec contraintes (HTc). Ce cadre permet de distinguer entre « Ici » (connaissance actuelle) et « Là » (connaissance potentielle), permettant la représentation de variables indéfinies.

   • Indéfini : Les variables entières sont indéfinies par défaut. Une variable n'est définie que si elle est « fondée » (dérivée) à travers les règles du programme.
   • Agrégats stricts vs non stricts : Le langage distingue entre les opérations strictes (&sus) et non strictes (&sum).
     • &sus (Somme stricte) : Exige que tous les termes soient définis. Si une variable est indéfinie, l'atome de contrainte évalue à faux.
     • &sum (Somme non stricte) : Ignore les termes indéfinis du calcul (en les traitant comme l'élément neutre, 0), imitant le comportement d'agrégat ASP standard.
   • Termes conditionnels : flingo prend en charge les termes conditionnels de la forme s : l1, ..., ln, où un terme de produit s est utilisé si la conjonction de littéraux est vraie, sinon un terme par défaut (dépendant du contexte) est utilisé.

2. Syntaxe et fonctionnalités :

   • Atomes de contrainte : Prend en charge les atomes &sum, &sus, &min, &max et &df (défini).
   • Règles d'assignation : Introduit des règles de la forme &fun{t1; ...; tn} =: s :- l1, ..., lm, qui définissent la variable s basée sur les termes t1...tn uniquement lorsque les conditions sont remplies et que les variables sources sont définies.
   • Règles de choix pour les entiers : Prend en charge les règles de choix basées sur des intervalles (par exemple &in{s1..s2} =: x) permettant l'assignation non déterministe de variables entières.

3. Implémentation et traduction :

   • Le solveur flingo est implémenté comme une extension de clingo utilisant son interface de théorie.
   • Crucialement, flingo utilise clingcon comme backend. Pour y parvenir, le système effectue une série de huit transformations de réécriture en temps linéaire pour traduire les programmes flingo en programmes clingcon standards.
   • Cette traduction implique :
     • Le remplacement des termes conditionnels par des atomes propositionnels et des règles auxiliaires.
     • La conversion des opérations &sum (non strictes) en opérations &sus (strictes) combinées à des règles qui gèrent les variables indéfinies en leur attribuant une valeur neutre (0) uniquement lorsque nécessaire pour le backend.
     • Le codage des opérations &min et &max en utilisant &sus et des atomes propositionnels auxiliaires.
     • La garantie que les variables indéfinies dans flingo ne résultent pas en plusieurs modèles stables dans le backend en gérant explicitement l'état « indéfini ».

Contributions clés

1. Conception de langage : L'introduction de flingo, un langage qui unifie les fonctionnalités déclaratives de l'ASP (défauts, indéfini, choix, agrégats) avec l'efficacité de la résolution de contraintes numériques.
2. Formalisation sémantique : Une définition rigoureuse de la sémantique de flingo basée sur HTc, traitant spécifiquement la gestion des variables entières indéfinies et la distinction entre agrégats stricts et non stricts.
3. Mécanisme de traduction : Une traduction prouvée de la syntaxe flingo vers le format d'entrée clingcon, démontrant que l'expressivité améliorée peut être réalisée en utilisant des backends CASP haute performance existants.
4. Propriétés théoriques : L'article établit des propositions montrant la relation entre les modèles flingo et clingcon. Notamment, il démontre que flingo permet un raisonnement non monotone sur les variables entières (par exemple, une règle x = 1 :- &sus{y} = 1 produit un x indéfini si y est indéfini, alors que l'ajout du fait &sus{y} = 1 rend x défini), une fonctionnalité impossible dans clingcon standard.

Résultats et évaluation
L'article fournit des exemples illustratifs pour démontrer l'utilité de flingo :

• Exemple de tarif : Réexamine un problème impliquant des tarifs par défaut et des exceptions. flingo permet un encodage naturel où des valeurs par défaut sont attribuées sauf si des exceptions spécifiques (par exemple, l'acier) sont définies, et où le revenu fiscal est calculé en utilisant des sommes non strictes qui ignorent les tarifs indéfinis.
• Configuration de vélo : Un problème de configuration impliquant un cadre et un sac optionnel avec des calculs de prix. L'exemple montre comment flingo gère les composants optionnels, les intervalles de prix par défaut et l'agrégation des prix, tout en maintenant l'apparence et le ressenti de l'ASP standard.
• Affirmation empirique : Les auteurs déclarent que flingo a été utilisé pour modéliser des problèmes de configuration dans le langage de configuration Coom. Dans ces cas, flingo surpasse considérablement clingo (sans contraintes) sur des problèmes avec des attributs numériques présentant de grands domaines.

Signification
L'article affirme que flingo comble le fossé entre la modélisation ASP de haut niveau et les exigences opérationnelles de la résolution de contraintes numériques. Sa signification réside dans :

• Préservation du paradigme ASP : Il permet aux utilisateurs de conserver les fonctionnalités de modélisation ASP standard (comme les défauts et les agrégats) même lorsqu'ils travaillent avec des contraintes numériques, évitant ainsi la nécessité d'adapter les modèles aux limitations du backend de contraintes.
• Gestion de l'indéfini : Il prend en charge formellement le concept de variables indéfinies dans un contexte de contraintes, ce qui est crucial pour la modélisation d'informations incomplètes et de défauts.
• Implémentation pratique : En traduisant vers clingcon, il exploite l'efficacité des solveurs CASP de pointe sans nécessiter une architecture de solveur complètement nouvelle, rendant l'approche immédiatement applicable.

Les auteurs notent que si l'implémentation actuelle repose sur la grammaire de théorie de clingo, les travaux futurs se concentreront sur l'affinement du langage d'entrée et l'optimisation du processus de traduction pour améliorer davantage l'évolutivité. Le système est disponible publiquement.