💻 computer science

DateSAT: A Framework for Solving Date and Period Constraints

Cet article présente DateSAT, le premier cadre permettant d'exprimer et de résoudre formellement des contraintes de satisfiabilité impliquant des dates et des périodes calendaires en les réduisant à des formules SMT basées sur des entiers, et valide son efficacité par une évaluation empirique sur un ensemble de données curaté de 450 contraintes.

Auteurs originaux : Leyi Cui, Shrey Tiwari, Rohan Padhye

Publié 2026-05-26

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Leyi Cui, Shrey Tiwari, Rohan Padhye

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 essayez de résoudre une énigme : « Avant-hier, j'avais 25 ans, et l'année prochaine, j'aurai 28 ans. » Quand est-ce possible ?

Pour un humain, c'est un casse-tête amusant. Pour un ordinateur, c'est un cauchemar. Les ordinateurs sont excellents en mathématiques, mais ils sont terribles avec les calendriers. Ils ne « savent » pas que février compte parfois 29 jours, ou qu'ajouter « un mois » au 31 janvier ne donne pas le 31 février (car ce jour n'existe pas).

Ce papier présente DateSAT, un nouvel outil conçu pour apprendre aux ordinateurs à raisonner sur les dates et les périodes sans se perdre.

Voici comment les auteurs ont décomposé le problème, en utilisant quelques analogies du quotidien :

1. Le Problème : Les ordinateurs détestent le temps « flou »

Imaginez un ordinateur comme un bibliothécaire très strict qui ne comprend que les nombres exacts. Si vous lui demandez d'ajouter « 1 mois » à une date, il panique si les mathématiques ne s'alignent pas parfaitement.

Le désordre du monde réel : Le papier souligne que ce n'est pas seulement une énigme. De vrais logiciels se sont plantés à cause de bugs liés aux dates. Par exemple, un bug a un jour fait cesser le fonctionnement des pompes à essence en Nouvelle-Zélande le 29 février, car l'ordinateur ne savait pas comment gérer le jour supplémentaire. Un autre bug a poussé le Bureau des brevets des États-Unis à attribuer des dates d'expiration incorrectes à des milliers de brevets.
Le bug de l'IA : Même l'IA moderne (comme les chatbots que nous utilisons aujourd'hui) se trompe souvent sur ces énigmes de dates, car elles ne sont pas conçues pour effectuer des calculs calendaires stricts.

2. La Solution : DateSAT (Le « Traducteur de calendrier »)

Les auteurs ont construit un cadre appelé DateSAT. Imaginez DateSAT comme un traducteur qui s'intercale entre la question complexe d'un humain sur une date et le cerveau mathématique strict d'un ordinateur.

L'entrée : Vous donnez à DateSAT une question comme : « Est-il possible qu'une entreprise organise une élection légale 500 jours après l'achat d'actions, si l'échéance est fixée à 9 mois après la « date d'acquisition » ? »
La magie : DateSAT traduit ce problème de calendrier désordonné, en langage humain, en un problème mathématique propre et strict qu'un résolveur informatique (appelé résolveur SMT) peut traiter parfaitement.

3. Comment ça marche : Cinq « cartes » différentes

La partie la plus difficile du projet consistait à déterminer comment traduire le calendrier en mathématiques. Les auteurs ont essayé cinq stratégies différentes, comme essayer de naviguer dans une ville en utilisant cinq types de cartes différents :

La carte naïve (Le marcheur pas à pas) : Cette méthode tente d'avancer jour par jour. Si vous ajoutez 100 jours, elle fait 100 petits pas. Elle est très précise mais incroyablement lente, comme traverser un pays un pied après l'autre.
La carte d'époque (Le repère d'étape) : Cette méthode choisit un point de départ fixe (comme le « 1er mars 2000 ») et compte combien de jours se sont écoulés depuis. Elle est excellente pour ajouter des jours, mais se perd quand il faut sauter par « mois » ou par « années ».
La carte hybride (La double vue) : Cette stratégie utilise deux cartes à la fois. Elle utilise la carte « Repère » pour ajouter des jours et la carte « Pas à pas » pour ajouter des mois. Elle bascule entre elles uniquement lorsque nécessaire pour gagner du temps.
La carte Alpha-Bêta (La grille de calendrier) : C'est un raccourci astucieux. Au lieu de compter chaque jour, elle compte « combien de mois se sont écoulés » et « combien de jours dans le mois en cours ». C'est comme savoir que vous êtes à « Rue 5, Maison 3 » au lieu de compter chaque maison depuis le début de la ville.
La carte Alpha-Bêta-Table (La triche) : C'est la gagnante. Elle utilise l'idée de la « Grille de calendrier » mais ajoute une table de triche pré-écrite. Puisque les calendriers se répètent par cycles (tous les 4 ans), l'outil consulte simplement la réponse dans un tableau au lieu de faire les mathématiques à chaque fois. C'est la méthode la plus rapide, résolvant des problèmes complexes jusqu'à 2,4 fois plus vite que la méthode « Naïve » lente.

4. L'essai routier : DateSATBench

Pour prouver que leur outil fonctionne, les auteurs n'ont pas simplement inventé des questions au hasard. Ils ont créé une suite de tests appelée DateSATBench avec 450 problèmes différents :

100 ont été générés par une IA pour trouver des cas limites piégeux.
150 étaient des « tests de stress » générés aléatoirement conçus pour faire craquer le système.
200 ont été extraits de véritables lois fiscales américaines pour voir s'il pouvait gérer de vrais documents juridiques.

Les Résultats :

L'outil a résolu 85 % des problèmes en moins d'une minute.
La méthode « Triche » (Alpha-Bêta-Table) était le champion incontesté, résolvant des problèmes en une fraction de seconde là où la méthode « Naïve » prenait beaucoup plus de temps.
Dans un test, ils ont découvert un bug caché dans une fonction Python écrite par deux programmeurs différents pour vérifier si une date se situait dans une fenêtre de 18 mois. Les testeurs humains avaient manqué le bug, mais DateSAT l'a trouvé instantanément.

5. Pourquoi cela compte

Le papier conclut que DateSAT est le premier outil permettant aux ordinateurs de raisonner sur les dates et les périodes de manière symbolique. Cela signifie qu'il peut vérifier si un morceau de code est logiquement correct concernant le temps, ou si un contrat juridique contient une contradiction dans ses dates, sans avoir besoin d'exécuter le code un million de fois pour voir s'il plante.

En bref, DateSAT donne aux ordinateurs une compréhension de « bon sens » des calendriers, transformant la logique liée aux dates, source de bugs coûteux, en un problème mathématique résoluble.

Résumé Technique : DateSAT

Énoncé du Problème

Les dates et les périodes calendaires sont omniprésentes dans l'analyse logicielle, le traitement de données et le raisonnement sur les documents juridiques. Cependant, la logique calendaire est intrinsèquement sujette aux erreurs en raison des longueurs de mois irrégulières, des années bissextiles et des ambiguïtés dans l'arithmétique des périodes (par exemple, la non-commutativité de l'ajout d'"un mois" par rapport à "un jour"). Les outils existants d'analyse et de vérification de programmes manquent de support natif pour les dates, ce qui force à recourir à l'exécution concrète ou à un traçage symbolique complexe des implémentations de bibliothèques (par exemple, dateutil), menant souvent à une explosion des contraintes. De plus, les Grands Modèles de Langage (LLM) échouent fréquemment dans les tâches de raisonnement temporel. Le problème central abordé est l'absence d'un cadre formel pour exprimer et résoudre des contraintes de satisfiabilité impliquant des dates et des périodes calendaires de manière symbolique.

Méthodologie

L'article présente DateSAT, un cadre qui étend l'arithmétique linéaire entière sans quantificateurs (QF-LIA) avec deux nouveaux sorts : Date et Période.

Formalisation

Sémantique : Les dates sont définies comme des triplets $(y, m, d)$ $(y, m, d)$ suivant les règles du calendrier grégorien. Les périodes sont des triplets $(n_y, n_m, n_d)$ $(n_{y}, n_{m}, n_{d})$ . Le cadre adopte une sémantique spécifique pour l'addition date-période (cohérente avec des bibliothèques comme java.time de Java et dateutil de Python) :
1. Addition Année/Mois : Effectuée en premier, avec une gestion des débordements qui arrondit vers le bas les dates invalides (par exemple, 31 jan + 1 mois $\to$ 28/29 fév).
2. Addition Jour : Effectuée en second, permettant les débordements vers les mois suivants.
  Cette sémantique garantit que l'ajout d'une période à une date valide produit toujours une date valide (Théorème 1).
Langage d'Entrée : Le langage prend en charge des variables de dates libres, l'arithmétique date/période, les comparaisons et l'extraction de composantes (année, mois, jour). La logique est prouvée décidable par réduction au QF-LIA.

Stratégies de Résolution

Les auteurs proposent cinq stratégies de codage pour mapper les contraintes DateSAT vers des formules SMT sur les entiers, implémentées à l'aide du solveur Z3. Ces stratégies opèrent un compromis entre la profondeur logique (imbrication des blocs if-then-else) et la complexité arithmétique (nombre d'opérations entières) :

Codage Naïf : Représente les dates comme des tuples $(y, m, d)$ . L'arithmétique date-période est déroulée étape par étape, conduisant à une profondeur logique de $O(|n_d|)$ due aux ITE imbriqués pour les débordements de jours.
Codage basé sur l'Époque : Représente les dates comme un entier unique $\Delta$ (jours depuis une époque fixe). Les auteurs sélectionnent le 1er mars 2000 comme époque pour simplifier les cycles d'années bissextiles (cycles de 1461 jours). L'addition de jours devient $O(1)$ , mais l'arithmétique année/mois nécessite de reconvertir $\Delta$ en $(y, m, d)$ , introduisant des contraintes complexes de division/modulo.
Codage Hybride : Maintient à la fois les représentations $(y, m, d)$ et $\Delta$ pour chaque date. Il utilise des indicateurs de cohérence paresseux pour basculer entre les représentations uniquement lorsque nécessaire (par exemple, utiliser $\Delta$ pour les opérations uniquement sur les jours et $(y, m, d)$ pour l'arithmétique des mois).
Codage Alpha-Bêta : Représente une date comme un couple $(\alpha, \beta)$ , où $\alpha$ est le nombre de mois depuis l'époque et $\beta$ est le décalage de jour dans ce mois. Cela évite une imbrication profonde en utilisant l'arithmétique modulaire pour déterminer les longueurs de mois.
Codage Alpha-Bêta-Table : Une optimisation de la stratégie Alpha-Bêta pour les instances bornées (1900–2100). Elle utilise des tables de recherche précalculées (cycles de 48 mois) pour les jours par mois et les jours avant le mois, remplaçant l'arithmétique complexe par des accès aux tableaux et des opérations modulo.

Vérification de la Correction

La correction des codages basés sur l'Époque, Hybride et Alpha-Bêta par rapport à la base de référence Naïve a été formellement vérifiée à l'aide de l'assistant de preuve Verus. Les preuves établissent que ces codages sont équivalentement satisfaisables avec le codage Naïf pour des contraintes bien formées.

Benchmark et Évaluation

Les auteurs ont constitué DateSATBench, un ensemble de données de 450 contraintes provenant de trois sources :

Synthétisé par LLM (100) : Axé sur des cas limites sémantiques (par exemple, années bissextiles, limites de mois).
Échantillonné par Grammaire (150) : Généré aléatoirement pour tester la performance du solveur sur des cas difficiles/in-satisfaisables.
Fondé sur le Droit (200) : Dérivé des statuts du Code des Revenus Internes des États-Unis (par exemple, délais d'élection de la section 338(g)).

Résultats :

Performance : Sur l'ensemble de données juridique, la stratégie Alpha-Bêta-Table a obtenu les meilleures performances, résolvant 98,45 % des contraintes avec un temps médian de 0,13 seconde.
Accélération : Par rapport à la base de référence Naïve, Alpha-Bêta-Table a fourni une accélération médiane de 2,41× sur l'ensemble de la suite de benchmarks (430 contraintes solubles).
Efficacité : La stratégie Hybride a montré des améliorations significatives sur les contraintes échantillonnées par grammaire (temps médian 4,69 s contre 28,07 s pour Naïf), tandis que la stratégie basée sur l'Époque excellait dans les cas simples synthétisés par LLM.
Évolutivité : À mesure que les contraintes devenaient plus complexes, le choix de la stratégie de codage est devenu de plus en plus critique, la stratégie Alpha-Bêta-Table maintenant une robustesse là où d'autres ont expiré.

Contributions Clés

Formalisation : Une définition rigoureuse de la satisfiabilité des contraintes de dates et de périodes, incluant la sémantique pour l'arithmétique et la comparaison.
Stratégies : Cinq stratégies de codage distinctes pour réduire la logique des dates à l'arithmétique entière, équilibrant profondeur logique et complexité arithmétique.
Implémentation : Une implémentation Python open-source utilisant Z3, disponible à l'adresse cmu-pasta/DateSAT.
Benchmark : La suite DateSATBench (450 contraintes) pour évaluer les outils de raisonnement sur les dates.
Évaluation : Une étude empirique démontrant que les codages spécialisés surpassent significativement les approches naïves, en particulier pour les contraintes légales et synthétiques complexes.

Importance et Revendications

L'article revendique présenter le premier cadre pour exprimer et résoudre des contraintes de satisfiabilité impliquant des dates et des périodes calendaires. Son importance réside dans :

Combler le Vide : Aborder le manque de support d'outil pour le raisonnement formel sur la logique des dates, une source connue de bugs logiciels (par exemple, erreurs d'expiration de brevets, pannes de cloud).
Permettre la Vérification : Fournir un mécanisme pour vérifier l'équivalence dans le refactorisation de code (par exemple, remplacer des appels de bibliothèque par une logique personnalisée) et valider la conformité juridique sans dépendre de LLMs sujets aux erreurs ou de tests concrets exhaustifs.
Fondation pour le Travail Futur : Offrir un benchmark et un solveur qui peuvent être intégrés dans des outils de vérification de programmes et des systèmes d'IA Agentic nécessitant un raisonnement temporel précis.

Les auteurs restent modestes, notant que si leur implémentation actuelle utilise Z3 comme backend, un travail futur pourrait impliquer l'intégration directe de la logique des dates dans SMT-LIB en tant que nouvelle théorie ou l'exploration de codages par vecteurs de bits pour les instances bornées. Ils soulignent que leur travail est une étape fondamentale vers un raisonnement principé sur les calculs temporels.