Seonglae ChoTraditional leap year determination is based on
y%4, y%100, y%400 checks, but this can be reduced to just three CPU instructions (mul, and, cmp) using bit operations and constant multiplication. Specifically,using the Z3 SMT solver to find three magic numbers
f=1073750999, m=3221352463, t=126976This formula alone enables accurate leap year determination within the range 0 ≤ y ≤ 102,499. A 64-bit version can be derived using similar methods to find constants that enable accurate determination for approximately 5.9×10⁹ years, and benchmarks with random inputs show a performance improvement of about 3.8 times compared to traditional implementations.