Two runs on the same design can differ in cost by orders of magnitude while proving the same thing, and the reason is representation, not logic. One engine stores state sets as decision diagrams whose size depends on variable order; another unrolls steps into clauses whose count grows with depth. Knowing both explains why a proof stalls and which reduction to reach for.
A decision diagram (a BDD) stores a Boolean function as a graph of if-then-else nodes, one level per variable, with identical subgraphs shared and decisions that do not matter skipped. Its size depends on the variable order. For (x1 and x2) or (x3 and x4) or (x5 and x6), keeping each pair adjacent gives 6 nodes, while interleaving the pairs (x1, x3, x5, then x2, x4, x6) gives 14: the diagram must remember which pairs have half their inputs set. With four pairs the counts are 8 grouped and 30 interleaved, and the gap keeps widening. Same function, same engine, several times the memory: order is a first-class cost driver, and reordering heuristics exist precisely because of it. Not every function is sensitive: a six-input parity needs 11 nodes under any order.
A solver-based engine takes a different route. It copies the combinational logic once per cycle, ties the copies together through the registers, and asks for an assignment that breaks a property. A SAT solver works on clauses over single bits; an SMT solver keeps the same unrolling but states constraints on whole vectors (adders, comparators, multiplexers), so there are fewer and wider constraints and the same one-copy-per-cycle structure. As SAT arithmetic, each two-input gate costs about 3 clauses, so 50,000 gates and 2,000 state bits give 3 x 50,000 + 2,000 = 152,000 clauses per step, 4.56 million at depth 30 and 45.6 million at depth 300. This is illustrative arithmetic about the method, not a measurement of any product, and where memory ends a real run depends on the tool and the machine.
The first script counts the nodes of the reduced diagram exactly: for each variable level it collects the distinct sub-functions that really depend on that variable. It asserts 6 grouped and 14 interleaved for the pair function, 8 and 30 for four pairs, and, as a failing partner, that parity is not order-sensitive: asserting that it is gets caught. The second script wraps the clause arithmetic in a checker; a model that forgets the register-link equalities fails the same checker.
from itertools import product
def bdd_nodes(f, n, order):
"""Internal nodes of the reduced ordered diagram of f under a variable order."""
nodes = set()
for k in range(n):
for prefix in product((0, 1), repeat=k):
fixed = dict(zip(order[:k], prefix))
rest = order[k:]
table = []
for vals in product((0, 1), repeat=len(rest)):
a = dict(fixed)
a.update(zip(rest, vals))
table.append(f(a))
half = len(table) // 2
lo, hi = tuple(table[:half]), tuple(table[half:])
if lo != hi: # this sub-function really depends on order[k]
nodes.add((k, tuple(table)))
return len(nodes)
def pair_or(npairs):
return lambda a: int(any(a[2 * i] and a[2 * i + 1] for i in range(npairs)))
def parity(a):
return sum(a.values()) % 2
def order_sensitive(f, n, o1, o2):
return bdd_nodes(f, n, o1) != bdd_nodes(f, n, o2)
grouped = [0, 1, 2, 3, 4, 5]
interleaved = [0, 2, 4, 1, 3, 5]
assert bdd_nodes(pair_or(3), 6, grouped) == 6
assert bdd_nodes(pair_or(3), 6, interleaved) == 14
g4 = list(range(8))
i4 = [0, 2, 4, 6, 1, 3, 5, 7]
assert bdd_nodes(pair_or(4), 8, g4) == 8
assert bdd_nodes(pair_or(4), 8, i4) == 30
assert order_sensitive(pair_or(3), 6, grouped, interleaved)
# injected data: parity is order-insensitive, so claiming otherwise must be caught
assert bdd_nodes(parity, 6, grouped) == 11
caught = False
try:
assert order_sensitive(parity, 6, grouped, interleaved)
except AssertionError:
caught = True
assert caught, "sensitivity check accepted an order-insensitive function"
print("PASS: pair function 6 nodes grouped, 14 interleaved; parity 11 in any order")def clauses(gates, flops, depth, link_flops=True):
per_step = 3 * gates + (flops if link_flops else 0)
return per_step * depth
def check_projection(model):
assert model(50000, 2000, 1) == 152000
assert model(50000, 2000, 30) == 4560000
assert model(50000, 2000, 300) == 45600000
check_projection(clauses)
# injected model: forgets the register-link equalities
def forgetful(gates, flops, depth):
return clauses(gates, flops, depth, link_flops=False)
caught = False
try:
check_projection(forgetful)
except AssertionError:
caught = True
assert caught, "projection check accepted a model without register links"
print("PASS: 152000 clauses per step, 4.56 million at depth 30, 45.6 million at depth 300; miscount caught")Cost is blamed on representation or search, never on the property being true.
Any claim that one order or encoding is better comes with two counted numbers, not adjectives.
Clause projections are labelled illustrative unless they were read from a run.
Recheck a stalled symbolic run by asking for the state-bit count in the cone of the property first: a jump from hundreds to thousands of bits points at the cone, not the engine. For solver-based runs compare the depth against the clause projection above; if the run is far slower than the projection suggests, the difficulty is search order inside the solver, and splitting or strengthening helps more than waiting.
That representation dominates: try reordering or restructuring before concluding the property is hard. The logic is identical; only the storage changed.