Compact SAT and MaxSAT Encodings for Business-to-Business Meeting Scheduling with Idle-Time Balancing

Sintesi Tecnica: Codifiche Compatte SAT e MaxSAT per la Pianificazione di Incontri B2B con Bilanciamento dei Tempi di Inattività

Definizione del Problema

Il documento affronta la pianificazione di incontri Business-to-Business (B2B), un problema di ottimizzazione combinatoria in cui le riunioni pairwise richieste devono essere assegnate a specifici slot temporali e sedi. La pianificazione deve soddisfare diversi vincoli:

• Non sovrapposizione dei partecipanti: Un partecipante non può assistere a due incontri simultaneamente.
• Capacità della sede: Il numero di incontri in uno qualsiasi slot temporale non può superare il numero di sedi disponibili ($K$).
• Disponibilità e Restrizioni: Gli inconti devono avvenire entro le sessioni richieste, gli slot fissi o gli slot proibiti.
• Precedenza: Archi diretti $(i, j)$ impongono che l'incontro $i$ avvenga prima dell'incontro $j$.

L'obiettivo proposto in questo lavoro differisce dalle formulazioni precedenti (che spesso minimizzano i "gruppi di pause" o limitano la disparità nel conteggio delle pause). Questo studio minimizza il range dei totali di slot di inattività interna ($\Delta I$) tra i partecipanti con almeno due incontri. Gli slot di inattività interna sono definiti come il tempo non occupato strettamente compreso tra il primo e l'ultimo incontro assegnato a un partecipante. Questa metrica distingue tra brevi interruzioni e attese più lunghe, puntando a una distribuzione del carico bilanciata simile al Problema del Curriculum Accademico Bilanciato (BACP). Viene inoltre riportata una misura dell'inattività aggregata ($I_\Sigma$) come metrica complementare.

Metodologia

Gli autori propongono una codifica SAT (Soddisfacibilità Booleana) e MaxSAT compatta che integra tre miglioramenti primari nella modellazione rispetto alle formulazioni pubblicate esistenti:

1. Filtraggio del Dominio Preservante la Soluzione (Preprocessing):
   Prima di generare la Forma Normale Congiuntiva (CNF), gli autori applicano un algoritmo di pre-elaborazione (Algoritmo 1) che rimuove le assegnazioni non supportate. Questo integra:

   • Filtri di limite endpoint: Propagazione dei vincoli di precedenza lungo i percorsi (utilizzando archi diretti o chiusura transitiva).
   • Matching per partecipante: Rimozione delle assegnazioni che non possono far parte di uno schema privo di conflitti per un partecipante specifico.
   • Propagazione degli slot saturi: Eliminazione degli slot in cui la capacità è già completamente utilizzata da assegnazioni forzate.
   • Affermazione: Questo processo preserva tutti gli schemi ammissibili riducendo al contempo la dimensione del dominio, riducendo così il numero di variabili e clausole.

2. Codifica Sparse Shared-Suffix Precedence (SPARSESUFFIX):
   Invece di codificare le relazioni di precedenza utilizzando clausole pairwise (che possono essere quadratiche rispetto alla dimensione del dominio), gli autori introducono una codifica sparsa.

   • Essa materializza solo i distinti "punti di taglio" (cut points) nel dominio del predecessore in cui il vincolo diventa attivo.
   • Riutilizza variabili ausiliarie per tagli uguali tra diverse relazioni.
   • Questo approccio è dimostrato equivalente alle clausole pairwise ma riduce significativamente il conteggio delle clausole, in particolare se combinato con la riduzione del dominio.

3. Obiettivo basato sul Range dell'Inattività:
   Il documento introduce una codifica esatta per minimizzare il range degli slot di inattività interna ($\Delta I$).

   • Deriva i primi e gli ultimi slot occupati per ogni partecipante.
   • Utilizza un numero lineare di variabili ausiliarie per calcolare la differenza tra il massimo e il minimo conteggio di inattività tra tutti i partecipanti rilevanti.

Lo studio valuta questi componenti contro una formulazione baseline ORG-MAXSAT (un adattamento di un modello pubblicato) e solver commerciali (Gurobi, CPLEX, CP Optimizer). La valutazione copre 126 istanze di benchmark ufficiali e 100 istanze "Stress" derivate con diverse densità di precedenza.

Contributi Chiave

Il documento identifica tre contributi specifici:

1. Procedura di Preprocessing: Un filtro integrato che rimuove le assegnazioni non supportate prima della generazione della CNF. La Proposizione 1 dimostra che questo preserva l'ammissibilità e i risultati empirici mostrano che riduce le variabili di assegnazione del 24,1% e le clausole del 16,2%.
2. Rappresentazione Sparse Shared-Suffix: Una codifica esatta (SPARSESUFFIX) che materializza solo i punti di taglio richiesti nel dominio del predecessore. La Proposizione 3 dimostra la sua equivalenza alle clausole pairwise. Lo studio dimostra che mentre la riduzione del dominio abbassa il conteggio delle variabili, la condivisione del suffisso (suffix sharing) riduce indipendentemente il conteggio delle clausole.
3. Obiettivo Specifico per il B2B: Un obiettivo basato sul range dell'inattività che misura la disparità nei tempi di attesa interna, codificato con un numero lineare di variabili ausiliarie.

Risultati Sperimentali

Gli esperimenti sono stati condotti su una macchina a 4 core con un limite di tempo di 7.200 secondi. Le scoperte principali includono:

• Dimensione della Formula e Memoria: Rispetto alla baseline ORG-MAXSAT adattata, la proposta codifica compatta ha ridotto il conteggio mediano delle clausole del 40,3% e l'uso mediano del picco di memoria del 55,9%.
• Impatto della Riduzione del Dominio: Il filtraggio del dominio da solo ha ridotto le variabili di assegnazione del 24,1% e le clausole del 16,2%, contribuendo la quota maggiore alla riduzione della dimensione della formula.
• Codifica della Precedenza: La codifica SPARSESUFFIX ha ridotto il conteggio mediano delle clausole dello 0,5%–1,0% sulle istanze di precedenza ufficiali e fino al 5,5% sulle istanze derivate ad alta densità (quando combinata con la chiusura transitiva).
• Performance dei Solver:
  • Tutti e tre i metodi SAT/MaxSAT proposti (Incremental SAT, Non-Incremental SAT e UWrMaxSAT) hanno risolto tutti i 126 casi ufficiali.
  • Rispetto a Gurobi (l'unico solver commerciale ad aver risolto tutti i casi), i metodi SAT/MaxSAT proposti hanno ottenuto tempi totali mediani inferiori.
  • Incremental SAT ha ottenuto il tempo mediano più basso (0,227s) tra i metodi completi.
  • CP Optimizer ha avuto il tempo mediano più basso (0,110s) ma non è riuscito a risolvere 11 istanze entro il limite di tempo.

Significato e Rivendicazioni

Il documento afferma che la proposta codifica compatta offre un significativo miglioramento dell'efficienza rispetto alle esistenti formulazioni booleane per la pianificazione di incontri B2B. Separando il filtraggio del dominio dalla rappresentazione della precedenza, gli autori dimostrano che la riduzione del dominio è il driver principale per la riduzione della dimensione della formula, mentre la codifica sparse shared-suffix fornisce un ulteriore abbattimento delle clausole indipendentemente dall'insieme delle relazioni.

Lo studio asserisce che il nuovo obiettivo del range dell'inattività fornisce una misura della qualità dello schema più sfumata rispetto alle precedenti metriche dei "gruppi di pause", distinguendo tra brevi interruzioni e attese lunghe. Inoltre, i risultati indicano che i moderni solver SAT e MaxSAT, se dotati di queste codifiche compatte, possono superare i principali solver MIP e CP in termini di tempo di risoluzione mediano per questa specifica classe di problemi, risolvendo tutti gli istanze di benchmark dove alcuni solver commerciali sono andati in timeout.

Gli autori rimangono modesti riguardo al lavoro futuro, notando che lo studio attuale si concentra sulla tempistica di esecuzione singola e che la ricerca futura potrebbe esplorare esecuzioni temporali ripetute e obiettivi lessicografici (minimizzare $\Delta I$ prima di $I_\Sigma$).