💻 computer science

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

Cet article présente des encodages SAT et MaxSAT compacts pour la planification de réunions interentreprises qui utilisent le filtrage de domaine et des variables partagées pour réduire considérablement le nombre de clauses et l'utilisation de la mémoire tout en minimisant les plages d'inactivité des participants, surpassant à la fois une formulation MaxSAT publiée et le solveur commercial Gurobi en termes d'efficacité de résolution.

Auteurs originaux : Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Publié 2026-08-04

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous soyez l'organisateur de fêtes ultime pour une immense convention commerciale à enjeux élevés. Vous avez des centaines de personnes qui doivent avoir des réunions en tête-à-tête, mais tout le monde a des emplois du temps différents, certaines salles sont minuscules tandis que d'autres sont énormes, et certaines réunions doivent impérativement avoir lieu avant que d'autres ne puissent commencer. Votre objectif n'est pas seulement de donner une réunion à tout le monde ; c'est de s'assurer que personne ne reste assis à s'ennuyer trop longtemps entre ses rendez-vous. C'est le puzzle chaotique de la « planification de réunions interentreprises (B2B) ».

Pour résoudre cela, les informaticiens utilisent un type spécial de jeu logique appelé SAT (Satisfiabilité). Considérez le SAT comme un détective super intelligent qui vérifie si un ensemble de règles peut être vrai en même temps. Si vous dites au détective : « La réunion A doit avoir lieu avant la réunion B, mais la réunion B doit avoir lieu avant la réunion A », le détective répond instantanément : « Impossible ! ». Mais si les règles sont complexes mais possibles, le détective trouve un emploi du temps valide. Une autre version, le MaxSAT, est comme un détective qui non seulement trouve un emploi du temps valide, mais essaie aussi de le rendre parfait en minimisant le temps que les gens passent à attendre. Ce travail explore comment nous pouvons rendre ces détectives logiques plus rapides et plus intelligents lors de l'organisation de ces événements commerciaux complexes.

Le Problème : Un Réseau de Réunions Enchevêtrés

Dans le monde des réunions d'affaires, les choses deviennent vite désordonnées. Vous avez une liste de réunions, une liste de créneaux horaires et une liste de salles. Les règles sont strictes :

Pas de chevauchement : Une personne ne peut pas être à deux endroits à la fois.
Limites de capacité : Une salle ne peut pas accueillir plus de réunions que sa capacité.
Précédence : Certaines réunions doivent se dérouler avant d'autres (comme un briefing matinal avant un atelier de l'après-midi).
Le problème de l'« Inactivité » : Le véritable casse-tête est le « temps d'inactivité ». Si un participant a une réunion à 9h00 et que sa prochaine réunion n'est pas avant 11h00, il a deux heures de « temps d'inactivité ». L'objectif de cette recherche est d'équilibrer cela afin que personne ne soit laissé à attendre pendant des heures pendant que d'autres n'attendent que quelques minutes. C'est une question d'équité et d'efficacité.

L'Ancienne Méthode vs La Nouvelle Méthode

Les chercheurs ont examiné une méthode existante (appelée ORG-MAXSAT) qui était déjà plutôt bonne. Cependant, ils ont remarqué qu'elle revenait à essayer d'organiser une fête en écrivant chaque combinaison possible d'invités et d'horaires, même celles qui sont évidemment impossibles. C'était encombrant, lent et consommait beaucoup de mémoire informatique.

L'équipe de l'Université de technologie de VNU au Vietnam a décidé de construire une version « compacte ». Ils ont introduit trois astuces principales pour réduire le problème :

Le filtre de « Pré-vérification » (Filtrage de domaine) : Avant même de demander au détective informatique de résoudre le puzzle, ils ont ajouté un filtre intelligent. Ce filtre examine les règles et élimine immédiatement les options impossibles. Par exemple, si une réunion doit avoir lieu après une autre qui se termine à 14h00, le filtre supprime instantanément tous les créneaux horaires avant 14h00 de la liste des possibilités. C'est comme nettoyer le désordre sur un bureau avant d'essayer de trouver un stylo spécifique. Ils ont prouvé que ce filtre ne jette jamais une solution valide ; il ne fait qu'éliminer les déchets.
L'« Escalier Partagé » (Encodage de suffixe partagé creux) : Lorsqu'il s'agit des règles de « doit se passer avant », l'ancienne méthode écrivait une note séparée pour chaque paire de réunions. Si vous aviez 100 réunions, cela représentait des milliers de notes. La nouvelle méthode a remarqué que beaucoup de ces notes disaient la même chose. Au lieu d'écrire « Réunion A avant B », « Réunion A avant C » et « Réunion A avant D » séparément, ils ont créé un « escalier » de logique partagé. Ils réutilisent des variables pour des situations similaires, comme utiliser une clé maîtresse pour plusieurs portes au lieu de fabriquer une nouvelle clé pour chaque serrure.
Le score d'« Équité » (Équilibrage du temps d'inactivité) : Au lieu de simplement compter le nombre de pauses que les gens ont, ils ont créé une nouvelle façon de mesurer le « temps d'inactivité ». Ils regardent le temps entre la première réunion d'une personne et sa dernière réunion. Si quelqu'un a des réunions à 9h00 et 11h00, son « étendue » est de deux heures. S'il n'a qu'une seule réunion, il a zéro temps d'inactivité. Le but est que la différence entre le temps d'inactivité de la personne la plus occupée et celui de la personne la moins occupée soit la plus petite possible.

Ce Qu'Ils Ont Découvert

Les chercheurs ont testé leur nouvelle méthode « Compacte » par rapport à l'ancienne et par rapport à certains logiciels commerciaux très puissants (comme Gurobi et CPLEX) sur 126 cas de test officiels et 100 cas de « test de résistance » supplémentaires avec encore plus de réunions.

Voici les résultats, qui sont assez impressionnants :

Taille plus réduite : La nouvelle méthode a réduit le nombre de « clauses » logiques (les règles que le détective informatique doit vérifier) de 40,3 % en moyenne.
Moins de mémoire : Elle a utilisé 55,9 % de mémoire de pointe en moins. Imaginez avoir besoin de moitié moins de RAM pour résoudre le même puzzle.
Vitesse accrue : Le temps total pour résoudre les problèmes a chuté de 14,0 %.
La puissance du filtrage : L'utilisation du seul filtre de « Pré-vérification » a réduit le nombre de variables de 24,1 % et les règles de 16,2 %.
La puissance du partage : L'astuce de l'« Escalier Partagé » a réduit encore de 0,5 % à 5,5 % le nombre de règles, selon l'encombrement du planning.

Le Verdict

La partie la plus excitante est que leur nouvelle méthode SAT et MaxSAT compacte a été capable de résoudre chacun des 126 cas de test officiels. Mieux encore, elle l'a fait plus rapidement que le principal solveur commercial, Gurobi, en termes de temps médian. Alors que d'autres outils commerciaux (comme CPLEX et CP Optimizer) ont eu du mal à résoudre tous les cas dans le délai imparti, cette nouvelle approche basée sur le SAT les a tous gérés.

L'article ne prétend pas avoir résolu les problèmes de planification de l'univers pour toujours, mais il a certainement montré qu'en nettoyant les règles et en partageant le travail plus intelligemment, nous pouvons rendre les ordinateurs bien meilleurs pour organiser nos vies bien remplies. Il transforme un nœud massif et emmêlé de réunions en un emploi du temps net et équilibré, où chacun obtient sa part équitable de temps, et où personne ne reste trop longtemps à attendre dans le couloir.

Résumé Technique : Encodages Compacts SAT et MaxSAT pour la Planification de Réunions B2B avec Équilibrage du Temps d'Inactivité

Définition du Problème

L'article traite de la planification de réunions B2B (Business-to-Business), un problème d'optimisation combinatoire où des réunions par paires demandées doivent être assignées à des créneaux horaires et des lieux spécifiques. La planification doit satisfaire plusieurs contraintes :

Non-chevauchement des participants : Un participant ne peut pas assister à deux réunions simultanément.
Capacité des lieux : Le nombre de réunions dans n'importe quel créneau ne peut excéder le nombre de lieux disponibles ( $K$ ).
Disponibilité et Restrictions : Les réunions doivent avoir lieu dans les sessions demandées, les créneaux fixes ou les créneaux interdits.
Précédence : Des arcs dirigés $(i, j)$ imposent que la réunion $i$ ait lieu avant la réunion $j$ .

L'objectif proposé dans ce travail diffère des formulations antérieures (qui visent souvent à minimiser les « groupes de pauses » ou à borner la disparité dans le nombre de pauses). Au lieu de cela, cette étude minimise la plage des totaux de créneaux d'inactivité internes ( $\Delta I$ ) parmi les participants ayant au moins deux réunions. Les créneaux d'inactivité internes sont définis comme le temps non occupé situé strictement entre la première et la dernière réunion assignée d'un participant. Cette métrique distingue les courtes interruptions des attentes plus longues, visant une distribution équilibrée de la charge similaire au Problème de Curriculum Académique Équilibré (BACP). Une mesure de l'inactivité agrégée ( $I_\Sigma$ ) est également rapportée comme une métrique complémentaire.

Méthodologie

Les auteurs proposent un encodage SAT (Satisfiabilité Booléenne) et MaxSAT compact qui intègre trois améliorations de modélisation primaires par rapport aux formulations publiées existantes :

Filtrage de Domaine Préservant la Solution (Prétraitement) :
Avant de générer la Forme Normale Conjonctive (FNC), les auteurs appliquent un algorithme de prétraitement (Algorithme 1) qui élimine les assignations non supportées. Cela intègre :
- Filtres de bornes de terminaison : Propagation des contraintes de précédence le long des chemins (en utilisant soit des arcs directs, soit la fermeture transitive).
- Correspondance par participant : Élimination des assignations qui ne peuvent pas faire partie d'un calendrier sans conflit pour un participant spécifique.
- Propagation de créneaux saturés : Élimination des créneaux dont la capacité est déjà entièrement utilisée par des assignations forcées.
- Revendication : Ce processus préserve tous les calendriers réalisables tout en réduisant la taille du domaine, réduisant ainsi le nombre de variables et de clauses.
Encodage de Suffixe Partagé Clair de Précédence (SPARSESUFFIX) :
Au lieu d'encoder les relations de précédence à l'aide de clauses par paires (qui peuvent être quadratiques par rapport à la taille du domaine), les auteurs introduisent un encodage clair.
- Il matérialise uniquement les « points de coupure » distincts dans le domaine du prédécesseur où la contrainte devient active.
- Il réutilise des variables auxiliaires pour les coupures égales à travers différentes relations.
- Cette approche est prouvée équivalente aux clauses par paires mais réduit considérablement le nombre de clauses, particulièrement lorsqu'elle est combinée à la réduction de domaine.
Objectif de Temps d'Inactivité Basé sur la Plage :
Le papier introduit un encodage exact pour minimiser la plage des créneaux d'inactivité internes ( $\Delta I$ ).
- Il dérive les premiers et derniers créneaux occupés pour chaque participant.
- Il utilise un nombre linéaire de variables auxiliaires pour calculer la différence entre le maximum et le minimum des comptes d'inactivité parmi tous les participants concernés.

L'étude évalue ces composants par rapport à une formulation de référence ORG-MAXSAT (une adaptation d'un modèle publié) et des solveurs commerciaux (Gurobi, CPLEX, CP Optimizer). L'évaluation couvre 126 instances de référence officielles et 100 instances dérivées de type « Stress » avec des densités de précédence variables.

Contributions Clés

Le papier identifie trois contributions spécifiques :

Procédure de Prétraitement : Un filtre intégré qui élimine les assignations non supportées avant la génération de la FNC. La Proposition 1 prouve que cela préserve la faisabilité, et les résultats empiriques montrent que cela réduit les variables d'assignation de 24,1 % et les clauses de 16,2 %.
Représentation de Suffixe Partagé Clair : Un encodage exact (SPARSESUFFIX) qui matérialise uniquement les points de coupure requis du domaine du prédécesseur. La Proposition 3 prouve son équivalence avec les clauses par paires. L'étude démontre que si la réduction de domaine diminue les comptes de variables, le partage de suffixe réduit indépendamment les comptes de clauses.
Objectif Spécifique au B2B : Un objectif de plage de temps d'inactivité qui mesure la disparité des temps d'attente internes, encodé avec un nombre linéaire de variables auxiliaires.

Résultats Expérimentaux

Les expériences ont été menées sur une machine à 4 cœurs avec une limite de temps de 7 200 secondes. Les conclusions clés incluent :

Taille de la Formule et Mémoire : Comparée à la base de référence ORG-MAXSAT adaptée, l'encodage compact proposé a réduit le nombre médian de clauses de 40,3 % et l'utilisation médiane de la mémoire de pointe de 55,9 %.
Impact de la Réduction de Domaine : Le filtrage de domaine seul a réduit les variables d'assignation de 24,1 % et les clauses de 16,2 %, contribuant à la plus grande part de la réduction de la taille de la formule.
Encodage de Précédence : L'encodage SPARSESUFFIX a réduit le nombre médian de clauses de 0,5 % à 1,0 % sur les instances de précédence officielles et jusqu'à 5,5 % sur les instances dérivées de plus haute densité (lorsqu'il est combiné avec la fermeture transitive).
Performance des Solveurs :
- Les trois méthodes SAT/MaxSAT proposées (SAT incrémental, SAT non incrémental et UWrMaxSAT) ont résolu les 126 instances officielles.
- Comparé à Gurobi (le seul solveur commercial ayant résolu toutes les instances), les méthodes SAT/MaxSAT proposées ont obtenu des temps totaux médians plus faibles.
- Le SAT incrémental a obtenu le temps médian le plus bas (0,227s) parmi les méthodes complètes.
- CP Optimizer a eu le temps médian le plus bas (0,110s) mais a échoué à résoudre 11 instances dans la limite de temps.

Signification et Revendications

Le papier affirme que l'encodage compact proposé offre une amélioration significative de l'efficacité par rapport aux formulations booléennes existantes pour la planification de réunions B2B. En séparant le filtrage de domaine de la représentation de précédence, les auteurs démontrent que la réduction de domaine est le principal moteur de la réduction de la taille de la formule, tandis que l'encodage de suffixe partagé clair fournit une réduction de clauses supplémentaire indépendante de l'ensemble des relations.

L'étude soutient que le nouvel objectif de plage de temps d'inactivité fournit une mesure plus nuancée de la qualité du calendrier que les mesures précédentes de « groupes de pauses », en distinguant les courtes interruptions des attentes longues. De plus, les résultats indiquent que les solveurs SAT et MaxSAT modernes, lorsqu'ils sont équipés de ces encodages compacts, peuvent surpasser les principaux solveurs MIP et CP commerciaux en termes de temps de résolution médian pour cette classe spécifique de problèmes, résolvant toutes les instances de référence où certains solveurs commerciaux ont expiré.

Les auteurs restent modestes quant aux travaux futurs, notant que l'étude actuelle se concentre sur le temps d'exécution unique et que les recherches futures pourraient explorer les exécutions de temps répétées et les objectifs lexicographiques (minimiser $\Delta I$ avant $I_\Sigma$ ).