In the 2022 AMC 10A competition, Problem #24 introduces a condition on digit strings that connects directly to the combinatorics of parking functions:

Contest Problem Statement:
"How many strings of length 5 formed from the digits 0, 1, 2, 3, 4 are there such that for each $j \in \{1, 2, 3, 4\}$, at least $j$ of the digits are less than $j$?
(For example, 02214 satisfies this condition because it contains at least 1 digit less than 1, at least 2 digits less than 2, at least 3 digits less than 3, and at least 4 digits less than 4. The string 23404 does not satisfy the condition because it does not contain at least 2 digits less than 2.)"

Analyzing the Four Conditions

Any length-$5$ string formed from $\{0, 1, 2, 3, 4\}$ must satisfy:

1. $j = 1$: At least $1$ digit must be $< 1$. The only digit $< 1$ is $0$, so every valid string must contain at least one $0$.
2. $j = 2$: At least $2$ digits must be $< 2$ (drawn from $\{0, 1\}$).
3. $j = 3$: At least $3$ digits must be $< 3$ (drawn from $\{0, 1, 2\}$).
4. $j = 4$: At least $4$ digits must be $< 4$ (drawn from $\{0, 1, 2, 3\}$).

The total number of unconstrained strings of length $5$ is $5^5 = 3,125$. How many of these $3,125$ satisfy all four inequality conditions?

The Parking Function Connection

If you sort the five digits in non-decreasing order: $$s_1 \le s_2 \le s_3 \le s_4 \le s_5$$ the condition "at least $j$ digits are less than $j$" means: $$s_1 < 1 \implies s_1 = 0, \quad s_2 \le 1, \quad s_3 \le 2, \quad s_4 \le 3, \quad s_5 \le 4$$ In mathematics, any sequence whose non-decreasing sort satisfies $s_i \le i - 1$ is called a parking function! A famous theorem proved by Alan Konheim and Benjamin Weiss (1969) states that the number of parking functions of length $n$ on $\{0, 1, \dots, n-1\}$ is: $$(n + 1)^{n - 1}$$ For $n = 5$ digits: $$(5 + 1)^{5 - 1} = 6^4 = 1,296$$

Declarative Verification in Prolog

In Prolog, we can express the counting condition with a recursive predicate count_lt(List, Limit, Count) that counts how many numbers in a list are strictly below a threshold. Then we filter the search space and verify the result!

Prolog automatically tests and counts the strings meeting these inequality filters, confirming the parking function theorem result of 1,296.