💻 computer science

DateSAT: A Framework for Solving Date and Period Constraints

Dit artikel introduceert DateSAT, het eerste raamwerk voor het formeel uitdrukken en oplossen van vervullingsconstraints die data en kalenderperioden betrekken door ze te reduceren tot op gehele getallen gebaseerde SMT-formules, en valideert de effectiviteit daarvan door middel van een empirische evaluatie op een gecureerde dataset van 450 constraints.

Oorspronkelijke auteurs: Leyi Cui, Shrey Tiwari, Rohan Padhye

Gepubliceerd 2026-05-26

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Leyi Cui, Shrey Tiwari, Rohan Padhye

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een raadsel probeert op te lossen: "De dag voor gisteren was ik 25, en volgend jaar word ik 28." Wanneer is dit mogelijk?

Voor een mens is dit een leuk hersenkraker. Voor een computer is het een nachtmerrie. Computers zijn geweldig in wiskunde, maar ze zijn verschrikkelijk in kalenders. Ze "weten" niet dat februari soms 29 dagen heeft, of dat het toevoegen van "één maand" aan 31 januari niet uitkomt op 31 februari (omdat die dag niet bestaat).

Dit artikel introduceert DateSAT, een nieuw hulpmiddel dat computers leert om na te denken over datums en tijdsperiodes zonder in de war te raken.

Hier is hoe de auteurs dit hebben opgesplitst, met behulp van alledaagse analogieën:

1. Het Probleem: Computers Hebben een Hekel aan "Vage" Tijd

Stel je een computer voor als een zeer strenge bibliothecaris die alleen exacte getallen begrijpt. Als je het vraagt om "1 maand" aan een datum toe te voegen, raakt het in paniek als de wiskunde niet perfect klopt.

De Wereldse Chaos: Het artikel wijst erop dat dit niet zomaar een raadsel is. Echte software is gecrasht door datumbugs. Bijvoorbeeld: een bug zorgde er ooit voor dat benzinepompen in Nieuw-Zeeland op 29 februari stopten met werken, omdat de computer niet wist hoe het de extra dag moest verwerken. Een andere bug zorgde ervoor dat het Amerikaanse Octrooibureau de verkeerde vervaldatums gaf aan duizenden octrooien.
De AI-Glitch: Zelfs moderne AI (zoals de chatbots die we vandaag gebruiken) krijgt deze datumraadsels vaak verkeerd, omdat ze niet zijn gebouwd om strikte kalenderwiskunde te doen.

2. De Oplossing: DateSAT (De "Kalendervertaler")

De auteurs bouwden een raamwerk genaamd DateSAT. Denk aan DateSAT als een vertaler die tussen een complexe datumvraag van een mens en de strenge wiskundige hersenen van een computer zit.

De Invoer: Je geeft DateSAT een vraag zoals: "Is het mogelijk dat een bedrijf een wettelijke verkiezing 500 dagen na het kopen van aandelen houdt, als de deadline 9 maanden na de 'aankoopdatum' ligt?"
De Magie: DateSAT vertaalt dit rommelige, menselijke kalenderprobleem in een schoon, strikt wiskundig probleem dat een computerafwijzer (een SMT-oplosser) perfect kan verwerken.

3. Hoe Het Werkt: Vijf Verschillende "Kaarten"

Het moeilijkste deel van het project was uitzoeken hoe je de kalender naar wiskunde vertaalt. De auteurs probeerden vijf verschillende strategieën, alsof je een stad probeert te navigeren met vijf verschillende soorten kaarten:

De Naïeve Kaart (De Stap-voor-Stap Wandelaar): Deze methode probeert dag voor dag te lopen. Als je 100 dagen optelt, zet het 100 kleine stapjes. Het is zeer nauwkeurig maar ongelooflijk traag, alsof je een land doorkruist met één voet per keer.
De Epoch-Kaart (De Meestepunt-Marker): Deze methode kiest een vast startpunt (zoals "1 maart 2000") en telt hoeveel dagen er sindsdien zijn verstreken. Het is geweldig voor het optellen van dagen, maar raakt in de war wanneer je moet springen in "maanden" of "jaren".
De Hybride Kaart (Het Dubbelzicht): Deze strategie gebruikt twee kaarten tegelijk. Het gebruikt de "Meestepunt"-kaart voor het optellen van dagen en de "Stap-voor-Stap"-kaart voor het optellen van maanden. Het schakelt alleen over wanneer nodig om tijd te besparen.
De Alpha-Beta Kaart (Het Kalenderrooster): Dit is een slimme afkorting. In plaats van elke enkele dag te tellen, telt het "hoeveel maanden zijn verstreken" en "hoeveel dagen in de huidige maand". Het is alsof je weet dat je op "Straat 5, Huis 3" bent in plaats van elk huis vanaf het begin van de stad te tellen.
De Alpha-Beta-Tabel Kaart (Het Spiekbriefje): Dit is de winnaar. Het gebruikt het "Kalenderrooster"-idee maar voegt een vooraf geschreven spiekbriefje toe. Omdat kalenders zich in cycli herhalen (elke 4 jaar), zoekt het hulpmiddel het antwoord gewoon op in een tabel in plaats van elke keer de wiskunde te doen. Dit is de snelste methode en lost complexe problemen tot 2,4 keer sneller op dan de trage "Naïeve" methode.

4. De Proefrit: DateSATBench

Om te bewijzen dat hun hulpmiddel werkt, verzonnen de auteurs niet zomaar willekeurige vragen. Ze bouwden een testset genaamd DateSATBench met 450 verschillende problemen:

100 werden gegenereerd door AI om lastige randgevallen te vinden.
150 waren willekeurig gegenereerde "stress-tests" ontworpen om het systeem te breken.
200 waren gehaald uit echte Amerikaanse belastingwetten om te zien of het echte juridische documenten kon verwerken.

De Resultaten:

Het hulpmiddel loste 85% van de problemen op in minder dan een minuut.
De "Spiekbriefje"-methode (Alpha-Beta-Tabel) was de duidelijke kampioen en loste problemen op in een fractie van een seconde die de "Naïeve" methode veel langer kostte.
In één test vonden ze een verborgen bug in een Python-functie die door twee verschillende programmeurs was geschreven om te controleren of een datum binnen een venster van 18 maanden viel. De menselijke testers misten de bug, maar DateSAT vond het direct.

5. Waarom Dit Belangrijk Is

Het artikel concludeert dat DateSAT het eerste hulpmiddel is dat computers in staat stelt om symbolisch te redeneren over datums en periodes. Dit betekent dat het kan controleren of een stuk code logisch correct is wat tijd betreft, of of een juridisch contract een tegenstrijdigheid in zijn datums heeft, zonder dat het de code een miljoen keer hoeft uit te voeren om te zien of het crasht.

Kortom, DateSAT geeft computers een "gezond verstand" begrip van kalenders, waardoor datumgerelateerde logica verandert van een bron van dure bugs in een oplosbaar wiskundig probleem.

Technische Samenvatting: DateSAT

Probleemstelling

Datums en kalenderperiodes zijn alomtegenwoordig in softwareanalyse, gegevensverwerking en redenering over juridische documenten. Kalenderlogica is echter inherent foutgevoelig vanwege onregelmatige maandlengtes, schrikkellijaren en ambiguïteiten in periode-aritmetiek (bijvoorbeeld de niet-commutativiteit van het toevoegen van "één maand" versus "één dag"). Bestaande programma-analyse- en verificatietools missen native ondersteuning voor datums, wat leidt tot afhankelijkheid van concrete uitvoering of complexe symbolische tracing van bibliotheekimplementaties (zoals dateutil), wat vaak resulteert in een explosie van constraints. Bovendien falen Large Language Models (LLM's) frequent bij taken voor temporele redenering. Het kernprobleem dat wordt aangepakt, is het ontbreken van een formeel raamwerk om vervulbaarheidsconstraints met betrekking tot datums en kalenderperiodes symbolisch uit te drukken en op te lossen.

Methodologie

Het artikel introduceert DateSAT, een raamwerk dat kwantorvrije lineaire geheeltallige aritmetiek (QF-LIA) uitbreidt met twee nieuwe sorts: Date en Period.

Formalisering

Semantiek: Datums worden gedefinieerd als drietallen $(y, m, d)$ $(y, m, d)$ volgens de regels van de Gregoriaanse kalender. Periodes zijn drietallen $(n_y, n_m, n_d)$ $(n_{y}, n_{m}, n_{d})$ . Het raamwerk hanteert een specifieke semantiek voor datum-periode-optelling (consistent met bibliotheken zoals Java's java.time en Python's dateutil):
1. Jaar/Maand-optelling: Wordt eerst uitgevoerd, met overflow-handling die ongeldige datums naar beneden afrondt (bijvoorbeeld 31 januari + 1 maand $\to$ 28/29 februari).
2. Dag-optelling: Wordt tweede uitgevoerd, waarbij overflows naar volgende maanden worden toegestaan.
  Deze semantiek zorgt ervoor dat het toevoegen van een periode aan een geldige datum altijd resulteert in een geldige datum (Stelling 1).
Invoertaal: De taal ondersteunt vrije datumvariabelen, datum/periode-aritmetiek, vergelijkingen en componentextractie (jaar, maand, dag). De logica is bewezen decidabel via reductie tot QF-LIA.

Oplossingsstrategieën

De auteurs stellen vijf coderingsstrategieën voor om DateSAT-constraints af te beelden op SMT-formules over gehele getallen, geïmplementeerd met de Z3-oplosser. Deze strategieën wisselen af tussen logische diepte (nesting van if-then-else-blokken) en aritmetische complexiteit (aantal geheeltallige bewerkingen):

Naive Codering: Stelt datums voor als $(y, m, d)$ -tupels. Datum-periode-aritmetiek wordt stap voor stap uitgerold, wat leidt tot een logische diepte van $O(|n_d|)$ vanwege geneste ITE's voor dag-overflows.
Epoch-gebaseerde Codering: Stelt datums voor als een enkel geheel getal $\Delta$ (dagen sinds een vaste epoch). De auteurs kiezen 1 maart 2000 als epoch om schrikkellijarcycli te vereenvoudigen (1461-dag cycli). Dag-optelling wordt $O(1)$ , maar jaar/maand-aritmetiek vereist het converteren van $\Delta$ terug naar $(y, m, d)$ , wat complexe deling/modulo-constraints introduceert.
Hybride Codering: Houdt zowel $(y, m, d)$ - als $\Delta$ -representaties bij voor elke datum. Het maakt gebruik van lazy consistentievlaggen om alleen bij behoefte tussen representaties te schakelen (bijvoorbeeld $\Delta$ gebruiken voor alleen-dag-bewerkingen en $(y, m, d)$ voor maand-aritmetiek).
Alpha-Beta Codering: Stelt een datum voor als een paar $(\alpha, \beta)$ , waarbij $\alpha$ het aantal maanden sinds de epoch is en $\beta$ de dag-offset binnen die maand. Dit vermijdt diepe nesting door modulair rekenen te gebruiken om maandlengtes te bepalen.
Alpha-Beta-Table Codering: Een optimalisatie van de Alpha-Beta-strategie voor begrenste instanties (1900–2100). Het maakt gebruik van vooraf berekende opzoektabellen (48-maand cycli) voor dagen-per-maand en dagen-voor-maand, waarbij complexe aritmetiek wordt vervangen door array-opzoeking en modulo-bewerkingen.

Correctheidsverificatie

De correctheid van de Epoch-gebaseerde, Hybride en Alpha-Beta-coderingen ten opzichte van de Naive baseline is formeel geverifieerd met de Verus bewijshulp. De bewijzen stellen vast dat deze coderingen equisatisfiable zijn met de Naive codering voor goed gevormde constraints.

Benchmark en Evaluatie

De auteurs hebben DateSATBench samengesteld, een dataset van 450 constraints uit drie bronnen:

LLM-gegenereerd (100): Gericht op semantische randgevallen (bijvoorbeeld schrikkellijaren, maandgrenzen).
Grammatica-gesampleerd (150): Willekeurig gegenereerd om de prestaties van de oplosser te testen op moeilijke/onvervulbare gevallen.
Juridisch onderbouwd (200): Afgeleid van statuten van de Amerikaanse Internal Revenue Code (bijvoorbeeld termijnen voor verkiezingen volgens Sectie 338(g)).

Resultaten:

Prestaties: Op de juridische dataset behaalde de Alpha-Beta-Table strategie de beste prestaties, waarbij 98,45% van de constraints werd opgelost met een mediane tijd van 0,13 seconden.
Snelheidswinst: In vergelijking met de Naive baseline bood Alpha-Beta-Table een mediane snelheidswinst van 2,41× over de volledige benchmark-suite (430 oplosbare constraints).
Efficiëntie: De Hybride strategie toonde significante verbeteringen op grammatica-gesampleerde constraints (mediane tijd 4,69s versus 28,07s voor Naive), terwijl de Epoch-gebaseerde strategie excelleerde in eenvoudige LLM-gegenereerde gevallen.
Schaalbaarheid: Naarmate constraints complexer werden, werd de keuze van coderingsstrategie steeds kritischer, waarbij de Alpha-Beta-Table strategie robuustheid behield waar andere uitliepen op time-out.

Belangrijkste Bijdragen

Formalisering: Een rigoureuze definitie van vervulbaarheid van datum- en periode-constraints, inclusief semantiek voor aritmetiek en vergelijking.
Strategieën: Vijf distincte coderingsstrategieën voor het reduceren van datumslogica tot geheeltallige aritmetiek, waarbij logische diepte en aritmetische complexiteit in evenwicht worden gebracht.
Implementatie: Een open-source Python-implementatie met Z3, beschikbaar op cmu-pasta/DateSAT.
Benchmark: De DateSATBench-suite (450 constraints) voor het evalueren van tools voor datumredenering.
Evaluatie: Een empirische studie die aantoont dat gespecialiseerde coderingen aanzienlijk beter presteren dan naïeve benaderingen, met name voor complexe juridische en synthetische constraints.

Betekenis en Aanspraken

Het artikel claimt het eerste raamwerk te presenteren voor het uitdrukken en oplossen van vervulbaarheidsconstraints met betrekking tot datums en kalenderperiodes. De betekenis hiervan ligt in:

Het Overbruggen van de Kloof: Het aanpakken van het gebrek aan tool-ondersteuning voor formele redenering over datumslogica, een bekende bron van softwarefouten (bijvoorbeeld fouten bij patentvervaltijden, clouduitval).
Verificatie mogelijk maken: Het bieden van een mechanisme om equivalentie te verifiëren bij code-refactoring (bijvoorbeeld het vervangen van bibliotheekoproepen door aangepaste logica) en juridische naleving te valideren zonder afhankelijkheid van foutgevoelige LLM's of exhaustieve concrete testen.
Fundament voor toekomstig werk: Het bieden van een benchmark en oplosser die kunnen worden geïntegreerd in programma-verificatietools en Agentic AI-systemen die nauwkeurige temporele redenering vereisen.

De auteurs blijven bescheiden en merken op dat hoewel hun huidige implementatie Z3 als backend gebruikt, toekomstig werk zou kunnen leiden tot het integreren van datumslogica direct in SMT-LIB als een nieuwe theorie of het verkennen van bitvector-coderingen voor begrenste instanties. Ze benadrukken dat hun werk een fundamentele stap is naar principiële redenering over temporele berekeningen.