Metric Time Without the Clock: Making ASP Scale Again

Calendars are harmless until a computer has to reason about them.

A human can say, “Ram has a dentist appointment in one hour, must pick up his insurance card from home, needs cash from the ATM, and travel takes 15, 20, 30, or 40 minutes depending on the route.” We see a small planning problem. A logic system sees actions, states, deadlines, durations, inertia, and a very annoying question: should every possible minute become a Boolean object?

That question is the center of Implementing Metric Temporal Answer Set Programming, the paper behind today’s Cognaptus note.¹ The paper is not trying to make Answer Set Programming fashionable again. ASP was never exactly streetwear. It is doing something more useful: showing how metric temporal ASP can keep the symbolic strengths of ASP while avoiding the most obvious way to destroy its scalability—representing fine-grained time as a huge pile of grounded Boolean atoms.

The core idea is simple enough to state and difficult enough to formalize:

Do not make the ASP grounder enumerate the clock when a constraint solver can represent the clock directly.

That is the mechanism. Everything else in the paper—Here-and-There logic, metric traces, Tseitin-style translations, meta-encodings, clingcon, clingo[dl], and the dentist example—serves that move.

The real bottleneck is not time; it is grounding time into atoms

Answer Set Programming is attractive for planning because it lets modelers describe rules, defaults, choices, and constraints declaratively. You specify what must hold, what may happen, and what is forbidden; the solver searches for stable models that satisfy the specification.

That works beautifully until quantitative time enters the room.

A normal temporal planning model can say that something holds at step 0, then step 1, then step 2. But metric temporal reasoning needs more than step order. It needs distances between time points. “The next state happens 15 to 16 minutes later” is not the same as “the next state happens one symbolic step later.” In the dentist example, moving from office to home takes 15 minutes; moving from office to dentist takes 30; the goal must be achieved within 60 minutes.

The naive ASP-style route is to encode possible time values as Boolean atoms. An atom like t(k,d) can mean: at trace step k, the actual time is d. Then the grounder must generate rules and constraints over possible k and possible d.

That is where the clock becomes a weapon pointed at the modeler.

If the upper time bound is 60, the Boolean encoding is already carrying many possible time values. If the same problem is measured in half-minutes, seconds, or scaled durations, the logical shape of the problem has not changed much, but the grounded program can grow dramatically. The paper’s accepted misconception is exactly here: metric temporal ASP is not just ordinary ASP with a few more steps. Finer time precision can change the computational object the solver receives.

The paper formalizes this in two target directions:

The important distinction is not aesthetic. In the Boolean route, time precision expands the grounded search space. In the constraint route, the timing function is represented directly as integer variables, with constraints like “the next time point must be at least $M$ and less than $N$ minutes later.”

The paper’s technical contribution is to prove that this move is not merely an implementation trick. It gives complete and correct translations from metric ASP into regular ASP and into ASP with difference constraints, first for a restricted “plain” fragment and then for a more general metric fragment.

Plain metric programs handle transitions; general metric programs handle global temporal questions

The paper divides metric logic programs into two fragments.

The plain fragment is designed for transition rules. It allows metric next operators in a way that is enough to model basic state changes: if Ram moves from office to home, then in the next state—constrained by the travel duration—Ram is at home. This captures the mechanics of actions with durations.

But the plain fragment is not enough for global temporal queries. “Ram eventually reaches the dentist within 60 minutes with both required items” is not just a transition effect. It is a goal condition over a time interval. That requires metric operators such as eventually and always.

So the paper introduces a general fragment that allows broader metric temporal atoms. To make this implementable, arbitrary metric formulas are translated into metric logic programs through a Tseitin-style construction: subformulas get fresh auxiliary atoms, and those atoms are tied back to the original formula through equivalence-like rules.

This sounds like formal plumbing because it is formal plumbing. But it matters. Without this layer, the system could handle timed transitions but not the kind of deadline-oriented questions that business planning systems actually ask.

A useful way to read the two fragments is this:

The general fragment is more expressive, but it introduces auxiliary atoms and witness structures. For “eventually,” the system needs to identify a future state that witnesses truth within the allowed interval. For “always,” it needs to reason about all relevant future states. That is not free, no matter how politely the notation behaves.

The mechanism: replace clock enumeration with difference constraints

The central design move appears when the paper translates timing functions.

A timed trace has symbolic states and a timing function. In the dentist example, the trace might have four planning steps, but the actual times attached to those steps could be 0, 15, 35, and 60. The Boolean translation represents such assignments by selecting atoms from a range:

• t(0,0)
• t(1,15)
• t(2,35)
• t(3,60)

To ensure time increases, the encoding must generate rules over possible values. To ensure the difference between step $k$ and step $k+1$ lies inside an interval, it must compare many possible pairs of time values.

The constraint translation does something cleaner. It uses integer variables:

• t(0)
• t(1)
• t(2)
• t(3)

Then it adds difference constraints. In plain language:

For an interval $[M,N)$, it can enforce:

The paper implements these with ASP systems that support difference constraints, specifically clingcon and clingo[dl]. In implementation terms, the modeler writes a metric ASP-like program; the system reifies the ground program; a meta-encoding interprets temporal operators; and the final timing constraints are passed to the hybrid backend.

This is why the title of the paper could have been “Do Not Ground the Clock,” although admittedly that sounds like advice from a tired airport employee.

The mechanism has three layers:

The ASP solver still handles the qualitative logic: actions, choices, effects, inertia, and goal structure. The constraint machinery handles the metric part: whether the time differences fit the intervals.

That separation is the business-relevant idea.

The proofs matter because optimization without semantics is just a faster mistake

The paper spends much of its space proving completeness and correctness. For a business reader, this can feel remote. It is not.

The point of the proofs is to show that the translated programs preserve the intended metric equilibrium semantics. In plainer terms: when the translation returns a model, that model corresponds to a valid metric temporal model; and when a valid metric temporal model exists, the translation can represent it.

The paper proves this for:

1. plain metric programs translated into ordinary HT / ASP;
2. plain metric programs translated into HT with constraints;
3. general metric programs translated into ordinary HT / ASP;
4. general metric programs translated into HT with constraints.

The appendix supplies the machinery: three-valued semantics, splitting arguments, correspondence between timed traces and interpretations, and proofs that auxiliary atoms behave like the formulas they replace. This is not decorative theory. It is what prevents the implementation from becoming a clever but semantically leaky encoding.

In enterprise planning, semantic leakage is expensive. A workflow optimizer that finds a plan by accidentally changing the meaning of “within one hour” is not an optimizer. It is a lawsuit with a progress bar.

The implementation is deliberately modest, but the architecture is clear

The implementation uses clingo’s reification and meta-encoding framework. The paper shows how a metric logic program for the dentist example can be represented, reified, and interpreted through meta-encodings.

The basic metric program includes facts such as locations and items, rules for movement, rules for picking up items, and inertia-like rules. Metric next operators encode duration-sensitive transitions. The goal condition is represented separately using an eventually operator: Ram must eventually satisfy the goal within the allowed interval.

For plain metric programs, the implementation handles metric next. For general metric programs, the meta-encoding expands to handle next, always, and eventually, using auxiliary atoms for truth and witness relationships.

The implementation should be read as a proof-of-concept architecture rather than a polished production system. The authors say as much: the meta-encoding serves as a blueprint for a more sophisticated future implementation. That matters when interpreting the experiments. The paper is not benchmarking a fully optimized industrial scheduler. It is testing whether the proposed translation changes the scaling behavior in the expected direction.

It does.

The experiments show the grounding cliff, not a universal performance law

The results section uses the dentist example and scales it by multiplying durations and, for the pure clingo Boolean route, the corresponding time bound. This is a sensitivity test on time granularity. It asks: if the same logical planning structure is measured on a larger or finer time scale, does the implementation suffer?

The answer depends sharply on how time is represented.

In the setting without the goal condition, clingo’s Boolean route grows from hundreds of thousands of grounded rules to tens of millions as the duration factor increases. At factor 10, the table reports more than 30 million rules for one fragment and more than 33 million for the other. The solving and grounding times rise accordingly. By contrast, the clingcon and clingo[dl] encodings stay at 1,879 rules for the plain fragment and 2,110 rules for the general fragment in that setting, with reported grounding and solving times essentially flat.

The table below interprets the evidence rather than pretending the experiment is broader than it is:

The second experiment adds the goal condition and uses the general fragment. Here the contrast becomes even more interesting. The difference-constraint approaches still keep the rule count fixed at 2,269 across the scaled duration factors. The pure clingo route grows sharply: at factor 10, the table reports 40,672,813 rules, 284.98 seconds of grounding time, and 5,652.98 seconds of solving time.

The paper also reports time to first model in parentheses. For factor 10, clingo finds the first model in 145 seconds, but total solving time reaches 5,652.98 seconds. The authors interpret this as evidence that much of the remaining time is spent ensuring there are no other models. That is a useful distinction. Finding one feasible plan and proving uniqueness or exhausting alternatives are different computational tasks. Many operational systems care about the first good feasible plan. Some compliance or verification systems care about completeness. Confusing the two is a classic way to oversell a solver demo.

The general fragment also relies more on solving than the plain one because it introduces auxiliary atoms and witness structures. This is exactly the expected cost of saying “eventually within this interval” rather than merely “the next transition takes this long.”

The business lesson is architectural: keep rules symbolic, outsource metric time

The business implication is not “use ASP for everything.” That would be adorable, in the way all universal tool claims are adorable.

The better lesson is architectural. Many real planning and scheduling systems combine two kinds of logic:

1. qualitative rules: what actions are allowed, what states follow, what exceptions matter, what defaults apply;
2. quantitative timing: deadlines, durations, minimum gaps, maximum waits, travel times, service windows.

Trying to collapse both into ordinary Boolean grounding can make time precision artificially expensive. The paper shows a cleaner split: let ASP represent the qualitative decision structure, while difference constraints represent metric time.

This maps naturally to several business domains:

What the paper directly shows is narrower: two semantically justified translation routes, implemented via clingo-style meta-encodings, tested on a small dentist planning example. What Cognaptus infers is broader but bounded: when symbolic planning and metric time interact, system architects should avoid forcing time precision into the Boolean grounding layer unless they have a strong reason.

This is not merely a solver-level optimization. It changes how one designs the representation.

A bad architecture asks: “How many time atoms do we need?”

A better architecture asks: “Which parts of the problem are logical choices, and which parts are numeric relations between time variables?”

That second question is where scalable planning systems usually begin.

The general fragment is more expressive, but witnesses are not free

The paper’s general fragment deserves careful interpretation. It enables global metric operators such as eventually and always. That is essential for deadline-oriented goals. But the encoding must introduce auxiliary atoms that represent whether formulas are true at specific states and whether a future state witnesses an eventually condition.

This is the right tradeoff, but it is still a tradeoff.

In the goal experiment, the difference-constraint systems keep grounding small, but the paper notes that global operators generate more complex solving behavior. For the pure clingo route, adding eventually creates a disjunctive program to find the witness of truth. For the constraint routes, the example remains easy, but the mechanism itself tells us that harder instances may expose backend-specific behavior.

This is why “decouples performance from time granularity” should not be misread as “solves temporal planning.” The result is about one major scaling factor: the granularity or magnitude of metric time. It does not eliminate the combinatorics of planning, action choice, global temporal witnesses, or model enumeration.

Business translation: this architecture can reduce one avoidable source of explosion. It does not repeal computational complexity. Sadly, no paper gets to do that. Not even with Greek letters.

Boundaries: the clock is outsourced, not destroyed

The paper is admirably clear about the limits.

First, the empirical results are indicative. They use a small running example, not a broad benchmark suite across logistics, manufacturing, compliance, and resource-constrained scheduling. The observed independence from time granularity is compelling for the tested mechanism, but it should not be treated as a universal runtime guarantee.

Second, outsourcing time to difference constraints has its own costs. The authors note that clingo[dl] maps difference constraints into graphs whose nodes are time variables and whose weighted edges reflect constraints, leading to quadratic space complexity. clingcon uses a lazy approach that gradually unfolds an ASP encoding of linear constraints; in the worst case, this can approach the space requirements of the Boolean translation.

Third, constraints hidden from the ASP solver cannot directly guide the ASP search. That is a subtle but important limitation. Moving timing into a constraint backend reduces grounding pressure, but it may also remove useful information from the symbolic solver’s search heuristics. Whether that tradeoff helps depends on the instance structure.

Fourth, the discrepancy between the two translations is smaller when the timing function is essentially the identity function—when intervals refer only to state indices rather than fine-grained metric time. In such cases, the Boolean route is less punished by time granularity. The authors also mention that better Boolean encodings, such as order encodings, could improve the non-constraint route.

So the practical rule is not “difference constraints always win.” The practical rule is more precise:

Difference constraints are most valuable when metric time precision would otherwise force ASP to ground many irrelevant clock possibilities.

That is the setting where the paper’s architecture is strongest.

What this means for enterprise AI systems that still need rules

Most current enterprise AI discussion is about language models, retrieval, agents, and orchestration. That is understandable. LLMs are the visible layer. But many operational systems still need exact symbolic reasoning underneath: schedules must satisfy deadlines, workflows must obey rules, and plans must be executable rather than merely plausible.

Metric temporal ASP sits in that less glamorous but highly consequential layer. It is the machinery for problems where “looks reasonable” is not enough. A plan either gets Ram to the dentist within one hour with the required items, or it does not. No amount of fluent explanation changes the travel time.

The paper’s contribution is therefore not only a technical translation. It is a reminder about system decomposition. If a business process has symbolic rules and metric constraints, do not automatically push both into one representation because the modeling language makes it convenient. Convenience at modeling time can become a grounding bill at runtime.

A good enterprise architecture should separate:

• rule semantics from numeric feasibility;
• qualitative choices from metric timing;
• model expressiveness from solver burden;
• finding one feasible plan from proving model completeness.

That separation is exactly what this paper formalizes.

Conclusion: the clock belongs in the right subsystem

The easy misconception is that metric time merely adds more steps to temporal ASP. The paper shows why that is too casual. Time granularity can become a grounding problem, and grounding problems are not solved by optimism, dashboards, or calling the solver “agentic.” There, I saved someone a procurement meeting.

The paper’s strongest contribution is a semantically grounded mechanism: translate metric ASP into either ordinary ASP or ASP with difference constraints, and use the latter to represent timing functions directly as integer variables. The proofs establish that the translation preserves the intended metric equilibrium semantics. The implementation shows that clingo-style meta-encodings can realize the idea. The dentist experiments show the expected scaling contrast: Boolean time grounding grows with the clock; difference-constraint encodings largely do not.

For business readers, the lesson is not to memorize HT, MHT, or the exact syntax of &sum. The lesson is to recognize a design pattern: when planning systems combine symbolic rules with quantitative time, the clock should not be blindly grounded into Boolean atoms. It should be represented where numeric relations belong.

Metric time is not the enemy. Grounding the clock is.

Cognaptus: Automate the Present, Incubate the Future.