{'fraction_non_alphanumeric': 0.05656784767413835, 'fraction_numerical': 0.01371414798746686, 'mean_word_length': 3.8669794721407627, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 26, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards Parallel Boolean Functional Synthesis

Given a relational specification R(X, Y), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applications in several areas. In this paper, we present the first parallel approach for solving this problem, using compositional and CEGAR-style reasoning as key building blocks. We show by means of extensive experiments that our approach outperforms existing tools on a large class of benchmarks.


Introduction
Given a relational specification of input-output behaviour, synthesizing outputs as functions of inputs is a key step in several applications, viz. program repair [13], program synthesis [27], adaptive control [24] etc. The synthesis problem is, in general, uncomputable. However, there are practically useful restrictions that render the problem solvable, e.g., if all inputs and outputs are Boolean, the problem is computable in principle. Nevertheless, functional synthesis may still require formidable computational effort, especially if there are a large number of variables and the overall specification is complex. This motivates us to investigate techniques for Boolean functional synthesis that work well in practice.
Formally, let X be a sequence of m input Boolean variables, and Y be a sequence of n output Boolean variables. A relational specification is a Boolean formula ϕ(X, Y ) that expresses a desired input-output relation. The goal in Boolean functional synthesis is to synthesize a function F : {0, 1} m → {0, 1} n that satisfies the specification. Thus, for every value of X, if there exists some value of Y such that ϕ(X, Y ) = 1, we must also have ϕ(X, F (X)) = 1. For values of X that do not admit any value of Y such that ϕ(X, Y ) = 1, the value of F (X) is inconsequential. Such a function F is also refered to as a Skolem function for Y in ϕ(X, Y ) [21,14].
An interesting example of Boolean functional synthesis is the problem of integer factorization. Suppose Y 1 and Y 2 are n-bit unsigned integers, X is a 2n-bit unsigned integer and × [n] denotes n-bit unsigned multiplication. The relational specification ϕ fact (X, Y 1 , Y 2 ) ≡ ((X = Y 1 × [n] Y 2 ) ∧ (Y 1 = 1) ∧ (Y 2 = 1)) specifies that Y 1 and Y 2 are non-trivial factors of X. This specification can be easily encoded as a Boolean relation. The corresponding synthesis problem requires us to synthesize the factors Y 1 and Y 2 as functions of X, whenever X is nonprime. Note that this problem is known to be hard, and the strength of several cryptographic systems rely on this hardness.
Existing approaches to Boolean functional synthesis vary widely in their emphasis, ranging from purely theoretical treatments (viz. [5,19,9,6,22,2]) to those motivated by practical tool development (viz. [20,21,11,28,14,10,16,3,27,26,17]). A common aspect of these approaches is their focus on sequential algorithms for synthesis. In this paper, we present, to the best of our knowledge, the first parallel algorithm for Boolean functional synthesis. A key ingredient of our approach is a technique for solving the synthesis problem for a specification ϕ by composing solutions of synthesis problems corresponding to sub-formulas in ϕ. Since Boolean functions are often represented using DAG-like structures (such as circuits, AIGs [15], ROBDDs [1,7]), we assume w.l.o.g. that ϕ is given as a DAG. The DAG structure provides a natural decomposition of the original problem into sub-problems with a partial order of dependencies between them. We exploit this to design a parallel synthesis algorithm that has been implemented on a message passing cluster. Our initial experiments show that our algorithm significantly outperforms state-of-the-art techniques on several benchmarks.

Related work:
The earliest solutions to Boolean functional synthesis date back to Boole [5] and Lowenheim [19], who considered the problem in the context of Boolean unification. Subsequently, there have been several investigations into theoretical aspects of this problem (see e.g., [9,6,22,2]). More recently, there have been attempts to design practically efficient synthesis algorithms that scale to much larger problem sizes. In [21], a technique to synthesize Y from a proof of validity of ∀X∃Y ϕ(X, Y ) was proposed. While this works well in several cases, not all specifications admit the validity of ∀X∃Y ϕ(X, Y ). For example, ∀X∃Y ϕ fact (X, Y ) is not valid in the factorization example. In [11,28], a synthesis approach based on functional composition was proposed. Unfortunately, this does not scale beyond small problem instances [14,10]. To address this drawback, a CEGAR based technique for synthesis from factored specifications was proposed in [14]. While this scales well if each factor in the specification depends on a small subset of variables, its performance degrades significantly if we have a few "large" factors, each involving many variables, or if there is significant sharing of variables across factors. In [20], Macii et al implemented Boole's and Lowenheim's algorithms using ROBDDs and compared their performance on small to medium-sized benchmarks. Other algorithms for synthesis based on ROBDDs have been investigated in [16,3]. A recent work [10] adapts the functional composition approach to work with ROBDDs, and shows that this scales well for a class of benchmarks with pre-determined variable orders. However, finding a good variable order for an arbitrary relational specification is hard, and our experiments show that without prior knowledge of benchmark classes and corresponding good variable orders, the performance of [10] can degrade significantly. Techniques using templates [27] or sketches [26] have been found to be effective for synthesis when we have partial information about the set of can-didate solutions. A framework for functional synthesis, focused on unbounded domains such as integer arithmetic, was proposed in [17]. This relies heavily on tailor-made smart heuristics that exploit specific form/structure of the relational specification.

Preliminaries
Let X = (x 1 , . . . x m ) be the sequence of input variables, and Y = (y 1 , . . . y n ) be the sequence of output variables in the specification ϕ(X, Y ). Abusing notation, we use X (resp. Y ) to denote the set of elements in the sequence X (resp. Y ), when there is no confusion. We use 1 and 0 to denote the Boolean constants true and false, respectively. A literal is either a variable or its complement. An assignment of values to variables satisfies a formula if it makes the formula true. We assume that the specification ϕ(X, Y ) is represented as a rooted DAG, with internal nodes labeled by Boolean operators and leaves labeled by input/output literals and Boolean constants. If the operator labeling an internal node N has arity k, we assume that N has k ordered children. Fig. 1 shows an example DAG, where the internal nodes are labeled by AND and OR operators of different arities. Each node N in such a DAG represents a Boolean formula Φ(N ), which is inductively defined as follows. If N is a leaf, Φ(N ) is the label of N . If N is an internal node labeled by op with arity k, and if the ordered children of N are c 1 , . . . c k , then Φ(N ) is op(Φ(c 1 ), . . . Φ(c k )). A DAG with root R is said to represent the formula Φ(R). Note that popular DAG representations of Boolean formulas, such as AIGs, ROBDDs and Boolean circuits, are special cases of this representation.
A k-ary Boolean function f is a mapping from {0, 1} k to {0, 1}, and can be viewed as the semantics of a Boolean formula with k variables. We use the terms "Boolean function" and "Boolean formula" interchangeably, using formulas mostly to refer to specifications. Given a Boolean formula ϕ and a Boolean function f , we use ϕ[y → f ] to denote the formula obtained by substituting every occurrence of the variable y in ϕ with f . The set of variables appearing in ϕ is called the support of ϕ. If f and g are Boolean functions, we say that f abstracts g and g refines f , if g → f , where → denotes logical implication.
Given the specification ϕ(X, Y ), our goal is to synthesize the outputs y 1 , . . . y n as functions of X. Unlike some earlier work [21,4,12], we do not assume the validity of ∀X∃Y ϕ(X, Y ). Thus, we allow the possibility that for some values of X, there may be no value of Y that satisfies ϕ(X, Y ). This allows us to accommodate some important classes of synthesis problems, viz. integer factorization.
If y 1 = f 1 (X), . . . y n = f n (X) is a solution to the synthesis problem, we say that (f 1 (X), . . . f n (X)) realizes Y in ϕ(X, Y ). For notational clarity, we simply use (f 1 , . . . f n ) instead of (f 1 (X), . . . f n (X)) when X is clear from the context.
In general, an instance of the synthesis problem may not have a unique solution. The following proposition, stated in various forms in the literature, characterizes the space of all solutions, when we have one output variable y. Proposition 1. A function f (X) realizes y in ϕ(X, y) iff the following holds: As a corollary, both ϕ[y → 1] and ¬ϕ[y → 0] realize y in ϕ(X, y). Proposition 1 can be easily extended when we have multiple output variables in Y . Let ⊑ be a total ordering of the variables in Y , and assume without loss of generality that y 1 ⊑ y 2 ⊑ · · · y n . Let − → F denote the vector of Boolean functions (f 1 (X), . . . f n (X)). For i ∈ {1, . . . n}, define ϕ (i) to be ∃y 1 . . . ∃y i−1 ϕ, and ϕ , with the obvious modifications for i = 1 (no existential quantification) and i = n (no substitution). The following proposition, once again implicit in the literature, characterizes the space of all solutions − → F that realize Y in ϕ(X, Y ).

Proposition 2. The function vector
Propositions 1 and 2 are effectively used in [11,28,14,10] to sequentially synthesize y 1 , . . . y n as functions of X. Specifically, output y 1 is first synthesized as a function g 1 (X, y 2 , . . . y n ). This is done by treating y 1 as the sole output and X ∪ {y 2 , . . . y n } as the inputs in ϕ(X, Y ). By substituting g 1 for y 1 in ϕ, we obtain ϕ (2) ≡ ∃y 1 ϕ(X, Y ). Output y 2 can then be synthesized as a function g 2 (X, y 3 , . . . y n ) by treating y 2 as the sole output and X ∪ {y 3 , . . . y n } as the inputs in ϕ (2) . Substituting g 2 for y 2 in ϕ (2) gives ϕ (3) ≡ ∃y 1 ∃y 2 ϕ(X, Y ). This process is then repeated until we obtain y n as a function g n (X). The desired functions f 1 (X), . . . f n (X) realizing y 1 , . . . y n can now be obtained by letting f n (X) be g n (X), and f i (X) be (· · · (g i [y i+1 → f i+1 (X)]) · · · )[y n → f n (X)], for all i from n − 1 down to 1. Thus, given ϕ(X, Y ), it suffices to obtain (g 1 , . . . g n ), where g i has support X ∪ {y i+1 , . . . y n }, in order to solve the synthesis problem. We therefore say that (g 1 , . . . g n ) effectively realizes Y in ϕ(X, Y ), and focus on obtaining (g 1 , . . . g n ).
Proposition 1 implies that for every i ∈ {1, . . . n}, the function g i ≡ ϕ (i) [y i → 1] realizes y i in ϕ (i) . With this choice for g i , it is easy to see that ∃y i ϕ (i) (or ϕ (i+1) ) can be obtained as . While synthesis using quantifier elimination by such self-substitution [10] has been shown to scale for certain classes of specifications with pre-determined optimized variable orders, our experience shows that this incurs significant overheads for general specifications with unknown "good" variable orders. An alternative technique for factored specification was proposed by John et al [14], in which initial abstractions of g 1 , . . . g n are first computed quickly, and then a CEGAR-style [8] loop is used to refine these abstractions to correct Skolem functions. We use John et al's refinement technique as a black-box module in our work; more on this is discussed in Section 3.1.
If N is a node in the DAG representation of the specification, we abuse notation and use ∆ yi (N ) to denote ∆ yi (Φ(N )), and similarly for Γ yi (N ), − → ∆(N ) and − → Γ (N ). Furthermore, if both Y and N are clear from the context, we use , respectively. It is easy to see that the supports of both Γ i and ∆ i are (subsets of) X ∪ {y i+1 , . . . y n }. Furthermore, it follows from Definition 1 that whenever Γ i (resp. ∆ i ) evaluates to 1, if the output y i has the value 1 (resp. 0), then ϕ must evaluate to 0. Conversely, if Γ i (resp. ∆ i ) evaluates to 0, it doesn't hurt (as far as satisfiability of ϕ(X, Y ) is concerned) to assign the value 1 (resp. 0) to output y i . This suggests that both ¬Γ i and ∆ i suffice to serve as the function g i (X, y i+1 , . . . y n ) when synthesizing functions for multiple output variables. The following proposition, adapted from [14], follows immediately, where we have abused notation and used ¬ − → Γ to denote (¬Γ 1 , . . . ¬Γ n ).
Proposition 3 shows that it suffices to compute − → ∆ (or − → Γ ) from ϕ(X, Y ) in order to solve the synthesis problem. In the remainder of the paper, we show how to achieve this compositionally and in parallel by first computing refinements of ∆ i (resp. Γ i ) for all i ∈ {1, . . . n}, and then using John et al's CEGAR-based technique [14] to abstract them to the desired ∆ i (resp. Γ i ). Throughout the paper, we use δ i and γ i to denote refinements of ∆ i and Γ i respectively.

Exploiting compositionality
Given a specification ϕ(X, Y ), one way to synthesize y 1 , . . . y n is to decompose ϕ(X, Y ) into sub-specifications, solve the synthesis problems for the subspecifications in parallel, and compose the solutions to the sub-problems to obtain the overall solution. A DAG representation of ϕ(X, Y ) provides a natural recursive decomposition of the specification into sub-specifications. Hence, the key technical question relates to compositionality: how do we compose solutions to synthesis problems for sub-specifications to obtain a solution to the synthesis problem for the overall specification? This problem is not easy, and no state-ofthe-art tool for Boolean functional synthesis uses such compositional reasoning.
Our compositional solution to the synthesis problem is best explained in three steps. First, for a simple, yet representationally complete, class of DAGs representing ϕ(X, Y ), we present a lemma that allows us to do compositional synthesis at each node of such a DAG. Next, we show how to use this lemma to design a parallel synthesis algorithm. Finally, we extend our lemma, and hence the scope of our algorithm, to significantly more general classes of DAGs.

Compositional synthesis in AND-OR DAGs
For simplicity of exposition, we first consider DAGs with internal nodes labeled by only AND and OR operators (of arbitrary arity). Fig. 1 shows an example of such a DAG. Note that this class of DAGs is representationally complete for Boolean specifications, since every specification can be expressed in negation normal form (NNF). In the previous section, we saw that computing ∆ i (ϕ) or Γ i (ϕ) for all i in {1, . . . n} suffices for purposes of synthesis. The following lemma shows the relation between ∆ i and Γ i at an internal node N in the DAG and the corresponding formulas at the node's children, say c 1 , . . . c k .
Proof. The proof of this lemma follows from Definition 1. Consider the case of disjunction op = ∨, i.e., Equation (1) for ∆ (the case for Γ is similar). Then On the other hand for conjunction op = ∧, i.e., Equation (2) (and similarly for Γ), we only have one direction: This completes the proof. ⊓ ⊔ Thus, if N is an OR-node, we obtain ∆ i (N ) and Γ i (N ) directly by conjoining ∆ i and Γ i at its children. However, if N is an AND-node, disjoining the ∆ i and Γ i at its children only gives refinements of ∆ i (N ) and Γ i (N ) (see Equation (2)). Let us call these refinements δ i (N ) and γ i (N ) respectively. To obtain ∆ i (N ) and Γ i (N ) exactly at AND-nodes, we must use the CEGAR technique developed in [14] to iteratively abstract δ i (N ) and γ i (N ) obtained above. More on this is discussed below.
A CEGAR step involves constructing, for each i from 1 to n, a Boolean error formula Err δi (resp. Err γi ) such that the error formula is unsatisfiable iff . A SAT solver is then used to check the satisfiability of the error formula. If the formula is unsatisfiable, we are done; otherwise the satisfying assignment can be used to further abstract the respective refinement. This check-and-abstract step is then repeated in a loop until the error formulas become unsatisfiable. Following the approach outlined in [14], it can be shown that if we use Err δi ≡ ¬δ i ∧ i j=1 (y j ↔ δ j ) ∧ ¬ϕ and Err γi ≡ ¬γ i ∧ i j=1 (y j ↔ ¬γ j ) ∧ ¬ϕ, and perform CEGAR in order from i = 1 to i = n, it suffices to gives us ∆ i and Γ i . For details of the CEGAR implementation, the reader is referred to [14]. The above discussion leads to a straightforward algorithm Compute (shown as Algorithm 1) that computes − → ∆(N ) and − → Γ (N ) for a node N , using − → ∆(c j ) and − → Γ (c j ) for its children c j . Here, we have assumed access to a black-box function Perform Cegar that implements the CEGAR step.

A parallel synthesis algorithm
The DAG representation of ϕ(X, Y ) gives a natural, recursive decomposition of the specification, and also defines a partial order of dependencies between the corresponding synthesis sub-problems. Algorithm Compute can be invoked in parallel on nodes in the DAG that are not ordered w.r.t. this partial order, as long as Compute has already been invoked on their children. This suggests a simple parallel approach to Boolean functional synthesis. Algorithm ParSyn, shown below, implements this approach, and is motivated by a message-passing architecture. We consider a standard manager-worker configuration, where one out of available m cores acts as the manager, and the remaining m − 1 cores act as workers. All communication between the manager and workers is assumed to happen through explicit send and receive primitives.
The manager uses a queue Q of ready-to-process nodes. Initially, Q is initialized with the leaf nodes in the DAG, and we maintain the invariant that all nodes in Q can be processed in parallel. If there is an idle worker W and if Q is not empty, the manager assigns the node N at the front of Q to worker W for processing. If N is an internal DAG node, the manager also sends − → ∆(c j ) and − → Γ (c j ) for every child c j of N to W . If there are no idle workers or if Q is empty, the manager waits for a worker, say W ′ , to finish processing its assigned node, say N ′ . When this happens, the manager stores the result sent by W ′ as − → ∆(N ′ ) and − → Γ (N ′ ). It then inserts one or more parents N ′′ of N ′ in the queue Q, if all children of N ′′ have been processed. The above steps are repeatedly executed at the manager until all DAG nodes have been processed. The job of a worker W is relatively simple: on being assigned a node N , and on receiving − → ∆(c j ) and − → Γ (c j ) for all children c j of N , it simply executes Algorithm Compute on N and returns − → ∆(N ), − → Γ (N ) . Note that Algorithm ParSyn is guaranteed to progress as long as all workers complete processing the nodes assigned to them in finite time. The partial order of dependencies between nodes ensures that when all workers are idle, either all nodes have already been processed, or at least one unprocessed node has − → ∆ and − → Γ computed for all its children, if any.

Extending the Composition Lemma and algorithms
So far, we have considered DAGs in which all internal nodes were either ANDor OR-nodes. We now extend our results to more general DAGs. We do this by generalizing the Composition Lemma to arbitrary Boolean operators. Specifically, given the refinements δ i (c j ) and γ i (c j ) at all children c j of a node N , we show how to compose these to obtain δ i (N ) and γ i (N ), when N is labeled by an arbitrary Boolean operator. Note that the CEGAR technique discussed in Section 3.1 can be used to abstract the refinements δ i and γ i to ∆ i and Γ i

Algorithm 2: ParSyn
Input: AND-OR DAG with root Rt representing ϕ(X, Y ) in NNF form Output: (g1, . . . gn) that effectively realize Y in ϕ(X, Y ) /* Algorithm for Manager */ 1 Queue Q ; /* Invariant: Q has nodes that can be processed in parallel, i.e., leaves or nodes whose children have their wait until some worker W ′ processing node N ′ becomes free; Mark node N ′ as processed; respectively, at any node of interest. Therefore, with our generalized Composition Lemma, we can use compositional synthesis for specifications represented by general DAGs, even without computing ∆ i and Γ i exactly at all DAG nodes. This gives an extremely powerful approach for parallel, compositional synthesis.
where op is an r-ary Boolean operator. For convenience of notation, we use ¬N to denote ¬Φ(N ), and similarly for other nodes, in the subsequent discussion. Suppose we are given δ i (c j ), γ i (c j ), δ i (¬c j ) and γ i (¬c j ), for 1 ≤ j ≤ r. We wish to compose these appropriately to compute δ i (N ), γ i (N ), δ i (¬N ) and γ i (¬N ) for 1 ≤ i ≤ n. Once we have these refinements, we can adapt Algorithm 1 to work for node N , labeled by an arbitrary Boolean operator op.
Proof. We provide a proof for the first implication. The proofs for the other implications are similar. Consider an assignment η of values to X ∪ {y 1 , . . . y n } such that η satisfies the left hand side of implication (1). We show below that η satisfies ∆ i (N ) as well.
Let η ⋆ denote an assignment of values to variables that coincides with η for all variables, except possibly for y i . Formally, η ⋆ (v) = η(v) for v ∈ X ∪ {y 1 , . . . y i−1 , y i+1 , . . . y n } and η ⋆ (y i ) = 0. We use η ⋆ (v) to denote the value assigned to variable v in η ⋆ . If ψ is a Boolean formula, we abuse notation and use η ⋆ (ψ) to denote the value that ψ evaluates to, when variables are assigned values according to η ⋆ .
Since the right hand side of implication (1) does not have y i in its support, it suffices to show that η ⋆ satisfies ∆ i (N ). Furthermore, since neither side of implication (1) depends on {y 1 , . . . y i−1 }, our arguments work for all values of {y 1 , . . . y i−1 }. Hence, it suffices to show that η ⋆ (N ) = 0.
Proof. To see why this is true, note that η ⋆ satisfies the left hand side of implication (1), and hence it satisfies δ i (c l ). Since η ⋆ (y i ) = 0, it follows from the definition of δ i (·) that η ⋆ (c l ) = 0.
From the definition of Ω l,op,≺ , it is easy to see that (Ω l,op,≺ [z s → ¬z s ]) r s=l+1 is exactly ∆ z l (op). Therefore, Ω l,op,≺ evaluated at ρ has the same value, i.e.
The other implications can be similarly proved following this same template.

⊓ ⊔
We simply illustrate the idea behind the lemma with an example here.
Recalling the definition of δ z2 (·), if we set z 3 = 1, z 4 = 0 and z 2 = 0, then op must evaluate to 0 regardless of the value of z 1 . By substituting δ i (¬c 3 ) for z 3 and δ i (c 4 ) for z 4 in Ω 2,op , we get the formula δ i (¬c 3 ) ∧ δ i (c 4 ). Denote this formula by χ and note that its support is X ∪ {y i+1 , . . . y n }. Note also from the definition of δ i (·) that if χ evaluates to 1 for some assignment of values to X ∪ {y i+1 , . . . y n } and if y i = 0, evaluates to 0 and Φ(c 4 ) evaluates to 0, regardless of the values of y 1 , . . . y i−1 . This means that z 3 = 1 and z 4 = 0, and hence δ z2 (op) = 1. If z 2 (or Φ(c 2 ) can also be made to evaluate to 0 for the same assignment of values to X ∪ {y i , y i+1 , . . . y n }, then N = op(c 1 , . . . c r ) must evaluate to 0, regardless of the values of {y 1 , . . . y i−1 }. Since y i = 0, values assigned to X ∪{y i+1 , . . . y n } must therefore be a satisfying assignment of ∆ i (N ). One way of achieving this is to ensure that ∆ i (c 2 ) evaluates to 1 for the same assignment of values to X ∪ {y i+1 , . . . y n } that satisfies χ. Therefore, we require the assignment of values to X ∪ {y i+1 , . . . y n } to satisfy χ ∧ ∆ i (c 2 ), or even χ∧δ i (c 2 ). Since χ = δ i (¬c 3 )∧δ i (c 4 ), we get δ i (c 2 )∧δ i (¬c 3 )∧δ i (c 4 ) as a refinement of ∆ i (N ).
Applying the generalized Composition Lemma: Lemma 2 suggests a way of compositionally obtaining δ i (N ), γ i (N ), δ i (¬N ) and γ i (¬N ) for an arbitrary Boolean operator op. Specifically, the disjunction of the left-hand sides of implications (1) and (2) in Lemma 2, disjoined over all l ∈ {1, . . . r} and over all total orders (≺) of {z 1 , . . . z r }, gives a refinement of ∆ i (N ). A similar disjunction of the left-hand sides of implications (3) and (4) in Lemma 2 gives a refinement of Γ i (ϕ). The cases of ∆ i (¬N ) and Γ i (¬N ) are similar. This suggests that for each operator op that appears as label of an internal DAG node, we can pre-compute a template of how to compose δ i and γ i at the children of the node to obtain δ i and γ i at the node itself. In fact, pre-computing this template for op = ∨ and op = ∧ by disjoining as suggested above, gives us exactly the left-to-right implications, i.e., refinements of ∆ i (N ) and Γ i (N ), as given by Lemma 1. We present templates for some other common Boolean operators like if-then-else in the next subsection.
Once we have pre-computed templates for composing δ i and γ i at children of a node N to get δ i (N ) and γ i (N ), we can use these pre-computed templates in Algorithm 1, just as we did for AND-nodes. This allows us to apply compositional synthesis on general DAG representations of Boolean relational specifications.
Optimizations using partial computations: Given δ i and γ i at children of a node N , we have shown above how to compute δ i (N ) and γ i (N ). To compute ∆ i (N ) and Γ i (N ) exactly, we can use the CEGAR technique outlined in Section 3.1. While this is necessary at the root of the DAG, we need not compute ∆ i (N ) and Γ i (N ) exactly at each intermediate node. In fact, the generalized Composition Lemma allows us to proceed with δ i (N ) and γ i (N ). This suggests some optimizations: (i) Instead of using the error formulas introduced in Section 3.1, that allow us to obtain ∆ i (N ) and Γ i (N ) exactly, we can use the error formula used in [14]. The error formula of [14] allows us to obtain some Skolem function for y i (not necessarily ∆ i (N ) or ¬Γ i (N )) using the sub-specification Φ(N ) corresponding to node N . We have found CEGAR based on this error formula to be more efficient in practice, while yielding refinements of ∆ i (N ) and Γ i (N ). In fact, we use this error formula in our implementation. (ii) We can introduce a timeout parameter, such that − → ∆(N ), − → Γ (N ) are computed exactly at each internal node until we timeout happens. Subsequently, for the nodes still under process, we can simply combine δ i and γ i at their children using our pre-computed composition templates, and not invoke CEGAR at all. The only exception to this is at the root node of the DAG where CEGAR must be invoked.

Application of Lemma 2 through Examples
In this subsection, with the help of examples, we present the computation of the ∆ . and Γ . templates for various boolean formulae. We also compare these templates with those obtained by using Algorithm 1.

Example 1.
To begin with, we demonstrate how to derive the templates for the ∧ operator.
Let ϕ = c 1 ∧c 2 where c 1 , c 2 are arbitrary boolean formulae and have (a subset of) X ∪ Y in their support. As shown in Figure 2, let z 1 and z 2 be fresh Boolean variables. We first compute the relevant γ(.) and δ(.)'s for z 1 ∧ z 2 and then use Lemma 2 to compute the template for ∆ i (ϕ) and Γ i (ϕ).
Using the Generalized Compositional lemma, (Lemma 2), we get: On disjunction of the terms on the LHS, we get the following template which is exactly the same as that proved in Lemma 1.
Again, using the Generalized Compositional lemma, (Lemma 2), we get: By disjuncting the terms in the LHS, we get the following template δ i (c 1 ) ∧ δ i (c 2 ) → ∆ i (ϕ) ; which is, again, the same as that proved in Lemma 1. where c 1 , c 2 , c 3 are arbitrary boolean formulae and have (a subset of) X ∪ Y in their support. As before, let z 1 , z 2 and z 3 be fresh Boolean variables. We first compute the relevant γ(.) and δ(.)'s for ite(z 1 , z 2 , z 3 ) and then use Lemma 2 to compute the template for ∆ i (ϕ) and Γ i (ϕ).
Finally, on existentially quantifying z 1 and z 2 from F , we get: ∃z 1 ∃z 2 F = 1; which gives ∆ 3 (F ) = Γ 3 (F ) = 0 From Lemma 2, we have: Combining these terms, we get the template for ∆ i (ϕ) as: Similarly, the template for Γ i (ϕ) is: Note that, we can also represent ite(c 1 , c 2 , c 3 ) as a formula G containing only AND, OR and NOT operators and derive the template directly using Lemma 1. That is, let G = (c 1 ∧ c 2 ) ∨ (¬c 1 ∧ c 3 ). Using Algorithm 1 (and not doing Step 14 of Perform Cegar), we get the following: Here again, the templates given by Lemma 1 and Lemma 2 are the same. However, in the next example we consider a boolean function where the two differ.
Example 4. With the help this example, we demonstrate that Lemma 2 can give better underapproximations than the approach presented in Algorithm 1. Let where c 1 , c 2 , c 3 are arbitrary boolean formulae and have (a subset of) X ∪ Y in their support. As before, let z 1 , z 2 and z 3 be fresh Boolean variables.
Using the compositional lemma we get: Disjunction of the terms on the LHS, allows us to get: However, if we represent ϕ = (c 1 ⊕ c 2 ) ∧ (c 1 ⊕ c 3 ) as a boolean formula containing AND's and OR's as ϕ = ((¬c 1 ∧ c 2 ) ∨ (c 1 ∧ ¬c 2 )) ∧ (((¬c 1 ∧ c 3 ) ∨ (c 1 ∧ ¬c 3 )). Using Algorithm 1 (and not doing Step 14 of Perform Cegar), we only get the following: Note that in addition to the terms above, the template for ∆ i (ϕ) derived using Lemma 2 also has the additional terms (δ i (c 2 ) ∧ δ i (¬c 3 )) ∨ (δ i (¬c 2 ) ∧ δ i (c 3 )). It can easily be seen that these two terms are necessary, if c 2 = c 3 then ϕ will not evaluate to true. This example shows Lemma 2 can give better underapproximations than Lemma 1 for complex boolean formulae.

Experimental results
Experimental methodology. We have implemented Algorithm 2 with the error formula from [14] used for CEGAR in Algorithm 1 (in function Perform Cegar), as described at the end of Section 3.3. We call this implementation ParSyn in this section, and compare it with the following algorithms/tools: (i) CSk: This is based on the sequential algorithm for conjunctive formulas, presented in [14]. For non-conjunctive formulas, the algorithm in [14], and hence CSk, reduces to [11,28]. (ii) RSynth: The RSynth tool as described in [10]. (iii) Bloqqer: As prescribed in [21], we first generate special QRAT proofs using the preprocessing tool bloqqer, and then generate Boolean function vectors from the proofs using the qrat-trim tool.
Our implementation of ParSyn, available online at [25], makes extensive use of the ABC [18] library to represent and manipulate Boolean functions as AIGs. We also use the default SAT solver provided by ABC, which is a variant of MiniSAT. We present our evaluation on three different kinds of benchmarks.
1. Disjunctive Decomposition Benchmarks: Similar to [14], these benchmarks were generated by considering some of the larger sequential circuits in the HWMCC10 benchmark suite, and formulating the problem of disjunctively decomposing each circuit into components as a problem of synthesizing a vector of Boolean functions. Each generated benchmark is of the form ∃Y ϕ(X, Y ) where ∃X(∃Y ϕ(X, Y )) is true. However, unlike [14], where each benchmark (if not already a conjunction of factors) had to be converted into factored form using Tseitin encoding (which introduced additional variables), we have used these benchmarks without Tseitin encoding. 2. Arithmetic Benchmarks: These benchmarks were taken from the work described in [10]. Specifically, the benchmarks considered are floor, ceiling, decomposition, equalization and intermediate (see [10] for details). 3. Factorization Benchmarks: We considered the integer factorization problem for different bit-widths, as discussed in Section 1.
For each arithmetic and factorization benchmark, we first specified the problem instance as an SMT formula and then used Boolector [23] to generate the Boolean version of the benchmark. For each arithmetic benchmark, three variants were generated by varying the bit-width of the arguments of arithmetic operators; specifically, we considered bit-widths of 32, 128 and 512. Similarly, for the factorization benchmark, we generated four variants, using 8, 10, 12 and 16 for the bit-width of the product. Further, as Bloqqer requires the input to be in qdimacs format and RSynth in cnf format, we converted each benchmark into qdimacs and cnf formats using Tseitin encoding [29]. All benchmarks and the procedure by which we generated them are detailed in [25].
Variable ordering: We used the same ordering of variables for all algorithms. For each benchmark, the variables are ordered such that the variable which occurs in the transitive fan-in of the least number of nodes in the AIG representation of the specification, appears at the top. For RSynth this translated to an interleaving of most of the input and output variables.
Machine details : All experiments were performed on a message-passing cluster, where each node had 20 cores and 64 GB main memory, each core being a 2.20 GHz Intel Xeon processor. The operating system was Cent OS 6.5. For CSk, Bloqqer, and RSynth, a single core on the cluster was used. For all comparisons, ParSyn was executed on 4 nodes using 5 cores each, so that we had both intranode and inter-node communication. The maximum time given for execution was 3600 seconds, i.e., 1 hour. We also restricted the total amount of main memory (across all cores) to be 16GB. The metric used to compare the different algorithms was the time taken to synthesize Boolean functions. Effect of the number of cores. For this experiment, we chose 5 of the larger benchmarks. Of these, two benchmarks belonged to the disjunctive decomposition category, two belonged to the arithmetic benchmark category and one was the 12 bit factorization benchmark. The number of cores was varied from 2 to 25. With 2 cores, ParSyn behaves like a sequential algorithm with one core acting as the manager and the other as the worker with all computation happening at the worker core. Hence, with 2 cores, we see the effect of compositionality without parallelism. For number of cores > 2, the number of worker cores increase, and the computation load is shared across the worker cores. Figure 3a shows the results of our evaluation. The topmost points indicated by FL are instances for which ParSyn timed out. We can see that, for all 5 benchmarks, the time taken to synthesize Boolean function vectors when the number of cores is 2 is considerable; in fact, ParSyn times out on three of the benchmarks. When we increase the number of cores we observe that (a) by synthesizing in parallel, we can now solve benchmarks for which we had timed out earlier, and (b) speedups of about 4 − 5 can be obtained with 5 − 15 cores. From 15 cores to 25 cores, the performance of the algorithm, however, is largely invariant and any further increase in cores does not result in further speed up.

Results
To understand this, we examined the benchmarks and found that their AIG representatation have more nodes close to the leaves than to the root (similar to the DAG in Figure 1). The time taken to process a leaf or a node close to a leaf is typically much less than that for a node near the root. Furthermore, the dependencies between the nodes close to the root are such that at most one or two nodes can be processed in parallel leaving most of the cores unutilized. When the number of cores is increased from 2 to 5 − 15, the leaves and the nodes close to the leaves get processed in parallel, reducing the overall time taken by the algorithm. However, the time taken to process the nodes close to the root remains more or less the same and starts to dominate the total time taken. At this point, even if the number of cores is further increased, it does not significantly reduce the total time taken. This behaviour limits the speed-ups of our algorithm. For the remaining experiments, the number of cores used for ParSyn was 20.
ParSyn vs CSk: As can be seen from Figure 3b, CSk ran successfully on only 12 of the 46 benchmarks, whereas ParSyn was successful on 39 benchmarks, timing out on 6 benchmarks and running out of memory on 1 benchmark. Of the benchmarks that CSk was successful on, 9 belonged to the arithmetic category, 2 to the factorization and 1 to the disjunctive decomposition category. On further examination, we found that factorization and arithmetic benchmarks (except the intermediate problems) were conjunctive formulae whereas disjunctive decomposition benchmarks were arbitrary Boolean formulas. Since CSk has been specially designed to handle conjunctive formulas, it is successful on some of these benchmarks. On the other hand, since disjunctive decomposition benchmarks are not conjunctive, CSk treats the entire formula as one factor, and the algorithm reduces to [11,28]. The performance hit is therefore not surprising; it has been shown in [14] and [10] that the algorithms of [11,28] do not scale to large benchmarks. In fact, CSk was successful only on the smallest disjunctive decomposition benchmark.
ParSyn vs RSynth: As seen in Figure 4a, RSynth was successful only on 3 of the 46 benchmarks; it timed out on 37 and ran out of memory on 6 benchmarks. The 3 benchmarks that RSynth was successful on were the smaller factorization benchmarks. Note that the arithmetic benchmarks used in [10] are semantically the same. In [10], custom variable orders were used to construct the ROBDDs, which resulted in compact ROBDDs. In our case, we use the variable ordering heuristic mentioned above (see Sec. 4.1), and include the considerable time taken to build BDDs from cnf representation. As mentioned in Section 1, if we know a better variable ordering, then the time taken can potentially reduce. However, we do not know the optimal variable order for an arbitrary specification in general. We also found the memory footprint of RSynth to be higher as indicated by the memory-outs. This is not surprising, as RSynth uses BDDs to represent Boolean formula and it is well-known that BDDs can have large memory requirements.
ParSyn vs Bloqqer: Since Bloqqer cannot synthesize Boolean functions for formulas wherein ∀X∃Y ϕ(X, Y ) is not valid, we restricted our comparison to only the disjunctive decomposition and arithmetic benchmarks, totalling 42 in number. From Figure 4b, we can see that Bloqqer successfully synthesizes Boolean functions for 25 of the 42 benchmarks. For several benchmarks for which it is successful, it outperforms ParSyn. In line 14 of Algorithm 1, Perform Cegar makes extensive use of the SAT solver, and this is reflected in the time taken by ParSyn. However, for the remaining 17 benchmarks, Bloqqer gave a Not Verified message indicating that it could not synthesize Boolean functions for these benchmarks. In comparison, ParSyn was successful on most of these benchmarks.
Effect of timeouts on ParSyn. Finally, we discuss the effect of the timeout optimization discussed in Section 3.3. Specifically, for 60 seconds (value set through a timeout parameter), starting from the leaves of the AIG representation of a specification, we synthesize exact Boolean functions for DAG nodes. After timeout, on the remaining intermediate nodes, we do not invoke the CEGAR step at all, except at the root node of the AIG. This optimization enabled us to handle 3 more benchmarks, i.e., ParSyn with this optimization synthesized Boolean function vectors for all the equalization benchmarks (in < 340 seconds). Interestingly, ParSyn without timeouts was unable to solve these problems. This can be explained by the fact that in these benchmarks many internal nodes required multiple iterations of the CEGAR loop to compute exact Boolean functions, which were, however, not needed to compute the solution at the root node.

Conclusion and future work
In this paper, we have presented the first parallel and compositional algorithm for complete Boolean functional synthesis from a relational specification. A key feature of our approach is that it is agnostic to the semantic variabilities of the input, and hence applies to a wide variety of benchmarks. In addition to the disjunctive decomposition of graphs and the arithmetic operation benchmarks, we considered the combinatorially hard problem of factorization and attempted to generate a functional characterization for it. We found that our implementation outperforms existing tools in a variety of benchmarks.
There are many avenues to extend our work. First, the ideas for compositional synthesis that we develop in this paper could potentially lead to parallel implementations of other synthesis tools, such as that described in [10]. Next, the factorization problem can be generalized to synthesis of inverse functions for classically hard one-way functions, as long as the function can be described efficiently by a circuit/AIG. Finally, we would like to explore improved ways of parallelizing our algorithm, perhaps exploiting features of specific classes of problems.