FLINGO -- Instilling ASP Expressiveness into Linear Integer Constraints

Sintesi Tecnica di "flingo — Instilling ASP Expressiveness into Linear Integer Constraints"

Enunciato del Problema
La Programmazione a Risposta di Insiemi con Vincoli (CASP) è un paradigma ibrido progettato per gestire calcoli numerici che superano la scalabilità degli strumenti standard di Programmazione a Risposta di Insiemi (ASP). Mentre l'ASP standard si basa su una fase di grounding seguita dalla risoluzione, il CASP delega i vincoli numerici a un solver backend (tipicamente basato sui principi della Satisfiability Modulo Theory) per evitare l'esplosione del grounding causata da grandi domini numerici. Tuttavia, i solver CASP attuali, come clingcon, soffrono di un significativo divario di modellazione: la specifica degli atomi di vincolo spesso si allinea ai requisiti operativi del backend numerico piuttosto che alle funzionalità dichiarative di alto livello del paradigma ASP.

Nello specifico, quando gli attributi numerici sono rappresentati come variabili di vincolo nei sistemi esistenti, diverse funzionalità fondamentali dell'ASP vengono perse o diventano difficili da esprimere:

1. Indefinitezza: La capacità di lasciare gli attributi indefiniti (in opposizione all'assegnazione di un valore predefinito).
2. Valori Predefiniti: La capacità di dichiarare valori predefiniti che possono essere sovrascritti da eccezioni.
3. Assegnazioni Non Deterministiche: La capacità di effettuare scelte non deterministiche riguardo ai valori degli attributi tramite regole di scelta.
4. Aggregati: La capacità di utilizzare aggregati (ad esempio, somme, minimi) su variabili di vincolo, in particolare quando tali variabili potrebbero essere indefinite.

Gli approcci esistenti, come la logica dell'Here-and-There con vincoli (HTc), hanno gettato le basi semantiche per l'indefinitezza e gli aggregati, ma mancavano di una definizione linguistica completa e di un'implementazione di strumenti che integrasse pienamente queste funzionalità in un flusso di lavoro CASP standard.

Metodologia
Gli autori introducono flingo, un nuovo sistema e linguaggio CASP che estende clingo per incorporare la suddetta espressività ASP direttamente nei vincoli lineari sugli interi. La metodologia si fonda sui seguenti componenti:

1. Fondamenta Semantiche (HTc): La semantica di flingo è formalizzata utilizzando la Logica dell'Here-and-There con vincoli (HTc). Questo framework permette di distinguere tra "Here" (conoscenza corrente) e "There" (conoscenza potenziale), consentendo la rappresentazione di variabili indefinite.

   • Indefinitezza: Le variabili intere sono indefinite di default. Una variabile è definita solo se è "fondata" (derivata) attraverso le regole del programma.
   • Aggregati Rigidi vs. Non Rigidi: Il linguaggio distingue tra operazioni rigide (&sus) e non rigide (&sum).
     • &sus (Somma Rigida): Richiede che tutti i termini siano definiti. Se una variabile è indefinita, l'atomo di vincolo valuta a falso.
     • &sum (Somma Non Rigida): Scarta i termini indefiniti dal calcolo (trattandoli come l'elemento neutro, 0), mimando il comportamento standard degli aggregati ASP.
   • Termini Condizionali: flingo supporta termini condizionali della forma s : l1, ..., ln, dove un termine prodotto s è utilizzato se la congiunzione dei letterali vale, altrimenti viene utilizzato un termine predefinito (dipendente dal contesto).

2. Sintassi e Funzionalità:

   • Atomi di Vincolo: Supporta gli atomi &sum, &sus, &min, &max e &df (defined).
   • Regole di Assegnazione: Introduce regole della forma &fun{t1; ...; tn} =: s :- l1, ..., lm, che definiscono la variabile s basandosi sui termini t1...tn solo quando le condizioni sono soddisfatte e le variabili sorgente sono definite.
   • Regole di Scelta per Interi: Supporta regole di scelta basate su intervalli (ad esempio, &in{s1..s2} =: x) che permettono l'assegnazione non deterministica di variabili intere.

3. Implementazione e Traduzione:

   • Il solver flingo è implementato come estensione di clingo utilizzando la sua interfaccia teorica.
   • Crucialmente, flingo utilizza clingcon come backend. Per raggiungere questo obiettivo, il sistema esegue una serie di otto trasformazioni di riscrittura in tempo lineare per tradurre i programmi flingo in programmi clingcon standard.
   • Questa traduzione comporta:
     • La sostituzione dei termini condizionali con atomi proposizionali e regole ausiliarie.
     • La conversione delle operazioni &sum (non rigide) in operazioni &sus (rigide) combinate con regole che gestiscono le variabili indefinite assegnando loro un valore neutro (0) solo quando necessario per il backend.
     • La codifica delle operazioni &min e &max utilizzando &sus e atomi proposizionali ausiliari.
     • L'assicurazione che le variabili indefinite in flingo non risultino in modelli stabili multipli nel backend gestendo esplicitamente lo stato "indefinito".

Contributi Chiave

1. Progettazione del Linguaggio: L'introduzione di flingo, un linguaggio che unisce le funzionalità dichiarative dell'ASP (predefiniti, indefinitezza, scelta, aggregati) con l'efficienza della risoluzione dei vincoli numerici.
2. Formalizzazione Semantica: Una definizione rigorosa della semantica di flingo basata su HTc, che affronta specificamente la gestione delle variabili intere indefinite e la distinzione tra aggregati rigidi e non rigidi.
3. Meccanismo di Traduzione: Una traduzione dimostrata dalla sintassi flingo al formato di input clingcon, che dimostra come l'espressività potenziata possa essere realizzata utilizzando backend CASP ad alte prestazioni esistenti.
4. Proprietà Teoriche: Il documento stabilisce proposizioni che mostrano la relazione tra i modelli flingo e clingcon. In particolare, dimostra che flingo permette un ragionamento non monotono sulle variabili intere (ad esempio, una regola x = 1 :- &sus{y} = 1 produce una x indefinita se y è indefinita, mentre l'aggiunta del fatto &sus{y} = 1 rende x definita), una funzionalità non possibile nel clingcon standard.

Risultati e Valutazione
Il documento fornisce esempi illustrativi per dimostrare l'utilità di flingo:

• Esempio delle Tariffe: Riprende un problema che coinvolge tariffe predefinite ed eccezioni. flingo permette una codifica naturale in cui i valori predefiniti sono assegnati a meno che non siano definite eccezioni specifiche (ad esempio, acciaio), e il reddito fiscale è calcolato utilizzando somme non rigide che ignorano le tariffe indefinite.
• Configurazione della Bicicletta: Un problema di configurazione che coinvolge un telaio e un optional borsello con calcoli dei prezzi. L'esempio mostra come flingo gestisca componenti opzionali, intervalli di prezzo predefiniti e l'aggregazione dei prezzi, mantenendo al contempo l'aspetto e la sensazione dell'ASP standard.
• Affermazione Empirica: Gli autori dichiarano che flingo è stato utilizzato per modellare problemi di configurazione nel linguaggio di configurazione Coom. In questi casi, flingo supera significativamente clingo (senza vincoli) su problemi con attributi numerici che presentano grandi domini.

Significato
Il documento afferma che flingo colma il divario tra la modellazione ASP di alto livello e i requisiti operativi della risoluzione dei vincoli numerici. La sua importanza risiede in:

• Preservazione del Paradigma ASP: Permette agli utenti di mantenere le funzionalità di modellazione ASP standard (come predefiniti e aggregati) anche quando si lavora con vincoli numerici, evitando la necessità di adattare i modelli ai limiti del backend dei vincoli.
• Gestione dell'Indefinitezza: Supporta formalmente il concetto di variabili indefinite in un contesto di vincoli, il che è cruciale per la modellazione di informazioni incomplete e predefiniti.
• Implementazione Pratica: Traducendo in clingcon, sfrutta l'efficienza dei solver CASP all'avanguardia senza richiedere un'architettura di solver completamente nuova, rendendo l'approccio immediatamente applicabile.

Gli autori notano che, sebbene l'implementazione attuale si basi sulla grammatica teorica di clingo, il lavoro futuro si concentrerà sul perfezionamento del linguaggio di input e sull'ottimizzazione del processo di traduzione per migliorare ulteriormente la scalabilità. Il sistema è pubblicamente disponibile.