Logic

The order of the questions

Decide a Boolean function by asking about its variables one at a time, and share every state that behaves alike. For a₁b₁ + a₂b₂ + … the result has 2n + 2 nodes if partners are asked together and 2ⁿ⁺¹ if they are apart. All 40,320 orders of eight variables give anything from 10 to 32 nodes, while multiplication's middle bit grows fast in the best order of all.
14 min read 5 figures Decided by exhaustionSmall cases lie

Worth reading first: How many gates a truth table needs · The formula that cannot share.

A truth table has a row for every input, which makes it exact and enormous: a function of forty variables has about a trillion rows. A formula can be vastly shorter, but the formula that cannot share showed its limits, and whether two formulas mean the same is a hard question. In the 1980s, when circuits had grown too large to compare by any existing method, Randal Bryant took a structure that had been around since the 1950s, added two simple rules, and produced something that seemed to have all the advantages at once. It is a picture of a function, and two functions are equal exactly when their pictures are the same.

There is one catch, and this essay is about that catch. The picture depends on the order in which the variables are asked about, and the size of the picture can change from a few dozen nodes to more than a computer can hold, with nothing changing in the function at all. The order of the questions matters more than almost anything else one can choose, and finding the best order is itself intractable.

One function, two orders. The function a₁b₁ + a₂b₂ + a₃b₃ as a reduced decision diagram: 8 nodes with partners together, 16 nodes with them apart.
Fig. 1 The function a1b1+a2b2+a3b3a_1 b_1 + a_2 b_2 + a_3 b_3 as two reduced decision diagrams: the same function, in 8 nodes when partners are asked together and in 16 when they are apart.

Asking one question at a time

Start from a decision tree. Ask about x1x_1, then along each branch ask about x2x_2, and so on, with the leaves holding the answer. That is simply a truth table drawn as a tree, with 2n2^n leaves. Two rules shrink it. Share: if two nodes at any point would behave identically on all remaining inputs, keep one and redirect everything to it. Skip: if a node’s two outgoing branches lead to the same place, the question is irrelevant, so remove the node. Apply these until neither applies.

C. Y. Lee described such diagrams in 1959, and Sheldon Akers developed them in 1978. Bryant’s contribution, in 1986, was to insist on one fixed order of the variables along every path and to apply the rules fully, and then to observe the consequence. For a fixed order, every function has exactly one reduced diagram. So equality of functions is a matter of comparing two pictures. Whether a function is satisfiable is whether the box marked 1 is present. The number of satisfying inputs can be counted by a single pass from bottom to top. Two diagrams can be combined by any logical operation, in time about the product of their sizes. It is hard to overstate how convenient that is, since each of these tasks on a formula is as hard as anything in the theory of satisfiability.

A diagram’s nodes have a simple meaning, and it explains everything to come. When the first few variables have been asked about, what remains is some function of the others. A node at a given level is one distinct such remainder: one thing the computation might still need to remember. So the width of a diagram at a level is how much memory about the past it must carry, and this picture is what any reasoning about size turns on.

That should sound familiar. A diagram that reads its input in order and keeps only what the future can distinguish is a finite automaton with its alphabet read one letter at a time, and sharing equivalent remainders is the step that minimises one. The classification of remainders is the idea behind what a formula of monadic logic can say about a word, and it gives the same kind of lower bound: count the things that must be told apart. Renaming and negating variables, which truth tables up to renaming treats as making no difference at all, does make a difference here, and renaming variables is exactly what changes the size. A monotone function, the kind that only goes up, gets no special treatment either, with some of them small and most of them large.

Partners together or apart

Take a1b1+a2b2+⋯+anbna_1 b_1 + a_2 b_2 + \cdots + a_n b_n. Ask the variables with partners side by side, a1,b1,a2,b2,…a_1, b_1, a_2, b_2, \ldots. After reading each pair, the only thing to remember is whether a pair has already been true, and if it has, the answer is already known. So the diagram is a thin chain, of 2n+22n + 2 nodes. Now ask all of the aa’s first. By the time they have all been read, the function depends on which of them were true, since each subset leaves a different set of bb’s that might finish the job. That is 2n2^n remainders, and they are all different. The diagram has to hold every one.

Linear in one order and exponential in another. Reduced diagram sizes for a₁b₁ + … + aₙbₙ: partners together 4, 6, 8, 10, 12, 14, 16, 18; apart 4, 8, 16, 32, 64, 128, 256, 512.
Fig. 2 Sizes of both orders, built from truth tables up to sixteen variables, on a logarithmic scale: one grows by two for each new pair, and the other doubles.

Both formulas were checked by direct construction, up to eight pairs: 18 nodes against 512. With 40 pairs, one order would take 82 nodes and the other more than two trillion. Nothing about the function has changed, nor has its logic. The difference lies entirely in what must be remembered from one question to the next, and that is a fact about the order, not the function. It is the same phenomenon as bracketing a chain of products, or eliminating variables in the right order, where the arrangement decides everything. Here, in contrast with elimination, the bad order is not merely slower. It is a different and much larger object, and it has to fit in memory.

Every order, at eight variables

For a small function, all orders can be tried. With eight variables there are 40,320.

Every order of eight variables. All 40320 orders of the eight variables of a₁b₁ + … + a₄b₄: best 10 in 384 orders, worst 32 in 9216, mean 21.657.
Fig. 3 All 40,320 orders of the eight variables of a1b1+⋯+a4b4a_1 b_1 + \cdots + a_4 b_4 by the size of the diagram: best 10, worst 32, mean 21.66, with the best orders in the warm bar.

The sizes run from 10 to 32, in even steps, with a mean of 21.66. Only 384 orders reach the best, and it is easy to see why that number is what it is: those are exactly the orders keeping each pair together, 4!4! ways to order the pairs, and 242^4 ways to order within each pair, 24×16=38424 \times 16 = 384. So the census confirms the argument above. No order was found that does equally well in some other way. A random order lands about midway between best and worst, and the worst is reached by 9,216 of the orders. The shape of this histogram warns against a tempting belief. A random order is usually bad, and yet a slightly better order is usually available. Practical programs exploit that, moving one variable at a time up and down the order and keeping the best position, a method called sifting, from Richard Rudell in 1993. It works well, without any guarantee.

Finding the best order exactly

Trying all orders takes n!n! work. But notice what the argument about remainders says. The number of nodes testing variable vv depends only on the set of variables above vv and not on their order. That gives a dynamic programme over subsets, due to Steven Friedman and Kenneth Supowit in 1990: the cheapest way to build the diagram with some set at the top is the cheapest for a smaller set, plus the width of the next variable. It needs about 3n3^n work, and that is exact. The programme here was checked against all 720 orders on a six-variable function and it agreed, and then used up to twelve variables, where trying all 12!12! orders is not an option.

Which functions an order can save. Exact least and greatest node counts over all orders: parity: 9/9, 13/13, 17/17, 21/21, 25/25; majority: 8/8, 14/14, 22/22, 32/32, 44/44; carry out of a sum: 7/9, 10/20, 13/43, 16/90, 19/185; pairs a₁b₁ + …: 6/8, 8/16, 10/32, 12/64, 14/128; middle bit of a product: 8/9, 14/24, 31/71, 63/207, 136/649.
Fig. 4 The smallest and largest diagrams over all orders, found exactly, for five functions from four to twelve variables: nothing changes for parity and majority, and the middle bit of a product stays large in its best order.

The table sorts functions by how much an order can help. Parity takes exactly 2n+12n + 1 nodes in any order, and it is the same for majority, at a larger size: 8, 14, 22, 32 and 44. Both are symmetric, so renaming their variables does not change them, and order cannot matter. The carry out of a sum is at the other extreme. With the two numbers’ digits interleaved, it costs 19 nodes at twelve variables, while with one number first it costs 185. That is because an adder needs only one bit of memory, the carry, as long as the digits arrive together.

The last row is the point of the table. For the middle bit of a product of two numbers, the best order costs 8, 14, 31, 63 and 136 nodes, roughly doubling at each step, as the worst goes 9, 24, 71, 207 and 649. Bryant proved in 1991 that this is a theorem: for every order the middle bit of an nn-bit multiplication takes at least 2n/82^{n/8} nodes, so that the exponential cannot be escaped by cleverness. Adding is easy, and multiplying is not, and this has a concrete meaning in that a diagram-based verifier can check an adder of any size and cannot check a large multiplier. In the 1990s, after a famous flaw in a division circuit cost one chip manufacturer a large sum, this became a practical and expensive limitation, and special-purpose methods for arithmetic circuits have been needed since.

One small technical thing went wrong in this computation and it is instructive. The first version of the programme compared remainders by a multiplicative hash, and it reported that parity took 20 nodes at ten variables where it should take 21. Parity’s truth table is the Thue–Morse sequence, and that sequence is known for defeating such hashes: complementary blocks of it have the same polynomial hash modulo a power of two. The test 2n+12n + 1 caught it, after which the hash was mixed differently. A function has no idea that it is special, and it is worth checking a calculation against a case that is known exactly.

All the functions of four variables

All 65,536 functions of four variables. Least and greatest diagram sizes over all 24 orders: mean 8.2072 and 10.4502; the order changes the size for 64304 functions.
Fig. 5 Every one of the 65,536 functions of four variables with its smallest and largest diagram over all 24 orders.

For four variables, all 65,536 functions can be examined, each in all 24 orders. The best order gives a mean of 8.21 nodes, the worst 10.45. The order matters for 98.1% of functions, by a modest amount, as is natural when there are so few variables: the largest best size is 10. And almost no function of four variables is small in every order.

For many variables, a counting argument of the type from how many gates a truth table needs settles what most functions do. There are 22n2^{2^n} functions, and far fewer small diagrams, so that nearly all functions need about 2n/n2^n/n nodes in any order. So small diagrams are a rare privilege, of the same kind as small circuits. The functions that have them are the ones with short memories: adders, comparators, control logic and the kinds of functions that people design. That is the reason that these diagrams worked. Hardware designers build circuits that have structure and regularity, and those have small diagrams in a good order. Jerry Burch, Edmund Clarke, Kenneth McMillan, David Dill and L. J. Hwang’s 1990 paper on symbolic model checking reported verifying systems with 102010^{20} states using these diagrams, a claim that would have sounded absurd before that time. It is a very large number of states to summarise by a table of a few thousand nodes, and it works only because the set of reachable states has a short memory.

Choosing is hard

Since an order decides everything, an algorithm that could quickly find a good order would be extremely valuable. There is not one, as far as is known. Beate Bollig and Ingo Wegener showed in 1996 that deciding whether a given diagram can be reordered to have at most a given number of nodes is NP-complete. Finding one within any constant factor of the optimum is hard as well, by Detlef Sieling’s result of 2002. So the dynamic programme above is close to the best kind of exact method that can reasonably be hoped for, and it stops being practical well before forty variables.

There is a related point about what a diagram cannot express. Because it reads variables once in a fixed order, a diagram is a very limited form of computation. It is a read-once branching program, and functions such as the middle bit of a product or a certain kind of hidden-weight function, whose answer depends on counting then looking up, are hard for it. Allowing reading a variable more than once, or letting different paths use different orders, gives other families, with other trade-offs: free diagrams are stronger, and they lose the uniqueness that makes the whole thing useful. A SAT solver based on resolution makes a different bargain. It handles many formulas whose diagrams would be astronomically large, and it gives up the canonical form. Since about 2000, solvers have taken over a large share of the work that diagrams did, though diagrams are still in use when a compact, complete representation of a whole set is what is wanted.

What the numbers do not say

The tables are exact for what they cover, and they stop at twelve variables. The doubling of the middle-bit row looks like a clean exponential, and in that range it grows much faster than the proved bound of 2n/82^{n/8}, which corresponds to 26/82^{6/8} for the twelve-variable case and does not tell anything at this size. Nothing about the size of the base can be concluded from five points. The eight-variable histogram is one function, a very simple one. Other functions have quite different shapes, so that the conclusion about random orders is suggestive only. Finally, a real diagram package also supports complement edges and shared structure between many functions, which change these counts by a modest factor, and they were not used.

What was computed and what was quoted

All sizes were built directly from truth tables, level by level, with the node counts including the two terminal boxes. The formulas 2n+22n + 2 and 2n+12^{n+1} were checked up to eight pairs and 2n+12n + 1 for parity up to twelve variables. The census of 40,320 orders and of 65,536 functions in 24 orders are complete. The dynamic programme was checked on a six-variable function against all 720 orders. It compares cofactors with two 32-bit hashes, so a hash collision would be possible in principle, though parity’s exact values and the six-variable check found none after the mixing was improved.

The theorems of Bryant, Friedman and Supowit, Bollig and Wegener, and Sieling are quoted, along with the history and the model-checking figure. The 2n/82^{n/8} bound and the counting statement were not derived here.

Still open: the true cost of the middle bit

What is the exact growth rate of the best diagram for multiplication’s middle bit? Bryant’s lower bound of 2n/82^{n/8} has since been raised considerably by Philipp Woelfel, who also gave the first non-trivial upper bound, and the two exponents still do not meet. The true base is not known, and the numbers in the table are too few to say. Each extra pair of variables doubles the cost of the programme, and the tables cannot be pushed much past twenty variables in any straightforward way.

A broader question is what property of a function decides its diagram’s size. A function’s one-way communication complexity across each cut gives a lower bound on the width, and it is the right notion, since a level of the diagram is exactly the memory a one-way message across that cut has to carry. But no simple measure on a formula has been found to predict how large its best diagram will be. Whether there is a good approximate way of finding a good order, for the structured circuits that actually occur, is the practical form of this question. Sifting, which is a heuristic with no guarantee, remains what is used.

What has to be remembered

A reduced decision diagram’s width at a level is the number of different things that the questions so far can leave to be decided, so its size measures how much memory about the past a function needs in a given order. That is why one order of a function’s variables can take 2n+22n + 2 nodes and another 2n+12^{n+1}, and why a symmetric function does not care, and why multiplication cannot be saved at all.

Asking in a good order is what turned a table with a trillion rows into a picture with a hundred nodes, and it made it possible to check real hardware with more states than could be listed. The cost is that the good order has to be found, and that nobody knows how. It is rare in mathematics to see so plainly that the arrangement of a question can be as important as its content.

Shares its objects with

Essays that name at least two of the same things, and that neither author linked.

Named objects

A dashed tag is an object no other essay names yet.

Boolean functionDynamic programmingExhaustive searchLower boundNP-hardTruth table