text:
# Boolean Satisfiability with Transitivity ConstraintsSupported, in part, by the Semiconductor Research Corporation under contract 00-DC-684.

## 1 Introduction

Consider the following variant of the Boolean satisfiability problem. We are given a Boolean formula $`F_{\text{sat}}`$ over a set of variables $`𝒱`$. A subset $`𝒱`$ symbolically encodes a binary relation over $`N`$ elements that is reflexive, symmetric, and transitive. Each of these relational variables, $`e_{i,j}`$, where $`1i<jN`$, expresses whether or not the relation holds between elements $`i`$ and $`j`$. Typically, $``$ will be “sparse,” containing much fewer than the $`N(N1)/2`$ possible variables. Note that when $`e_{i,j}`$ for some value of $`i`$ and of $`j`$, this does not imply that the relation does not hold between elements $`i`$ and $`j`$. It simply indicates that $`F_{\text{sat}}`$ does not directly depend on the relation between elements $`i`$ and $`j`$.

A transitivity constraint is a formula of the form

$`e_{[i_1,i_2]}e_{[i_2,i_3]}\mathrm{}e_{[i_{k1},i_k]}`$ $``$ $`e_{[i_1,i_k]}`$ (1)
where $`e_{[i,j]}`$ equals $`e_{i,j}`$ when $`i<j`$ and equals $`e_{j,i}`$ when $`i>j`$. Let $`\mathrm{𝑇𝑟𝑎𝑛𝑠}()`$ denote the set of all transitivity constraints that can be formed from the relational variables. Our task is to find an assignment $`\chi :𝒱\{0,1\}`$ that satisfies $`F_{\text{sat}}`$, as well as every constraint in $`\mathrm{𝑇𝑟𝑎𝑛𝑠}()`$. Goel, et al. \[GSZAS98\] have shown this problem is NP-hard, even when $`F_{\text{sat}}`$ is given as an Ordered Binary Decision Diagram (OBDD) \[Bry86\]. Normally, Boolean satisfiability is trivial given an OBDD representation of a formula.

We are motivated to solve this problem as part of a tool for verifying pipelined microprocessors \[VB99\]. Our tool abstracts the operation of the datapath as a set of uninterpreted functions and uninterpreted predicates operating on symbolic data. We prove that a pipelined processor has behavior matching that of an unpipelined reference model using the symbolic flushing technique developed by Burch and Dill \[BD94\]. The major computational task is to decide the validity of a formula $`F_{\text{ver}}`$ in a logic of equality with uninterpreted functions \[BGV99a, BGV99b\]. Our decision procedure transforms $`F_{\text{ver}}`$ first by replacing all function application terms with terms over a set of domain variables $`\{v_i|1iN\}`$. Similarly, all predicate applications are replaced by formulas over a set of newly-generated propositional variables. The result is a formula $`F_{\text{ver}}^{}`$ containing equations of the form $`v_i=v_j`$, where $`1i<jN`$. Each of these equations is then encoded by introducing a relational variable $`e_{i,j}`$, similar to the method proposed by Goel, et al. \[GSZAS98\]. The result of the translation is a propositional formula $`\mathrm{𝑒𝑛𝑐𝑓}(F_{\text{ver}}^{})`$ expressing the verification condition over both the relational variables and the propositional variables appearing in $`F_{\text{ver}}^{}`$. Let $`F_{\text{sat}}`$ denote $`\neg \mathrm{𝑒𝑛𝑐𝑓}(F_{\text{ver}}^{})`$, the complement of the formula expressing the translated verification condition. To capture the transitivity of equality, e.g., that $`v_i=v_jv_j=v_kv_i=v_k`$, we have transitivity constraints of the form $`e_{[i,j]}e_{[j,k]}e_{[i,k]}`$. Finding a satisfying assignment to $`F_{\text{sat}}`$ that also satisfies the transitivity constraints will give us a counterexample to the original verification condition $`F_{\text{ver}}`$. On the other hand, if we can prove that there are no such assignments, then we have proved that $`F_{\text{ver}}`$ is universally valid.

We consider three methods to generate a Boolean formula $`F_{\text{trans}}`$ that encodes the transitivity constraints. The direct method enumerates the set of chord-free cycles in the undirected graph having an edge $`(i,j)`$ for each relational variable $`e_{i,j}`$. This method avoids introducing additional relational variables but can lead to a formula of exponential size. The dense method uses relational variables $`e_{i,j}`$ for all possible values of $`i`$ and $`j`$ such that $`1i<jN`$. We can then axiomatize transitivity by forming constraints of the form $`e_{[i,j]}e_{[j,k]}e_{[i,k]}`$ for all distinct values of $`i`$, $`j`$, and $`k`$. This will yield a formula that is cubic in $`N`$. The sparse method augments $``$ with additional relational variables to form a set of variables $`^+`$, such that the resulting graph is chordal \[Rose70\]. We then only require transitivity constraints of the form $`e_{[i,j]}e_{[j,k]}e_{[i,k]}`$ such that $`e_{[i,j]},e_{[j,k]},e_{[i,k]}^+`$. The sparse method is guaranteed to generate a smaller formula than the dense method.

To use a conventional Boolean Satisfiability (SAT) procedure to solve our constrained satisfiability problem, we run the checker over a set of clauses encoding both $`F_{\text{sat}}`$ and $`F_{\text{trans}}`$. The latest version of the fgrasp SAT checker \[M99\] was able to complete all of our benchmarks, although the run times increase significantly when transitivity constraints are enforced.

When using Ordered Binary Decision Diagrams to evaluate satisfiability, we could generate OBDD representations of $`F_{\text{sat}}`$ and $`F_{\text{trans}}`$ and use the apply algorithm to compute an OBDD representation of their conjunction. From this OBDD, finding satisfying solutions would be trivial. We show that this approach will not be feasible in general, because the OBDD representation of $`F_{\text{trans}}`$ can be intractable. That is, for some sets of relational variables, the OBDD representation of the transitivity constraint formula $`F_{\text{trans}}`$ will be of exponential size regardless of the variable ordering. The NP-completeness result of Goel, et al. shows that the OBDD representation of $`F_{\text{trans}}`$ may be of exponential size using the ordering previously selected for representing $`F_{\text{sat}}`$ as an OBDD. This leaves open the possibility that there could be some other variable ordering that would yield efficient OBDD representations of both $`F_{\text{sat}}`$ and $`F_{\text{trans}}`$. Our result shows that transitivity constraints can be intrinsically intractable to represent with OBDDs, independent of the structure of $`F_{\text{sat}}`$.

We present experimental results on the complexity of constructing OBDDs for the transitivity constraints that arise in actual microprocessor verification. Our results show that the OBDDs can indeed be quite large. We consider two techniques to avoid constructing the OBDD representation of all transitivity constraints. The first of these, proposed by Goel, et al. \[GSZAS98\], generates implicants (cubes) of $`F_{\text{sat}}`$ and rejects those that violate the transitivity constraints. Although this method suffices for small benchmarks, we find that the number of implicants generated for our larger benchmarks grows unacceptably large. The second method determines which relational variables actually occur in the OBDD representation of $`F_{\text{sat}}`$. We can then apply one of our three techniques for encoding the transitivity constraints in order to generate a Boolean formula for the transitivity constraints over this reduced set of relational variables. The OBDD representation of this formula is generally tractable, even for the larger benchmarks.

## 2 Benchmarks

Our benchmarks \[VB99\] are based on applying our verifier to a set of high-level microprocessor designs. Each is based on the DLX RISC processor described by Hennessy and Patterson \[HP96\]:

is a single-issue, five-stage pipeline capable of fetching up to one new instruction every clock cycle. It implements six instruction types: register-register, register-immediate, load, store, branch, and jump. The pipeline stages are: Fetch, Decode, Execute, Memory, and Write-Back. An interlock causes the instruction following a load to stall one cycle if it requires the loaded result. Branches and jumps are predicted as not-taken, with up to 3 instructions squashed when there is a misprediction. This example is comparable to the DLX example first verified by Burch and Dill \[BD94\].

has a complete first pipeline, capable of executing the six instruction types, and a second pipeline capable of executing arithmetic instructions. Between 0 and 2 new instructions are issued on each cycle, depending on their types and source registers, as well as the types and destination registers of the preceding instructions. This example is comparable to one verified by Burch \[Bur96\].

has two complete pipelines, i.e., each can execute any of the six instruction types. There are four load interlocks—between a load in Execute in either pipeline and an instruction in Decode in either pipeline. On each cycle, between 0 and 2 instructions can be issued.

In all of these examples, the domain variables $`v_i`$, with $`1iN`$, in $`F_{\text{ver}}^{}`$ encode register identifiers. As described in \[BGV99a, BGV99b\], we can encode the symbolic terms representing program data and addresses as distinct values, avoiding the need to have equations among these variables. Equations arise in modeling the read and write operations of the register file, the bypass logic implementing data forwarding, the load interlocks, and the pipeline issue logic.

Our original processor benchmarks can be verified without enforcing any transitivity constraints. The unconstrained formula $`F_{\text{sat}}`$ is unsatisfiable in every case. We are nonetheless motivated to study the problem of constrained satisfiability for two reasons. First, other processor designs might rely on transitivity, e.g., due to more sophisticated issue logic. Second, to aid designers in debugging their pipelines, it is essential that we generate counterexamples that satisfy all transitivity constraints. Otherwise the designer will be unable to determine whether the counterexample represents a true bug or a weakness of our verifier.

To create more challenging benchmarks, we generated variants of the circuits that require enforcing transitivity in the verification. For example, the normal forwarding logic in the Execute stage of 1$`\times `$DLX-C must determine whether to forward the result from the Memory stage instruction as either one or both operand(s) for the Execute stage instruction. It does this by comparing the two source registers ESrc1 and ESrc2 of the instruction in the Execute stage to the destination register MDest of the instruction in the memory stage. In the modified circuit, we changed the bypass condition $`\text{ESrc1}=\text{MDest}`$ to be $`\text{ESrc1}=\text{MDest}(\text{ESrc1}=\text{ESrc2}\text{ESrc2}=\text{MDest})`$. Given transitivity, these two expressions are equivalent. For each pipeline, we introduced four such modifications to the forwarding logic, with different combinations of source and destination registers. These modified circuits are named 1$`\times `$DLX-C-t, 2$`\times `$DLX-CA-t, and 2$`\times `$DLX-CC-t.

To study the problem of counterexample generation for buggy circuits, we generated 105 variants of 2$`\times `$DLX-CC, each containing a small modification to the control logic. Of these, 5 were found to be functionally correct, e.g., because the modification caused the processor to stall unnecessarily, yielding a total of 100 benchmark circuits for counterexample generation.

Table 1 gives some statistics for the benchmarks. The number of domain variables $`N`$ ranges between 13 and 25, while the number of equations ranges between 27 and 143. The verification condition formulas $`F_{\text{ver}}^{}`$ also contain between 42 and 77 propositional variables expressing the operation of the control logic. These variables plus the relational variables comprise the set of variables $`𝒱`$ in the propositional formula $`F_{\text{sat}}`$. The circuits with modifications that require enforcing transitivity yield formulas containing up to 19 additional equations. The final three lines summarize the complexity of the 100 buggy variants of 2$`\times `$DLX-CC. We apply a number of simplifications during the generation of formula $`F_{\text{sat}}`$, and hence small changes in the circuit can yield significant variations in the formula complexity.

## 3 Graph Formulation

Our definition of $`\mathrm{𝑇𝑟𝑎𝑛𝑠}()`$ (Equation 1) places no restrictions on the length or form of the transitivity constraints, and hence there can be an infinite number. We show that we can construct a graph representation of the relational variables and identify a reduced set of transitivity constraints that, when satisfied, guarantees that all possible transitivity constraints are satisfied. By introducing more relational variables, we can alter this graph structure, further reducing the number of transitivity constraints that must be considered.

For variable set $``$, define the undirected graph $`G()`$ as containing a vertex $`i`$ for $`1iN`$, and an edge $`(i,j)`$ for each variable $`e_{i,j}`$. For an assignment $`\chi `$ of Boolean values to the relational variables, define the labeled graph $`G(,\chi )`$ to be the graph $`G()`$ with each edge $`(i,j)`$ labeled as a 1-edge when $`\chi (e_{i,j})=1`$, and as a 0-edge when $`\chi (e_{i,j})=0`$.

A path is a sequence of vertices $`[i_1,i_2,\mathrm{},i_k]`$ having edges between successive elements. That is, each element $`i_p`$ of the sequence ($`1pk`$) denotes a vertex: $`1i_pN`$, while each successive pair of elements $`i_p`$ and $`i_{p+1}`$ ($`1p<k`$) forms an edge $`(i_p,i_{p+1})`$ We consider each edge $`(i_p,i_{p+1})`$ for $`1p<k`$ to also be part of the path. A cycle is a path of the form $`[i_1,i_2,\mathrm{},i_k,i_1]`$.

###### Proposition 1

An assignment $`\chi `$ to the variables in $``$ violates transitivity if and only if some cycle in $`G(,\chi )`$ contains exactly one 0-edge.

Proof: If. Suppose there is such a cycle. Letting $`i_1`$ be the vertex at one end of the 0-edge, we can trace around the cycle, giving a sequence of vertices $`[i_1,i_2,\mathrm{},i_k]`$, where $`i_k`$ is the vertex at the other end of the 0-edge. The assignment has $`\chi (e_{[i_j,i_{j+1}]})=1`$ for $`1j<k`$, and $`\chi (e_{[i_1,i_k]}=0)`$, and hence it violates Equation 1.

Only If. Suppose the assignment violates a transitivity constraint given by Equation 1. Then, we construct a cycle $`[i_1,i_2,\mathrm{},i_k,i_1]`$ of vertices such that only edge $`(i_k,i_1)`$ is a 0-edge.  $`\mathrm{}`$

A path $`[i_1,i_2,\mathrm{},i_k]`$ is said to be acyclic when $`i_pi_q`$ for all $`1p<qk`$. A cycle $`[i_1,i_2,\mathrm{},i_k,i_1]`$ is said to be simple when its prefix $`[i_1,i_2,\mathrm{},i_k]`$ is acyclic.

###### Proposition 2

An assignment $`\chi `$ to the variables in $``$ violates transitivity if and only if some simple cycle in $`G(,\chi )`$ contains exactly one 0-edge.

Proof: The “if” portion of this proof is covered by Proposition 1. The “only if” portion is proved by induction on the number of variables in the antecedent of the transitivity constraint (Equation 1.) That is, assume a transitivity constraint containing $`k`$ variables in the antecedent is violated and that all other violated constraints have at least $`k`$ variables in their antecedents. If there are no values $`p`$ and $`q`$ such that $`1p<qk`$ and $`i_p=i_q`$, then the cycle $`[i_1,i_2,\mathrm{}i_k,i_1]`$ is simple. If such values $`p`$ and $`q`$ exist, then we can form a transitivity constraint:

$`e_{[i_1,i_2]}\mathrm{}e_{[i_{p1},i_p]}e_{[i_q,i_{q+1}]}\mathrm{}e_{[i_{k1},i_k]}`$ $``$ $`e_{[i_1,i_k]}`$
This transitivity constraint contains fewer than $`k`$ variables in the antecedent, but it is also violated. This contradicts our assumption that there is no violated transitivity constraint with fewer than $`k`$ variables in the antecedent.  $`\mathrm{}`$

Define a chord of a simple cycle to be an edge that connects two vertices that are not adjacent in the cycle. More precisely, for a simple cycle $`[i_1,i_2,\mathrm{},i_k,i_1]`$, a chord is an edge $`(i_p,i_q)`$ in $`G()`$ such that $`1p<qk`$, with $`p+1<q`$, and either $`p1`$ or $`qk`$. A cycle is said to be chord-free if it is simple and has no chords.

###### Proposition 3

An assignment $`\chi `$ to the variables in $``$ violates transitivity if and only if some chord-free cycle in $`G(,\chi )`$ contains exactly one 0-edge.

Proof: The “if” portion of this proof is covered by Proposition 1. The “only if” portion is proved by induction on the number of variables in the antecedent of the transitivity constraint (Equation 1.) Assume a transitivity constraint with $`k`$ variables is violated, and that no transitivity constraint with fewer variables in the antecedent is violated. If there are no values of $`p`$ and $`q`$ such that there is a variable $`e_{[i_p,i_q]}`$ with $`p+1<q`$ and either $`p1`$ or $`qk`$, then the corresponding cycle is chord-free. If such values of $`p`$ and $`q`$ exist, then consider the two cases illustrated in Figure 1, where 0-edges are shown as dashed lines, 1-edges are shown as solid lines, and the wavy lines represent sequences of 1-edges. Case 1: Edge $`(i_p,i_q)`$ is a 0-edge (shown on the left). Then the transitivity constraint:

$`e_{[i_p,i_{p+1}]}\mathrm{}e_{[i_{q1},i_q]}`$ $``$ $`e_{[i_p,i_q]}`$
is violated and has fewer than $`k`$ variables in its antecedent. Case 2: Edge $`(i_p,i_q)`$ is a 1-edge (shown on the right). Then the transitivity constraint:

$`e_{[i_1,i_2]}\mathrm{}e_{[i_{p1},i_p]}e_{[i_p,i_q]}e_{[i_q,i_{q+1}]}\mathrm{}e_{[i_{k1},i_k]}`$ $``$ $`e_{[i_1,i_k]}`$
is violated and has fewer than $`k`$ variables. Both cases contradict our assumption that there is no violated transitivity constraint with fewer than $`k`$ variables in the antecedent.  $`\mathrm{}`$

Each length $`k`$ cycle $`[i_1,i_2,\mathrm{},i_k,i_1]`$ yields $`k`$ constraints, given by the following clauses. Each clause is derived by expressing Equation 1 as a disjunction.

$$\begin{array}{c}\neg e_{[i_1,i_2]}\mathrm{}\neg e_{[i_{k1},i_k]}e_{[i_k,i_1]}\hfill \\ \neg e_{[i_2,i_3]}\mathrm{}\neg e_{[i_{k1},i_k]}\neg e_{[i_k,i_1]}e_{[i_1,i_2]}\hfill \\ \mathrm{}\hfill \\ \neg e_{[i_k,i_1]}\neg e_{[i_1,i_2]}\mathrm{}\neg e_{[i_{k2},i_{k1}]}e_{[i_{k1},i_k]}\hfill \end{array}$$
(2)
For a set of relational variables $``$, we define $`F_{\text{trans}}()`$ to be the conjunction of all transitivity constraints for all chord-free cycles in the graph $`G()`$.

###### Theorem 1

An assignment to the relational variables $``$ will satisfy all of the transitivity constraints given by Equation 1 if and only if it satisfies $`F_{\text{trans}}()`$.

This theorem follows directly from Proposition 3 and the encoding given by Equation 2.

### 3.1 Enumerating Chord-Free Cycles

To enumerate the chord-free cycles of a graph, we exploit the following properties. An acyclic path $`[i_1,i_2,\mathrm{},i_k]`$ is said to have a chord when there is an edge $`(i_p,i_q)`$ in $`G()`$ such that $`1p<qk`$ with $`p+1<q`$, and either $`p1`$ or $`qk`$. We classify a chord-free path as terminal when $`(i_k,i_1)`$ is in $`G()`$, and as extensible otherwise.

###### Proposition 4

A path $`[i_1,i_2,\mathrm{},i_k]`$ is chord-free and terminal if and only if the cycle $`[i_1,i_2,\mathrm{},i_k,i_1]`$ is chord-free.

This follows by noting that the conditions imposed on a chord-free path are identical to those for a chord-free cycle, except that the latter includes a closing edge $`(i_k,i_1)`$.

A proper prefix of path $`[i_1,i_2,\mathrm{},i_k]`$ is a path $`[i_1,i_2,\mathrm{},i_j]`$ such that $`1j<k`$.

###### Proposition 5

Every proper prefix of a chord-free path is chord-free and extensible.

Clearly, any prefix of a chord-free path is also chord-free. If some prefix $`[i_1,i_2,\mathrm{},i_j]`$ with $`j<k`$ were terminal, then any attempt to add the edge $`(i_j,i_{j+1})`$ would yield either a simple cycle (when $`i_{j+1}=i_1`$), some other cycle (when $`i_{j+1}=i_p`$ for some $`1<p<j`$), or a path having $`(i_1,i_j)`$ as a chord.

Given these properties, we can enumerate the set of all chord-free paths by breadth first expansion. As we enumerate these paths, we also generate $`C`$, the set of all chord-free cycles. Define $`P_k`$ to be the set of all extensible, chord-free paths having $`k`$ vertices, for $`1kN`$.

Initially we have $`P_1=\{[i]|1in\}`$, and $`C=\mathrm{}`$. Given set $`P_k`$, we generate set $`P_{k+1}`$ and add some cycles of length $`k+1`$ to $`C`$. For each path $`[i_1,i_2,\mathrm{},i_k]P_k`$, we consider the path $`[i_1,i_2,\mathrm{},i_k,i_{k+1}]`$ for each edge $`(i_k,i_{k+1})`$ in $`G()`$. When $`i_{k+1}=i_p`$ for some $`1p<k`$, we classify the path as cyclic. When there is an edge $`(i_{k+1},i_p)`$ in $`G()`$ for some $`1<p<k`$, we classify the path as having a chord. When there is an edge $`(i_{k+1},i_1)`$ in $`G()`$, we add the cycle $`[i_1,i_2,\mathrm{},i_k,i_{k+1},i_1]`$ to $`C`$. Otherwise, we add the path to $`P_{k+1}`$.

After generating all of these paths, we can use the set $`C`$ to generate the set of all chord-free cycles. For each terminal, chord-free cycle having $`k`$ vertices, there will be $`2k`$ members of $`C`$—each of the $`k`$ edges of the cycle can serve as the closing edge, and a cycle can traverse the closing edge in either direction. To generate the set of clauses given by Equation 2, we simply need to choose one element of $`C`$ for each closing edge, e.g., by considering only cycles $`[i_1,\mathrm{},i_k,i_1]`$ for which $`i_1<i_k`$.

As Figure 2 indicates, there can be an exponential number of chord-free cycles in a graph. In particular, this figure illustrates a family of graphs with $`3n+1`$ vertices. Consider the cycles passing through the $`n`$ diamond-shaped faces as well as the edge along the bottom. For each diamond-shaped face $`F_i`$, a cycle can pass through either the upper vertex or the lower vertex. Thus there are $`2^n`$ such cycles. In addition, the edges forming the perimeter of each face $`F_i`$ create a chord-free cycle, giving a total of $`2^n+n`$ chord-free cycles.

The columns labeled “Direct” in Table 2 show results for enumerating the chord-free cycles for our benchmarks. For each correct microprocessor, we have two graphs: one for which transitivity constraints played no role in the verification, and one (indicated with a “t” at the end of the name) modified to require enforcing transitivity constraints. We summarize the results for the transitivity constraints in our 100 buggy variants of 2$`\times `$DLX-CC in terms of the minimum, the average, and the maximum of each measurement. We also show results for five synthetic benchmarks consisting of $`n\times n`$ planar meshes $`M_n`$, with $`n`$ ranging from 4 to 8, where the mesh for $`n=6`$ is illustrated in Figure 3. For all of the circuit benchmarks, the number of cycles, although large, appears to be manageable. Moreover, the cycles have at most 4 edges. The synthetic benchmarks, on the other hand, demonstrate the exponential growth predicted as worst case behavior. The number of cycles grows quickly as the meshes grow larger. Furthermore, the cycles can be much longer, causing the number of clauses to grow even more rapidly.

### 3.2 Adding More Relational Variables

Enumerating the transitivity constraints based on the variables in $``$ runs the risk of generating a Boolean formula of exponential size. We can guarantee polynomial growth by considering a larger set of relational variables. In general, let $`^{}`$ be some set of relational variables such that $`^{}`$, and let $`F_{\text{trans}}(^{})`$ be the transitivity constraint formula generated by enumerating the chord-free cycles in the graph $`G(^{})`$.

###### Theorem 2

If $``$ is the set of relational variables in $`F_{\text{sat}}`$ and $`^{}`$, then the formula $`F_{\text{sat}}F_{\text{trans}}()`$ is satisfiable if and only if $`F_{\text{sat}}F_{\text{trans}}(^{})`$ is satisfiable.

We introduce a series of lemmas to prove this theorem. For a propositional formula $`F`$ over a set of variables $`𝒜`$ and an assignment $`\chi :𝒜\{0,1\}`$, define the valuation of $`F`$ under $`\chi `$, denoted $`\left[F\right]_\chi `$, to be the result of evaluating formula $`F`$ according to assignment $`\chi `$. We first prove that we can extend any assignment over a set of relational variables to one over a superset of these variables yielding identical valuations for both transistivity constraint formulas.

###### Lemma 1

For any sets of relational variables $`_1`$ and $`_2`$ such that $`_1_2`$, and for any assignment $`\chi _1:_1\{0,1\}`$, such that $`\left[F_{\text{trans}}(_1)\right]_{\chi _1}=1`$, there is an assignment $`\chi _2:_2\{0,1\}`$ such that $`\left[F_{\text{trans}}(_2)\right]_{\chi _2}=1`$

Proof: We consider the case where $`_2=_1\{e_{i,j}\}`$. The general statement of the proposition then holds by induction on $`|_2||_1|`$.

Define assignment $`\chi _2`$ to be:

$`\chi _2(e)`$ $`=`$ $`\{\begin{array}{cc}\chi _1(e),\hfill & ee_{i,j}\hfill \\ 1,\hfill & \text{Graph }G(_1,\chi )\text{ has a path of 1-edges from node }i\text{ to node }j\text{.}\hfill \\ 0,\hfill & \text{otherwise}\hfill \end{array}`$
We consider two cases:

1. If $`\chi _2(e_{i,j})=0`$, then any cycle in $`G(_2,\chi _2)`$ through $`e_{i,j}`$ must contain a 0-edge other than $`e_{i,j}`$. Hence adding this edge does not introduce any transitivity violations.
2. If $`\chi _2(e_{i,j})=1`$, then there must be some path $`P_1`$ of 1-edges between nodes $`i`$ and $`j`$ in $`G(_1,\chi _1)`$. In order for the introduction of 1-edge $`e_{i,j}`$ to create a transitivity violation, there must also be some path $`P_2`$ between nodes $`i`$ and $`j`$ in $`G(_1,\chi _1)`$ containing exactly one 0-edge. But then we could concatenate paths $`P_1`$ and $`P_2`$ to form a cycle in $`G(_1,\chi _1)`$ containing exactly one 0-edge, implying that $`\left[F_{\text{trans}}(_1)\right]_{\chi _1}=0`$. We conclude therefore that adding 1-edge $`e_{i,j}`$ does not introduce any transitivity violations.

$`\mathrm{}`$

###### Lemma 2

For $`_1_2`$ and for any assignment $`\chi _2:_2\{0,1\}`$, such that $`\left[F_{\text{trans}}(_2)\right]_{\chi _2}=1`$, we also have $`\left[F_{\text{trans}}(_1)\right]_{\chi _2}=1`$

Proof: We note that any cycle in $`G(_1,\chi _2)`$ must be present in $`G(_2,\chi _2)`$ and have the same edge labeling. Thus, if $`G(_2,\chi _2)`$ has no cycle with a single 0-edge, then neither does $`G(_1,\chi _2)`$.  $`\mathrm{}`$

We now return to the proof of Theorem 2.

Proof: Suppose that $`F_{\text{sat}}F_{\text{trans}}()`$ is satisfiable, i.e., there is some assignment $`\chi `$ such that $`\left[F_{\text{sat}}\right]_\chi =\left[F_{\text{trans}}()\right]_\chi =1`$. Then by Lemma 1 we can find an assignment $`\chi ^{}`$ such that $`\left[F_{\text{trans}}(^{})\right]_\chi ^{}=1`$. Furthermore, since the construction of $`\chi ^{}`$ by Lemma 1 preserves the values assigned to all variables in $``$, and these are the only relational variables occurring in $`F_{\text{sat}}`$, we can conclude that $`\left[F_{\text{sat}}\right]_\chi ^{}=1`$. Therefore $`F_{\text{sat}}F_{\text{trans}}(^{})`$ is satisfiable.

Suppose on the other hand that $`F_{\text{sat}}F_{\text{trans}}(^{})`$ is satisfiable, i.e., there is some assignment $`\chi ^{}`$ such that $`\left[F_{\text{sat}}\right]_\chi ^{}=\left[F_{\text{trans}}(^{})\right]_\chi ^{}=1`$. Then by Lemma 2 we also have $`\left[F_{\text{trans}}()\right]_\chi ^{}=1`$, and hence $`F_{\text{sat}}F_{\text{trans}}()`$ is satisfiable.  $`\mathrm{}`$

Our goal then is to add as few relational variables as possible in order to reduce the size of the transitivity formula. We will continue to use our path enumeration algorithm to generate the transitivity formula.

### 3.3 Dense Enumeration

For the dense enumeration method, let $`_N`$ denote the set of variables $`e_{i,j}`$ for all values of $`i`$ and $`j`$ such that $`1i<jN`$. Graph $`G(_N)`$ is a complete, undirected graph. In this graph, any cycle of length greater than three must have a chord. Hence our algorithm will enumerate transitivity constraints of the form $`e_{[i,j]}e_{[j,k]}e_{[i,k]}`$, for all distinct values of $`i`$, $`j`$, and $`k`$. The graph has $`N(N1)`$ edges and $`N(N1)(N2)/6`$ chord-free cycles, yielding a total of $`N(N1)(N2)/2=O(N^3)`$ transitivity constraints.

The columns labeled “Dense” in Table 2 show the complexity of this method for the benchmark circuits. For the smaller graphs 1$`\times `$DLX-C, 1$`\times `$DLX-C-t, $`M_4`$ and $`M_5`$, this method yields more clauses than direct enumeration of the cycles in the original graph. For the larger graphs, however, it yields fewer clauses. The advantage of the dense method is most evident for the mesh graphs, where the cubic complexity is far superior to exponential.

### 3.4 Sparse Enumeration

We can improve on both of these methods by exploiting the sparse structure of $`G()`$. Like the dense method, we want to introduce additional relational variables to give a set of variables $`^+`$ such that the resulting graph $`G(^+)`$ becomes chordal \[Rose70\]. That is, the graph has the property that every cycle of length greater than three has a chord.

Chordal graphs have been studied extensively in the context of sparse Gaussian elimination. In fact, the problem of finding a minimum set of additional variables to add to our set is identical to the problem of finding an elimination ordering for Gaussian elimination that minimizes the amount of fill-in. Although this problem is NP-complete \[Yan81\], there are good heuristic solutions. In particular, our implementation proceeds as a series of elimination steps. On each step, we remove some vertex $`i`$ from the graph. For every pair of distinct, uneliminated vertices $`j`$ and $`k`$ such that the graph contains edges $`(i,j)`$ and $`(i,k)`$, we add an edge $`(j,k)`$ if it does not already exist. The original graph plus all of the added edges then forms a chordal graph. To choose which vertex to eliminate on a given step, our implementation uses the simple heuristic of choosing the vertex with minimum degree. If more than one vertex has minimum degree, we choose one that minimizes the number of new edges added.

The columns in Table 2 labeled “Sparse” show the effect of making the benchmark graphs chordal by this method. Observe that this method gives superior results to either of the other two methods. In our implementation we have therefore used the sparse method to generate all of the transitivity constraint formulas.

## 4 SAT-Based Decision Procedures

Most Boolean satisfiability (SAT) checkers take as input a formula expressed in clausal form. Each clause is a set of literals, where a literal is either a variable or its complement. A clause denotes the disjunction of its literals. The task of the checker is to either find an assignment to the variables that satisfies all of the clauses or to determine that no such assignment exists. We can solve the constrained satisfiability problem using a conventional SAT checker by generating a set of clauses $`C_{\text{trans}}`$ representing $`F_{\text{trans}}(^+)`$ and a set of clauses $`C_{\text{sat}}`$ representing the formula $`F_{\text{sat}}`$. We then run the checker on the combined clause set $`C_{\text{sat}}C_{\text{trans}}`$ to find satisfying solutions to $`F_{\text{sat}}F_{\text{trans}}(^+)`$.

In experimenting with a number of Boolean satisfiability checkers, we have found that fgrasp \[MS99\] has the best overall performance. The most recent version can be directed to periodically restart the search using a randomly-generated variable assignment \[M99\]. This is the first SAT checker we have tested that can complete all of our benchmarks. All of our experiments were conducted on a 336 MHz Sun UltraSPARC II with 1.2GB of primary memory.

As indicated by Table 3, we ran fgrasp on clause sets $`C_{\text{sat}}`$ and $`C_{\text{trans}}C_{\text{sat}}`$, i.e., both without and with transitivity constraints. For benchmarks 1$`\times `$DLX-C, 2$`\times `$DLX-CA, and 2$`\times `$DLX-CC, the formula $`F_{\text{sat}}`$ is unsatisfiable. As can be seen, including transitivity constraints increases the run time significantly. For benchmarks 1$`\times `$DLX-C-t, 2$`\times `$DLX-CA-t, and 2$`\times `$DLX-CC-t, the formula $`F_{\text{sat}}`$ is satisfiable, but only because transitivity is not enforced. When we add the clauses for $`F_{\text{trans}}`$, the formula becomes unsatisfiable. For the buggy circuits, the run times for $`C_{\text{sat}}`$ range from under 1 second to over 36 minutes. The run times for $`C_{\text{trans}}C_{\text{sat}}`$ range from less than one second to over 12 hours. In some cases, adding transitivity constraints actually decreased the CPU time (by as much as a factor of 5), but in most cases the CPU time increased (by as much as a factor of 69). On average (using the geometric mean) adding transitivity constraints increased the CPU time by a factor of 2.3. We therefore conclude that satisfiability checking with transitivity constraints is more difficult than conventional satisfiability checking, but the added complexity is not overwhelming.

## 5 OBDD-Based Decision Procedures

A simple-minded approach to solving satisfiability with transitivity constraints using OBDDs would be to generate separate OBDD representations of $`F_{\text{trans}}`$ and $`F_{\text{sat}}`$. We could then use the Apply operation to generate an OBDD for $`F_{\text{trans}}F_{\text{sat}}`$, and then either find a satisfying assignment or determine that the function is unsatisfiable. We show that for some sets of relational variables $``$, the OBDD representation of $`F_{\text{trans}}()`$ can be too large to represent and manipulate. In our experiments, we use the CUDD OBDD package with dynamic variable reordering by sifting.

### 5.1 Lower Bound on the OBDD Representation of $`F_{\text{trans}}()`$

We prove that for some sets $``$, the OBDD representation of $`F_{\text{trans}}()`$ may be of exponential size for all possible variable orderings. As mentioned earlier, the NP-completeness result proved by Goel, et al. \[GSZAS98\] has implications for the complexity of representing $`F_{\text{trans}}()`$ as an OBDD. They showed that given an OBDD $`G_{\text{sat}}`$ representing formula $`F_{\text{sat}}`$, the task of finding a satisfying assignment of $`F_{\text{sat}}`$ that also satisfies the transitivity constraints in $`\mathrm{𝑇𝑟𝑎𝑛𝑠}()`$ is NP-complete in the size of $`G_{\text{sat}}`$. By this, assuming $`P\mathrm{𝑁𝑃}`$, we can infer that the OBDD representation of $`F_{\text{trans}}()`$ may be of exponential size when using the same variable ordering as is used in $`G_{\text{sat}}`$. Our result extends this lower bound to arbitrary variable orderings and is independent of the $`P`$ vs. $`\mathrm{𝑁𝑃}`$ problem.

Let $`M_n`$ denote a planar mesh consisting of a square array of $`n\times n`$ vertices. For example, Figure 3 shows the graph for $`n=6`$. Being a planar graph, the edges partition the plane into faces. As shown in Figure 3 we label these $`F_{i,j}`$ for $`1i,jn1`$. There are a total of $`(n1)^2`$ such faces. One can see that the set of edges forming the border of each face forms a chord-free cycle of $`M_n`$. As shown in Table 2, many other cycles are also chord-free, e.g., the perimeter of any rectangular region having height and width greater than 1, but we will consider only the cycles corresponding to single faces.

Define $`_{n\times n}`$ to be a set of relational variables corresponding to the edges in $`M_n`$. $`F_{\text{trans}}(_{n\times n})`$ is then an encoding of the transitivity constraints for these variables.

###### Theorem 3

Any OBDD representation of $`F_{\text{trans}}(_{n\times n})`$ must have $`\mathrm{\Omega }(2^{n/4})`$ vertices.

To prove this theorem, consider any ordering of the variables representing the edges in $`M_n`$. Let $`A`$ denote those in the first half of the ordering, and $`B`$ denote those in the second half. We can then classify each face according to the four edges forming its border:

All are in $`A`$.

All are in $`B`$.

Some are in $`A`$, while others are in $`B`$. These are called “split” faces.

Observe that we cannot have a type A face adjacent to a type B face, since their shared edge cannot be in both $`A`$ and $`B`$. Therefore there must be split faces separating any region of type A faces from any region of type B faces.

For example, Figure 4 shows three possible partitionings of the edges of $`M_6`$ and the resulting classification of the faces. If we let $`a`$, $`b`$, and $`c`$ denote the number of faces of each respective type, we see that we always have $`c5=n1`$. In particular, a minimum value for $`c`$ is achieved when the partitioning of the edges corresponds to a partitioning of the graph into a region of type A faces and a region of type B faces, each having nearly equal size, with the split faces forming the boundary between the two regions.

###### Lemma 3

For any partitioning of the edges of mesh graph $`M_n`$ into equally-sized sets $`A`$ and $`B`$, there must be at least $`(n3)/2`$ split faces.

Note that this lower bound is somewhat weak—it seems clear that we must have $`cn1`$. However, this weaker bound will suffice to prove an exponential lower bound on the OBDD size.

Proof: Our proof is an adaptation of a proof by Leighton \[Lei92, Theorem 1.21\] that $`M_n`$ has a bisection bandwidth of at least $`n`$. That is, one would have to remove at least $`n`$ edges to split the graph into two parts of equal size.

Observe that $`M_n`$ has $`n^2`$ vertices and $`2n(n1)`$ edges. These edges are split so that $`n(n1)`$ are in $`A`$ and $`n(n1)`$ are in $`B`$.

Let $`M_n^D`$ denote the planar dual of $`M_n`$. That is, it contains a vertex $`u_{i,j}`$ for each face $`F_{i,j}`$ of $`M_n`$, and edges between pairs of vertices such that the corresponding faces in $`M_n`$ have a common edge. In fact, one can readily see that this graph is isomorphic to $`M_{n1}`$.

Partition the vertices of $`M_n^D`$ into sets $`U_a`$, $`U_b`$, and $`U_c`$ according to the types of their corresponding faces. Let $`a`$, $`b`$, and $`c`$ denote the number of elements in each of these sets. Each face of $`M_n`$ has four bordering edges, and each edge is the border of at most two faces. Thus, as an upper bound on $`a`$, we must have $`4a2n(n1)`$, giving $`an(n1)/2`$, and similarly for $`b`$. In addition, since a face of type A cannot be adjacent in $`M_n`$ to one of type B, no vertex in $`U_a`$ can be adjacent in $`M_n^D`$ to one in $`U_b`$.

Consider the complete, directed, bipartite graph having as edges the set $`(U_a\times U_b)(U_b\times U_a)`$, i.e., a total of $`2ab`$ edges. Given the bounds: $`a+b=(n1)^2c`$, $`an(n1)/2`$, and $`bn(n1)/2`$, the minimum value of $`2ab`$ is achieved when either $`a=n(n1)/2`$ and $`b=(n1)^2(n1)n/2c=(n1)(n2)/2c`$, or vice-versa, giving a lower bound:

$`2ab`$ $``$ $`2[n(n1)/2][(n1)(n2)/2c]`$
$`=`$ $`n(n1)^2(n2)/2cn(n1)`$
We can embed this bipartite graph in $`M_n^D`$ by forming a path from vertex $`u_{i,j}`$ to vertex $`u_{i^{},j^{}}`$, where either $`u_{i,j}U_a`$ and $`u_{i^{},j^{}}U_b`$, or vice-versa. By convention, we will use the path that first follows vertical edges to $`u_{i^{},j}`$ and then follows horizontal edges to $`u_{i^{},j^{}}`$. We must have at least one vertex in $`U_c`$ along each such path, and therefore removing the vertices in $`U_c`$ would cut all $`2ab`$ paths.

For each vertex $`u_{i,j}U_c`$, we can bound the total number of paths passing through it by separately considering paths that enter from the bottom, the top, the left, and the right. For those entering from the bottom, there are at most $`ni1`$ source vertices and $`i(n1)`$ destination vertices, giving at most $`i(ni1)(n1)`$ paths. This quantity is maximized for $`i=(n1)/2`$, giving an upper bound of $`(n1)^3/4`$. A similar argument shows that there are at most $`(n1)^3/4`$ paths entering from the top of any vertex. For the paths entering from the left, there are at most $`(j1)(n1)`$ source vertices and $`(nj)`$ destinations, giving at most $`(j1)(nj)(n1)`$ paths. This quantity is maximized when $`j=(n1)/2`$, giving an upper bound of $`(n1)^3/4`$. This bound also holds for those paths entering from the right. Thus, removing a single vertex would cut at most $`(n1)^3`$ paths.

Combining the lower bound on the number of paths $`2ab`$, the upper bound on the number of paths cut by removing a single vertex, and the fact that we are removing $`c`$ vertices, we have:

$`c(n1)^3`$ $``$ $`n(n1)^2(n2)/2cn(n1)`$
$`c(n1)^3+cn`$ $``$ $`n(n1)(n2)/2`$
$`c(n^2n+1)`$ $``$ $`n(n1)(n2)/2`$
We can rewrite $`n(n1)(n2)`$ as $`(n^2n+1)(n3)+n^22n+3`$. Observing that $`n^22n+3>0`$ for all values of $`n`$, we have:

$`c(n^2n+1)`$ $``$ $`(n^2n+1)(n3)/2+(n^22n+3)/2`$
$``$ $`(n^2n+1)(n3)/2`$
$`c`$ $``$ $`(n3)/2`$
$`\mathrm{}`$

A set of faces is said to be edge independent when no two members of the set share an edge.

###### Lemma 4

For any partitioning of the edges of mesh graph $`M_n`$ into equally-sized sets $`A`$ and $`B`$, there must be an edge-independent set of split faces containing at least $`(n3)/4`$ elements.

Proof: Classify the parity of face $`F_{i,j}`$ as “even” when $`i+j`$ is even, and as “odd” otherwise. Observe that no two faces of the same parity can have a common edge. Divide the set of split faces into two subsets: those with even parity and those with odd. Both of these subsets are edge independent, and one of them must have at least 1/2 of the elements of the set of all split faces.  $`\mathrm{}`$

We can now complete the proof of Theorem 3 Proof: Suppose there is an edge-independent set of $`k`$ split faces. For each split face, choose one edge in $`A`$ and one edge in $`B`$ bordering that face. For each value $`\stackrel{}{y}\{0,1\}^k`$, define assignment $`\alpha _\stackrel{}{y}`$ (respectively, $`\beta _\stackrel{}{y}`$), to the variables representing edges in $`A`$ (resp., $`B`$) as follows. For an edge $`e`$ that is not part of any of the $`k`$ split faces, define $`\alpha _\stackrel{}{y}(e)=0`$ (resp., $`\beta _\stackrel{}{y}(e)=0`$). For an edge $`e`$ that is part of a split face, but it was not one of the ones chosen specially, let $`\alpha _\stackrel{}{y}=1`$ (resp., $`\beta _\stackrel{}{y}(e)=1`$). For an edge $`e`$ that is the chosen variable in face $`i`$, let $`\alpha _\stackrel{}{y}(e)=y_i`$ (resp., $`\beta _\stackrel{}{y}(e)=y_i`$). This will give us an assignment $`\alpha _\stackrel{}{y}\beta _\stackrel{}{y}`$ to all of the variables that evaluates to 1. That is, for each independent, split face $`F_i`$, we will have two 1-edges when $`y_i=0`$ and four 1-edges when $`y_i=1`$. All other cycles in the graph will have at least two 0-edges.

On the other hand, for any $`\stackrel{}{y},\stackrel{}{z}\{0,1\}^k`$ such that $`\stackrel{}{y}\stackrel{}{z}`$ the assignment $`\alpha _\stackrel{}{y}\beta _\stackrel{}{z}`$ will cause an evaluation to 0, because for any face $`i`$ where $`y_iz_i`$, all but one edge will be assigned value 1. Thus, the set of assignments $`\{\alpha _\stackrel{}{y}|\stackrel{}{y}\{0,1\}^k\}`$ forms an OBDD fooling set, as defined in \[Bry91\], implying that the OBDD must have at least $`2^k2^{(n3)/4}=\mathrm{\Omega }(2^{n/4})`$ vertices.  $`\mathrm{}`$

We have seen that adding relational variables can reduce the number of cycles and therefore simplify the transitivity constraint formula. This raises the question of how adding relational variables affects the BDD representation of the transitivity constraints. Unfortunately, the exponential lower bound still holds.

###### Corollary 1

For any set of relational variables $``$ such that $`_{n\times n}`$, any OBDD representation of $`F_{\text{trans}}()`$ must contain $`\mathrm{\Omega }(2^{n/8})`$ vertices.

The extra edges in $``$ introduce complications, because they create cycles containing edges from different faces. As a result, our lower bound is weaker.

Define a set of faces as vertex independent if no two members share a vertex.

###### Lemma 5

For any partitioning of the edges of mesh graph $`M_n`$ into equal-sized sets $`A`$ and $`B`$, there must be a vertex-independent set of split faces containing at least $`(n3)/8`$ elements.

Proof: Partition the set of split faces into four sets: EE, EO, OE, and OO, where face $`F_{i,j}`$ is assigned to a set according to the values of $`i`$ and $`j`$:

1. Both $`i`$ and $`j`$ are even.
2. $`i`$ is even and $`j`$ is odd.
3. $`i`$ is odd and $`j`$ is even.
4. Both $`i`$ and $`j`$ are odd.

Each of these sets is vertex independent. At least one of the sets must contain at least $`1/4`$ of the elements. Since there are at least $`(n3)/2`$ split faces, one of the sets must contain at least $`(n3)/8`$ vertex-independent split faces.  $`\mathrm{}`$

We can now prove Corollary 1.

Proof: For any ordering of the variables in $``$, partition them into two sets $`A`$ and $`B`$ such that those in $`A`$ come before those in $`B`$, and such the number of variables that are in $`_{n\times n}`$ are equally split between $`A`$ and $`B`$. Suppose there is a vertex-independent set of $`k`$ split faces. For each value $`\stackrel{}{y}\{0,1\}^k`$, we define assignments $`\alpha _\stackrel{}{y}`$ to the variables in $`A`$ and $`\beta _\stackrel{}{y}`$ to the variables in $`B`$. These assignments are defined as they are in the proof of Theorem 3 with the addition that each variable $`e_{i,j}`$ in $`_{n\times n}`$ is assigned value 0. Consider the set of assignments $`\alpha _\stackrel{}{y}\beta _\stackrel{}{z}`$ for all values $`\stackrel{}{y},\stackrel{}{z}\{0,1\}^k`$. The only cycles in $`G(,\alpha _\stackrel{}{y}\beta _\stackrel{}{z})`$ that can have less than two 0-edges will be those corresponding to the perimeters of split faces. As in the proof of Theorem 3, the set $`\{\alpha _\stackrel{}{y}|\stackrel{}{y}\{0,1\}^k\}`$ forms an OBDD fooling set, as defined in \[Bry91\], implying that the OBDD must have at least $`2^k2^{(n3)/8}=\mathrm{\Omega }(2^{n/8})`$ vertices.  $`\mathrm{}`$

Our lower bounds are fairly weak, but this is more a reflection of the difficulty of proving lower bounds. We have found in practice that the OBDD representations of the transitivity constraint functions arising from benchmarks tend to be large relative to those encountered during the evaluation of $`F_{\text{sat}}`$. For example, although the OBDD representation of $`F_{\text{trans}}(^+)`$ for benchmark 1$`\times `$DLX-C-t is just 2,692 nodes (a function over 42 variables), we have been unable to construct the OBDD representations of this function for either 2$`\times `$DLX-CA-t (178 variables) or 2$`\times `$DLX-CC-t (193 variables) despite running for over 24 hours.

### 5.2 Enumerating and Eliminating Violations

Goel, et al. \[GSZAS98\] proposed a method that generates implicants (cubes) of the function $`F_{\text{sat}}`$ from its OBDD representation. Each implicant is examined and discarded if it violates a transitivity constraint. In our experiments, we have found this approach works well for the normal, correctly-designed pipelines (i.e., circuits 1$`\times `$DLX-C, 2$`\times `$DLX-CA, and 2$`\times `$DLX-CC) since the formula $`F_{\text{sat}}`$ is unsatisfiable and hence has no implicants. For all 100 of our buggy circuits, the first implicant generated contained no transitivity violation and hence was a valid counterexample.

For circuits that do require enforcing transitivity constraints, we have found this approach impractical. For example, in verifying 1$`\times `$DLX-C-t by this means, we generated 253,216 implicants, requiring a total of 35 seconds of CPU time (vs. 0.2 seconds for 1$`\times `$DLX-C). For benchmarks 2$`\times `$DLX-CA-t and 2$`\times `$DLX-CC-t, our program ran for over 24 hours without having generated all of the implicants. By contrast, circuits 2$`\times `$DLX-CA and 2$`\times `$DLX-CC can be verified in 11 and 29 seconds, respectively. Our implementation could be improved by making sure that we generate only implicants that are irredundant and prime. In general, however, we believe that a verifier that generates individual implicants will not be very robust. The complex control logic for a pipeline can lead to formulas $`F_{\text{sat}}`$ containing very large numbers of implicants, even when transitivity plays only a minor role in the correctness of the design.

### 5.3 Enforcing a Reduced Set of Transitivity Constraints

One advantage of OBDDs over other representations of Boolean functions is that we can readily determine the true support of the function, i.e., the set of variables on which the function depends. This leads to a strategy of computing an OBDD representation of $`F_{\text{sat}}`$ and intersecting its support with $``$ to give a set $`\widehat{}`$ of relational variables that could potentially lead to transitivity violations. We then augment these variables to make the graph chordal, yielding a set of variables $`\widehat{}^+`$ and generate an OBDD representation of $`F_{\text{trans}}(\widehat{}^+)`$. We compute $`F_{\text{sat}}F_{\text{trans}}(\widehat{}^+)`$ and, if it is satisfiable, generate a counterexample.

Table 4 shows the complexity of the graphs generated by this method for our benchmark circuits. Comparing these with the full graphs shown in Table 2, we see that we typically reduce the number of relational vertices (i.e., edges) by a factor of 3 for the benchmarks modified to require transitivity and by an even greater factor for the buggy circuit benchmarks. The resulting graphs are also very sparse. For example, we can see that both the direct and sparse methods of encoding transitivity constraints greatly outperform the dense method.

Table 5 shows the complexity of applying the OBDD-based method to all of our benchmarks. The original circuits 1$`\times `$DLX-C, 2$`\times `$DLX-CA, and 2$`\times `$DLX-CC yielded formulas $`F_{\text{sat}}`$ that were unsatisfiable, and hence no transitivity constraints were required. The 3 modified circuits 1$`\times `$DLX-C-t, 2$`\times `$DLX-CA-t, and 2$`\times `$DLX-CC-t are more interesting. The reduction in the number of relational variables makes it feasible to generate an OBDD representation of the transitivity constraints. Compared to benchmarks 1$`\times `$DLX-C, 2$`\times `$DLX-CA, and 2$`\times `$DLX-CC, we see there is a significant, although tolerable, increase in the computational requirement to verify the modified circuits. This can be attributed to both the more complex control logic and to the need to apply the transitivity constraints.

For the 100 buggy variants of 2$`\times `$DLX-CC, $`F_{\text{sat}}`$ depends on up to 52 relational variables, with an average of 17. This yielded OBDDs for $`F_{\text{trans}}(\widehat{}^+)`$ ranging up to 93,937 nodes, with an average of 1,483. The OBDDs for $`F_{\text{sat}}F_{\text{trans}}(\widehat{}^+)`$ ranged up to 438,870 nodes (average 25,057), showing that adding transitivity constraints does significantly increase the complexity of the OBDD representation. However, this is just one OBDD at the end of a sequence of OBDD operations. In the worst case, imposing transitivity constraints increased the total CPU time by a factor of 2, but on average it only increased by 2%. The memory required to generate $`F_{\text{sat}}`$ ranged from 9.8 to 50.9 MB (average 15.5), but even in the worst case the total memory requirement increased by only 2%.

## 6 Conclusion

By formulating a graphical interpretation of the relational variables, we have shown that we can generate a set of clauses expressing the transitivity constraints that exploits the sparse structure of the relation. Adding relational variables to make the graph chordal eliminates the theoretical possibility of there being an exponential number of clauses and also works well in practice. A conventional SAT checker can then solve constrained satisfiability problems, although the run times increase significantly compared to unconstrained satisfiability. Our best results were obtained using OBDDs. By considering only the relational variables in the true support of $`F_{\text{sat}}`$, we can enforce transitivity constraints with only a small increase in CPU time.


format: text

text:
# Quantum Measurement and Shannon Information, A Reply to M. J. W. Hall

\[

## Abstract

Motivated by Hall’s recent comment in quant-ph/0007116 we point out in some detail the essence of our reasoning why we believe that Shannon’s information is not an adequate choice when defining the information gain in quantum measurements as opposed to classical observations.

\]

In a recent comment , Hall raises some very interesting points with respect to our recently published criticism  of the applicability of Shannon’s measure  of information to quantum measurement. Before answering some of Hall’s criticism directly we would like to recall some of the essential points of our view:

1) We require from an information measure appropriate to a quantum experiment that it firstly describes the information gain of an individual experiment and secondly that the total information gain is described by the sum of a complete set of non-commuting, i.e. complementary, observables.

2) We require that the information gain be directly based on the observed probabilities, (and not, for example, on the precise sequence of individual outcomes observed on which Shannon’s measure of information is based).

3) As the particular choice of the complete set of non-commuting observables is at the whim of the experimentalist, and as the total information content of a quantum system must be independent of the experimentalist’s choice, we require the total information content to be invariant upon that choice.

For the purpose of further discussion we denote the measure of information in the measurement of observable $`\widehat{A}`$ by $`I(\stackrel{}{p})`$ where $`\stackrel{}{p}=p_1,\mathrm{},p_n`$ are probabilities for outcomes to occur. Then the total information content of the quantum system is defined as the sum of individual measures of information over a complete set $`\widehat{A}_1,\mathrm{},\widehat{A}_j,\mathrm{}`$ of mutually complementary observables, i.e. $`I_{total}_jI(\stackrel{}{p}_j)`$ where $`\stackrel{}{p}_j`$ is the probability distribution observed in the measurement of observable $`\widehat{A}_j`$. With the specific measure of information $`I(\stackrel{}{p})`$ (proportional to the sum of the squares of probabilities) that both mathematically and conceptually differs from the Shannon measure the total information of the quantum system is shown to have the property of invariance required in 3) above .

An essential point of our argument is that Shannon’s measure of information is intimately tied to the notion of systems carrying properties prior to and independent of observation. This is certainly the case for classical systems but, in general, this is not true for quantum systems. It is only true for quantum systems in the rare case of measurements performed in a basis where the density matrix of the system is purely diagonal. Be it a pure state, which is measured using an apparatus to whom the state is an eigenstate, or be it a mixed state, in its diagonal representation where the probabilities for the subsystems occur can be viewed as classical probabilities for the measurement results in that diagonal basis.

While Hall seems to agree that Shannon’s reasoning of breaking down a decision tree of various ways cannot be applied to consecutive quantum measurements for non-commuting observables, he suggests that this observation of ours is not relevant in judging whether Shannon’s information is applicable to quantum measurement. We note that at least one of the reasons given to justify the use of Shannon’s information in general is therefore unapplicable, yet we would suggest that we cannot agree with Hall’s point where he criticizes our use of the Fadeev  form of the so-called grouping axiom. In particular he suggests that the grouping axiom which, we agree, directly leads to Shannon’s information can still be used if one considers non-overlapping distributions which are defined such that there exists some measurement which is able to discriminate between them with certainty.

We suggest that this is exactly the case when we observe a density matrix in its eigenbasis where it has no non-diagonal terms, that is, when we can indeed introduce classical probabilities. Yet, clearly, if we consider other observables, where the density matrix is not non-diagonal, we certainly arrive at states which are coherent superposition of the basis states and therefore if we perform the measurement in this new basis the distributions cannot uniquely be defined. It should also be noted that the results observed in one single quantum measurement can always be assumed as emerging from a classical mixture of non-overlapping distributions with weights being equal to the probabilities for the results observed. Yet again, these distributions cannot be defined uniquely for all possible non-commuting measurements . Therefore, we suggest that this argument by Hall actually can be viewed as supporting our general proposition.

In his comment Hall analyzes some geometrical properties of Shannon and von Neumann entropies and he gives a connection between them pointing to the existence of a unique measure of uncertainty for classical and quantum systems with the geometrical properties of a ”volume” . This leads him to the conclusion that the von Neumann entropy is in fact an appropriate quantum generalization of Shannon entropy. While it might be of theoretical importance to request for an adequate measure of information in classical and quantum physics certain well-defined geometrical properties, we suggest to judge the physical significance of a measure of information by its operational properties because after all every information about the system is obtained at only by observation.

Following this requirement we argue that, with the only exception for results of measurement in a basis decomposing the density matrix into a classical mixture when it is equivalent to Shannon’s information and therefore indeed refers to the information gain in an individual measurement experiment, the von Neumann entropy is just a measure of the purity of the given density matrix without any explicit reference to information contained in individual measurements.

Hall argued that this kind of criticism also holds for our proposed total information content because for the measurement in the basis in which the density matrix is diagonal the measure of information $`I(\stackrel{}{p})`$ is equal to the total information $`I_{total}(\widehat{\rho })`$. We emphasize that for a complete set of mutually complementary observables, thus including also those for which the density matrix cannot be decomposed into a classical mixture, and furthermore without knowledge of the basis in which the density matrix is diagonal, we always have $`I_{total}(\widehat{\rho })=_jI(\stackrel{}{p}_j)`$. In contrary there is no such relation for the von Neumann entropy and the set of individual Shannon’s measures associated to mutually complementary measurements. The case of $`I(\stackrel{}{p})=I_{total}(\widehat{\rho })`$ is just an extreme one of maximal knowledge of one observable at the expense of complete ignorance of complementary ones, however the value of the total information remains unchanged also for other choices of a complete set of observables where we have only partial knowledge of them.

In relation to Hall’s argument mentioned above, it might be of interest that besides the discussed case of the measurement in the basis in which the density matrix is diagonal there exists an infinitely large set of individual measurements for all of which the measure of information is indeed equal to the total information content. We explain this on the simple example of a spin-1/2 particle for which we know to have three mutually complementary measurements. These are the measurements of spin along orthogonal directions $`x^1`$, $`x^2`$ and $`x^3`$. From the three von Neumann measurements we may formally constitute one single measurement with 6 outcomes described by a POVM

$`{\displaystyle \frac{1}{3}}{\displaystyle \underset{j}{\overset{3}{}}}|𝐱^j𝐱^j|+|𝐱^j𝐱^j|=\widehat{1}.`$ (1)
This is just the properly normalized sum of three completeness relations. From this one single POVM we obtain 6 probabilities. Inserting them in the expression for our measure of information we get a quantity which is invariant under unitary transformation. We find it intriguing that just from one single POVM experiment we can obtain the total information of the quantum system which comprises in itself all possible mutually complementary classes of information.

Hall also suggests that the von Neumann can be viewed as an operational concept as it is based on probabilities. We remark that the usual procedure to obtain the von Neumann entropy includes performance of the sufficient number of measurements necessary for complete specification of the density matrix, calculation of its elements using a very specific and well-defined prescription from quantum theory that connects probabilities observed in the measurements and complex elements of the density matrix, and finally performing a particular mathematical operation In the formulation of our information content we were lead by an operationally based plausible idea that in quantum mechanics an experimentalist can have only partial knowledge about mutually exclusive measurements in general without any further reference to the structure of the theory. By simple summarizing these partial knowledges we obtain immediately a quantity which turns out to be invariant under unitary transformation in contrast to the procedure mentioned above where one has to use concepts from quantum theory from the beginning.

Finally Hall makes the interesting suggestion of defining our new measure of information not only via complete sets of mutually complementary observables but by an average over all non-degenerate Hermitian observables. This apparently is a nice generalization independent of the question whether or not a complete set of mutually complementary observables exists for Hilbert spaces of any dimension.

We would like to thank Zdenek Hradil for helpful comments and discussions. This work has been supported by the Austrian Science Foundation FWF, Project No. F1506 and the US National Science Foundation NSF Grant No. PHY 97-22614.


text:
# Randomness on the Lattice

## 1 Introduction

A significant part of our understanding of nonperturbative phenomena in QCD, such as chiral symmetry breaking, confinement or the existence of nuclei, results from simulations of the QCD partition function on a Euclidean space-time lattice (see  for reviews). In spite of its numerous successes, this approach has several disadvantages. One of them is the use of Euclidean space-time which requires a highly nontrivial analytical continuation to Minkowski space-time. One of the promising approaches that works directly in a Hamiltonian framework is discrete light-cone QCD , but its results for 4-dimensional nonabelian gauge theories can not yet compete with lattice QCD. A second disadvantage of lattice QCD is that analytical understanding of most lattice data seems beyond reach. Therefore, it is imperative to provide an analytical explanation of lattice observables whenever possible. One such observable is the Euclidean Dirac spectrum. We have proved  our conjecture  that the fluctuations of the smallest Dirac eigenvalues are given by a chiral Random Matrix Theory (chRMT) with the global symmetries of the QCD partition function. In this lecture we give a review of recent lattice simulations that support this assertion. A recent comprehensive review of chiral Random in QCD was given in .

Of course, chRMT cannot provide us with a $`complete`$ description of the QCD Dirac spectrum. What is the domain of validity of chRMT? To answer this question we need to identify three different scales in the Dirac spectrum. The first scale is the smallest nonzero eigenvalue, $`\lambda _{\mathrm{min}}`$. Its average position is given by the mean level spacing, $`\mathrm{\Delta }(\lambda )`$, which is the inverse of the average spectral density near zero, $`\rho (0)`$,

$`\lambda _{\mathrm{min}}\mathrm{\Delta }\lambda ={\displaystyle \frac{1}{\rho (0)}}={\displaystyle \frac{\pi }{\mathrm{\Sigma }V}}.`$ (1)
Because of the axial symmetry the nonzero eigenvalues of the Euclidean Dirac operator $`D`$ appear in pairs $`\pm \lambda _k`$. The average spectral density is then defined by $`\rho (\lambda )=_k\delta (\lambda \lambda _k)`$, and $`\pi \rho (0)/V`$ (with $`V`$ the volume of space-time) is identified as the chiral condensate, $`\mathrm{\Sigma }`$, through the Banks-Casher formula . A second scale in the Dirac spectrum is the mass scale for which the Compton wavelength of the corresponding Goldstone boson is equal to the size of the box. This scale, also known as the Thouless energy, is given by

$`m_c={\displaystyle \frac{F^2}{\mathrm{\Sigma }L^2}},`$ (2)
where $`L`$ is the linear size of the box. A third scale is the typical hadronic mass scale given by $`\mathrm{\Lambda }_{\mathrm{QCD}}`$.

Because QCD has a mass gap, for volumes with $`\mathrm{\Lambda }_{\mathrm{QCD}}L1`$, the QCD partition function in the phase of spontaneous broken chiral symmetry, reduces to that of a gas of Goldstone bosons. For momenta and masses well below $`\mathrm{\Lambda }_{\mathrm{QCD}}`$, this effective chiral partition function can be written down solely on the basis of the global symmetries of QCD. A further simplification arises for $`mm_c`$. In this domain the fluctuations of the constant fields are much larger than the fluctuations of the nonzero momentum modes and kinetic term of the chiral Lagrangian can be ignored in the calculation of the mass dependence of the partition function . This is the domain of validity chiral Random Matrix Theory. A formal proof of this statement  requires the introduction of additional ghost quarks with spectral mass $`z`$ equal to the argument of the resolvent of the Dirac operator. Because $`z`$ is a free parameter, it can always be chosen such that $`zm_c`$, and the Dirac spectrum in this domain is thus given by chiral Random Matrix Theory.

## 2 Chiral Random Matrix Theory

The chiral random matrix partition function with the global symmetries of the QCD partition function is defined by

$`Z_\beta ^\nu (M)={\displaystyle DW\underset{f=1}{\overset{N_f}{}}det\left(\begin{array}{cc}m_f& iW\\ iW^{}& m_f\end{array}\right)e^{\frac{N\beta }{4}\mathrm{\Sigma }\mathrm{Tr}W^{}W}},`$ (5)
where $`W`$ is a $`n\times m`$ matrix with $`\nu =|nm|`$ and $`N=n+m`$. As is the case in QCD, we assume that the equivalent of the topological charge $`\nu `$ does not exceed $`\sqrt{N}`$, so that, to a good approximation, $`n=N/2`$. Then the parameter $`\mathrm{\Sigma }`$ can be identified as the chiral condensate and $`N`$ as the dimensionless volume of space time (Our units are defined such that the density of the modes $`N/V=1`$). The chiral ensembles are classified according to the Dyson index $`\beta `$. The matrix elements of $`W`$ are either real ($`\beta =1`$, chiral Gaussian Orthogonal Ensemble (chGOE)), complex ($`\beta =2`$, chiral Gaussian Unitary Ensemble (chGUE)), or quaternion real ($`\beta =4`$, chiral Gaussian Symplectic Ensemble (chGSE)). For QCD with three or more colors and quarks in the fundamental representation the matrix elements of the Dirac operator are complex and we have $`\beta =2`$. The ensembles with $`\beta =1`$ and $`\beta =4`$ are relevant in the case of two colors or adjoint fermions. For staggered fermions, the value of the Dyson index in these two cases is reversed. The reason for choosing a Gaussian distribution of the matrix elements is its mathematically simplicity. It can be shown that the correlations of the eigenvalues on the scale of the average level spacing do not depend on the details of the probability distribution .

## 3 Lattice Results

We start this section by stressing that only spectral properties on the scale of the average level spacing can be described by Random Matrix Theory. We thus unfold the spectrum by rescaling the eigenvalues according to the macroscopic average level spacing obtained by averaging over many consecutive levels inside a small but finite interval. Below we always discuss the statistical properties of the unfolded eigenvalues, with average spectral density equal to unity. They have been analyzed in several different ways.

First, by means of the microscopic spectral density defined by

$`\rho _s(u)=\underset{V\mathrm{}}{lim}{\displaystyle \frac{1}{V\mathrm{\Sigma }}}\rho ({\displaystyle \frac{u}{V\mathrm{\Sigma }}}).`$ (6)
For $`\beta =2`$ it is given by

$`\rho _s(z)={\displaystyle \frac{z}{2}}\left[J_{N_f+|\nu |}^2(z)J_{N_f+|\nu |+1}(z)J_{N_f+|\nu |1}(z)\right].`$ (7)
The result for $`\beta =1`$  and $`\beta =4`$  is more complicated but can be expressed as an integral over Bessel functions. The microscopic spectral density was first observed for Dirac spectra of instanton liquid field configurations  both for $`N_c=2`$ and $`N_c=3`$. Its first lattice studies, for quenched $`SU(2)`$ gauge theory with staggered fermions (with Dyson index $`\beta =1`$), were performed in  (see Fig. 1). The agreement between lattice QCD at Random matrix theory is equally good for $`N_c=3`$  (with Dyson index $`\beta =2`$), for QCD with adjoint fermions , which is in the class $`\beta =1`$, and for strong coupling $`U(1)`$ gauge theory  (also with Dyson index $`\beta =2`$). Although most results have been obtained in the quenched limit, the agreement with chRMT for dynamical quark masses of order $`1/V\mathrm{\Sigma }`$  or massless quarks in the Schwinger model  is equally impressive.

In Fig. 2 we show the microscopic spectral density for dimensionless dynamical quark mass $`\mu =mV\mathrm{\Sigma }`$ as given in the legend of the figure.

A second way to study the Dirac spectrum is by means of the valence quark mass dependence of the chiral condensate defined by

$`\mathrm{\Sigma }(z)={\displaystyle \frac{1}{V}}\mathrm{Tr}{\displaystyle \frac{1}{D+z}}.`$ (8)
Its analytical expression can be derived from the low-energy limit of the QCD partition function  as well as from chRMT . For $`\beta =2`$ we find

$$\frac{\mathrm{\Sigma }(z)}{\mathrm{\Sigma }}=x\left[I_a(x)K_a(x)+I_{a+1}(x)K_{a1}(x)\right],$$
(9)
where $`a=N_f+|\nu |`$ and $`x=zV\mathrm{\Sigma }`$. In Fig. 3 we compare  the analytical result (full line) with lattice data obtained by the Columbia group . The point above which the lattice data depart from the the chRMT result agrees with our estimate of the Thouless energy (2). These results have been confirmed by independent simulations  and have been extended to other symmetry classes .

A third way to analyze the statistical properties of the Dirac eigenvalues is by means of the distribution of the smallest eigenvalues. As an example, the analytical result for $`\beta =2`$ is given by , $`P(\lambda _{\mathrm{min}})=\frac{\lambda _{\mathrm{min}}}{2}\mathrm{exp}(\lambda _{\mathrm{min}}^2/4)`$. The results for $`\beta =1`$, $`\beta =4`$, and nonzero quark masses, are more complicated . In Fig. 1 we show results  for quenched $`SU(2)`$ lattice data. Results for all three symmetry classes as well as nonzero topological charge  are shown in Fig. 4. The latter results were obtained with the overlap Dirac operator. Dirac spectra of the Schwinger model have also been analyzed at nonzero topological charge  and complete agreement with chRMT was found . The continuum limit of the staggered Dirac operators is approached very slowly, and on today’s lattices the Dirac spectra are described by analytical results for zero topological charge . Recently, analytical results for the $`k`$’th smallest eigenvalue  gave a perfect description of the lattice data .

A more subtle way to study the statistical properties of eigenvalues is by means of the two-point correlation function defined as

$`\rho (\lambda ,\lambda ^{})={\displaystyle \underset{k,l}{}}\delta (\lambda \lambda _k)\delta (\lambda ^{}\lambda _l).`$ (10)
The two-point correlation function for the quenched $`SU(2)`$ staggered Dirac operator was compared with chRMT in . Also for instanton liquid gauge field configuration one finds  agreement with chRMT in its domain of validity. The volume dependence of the Thouless energy was investigated both for instanton liquid configurations  and lattice QCD simulations  and good agreement with the theoretical predictions  was found. A related quantity is the disconnected scalar susceptibility defined by

$$\chi ^{\mathrm{disc}}(m)=\frac{1}{N}\underset{k,l=1}{\overset{N}{}}\frac{1}{(i\lambda _k+m)(i\lambda _l+m)}\frac{1}{N}\underset{k=1}{\overset{N}{}}\frac{1}{i\lambda _k+m}^2.$$
(11)
Lattice results  (see Fig. 5) show a sharp transition point which can be identified as the Thouless energy. Below this energy the susceptibility follows the chRMT prediction (dashed curve). A complete analytical description up to $`\mathrm{\Lambda }_{\mathrm{QCD}}`$ is obtained from chiral perturbation theory (full curve)  which applies in the domain $`\lambda _{\mathrm{min}}m\mathrm{\Lambda }_{\mathrm{QCD}}`$. Similar agreement has been found for the scalar susceptibility of the $`U(1)`$ staggered Dirac operator .

Dirac spectra at finite temperature and nonzero chemical potential have been studied in much less detail. Because of finite size effects comparisons with chRMT are difficult at the critical temperature. Dirac spectra near $`T_c`$ were analyzed in detail in . Because the chiral phase transition in chRMT has mean field critical exponents  there is no reason to believe that the eigenvalue fluctuations follow the Random Matrix predictions  at the critical point. However, beyond $`T_c`$ there is some evidence that the smallest eigenvalues show a fluctuation behavior as predicted by RMT . At nonzero chemical potential the Dirac operator is nonhermitian and its eigenvalues are scattered in the complex plane. Recent work  shows that the global spectral properties are described by a chiral Lagrangian  or Random Matrix Theory . The statistical analysis of the eigenvalue fluctuations is much more complicated in this case, but the first lattice results  seem to confirm the theoretical expectations .

Up to now we only discussed the statistical properties of the Dirac eigenvalues near $`\lambda =0`$. Although physically less relevant, one can also analyze the statistics of the eigenvalues in the bulk of the spectrum. Assuming that the statistical properties do not change along the spectrum we can average in two different ways: by averaging over independent gauge field configurations and by averaging over the spectrum. The advantage of spectral averaging is that it requires only one or a few independent gauge field configurations. The equality of the two averages is known as spectral ergodicity and was investigated in the context of QCD Dirac spectra in . The Thouless energy was only found in ensemble averaging. The enhanced eigenvalue fluctuations result from the “collective” motion of the eigenvalues in the evolution of the ensemble. In Fig. 6 we show  the spacing distribution $`P(S)`$ of neighboring eigenvalues, the number variance $`\mathrm{\Sigma }^2(n)`$ and the $`\mathrm{\Delta }_3`$ statistic. The number variance is defined as the variance of the number of levels in an interval containing $`n`$ eigenvalues on average, and $`\mathrm{\Delta }_3(n)`$ is obtained by integrating $`\mathrm{\Sigma }^2(n)`$ over a smoothening kernel. The question has been raised whether eigenvalue correlations in the bulk are different above and below $`T_c`$, but no effects have been seen  (see also Fig. 7). A transition toward Poisson statistics only takes place at very small values of the coupling constant (see Fig. 7).

Finally, lattice results for QCD Dirac operator in 3 dimensions  have been compared with Random Matrix Theory. In this case one finds agreement with the Wigner-Dyson ensembles , but we will not discuss this topic in this review.

## 4 Conclusions

The generating function of the Dirac spectrum is given by the QCD partition function with additional ghost quarks with a mass scale given by the region of the the Dirac spectrum we are interested in. At low energies this partition function reduces to a gas of weakly interacting Goldstone modes. In the domain where the kinetic term can be neglected it reduces to a chiral Random Matrix Theory with the global symmetries of the QCD partition function. The predictions based on these arguments have been confirmed by numerous lattice QCD simulations. This does not mean that one can refrain from doing lattice simulations. The point is that universal behavior and the phenomenologically relevant nonuniversal properties are found in the same lattice simulations. The real progress is the understanding of the symbiosis of these two features of the strong interactions.