Implicit evaluation: querying members whose automata are too big to build#

Every uniformly automatic class answers a first-order query by compiling it to one automaton and then running each member’s advice through it. That is unbeatable when you ask many queries — but it has two failure modes:

the query automaton is expensive to build (you pay it once, then amortise), and
for some members the base automata themselves are infeasible — the advice alphabet is astronomical, so the \(O(|\Sigma|^{\text{arity}})\) transition tables cannot even be written down.

The autstr.implicit layer sidesteps both by never building anything: it evaluates a formula bottom-up on the fly over the base transition functions. Boolean connectives keep composite states and step the base automata; exists is an on-the-fly powerset over the (tiny) element alphabet; not flips acceptance. Because the advice is fixed input, the cost is driven by quantifier alternation, not by alphabet size.

Every class exposes check_implicit (model checking) and evaluate_implicit (the whole satisfying set). This notebook shows what that buys — and what it costs.

A member whose automaton cannot be built#

CutRankGroups(2, d=3) is the bounded-rank-width class-2 groups over the chain ring \(\mathbb{Z}/8\). The advice alphabet is so large that the explicit presentation refuses to build:

from autstr.groups import CutRankGroups

G8 = CutRankGroups(2, d=3)                 # exponent-8 center
adv8 = G8.advice(3, G8.clique_form(3))
try:
    _ = G8.cls                              # attempt to build the automata
except ValueError as e:
    print('building the automaton fails:', e)

building the automaton fails: advice alphabet too large to build the explicit presentation automata: 512 letters, ~2e+07 transition enumerations (cap 2e+07); use check_implicit or simulate instead

# ... yet the group law is still decided, implicitly, straight from the transitions.
g, h = ((5,), (3, 1, 6)), ((2,), (7, 4, 1))
z = G8.multiply(3, G8.clique_form(3), g, h)
print('g * h =', z)
print('M(g, h, z) holds:        ', G8.check_implicit('M(x,y,z)', adv8, x=g, y=h, z=z))
print('g is non-central:        ',
      G8.check_implicit('exists y.(exists z.(M(x,y,z) and (not M(y,x,z))))', adv8, x=g))
print('the member is non-abelian:',
      G8.check_implicit('exists x.(exists y.(exists z.(M(x,y,z) and (not M(y,x,z)))))', adv8))

g * h = ((0,), (2, 5, 7))
M(g, h, z) holds:         True
g is non-central:         True
the member is non-abelian: True

The runtime trade-off#

On a member whose automaton can be built — the field \(\mathbb{F}_2\) version — we can time both paths. The compiled path pays a one-time compile, then each query is a fast DFA run; the implicit path skips the compile but pays a per-query on-the-fly cost that grows with quantifier alternation.

import time, random, itertools

G = CutRankGroups(2); n = 3; form = G.clique_form(n); adv = G.advice(n, form)
elems = [((b,), a) for b in range(G.q) for a in itertools.product(range(G.q), repeat=n)]
rng = random.Random(0)

def per_query_us(fn, args, repeat=100):
    sample = [rng.choice(args) for _ in range(repeat)]
    t = time.perf_counter()
    for a in sample:
        fn(*a)
    return (time.perf_counter() - t) / repeat * 1e6

def compiled_runner(phi, free):
    dfa, variables = G.evaluate(phi)        # compile once
    def run(*vals):
        cols = {'advice': list(adv)}
        cols.update({v: G.encode(val, n) for v, val in zip(free, vals)})
        return dfa.accepts([tuple(cols[v][i] for v in variables) for i in range(len(adv))])
    return run

pairs = [(g, h) for g in elems for h in elems]
singles = [(g,) for g in elems]

for label, phi, free, args in [
        ('1 quantifier   exists z.(M(x,y,z) and M(y,x,z))',
         'exists z.(M(x,y,z) and M(y,x,z))', ['x', 'y'], pairs),
        ('2 quantifiers  exists y z.(M(x,y,z) and not M(y,x,z))',
         'exists y.(exists z.(M(x,y,z) and (not M(y,x,z))))', ['x'], singles)]:
    t = time.perf_counter(); run = compiled_runner(phi, free); compile_ms = (time.perf_counter() - t) * 1e3
    c = per_query_us(run, args)
    imp = per_query_us(lambda *v: G.check_implicit(phi, adv, **dict(zip(free, v))), args)
    print(f'{label}\n    compile {compile_ms:5.0f} ms   '
          f'compiled {c:6.0f} us/query   implicit {imp:6.0f} us/query   '
          f'({imp / c:.0f}x slower)\n')

1 quantifier   exists z.(M(x,y,z) and M(y,x,z))
    compile   108 ms   compiled    141 us/query   implicit    565 us/query   (4x slower)
2 quantifiers  exists y z.(M(x,y,z) and not M(y,x,z))
    compile    84 ms   compiled     23 us/query   implicit    955 us/query   (41x slower)

So the rule of thumb: compile when you will ask many queries (the per-query DFA run is tiny and the compile amortises), and reach for the implicit path when either the compile is disproportionate to how often you will query, or — as with \(\mathbb{Z}/8\) above — the automaton cannot be built at all. The implicit slowdown is one query’s worth of on-the-fly work, and it grows with quantifier alternation.

Satisfying sets without enumeration#

evaluate_implicit returns the whole satisfying set of a formula’s open variables. A single forward pass plus a backward counting DP give the exact solution count without enumerating anything (len), and iteration yields the assignments lazily.

# The unique inverse of g in the (unbuildable) Z/8 member.
inv = G8.evaluate_implicit('M(x,y,u)', adv8, x=g, u=G8.identity(3))
print('number of inverses:', len(inv))            # exactly 1, known without enumerating
y = next(iter(inv))['y']
print('g^{-1} =', y, ' and g * g^{-1} = e:',
      G8.multiply(3, G8.clique_form(3), g, y) == G8.identity(3))

number of inverses: 1
g^{-1} = ((6,), (5, 7, 2))  and g * g^{-1} = e: True

# The centralizer of a field element, cross-checked against brute force.
gf = ((1,), (1, 0, 1))
cent = G.evaluate_implicit('exists z.(M(x,y,z) and M(y,x,z))', adv, x=gf)
brute = [e for e in elems if G.multiply(n, form, gf, e) == G.multiply(n, form, e, gf)]
print('centralizer size (DP count):', len(cent), '  brute force:', len(brute))
print('whole domain size:', len(G.evaluate_implicit('Eq(x,x)', adv)), '=', G.q ** (n + 1))

centralizer size (DP count): 8   brute force: 8
whole domain size: 16 = 16

Fully implicit presentations#

ImplicitClass / ImplicitTreeClass package functional atoms and an element alphabet as a first-class presentation — a uniformly automatic class given purely by transition functions, for members where even writing the presentation down is infeasible. Nothing is ever compiled; it offers only check and evaluate.

from autstr import implicit as im

icls = im.ImplicitClass(G8._implicit_atoms(), list(G8.digits))
w = G8.encode(g, 3)
print('Eq(g, g):        ', icls.check('Eq(x,x)', adv8, x=w))
print('non-abelian:     ',
      icls.check('exists x.(exists y.(exists z.(M(x,y,z) and (not M(y,x,z)))))', adv8))
print('domain has 8^4 = %d elements:' % (8 ** 4),
      len(icls.evaluate('Eq(x,x)', adv8)) == 8 ** 4)

Eq(g, g):         True
non-abelian:      True
domain has 8^4 = 4096 elements: True

The heavy group classes (CutRankGroups, CutRankTreeGroups, CocycleRankWidthGroups) and the graph class RankWidthClass all route check_implicit / evaluate_implicit through their implicit_cls, so the largest members — the whole point of a uniform presentation — stay queryable even when no single automaton for them can be built.

Implicit evaluation: querying members whose automata are too big to build

Contents

Implicit evaluation: querying members whose automata are too big to build#

A member whose automaton cannot be built#

The runtime trade-off#

Satisfying sets without enumeration#

Fully implicit presentations#