In our view, the main contributions of this work are in bringing attention to the need for compactness in program synthesis; showing its independence from existing criteria; giving a precise formulation in terms of minimality; and in designing and implementing algorithms to synthesize compact strategies.

### 2 Background

Automata A finite automaton is a tuple (Q, Σ, Q, δ, F ˆ ) where Q is a set of states; Σ is a set of letters, an alphabet; Qˆ is a non-empty set of initial states; δ ⊆ Q × Σ × Q is a transition relation; and F is a non-empty set of final states.

A word over Σ is a (possibly empty) sequence of letters from Σ. For a word w, its length |w| is the number of letters in w if w is finite and ω if w is infinite. We assume the standard definition of a run of the automaton on a word. If w is finite, a run on w is accepting if the last state of the run is in F; if w is infinite, a run is accepting by the B¨uchi condition if a state in F occurs on the run infinitely often. The language of an automaton is the set of words for which there exists an accepting run. One typically distinguishes between the finite-word language and the infinite-word language of an automaton. An automaton is deterministic if there is exactly one initial state and for every q and a, there is at most one q 0 such that (q, a, q0 ) is in δ.

We use the standard abbreviations DFA, NFA and NBA for a deterministic automaton, a nondeterministic automaton over finite words, and a nondeterministic B¨uchi automaton over infinite words respectively.

LTL Linear Temporal Logic (LTL) is a logic defined over a set of atomic propositions, AP. The logic has the following minimal grammar, where p ∈ AP:

$$f := p \quad | \quad f\_1 \land f\_2 \mid \neg f\_1 \mid \propto f\_1 \mid f\_1 \Downarrow f\_2 \rangle$$

The satisfaction relation is defined over infinite words where each letter is a subset of AP. It has the form w, i |= f for a word w and a natural number i, and is given by structural induction on formulas. We omit the standard definition. The language of a formula is the set of words that satisfy it. Standard constructions compile an LTL formula to an NBA that accepts the same language (cf. [18,39]), possibly incurring an exponential blowup.

Programs as Transition Systems A program is represented by its state transition system. This is a Moore machine, defined as a tuple (S, S, I, O, R, o ˆ ) where S is a set of states, Sˆ is a non-empty set of initial states; I is a set of input values; O is a set of output values; R ⊆ S × I × S is the transition relation, which must be total on I; and o : S → O is the output mapping. An execution of this system is an unbounded alternating sequence of states and inputs, and takes the form s0, a0, s1, a1, . . ., such that for each i, the triple (si , ai , si+1) is in the transition relation. A computation is an execution of this form where s0 is an initial state.

Input-Output Words An input-output word (i/o word for short) is a pair of sequences (a, b) where a is a sequence of inputs, b is a sequence of outputs, and |b| = 1 + |a|. The input-output word induced by a program execution s0, a0, s1, a1, . . . is the pair (a, b) with b = o(s0), o(s1), . . .. We sometimes write an i/o word in the linear format b0, a0, b1, a1, . . . for clarity. It is also common (cf. [32]) to view an infinite i/o word (a, b) in the "zipped" form a ./ b = (a0, b0),(a1, b1), . . .. For a temporal property ϕ defined over input and output predicates and program M, the program M satisfies ϕ, written M |= ϕ, if the zipped input-output word of every computation of M satisfies ϕ. Each atomic proposition is a function in I × O → Bool; an i/o pair (a, b) induces the set of propositions {p | p(a, b)}.

Games and Strategies A strategy is a function from finite sequences of inputs to outputs, represented as σ : I ∗ → O. For an infinite input sequence a = a0, a1, . . ., the strategy σ induces the infinite output sequence denoted σ(a), given by σ(), σ(a0), σ(a0, a1), . . .. A play for input a is the i/o word (a, b = σ(a)). We sometimes abuse this notation and use σ(a) to refer to the play induced by a. A play is winning for a temporal property ϕ if it satisfies this property when viewed as a zipped i/o word. A strategy σ is winning for ϕ if for every input a, the play on a is winning for ϕ.

The realizability question is: given a property ϕ, determine whether there exists a program satisfying ϕ. The synthesis question is: given a property ϕ that is realizable, construct a program that satisfies ϕ. A strategy σ induces a deterministic program with an infinite state space, denoted P(σ) = (S, S, I, O, R, o ˆ ). The state space S is the set of finite input sequences I ∗ , the initial state is , the output label for state x is σ(x) and the transition relation R is given by {(x, a, xa) | x ∈ I ∗ , a ∈ I}. This is in fact an infinite complete tree over I (sometimes called a "fulltree") where each node is labeled by an output value. A labeled fulltree, in turn, corresponds to a strategy and a deterministic program.

Synthesis Methods for Temporal Properties There is an extensive literature on methods to synthesize programs from LTL specifications (cf. [34,32,31,26] and tools that implement various algorithms (cf. [33,8,17,27,35,20]), all based on the conversion from LTL formulas to equivalent automata.

The classical approach to realizability of temporal properties (which we only sketch here, cf. [34,32]) is via the connection between programs, strategies, and labeled fulltrees. If a property ϕ is realizable, there is a deterministic program M satisfying ϕ. This program may also be seen as a strategy and a fulltree. From a deterministic word automaton with the same language as ϕ, one constructs a tree automaton that accepts precisely the fulltrees that satisfy ϕ. Now ϕ is realizable if and only if the language of this tree automaton is non-empty. For properties in LTL, this procedure can be carried out in 2EXPTIME in the length of the formula ϕ; the problem is 2EXPTIME-complete [32]. A winning strategy can be extracted as a finite state, deterministic reactive program from the tree automaton, thanks to the finite-model property of temporal logic. This approach is implemented in the tool Strix [30].

Two other approaches have been developed. One is to limit the logic: the GR(1) fragment expresses many useful properties, has a lower complexity (DEX-PTIME), and can be implemented easily using symbolic (BDD-based) methods [31]. This is implemented in several tools [33,8,17,27]. The bounded synthesis method applies to full LTL and is iterative in nature. By placing bounds on the size of the intended program and the ranking argument for formula satisfaction, one obtains a simpler safety game, which can be solved using symbolic methods [26,35,20]. The approach is implemented in [11,19].

We use two of the approaches described above in this work. The classical approach is used to determine compact realizability of an arbitrary LTL formula, while GR(1) approach is used in the multi-robot setting.

### 3 Compactness

We formulate compactness for temporal specifications, investigate its properties, and show how to synthesize a compact strategy through a specification transformation. We consider specifications on infinite words for simplicity and to match the semantics of temporal logic.

A relation ≺O over the set of infinite output words is a preference relation if its transitive closure ≺ + O is irreflexive. We informally say that word b is better than b 0 if b ≺ + O b 0 holds. As the transitive closure is irreflexive, it is not possible for a word to be better than itself, matching intuition. This relation is extended to input-output words as follows. An i/o word (a, b) is better than an i/o word (a 0 , b0 ) if (1) the input sequences a and a 0 are identical, and (2) b ≺ + O b 0 . The first condition ensures that comparable words have the same input sequence, which is important as we are ultimately interested in the i/o words that are generated as plays of strategies.

Definition 1 (Compact Strategy). A strategy σ is compact for an i/o language L if (1) σ is a winning strategy for L and (2) for every input sequence a, there is no i/o word (a, b0 ) such that (a, b0 ) satisfies L and (a, b0 ) is better than the i/o word (a, b = σ(a)) that is produced as the play of σ on input a.

The first condition ensures that σ is a valid strategy for L; the second that a compact strategy produces the "best possible" output for each input. We say that a language L is compactly realizable if it has a compact strategy.

Theorem 1. A language L is realizable if it is compactly realizable. The converse does not hold.

Proof. From right-to-left, consider a compact strategy σ for L. From the definition, σ is a winning strategy for L, hence L is realizable.

The converse does not hold. Let the input set I = {0, 1} and the output set O = {c, d} with the output preference ordering c < d extended point-wise to output words. Let the specification L consist of sequences of the form c(0c) ω and d({0, 1}d) ω. This is realizable. No winning strategy can produce c on as there can be no win on input 1ω. The single winning strategy produces d on every input sequence, including . But this strategy is not compact: for input 0ω it generates d(0d) ω, but there is the better word c(0c) ω in L. ut

Standard realizability is monotone: if L 0 ⊆ L and program M satisfies L 0 , then M also satisfies L. However, compact realizability is neither monotone nor anti-monotone (proof in the full version). As is the case with deduction systems for commonsense reasoning (cf. [37]), non-monotonicity is a consequence of the formulation in terms of minimality.

The simple example from the Introduction is easily extended to a collection of N "if-condition-then-action" requirements. The IFTTT service (https://ifttt. com) or Apple Shortcuts implement these operationally, using an event-driven rule engine. However, from the viewpoint of temporal logic and synthesis, the results can be unexpected, as we have seen. The N requirements in LTL have the shape (V i : G(a(i) ⇒ X b(i))). The smallest model is one with a single state, issuing all the b actions unconditionally. This is clearly unintended. The intended model, which is compact, has 2N states, one for each subset of the b actions. Thus, the gap between the smallest non-compact and compact models can be exponential in the length of the specification.

We now show the main theorem that links compact and standard realizability through a specification transformation.

Definition 2 (minimal language). For a language L over alphabet Σ and a preference relation ≺ on Σ-words, the minimal elements of L form the language

$$\min(L, \prec) = \{x \: \mid \ x \in L \land \neg(\exists y : y \in L \land y \prec^+ x)\}$$

I.e., a word x is in min(L, ≺) if it belongs to L and there is no word y in L that is transitively better than x.

Theorem 2. Language L is compactly realizable if and only if min(L, ≺) is realizable.

Proof. (Left-to-right) Let σ be a strategy that compactly realizes L. Consider any input sequence a. The output b = σ(a) produced by the strategy is such that there is no word in L that is better than (a, b), by the definition of compactness. Hence, (a, b) is in min(L, ≺). As this holds for each input sequence, σ is a winning strategy for min(L, ≺).

(Right-to-left) Let σ be a winning strategy for min(L, ≺). For any input sequence a and its corresponding output b = σ(a), the word x = (a, b) must satisfy min(L, ≺). By the definition of min, we have that (1) x also satisfies L. Moreover, (2) there is no i/o word y that is better than x and also satisfies L. From (1) and (2), σ is a compact strategy for L. ut

#### 3.1 Effective Minimality Constructions for LTL

Theorem 2 implies that one can reduce compact realizability to standard realizability. Given a temporal specification ϕ, we transform its language L(ϕ) to the language C(ϕ) = min(L(ϕ), ≺). Starting from an LTL formula f, we give two constructions: one for the minimal language C(f), the other for its complement. The constructions assume that the relation ≺+ can be expressed as an NBA, which is the case for the preference order defined in the Introduction.

The first construction directly follows Definition 2. The left-hand term (x ∈ L(f)) is fulfilled by the standard conversion from LTL formula f to an NBA Af . For the right-hand term, we use the same NBA Af , now re-defined over y, for the y ∈ L(f) term; intersect this with the NBA for ≺+; then project onto x and complement to obtain an NBA for the right-hand conjunct. The intersection of these two NBAs provides an NBA for C(f). These steps may result a worst-case double exponential blowup in the size of f: the first exponential is in the construction of Af ; the second is in the complementation step. A similar construction applies if the specification is given directly as an NBA.

The second construction produces an NBA for the complement of the minimal language, with "only" a worst-case single exponential blowup. The complement of C(f) is (from the definition) {x | x 6∈ L(f) ∨ (∃y : y ∈ L(f) ∧ y ≺+ x)}. For an LTL formula f, one constructs NBAs Af and A¬f for the LTL formulas f and ¬f, respectively. An NBA for (∃y : y ∈ L(f) ∧ y ≺+ x) is obtained as in the first construction by omitting the final complementation step. The union of this NBA with the NBA for A¬f gives an NBA for the complement of C(f).

The NBA for the complement of C(f) can be used to model-check whether a given strategy is compact. It can also be used to synthesize machines using bounded synthesis, which requires an NBA for the complement of the specification property. The worst-case blowups are unavoidable: that follows from a lower-bound result by Birget [5] and a simpler but less general result of ours, discussed in the full version of this paper.

#### 3.2 Relationship to Quantitative Synthesis

The formulation of compactness is in terms of a qualitative notion of minimality. A natural question is the relationship to methods for synthesis with quantitative objectives; in particular, methods for producing programs with optimal worst-case or average-case behavior [6,13]. Expanding on the argument in the Introduction, we establish that worst-case optimality cannot always distinguish between compact and non-compact solutions to a given specification.

In quantitative formulations, the synthesis game is formulated so that each transition has an associated reward. The reward of an infinite computation is defined using standard cumulative metrics such as mean-payoff (the limit of average rewards over successively longer prefixes) or discounted sum (the sum of rewards over the computation discounted geometrically, i.e., the k'th reward contributes a factor d k , where d ∈ (0, 1) is the discount factor). The objective is to find a winning strategy with maximum worst-case reward, where the worstcase reward is the minimum reward over all inputs. In the stochastic form of the game, an additional probabilistic player "Nature" is introduced, and the objective is to find a winning strategy with the maximum average-case reward, where the average is the expectation taken over the induced probability space. Precise definitions of these concepts can be found in [6].

Worst-case optimality We return to the example discussed in the Introduction. There, we had assumed for simplicity that each action set is assigned a cost that is its cardinality. However, the reasoning carries over to any cost function that is monotonic with respect to set inclusion: i.e., if A ⊂ B then cost(A) < cost(B). Intuitively, monotonicity captures the preference for choosing a smaller set of output actions. Consider the mean-payoff cost of an infinite execution where the input a is always true. For the non-compact program in Figure 1(i), it is obvious that the limit of the average cost is cost({b}). That is also the case for the compact program in Figure 1(ii): the fact that the initial cost is cost(∅) is swamped in the limit. This is the worst case input for both programs by the monotonicity of the cost function. The best case for the program on the right is when the input a is almost everywhere false. Thus, worst-case optimality cannot distinguish between the two programs for any monotonic cost function.

Average-case optimality We now show that average-case optimality also cannot always distinguish between compact and non-compact strategies. The general principle is that if a strategy is non-compact only for a finite prefix of a computation, its average-case cost in the limit will be the same as the cost of a strategy which performs in a compact manner throughout.

Consider the input set I = {0, 1}. Suppose that inputs are chosen uniformly at random. The output set O is the set of subsets of the action set A = {a, b}. Let the specification be the following: the initial choice of output set is either {a} or A; all subsequent outputs must be A. There are only two winning strategies, which differ only in their choice of initial output (either {a} or A); both produce output A subsequently regardless of the input. Assuming unit cost per output

action, the average cost of a run of length n is thus (1 + 2(n − 1))/n for the first strategy and 2 for the second. In the limit, both strategies have average cost 2, although the first is compact, while the second is not. This argument also applies for an arbitrary but monotone cost function.

In our view, quantitative measures are best suited to modeling the real cost of actions rather than to modeling a preference ordering. The two may, however, be combined to good effect. As compactness is ensured with a specification transformation, one can modularly apply quantitative synthesis to the transformed specification min(L, ≺) to obtain strategies that are compact and also optimal with respect to a cost metric.

#### 3.3 Approximating Compactness

The worst-case exponential blowups can make it difficult to produce compact strategies. Moreover, Theorem 1 asserts that there are specifications that are realizable but have no compact strategies. For both reasons, we describe methods by which one can approximate the compactness criterion.

Approximately Minimal Languages The first method is to tighten the language L to L 0 that lies between L and min(L, ≺); we call L 0 approximately minimal for L. We synthesize a program satisfying L 0 . Given an NBA A for L over alphabet I × O, we construct an NBA Aˆ whose language is approximately minimal for L. This construction applies only to a class of preference relations that are induced pointwise by a partial order ≤ on individual letters of the output set O.

For infinite i/o words w = (a, b) and w 0 = (a 0 , b0 ), define w ≺p w 0 iff (1) for all i, ai = a 0 i (inputs are identical) and bi ≤ b 0 i , and (2) there is some i for which bi < b0 i . We say that w p w 0 if w ≺p w 0 or w = w 0 . The ordering ≺p is transitive and regular. It is easy to construct an automaton accepting ≺p, which checks condition (1) at each position of the zipped word w ./ w0 , and accepts only if condition (2) holds at some position on the zipped word. The subset and cardinality preference relations introduced earlier are of this type.

Given an NBA A recognizing L, the NBA Aˆ is constructed by excluding certain transitions of A. Specifically, a transition (q,(a1, b1), q0 ) of A is omitted in Aˆ if there is a "better" transition (q,(a2, b2), q0 ) in A with a1 = a2 and b2 < b1. Automaton Aˆ can be efficiently constructed from A by performing a single pass over δ. The set of states, initial states and final states are identical in A and Aˆ.

Theorem 3. For a pointwise preference order ≤ over O, L(Aˆ) is an approximately minimal language for L.

Proof. It is easy to see that L(Aˆ) ⊆ L(A), as an accepting run in Aˆ is also an accepting run in A.

For the other inclusion, let w be in min(L, ≺p). Then, w is also in L. Thus, there is an accepting run ρ for w in A. If all transitions in ρ are present in Aˆ, then w is also in L(Aˆ). If not, there is a transition (q,(a1, b1), q0 ) at the k-th step of ρ (for some k) that is not present in Aˆ. By construction, there must be a transition (q,(a1, b2), q0 ) in A such that b2 < b1. Now consider the run ρ 0 that is generated by swapping transition (q,(a1, b1), q0 ) with (q,(a1, b2), q0 ) at the k-th step. This is also an accepting run, on a word w 0 that is identical to w except that it has (a1, b2) rather than (a1, b1) as its k-th entry. As w 0 is in L and w 0 ≺p w, it cannot be the case that w is in min(L, ≺p), a contradiction. ut

Minimal Strategies for L The second method searches greedily for compact strategies in a game graph for L. For strategies σ and σ 0 , say that σ v σ 0 (read as "σ is better than σ 0") if for all input sequences a, σ(a) = σ 0 (a) or σ(a) ≺+ σ 0 (a). I.e., the output on input a is using σ is at least as good as that using σ 0 . The minimal elements according to this ordering are called minimal strategies for L. It is easy to show that every compact strategy for L is a minimal strategy for L. The converse does not hold.

The greedy construction applies to a game graph for L where strategies are memoryless (e.g., if synthesis for L is a safety game or a parity game), and if the preference order is pointwise, as defined above. The core idea is simple: compute the set of winning positions; then nondeterministically and greedily extract a strategy by choosing only those transitions between successive winning positions that are output-minimal with respect to <. In the full version, it is shown that any strategy extracted in this manner is minimal for L.

### 4 Evaluation

### 4.1 Multi-Robot Coordination

Our original motivation to investigate compactness comes from an application to multi-robot orchestration. Due to space limitations, we describe this setting in brief. One has available multiple, heterogeneous robots, each capable of carrying out certain actions, some of which cannot be allowed to overlap. The goal is to perform specified tasks by (a) assigning robots to carry out actions and (b) sequence the actions appropriately. Tasks are described in a simple declarative language, called Resh [12], that has been implemented and used to control groups of mobile robots. A useful subset of Resh is given by the following grammar, where A is the set of action names and R is a set of robot names.

$$S := a \to R \mid S \Rightarrow S \mid S \& S \mid S \mid S \mid S + S$$

The interpretation of these operators is in terms of a finite-word input-output sequence. A term a → R is interpreted as "perform action a using one of the robots in R." For this, a control strategy chooses a robot r in R, and produces a "(begin a on r)" output event. Action duration is not fixed: E.g., the time taken to perform a "move to position p" action may vary as the robot maneuvers around humans. The completion signal is a "(end a on r)" event that is an input to the control strategy. The other operators are interpreted as ⇒ (sequencing), & (concurrent), | (choice), and + (concurrent with both tasks starting together). The interpretation of each operator produces a regular language.

The finite-word semantics is appropriate for robotics tasks that must be performed to completion. The same observation motivates the use of LTLf (a finite-word variant of LTL) in [38] to specify robotics tasks. A winning control strategy is one that satisfies the semantics of the operators.

As action completions are uncontrolled, even a simple specification such as a → R is unrealizable if the completion signal is never issued by an adversarial environment. It is thus necessary to restrict the environment so that every initiated action is eventually completed. This assumption must be interpreted over infinite words. It has the shape of a conjunction of LTL formulas G(begin(a, r) ⇒ X F end(a, r)) over all actions a and robots r. This can be represented by a DBA which tracks the set of pending (i.e., begun but not ended) actions. This DBA is worst-case exponential in the number of action-robot pairs, but in practice is limited by the concurrency in the specification.

In order to match the infinite-word environment constraint, the Resh system specification must be extended to infinite words. This is done by saying that an infinite word w satisfies the specification if there is a prefix x of w such that x satisfies the specification. Being a regular language, a Resh specification is representable as a DFA; this is extended to infinite words as a DBA by replacing the outgoing transitions of each final state with a self-loop on all inputs.

We have arrived at the final form of the synthesis question, which has the shape E ⇒ S, where E (the environment assumptions) and S (the system specification) are both representable as deterministic B¨uchi automata. That is precisely the general form of a GR(1) specification [31]; therefore, algorithms for GR(1) synthesis can be applied to synthesize finite-state controllers.

Implementation and Experiments. Our initial experiments in synthesis with (E ⇒ S) occasionally produced non-compact strategies, which motivated this exploration of compactness. We now use the modified specification E ⇒ Sˆ, where the system portion is made approximately compact through the construction in Section 3.3, which preserves the GR(1) format. This specification produces compact strategies for all cases we have examined.

Our implementation of GR(1) synthesis uses a SAT solver, similar to the method of [10]; we found this to be significantly faster than BDD-based methods. As there is not a well-defined set of benchmarks for robotics or Resh specifications, we generate 500 specifications at random, producing specifications with parse-tree depth 4, biased slightly to prefer the sequencing operation (i.e., ⇒ ) over the others, as is likely to be the case in practice.

The system specification is set up to have two robots. Actions are allowed to overlap, which implies that all specifications are realizable. Of the 500 specifications, the GR(1) game graph was generated for 428 (85%) within a timeout limit of 5 minutes for each specification. (The Resh-to-automaton construction uses BDDs to symbolically represent output event sets, which sometimes blows up.) All 428 game graphs are solved by the SAT-based GR(1) procedure within a timeout of 5 minutes per game. The median solution time is 3 seconds; 90% are solved within 30 seconds; and all are solved within 225 seconds. We also experimented with a small hand-designed group of specifications where certain action overlaps are forbidden, which are also resolved efficiently.

### 4.2 Compactness for LTL

We now describe an implementation of a compact synthesis pipeline for general LTL specifications. Our experiments use the benchmarks from the SYNTCOMP (2020) competition.4 In these experiments, the preference order is fixed as the pointwise subset order. We were forced to make this arbitrary choice as there is limited information about the origin of the benchmark problems, so we could not tailor the ordering to the problem domain.

The goal is (1) to determine the difficulty of constructing a compact synthesis pipeline for LTL, and (2) to gauge the practical feasibility of the compact synthesis procedures. The experiments are designed to answer the following questions that arise from (2): (Q1) What is the overhead on generating compact strategies compared to standard synthesis? (Q2) Is the approximation procedure more efficient than exact compactness? and (Q3) How effective are the approximate constructions at producing compact strategies?

Fig. 2. An overview of the workflow for our experiments and tool. In the figure, minˆ refers to the approximate minimal language, while RefModel(f) refers to the reference model for formula f.

A high-level overview of the internal structure of our tool is in Fig. 2. Our implementation chains together several known tools: the automaton libraries SPOT (v. 2.9.5) and Owl (v.20.06)[25], the synthesis tool Strix (v. 20.10)[30] and the model checker NuSMV (v. 2.6.0) [14]. We also use the AIGER toolkit [4] as well as the Syfco synthesis format converter5 . We are grateful to the authors for making these tools freely available.

4 At https://github.com/SYNTCOMP/benchmarks.

5 At https://github.com/reactive-systems/syfco

Our tool offers three main features: (1) Compact Realizability: given an LTL formula f, determine if f is compactly realizable. This feature uses the compactness transformation from Section 3.1 to produce an automaton for the complement of the minimal language, which is then complemented, determinized and synthesized using Strix; (2) Compactness Test: given an LTL formula f and a candidate program P, determine if P is a compact program for f; and (3) Approximate Compact Realizability: given an LTL formula f, generate an approximately compact strategy. Here we implement the construction of the approximate minimal automaton from Section 3.3.

Our experiments were carried out on a Linux VM running Ubuntu 20.04 with 12 GB of memory. Naturally, we only consider synthesizing compact strategies for specifications that are realizable 6 . The results can be summarized as follows: (A1) We compare the efficiency of compact synthesis to the standard synthesis by evaluating the number of specifications that can be synthesized within a certain time limit. We fix this time limit to be 10 minutes, and use Strix for standard synthesis. (With this limit, the entire run over the benchmarks takes several hours.) Strix determines realizability for 396 specifications out of 421 (∼ 94%), while our tool determines compact realizability for 213 (∼ 50%). (A2) Within the same time limit, the approximation technique determines realizability for 398 specifications, significantly more than for exact compactness and about the same as for standard realizability. (A3) We model-check the strategies generated through approximate compact realizability. Model-checking for compactness requires the complement minimal automaton of a specification, so we set the time limit of 10 minutes per specification to generate this automaton. Within this limit, our tool manages to construct the required automaton for 246 specifications. Generating approximate compact strategies for these 246 specifications, and applying the Compactness Test on these strategies, we find that ∼ 42% of the synthesized strategies are compact.

In addition, we tried our tool on the generalized version of the example specification from the introduction (V i : G(a(i) ⇒ X b(i))). Our tool can synthesize a compact strategy till N = 8 fairly quickly, after which our setup struggles to compile the original LTL formula to an NBA. On the same set of specifications, the approximate techniques also produce a compact strategy.

The implementation process was fairly straightforward, a pleasant surprise given the number of tools and format conversions involved. We had to patch some tools to extend their capabilities (e.g., to allow automata as specifications) and to implement format conversions.

In summary, compact synthesis is feasible for a substantial number of specifications. Where it is not – due either to blowups in automaton construction or due to the gap between normal and compact realizability – one can use the approximation procedure defined in Section 3.3 to generate strategies that are minimal with respect to the strategy ordering.

6 We refer to the helpful classification of these benchmarks into realizable and unrealizable ones from https://github.com/meyerphi/syntcomp-reference/.

### 5 Related Work

We discuss closely related work in synthesis and commonsense reasoning.

Qualitative Temporal Synthesis There is a considerable literature on the synthesis of open reactive programs from LTL specifications, starting with the seminal work by Pnueli and Rosner [32]. The beautiful theoretical results are made practical by the discovery of efficient algorithms for the GR(1) subclass [9,31], and procedures for bounded synthesis [21,36], based on so-called "Safraless" procedures [26]. These algorithms have been implemented in several tools,

e.g., [11,15,16,19,23,33,27]. Our work builds on this basis by transforming the search for compact strategies to a standard synthesis question that can be handled by these tools.

In the robotics domain, prior work investigates synthesis for an interpretation of LTL over finite words called LTLf [22,38,40]. Although Resh is similarly restricted to finite-word properties, a central difference is that specifications in LTLf (like LTL) are defined over propositions on robot and world state, and not in terms of actions of an unknown duration.

There are many ways to choose between satisfying models: e.g., [7] designs synthesis procedures that produce minimally vacuous models. While the formulations differ, there is a common thread in the notion of minimality with respect to an ordering over models.

Quantitative Temporal Synthesis A substantial body of work in temporal synthesis is focused on quantitative objectives. These problems are represented by games where each action has an associated cost (or, dually, reward) and the objective is to find strategies that minimize cost (or, maximize reward) (cf. [6]).  One could attempt to model compactness by assigning costs to actions such that if word x is better than word y then x has the lower cost. We chose not to develop solutions along such quantitative lines for two main reasons: first, as the connection between cost and preference is indirect, setting up the right cost assignments to model a desired preference ordering is difficult; secondly, the theoretical complexity and practical difficulty of quantitative synthesis is high. Instead, we chose to tackle the question in a qualitative manner.

As shown in Section 3, quantitative measures cannot always differentiate between compact and non-compact solutions. Using the specification transformation developed here, the two methods can, however, be used in cooperation: one can model the real costs of actions in a manner that is orthogonal to the preference ordering and compute minimal-cost, compact strategies.

A recent work [1] focuses on the "quality" of satisfaction of an LTL formula (e.g., preferring to satisfy one part of a specification over another). Synthesis is through a reduction to a standard LTL specification; unfortunately this has a worst-case exponential blowup.

Non-Monotonic Reasoning. As mentioned briefly in the introduction, the compactness criterion is a form of commonsense reasoning: one does not expect synthesized solutions to include unnecessary actions. Commonsense reasoning is exemplified by the classical frame problem, introduced in [29], which shows that the freedom of interpretation given by logic must be restricted in order to achieve commonsense conclusions.

It was soon recognized that such restrictions imply a non-standard notion of deduction, which is not monotonic: adding new hypotheses can invalidate current conclusions [37]. In [28], McCarthy suggests a formulation in terms of a circumscription operation: each inference is guarded with a "not(abnormal)" predicate, and a successor state is one where the extent of this predicate is minimized—i.e., abnormal effects are maximally limited while avoiding inconsistencies. Logically, this is specified in second-order logic as ϕ(A) ∧ ¬(∃B : B ⊂ A ∧ ϕ(B)), where ϕ is the specification and A is the abnormality predicate. Readers will immediately notice the similarity to the definition of min(L, ≺).

The importance of a general preference order in place of the fixed subset relation is laid out in [24]; the authors propose reasonable properties that any nonmonotonic inference relation should meet, and show that a definition in terms of a preference ordering satisfies those properties. Our formulation of compactness is based on similar notions of minimality over a preference ordering on words. This is at the root of the non-monotonicity of compactness. These similarities hint at deeper connections between compactness and non-monotonic commonsense reasoning; we aim to investigate those in future work.

Acknowledgments. We would like to thank colleagues at Bell Labs and at NYU for interesting discussions and helpful comments regarding this work. This work was supported in part by the National Science Foundation grant CCF-1563393 and by DARPA under contract HR001120C0159. The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense, the U.S. Government, or the National Science Foundation.

### References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

### ZDD Boolean Synthesis**⋆**

Yi Lin  1 , Lucas M. Tabajara1 ⋆⋆, and Moshe Y. Vardi1

Rice University, Houston TX 77005, USA<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
Abstract. Motivated by applications in boolean-circuit design, boolean synthesis is the process of synthesizing a boolean function with multiple outputs, given a relation between its inputs and outputs. Previous work has attempted to solve boolean functional synthesis by converting a specification formula into a Binary Decision Diagram (BDD) and quantifying existentially the output variables. We make use of the fact that the specification is usually given in the form of a Conjunctive Normal Form (CNF) formula, and we can perform resolution on a symbolic representation of a CNF formula in the form of a Zero-suppressed Binary Decision Diagram (ZDD). We adapt the realizability test to the context of CNF and ZDD, and show that the Cross operation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis.

Keywords: Boolean synthesis · Binary decision diagram · Zero-suppressed binary decision diagram · Quantifier elimination · Resolution.

### 1 Introduction

Boolean functions are widely used in electronic circuits, and thus in many aspects of computing, to describe operations over binary values. Often the most natural way to express such an operation is as a declarative relation between inputs and outputs. Implementing these operations in practice, however, requires a functional, rather than declarative, representation. The process of constructing a function that generates outputs directly from inputs, based on a given declarative relation between them, is called boolean synthesis. For example, boolean synthesis can be applied in constructing a full logical circuit from a relational specification [9,15] or an unknown intermediate component in an existing logical circuit [12]. Boolean synthesis is also useful for computing certificates for quantified boolean formulas (QBF), and advances in QBF solving and boolean synthesis are motivated by each other [3,20].

Formally, we are given a specification f(x, ⃗ y⃗), from B m × B n to B, relating two sets of boolean variables. The specification holds true if and only if y⃗ is a

c The Author(s) 2022

⋆ Work supported in part by NSF grants CCF-1704883, IIS-1830549, CNS-2016656, DoD MURI grant N00014-20-1-2787, and an award from the Maryland Procurement Office.

⋆⋆ Currently at Runtime Verification, Inc.

D. Fisman and G. Rosu (Eds.): TACAS 2022, LNCS 13243, pp. 64–83, 2022. https://doi.org/10.1007/978-3-030-99524-9\_4

correct output for the inputs x⃗. We solve the synthesis problem following the convention of splitting it into two sub-problems [9]:

Given a propositional formula f as the relational specification, we aim to synthesize a boolean function g that is correct by construction, meaning that as long as the input is realizable the output will satisfy the specification.

Prior work solved the boolean functional synthesis by converting the specification formula into a Binary Decision Diagram (BDD), defined in Section 2, and quantifying the output variables existentially [9]. BDDs constitute a formalism for representing Boolean functions, supported by mature tools such as CUDD [22]. The size of a BDD representing a formula can, however, be exponential in the number of variables. Oftentimes, it is even not possible to construct the BDD before starting to solve the problem [9]. Noticing how this blow-up in BDD size has restricted the potential of existing BDD-based synthesis algorithms, we seek to develop an algorithm that reduces the impact of this exponential blowup. Hence we look for an alternative data structure that might be more promising in representing boolean formulas compactly.

We identify here Zero-Suppressed Binary Decision Diagram (ZDD) [16], defined in Section 2, as such an alternative approach. ZDDs have been shown to sometimes outperform BDDs in the context of QBF solving [19]. Unlike BDDs, which represent a boolean formula semantically via the set of satisfying assignments, ZDDs are designed to encode sets of sets [14], allowing them to represent syntactically a formula in Conjunctive Normal Form (CNF) as a set of clauses, which are themselves sets of literals. This means that it may require an exponential-size BDD to represent a CNF formula, which can be alternatively compactly encoded as a polynomial-size ZDD representation.

It can be expected, however, that this more compact representation comes at a cost. Since ZDDs do not represent the solution sets directly like BDDs do, solving realizability and synthesis over this representation might require additional effort. With this in mind. we perform here a full investigation comparing ZDDs and BDDs for boolean synthesis. We focus on the following research questions:

Our synthesis problem can often be expressed as boolean synthesis for CNF specifications, as the boolean specification in synthesis problems is often given in CNF form, and even non-CNF specifications can be easily converted to CNF. Once specification formulas are given in CNF, it is possible to perform realizability by using the resolution operation, which is equivalent to existentially quantifying the output variables directly from the CNF formula. Each resolution step increases the number of clauses quadratically. But when a ZDD is used to represent the CNF formula, even when the number of clauses increases quadratically, the size of the ZDD tends to increase to a lesser extent.

The crux of our contribution is a boolean-synthesis algorithm that performs resolution on a symbolic, ZDD-based representation of CNF formulas. To solve the first sub-problem of realizability, we compute the set R ⊆ B m of all realizable inputs, and then check the full and partial realizability of the input domain. The realizable set is generated by applying resolution to the ZDD representation of the CNF formula, based on operations defined in previous work [4,5,19].

The second sub-problem requires construction of a witness function g ∶ B m → B n for the output variables y⃗ ∈ B n . We adapt the formulas defined in previous work [9] to the context of CNF, eliminating one output variable yi ∈ B at a time, and make use of the fact that resolution is equivalent to existential quantification. In this way we can extract a witness gi ∶ B m → B for variable yi without abandoning the ZDD representation.

After substituting the witness of an output variable back in the formula, we need to compute the next witness. This leads to our next challenge, which is how to guarantee that the formula remains in CNF after performing this substitution. The overall form of the entire formula after substitution is dependent on the form of the substituted witness function gi : clauses where yi is positive can be converted back to CNF if gi is also in CNF, but clauses where yi is negative require gi to be in Disjunctive Normal Form (DNF). Thus, what we need are two equivalent witness functions, one in CNF and the other in DNF.

Our solution is to use the Cross ZDD operation, first defined by Knuth [14]. We show that if the Cross operation, defined on "families of sets" [14], is applied to a ZDD representation of a CNF formula, then the result can be interpreted as the ZDD for an equivalent DNF. In this way, with the Cross operation, we can use the CNF version of a witness for positive occurrences of a variable, and use the equivalent DNF version for negative occurrences, while both preserving the equivalence and ensuring that the resulting formula remains in CNF.

Our experimental evaluation confirms the advantages of ZDDs in compilation, thanks to their linear size and direct correspondence to the CNF formula structure. As expected, this more compact representation can come with a tradeoff of increasing the difficulty of constructing witnesses. Therefore, in synthesis performance, neither ZDDs nor BDDs dominate across the board, each performing better in different families of formulas. We therefore advocate for the ZDD-based approach as an addition to the portfolio of boolean synthesis tools, serving as a complement to BDD-based approaches [11].

As shown in related works on boolean synthesis, there exist alternative tools including CegarSkolem [13], BFSS [1] and Manthan [10]. Our focus of comparison here is, however, on improvements to decision-diagrams based tools

for boolean synthesis, rather than tools based, for example, on QBF solvers. Decision-diagram based approaches enjoy some unique advantage. For example, decision diagrams facilitate partitioned-form representation [23]. Also, decision diagrams can be used as intermediate-step representation in temporal synthesis [24]. These unique advantages justify, we believe, our focus here on decisiondiagram based approaches. We return to this point in our discussion of future work.

### 2 Preliminaries

Boolean Formulas and Functions. Boolean formulas and boolean functions are built upon the boolean set B = {0, 1}. We identify a boolean formula f(x⃗) over m propositional variables x⃗ = (x1, . . . , xm) with the boolean function f ∶ B m → B such that f(a⃗) = 1 for an assignment a⃗ = (a1, . . . , am) ∈ B m if and only if a⃗ is a satisfying assignment to x⃗ in the formula. Two boolean formulas f and f ′ are logically equivalent if they represent the same boolean function (and therefore have the same set of satisfying assignments). Substitution of a boolean expression d(x⃗) in place of a variable xi in a boolean formula f(x⃗) is denoted by f[xi ↦ d] and defined by f[xi ↦ d](x⃗) = f(x1, . . . , xi−1, d(x⃗), xi+1, . . . , xm).

Conjunctive and Disjunctive Normal Forms. A literal is either a variable or the negation of a variable. A clause is a disjunction of literals, and a cube is a conjunction of literals. A boolean formula in the form of a conjunction of clauses is said to be in Conjunctive Normal Form (CNF), and a boolean formula in the form of a disjunction of cubes is said to be in Disjunctive Normal Form (DNF).

Definition 1 (Boolean Synthesis Problem). Given a boolean formula f(x, ⃗ y⃗) in CNF with m + n boolean variables, partitioned into m input variables x⃗ = (x1, . . . , xm) and n output variables y⃗ = (y1, . . . , yn), construct:

Binary Decision Diagrams. A (Reduced Ordered) Binary Decision Diagram (BDD) [2] is a directed acyclic graph that represents a boolean function. Internal nodes of the BDD represent boolean variables, and paths on the BDD correspond to assignments, leading either to a terminal node 1 if satisfying or 0 if unsatisfying. We assume that all BDDs are ordered, meaning that variables are ordered in the same way along every path, and reduced, meaning that superfluous nodes are removed and identical subgraphs are merged. Given these two conditions, BDDs are a canonical representation, meaning that two BDDs with the same variable order that represent the same function will be identical [2]. The variable order used can have a major impact on the BDD's size, and two BDDs representing the same function but with different orders can have an exponential difference in size.

Zero-Suppressed Decision Diagrams. A Zero-Suppressed Binary Decision Diagram (ZDD), is a data structure first defined in [16]. ZDDs are similar to BDDs but use a different reduction rule: while BDDs remove nodes where both edges point to the same child, ZDDs remove nodes where the 1-edge (edge assigning the variable to 1) points directly to the 0-terminal. Specifically, the 0-ZDD encodes formulas that are always valid, and the 1-ZDD encodes contradiction.

Semantics on Families of Sets. ZDDs can be used to implicitly represent families of subsets of a set S, where the variables in the ZDD correspond to elements of S that can be either present or absent in a subset [14]. For a ZDD Z, we denote by JZK the family of subsets represented by Z. We define J0K = ∅ and J1K = {∅} for the terminals 0 and 1, respectively. Using Z(x, Z0, Z1) to denote a ZDD with variable x as the root, ZDD Z0 as the 0-child and ZDD Z1 as the 1-child, we define JZ(x, Z0, Z1)K = JZ0K∪{{x}∪α ∣ α ∈ JZ1K}. Note that using this interpretation every subset in the family corresponds to a path to the terminal 1 on the ZDD. Since CNF formulas can be viewed as sets of clauses, where a clause can be viewed as a set of literals, we can use ZDDs to represent CNF formulas syntactically. When representing a formula in CNF by a ZDD, for each atomic proposition p we treat its positive and negative literals p and (¬p) as two distinct variables xp and x¬p. Then every path leading to the 1-terminal corresponds to a clause in the CNF formula, where xl connects to its 1-edge in the path if and only if the literal l is in the corresponding clause.

ZDD Operations. We use standard ZDD operations such as Subset0, Subset1, Change, Union, Intersect, and Difference, defined previously in [17] and implemented in the CUDD package [22]. In terms of families of sets, Subset0 (Z, x ) returns the family of all sets α such that α ∈ JZK and x ∈/ α, and Subset1 (Z, x ) returns the family of all sets α ∖ {x} such that α ∈ JZK and x ∈ α. Change(Z, x ) returns the family {α ∪ {x} ∣ α ∈ JZK and x ∈/ α} ∪ {α ∖ {x} ∣ α ∈ JZK and x ∈ α}. The operation Resolution(x, Z) returns the ZDD representing the result of applying resolution to variable x in the CNF represented by Z. It is implemented following [4], using the operations SubsumptionFreeUnion, which takes the union of two families of sets while removing subsumed sets, and ClauseDistribution, which returns the family of sets resulting from applying distribution over two given sets of clauses. The witness-construction phase also requires the Cross operation defined in [14] to convert between CNF and DNF representations. See Section 4 for details.

### 3 Realizability Using ZDDs

We describe in this work a ZDD-based algorithm to solve the Boolean-Synthesis Problem described in Definition 1. This means that the specification f(x, ⃗ y⃗), the realizability set R and the witness function g are all represented by CNF formulas encoded as ZDDs, as defined in Section 2. In this section we describe how to compute the realizability set R and analyze it to answer whether the specification is partially or fully realizable. In Section 4 we describe how to compute the witness function g.

#### 3.1 Realizable Set R

In order to construct the set R of realizable assignments to the input variables x⃗, as described in Definition 1, we need to quantify existentially the output variables y⃗, analogously to the BDD-based approach of [9].

To compute f0, . . . , fn as CNF formulas, we apply the resolution operation, which is equivalent to existential quantification [7]. We first state a normal-form lemma.

Lemma 1. [4] Let f be a CNF formula. Let f + p denote the conjunction of all clauses α such that (p∨α) is a clause in f. Let f − p denote the conjunction of all clauses β such that ((¬p) ∨ β) is a clause in f. Let f ′ p denote the conjunction of clauses γ in f where neither p nor (¬p) is a literal in γ. Then f is logically equivalent to (p ∨ f + p ) ∧ (¬p ∨ f − p ) ∧ f ′ p for a boolean variable p.

Proof. The claim follows from [4].

Next we show how to use resolution to existentially quantify a variable from a formula in the normal form of Lemma 1.

Lemma 2. Let y be a boolean variable, then the boolean formula (∃y)((y∨f + y )∧ (¬y ∨ f − y ) ∧ f ′ y ) is logically equivalent to ((f + y ∨ f − y ) ∧ f ′ y ).

Proof.

$$\begin{split} & (\exists y) \{ (y \lor f\_y^{+}) \land (\neg y \lor f\_y^{-}) \land f\_y^{\prime} \} \\ & \equiv (\exists y) \{ ((y \land \neg y) \lor (y \land f\_y^{-}) \lor (f\_y^{+} \land \neg y) \lor (f\_y^{+} \land f\_y^{-}) ) \land f\_y^{\prime} \} \\ & \equiv (\{ \exists y) (y \land f\_y^{-}) \lor (\exists y) (f\_y^{+} \land \neg y) \lor (\exists y) (f\_y^{+} \land f\_y^{-}) \} \land f\_y^{\prime} \qquad (f\_y^{\prime} \text{ excludes } y) \\ & \equiv ((\{ \exists y) (y \land f\_y^{-}) \lor (\exists y) (f\_y^{+} \land \neg y) \lor (f\_y^{+} \land f\_y^{-}) ) \land f\_y^{\prime} \} \qquad (f\_y^{+}, f\_y^{-} \text{ excludes } y) \\ & \equiv ((f\_y^{-} \lor f\_y^{+} \lor (f\_y^{+} \land f\_y^{-})) \land f\_y^{\prime}) \qquad (f\_y^{+}, f\_y^{-} \text{ excludes } y) \\ & \equiv ((f\_y^{-} \lor f\_y^{+}) \land f\_y^{\prime}) \end{split}$$

We call the formula ((f + y ∨ f − y ) ∧ f ′ y ) the resolution of the variable y in f. Note that this formula (specifically the subformula (f + y ∨f − y )) is not in CNF, but can be easily rewritten in CNF by distributing the clauses in f + y over the clauses in f − y . The equivalence of resolution and existential quantification then follows from Lemmas 1 and 2 above:

Corollary 1. For a formula f and a boolean variable y, the formula (∃y)f is logically equivalent to ((f + y ∨ f − y ) ∧ f ′ y ).

Proof. The claim follows from Lemmas 1 and 2.

We represent f + y , f− y , f′ y by ZDDs by applying the Subset0 and Subset1 operations described in Section 2: Z + y = Subset1(Z, y), Z − y = Subset1(Z,¬y), and Z ′ y = Subset0(Subset0(Z, y),¬y). We then use the ClauseDistribution operation to distribute the clauses of Z + y over Z − y , and the SubsumptionFreeUnion operation to combine all clauses into a single ZDD. This implements the operation Resolution(yi , Z) mentioned in Section 2. In practice, we follow the Cut-Elimination Algorithm of [4], which also eliminates tautologies by removing clauses where the same variable appears both positively and negatively. Therefore we can assume that the ZDD representations of f0, . . . , fn do not include subsumed and tautological clauses, which may also lead to smaller ZDDs.

The advantage of applying resolution symbolically over a ZDD representation, rather than directly over the CNF formula is that every resolution step increases the number of clauses in the formula quadratically. Thus, the number of clauses after multiple resolution steps can easily grow exponentially. ZDDs, compared to representing clauses explicitly, are well-equipped for representing compactly large sets of clauses, often being able to represent an exponential set of clauses in polynomial space [16]. The ZDD representation also makes it easy to remove subsumed and tautological clauses, further reducing size.

#### 3.2 Full and Partial Realizability

When the realizable set R is represented by a BDD, as in [9], it is easy to check whether R = ∅ or R = B m, as this corresponds to the BDD being equal to 0 or 1, respectively. This is less straightforward for a ZDD representation, which

expresses R indirectly by the set of clauses in its CNF representation f0, rather than the set of assignments itself. We say that a CNF specification f(x, ⃗ y⃗) is fully realizable if and only if all a⃗ ∈ B m have some ⃗b ∈ B n so that f(a, ⃗ ⃗b) holds. This corresponds to R = B m. Similarly, we say that f is partially realizable if and only if there is some a⃗ for which there exists some ⃗b so that f(a, ⃗ ⃗b) holds. This corresponds to R ≠ ∅. After computing a ZDD representation of R, we wish to check full and partial realizability over this representation.

Theorem 1. The CNF specification f(x, ⃗ y⃗) is fully realizable if and only if the ZDD for f0 is equivalent to the 0-ZDD.

Proof. The specification f(x, ⃗ y⃗) is fully realizable if and only if the CNF formula f0 representing R is a tautology, which means that every clause of R has both p and ¬p for some variable p, i.e., every clause is a tautology. Tautologies, however, are automatically removed by the Resolution operation, as explained in Section 3.1. Thus, full realizability occurs if and only if the set of clauses is empty, represented by the ZDD 0.

Note that the realizability R is represented by the CNF formula f0 ≡ (∃y1) . . . (∃yn)f, which does not contain any free occurrences of y⃗ variables. We then perform resolution on the x⃗ variables in the same way as we did for the y⃗ variables. Then the original formula is partially realizable if and only if (∃x1)(∃x2) . . .

(∃xm)f0 is true, meaning that resolution does not derive a contradiction. If a contradiction is derived, the resulting ZDD is the terminal 1, representing the empty clause. Otherwise it is the terminal 0.

Theorem 2. The CNF specification f(x, ⃗ y⃗) is partially realizable if and only if the ZDD representing (∃x1)(∃x2) . . . (∃xm)f0 is equivalent to the 0-ZDD.

Proof. Since all variables are existentially quantified, the ZDD must be either the terminal 0 (representing the empty CNF, equivalent to true) or the terminal 1 (representing a CNF with an empty clause, equivalent to false). In the first case, the formula (∃x1) . . . (∃xm)(∃y1) . . . (∃yn)f is true, meaning that there is an assignment that satisfies f(x, ⃗ y⃗), which by definition makes f partially realizable. In the second case, the formula is false, meaning that there is no such assignment, and therefore f is not partially realizable.

### 4 Synthesis Using ZDDs

As described in [9], once we have computed the formulas f1, . . . , fn with the output variables existentially quantified, we can construct the witness gi for variable yi from the formula fi[y1 ↦ g1]. . .[yi−1 ↦ gi−1], after having computed the witnesses g1, . . . , gi−1 for the preceding variables. In [9], two witness functions were presented for variable yi : the default-1 witness fi[y1 ↦ g1]. . .[yi−1 ↦ gi−1][yi ↦ 1] and the default-0 witness (¬fi)[y1 ↦ g1]. . .[yi−1 ↦ gi−1][yi ↦ 0]. In this work, however, we additionally want to ensure that we maintain the CNF form of the specification after substituting g1, . . . , gi−1 into fi , to enable ZDD representation. In this section we show how to construct and substitute witnesses so that the result remains in CNF.

For ZDD-based algorithms, the iterated substitution approach requires more sophistication for the construction of the witnesses, compared to the iteratedsubstitution approach for BDDs. We solve this problem in Section 4.2. As in [9], the resulting witnesses guarantee that f(a, g ⃗ 1(a⃗), . . . , gn(a⃗)) = 1 for all realizable input assignments a⃗ ∈ R.

### 4.1 Witnesses for Single-Dimension Output Variable

As in [9], we start by defining witnesses for the case when there is a single output variable:

Lemma 3.  Then the formulas f − y and ¬f + y are witnesses for the variable y.

Proof. The realizability set, as defined in Section 3.1, is R = {a⃗ ∈ B m ∣ (∃y)f[x⃗ ↦ a⃗] ≡ 1}.

Now we want to show f(a, g ⃗ (a⃗)) = 1, i.e., f[y ↦ g(x⃗)][x⃗ ↦ a⃗] = 1, for both g(x⃗) = f − y and g(x⃗) = ¬f + y .

For g(x⃗) = f − y , since f ≡ f ′ y ∧ (y ∨ f + y ) ∧ ((¬y) ∨ f − y ), we are left to show f[y ↦ f − y ][x⃗ ↦ a⃗] ≡ (f ′ y ∧ (f − y ∨ f + y ) ∧ ((¬f − y ) ∨ f − y ))[x⃗ ↦ a⃗] ≡ 1. By (1) we are only left to show ((¬f − y ) ∨ f − y )[x⃗ ↦ a⃗] ≡ 1, which follows from the left-hand side being a tautology.

Similarly, for g(x⃗) = ¬f + y , we need to show f(a, g ⃗ (a⃗)) = f[y ↦ (¬f + y )][x⃗ ↦ a⃗] ≡ 1. This is equivalent to showing that (f ′ y∧((¬f + y )∨f + y )∧(f + y ∨f − y ))[x⃗ ↦ a⃗] ≡ 1. By (1) we are only left to show ((¬f + y ) ∨ f + y )[x⃗ ↦ a⃗] ≡ 1, a tautology.

Note that the witness f − y is in CNF, while the witness ¬f + y , being the negation of a CNF formula, can be more easily represented in DNF. Note also that these witnesses do not correspond exactly to the default-1 and default-0 witnesses of [9], which would more specifically be equivalent to f − y ∧ f ′ y and ¬(f + y ∧ f ′ y ), respectively. We choose the alternative witnesses because they contain fewer clauses, and thus are more likely to produce a more efficient ZDD representation.

### 4.2 Preserve CNF by Equivalent Witnesses

We now explain how to construct witnesses of multiple output variables. Let fn, . . . , f0 be as defined in Section 3.1. We can then compute a witness for each yi iteratively, as in [9]. Using the f − y witness from Lemma 3, for example, this means gi(x⃗) = (fi[y1 ↦ g1]. . .[yi−1 ↦ gi−1])− yi , where gi is the witness for variable yi .

The substitution fi[y ↦ g], however, is not necessarily in CNF. But Lemma 3 requires that the formula is in CNF in order to extract the next witness. This means that we need to find a way to perform the substitution in a way that the result remains in CNF.

Recall that, since our Resolution operation removes tautological clauses, each variable can only occur in positive or negative form in a clause, but not both. If the witness g is in CNF, e.g., g = f − y , we can substitute this witness in a clause (y∨l1∨l2∨. . .) where y occurs in positive form. The result is a disjunction of the literals l1,l2, . . . and the CNF g = (cl1 ∧ cl2 ∧ . . .). By distribution, we can write this as an equivalent CNF ((cl1 ∨l1 ∨l2 ∨. . .)∧(cl2 ∨l1 ∨l2 ∨. . .)∧. . .). Likewise, if the witness g for y is in DNF, e.g., g = (¬f + y ), then, after the substitution, every clause (¬y ∨ l1 ∨ l2 ∨ . . .) where y appears in negative form can be converted to the CNF (¬(¬(cl1 ∧ cl2 ∧ . . .)) ∨ l1 ∨ l2 ∨ . . .) ≡ ((cl1 ∧ cl2 ∧ . . .) ∨ l1 ∨ l2 ∨ . . .) ≡ ((cl1 ∨ l1 ∨ l2 ∨ . . .) ∧ (cl2 ∨ l1 ∨ l2 ∨ . . .) ∧ . . .).

The problem, therefore, is that if we want the result to be in CNF, CNF witnesses work well for positive occurrences, while DNF witnesses work well for negative occurrences. Thus, as long as we can find an efficient conversion between CNF formulas and their equivalent DNF formulas, we can ensure that the substitution formula fi[y ↦ g] can be written as a CNF. For this purpose, we introduce the Cross operator from [14].

### Definition 2 (Cross operation).

Let S be a family of sets of literals. Then

$$Cross(S) = Minimal\{t \mid \forall s\_i \in S : t \cap s\_i \neq \mathcal{O}\},$$

where

$$Minimal(S) = \{ t \in S \mid \forall s \in S : s \subseteq t \to s = t \} \dots$$

Hence, Cross(S) is a family of sets of literals, such that every set t of literals in Cross(S) has at least a common literal with every set of literals in S. Moreover, every set t in Cross(S) is irredundant [14], meaning they are the smallest possible sets satisfying this property.

Specifically, if S represents a given CNF f, where every set si ∈ S represents a clause and the elements of si are the literals in that clause, then Cross(S) represents the set of smallest possible sets t such that t has at least one common literal with every disjunctive clause of f. Equivalently speaking, Cross(S) collects all t such that every disjunctive clause is satisfied, i.e., it is a collection of all irredundant sets of literals corresponding to irredundant assignments to variables. This further means Cross(S) is a collection of prime implicants of f [6,14], whose disjunction has been proved to be a DNF equivalent to the CNF f. Therefore, whenever a CNF is given, we can construct a set S of sets, where every set in S collects literals in a disjunctive clause of the CNF. Then Cross(S) returns a set of sets representing an equivalent DNF. Conversely, when interpreted as a DNF, Cross(S) is equivalent to S interpreted as a CNF.

By the analysis above, we can extend Definition 2 of the Cross operation to CNF formulas:

Definition 3 (CNF Cross operation).  Let S = {L1, . . . , Lk} be the representation of f as a family of sets. Then,

$$Cross(f) = \bigvee\_{L'\_i \in Crosos(S)} \bigwedge\_{\ell \in L'\_i} \ell$$

Note that Cross(f) is a DNF formula. We can similarly define in an analogous way the Cross of a DNF formula as a CNF formula. We can verify that Cross(f) and f are equivalent:

Lemma 4. For a CNF formula f, Cross(f) ≡ f.

Proof. By analysis above, the set Cross(S) includes elements L ′ i s which are irredundant smallest sets that each has common literal with every set of literals in S. Therefore, every conjunction ⋀`∈L′ i `, or cube, has common literal with every disjunctive clauses in CNF f, and thus every cube has the same boolean values under the same set of truth assignments as a prime implicant [6,21] of CNF f. Then it follows that the DNF Cross(f), as a disjunction of these conjunctions, is logically equivalent to the disjunction of all prime implicants of the CNF f, as proved by previous works [21].

Note that the same result also holds for DNF formulas, following from the fact that Cross(f) ≡ f if and only if ¬Cross(f) ≡ ¬f.

Now we aim to show how to construct witnesses one by one, why this construction is correct, and why this construction is viable. First, if we fix the witness gj = (fi) − yj , and substitute positive and negative occurrences with gj and Cross(gj ) in the CNF formula fi , then the equivalence and CNF form of fi[yj ↦ gj ] can both be preserved. We use the following lemma:

Lemma 5. Let f and g be given as CNF formulas. Then f[y ↦ g] is equivalent to (g ∨ f + y ) ∧ (¬Cross(g) ∨ f − y ) ∧ f ′ y .

Proof.

 By distribution of f + y over clauses in g, and distribution of f − y over clauses in ¬Cross(g), the resulting expression (g ∨ f + y ) ∧ (¬Cross(g) ∨ f − y ) ∧ f ′ y can be converted to CNF form.

Alternatively, we can pick the witness g = ¬f + y , and instead substitute Cross(g) on positive occurrences and g on negative occurrences of y. Similarly, the formula (Cross(g) ∨ f + y ) ∧ (¬g ∨ f − y ) ∧ f ′ y can also be converted to an equivalent CNF. Therefore, the equivalence and CNF form is preserved for fi[yj ↦ gj ], leading to the following corollary.

Corollary 2. Every step in gi(x⃗) = (fi[y1 ↦ g1]. . .[yi−1 ↦ gi−1])− yi can be performed so it returns a CNF formula.

Proof. Corollary 2 follows from Lemma 3, Definition 3, and Lemma 5

Finally, we have the witnesses constructed in this process:

Theorem 3. Let gi(x⃗) = (fi[y1 ↦ g1]. . .[yi−1 ↦ gi−1])− yi for 0 ≤ i ≤ n. Then, gi is a witness for yi in f, for every yi. The same applies if gi(x⃗) = ¬(fi[y1 ↦ g1]. . .[yi−1 ↦ gi−1])+ yi

Proof. Theorem 3 follows from Lemma 5 and Corollary 2.

#### 4.3 Algorithm for Constructing Witnesses

In the last subsection we described how to uses Knuth's Cross operation to facilitate CBF/DNF conversion, enabling the use of iterated substitution. We describe our novel algorithm for synthesis using ZDDs.

We start by presenting the ZDD implementation of Cross function from Definition 2, following [14]:

if ZDD Z is the 1-terminal then return 0-terminal; else if ZDD Z is the 0-terminal then return 1-terminal; else // Zl denotes the ZDD rooted at 0-child of root of Z // Zh denotes the ZDD rooted at 1-child of root of Z Zr = Union(Zl , Zh); Zll = Cross(Zr); Zr = Cross(Zl); Zhh = Difference(Zr, Zll); // Var(Z) denotes the variable at the root node of Z Z ′ = NewZDD(Var(Z), Zll, Zhh); return Z';

#### end

We now explain how to perform the substitution following Lemma 5, where we want to construct a ZDD of f[y ↦ g], where f and g are CNF formulas and y is a variable. Denote the ZDD representation of f as Zf and that of g as Zg. Then we compute the ZDD Cross(Zg) using the algorithm above. Recall that this ZDD represents a DNF formula that is equivalent to g.

To construct a ZDD for the formula in Lemma 5, we need a ZDD for ¬Cross(g). But note that the ZDD for the CNF ¬Cross(g) is equal to the ZDD for the DNF Cross(g) except replacing every positive literal p with the its negative literal ¬p and vice-versa. Therefore, we want to swap p and ¬p in Cross(Zg).

We retrieve the clauses with neither p nor ¬p by

Z1 = Subset0 (Subset0 (Cross(Zg), p),¬p).

Then we swap p with ¬p in every clause where p appears positively:

Z2 = Change(Subset1 (Cross(Zg), p),¬p).

And we swap ¬p with p in every clause where p appears negatively:

Z3 = Change(Subset1 (Cross(Zg),¬p), p).

Finally, taking the union of Z1, Z2 and Z3 gives us the ZDD ¬Cross(Zg) encoding the CNF for the negation of Cross(Zg).

Let Z + y , Z − y and Z ′ y be the ZDDs for f + y , f − y and f ′ y , respectively, constructed as described in Section 3.1. We compute the ZDDs for (g∨f + y ) and (¬Cross(g)∨ f − y ) by ClauseDistribution(Zg, Z+ y ) and ClauseDistribution(¬Cross(Zg), Z− y ), respectively. We then take the Union of these two ZDDs and Z ′ y to get the ZDD for (g ∨ f + y ) ∧ (¬Cross(g) ∨ f − y ) ∧ f ′ y , which is exactly the ZDD for f[y ↦ g] by Lemma 5.

### 5 Experimental Evaluations

### 5.1 Experimental Methodology and and Setting

We perform a comparison between our ZDD-based synthesizer, ZSynth, and the tool RSynth described by [9], using challenging ΠP 2 benchmarks from the QBFEVAL 2016 data set [18], the latest QBFEVAL set that includes a 2QBF (forall-exists) track, which is the format our benchmarks require. Each benchmark ran for 24 hours on Rice University's NOTS cluster with 64G RAM size. We focus our comparison on the Fixpoint Detection, MutexP, and QShifter benchmark families, omitting those families that are either too easy or too hard to solve for both tools, namely, the Tree, Ranking Functions, Reduction Finding, and Sorting Networks families [18]. For those families, either both tools solved all instances or none. Of these omitted benchmark families, Tree is very simple and is solved very quickly by both tools, while the others could be synthesized by neither tool. therefore we choose to focus on the three families that provide an interesting comparison. Fixpoint Detection, MutexP and QShifter have, respectively, 146, 7, and 6 instances.

For each tool we evaluate both total time and peak memory consumption for compilation, realizability, and synthesis, as well as the DD size for the original formula in each symbolic representation. We use the maximum cardinality search (MCS) heuristic [23] to determine the ordering of variables in both ZDDs and BDDs.Due to restrictions on available time and space resources, some benchmarks show out-of-time and out-of-memory failures. We measure the performance of both tools on the benchmarks that are solved. The experimental evaluations conclude that the ZDD-based approach is complementary to the BDD-based approach.

### 5.2 Compilation Time and Size of Diagram Representing Original Formula

We first compare the performance of CNF compilation into ZDDs and BDDs, following the first research question proposed in Section 1. The log-scale bar plot in Fig. 1 presents compilation time for the benchmarks from the selection families, per Section 5.1. The size of the bars representing each formula is proportional to the compilation time.

The compilation into a ZDD takes polynomial (at most quadratic) time, because paths in the ZDD correspond to clauses, and therefore the size of the ZDD is always linear in the size of the formula. In contrast, the compilation into a BDD can be exponential, because paths in a BDD correspond to assignments, and therefore the number of paths can be exponential. The advantage of ZDDs as a compact representation is consistent with our conjecture. Across all benchmark families in QBFEVAL'16, compilation into ZDDs takes less time and space than BDDs in most cases.

It is worth noting that we construct here the ZDD representation of the CNF formulas by adding one clause at a time using the Union operator. Compilation could be further optimized by using a divide-and-conquer approach, where we split the set of clauses in half, construct ZDDs for each half recursively, and then take their union.

Fig. 1: Compilation time of the CNF: red = BDD, blue = ZDD

#### 5.3 Realizability Time

The plot in Fig. 2 summarizes for each family the time spent on constructing the realizability set and checking partial and full realizability. The dashed lines in red illustrate RSynth results, while the solid lines in dark blue with the same shapes show ZSynth results. As each solvers have the families where it has an advantage in, we note how many instances of each family each solver is able to solve within a given time. We include data for all benchmarks that completed the

Fig. 2: Percentage solved for realizability within a given timeout. Dashed red = BDD, solid blue = ZDD.

realizability phase. The graph plots the percentage of benchmarks in each family that RSynth and ZSynth complete for a given timeout, with 100% meaning that all instances of that family were solved.

We see from Fig. 2 that RSynth solves more cases of the Fixpoint Detection family, and does so faster than ZSynth. Most of the cases it solves are completed in under 10ms. On the other hand, ZSynth has the advantage in the QShifter and MutexP families, for which it is able to solve more cases in a shorter time. Therefore, ZSynth and RSynth each performs better on different families of benchmarks. This allows us to answer the second research question proposed in Section 1 with the observation that neither approach dominates across the board, rather realizability performance is dependent on the benchmark family. As we see below in Section 5.4, these general results also extend to end-to-end synthesis.

### 5.4 End-to-End Time and Peak Memory

Our observations for end-to-end synthesis time–including compilation, realizability, and witness construction–are plotted in Fig. 3. Similarly to realizability time, the total end-to-end synthesis time shows strongly family-dependent results. Both ZSynth and RSynth display better relative performance on the same families as they did for realizability. In families where ZSynth solves more instances, including QShifter and MutexP, ZSynth also takes less time in most

Fig. 3: Percentage solved end-to-end within a given timeout. Dashed red = BDD, solid blue = ZDD.

cases, and vice-versa for those families where RSynth solves more benchmarks end-to-end.

We observed in our experiments that memory and time were generally correlated, meaning that benchmarks that took more time also consumed more memory. This is expected when dealing with algorithms based on decision diagrams, since the biggest factor that impacts the performance of such algorithms is diagram size. In practice, memory comparison between RSynth and ZSynth in compilation, realizability and witness construction have similar patterns as the time comparison. Even if ZDDs have an advantage in representing the initial specification, the overall memory consumption for realizability and synthesis is, similarly to running time, largely dependent on the benchmark family.

### 5.5 Scalable Benchmarks Show ZDD has Slower Growing Demands of Time and Space

To analyze the scalability of ZDDs in relation to BDDs, as per the fifth research question in Section 1, we take a closer look at the running time and node counts of ZSynth and RSynth in the benchmarks of the QShifter family. All benchmarks in this family follow the same structure, just scaled based on a numerical parameter. For a parameter n, qshifter\_n has 2 2n+1 clauses, 2 n + n input variables and 2 n output variables, so we expect to see exponential trends in the measured values.

The results can be found in Fig. 4, which considers only QShifter because it can be scaled based on a parameter, and RSynth did not solve enough instances of MutexP to have an interesting scalability comparison. Since RSynth solves only up to the smallest instances in the QShifter family, we use the maximal time limit, illustrated by the "X" in the plot not connected to any line, as a conservative underestimation for the running time of further instances. (Therefore, the compilation, realizability and end-to-end times for RSynth in qshifter\_5 must be higher than the "X" mark.) As QShifter benchmarks are regular in their constructions, we can observe the trend of the exponent.

The results for RSynth, both for time and number of nodes, always has a steeper slope in the parameter n. Since the graph is in log scale, straight lines represent an exponential increase, and the slope represents the coefficient of the exponent. Therefore, although both ZSynth and RSynth grow exponentially, in both time and space, ZSynth is more efficient by an exponential factor.

These results suggest that there are families for which we can expect ZDD synthesizers to require significantly fewer resources in time and space as the size of the formulas grows. The QShifter family is one example of a family where the ZDD algorithm performs better by an exponential factor.

Fig. 4: Scalable family evaluations: dashed red = BDD, solid blue = ZDD.

### 5.6 Overall Comparison

As explained in Section 5.1, we focus on evaluating the synthesizers on the Fixpoint Detection, QShifter, and MutexP families of benchmarks [18]. ZSynth

Table 1: Percentage of end-to-end completed instances in each family. Benchmark Family Name RSynth (BDD) ZSynth (ZDD)

shows clear time and space advantages on the MutexP and QShifter families, while RSynth performs better in the Fixpoint Detection family. In Table 1, we show how much of each family either tool was able to solve.

Next, we summarize the overall results of our experimental performance comparison. In families where ZDD completed more instances end-to-end, we can see that ZDD has better performance in all bases of comparison, including compilation, realizability, and end-to-end time, as well as diagram node count for the original formula and peak node count. Additionally, Section 5.5 shows that there exist families of scalable benchmarks for which the time and space demands of ZDDs grow more slowly than BDDs by an exponential factor, as illustrated by the smaller slope in Fig. 4.

Even in the Fixpoint Detection family, where BDDs solve more instances, ZDDs show advantages in compilation time, initial diagram size, and smaller scaling slopes in time and space. In realizability and overall synthesis performance, neither our ZDD-based algorithm nor the BDD-based algorithm dominates across the board, each performing better in those families where it can solve more instances.

### 6 Conclusion

We conclude that ZDD-based algorithms are competitive with those based on BDDs, and both have their place in a portfolio of solvers for boolean synthesis. Since both BDDs and ZDDs can be converted to circuits, we advocate that an industrial solver would benefit from both approaches. In CNF-specified boolean-synthesis problems, BDD and ZDD are orthogonal approaches, and circumstances exist where each one of the solvers shows leading performance. For this type of problems, our portfolio advocates a multi-engine approach that is inclusive of both approaches.

As most tools for QBF solving and synthesis solving handle the input formula monolithically, future research based on this work includes an exploration of partitioning of variables [8] and factored synthesis [23] in the context of ZDDs. Another direction is to explore the usage of ZDD-based techniques in the context of temporal synthesis, cf. [24].

### References

1. Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What's hard about Boolean functional synthesis? In: Proc. 30th Int'l Conf. on Computer Aided Verification, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 251–269. Springer (2018). https://doi.org/10.1007/978-3-319-96145-3\_14, https://doi.org/ 10.1007/978-3-319-96145-3\_14

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Verification

## **Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems**

André Greiner-Petter1 () , Howard S. Cohl2 , Abdou Youssef 2*,*3 , Moritz Schubotz1*,*4 , Avi Trost5 , Rajen Dey6 , Akiko Aizawa7 , and Bela Gipp1

1 University of Wuppertal, Wuppertal, Germany,

<EMAIL_ADDRESS>
2 National Institute of Standards and Technology,

Mission Viejo, CA, U.S.A<EMAIL_ADDRESS>
3 George Washington University, Washington, D.C., U.S.A<EMAIL_ADDRESS>
4 FIZ Karlsruhe, Berlin, Germany<EMAIL_ADDRESS>
5 Brown University, Providence, RI, U.S.A<EMAIL_ADDRESS>
6 University of California Berkeley, Berkeley, CA, U.S.A<EMAIL_ADDRESS>
7 National Institute of Informatics, Tokyo, Japan<EMAIL_ADDRESS>
**Abstract.** Digital mathematical libraries assemble the knowledge of years of mathematical research. Numerous disciplines (e.g., physics, engineering, pure and applied mathematics) rely heavily on compendia gathered findings. Likewise, modern research applications rely more and more on computational solutions, which are often calculated and verified by computer algebra systems. Hence, the correctness, accuracy, and reliability of both digital mathematical libraries and computer algebra systems is a crucial attribute for modern research. In this paper, we present a novel approach to verify a digital mathematical library and two computer algebra systems with one another by converting mathematical expressions from one system to the other. We use our previously developed conversion tool (referred to as LACAST) to translate formulae from the NIST Digital Library of Mathematical Functions to the computer algebra systems Maple and Mathematica. The contributions of our presented work are as follows: (1) we present the most comprehensive verification of computer algebra systems and digital mathematical libraries with one another; (2) we significantly enhance the performance of the underlying translator in terms of coverage and accuracy; and (3) we provide open access to translations for Maple and Mathematica of the formulae in the NIST Digital Library of Mathematical Functions.

**Keywords:** Presentation to Computation, LaCASt, LaTeX, Semantic La-TeX, Computer Algebra Systems, Digital Mathematical Library

### **1 Introduction**

Digital Mathematical Libraries (DML) gather the knowledge and results from thousands of years of mathematical research. Even though pure and applied mathematics are precise disciplines, gathering their knowledge bases over many years results in

issues which every digital library shares: consistency, completeness, and accuracy. Likewise, Computer Algebra Systems (CAS)8 play a crucial role in the modern era for pure and applied mathematics, and those fields which rely on them. CAS can be used to simplify, manipulate, compute, and visualize mathematical expressions. Accordingly, modern research regularly uses DML and CAS together. Nonetheless, DML [7,14] and CAS [1,20,11] are not exempt from having bugs or errors. Durán et al. [11] even raised the rather dramatic question: "*can we trust in [CAS]*?"

Existing comprehensive DML, such as the Digital Library of Mathematical Functions (DLMF) [10], are consistently updated and frequently corrected with errata9 . Although each chapter of the DLMF has been carefully written, edited, validated, and proofread over many years, errors still remain. Maintaining a DML, such as the DLMF, is a laborious process. Likewise, CAS are eminently complex systems, and in the case of commercial products, often similar to black boxes in which the magic (i.e., the computations) happens in opaque private code [11]. CAS, especially commercial products, are often exclusively tested internally during development.

An independent examination process can improve testing and increase trust in the systems and libraries. Hence, we want to elaborate on the following research question.

How can digital mathematical libraries and computer algebra systems be utilized to improve and verify one another?

Our initial approach for answering this question is inspired by our previous studies on translating DLMF equations to CAS [7]. In order to verify a translation tool from a specific LATEX dialect to Maple10. , we performed *symbolic* and *numeric* evaluations on equations from the DLMF. Our approach presumes that a proven equation in a DML must be also valid in a CAS. In turn, a disparity in between the DML and CAS would lead to an issue in the translation process. However, assuming a correct translation, a disparity would also indicate an issue either in the DML source or the CAS implementation. In turn, we can take advantage of the same approach to improve and even verify DML with CAS and vice versa. Unfortunately, previous efforts to translate mathematical expressions from various formats, such as LATEX [8,14,29], MathML [31], or OpenMath [18,30], to CAS syntax have shown that the translation will be the most critical part of this verification approach.

In this paper, we elaborate on the feasibility and limitations of the translation approach from DML to CAS as a possible answer to our research question. We further focus on the DLMF as our DML and the two general-purpose CAS Maple and Mathematica for this first study. This relatively sharp limitation is necessary in order to analyze the capabilities of the underlying approach to verify commercial CAS

8 In the sequel, the acronyms CAS and DML are used, depending on the context, interchangeably with their plurals.

9 https://dlmf.nist.gov/errata/ [accessed 09/01/2021]

10 The mention of specific products, trademarks, or brand names is for purposes of identification only. Such mention is not to be interpreted in any way as an endorsement or certification of such products or brands by the National Institute of Standards and Technology, nor does it imply that the products so identified are necessarily the best available for the purpose. All trademarks mentioned herein belong to their respective owners.

and large DML. The DLMF uses semantic macros internally in order to disambiguate mathematical expressions [27,35]. These macros help to mitigate the open issue of retrieving sufficient semantic information from a context to perform translations to formal languages [31,14]. Further, the DLMF and general-purpose CAS have a relatively large overlap in coverage of special functions and orthogonal polynomials. Since many of those functions play a crucial role in a large variety of different research fields, we focus in this study mainly on these functions. Lastly, we will take our previously developed translation tool LACAST [8,14] as the baseline for translations from the DLMF to Maple. In this successor project, we focus on improving LACAST to minimize the negative effect of wrong translations as much as possible for our study. In the future, other DML and CAS can be improved and verified following the same approach by using a different translation approach depending on the data of the DML, e.g., MathML [31] or OpenMath [18].

In particular, in this paper, we fix the majority of the remaining issues of LACAST [7], which allows our tool to translate twice as many expressions from the DLMF to the CAS as before. Current extensions include the support for the mathematical operators: sum, product, limit, and integral, as well as overcoming semantic hurdles associated with Lagrange (prime) notations commonly used for differentiation. Further, we extend its support to include Mathematica using the freely available *Wolfram Engine for Developers* (WED)11 (hereafter, with Mathematica, we refer to the WED). These improvements allow us to cover a larger portion of the DLMF, increase the reliability of the translations via LACAST, and allow for comparisons between two major generalpurpose CAS for the first time, namely Maple and Mathematica. Finally, we provide open access to all the results contained within this paper, including all translations of DLMF formulae, an endpoint to LACAST12, and the full source code of LACAST13 .

The paper is structured as follows. Section 2 explains the data in the DLMF. Section 3 focus on the improvements of LACAST that had been made to make the translation as comprehensive and reliable as possible for the upcoming evaluation. Section 4 explains the symbolic and numeric evaluation pipeline. Since Cohl et al. [7] only briefly sketched the approach of a numeric evaluation, we will provide an in-depth discussion of that process in Section 4. Subsequently, we analyze the results in Section 5. Finally, we conclude the findings and provide an outlook for upcoming projects in Section 6.

#### **1.1 Related Work**

Existing verification techniques for CAS often focus on specific subroutines or functions [26,20,5,12,6,25,21,17], such as a specific theorems [23], differential equations [19], or the implementation of the math.h library [24]. Most common are verification approaches that rely on intermediate verification languages [5,20,21,19,17], such as *Boogie* [25,2] or *Why3* [21,4], which, in turn, rely on proof assistants and theorem provers, such as *Coq* [5,3], *Isabelle* [19,28], or *HOL Light* [20,16,17]. Kaliszyk and Wiedijk [20] proposed on entire new CAS which is built on top of the proof assistant HOL Light so that each simplification step can be proven by the underlying

11 https://www.wolfram.com/engine/ [accessed 09/01/2021]

12 https://lacast.wmflabs.org/ [accessed 01/01/2022]

13 https://github.com/ag-gipp/LaCASt [accessed 04/01/2022]

architecture. Lewis and Wester [26] manually compared the symbolic computations on polynomials and matrices with seven CAS. Aguirregabiria et al. [1] suggested to teach students the known traps and difficulties with evaluations in CAS instead to reduce the overreliance on computational solutions.

Cohl et al. [7] developed the aforementioned translation tool LACAST, which translates expressions from a semantically enhanced LATEX dialect to Maple. By evaluating the performance and accuracy of the translations, we were able to discover a sign-error in one the DLMF's equations [7]. While the evaluation was not intended to verify the DLMF, the translations by the rule-based translator LACAST provided sufficient robustness to identify issues in the underlying library. To the best of our knowledge, besides this related evaluation via LACAST, there are no existing libraries or tools that allow for automatic verification of DML.

### **2 The DLMF dataset**

In the modern era, most mathematical texts (handbooks, journal publications, magazines, monographs, treatises, proceedings, etc.) are written using the document preparation system LATEX. However, the focus of LATEX is for precise control of the rendering mechanics rather than for a semantic description of its content. In contrast, CAS syntax is coercively unambiguous in order to interpret the input correctly. Hence, a transformation tool from DML to CAS must disambiguate mathematical expressions. While there is an ongoing effort towards such a process [32,22,34,13,36,33], there is no reliable tool available to disambiguate mathematics sufficiently to date.

The DLMF contains numerous relations between functions and many other properties. It is written in LATEX but uses specific semantic macros when applicable [35]. These semantic macros represent a unique function or polynomial defined in the DLMF. Hence, the semantic LATEX used in the DLMF is often unambiguous. For a successful evaluation via CAS, we also need to utilize all requirements of an equation, such as constraints, domains, or substitutions. The DLMF provides this additional data too and generally in a machine-readable form [35]. This data is accessible via the i-boxes (information boxes next to an equation marked with the icon ). If the information is not given in the attached i-box or the information is incorrect, the translation via LACAST would fail. The i-boxes, however, do not contain information about branch cuts (see Section B) or constraints. Constraints are accessible if they are directly attached to an equation. If they appear in the text (or even a title), LACAST cannot utilize them. The test dataset, we are using, was generated from DLMF Version 1.1.3 (2021-09-15) and contained 9*,*977 formulae with 1*,*505 defined symbols, 50*,*590 used symbols, 2*,*691 constraints, and 2*,*443 warnings for non-semantic expressions, i.e., expressions without semantic macros [35]. Note that the DLMF does not provide access to the underlying LATEX source. Therefore, we added the source of every equation to our result dataset.

### **3 Semantic LATEX to CAS translation**

The aforementioned translator LACAST was developed by Cohl and Greiner-Petter et al. [8,7,14]. They reported a coverage of 58.8% translations for a manually selected

part of the DLMF to the CAS Maple. This version of LACAST serves as a baseline for our improvements. In order to verify their translations, they used symbolic and numeric evaluations and reported a success rate of ∼16% for symbolic and ∼12% for numeric verifications.

Evaluating the baseline on the entire DLMF result in a coverage of only 31.6%. Hence, we first want to increase the coverage of LACAST on the DLMF. To achieve this goal, we first increasing the number of translatable semantic macros by manually defining more translation patterns for special functions and orthogonal polynomials. For Maple, we increased the number from 201 to 261. For Mathematica, we define 279 new translation patterns which enables LACAST to perform translations to Mathematica. Even though the DLMF uses 675 distinguished semantic macros, we cover ∼70% of all DLMF equations with our extended list of translation patterns (see Zipf's law for mathematical notations [15]). In addition, we implemented rules for translations that are applicable in the context of the DLMF, e.g., ignore ellipsis following floating-point values or \choose always refers to a binomial expression. Finally, we tackle the remaining issues outlined by Cohl et al. [7] which can be categorized into three groups: (i) expressions of which the arguments of operators are not clear, namely sums, products, integrals, and limits; (ii) expressions with prime symbols indicating differentiation; and (iii) expressions that contain ellipsis. While we solve some of the cases in Group (iii) by ignoring ellipsis following floating-point values, most of these cases remain unresolved. In the following, we elaborate our solutions for (i) in Section 3.1 and (ii) in Section 3.2.

#### **3.1 Parse sums, products, integrals, and limits**

Here we consider common notations for the sum, product, integral, and limit operators. For these operators, one may consider mathematically essential operator metadata (MEOM). For all these operators, the MEOM includes *argument(s)* and *bound variable(s)*. The operators act on the arguments, which are themselves functions of the bound variable(s). For sums and products, the bound variables are referred to as *indices*. The bound variables for integrals14 are called *integration variables*. For limits, the bound variables are continuous variables (for limits of continuous functions) and indices (for limits of sequences). For integrals, MEOM include precise descriptions of regions of integration (e.g., piecewise continuous paths/intervals/regions). For limits, MEOM include limit points (e.g., points in R *n* or C *n* for *n*∈N), as well as information related to whether the limit to the limit point is independent or dependent on the direction in which the limit is taken (e.g., one-sided limits).

For a translation of mathematical expressions involving the LATEX commands \sum, \int, \prod, and \lim, we must extract the MEOM. This is achieved by (a) determining the argument of the operator and (b) parsing corresponding subscripts, superscripts, and arguments. For integrals, the MEOM may be complicated, but certainly contains the argument (function which will be integrated), bound (integration) variable(s) and details related to the region of integration. Bound variable extraction is usually straightforward since it is usually contained within a differential expression

14 The notion of integrals includes: antiderivatives (indefinite integrals), definite integrals, contour integrals, multiple (surface, volume, etc.) integrals, Riemannian volume integrals, Riemann integrals, Lebesgue integrals, Cauchy principal value integrals, etc.

(infinitesimal, pushforward, differential 1-form, exterior derivative, measure, etc.), e.g., d*x*. Argument extraction is less straightforward since even though differential expressions are often given at the end of the argument, sometimes the differential expression appears in the numerator of a fraction (e.g., R *f*(*x*)d*x g*(*x*) ). In which case, the argument is everything to the right of the \int (neglecting its subscripts and superscripts) up to and including the fraction involving the differential expression (which may be replaced with 1). In cases where the differential expression is fully to the right of the argument, then it is a *termination symbol*. Note that some scientists use an alternate notation for integrals where the differential expression appears immediately to the right of the integral, e.g., R d*xf*(*x*). However, this notation does not appear in the DLMF. If such notations are encountered, we follow the same approach that we used for sums, products, and limits (see Section 3.1).

**Extraction of variables and corresponding MEOM** The subscripts and superscripts of sums, products, limits, and integrals may be different for different notations and are therefore challenging to parse. For integrals, we extract the bound (integration) variable from the differential expression. For sums and products, the upper and lower bounds may appear in the subscript or superscript. Parsing subscripts is comparable with the problem of parsing constraints [7] (which are often not consistently formulated). We overcame this complexity by manually defining patterns of common constraints and refer to them as blueprints. This blueprint pattern approach allows LACAST to identify the MEOM in the sub- and superscripts. A more detailed explanations with examples about the blueprints is available in the Appendix A15 .

**Identification of operator arguments** Once we have extracted the bound variable for sums, products, and limits, we need to determine the end of the argument. We analyzed all sums in the DLMF and developed a heuristic that covers all the formulae in the DLMF and potentially a large portion of general mathematics. Let *x* be the extracted bound variable. For sums, we consider a summand as a part of the argument if (I) it is the very first summand after the operation; or (II) *x* is an element of the current summand; or (III) *x* is an element of the following summand (subsequent to the current summand) and there is no termination symbol between the current summand and the summand which contains *x* with an equal or lower depth according to the parse tree (i.e., closer to the root). We consider a summand as a single logical construct since addition and subtraction are granted a lower operator precedence than multiplication in mathematical expressions. Similarly, parentheses are granted higher precedence and, thus, a sequence wrapped in parentheses is part of the argument if it obeys the rules (I-III). Summands, and such sequences, are always entirely part of sums, products, and limits or entirely not.

A termination symbol always marks the end of the argument list. Termination symbols are relation symbols, e.g., =, ≠ , ≤, closing parentheses or brackets, e.g., ), ], or *>*, and other operators with MEOMs, if and only if, they define the same bound variable. If *x* is part of a subsequent operation, then the following operator

15 The Appendix is available at https://arxiv.org/abs/2201.09488.

is considered as part of the argument (as in (II)). However, a special condition for termination symbols is that it is only a termination symbol for the current chain of arguments. Consider a sum over a fraction of sums. In that case, we may reach a termination symbol within the fraction. However, the termination symbol would be deeper inside the parse tree as compared to the current list of arguments. Hence, we used the depth to determine if a termination symbol should be recognized or not. Consider an unusual notation with the binomial coefficient as an example

$$\sum\_{k=0}^{n} \binom{n}{k} = \sum\_{k=0}^{n} \frac{\prod\_{m=1}^{n} m}{\prod\_{m=1}^{k} m \prod\_{m=1}^{n-k} m}. \tag{1}$$

This equation contains two termination symbols, marked red and green. The red termination symbol = is obviously for the first sum on the left-hand side of the equation. The green termination symbol Q terminates the product to the left because both products run over the same bound variable *m*. In addition, none of the other = signs are termination symbols for the sum on the right-hand side of the equation because they are deeper in the parse tree and thus do not terminate the sum.

Note that varN in the blueprints also matches multiple bound variable, e.g., P *m,k*∈*A*. In such cases, *x* from above is a list of bound variables and a summand is part of the argument if one of the elements of *x* is within this summand. Due to the translation, the operation will be split into two preceding operations, i.e., P *m,k*∈*A* becomes P *m*∈*A* P *k*∈*A*. Figure 1 shows the extracted arguments for some example sums. The same rules apply for extraction of arguments for products and limits.

Fig. 1: Example argument identifications for sums.

#### **3.2 Lagrange's notation for differentiation and derivatives**

Another remaining issue is the Lagrange (prime) notation for differentiation, since it does not outwardly provide sufficient semantic information. This notation presents two challenges. First, we do not know with respect to which variable the differentiation should be performed. Consider for example the Hurwitz zeta function *ζ*(*s,a*) [10, §25.11]. In the case of a differentiation *ζ* ′ (*s,a*), it is not clear if the function should be differentiated with respect to *s* or *a*. To remedy this issue, we analyzed all formulae in the DLMF which use prime notations and determined which variables (slots) for which functions represent the variables of the differentiation. Based on our analysis, we extended the translation patterns by meta information for semantic macros according to the slot of differentiation. For instance, in the case of the Hurwitz zeta function, the first slot is the slot for prime differentiation, i.e., *ζ* ′ (*s,a*)= d d*s ζ*(*s,a*). The identified variables of differentiations for the special functions in the DLMF can be considered to be the standard slots of differentiations, e.g., in other DML, *ζ* ′ (*s,a*) most likely refers to d d*s ζ*(*s,a*).

The second challenge occurs if the slot of differentiation contains complex expressions rather than single symbols, e.g., *ζ* ′ (*s* 2 *,a*). In this case, *ζ* ′ (*s* 2 *,a*) = d d(*s* 2) *ζ*(*s* 2 *,a*) instead of d d*s ζ*(*s* 2 *,a*). Since CAS often do not support derivatives with respect to complex expressions, we use the inbuilt substitution functions16 in the CAS to overcome this issue. To do so, we use a temporary variable temp for the substitution. CAS perform substitutions from the inside to the outside. Hence, we can use the same temporary variable temp even for nested substitutions. Table 1 shows the translation performed for *ζ* ′ (*s* 2 *,a*). CAS may provide optional arguments to calculate the derivatives for certain special functions, e.g., Zeta(n,z,a) in Maple for the *n*-th derivative of the Hurwitz zeta function. However, this shorthand notation is generally not supported (e.g., Mathematica does not define such an optional parameter). Our substitution approach is more lengthy but also more reliable. Unfortunately, lengthy expressions generally harm the performance of CAS, especially for symbolic manipulations. Hence, we have a genuine interest in keeping translations short, straightforward and readable. Thus, the substitution translation pattern is only triggered if the variable of differentiation is not a single identifier. Note that this substitution only triggers on semantic macros. Generic functions, including prime notations, are still skipped.

A related problem to MEOM of sums, products, integrals, limits, and differentiations are the notations of derivatives. The semantic macro for derivatives \deriv{w}{x} (rendered as d*w* d*x* ) is often used with an empty first argument to render the function behind the derivative notation, e.g., \deriv{}{x}\sin@{x} for d d*x* sin *x*. This leads to the same problem we faced above for identifying MEOMs. In this case, we use the same heuris-

Table 1: Example translations for the prime derivative of the Hurwitz zeta function with respect to *s* 2 .

tic as we did for sums, products, and limits. Note that derivatives may be written following the function argument, e.g., sin(*x*) d d*x* . If we are unable to identify any following summand that contains the variable of differentiation before we reach a termination symbol, we look for arguments prior to the derivative according to the heuristic (I-III).

**Wronskians** With the support of prime differentiation described above, we are also able to translate the Wronskian [10, (1.13.4)] to Maple and Mathematica. A translation requires one to identify the variable of differentiation from the elements of the Wronskian, e.g., *z* for W {Ai(*z*)*,*Bi(*z*)} from [10, (9.2.7)]. We analyzed all Wronskians in the DLMF and discovered that most Wronskians have a special

16 Note that Maple also support an evaluation substitution via the two-argument eval function. Since our substitution only triggers on semantic macros, we only use subs if the function is defined in Maple. In turn, as far as we know, there is no practical difference between subs and the two-argument eval in our case.

function in its argument—such as the example above. Hence, we can use our previously inserted metadata information about the slots of differentiation to extract the variable of differentiation from the semantic macros. If the semantic macro argument is a complex expression, we search for the identifier in the arguments that appear in both elements of the Wronskian. For example, in W {Ai(*z a* )*,ζ*(*z* 2 *,a*)}, we extract *z* as the variable since it is the only identifier that appears in the arguments *z a* and *z* 2 of the elements. This approach is also used when there is no semantic macro involved, i.e., from W {*z a ,z*2} we extract *z* as well. If LACAST extracts multiple candidates or none, it throws a translation exception.

### **4 Evaluation of the DLMF using CAS**

Fig. 2: The workflow of the evaluation engine and the overall results. Errors and abortions are not included. The generated dataset contains 9*,*977 equations. In total, the case analyzer splits the data into 10*,*930 cases of which 4*,*307 cases were filtered. This sums up to a set of 6*,*623 test cases in total.

For evaluating the DLMF with Maple and Mathematica, we follow the same approach as demonstrated in [7], i.e., we symbolically and numerically verify the equations in the DLMF with CAS. If a verification fails, symbolically and numerically, we identified an issue either in the DLMF, the CAS, or the verification pipeline. Note that an issue does not necessarily represent errors/bugs in the DLMF, CAS, or LACAST (see the discussion about branch cuts in Section B). Figure 2 illustrates the pipeline of the evaluation engine. First, we analyze every equation in the DLMF (hereafter referred to as test cases). A case analyzer splits multiple relations in a single line into multiple test cases. Note that only the adjacent relations are considered, i.e., with *f*(*z*)=*g*(*z*)=*h*(*z*), we generate two test cases *f*(*z*)=*g*(*z*) and *g*(*z*)=*h*(*z*) but not *f*(*z*)=*h*(*z*). In addition, expressions with ± and ∓ are split accordingly, e.g., *i* ±*i*=e∓*π/*2 [10, (4.4.12)] is split into *i* +*i*=e−*π/*2 and *i* −*i*=e+*π/*2 . The analyzer utilizes the attached additional information in each line, i.e., the URL in the DLMF, the used and defined symbols, and the constraints. If a used symbol is defined elsewhere in the DLMF, it performs substitutions. For example, the multi-equation [10, (9.6.2)] is split into six test cases and every *ζ* is replaced by 2 3 *z* 3*/*2 as defined in [10, (9.6.1)]. The substitution is performed on the parse tree of expressions [14]. A definition is

only considered as such, if the defining symbol is identical to the equation's left-hand side. That means, *z* = (3 2 *ζ*) 3*/*2 [10, (9.6.10)] is not considered as a definition for *ζ*. Further, semantic macros are never substituted by their definitions. Translations for semantic macros are exclusively defined by the authors. For example, the equation [10, (11.5.2)] contains the Struve **K***ν*(*z*) function. Since Mathematica does not contain this function, we defined an alternative translation to its definition **H***ν*(*z*)−*Yν*(*z*) in [10, (11.2.5)] with the Struve function **H***ν*(*z*) and the Bessel function of the second kind *Yν*(*z*), because both of these functions are supported by Mathematica. The second entry in Table 3 in the Appendix D shows the translation for this test case.

Next, the analyzer checks for additional constraints defined by the used symbols recursively. The mentioned Struve **K***ν*(*z*) test case [10, (11.5.2)] contains the Gamma function. Since the definition of the Gamma function [10, (5.2.1)] has a constraint ℜ*z >*0, the numeric evaluation must respect this constraint too. For this purpose, the case analyzer first tries to link the variables in constraints to the arguments of the functions. For example, the constraint ℜ*z >*0 sets a constraint for the first argument *z* of the Gamma function. Next, we check all arguments in the actual test case at the same position. The test case contains *Γ*(*ν*+1*/*2). In turn, the variable *z* in the constraint of the definition of the Gamma function ℜ*z >*0 is replaced by the actual argument used in the test case. This adds the constraint ℜ(*ν*+1*/*2)*>*0 to the test case. This process is performed recursively. If a constraint does not contain any variable that is used in the final test case, the constraint is dropped.

In total, the case analyzer would identify four additional constraints for the test case [10, (11.5.2)]. Table 3 in the Appendix D shows the applied constraints (including the directly attached constraint ℜ*z >*0 and the manually defined global constraints from Figure 3). Note that the constraints may contain variables that do not appear in the actual test case, such as ℜ*ν*+*k*+1*>*0. Such constraints do not have any effect on the evaluation because if a constraint cannot be computed to true or false, the constraint is ignored. Unfortunately, this recursive loading of additional constraints may generate impossible conditions in certain cases, such as |*Γ*(*iy*)| [10, (5.4.3)]. There are no valid real values of *y* such that ℜ(*iy*)*>*0. In turn, every test value would be filtered out, and the numeric evaluation would not verify the equation. However, such cases are the minority and we were able to increase the number of correct evaluations with this feature.

To avoid a large portion of incorrect calculations, the analyzer filters the dataset before translating the test cases. We apply two filter rules to the case analyzer. First, we filter expressions that do not contain any semantic macros. Due to the limitations of LACAST, these expressions most likely result in wrong translations. Further, it filters out several meaningless expressions that are not verifiable, such as *z* = *x* in [10, (4.2.4)]. The result dataset flag these cases with '*Skipped - no semantic math*'. Note that the result dataset still contains the translations for these cases to provide a complete picture of the DLMF. Second, we filter expressions that contain ellipsis17 (e.g., \cdots), approximations, and asymptotics (e.g., O(*z* 2 )) since those expressions cannot be evaluated with the proposed approach. Further, a definition is skipped if it is not a definition of a semantic macro, such as [10, (2.3.13)], because definitions without

17 Note that we filter out ellipsis (e.g., \cdots) but not single dots (e.g., \cdot).

an appropriate counterpart in the CAS are meaningless to evaluate. Definitions of semantic macros, on the other hand, are of special interest and remain in the test set since they allow us to test if a function in the CAS obeys the actual mathematical definition in the DLMF. If the case analyzer (see Figure 2) is unable to detect a relation, i.e., split an expression on *<*, ≤, ≥, *>*, =, or ≠ , the line in the dataset is also skipped because the evaluation approach relies on relations to test. After splitting multi-equations (e.g., ±, ∓, *a* = *b* = *c*), filtering out all non-semantic expressions, non-semantic macro definitions, ellipsis, approximations, and asymptotics, we end up with 6*,*623 test cases in total from the entire DLMF.

After generating the test case with all constraints, we translate the expression to the CAS representation. Every successfully translated test case is then symbolically verified, i.e., the CAS tries to simplify the difference of an equation to zero. Nonequation relations simplifies to Booleans. Non-simplified expressions are verified numerically for manually defined test values, i.e., we calculate actual numeric values for both sides of an equation and check their equivalence.

#### **4.1 Symbolic Evaluation**

The symbolic evaluation was performed for Maple as in [7]. However, we use the newer version Maple 2020. Another feature we added to LACAST is the support of packages in Maple. Some functions are only available in modules (packages) that must be preloaded, such as QPochhammer in the package QDifferenceEquations18 . The general simplify method in Maple does not cover *q*-hypergeometric functions. Hence, whenever LACAST loads functions from the *q*-hyper-geometric package, the better performing QSimplify method is used. With the WED and the new support for Mathematica in LACAST, we perform the symbolic and numeric tests for Mathematica as well. The symbolic evaluation in Mathematica relies on the full simplification19. For Maple and Mathematica, we defined the global assumptions *x,y*∈R and *k,n,m*∈N. Constraints of test cases are added to their assumptions to support simplification. Adding more global assumptions for symbolic computation generally harms the performance since CAS internally uses assumptions for simplifications. It turned out that by adding more custom assumptions, the number of successfully simplified expressions decreases.

#### **4.2 Numerical Evaluation**

Defining an accurate test set of values to analyze an equivalence can be an arbitrarily complex process. It would make sense that every expression is tested on specific values according to the containing functions. However, this laborious process is not suitable for evaluating the entire DML and CAS. It makes more sense to develop a general set of test values that (i) generally covers interesting domains and (ii) avoid singularities, branch cuts, and similar problematic regions. Considering these two attributes, we come up with the ten test points illustrated in Figure 3. It contains four complex values on the unit circle and six points on the real axis. The test values cover the

18 https://jp.maplesoft.com/support/help/Maple/view.aspx?path= QDifferenceEquations/QPochhammer [accessed 09/01/2021]

19 https://reference.wolfram.com/language/ref/FullSimplify.html [accessed 09/01/2021]

general area of interest (complex values in all four quadrants, negative and positive real values) and avoid the typical singularities at {0*,*±1*,*±*i*}. In addition, several variables are tied to specific values for entire sections. Hence, we applied additional global constraints to the test cases.

The numeric evaluation engine heavily relies on the performance of extracting free variables from an expression. Unfortunately, the inbuilt functions in CAS, if available, are not very reliable. As the authors explained in [7], a custom algorithm within Maple was necessary to extract identifiers. Mathematica has the undocumented function Reduce'FreeVariables for this purpose. However, both systems, the custom solution in Maple and the inbuilt Mathematica function,

Fig. 3: The ten numeric test values in the complex plane for general variables. The dashed line represents the unit circle |*z*| = 1. At the right, we show the set of values for special variable values and general global constraints. On the right, *i* is referring to a generic variable and not to the imaginary unit.

have problems distinguishing free variables of entire expressions from the bound variables in MEOMs, e.g., integration and continuous variables. Mathematica sometimes does not extract a variable but returns the unevaluated input instead. We regularly faced this issue for integrals. However, we discovered one example without integrals. For EulerE[n,0] from [10, (24.4.26)], we expected to extract {*n*} as the set of free variables but instead received a set of the unevaluated expression itself {EulerE[n,0]} 20. Since the extended version of LACAST handles operators, including bound variables of MEOMs, we drop the use of internal methods in CAS and extend LACAST to extract identifiers from an expression. During a translation process, LACAST tags every single identifier as a variable, as long as it is not an element of a MEOM. This simple approach proves to be very efficient since it is implemented alongside the translation process itself and is already more powerful as compared to the existing inbuilt CAS solutions. We defined subscripts of identifiers as a part of the identifier, e.g., *z*1 and *z*2 are extracted as variables from *z*1+*z*2 rather than *z*.

The general pipeline for a numeric evaluation works as follows. First, we replace all substitutions and extract the variables from the left- and right-hand sides of the test expression via LACAST. For the previously mentioned example of the Struve function [10, (11.5.2)], LACAST identifies two variables in the expression, *ν* and *z*. According to the values in Figure 3, *ν* and *z* are set to the general ten values. A numeric test contains every combination of test values for all variables. Hence, we generate 100 test calculations for [10, (11.5.2)]. Afterward, we filter the test values that violate the attached constraints. In the case of the Struve function, we end up with 25 test cases.

In addition, we apply a limit of 300 calculations for each test case and abort a computation after 30 seconds due to computational limitations. If the test case generates more than 300 test values, only the first 300 are used. Finally, we calculate

20 The bug was reported to and confirmed by Wolfram Research Version 12.0.

the result for every remaining test value, i.e., we replace every variable by their value and calculate the result. The replacement is done by Mathematica's ReplaceAll method because the more appropriate method With, for unknown reasons, does not always replace all variables by their values. We wrap test expressions in Normal for numeric evaluations to avoid conditional expressions, which may cause incorrect calculations (see Section 5.1 for a more detailed discussion of conditional outputs). After replacing variables by their values, we trigger numeric computation. If the absolute value of the result (i.e., the difference between left- and right-hand side of the equation) is below the defined threshold of 0*.*001 or true (in the case of inequalities), the test calculation is considered successful. A numeric test case is only considered successful if and only if every test calculation was successful. If a numeric test case fails, we store the information on which values it failed and how many of these were successful.

### **5 Results**

The translations to Maple and Mathematica, the symbolic results, the numeric computations, and an overview PDF of the reported bugs to Mathematica are available online on our demopage. In the following, we mainly focus on Mathematica because of page limitations and because Maple has been investigated more closely by [7]. The results for Maple are also available online. Compared to the baseline (≈31%), our improvements doubled the amount translations (≈62%) for Maple and reach ≈71% for Mathematica. The majority of expressions that cannot be translated contain macros that have no adequate translation pattern to the CAS, such as the macros for interval Weierstrass lattice roots [10, §23.3(i)] and the multivariate hypergeometric function [10, (19.16.9)]. Other errors (6% for Maple and Mathematica) occur for several reasons. For example, out of the 418 errors in translations to Mathematica, 130 caused an error because the MEOM of an operator could not be extracted, 86 contained prime notations that do not refer to differentiations, 92 failed because of the underlying LATEX parser [34], and in 46 cases, the arguments of a DLMF macro could not be extracted.

Out of 4*,*713 translated expressions, 1*,*235 (26*.*2%) were successfully simplified by Mathematica (1*,*084 of 4*,*114 or 26*.*3% in Maple). For Mathematica, we also count results that are equal to 0 under certain conditions as successful (called ConditionalExpression). We identified 65 of these conditional results: 15 of the conditions are equal to constraints that were provided in the surrounding text but not in the info box of the DLMF equation; 30 were produced due to branch cut issues (see Section B in the Appendix); and 20 were the same as attached in the DLMF but reformulated, e.g., *z*∈C\(1*,*∞) from [10, (25.12.2)] was reformulated to ℑ*z*=0 ̸ ∨ℜ*z <*1. The remaining translated but not symbolically verified expressions were numerically evaluated for the test values in Figure 3. For the 3*,*474 cases, 784 (22*.*6%) were successfully verified numerically by Mathematica (698 of 2*,*618 or 26*.*7% by Maple21). For 1*,*784 the numeric evaluation failed. In the evaluation process, 655