DateSAT: A Framework for Solving Date and Period Constraints
For developers and verification tool users, DateSAT addresses the lack of native date support in program analysis, reducing errors in calendrical logic.
DateSAT introduces the first framework for expressing and solving satisfiability constraints involving dates and calendar periods, formalizing date and period arithmetic and providing five solving strategies via SMT reduction. Evaluated on 450 constraints, it enables symbolic reasoning about calendrical operations.
Dates and calendar periods (i.e., days, months, years) appear frequently in tasks involving analysis of software, data, and documents. Prior research has shown that computer logic involving dates and calendrical calculations is error-prone due to tricky rules (e.g., irregularly sized months), ambiguities (e.g., scheduling one month from "Jan 31st"), and edge cases (e.g., leap years). However, existing program analysis and verification tools do not provide native support for dates, making it hard to reason about operations involving calendrical arithmetic symbolically. This paper presents DateSAT, the first framework for expressing and solving satisfiability constraints involving dates and calendar periods. The paper first formalizes an input language and the semantics of date and period arithmetic. The paper then presents five separate strategies for solving DateSAT constraints based on reductions to SMT formulas involving integers, which we have implemented using Z3 as a backend. We curate a dataset of 450 DateSAT constraints synthesized using LLM prompting, grammar-based sampling, and mining legal documents, and then present an empirical evaluation of DateSAT solver performance.