💻 computer science

DateSAT: A Framework for Solving Date and Period Constraints

Este artículo presenta DateSAT, el primer marco para expresar y resolver formalmente restricciones de satisfacibilidad que involucran fechas y periodos del calendario reduciéndolas a fórmulas SMT basadas en enteros, y valida su eficacia mediante una evaluación empírica en un conjunto de datos curado de 450 restricciones.

Autores originales: Leyi Cui, Shrey Tiwari, Rohan Padhye

Publicado 2026-05-26

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Leyi Cui, Shrey Tiwari, Rohan Padhye

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás intentando resolver un acertijo: "Anteayer tenía 25 años y el próximo año cumpliré 28". ¿Cuándo es esto posible?

Para un humano, esto es un divertido rompecabezas mental. Para una computadora, es una pesadilla. Las computadoras son excelentes en matemáticas, pero son terribles con los calendarios. No "saben" que febrero a veces tiene 29 días, o que sumar "un mes" al 31 de enero no da como resultado el 31 de febrero (porque ese día no existe).

Este artículo presenta DateSAT, una nueva herramienta diseñada para enseñar a las computadoras a pensar sobre fechas y periodos de tiempo sin confundirse.

Así es como los autores lo desglosaron, utilizando algunas analogías cotidianas:

1. El Problema: Las Computadoras Odian el Tiempo "Vago"

Piensa en una computadora como un bibliotecario muy estricto que solo entiende números exactos. Si le pides que sume "1 mes" a una fecha, entra en pánico si las matemáticas no coinciden perfectamente.

El Desorden del Mundo Real: El artículo señala que esto no es solo un acertijo. Software real se ha bloqueado debido a errores de fecha. Por ejemplo, un error hizo que las bombas de gasolina en Nueva Zelanda dejaran de funcionar el 29 de febrero porque la computadora no sabía cómo manejar el día extra. Otro error hizo que la Oficina de Patentes de EE. UU. otorgara fechas de vencimiento incorrectas a miles de patentes.
El Fallo de la IA: Incluso la IA moderna (como los chatbots que usamos hoy) suele equivocarse con estos acertijos de fechas porque no están diseñadas para realizar matemáticas de calendario estrictas.

2. La Solución: DateSAT (El "Traductor de Calendarios")

Los autores construyeron un marco llamado DateSAT. Piensa en DateSAT como un traductor que se sienta entre la compleja pregunta sobre fechas de un humano y el cerebro matemático estricto de una computadora.

La Entrada: Le das a DateSAT una pregunta como: "¿Es posible que una empresa realice una elección legal 500 días después de comprar acciones, si el plazo límite es 9 meses después de la 'fecha de adquisición'?"
La Magia: DateSAT traduce este problema de calendario desordenado y en lenguaje humano a un problema matemático limpio y estricto que un solucionador informático (llamado solucionador SMT) puede manejar perfectamente.

3. Cómo Funciona: Cinco "Mapas" Diferentes

La parte más difícil del proyecto fue averiguar cómo traducir el calendario a matemáticas. Los autores probaron cinco estrategias diferentes, como intentar navegar una ciudad usando cinco tipos diferentes de mapas:

El Mapa Ingenuo (El Caminante Paso a Paso): Este método intenta caminar día a día. Si sumas 100 días, da 100 pasos diminutos. Es muy preciso pero increíblemente lento, como cruzar un país paso a paso.
El Mapa de Época (El Marcador de Hitos): Este método elige un punto de partida fijo (como "1 de marzo de 2000") y cuenta cuántos días han pasado desde entonces. Es excelente para sumar días, pero se confunde cuando necesitas saltar por "meses" o "años".
El Mapa Híbrido (La Vista Dual): Esta estrategia usa dos mapas a la vez. Usa el mapa de "Hitos" para sumar días y el mapa de "Paso a Paso" para sumar meses. Cambia entre ellos solo cuando es necesario para ahorrar tiempo.
El Mapa Alfa-Beta (La Cuadrícula del Calendario): Este es un atajo inteligente. En lugar de contar cada día individual, cuenta "cuántos meses han pasado" y "cuántos días hay en el mes actual". Es como saber que estás en "Calle 5, Casa 3" en lugar de contar cada casa desde el inicio de la ciudad.
El Mapa Alfa-Beta-Tabla (La Hoja de Trucos): Este es el ganador. Usa la idea de la "Cuadrícula del Calendario" pero añade una hoja de trucos preescrita. Dado que los calendarios se repiten en ciclos (cada 4 años), la herramienta simplemente busca la respuesta en una tabla en lugar de hacer las matemáticas cada vez. Este es el método más rápido, resolviendo problemas complejos hasta 2.4 veces más rápido que el lento método "Ingenuo".

4. La Prueba de Fuego: DateSATBench

Para demostrar que su herramienta funciona, los autores no simplemente inventaron preguntas aleatorias. Construyeron un conjunto de pruebas llamado DateSATBench con 450 problemas diferentes:

100 fueron generados por IA para encontrar casos límite complicados.
150 fueron pruebas de estrés generadas aleatoriamente diseñadas para romper el sistema.
200 fueron extraídos de leyes fiscales reales de EE. UU. para ver si podía manejar documentos legales reales.

Los Resultados:

La herramienta resolvió el 85% de los problemas en menos de un minuto.
El método de "Hoja de Trucos" (Alfa-Beta-Tabla) fue el campeón indiscutible, resolviendo problemas en una fracción de segundo que le tomaron mucho más tiempo al método "Ingenuo".
En una prueba, encontraron un error oculto en una función de Python que dos programadores diferentes escribieron para verificar si una fecha estaba dentro de una ventana de 18 meses. Los probadores humanos pasaron por alto el error, pero DateSAT lo encontró instantáneamente.

5. Por Qué Esto Importa

El artículo concluye que DateSAT es la primera herramienta que permite a las computadoras razonar sobre fechas y periodos de manera simbólica. Esto significa que puede verificar si un fragmento de código es lógicamente correcto en cuanto al tiempo, o si un contrato legal tiene una contradicción en sus fechas, sin necesidad de ejecutar el código un millón de veces para ver si se bloquea.

En resumen, DateSAT le da a las computadoras una comprensión de "sentido común" de los calendarios, convirtiendo la lógica relacionada con fechas, que antes era fuente de errores costosos, en un problema matemático resoluble.

Resumen Técnico: DateSAT

Enunciado del Problema

Las fechas y los periodos del calendario son omnipresentes en el análisis de software, el procesamiento de datos y el razonamiento sobre documentos legales. Sin embargo, la lógica calendárica es inherentemente propensa a errores debido a las longitudes irregulares de los meses, los años bisiestos y las ambigüedades en la aritmética de periodos (por ejemplo, la no conmutatividad de añadir "un mes" frente a "un día"). Las herramientas existentes de análisis y verificación de programas carecen de soporte nativo para fechas, lo que obliga a depender de la ejecución concreta o del rastreo simbólico complejo de implementaciones de bibliotecas (por ejemplo, dateutil), lo que a menudo conduce a una explosión de restricciones. Además, los Modelos de Lenguaje Grandes (LLM) fallan frecuentemente en tareas de razonamiento temporal. El problema central abordado es la falta de un marco formal para expresar y resolver restricciones de satisfacibilidad que involucren fechas y periodos del calendario de manera simbólica.

Metodología

El artículo introduce DateSAT, un marco que extiende la aritmética lineal entera sin cuantificadores (QF-LIA) con dos nuevos tipos: Date (Fecha) y Period (Periodo).

Formalización

Semántica: Las fechas se definen como ternas $(y, m, d)$ $(y, m, d)$ siguiendo las reglas del calendario gregoriano. Los periodos son ternas $(n_y, n_m, n_d)$ $(n_{y}, n_{m}, n_{d})$ . El marco adopta una semántica específica para la suma de fecha-periodo (consistente con bibliotecas como java.time de Java y dateutil de Python):
1. Suma de Año/Mes: Se realiza primero, con manejo de desbordamiento que redondea hacia abajo las fechas inválidas (por ejemplo, 31 de enero + 1 mes $\to$ 28/29 de febrero).
2. Suma de Días: Se realiza segundo, permitiendo desbordamientos hacia meses subsiguientes.
  Esta semántica garantiza que añadir un periodo a una fecha válida siempre resulte en una fecha válida (Teorema 1).
Lenguaje de Entrada: El lenguaje admite variables de fecha libres, aritmética de fecha/periodo, comparaciones y extracción de componentes (año, mes, día). Se ha demostrado que la lógica es decidible mediante reducción a QF-LIA.

Estrategias de Resolución

Los autores proponen cinco estrategias de codificación para mapear las restricciones de DateSAT a fórmulas SMT sobre enteros, implementadas utilizando el solucionador Z3. Estas estrategias ofrecen compensaciones entre la profundidad lógica (anidamiento de bloques if-then-else) y la complejidad aritmética (número de operaciones enteras):

Codificación Ingenua: Representa las fechas como ternas $(y, m, d)$ . La aritmética de fecha-periodo se desarrolla paso a paso, lo que conduce a una profundidad lógica de $O(|n_d|)$ debido a los ITE anidados para desbordamientos de días.
Codificación Basada en Época: Representa las fechas como un único entero $\Delta$ (días desde una época fija). Los autores seleccionan el 1 de marzo de 2000 como época para simplificar los ciclos de años bisiestos (ciclos de 1461 días). La suma de días se vuelve $O(1)$ , pero la aritmética de año/mes requiere convertir $\Delta$ de nuevo a $(y, m, d)$ , introduciendo restricciones complejas de división/módulo.
Codificación Híbrida: Mantiene ambas representaciones $(y, m, d)$ y $\Delta$ para cada fecha. Utiliza banderas de consistencia perezosa para cambiar entre representaciones solo cuando es necesario (por ejemplo, usar $\Delta$ para operaciones solo de días y $(y, m, d)$ para aritmética de meses).
Codificación Alfa-Beta: Representa una fecha como un par $(\alpha, \beta)$ , donde $\alpha$ es el número de meses desde la época y $\beta$ es el desplazamiento de días dentro de ese mes. Esto evita un anidamiento profundo utilizando aritmética modular para determinar las longitudes de los meses.
Codificación Alfa-Beta-Tabla: Una optimización de la estrategia Alfa-Beta para instancias acotadas (1900–2100). Utiliza tablas de búsqueda precalculadas (ciclos de 48 meses) para los días del mes y los días antes del mes, reemplazando la aritmética compleja con búsquedas en arrays y operaciones de módulo.

Verificación de Corrección

La corrección de las codificaciones Basada en Época, Híbrida y Alfa-Beta en relación con la base de referencia Ingenua fue verificada formalmente utilizando el asistente de pruebas Verus. Las pruebas establecen que estas codificaciones son equisatisfacibles con la codificación Ingenua para restricciones bien formadas.

Benchmark y Evaluación

Los autores curaron DateSATBench, un conjunto de datos de 450 restricciones procedentes de tres fuentes:

Sintetizado por LLM (100): Centrado en casos límite semánticos (por ejemplo, años bisiestos, límites de meses).
Muestreado por Gramática (150): Generado aleatoriamente para poner a prueba el rendimiento del solucionador en casos difíciles/insatisfacibles.
Fundamentado Legalmente (200): Derivado de estatutos del Código de Rentas Internas de EE. UU. (por ejemplo, plazos para elecciones según la Sección 338(g)).

Resultados:

Rendimiento: En el conjunto de datos legal, la estrategia Alfa-Beta-Tabla logró el mejor rendimiento, resolviendo el 98,45 % de las restricciones con un tiempo mediano de 0,13 segundos.
Aceleración: En comparación con la base de referencia Ingenua, Alfa-Beta-Tabla proporcionó una aceleración mediana de 2,41× en toda la suite de benchmarks (430 restricciones resolubles).
Eficiencia: La estrategia Híbrida mostró mejoras significativas en las restricciones muestreadas por gramática (tiempo mediano de 4,69 s frente a 28,07 s para la Ingenua), mientras que la estrategia Basada en Época destacó en casos simples sintetizados por LLM.
Escalabilidad: A medida que las restricciones se volvían más complejas, la elección de la estrategia de codificación se volvió cada vez más crítica, manteniendo la estrategia Alfa-Beta-Tabla su robustez donde otras agotaron el tiempo de espera.

Contribuciones Clave

Formalización: Una definición rigurosa de la satisfacibilidad de restricciones de fecha y periodo, incluyendo semántica para aritmética y comparación.
Estrategias: Cinco estrategias de codificación distintas para reducir la lógica de fechas a aritmética entera, equilibrando la profundidad lógica y la complejidad aritmética.
Implementación: Una implementación de código abierto en Python utilizando Z3, disponible en cmu-pasta/DateSAT.
Benchmark: La suite DateSATBench (450 restricciones) para evaluar herramientas de razonamiento sobre fechas.
Evaluación: Un estudio empírico que demuestra que las codificaciones especializadas superan significativamente a los enfoques ingenuos, particularmente para restricciones legales y sintéticas complejas.

Significado y Afirmaciones

El artículo afirma presentar el primer marco para expresar y resolver restricciones de satisfacibilidad que involucren fechas y periodos del calendario. Su importancia radica en:

Cerrar la Brecha: Abordar la falta de soporte de herramientas para el razonamiento formal sobre la lógica de fechas, una fuente conocida de errores de software (por ejemplo, errores en la expiración de patentes, interrupciones en la nube).
Habilitar la Verificación: Proporcionar un mecanismo para verificar la equivalencia en la refactorización de código (por ejemplo, reemplazar llamadas a bibliotecas con lógica personalizada) y validar el cumplimiento legal sin depender de LLMs propensos a errores o pruebas concretas exhaustivas.
Fundamento para Trabajo Futuro: Ofrecer un benchmark y un solucionador que pueden integrarse en herramientas de verificación de programas y sistemas de IA Agente que requieran un razonamiento temporal preciso.

Los autores se mantienen modestos, señalando que, aunque su implementación actual utiliza Z3 como backend, el trabajo futuro podría implicar integrar la lógica de fechas directamente en SMT-LIB como una nueva teoría o explorar codificaciones de vectores de bits para instancias acotadas. Enfatizan que su trabajo es un paso fundamental hacia un razonamiento principiado sobre los cálculos temporales.