💻 computer science

DateSAT: A Framework for Solving Date and Period Constraints

Este artigo apresenta o DateSAT, o primeiro framework para expressar e resolver formalmente restrições de satisfabilidade envolvendo datas e períodos de calendário, reduzindo-as a fórmulas SMT baseadas em inteiros, e valida sua eficácia por meio de uma avaliação empírica em um conjunto de dados curado de 450 restrições.

Autores originais: Leyi Cui, Shrey Tiwari, Rohan Padhye

Publicado 2026-05-26

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Leyi Cui, Shrey Tiwari, Rohan Padhye

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está tentando resolver um enigma: "Anteontem eu tinha 25 anos, e no ano que vem farei 28." Quando isso é possível?

Para um humano, isso é um divertido quebra-cabeça mental. Para um computador, é um pesadelo. Computadores são ótimos em matemática, mas são terríveis em calendários. Eles não "sabem" que fevereiro às vezes tem 29 dias, ou que adicionar "um mês" a 31 de janeiro não resulta em 31 de fevereiro (porque esse dia não existe).

Este artigo apresenta o DateSAT, uma nova ferramenta projetada para ensinar computadores a pensar sobre datas e períodos sem se confundir.

Veja como os autores desdobraram isso, usando algumas analogias do cotidiano:

1. O Problema: Computadores Odeiam Tempo "Vago"

Pense em um computador como um bibliotecário muito rigoroso que só entende números exatos. Se você pedir para ele adicionar "1 mês" a uma data, ele entra em pânico se a matemática não bater perfeitamente.

A Bagunça do Mundo Real: O artigo aponta que isso não é apenas um enigma. Softwares reais travaram devido a bugs de data. Por exemplo, um bug fez com que bombas de combustível na Nova Zelândia parassem de funcionar em 29 de fevereiro porque o computador não sabia como lidar com o dia extra. Outro bug fez com que o Escritório de Patentes dos EUA concedesse datas de expiração erradas para milhares de patentes.
O Glitch da IA: Até mesmo a IA moderna (como os chatbots que usamos hoje) frequentemente erra esses enigmas de data porque não foram construídos para fazer matemática de calendário rigorosa.

2. A Solução: DateSAT (O "Tradutor de Calendário")

Os autores criaram um framework chamado DateSAT. Pense no DateSAT como um tradutor que fica entre a complexa pergunta sobre datas de um humano e o cérebro matemático rigoroso de um computador.

A Entrada: Você dá ao DateSAT uma pergunta como: "É possível que uma empresa realize uma eleição legal 500 dias após comprar ações, se o prazo for de 9 meses após a 'data de aquisição'?"
A Magia: O DateSAT traduz esse problema de calendário confuso, em linguagem humana, em um problema matemático limpo e rigoroso que um resolvedor de computador (chamado resolvedor SMT) pode lidar perfeitamente.

3. Como Funciona: Cinco "Mapas" Diferentes

A parte mais difícil do projeto foi descobrir como traduzir o calendário em matemática. Os autores tentaram cinco estratégias diferentes, como tentar navegar por uma cidade usando cinco tipos diferentes de mapas:

O Mapa Ingênuo (O Caminhante Passo a Passo): Este método tenta caminhar dia a dia. Se você adicionar 100 dias, ele dá 100 passinhos minúsculos. É muito preciso, mas incrivelmente lento, como atravessar um país um pé de cada vez.
O Mapa de Época (O Marcador de Marco): Este método escolhe um ponto de partida fixo (como "1º de março de 2000") e conta quantos dias se passaram desde então. É ótimo para adicionar dias, mas fica confuso quando você precisa pular por "meses" ou "anos".
O Mapa Híbrido (A Visão Dupla): Esta estratégia usa dois mapas ao mesmo tempo. Usa o mapa de "Marco" para adicionar dias e o mapa "Passo a Passo" para adicionar meses. Alterna entre eles apenas quando necessário para economizar tempo.
O Mapa Alfa-Beta (A Grade do Calendário): Esta é uma atalho inteligente. Em vez de contar cada dia individualmente, ele conta "quantos meses se passaram" e "quantos dias no mês atual". É como saber que você está na "Rua 5, Casa 3" em vez de contar cada casa desde o início da cidade.
O Mapa Alfa-Beta-Tabela (A Cola): Este é o vencedor. Usa a ideia da "Grade do Calendário", mas adiciona uma cola pré-escrita. Como os calendários se repetem em ciclos (a cada 4 anos), a ferramenta apenas consulta a resposta em uma tabela em vez de fazer a matemática toda vez. Este é o método mais rápido, resolvendo problemas complexos até 2,4 vezes mais rápido do que o método lento "Ingênuo".

4. O Teste de Estrada: DateSATBench

Para provar que sua ferramenta funciona, os autores não apenas inventaram perguntas aleatórias. Eles construíram um conjunto de testes chamado DateSATBench com 450 problemas diferentes:

100 foram gerados por IA para encontrar casos extremos complicados.
150 foram "testes de estresse" gerados aleatoriamente, projetados para quebrar o sistema.
200 foram extraídos de leis fiscais reais dos EUA para ver se conseguia lidar com documentos legais reais.

Os Resultados:

A ferramenta resolveu 85% dos problemas em menos de um minuto.
O método "Cola" (Alfa-Beta-Tabela) foi o campeão claro, resolvendo problemas em frações de segundo que levavam muito mais tempo para o método "Ingênuo".
Em um teste, eles encontraram um bug oculto em uma função Python que dois programadores diferentes escreveram para verificar se uma data estava dentro de uma janela de 18 meses. Os testadores humanos perderam o bug, mas o DateSAT o encontrou instantaneamente.

5. Por Que Isso Importa

O artigo conclui que o DateSAT é a primeira ferramenta que permite que computadores raciocinem sobre datas e períodos simbolicamente. Isso significa que pode verificar se um trecho de código é logicamente correto em relação ao tempo, ou se um contrato legal tem uma contradição em suas datas, sem precisar executar o código um milhão de vezes para ver se ele trava.

Em resumo, o DateSAT dá aos computadores uma compreensão de "senso comum" de calendários, transformando a lógica relacionada a datas de uma fonte de bugs caros em um problema matemático solucionável.

Resumo Técnico: DateSAT

Declaração do Problema

Datas e períodos de calendário são ubíquos na análise de software, processamento de dados e raciocínio sobre documentos legais. No entanto, a lógica calendárica é inerentemente propensa a erros devido a comprimentos irregulares de meses, anos bissextos e ambiguidades na aritmética de períodos (por exemplo, a não comutatividade de adicionar "um mês" versus "um dia"). As ferramentas existentes de análise e verificação de programas carecem de suporte nativo para datas, forçando a dependência de execução concreta ou rastreamento simbólico complexo de implementações de bibliotecas (por exemplo, dateutil), o que frequentemente leva à explosão de restrições. Além disso, os Grandes Modelos de Linguagem (LLMs) frequentemente falham em tarefas de raciocínio temporal. O problema central abordado é a falta de um quadro formal para expressar e resolver restrições de satisfabilidade envolvendo datas e períodos de calendário simbolicamente.

Metodologia

O artigo apresenta o DateSAT, um quadro que estende a aritmética linear inteira sem quantificadores (QF-LIA) com dois novos tipos: Date (Data) e Period (Período).

Formalização

Semântica: Datas são definidas como triplas $(y, m, d)$ $(y, m, d)$ seguindo as regras do calendário gregoriano. Períodos são triplas $(n_y, n_m, n_d)$ $(n_{y}, n_{m}, n_{d})$ . O quadro adota uma semântica específica para adição data-período (consistente com bibliotecas como java.time do Java e dateutil do Python):
1. Adição de Ano/Mês: Realizada primeiro, com tratamento de estouro que arredonda para baixo datas inválidas (por exemplo, 31 de jan + 1 mês $\to$ 28/29 de fev).
2. Adição de Dia: Realizada segundo, permitindo estouros em meses subsequentes.
  Esta semântica garante que adicionar um período a uma data válida sempre resulte em uma data válida (Teorema 1).
Linguagem de Entrada: A linguagem suporta variáveis de data livres, aritmética data/período, comparações e extração de componentes (ano, mês, dia). A lógica é provada decidível via redução para QF-LIA.

Estratégias de Resolução

Os autores propõem cinco estratégias de codificação para mapear restrições do DateSAT para fórmulas SMT sobre inteiros, implementadas usando o solucionador Z3. Essas estratégias negociam entre profundidade lógica (aninhamento de blocos if-then-else) e complexidade aritmética (número de operações inteiras):

Codificação Ingênua: Representa datas como tuplas $(y, m, d)$ . A aritmética data-período é desenrolada passo a passo, levando a uma profundidade lógica de $O(|n_d|)$ devido a ITEs aninhados para estouros de dias.
Codificação Baseada em Época: Representa datas como um único inteiro $\Delta$ (dias desde uma época fixa). Os autores selecionaram 1º de março de 2000 como a época para simplificar ciclos de anos bissextos (ciclos de 1461 dias). A adição de dias torna-se $O(1)$ , mas a aritmética de ano/mês requer converter $\Delta$ de volta para $(y, m, d)$ , introduzindo restrições complexas de divisão/módulo.
Codificação Híbrida: Mantém ambas as representações $(y, m, d)$ e $\Delta$ para cada data. Usa bandeiras de consistência preguiçosa para alternar entre representações apenas quando necessário (por exemplo, usando $\Delta$ para operações apenas de dia e $(y, m, d)$ para aritmética de mês).
Codificação Alfa-Beta: Representa uma data como um par $(\alpha, \beta)$ , onde $\alpha$ é o número de meses desde a época e $\beta$ é o deslocamento de dia dentro desse mês. Isso evita aninhamento profundo ao usar aritmética modular para determinar comprimentos de meses.
Codificação Alfa-Beta-Tabela: Uma otimização da estratégia Alfa-Beta para instâncias limitadas (1900–2100). Utiliza tabelas de consulta pré-computadas (ciclos de 48 meses) para dias-no-mês e dias-antes-do-mês, substituindo aritmética complexa por consultas de array e operações de módulo.

Verificação de Corretude

A corretude das codificações Baseada em Época, Híbrida e Alfa-Beta em relação à base Ingênua foi formalmente verificada usando o assistente de prova Verus. As provas estabelecem que essas codificações são equissatisfatíveis com a codificação Ingênua para restrições bem-formadas.

Benchmark e Avaliação

Os autores curaram o DateSATBench, um conjunto de dados de 450 restrições de três fontes:

Sintetizado por LLM (100): Focado em casos de borda semânticos (por exemplo, anos bissextos, limites de mês).
Amostrado por Gramática (150): Gerado aleatoriamente para testar o desempenho do solucionador em casos difíceis/insatisfatíveis.
Fundamentado Legalmente (200): Derivado de estatutos do Código de Receita Interna dos EUA (por exemplo, prazos para eleições da Seção 338(g)).

Resultados:

Desempenho: No conjunto de dados legal, a estratégia Alfa-Beta-Tabela alcançou o melhor desempenho, resolvendo 98,45% das restrições com um tempo mediano de 0,13 segundos.
Aceleração: Comparado à base Ingênua, Alfa-Beta-Tabela forneceu uma aceleração mediana de 2,41× em todo o conjunto de benchmarks (430 restrições solucionáveis).
Eficiência: A estratégia Híbrida mostrou melhorias significativas em restrições amostradas por gramática (tempo mediano de 4,69s vs. 28,07s para Ingênua), enquanto a estratégia Baseada em Época se destacou em casos simples sintetizados por LLM.
Escalabilidade: À medida que as restrições se tornavam mais complexas, a escolha da estratégia de codificação tornou-se cada vez mais crítica, com a estratégia Alfa-Beta-Tabela mantendo robustez onde outras esgotaram o tempo.

Contribuições Principais

Formalização: Uma definição rigorosa da satisfabilidade de restrições de data e período, incluindo semântica para aritmética e comparação.
Estratégias: Cinco estratégias de codificação distintas para reduzir a lógica de datas à aritmética inteira, equilibrando profundidade lógica e complexidade aritmética.
Implementação: Uma implementação em Python de código aberto usando Z3, disponível em cmu-pasta/DateSAT.
Benchmark: O conjunto de ferramentas DateSATBench (450 restrições) para avaliar ferramentas de raciocínio sobre datas.
Avaliação: Um estudo empírico demonstrando que codificações especializadas superam significativamente abordagens ingênuas, particularmente para restrições legais e sintéticas complexas.

Significado e Alegações

O artigo alega apresentar o primeiro quadro para expressar e resolver restrições de satisfabilidade envolvendo datas e períodos de calendário. Seu significado reside em:

Preenchendo a Lacuna: Abordar a falta de suporte de ferramentas para raciocínio formal sobre lógica de datas, uma fonte conhecida de bugs de software (por exemplo, erros de expiração de patentes, interrupções em nuvem).
Habilitando Verificação: Fornecer um mecanismo para verificar equivalência na refatoração de código (por exemplo, substituir chamadas de biblioteca por lógica personalizada) e validar conformidade legal sem depender de LLMs propensos a erros ou testes concretos exaustivos.
Fundação para Trabalho Futuro: Oferecer um benchmark e solucionador que podem ser integrados em ferramentas de verificação de programas e sistemas de IA Agêntica que exigem raciocínio temporal preciso.

Os autores permanecem modestos, observando que, embora sua implementação atual use o Z3 como backend, trabalhos futuros poderiam envolver integrar a lógica de datas diretamente no SMT-LIB como uma nova teoria ou explorar codificações de bitvector para instâncias limitadas. Eles enfatizam que seu trabalho é um passo fundamental em direção a um raciocínio principiado sobre computações temporais.