💻 computer science

DateSAT: A Framework for Solving Date and Period Constraints

This paper introduces DateSAT, the first framework for formally expressing and solving satisfiability constraints involving dates and calendar periods by reducing them to integer-based SMT formulas, and validates its effectiveness through an empirical evaluation on a curated dataset of 450 constraints.

Original authors: Leyi Cui, Shrey Tiwari, Rohan Padhye

Published 2026-05-26

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Leyi Cui, Shrey Tiwari, Rohan Padhye

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to solve a riddle: "The day before yesterday I was 25, and next year I will turn 28." When is this possible?

To a human, this is a fun brain teaser. To a computer, it's a nightmare. Computers are great at math, but they are terrible at calendars. They don't "know" that February sometimes has 29 days, or that adding "one month" to January 31st doesn't land on February 31st (because that day doesn't exist).

This paper introduces DateSAT, a new tool designed to teach computers how to think about dates and time periods without getting confused.

Here is how the authors broke it down, using some everyday analogies:

1. The Problem: Computers Hate "Fuzzy" Time

Think of a computer as a very strict librarian who only understands exact numbers. If you ask it to add "1 month" to a date, it panics if the math doesn't line up perfectly.

The Real-World Mess: The paper points out that this isn't just a puzzle. Real software has crashed because of date bugs. For example, a bug once caused gas pumps in New Zealand to stop working on February 29th because the computer didn't know how to handle the extra day. Another bug caused the US Patent Office to give the wrong expiration dates to thousands of patents.
The AI Glitch: Even modern AI (like the chatbots we use today) often gets these date riddles wrong because they aren't built to do strict calendar math.

2. The Solution: DateSAT (The "Calendar Translator")

The authors built a framework called DateSAT. Think of DateSAT as a translator that sits between a human's complex date question and a computer's strict math brain.

The Input: You give DateSAT a question like, "Is it possible for a company to make a legal election 500 days after buying stock, if the deadline is 9 months after the 'acquisition date'?"
The Magic: DateSAT translates this messy, human-language calendar problem into a clean, strict math problem that a computer solver (called an SMT solver) can handle perfectly.

3. How It Works: Five Different "Maps"

The hardest part of the project was figuring out how to translate the calendar into math. The authors tried five different strategies, like trying to navigate a city using five different types of maps:

The Naive Map (The Step-by-Step Walker): This method tries to walk day-by-day. If you add 100 days, it takes 100 tiny steps. It's very accurate but incredibly slow, like walking across a country one foot at a time.
The Epoch Map (The Milestone Marker): This method picks a fixed starting point (like "March 1, 2000") and counts how many days have passed since then. It's great for adding days, but getting confused when you need to jump by "months" or "years."
The Hybrid Map (The Dual-View): This strategy uses two maps at once. It uses the "Milestone" map for adding days and the "Step-by-Step" map for adding months. It switches between them only when necessary to save time.
The Alpha-Beta Map (The Calendar Grid): This is a clever shortcut. Instead of counting every single day, it counts "how many months have passed" and "how many days into the current month." It's like knowing you are on "Street 5, House 3" instead of counting every house from the start of the city.
The Alpha-Beta-Table Map (The Cheat Sheet): This is the winner. It uses the "Calendar Grid" idea but adds a pre-written cheat sheet. Since calendars repeat in cycles (every 4 years), the tool just looks up the answer in a table instead of doing the math every time. This is the fastest method, solving complex problems up to 2.4 times faster than the slow "Naive" method.

4. The Test Drive: DateSATBench

To prove their tool works, the authors didn't just make up random questions. They built a test suite called DateSATBench with 450 different problems:

100 were generated by AI to find tricky edge cases.
150 were randomly generated "stress tests" designed to break the system.
200 were pulled from real US tax laws to see if it could handle actual legal documents.

The Results:

The tool solved 85% of the problems in under a minute.
The "Cheat Sheet" method (Alpha-Beta-Table) was the clear champion, solving problems in a fraction of a second that took the "Naive" method much longer.
In one test, they found a hidden bug in a Python function that two different programmers wrote to check if a date was within an 18-month window. The human testers missed the bug, but DateSAT found it instantly.

5. Why This Matters

The paper concludes that DateSAT is the first tool that allows computers to reason about dates and periods symbolically. This means it can check if a piece of code is logically correct regarding time, or if a legal contract has a contradiction in its dates, without needing to run the code a million times to see if it crashes.

In short, DateSAT gives computers a "common sense" understanding of calendars, turning date-related logic from a source of expensive bugs into a solvable math problem.

Technical Summary: DateSAT

Problem Statement

Dates and calendar periods are ubiquitous in software analysis, data processing, and legal document reasoning. However, calendrical logic is inherently error-prone due to irregular month lengths, leap years, and ambiguities in period arithmetic (e.g., the non-commutativity of adding "one month" vs. "one day"). Existing program analysis and verification tools lack native support for dates, forcing reliance on concrete execution or complex symbolic tracing of library implementations (e.g., dateutil), which often leads to constraint explosion. Furthermore, Large Language Models (LLMs) frequently fail at temporal reasoning tasks. The core problem addressed is the lack of a formal framework to express and solve satisfiability constraints involving dates and calendar periods symbolically.

Methodology

The paper introduces DateSAT, a framework that extends quantifier-free linear integer arithmetic (QF-LIA) with two new sorts: Date and Period.

Formalization

Semantics: Dates are defined as triples $(y, m, d)$ $(y, m, d)$ following Gregorian calendar rules. Periods are triples $(n_y, n_m, n_d)$ $(n_{y}, n_{m}, n_{d})$ . The framework adopts a specific semantics for date-period addition (consistent with libraries like Java's java.time and Python's dateutil):
1. Year/Month Addition: Performed first, with overflow handling that rounds down invalid dates (e.g., Jan 31 + 1 month $\to$ Feb 28/29).
2. Day Addition: Performed second, allowing overflows into subsequent months.
  This semantics ensures that adding a period to a valid date always results in a valid date (Theorem 1).
Input Language: The language supports free date variables, date/period arithmetic, comparisons, and component extraction (year, month, day). The logic is proven decidable via reduction to QF-LIA.

Solving Strategies

The authors propose five encoding strategies to map DateSAT constraints to SMT formulas over integers, implemented using the Z3 solver. These strategies trade off between logical depth (nesting of if-then-else blocks) and arithmetic complexity (number of integer operations):

Naive Encoding: Represents dates as $(y, m, d)$ tuples. Date-period arithmetic is unrolled step-by-step, leading to $O(|n_d|)$ logical depth due to nested ITEs for day overflows.
Epoch-based Encoding: Represents dates as a single integer $\Delta$ (days since a fixed epoch). The authors select March 1, 2000 as the epoch to simplify leap-year cycles (1461-day cycles). Day addition becomes $O(1)$ , but year/month arithmetic requires converting $\Delta$ back to $(y, m, d)$ , introducing complex division/modulo constraints.
Hybrid Encoding: Maintains both $(y, m, d)$ and $\Delta$ representations for each date. It uses lazy consistency flags to switch between representations only when necessary (e.g., using $\Delta$ for day-only operations and $(y, m, d)$ for month arithmetic).
Alpha-Beta Encoding: Represents a date as a pair $(\alpha, \beta)$ , where $\alpha$ is the number of months since the epoch and $\beta$ is the day offset within that month. This avoids deep nesting by using modular arithmetic to determine month lengths.
Alpha-Beta-Table Encoding: An optimization of the Alpha-Beta strategy for bounded instances (1900–2100). It utilizes pre-computed lookup tables (48-month cycles) for days-in-month and days-before-month, replacing complex arithmetic with array lookups and modulo operations.

Correctness Verification

The correctness of the Epoch-based, Hybrid, and Alpha-Beta encodings relative to the Naive baseline was formally verified using the Verus proof assistant. The proofs establish that these encodings are equisatisfiable with the Naive encoding for well-formed constraints.

Benchmark and Evaluation

The authors curated DateSATBench, a dataset of 450 constraints from three sources:

LLM-Synthesized (100): Focused on semantic edge cases (e.g., leap years, month boundaries).
Grammar-Sampled (150): Randomly generated to stress-test solver performance on hard/unsatisfiable cases.
Legally Grounded (200): Derived from U.S. Internal Revenue Code statutes (e.g., Section 338(g) election deadlines).

Results:

Performance: On the legal dataset, the Alpha-Beta-Table strategy achieved the best performance, solving 98.45% of constraints with a median time of 0.13 seconds.
Speedup: Compared to the Naive baseline, Alpha-Beta-Table provided a median speedup of 2.41× across the entire benchmark suite (430 solvable constraints).
Efficiency: The Hybrid strategy showed significant improvements on grammar-sampled constraints (median time 4.69s vs. 28.07s for Naive), while the Epoch-based strategy excelled in simple LLM-synthesized cases.
Scalability: As constraints became more complex, the choice of encoding strategy became increasingly critical, with the Alpha-Beta-Table strategy maintaining robustness where others timed out.

Key Contributions

Formalization: A rigorous definition of date and period constraint satisfiability, including semantics for arithmetic and comparison.
Strategies: Five distinct encoding strategies for reducing date logic to integer arithmetic, balancing logical depth and arithmetic complexity.
Implementation: An open-source Python implementation using Z3, available at cmu-pasta/DateSAT.
Benchmark: The DateSATBench suite (450 constraints) for evaluating date reasoning tools.
Evaluation: An empirical study demonstrating that specialized encodings significantly outperform naive approaches, particularly for complex legal and synthetic constraints.

Significance and Claims

The paper claims to present the first framework for expressing and solving satisfiability constraints involving dates and calendar periods. Its significance lies in:

Bridging the Gap: Addressing the lack of tool support for formal reasoning about date logic, a known source of software bugs (e.g., patent expiration errors, cloud outages).
Enabling Verification: Providing a mechanism to verify equivalence in code refactoring (e.g., replacing library calls with custom logic) and validating legal compliance without relying on error-prone LLMs or exhaustive concrete testing.
Foundation for Future Work: Offering a benchmark and solver that can be integrated into program verification tools and Agentic AI systems requiring accurate temporal reasoning.

The authors remain modest, noting that while their current implementation uses Z3 as a backend, future work could involve integrating date logic directly into SMT-LIB as a new theory or exploring bitvector encodings for bounded instances. They emphasize that their work is a foundational step toward principled reasoning about temporal computations.