11institutetext: Rice University, Houston TX 77005, USA
11email<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
# Dynamic Programming for Symbolic Boolean Realizability and Synthesis111This
is the full version of this paper, with appendices included.

Yi Lin 11 0000-0001-8443-2246 Lucas M. Tabajara Currently at Runtime
Verification, Inc.11 0000-0001-9608-1404 Moshe Y. Vardi 11 0000-0002-0661-5773

###### Abstract

Inspired by recent progress in dynamic programming approaches for weighted
model counting, we investigate a dynamic-programming approach in the context
of boolean realizability and synthesis, which takes a conjunctive-normal-form
boolean formula over input and output variables, and aims at synthesizing
witness functions for the output variables in terms of the inputs. We show how
graded project-join trees, obtained via tree decomposition, can be used to
compute a BDD representing the realizability set for the input formulas in a
bottom-up order. We then show how the intermediate BDDs generated during
realizability checking phase can be applied to synthesizing the witness
functions in a top-down manner. An experimental evaluation of a solver –
DPSynth – based on these ideas demonstrates that our approach for Boolean
realizabilty and synthesis has superior time and space performance over a
heuristics-based approach using same symbolic representations. We discuss the
advantage on scalability of the new approach, and also investigate our
findings on the performance of the DP framework.

###### Keywords:

Boolean synthesis Binary decision diagram Dynamic programming Bucket
elimination.

##  1 Introduction

The _Boolean-Synthesis Problem_ [19] – a fundamental problem in computer-aided
design – is the problem of taking in a declarative boolean relation between
two sets of boolean variables – input and output – and generating boolean
functions, called _witness functions_ , that yield values to the output
variables with respect to the input variables so as to satisfy the boolean
relation. As a fundamental problem in computer-aided design, there are many
applications of boolean synthesis in circuit design. For example, based on a
circuit’s desired behavior, we can use boolean synthesis to automatically
construct the missing components of the circuit [3]. In addition to being used
in circuit design, boolean synthesis has recently found applications also in
temporal synthesis [30, 29], where the goal is to construct a a sequential
circuit that responds to environment inputs in a way that is guaranteed to
satisfy given temporal-logic specification.

Many approaches have been investigated for boolean synthesis, such as
knowledge compilation [1], QBF solving [23], and machine learning [17, 18].
Here we build on previous work on boolean synthesis using Binary Decision
Diagrams (BDDs) [27]. The main advantage of the decision-diagram approach is
that it provides not just the synthesized witness functions, but also the
realizability set of the specification, which is the set of inputs with
respect to which the specification is realizable. In _modular circuit design_
[19], where a system is composed of multiple modules that are independently
constructed, it is imperative to confirm the realizability set of a module, as
it has to match the output set of prior modules. Similarly, in the context of
temporal synthesis [30, 29], the winning set is constructed iteratively by
taking the union of realizability sets, where for each realizability set we
construct a witness function. The winning strategy is then constructed by
stitching together all these witness functions.

Motivated by applications that require the computation of both realizability
sets and witness functions, we describe here a decision-diagram approach that
can also handle _partially realizable_ specifications, where the realizability
set is neither empty nor necessarily universal. (Indeed, in our benchmark
suit, about 30% of the benchmarks are partially realizable.) Our tool,
_DPSynth_ computes the realizability sets and witness functions with respects
to these sets. While several recent synthesis tools do provide witnesses for
partially-realizable specifications, cf. [1, 17, 18], not all of them directly
output the realizability set, requiring it, instead, to be computed from the
witnesses and the original formula.

The boolean-synthesis problem starts with a boolean formula $\varphi(X,Y)$
over sets $X,Y$ of _input_ and _output_ variables. The goal is to construct
boolean formulas, called _witness functions_ (sometimes called _Skolem
functions_) [18, 1] – for the _output variables_ expressed in terms of the
_input variables_. The BDD-based approach to this problem [15] constructs the
BDD $B_{\varphi}(X,Y)$ for $\varphi$, and then quantifies existentially over
the $Y$ variables to obtain a BDD over the $X$ variables that captures the
_realizability set_ – the set of assignments $\tau_{X}$ in $2^{X}$ for which
an assignment $\tau_{Y}$ in $2^{Y}$ exists where
$B_{\varphi}(\tau_{X},\tau_{y})=1$. The witness functions can then be
constructed by iterating over the intermediate steps of the realizability
computation [15].

A challenge of this BDD-based approach is that it is often infeasible to
construct the BDD $B_{\varphi}$. _Factored Boolean Synthesis_ [27] assumes
that the formula $\varphi$ is given in conjunctive normal form (CNF), where
the individual clauses are called _factors_. Rather than constructing the
monolithic BDD $B_{\varphi}$, this approach constructs a BDD for each factor,
and then applies conjunction in a lazy way and existential quantification in
an eager way, using various heuristics to order conjoining and quantifying. As
shown in [27], the factored approach, _Factored RSynth_ , is more scalable
than the monolithic approach, RSynth. Thus, we use here Factored RSynth as the
baseline for comparison in this paper.

By _dynamic programming_ we refer to the approach that simplifies a
complicated problem by breaking it down into simpler sub-problems in a
recursive manner [5]. Unlike search-based approaches to Boolean reasoning, cf.
[21], which directly manipulate truth assignments, we use data structure based
on decision diagrams [7] that represents sets of truth assignments. This
approach is referred to as _symbolic_ , going back to [11].

The _symbolic dynamic-programming_ approach we propose here is inspired by
progress in _weighted model counting_ , which is the problem of counting the
number of satisfying (weighted) assignments of boolean formulas. Dudek, Phan,
and Vardi proposed in [14], an approach based on Algebraic Decision Diagrams,
which are the quantitative variants of BDDs [4]. Dudek et al. pointed out that
a monolithic approach is not likely to be scalable, and proposed a factored
approach, ADDMC, analogous to the approach in [27], in which conjunction is
done lazily and quantification eagerly. In follow-up work [12], they proposed
a more systematic way to order the quantification and conjunction operations,
based on dynamic programming over _project-join trees_ ; the resulting tool,
DPMC, was shown to scale better than ADDMC. In further follow-on work, they
proposed _graded project-join trees_ for _projected model counting_ , where
the input formula has two sets of variables – quantified variables and
counting variables [13]. Graded project-join tree offers a recursive
decomposition of the Boolean-Synthesis Problem into smaller tasks of
projections and join.

We show here how symbolic dynamic programming over graded project-join trees
can be applied to boolean synthesis. In our approach, realizability checking
is done using a BDD-based _bottom-up_ execution, analogous to the handling of
counting quantifiers in [13]. This enables us to compute the realizability set
and check its nonemptiness. We then present a novel algorithm for synthesizing
the witness functions using _top-down_ execution on graded project-join trees.
(In contrast, [13] both types of quantifiers are handled bottom-up). We
demonstrate the advantage of our bottom-up-top-down approach by developing a
tool, _DPSynth_. For a fair evaluation, we compare its performance to Factored
RSynth, which can also handle partially realizable specifications.

The main contributions of this work are as follows. First, we show how to
adapt the framework of projected counting to Boolean synthesis. In projected
counting there are two types of existential quantifiers – additive and
disjunctive [13], while Boolean synthesis combine universal and existential
quantifiers. Second, projected counting requires only a bottom-up pass over
the graded project-join trees, while here we introduce an additional, top-down
pass over the tree to perform the major part of boolean synthesis, which
is,witness construction.

The organization of the paper is as follows. After preliminaries in Section 2,
we show in Section 3 how to use graded project-join trees for boolean
realizability checking, and show that DPSynth generally scales better than
Factored RSynth. Then, in Section 4, we show how to extend this approach from
realizability checking to witness-function construction. Experimental
evaluation shows that DPSynth generally scales better than Factored RSynth
also for witness-function construction. We offer concluding remarks in Section
6.

##  2 Preliminary Definitions

###  2.1 Boolean Formula and Synthesis Concepts

A _boolean formula_ $\varphi(X)$, over a set $X$ of variables, represents a
_boolean function_ $f:2^{X}\to\mathbb{B}$, which selects subsets of $2^{X}$. A
truth assignment $\tau$ _satisfies_ $\varphi$ iff $\varphi(\tau)=1$. A boolean
formula in _conjunctive normal form (CNF)_ is a conjunction of _clauses_ ,
where a clause is a disjunction of _literals_ (a boolean variable or its
negation). When $\varphi$ is in CNF, we abuse notation and also use $\varphi$
to denote its own set of clauses. Given a CNF formula $\varphi(X,Y)$ over
_input_ and output variable $X$ and $Y$, the _realizability set_ of $\varphi$,
denoted $R_{\varphi}(X)\subseteq 2^{X}$, is the set of assignments $\sigma\in
2^{X}$ for which there exists an assignment $\tau\in 2^{Y}$ such that
$\varphi(\sigma\cup\tau)=1$. When $\varphi$ is clear from context, we simply
denote the realizability set by $R$.

######  Definition 1 (Realizability).

Let $\varphi(X,Y)$ be a CNF formula with $X$ and $Y$ as input and output
variables. We say that $\varphi$ is _fully realizable_ if $R=2^{X}$. We say
that $\varphi$ is _partially realizable_ if $R\neq\varnothing$. Finally, we
say that $\varphi$ is _nullary realizable_ if $R=\varnothing$.

Given the condition that the formula is at least partially realizable, the
boolean synthesis problem asks for a set of _witnesses_ for the output
variables generated on top of given input values, such that the formula is
satisfied. This sub-problem of constructing witnesses, is usually referred to
as synthesis.

The motivation behind synthesizing partially-realizable specifications is that
there are cases where a specification is not fully realizable, but it is still
useful to synthesize a function that works for all inputs in the realizability
set. An example is the factorization benchmark family, as discussed in the
introduction of [3], which takes an integer and aims to factor it into two
integers that are both not equal to 1. If the integer is prime, then there is
no valid factorization for this particular input, but it would still be
valuable to have a solution that works for all composite numbers. This is why
our attention to partially-realizable cases is a contribution of the paper,
while related works tend to focus mostly on fully-realizable instances.

######  Definition 2 (Witnesses in Boolean Synthesis Problem).

Let $\varphi(X,Y)$ denote a fully or partially realizable boolean formula with
input variables in $X=\\{x_{1},\ldots,x_{m}\\}$ and output variables
$Y=\\{y_{1},\ldots,y_{n}\\}$, and let $R_{\varphi}(X)\neq\varnothing$ be its
realizability set. A sequence $g_{1}(X),\ldots,g_{n}(X)$ of boolean functions
is a sequence of _witness functions_ for the $Y$ variables in $\varphi(X,Y)$
if for every assignment ${x}\in R_{\varphi}(X)$, we have that
$\varphi[X\mapsto{x}][y_{1}\mapsto g_{1}({x})]\ldots[y_{n}\mapsto g_{n}({x})]$
holds.

######  Definition 3 (Synthesis).

Given a partially or fully realizable CNF formula $\varphi(X,Y)$ with input
and output variables $X$ and $Y$, the _synthesis problem_ asks to
algorithmically construct a set of _witness functions_ for the $Y$ variables
in terms of the $X$ variables.

###  2.2 Dynamic Programming Concepts - Project-Join Trees

A _binary decision diagrams (BDD)_ [7] is directed acyclic graphs with two
terminals labeled by $0$ and $1$. A BDD provides a canonical representation of
boolean functions (and, by extension, boolean formulas). A (reduced, ordered)
BDD is constructed from a binary decision tree, using a uniform variable
order, of a boolean function by merging identical sub-trees and suppressing
redundant nodes (nodes where both children are the same). Each path from the
root of the BDD to the 1-terminal represents a satisfying assignment of the
boolean function it represents. Based on the combination of BDDs and project-
join trees, which is to be defined below, our dynamic-programming algorithm
solves the boolean synthesis problem.

######  Definition 4 (Project-Join Tree of a CNF formula).

A _project-join tree_ [12] for a CNF formula $\varphi(X)$ is defined as a
tuple $\mathcal{T}=(T,r,\gamma,\pi)$, where

  1. 1.

$T$ is a tree with a set $\mathcal{V}(T)$ of vertices, a set
$\mathcal{L}(T)\subseteq\mathcal{V}(T)$ of leaves, and a root
$r\in\mathcal{V}(T)$

  2. 2.

$\gamma:\mathcal{L}(T)\to\varphi$ is a bijection that maps the leaves of $T$
to the clauses of $\varphi$

  3. 3.

$\pi:\mathcal{V}(T)\setminus\mathcal{L}(T)\to 2^{X}$ is a function which
labels internal nodes with variable sets, where the labels $\\{\pi(n)\mid
n\in\mathcal{V}(T)\setminus\mathcal{L}(T)\\}$ form a partition of $X$, and

  4. 4.

If a clause $c\in\varphi$ contains a variable $x$ that belongs to the label
$\pi(n)$ of an internal node $n\in\mathcal{V}(T)\setminus\mathcal{L}(T)$, then
the associated leaf node $\gamma^{-1}(c)$ must descends from $n$.

A _Graded Project-Join Tree_ [13] is a generalization of project-join trees.

######  Definition 5 (Graded Project-Join Tree of a CNF formula [13]).

A project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$ of a CNF formula
$\varphi(X,Y)$ over variables $X\cup Y$, where $X\cap Y=\varnothing$, is _(
$X$, $Y$)-graded_ if there exist _grades_
$\mathcal{I}_{X},\mathcal{I}_{Y}\subseteq\mathcal{V}(T)$ that partition the
internal nodes $\mathcal{V}(T)\setminus\mathcal{L}(T)$, such that:

  1. 1.

For a node, its grade is always consistent with its labels. i.e., If
$n_{X}\in\mathcal{I}_{X}$ then $\pi(n_{X})\subseteq X$, and if
$n_{Y}\in\mathcal{I}_{Y}$ then $\pi(n_{Y})\subseteq Y$.

  2. 2.

If $n_{X}\in\mathcal{I}_{X}$ and $n_{Y}\in\mathcal{I}_{Y}$, then $n_{X}$ is
not a descendant of $n_{Y}$ in $T$.

Intuitively, in a graded project-join tree, the nodes are partitioned
according to a partition $(X,Y)$ of the variables, with nodes in the $X$ block
always appearing higher than nodes in the $Y$ block. As we shall see, this is
useful for formulas with two different types of quantifiers.

Figure 1 shows an example Graded Project-Join Tree for a CNF formula, along
with intermediate trees produced in the course of the execution of our
synthesis algorithm. In the upcoming sections we will refer back to this
example to illustrate the individual steps of the algorithm related to each
intermediate tree.

(a) A Graded Project-Join Tree Instance

(b) Tree after evaluating node 6

(c) Tree after evaluating node 7

(d) Tree after evaluating node 9

Figure 1: Original and intermediate trees generated by our algorithms for the
CNF example $(x_{1}\lor y_{4}\lor\neg y_{5})\land(\neg x_{3}\lor x_{2}\lor\neg
y_{5})\land(\neg x_{1}\lor x_{2}\lor y_{6})\land(\neg x_{3}\lor x_{1}\lor\neg
y_{4})\land(x_{1}\lor\neg x_{2}\lor x_{3}\lor y_{5})$. The label for each
internal node is denoted by $e$.

##  3 Realizability Checking222Proofs for all lemmas and theorems can be found
in the Appendix A.

Our overall approach has three phases: (1) _planning_ – constructing graded
project-join trees, (2) _realizability checking_ , and (3) _witness-function
synthesis_. The focus in this section is on realizability checking. We
construct the realizability set $R_{\varphi}(X)$ for an input formula
$\varphi(X,Y)$, and then use it to check for full and partial realizability,
as described in Definition 1.

For the planning phase, we use the planner described in [13], which is based
on _tree decomposition_ [24]. Computing minimal tree decomposition is known to
be an NP-hard problem [6], so planning may incur high computational overhead.
Nevertheless, tree-decomposition tools are getting better and better. The
planner uses an _anytime_ tree-decomposition tool, cf. [16], which outputs
tree decompositions of progressively lower width. Deciding when to quit
planning and start executing is done heuristically. In contrast, Factored
RSynth applies a _fixed_ set of fast heuristics, which incurs relatively small
overhead. We discuss the planning overhead further below.

###  3.1 Theoretical Basis and Valuations in Trees

The realizability set $R_{\varphi}(X)$ can be interpreted as a constraint over
the $X$ variables stating the condition that there exists an assignment to the
$Y$ variables that satisfies $\varphi$. In other words,
$R_{\varphi}(X)\equiv(\exists y_{1})\ldots(\exists y_{n})\varphi$, for
$Y=\\{y_{1},\ldots,y_{n}\\}$.

Therefore, we can construct $R$ from $\varphi=\bigwedge_{j}\varphi_{j}$ by
existentially quantifying all $Y$ variables. As observed in [27], however, a
clause that does not contain $y_{i}$ can be moved outside the existential
quantifier $(\exists y_{i})$. In other words, $(\exists
y_{i})\bigwedge_{j}\varphi_{j}\equiv\bigwedge_{y_{i}\not\in
AP(\varphi_{j})}\varphi_{j}\land(\exists y_{i})\bigwedge_{y_{i}\in
AP(\varphi_{j})}\varphi_{j}$, where $AP$ stands for atomic propositions in a
formula. This allows us to perform _early quantification_ to compute $R$ more
efficiently, since applying quantification on the smaller formula
$\bigwedge_{y_{i}\in AP(\varphi_{j})}(\varphi_{j})$ is likely less expensive
computationally than doing so on the full formula
$\varphi=\bigwedge_{j}(\varphi_{j})$.

Inspired by a similar observation in [13], we use the insight that a graded
project-join tree can be employed to guide early quantification. Consider the
following definition, which allows us to interpret a node $n$ in a project-
join tree as a boolean formula:

######  Definition 6 (BDD-Valuations of Nodes in Project Join Tree).

Let $n$ be a node in a graded project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$
with a partition of internal nodes into two grades $\mathcal{I}_{X}$ and
$\mathcal{I}_{Y}$, as defined in Section 2. Let the set of children nodes of
$n$ be denoted by $C(n)$. Let $\llbracket\alpha\rrbracket$ denote the BDD
encoding a boolean expression $\alpha$, and $\exists_{Z}f$ denote the
existential projection on $f$ with respect to variables in $Z$. We now define
a pair of mutually related valuation concepts for nodes in a project-join
tree, interpreting their BDD representations.

The _post-valuation_ of $n$ is defined as

$\texttt{BV}_{\texttt{post}}(\mathcal{T},n)=\begin{cases}\llbracket\gamma(n)\rrbracket,\hskip
28.45274pt&\text{if $n$ is a leaf node}\\\
\exists_{\pi(n)}\texttt{BV}_{\texttt{pre}}(\mathcal{T},n),&\text{if $n$ is an
internal node.}\end{cases}$

The _pre-valuation_ of $n$ is defined as

$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)=\begin{cases}\llbracket\gamma(n)\rrbracket,\hskip
28.45274pt&\text{if $n$ is a leaf node}\\\ \bigwedge_{n^{\prime}\in
C(n)}\texttt{BV}_{\texttt{post}}(\mathcal{T},n^{\prime}),&\text{if $n$ is an
internal node.}\end{cases}$

Intuitively, we evaluate an internal node $n$ by first taking the conjunction
of post-valuations of its children and then existentially quantifying the
variables $\pi(n)$ in its label. The former step generates a pre-valuation,
while the latter produces a post-valuation. We can safely perform
quantification of the variables in the label of $n$ after conjoining, because
every internal node $n$ must satisfy the property that all clauses containing
variables in $\pi(n)$ are descendants of $n$, by the definition of a project-
join tree.

Furthermore, recall that, by the definition of a $(X,Y)$-graded project-join
tree, all nodes in $\mathcal{I}_{Y}$ occur below all nodes in
$\mathcal{I}_{X}$. This allows us to turn Definition 6 into a procedure for
efficiently computing realizability of the CNF formula $\varphi$ using a
graded project-join tree as a guide:

  1. 1.

First, apply Definition 6 to the $\mathcal{I}_{Y}$ nodes of the tree,
producing a project-join tree for $R_{\varphi}(X)\equiv(\exists
y_{1})\ldots(\exists y_{n})\varphi$.

  2. 2.

Inspect this tree for full realizability (see below).

  3. 3.

Apply Definition 6 again in order to check partial realizability (see below).

For the CNF with the graded project-join tree in Figure 1(a), the pre- and
post-valuations for nodes $1,4,5,2,3$ are equivalent to the BDDs representing
their original clauses.
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},6)=\llbracket(x_{1}\lor y_{4}\lor\neg
y_{5})\land(\neg x_{3}\lor x_{1}\lor\neg
y_{4})\rrbracket,\texttt{BV}_{\texttt{post}}(\mathcal{T},6)=(\exists
y_{4})\texttt{BV}_{\texttt{pre}}(\mathcal{T},6)=(x_{1}\lor\neg y_{5}\lor\neg
x_{3}),\texttt{BV}_{\texttt{pre}}(\mathcal{T},7)=(x_{1}\lor\neg x_{2}\lor
x_{3}\lor y_{5})\land(\neg x_{3}\lor x_{2}\lor\neg y_{5})\land(x_{1}\lor\neg
y_{5}\lor\neg x_{3}),\texttt{BV}_{\texttt{post}}(\mathcal{T},7)=(\exists
y_{5})\texttt{BV}_{\texttt{pre}}(\mathcal{T},7)=\llbracket
1\rrbracket,\texttt{BV}_{\texttt{pre}}(\mathcal{T},9)=(\neg x_{1}\lor
x_{2}\lor y_{6}),and\texttt{BV}_{\texttt{post}}(\mathcal{T},9)=(\exists
y_{6})\texttt{BV}_{\texttt{pre}}(\mathcal{T},9)=\llbracket 1\rrbracket$.

##### Notations

We denote the set of children nodes and the set of descendants of $n$ by
$C(n)$ and $D(n)$. Let $\llbracket\cdot\rrbracket$ denote the BDD encoding of
the enclosed expression, and use $\texttt{projn}(B,Z)$ to denote a series of
existential projections on BDD $B$ with respect to variables in set $Z$.

1

Input: : an ($(X,Y)$-graded) project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$
of $\varphi$, and a particular node $n\in\mathcal{V}(\mathcal{T})$

Output: early determination of nullary realizability, otherwise outputs
$\texttt{BV}_{\texttt{post}}(\mathcal{T},n)$ and
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$

2

3if  _$n\in\mathcal{L}(T)$_

$\alpha\leftarrow\llbracket\gamma(n)\rrbracket,\texttt{pre-
BV}(\mathcal{T},n)\leftarrow\alpha$, $\texttt{post-
BV}(\mathcal{T},n)\leftarrow\alpha$// if $n$ is a leaf

4

5 else

6 $\texttt{post-BV}(\mathcal{T},n)\leftarrow\llbracket 1\rrbracket$,
$\texttt{pre-BV}(\mathcal{T},n)\leftarrow\llbracket 1\rrbracket$

7 for  _$n^{\prime}\in C(n)$_ do

8 if  _$\texttt{post-BV}(\mathcal{T},n^{\prime})==\llbracket 0\rrbracket$_

9 $\texttt{pre-BV}(\mathcal{T},n)\leftarrow\llbracket 0\rrbracket$,
$\texttt{post-BV}(\mathcal{T},n)\leftarrow\llbracket 0\rrbracket$

10 return _nullary realizable, no further synthesis needed_

11

12 end if

13 else

14 $\texttt{pre-BV}(\mathcal{T},n)\leftarrow\texttt{pre-
BV}(\mathcal{T},n)\land\texttt{post-BV}(\mathcal{T},n^{\prime})$

15 end if

16

17 if  _$\texttt{pre-BV}(\mathcal{T},n)==\llbracket 0\rrbracket$_

18 $\texttt{post-BV}(\mathcal{T},n)\leftarrow\llbracket 0\rrbracket$

19 return _nullary realizable, no further synthesis needed_

20 end if

21

22 end for

23 $\texttt{post-BV}(\mathcal{T},n)\leftarrow\textnormal{{Projn}}(\texttt{pre-
BV}(\mathcal{T},n),\pi(n))$

24 end if

25return _$\texttt{pre-BV}(\mathcal{T},n),\texttt{post-BV}(\mathcal{T},n)$_

Algorithm 1 $GenericValuation(\mathcal{T},n)$

Algorithm 1 presents a procedure to compute the pre and post-valuations of
Definition 6. In this algorithm pre-valuations are intermediate BDDs used to
compute the post-valuations, but their values are also used in Section 4 for
witness-function synthesis. Post-valuations, meanwhile, are used in Section
3.2 to determine if a given instance has a fully, partially, or unrealizable
domain.

Note that children nodes are always visited before parent nodes, per Algorithm
2. This guarantees that line 1 in GenericValuation is always viable. We now
assert the correctness of the Algorithm 1 by the following theorem.

######  Theorem 3.1.

If a graded project-join tree $\mathcal{T}$ and a particular node $n$ are
given, then (i) $\texttt{BV}_{\texttt{post}}(\mathcal{T},n)$ and (ii)
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$ returned by Algorithm 1 are as
defined in Definition 6.

######  Theorem 3.2.

Given a graded project-join tree $\mathcal{T}$ of a CNF formula $\varphi$, let
${{X_{\texttt{leaves}}}(\mathcal{T})}$ denote the set of highest level nodes
$n\in\mathcal{T}$ such that $\pi(n)\subseteq Y_{\varphi}$. Then the
realizability set $R_{\varphi}(X)$ can be represented by the conjunction
$\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$
of BDDs returned by Algorithm 1.

The pair of post and pre valuations defined in this section offer support for
both realizability checking and synthesis, respectively. Section 3.2 applies
$\texttt{BV}_{\texttt{post}}$ for realizability checking, and we show in
Section 4 how $\texttt{BV}_{\texttt{pre}}$ is used in witnesses construction.

###  3.2 Determining Nullary, Partial and Full Realizability

Using the post-valuations of nodes computed in Algorithm 1 as the result of
projecting variables on the conjunction of children nodes, we can construct
the realizability set and determine if it is full, partial or empty. In
practice, we represent the realizability set as a conjunction of BDDs, where
an input is in the set if it satisfies all BDDs in the conjunction.

##### Notation

Let $\texttt{XLeaves}(\mathcal{T})$ denote the set of $Y$ internal nodes whose
parents are not in $\mathcal{I}_{Y}$. This set is easily obtainable by means
such as graph-search algorithms.

We start by applying the pair of valuations computed in Algorithm 1 to the
first layer of $\mathcal{I}_{Y}$ nodes in the graded tree; that is, all
internal nodes in $\mathcal{I}_{Y}$ whose parent is not in $\mathcal{I}_{Y}$.
By replacing these nodes with leaves labeled by their post-valuation, we
obtain a project-join tree $\mathcal{T}_{X}$ for the formula $(\exists
y_{1})\ldots(\exists y_{n})\varphi$, which, as explained in Section 3.1,
corresponds to the realizability set. This procedure is implemented in
Algorithm 2.

In the case of the example formula in Figure 1, once we obtain the pre- and
post-valuations from Algorithm 1, $B_{pureX}=\llbracket 1\rrbracket$ and $b=1$
from the post-valuations $\texttt{BV}_{\texttt{post}}(\mathcal{T},7)$ (Figure
1(c)) and $\texttt{BV}_{\texttt{post}}(\mathcal{T},9)$ (Figure 1(d)) on
XLeaves. Hence we get full realizability.

Note that the formula $\varphi$ is fully realizable if and only if the
conjunction of the leaves in $\mathcal{T}_{X}$ is $1$, which holds true if and
only if all leaves are $1$. Therefore, at the end of Algorithm 2 we are also
able to answer whether $\varphi$ is fully realizable. Note also that if any of
the leaves is $0$, then their conjunction is $0$, meaning that $\varphi$ is
nullary realizable. Therefore, in some cases it might be possible to detect
nullary realizability in this step. If the formula is not fully realizable and
nullary realizability is not detected, then $\mathcal{T}_{X}$ is passed to the
next step to test partial realizability.

1

2

Explanation : This algorithm computes pre and post-valuations of nodes in the
leaves and in the $Y$ partition, simultaneously in the bottom-up manner checks
if the realizability set is tautology (fully realizable) or an _obvious_
negation (not realizable). If neither applies, it passes the new tree to
Algorithm 3.

Input: $\mathcal{T}=(T,r,\gamma,\pi)$: an $(X,Y)$-graded project-join tree
with internal nodes partitioned into $\mathcal{I}_{X}$, $\mathcal{I}_{Y}$.

Output: Returns _full_ or _nullary realizability_ if can determine by the end
of this algorithm. Otherwise, a project-join tree $\mathcal{T}_{X}$ of
$(\exists_{y\in Y}y)\varphi$ is passed to Algorithm 3 for further determining
between _partial_ and _nullary realizability_.

3

4$B_{pureX}\leftarrow$conjunction of clauses without $y$ variables

5 if  _$B_{pureX}==\llbracket 0\rrbracket$_ return _nullary realizable_

6 $\mathcal{T}_{X}\leftarrow\mathcal{T}$, $b\leftarrow 1$

7 if  _${\mathcal{I}_{Y}}$ is empty_ return _fully realizable_

8

9for  _$n\in\mathcal{I}_{Y}\cup\mathcal{L}(T)$_ do

10

$\texttt{GenericValuation}(\mathcal{T},n)$ // in bottom-up order from leaves
to root

11 if
_$\textnormal{{$\texttt{BV}_{\texttt{pre}}$}}(\mathcal{T}_{X},n)==\llbracket
0\rrbracket$_ return _nullary realizable_

12

13 end for

14

15for  _$n\in\textnormal{{XLeaves}}(\mathcal{T})$_ do

16

17 if
_$\textnormal{{$\texttt{BV}_{\texttt{post}}$}}(\mathcal{T}_{X},n)==\llbracket
0\rrbracket$_ return _nullary realizable_

18 else if
_$\textnormal{{$\texttt{BV}_{\texttt{post}}$}}(\mathcal{T}_{X},n)\neq\llbracket
1\rrbracket$_

19 $b\leftarrow 0$

20

21 end if

22

$\mathcal{V}(T_{X})\leftarrow\mathcal{V}(T_{X})\setminus D(n)$// remove the
descendants of $n$ from $\mathcal{T}_{X}$

23

$\mathcal{L}(T_{X})\leftarrow\mathcal{L}(T_{X})\cup\\{n\\}$// add $n$ to
leaves of $\mathcal{T}_{X}$

24

25 end for

26if  _$b==1$ and $B_{pureX}==\llbracket 1\rrbracket$_ return _fully
realizable_

return __HighValuation($\mathcal{T}_{X}$)__

Algorithm 2 $LowValuation(\mathcal{T})$

######  Theorem 3.3.

Given a graded project-join tree $\mathcal{T}$ for a CNF formula $\varphi$,
Algorithm 2 returns full realizability if and only if the formula $(\forall
X)(\exists Y)\varphi(X,Y)$ is true. And the algorithm returns nullary
realizability, if and only if the formula $(\exists X)(\exists Y)\varphi(X,Y)$
is false.

When the formula is not fully realizable, we proceed to pass the tree returned
by Algorithm 2 to Algorithm 3, which then distinguishes partial realizability
from nullary realizability. It does this by simply using Algorithm 1 to
compute the post-valuation of the root of $\mathcal{T}_{X}$.

In the case of the example in Figure 1, for this formula, we do not need to
check Algorithm 3 because by Algorithm 2 full realizability is returned.

1

2

Input: $\mathcal{T}_{X}=(T_{X},r_{X},\gamma_{X},\pi_{X})$ is the generated
tree from Algorithm 2, which is the project-join tree generated by projecting
out all $Y$ variables from the $(X,Y)$-graded tree for CNF $\varphi$.

Output: whether or not $\varphi$ is partially realizable

3

for  _$n\in\mathcal{I}_{X}$ // for all nodes in $I_{X}$ partition _

4 do

$\texttt{GenericValuation}(\mathcal{T},n)$ // in bottom-up order leaves to the
root

5

6 end for

7if
_$\textnormal{{$\texttt{BV}_{\texttt{post}}$}}(\mathcal{T}_{X},r_{X})==\llbracket
0\rrbracket$_ return _nullary realizable_

8 else return _partially realizable_

Algorithm 3 $HighValuation(\mathcal{T}_{X})$

Since this corresponds to taking the conjunction of the leaves (which are
themselves the post-valuation of the first layer of $Y$ nodes) and
existentially quantifying the $X$ variables, the result is $1$ if $\varphi$ is
partially realizable, and $0$ if not. Built on top of Theorem 3.2, we
formulate the correctness of the algorithm:

######  Theorem 3.4.

Given a CNF formula $\varphi$ and its graded project-join tree $\mathcal{T}$,
if we generate $\mathcal{T}_{X}$ by Algorithm 2, then Algorithm 3 returns the
correct status of realizability of $\varphi$.

##  4 Synthesis of Witness Functions

We now move to the third phase of our boolean-synthesis approach, where we
construct boolean expressions for the output variables, which are the witness
functions. More precisely, when the realizability set $R_{\varphi}(X)$, as
defined in Section 3, is nonempty, we proceed to witness construction. We now
formally define the concept of witnesses, in the context where the boolean
synthesis problem is given as a CNF specification and reduced ordered BDDs are
used for boolean-function representations.

The following lemma describes the _self-substitution method_ for witness
construction.

######  Lemma 1.

[15] Let $X$ be a set of input variables and $y$ a single output variable in a
Boolean CNF formula $\varphi(X,y)$ with $R_{\varphi}(X)\neq\varnothing$. Then
$g(X)=\varphi(X,y)[y\mapsto 1]$ is a witness for $y$ in $\varphi(X,y)$.

We now show how to extend this method to multiple output variables, building
towards an approach using graded project-join trees.

###  4.1 Monolithic Approach

The synthesis procedure here builds on the condition that partial
realizability is known, provided by the algorithms in Section. 3. While
solvers constructed by related works, as discussed in Section. 1, apply only
to fully realizable formulas, we show here that synthesis can also be
performed to obtain witness functions in the case of partial realizability.

As a stepping stone towards graded-tree-based synthesis, we first explain how
witness functions are constructed in the monolithic case. We review the basic
framework in [15], where the realizability set $R_{\varphi}(X)$ is obtained
through iterative quantification on $y_{n}$ to $y_{1}$, while witnesses are
obtained via iterative substitution on $y_{1}$ to $y_{n}$.

Denote the BDD encoding the original CNF formula $\varphi(X,Y)$ to be
$B_{\varphi}(X,Y)$. Then, a series of intermediate BDDs can be defined on the
way of obtaining the realizability sets $R_{\varphi}(X)$:

$\displaystyle B_{n}(X,y_{1},\ldots,y_{n})\equiv B_{\varphi},$
$\displaystyle\ldots$ $\displaystyle B_{i}(X,y_{1},\ldots,y_{i})\equiv(\exists
y_{i+1})B_{i+1},$ $\displaystyle\ldots$ $\displaystyle B_{0}(X)\equiv(\exists
y_{1})B_{1}$

Finally, the realizability set $R_{\varphi}(X)$ is $B_{0}(X)$.

Note that existential quantification proceeds here _inside-out_ , since
larger-indexed output variables are quantified before smaller-indexed output
variables. Witness construction, on the other hand, proceeds _outside-in_ :
witnesses are constructed in the reverse direction starting from the smallest-
indexed output variable $y_{1}$. The witnesses for variables
$y_{1},\ldots,y_{i-1}$ are substituted into $B_{i}$, from which we then
construct the next witness $g_{i}$. Using the witness given by Lemma 1, we
have:

$g_{1}$ is computed from: $B^{\prime}_{1}(X,y_{1})=B_{1}(X,y_{1}),$ via
$g_{1}=B^{\prime}_{1}[y_{1}\mapsto 1];$

$\ldots$

$g_{i}$ is computed from:
$B^{\prime}_{i}(X,y_{i})=B_{i}(X,y_{1},\ldots,y_{i})[y_{1}\mapsto g_{1}]$
$\ldots[y_{i-1}\mapsto g_{i-1}],$ via
$g_{i}=B^{\prime}_{i}(X,y_{i})[y_{i}\mapsto 1].$

The following lemma is based on [15].

######  Lemma 2.

If $R_{0}(X)\not=\varnothing$, then the $g_{i}$’s above are witness functions
for $Y$ in $\varphi(X,Y)$.

As the witnesses above are computed using the self-substitution method from
Lemma 1, each formula can have potentially many different witnesses. The
correctness of the procedure does not depend on which witness is used. RSynth
[15] applies the SolveEqn function of the CUDD package to compute a block of
witnesses at once by essentially the procedure above. The procedure produces
several witnesses for each variable, from which we chose one witnesses (by
setting a parameter to 1).

The above monolithic synthesis framework was generalized in [27] to the case
where the formula $\varphi$ is given as a conjunction of _factors_. A factor
can be a formula, for example, a single clause or a conjunction of clauses
(called a “cluster” in that work). In that case, the principle of early
quantification mentioned in Section 3.1 can be applied. See Appendix B for
details. As shown in [27], the tool, _Factored RSynth_ , generally outperforms
RSynth.

In the following section, we describe a factored approached to witness
construction using graded project-join trees.

###  4.2 Synthesis Using Graded Project-Join Trees

As we saw above, in the monolithic setting we compute the realizability set by
quantifying the $Y$ variables inside out, and then computing the witness
function for these variables outside in. In the graded project-tree framework,
we saw that the realizability set is computing by quantifying the $Y$
variables bottom-up.

Our framework works for both partial and fully realizable cases. We first
compute realizability sets going _bottom up_ the graded project-join tree for
$\varphi$ as in Section 3. We now show that the witness functions for the $Y$
variables can then be constructed by iterated substitution _top-down_. In
other words, we first compute the witnesses for the variables in the labels of
internal nodes at higher levels, and then propagate those down toward the
leaves. We compute witnesses from the pre-valuation
$\texttt{BV}_{\texttt{pre}}$ of a node in the tree, computed as in Algorithm
1. Note that, in contrast to the bottom-up realizability and top-down
synthesis described here, in projected model counting, where graded project-
join trees were introduced [13], the trees are processed fully in a bottom-up
fashion.

The following lemma is crucial to our approach.

######  Lemma 3.

Let $m$ and $n$ be two different internal nodes of a graded project-join tree
$\mathcal{T}$ such that $n$ is not a descendant of $m$. Then no variable in
$\pi(m)$ appears in $\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$.

We can derive from Lemma 3 the essential relation among witness functions for
different variables: since the witness for a variable $y_{i}\in\pi(n)$ is
computed from $\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$, this witness can
only depend on the witnesses of output variables $y_{j}\in\pi(m)$ such that
$n$ is a descendant of $m$.

Based on these insights, we present in Algorithm 4 our dynamic-programming
synthesis algorithm for producing the witnesses $g_{y}(X)$ for each output
variable $y$, represented by a BDD $W_{y}(X)$. The algorithm starts at the
top-most layer of $Y$ nodes, those whose parents are $X$ nodes, represented by
the set called XLeaves (line 4). For each node $n$ in this set (line 4), we
compute the set of witnesses $\\{W_{y}\mid y\in\pi(n)\\}$ from
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$ (line 4) using the monolithic
procedure from Section 4.1 (represented by the CUDD function
$\texttt{SolveEqn}(\pi(n),\texttt{BV}_{\texttt{pre}}(\mathcal{T},n))$,
mentioned in that section). Note that, since the tree is graded, these nodes
do not descend from any $Y$ nodes. Therefore, by Lemma 3, these witnesses
depend only on the $X$ variables.

As we compute the witnesses for a node, we add all of its (non-leaf) children
to the set of nodes to visit (line 4), representing the next layer of the
tree. After all nodes in the current set have been processed, we repeat the
process with the new layer (line 4).

1

Notation : $C(n)$: set of the children nodes of $n$

Notation : $D(n)$: set of the descendant nodes of $n$

Notation : $W_{y}$: BDD representing the witness of variable $y$

2

Notation : $\llbracket\alpha\rrbracket$: the BDD representation of boolean
expression $\alpha$

3

Notation : $\textnormal{{XLeaves}}(\mathcal{T})$ as in Algorithm 2

4

Input: $\mathcal{T}=(T,r,\gamma,\pi)$: the original $(X,Y)$-graded project-
join tree of CNF $\varphi$

Input: BDDs $\texttt{BV}_{\texttt{pre}}(m)$ for all $m\in\mathcal{I}_{Y}$

5

Output: a series of BDDs $W_{y},\forall y\in Y$, encoding the witness
functions for output variables

6

7$\texttt{synthNodes}\leftarrow\textnormal{{XLeaves}}(\mathcal{T})$

8 while  _$\texttt{synthNodes}\neq\\{\\}$_ do

// from top-down order from the root to leaves

9 for  _all $n\in\texttt{synthNodes}$_ do

10 for  _$n^{\prime}\in C(n)$_ do

11 if  _$n^{\prime}$ is not a leaf_

12 add $n^{\prime}$ to synthNodes

13

14 end if

15

16 end for

// monolithic algorithm presented in Section 4.1

17 $\\{W_{y}\mid
y\in\pi(n)\\}\leftarrow\texttt{SolveEqn}(\pi(n),\texttt{BV}_{\texttt{pre}}(\mathcal{T},n))$

18

19 for  _$n^{\prime\prime}\in D(n)$_ do

20 for  _all $y\in\pi(n)$_ do

// substitute new synthesized $y$ by their witnesses $W_{y}$ in the BDD
representing the pre-valuation of descendants $n^{\prime\prime}$

21
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n^{\prime\prime})\leftarrow\texttt{BV}_{\texttt{pre}}(\mathcal{T},n^{\prime\prime})[y\mapsto
W_{y}]$

22

23 end for

24

25 end for

26

27 end for

28

29 end while

30return _$W_{y},\forall y\in Y$_

Algorithm 4 ${DPSynth}(\mathcal{T})$

This continues until the set of children is empty (line 4). Note that, since
for each node $n$ we apply the monolithic synthesis procedure only to the
variables in $\pi(n)$, the witnesses can be dependent on the $Y$ variables of
its ancestors. Therefore, we finish the algorithm by iterating over the new
synthesized witnesses $W_{y}$ and substituting each into the pre-valuation of
descendant nodes that are computed later (lines 4-4). Note that this
overapproximates the set of dependencies on $y\in\pi(n)$ of the witnesses for
$y^{\prime}\in\pi(n^{\prime\prime})$ for $n^{\prime\prime}\in D(n)$, but since
$W_{y^{\prime}}[y\mapsto W_{y}]\equiv W_{y^{\prime}}$ when $y$ does not appear
in $W_{y^{\prime}}$, the result is still correct. At the end of this
procedure, all $W_{y}$ will be dependent only in the input variables $X$.

Continuing with the running example for the problem in Figure 1, once full
realizability is detected, we apply Algorithm 4 and construct the witnesses in
top-down manner. First, we get the witness $g_{6}=1$ for $y_{6}$ by
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},9)=\llbracket(\neg x_{1}\lor x_{2}\lor
y_{6})\rrbracket$. Then we construct the witness $g_{5}=(x_{1}\land
x_{2})\lor\neg x_{3}$ for $y_{5}$ by substituting $y_{5}=1$ in
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},7)=\llbracket(x_{1}\lor\neg x_{2}\lor
x_{3}\lor y_{5})\land(\neg x_{3}\lor x_{2}\lor\neg y_{5})\land(x_{1}\lor\neg
y_{5}\lor\neg x_{3})\rrbracket$. After that, we go to node $6$ and get
$g_{4}=x_{1}\lor\neg x_{3}$ from
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},6)=\llbracket(x_{1}\lor y_{4}\lor\neg
y_{5})\land(\neg x_{3}\lor x_{1}\lor\neg y_{4})\rrbracket$. By the algorithm,
we would need to substitute $g_{5}$ into
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},6)$ before computing $g_{4}$, but
since for this specific CNF $g_{4}$ is not actually dependent on $g_{5}$, this
does not change the witness. The witnesses are correct by
$\varphi[y_{4}\mapsto g_{4}][y_{5}\mapsto g_{5}][y_{6}\mapsto g_{6}]=1$.

The following theorem proves the correctness of witnesses constructed. First,
it is easy to see by an inductive argument that a witness is synthesized for
all output variables: all $Y$ nodes that do not descend from other $Y$ nodes
are included in the set processed in the first iteration, and if a node is
processed in one iteration, all of its children are included in the set for
the next iteration. Since the tree is graded, we have processed all of the $Y$
nodes, and since every output variable $y$ is in the label of some node, a
witness $W_{y}$ is computed for every $y$. Then, the following theorem states
the correctness of the witnesses constructed:

######  Theorem 4.1.

Algorithm 4 returns a set of BDDs encoding the witness functions for output
variables that satisfy the given CNF $\varphi$, assuming that
$\texttt{SolveEqn}(\pi(n)$, $\texttt{BV}_{\texttt{pre}}(\mathcal{T},n))$
returns correct witnesses for the variables in $\pi(n)$ in
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$.

##  5 Experimental Evaluation

###  5.1 Realizability-Checking Phase

Methodology: To examine our dynamic-programming graded-project-join-tree-based
approach for boolean realizability, we developed a software tool, _DPSynth_ ,
which implements the theoretical framework described above. We choose to
compare _DPSynth_ to _Factored RSynth_ , which as explained in the
introduction is the closest existing tool, also being based on decision
diagrams and outputting the realizability set along with the witnesses. Prior
work [27] already demonstrated that RSynth practically never outperforms
Factored RSynth, while Factored RSynth typically outperforms RSynth, so we
compare in this paper to Factored RSynth. (See Section 5.4 for an additional
comparison to a non-decision-diagram tool.) We measured the time and space
performance for determining realizability on a set of mature benchmarks,
described below. The experiments aim at answering the following research
questions:

  * •

Does our DP-based solution improve execution time for realizability checking?
Does the overhead of _planning_ time investment in DPSynth get paid off?

  * •

How does the relative weight of planning overhead vary between small and large
input instances?

  * •

How does DPSynth improve the scalability of realizability checking?

(Tree width is one of the critical parameters impacting the performance of the
graded project-jointree-based approach in running time. We discuss this issue
further in separate a subsection.)

We selected 318 benchmarks that are neither too easy (taking less than 1ms)
not too hard (such that the whole benchmark family is not solvable by either
solver) from the data set of forall-exists $\Pi^{P}_{2}$ CNFs from the QBFEVAL
[22] datasets from 2016 to 2019, without any more selection criteria, as the
editions of QBFEVAL in 2020 and 2022 do not include additional 2QBF instances
or tracks other than those included by 2019. Families of benchmarks that our
experiments run on include _reduction-finding query, mutexP, qshifter, ranking
functions, sorting networks, tree and fix-point detection_ families, and also
two additional scalable families, consisting of parametric integer
factorization and subtraction benchmarks from [3, 2].

Among the full benchmark suite, at least $33\%$ of the $285$ instances where
realizability can be checked by either DPSynth or factored RSynth are
partially realizable. In the benchmarks for which both tools are able to
synthesize a complete group of witnesses, $28\%$ are partially realizabile.
(No benchmark in the suite is identified as nullary realizable). We conclude
that partial realizability is a significant issue in Boolean synthesis. We now
present the experimental results analyzed according to the research questions
above

For each benchmark instance, we run the FlowCutter-based planner until we
obtain the first tree decomposition, and we declare timeout if no tree
decomposition is generated within ten minutes, in which case, the instance is
marked unsolved. Otherwise, we take the first tree generated, and proceed to
the execution phase of DPSynth, which includes BDD compilation, realizability
checking, and synthesis of witnesses. The maximal time limit for each instance
is set to be two hours for the execution phase. We measure planning time,
execution time, and end-to-end time.

Our implementation is based on the CUDD Library [26] with BDD operations, and
the FlowCutter tree-decomposition tool [20]. In our implementation, BDD
variables are in MCS order [27]. This ordering is based on the primal graph of
the input clause set, and was also used by Factored RSynth.

We ran the experiments on Rice University NOTS cluster, which assigns the jobs
simultaneously to a mix of HPE SL230s, HPE XL170r, and Dell PowerEdge C6420
nodes, each of which has 16-40 cores with 32-192 GB RAM that runs at 2.1-2.60
GHz. Each solver-benchmark combination ran on a single core.

Experimental Results: Our goal in this paper was to compare the performance of
the fast, CSP-based, formula-partitioning techniques of Factored RSynth [27],
to the heavier-duty formula-partitioning techniques based on tree
decomposition described above. For a fair comparison, the charts do not
include data points for those instances that timed out for one of the solvers.
(In total, DPSynth was able to solve 126 instances end-to-end, and RSynth
111.) Thus, our experiments compare _DPSynth_ to Factored RSynth. Our
conjecture is that such heavier-duty techniques pay off for larger formulas,
but not necessarily for smaller formulas.

(a) Time Comparison

(b) Scalable Families Time Growth

Figure 2:

Figure 2(a) shows overall running-time comparison between DPSynth and Factored
RSynth for realizability checking. A clear pattern that emerges is there is a
difference in relative performance between very small problems (solvable
within $1$ millisecond) and larger problems. DPSynth underperforms Factored
RSynth on small instances, but outperforms on larger instances and the
difference increases exponentially as input size grows. We conclude that
planning overhead dominates on small input instances, but that effect fades
off as instances get larger and the planning pays off. In memory usage
comparison444The charts for space consumption for both phases are in the
Appendix C. – using peak node count as a measurement – DPSynth uses less
memory than Factored RSynth. Here the graded project-join-tree approach is
advantageous, and planning incurs no overhead.

To evaluate scalability, we take the scalable benchmark families mentioned
previously, and compare the logarithmic-scale slope in their running time as
sizes of benchmarks increase. As indicated in Figure. 2(b), DPSynth scales
exponentially better than Factored RSynth, as the planning overhead fades in
significance as instances grow. We see a steeper slope on the exponential
scale in DPSynth trends over factored RSynth. Some data points for larger
benchmarks in the families (horizontal coordinates $3,4,5$ on chart) are
missing because factored RSynth is not able to finish solving these instances
in realizability-checking phase within the time limit.

###  5.2 Synthesis

The experiments on synthesis of witnesses answer the following research
questions:

  * •

How does DPSynth compare in execution time to factored RSynth?

  * •

Does the influence of _planning_ investment reduces as problem gets large?

  * •

What do we see in growth of tree widths and synthesis execution time?

Using the same set of benchmarks and setting under the methodology as in
Section 5.1, we applied our synthesis procedure to both fully realizable and
partially realizable benchmarks. This broadens the scope of Boolean synthesis
beyond that of fully realizable benchmarks, which is the scope of earlier
work, as discussed above. Regarding end-to-end synthesis (planning,
realizability checking, and synthesis, combined) DPSynth outperforms Factored
RSynth in running time as illustrated in Figure 3(a). As with realizability
checking, planning overhead dominates for small instances, as discussed in
Section 3, but DPSynth solves large benchmarks faster and shows significant
advantage as problem size increases, once the planning overhead fades in
significance. In memory usage there is consistent relative performance of
DPSynth vs. Factored RSynth.

We again selected three scalable benchmark families, scaled based on a
numerical parameter. As shown in Figure 3(b), DPSynth scales exponentially as
benchmark size increases. Similarly to the case in realizability checking, the
missing data points on larger benchmarks in the scalable families presented by
the dashed lines are caused by the timeouts by factored RSynth.

While DPSynth shows performance advantage over Factored RSynth with respect to
our benchmark suite, one cannot conclude that DPSynth always dominates
Factored RSynth. This is because DPSynth involves computationally nontrivial
planning phase, and it is not possible to say definitively that the planning
overhead always pays off.

(a) Synthesis Time: DPSynth vs. Factored RSynth

(b) Scalable Families Comparison

Figure 3:

We can conclude, however, that DPSynth is an important addition to the
portfolio of algorithms for boolean synthesis.

###  5.3 Tree Widths and Realizability

Graded project-join trees enable the computation of the realizability set in a
way that minimizes the set of support of intermediate ADDs (Algebraic Decision
Diagrams), saving time and memory. But computing these trees is a heavy
computational task. In this section, we study the impact of tree width on
realizability checking.

(a) DPSynth Realizability Time as Widths Increases

(b) DPSynth / Factored RSynth Realizability Time Ratio as Widths Increases

Figure 4:

Figure 4(a) presents the range of realizability time run by DPSynth along
increasing tree widths. As we see, increases in _tree widths_ implies an
increase in running time for realizability-checking. Figure 4(b), depicts the
ratio of realizability time, computed by that of DPSynth over Factored RSynth,
with respect to tree width, for problem instances that can be solved by both
solvers. As treewidth increases, the over-performance of DPSynth over Factored
RSynth increases, as planning overhead decreases in significance for higher-
treewidth instances.

Synthesis execution time has similar relation with tree widths.

###  5.4 Comparison with Non-BDD-Based Synthesis

To complement out evaluation, we include additional experiments to verify
whether DPSynth is competitive with non-BDD-based synthesis solvers, as
motivated in Section 1. We compare with Manthan [17], a leading tool that is
not based on decision diagrams, and find that DPSynth performs favorably.

We present a general picture by the following table, which shows the overall
strength of the dynamic-programming decision-diagram approach, by measuring
the time and space usage of experiments on the dataset selected from
QBFEVAL’16 to QBFEVAL’19. DPSynth and Manthan each is able to solve some
benchmarks that the other does not solve.

In order to compare the running time, we compare against Manthan using the
DPSynth _end-to-end synthesis_ time, which is the sum of tree-decomposition
time, compilation, realizability-checking time, and synthesis time.

As the overall picture of synthesis solving, DPSynth shows a better time
performance on most instances. DPSynth and Manthan each has strength on some
instances, but the number of benchmarks that only DPSynth solves is larger
than those solved only by Manthan. On those that are solved by both, DPSynth
takes less time in most of them. See Appendix D for more illustrative data on
specific fully and partially-realizable benchmarks.

| Number of benchmarks
---|---
solved by Manthan | 79
solved by DPSynth | 102
solved by both Manthan and DPSynth | 70
solved by Manthan but not by DPSynth | 9
solved by DPSynth but not by Manthan | 32

##  6 Concluding Remarks

To summarize the contribution in this work, we propose a novel symbolic
dynamic programming approach for realizability checking and witness
construction in boolean synthesis, based on graded project-join trees. The
algorithm we propose here combine a bottom-up realizability-checking phase
with a top-down synthesis phase. We demonstrated experimentally that our
approach, implemented in the DPSynth tool, is powerful and more scalable than
the approach based on CSP heuristics (Factored RSynth). Another crucial
contribution of this work is the inclusion of partial realizability checking,
which applies to 30% of the total number of benchmarks. As we explain in
introduction, this consideration is motivated by the need in modular circuit
design and temporal synthesis to locate the scope of realizable inputs in
iterative constructions.

There are many directions for future work. Variable ordering is a critical
issue in decision-diagram algorithms, and should be explored further in the
context of our approach. In particular, dynamic variable ordering should be
investigated [25]. Also, in our work here we used high-level API of the BDD
package CUDD, but it is possible that performance gains can be obtained by
using also low-level BDD-manipulating APIs. The question of how to provide
certificates of unrealizability also needs to be explored, c.f., [9, 8].

As mentioned earlier, quantifier elimination is a fundamental algorithmic
component in temporal synthesis [30]. Tabajara and Vardi explored a factored
approach for temporal synthesis [28]. It would be worthwhile to explore also
the graded project-tree approach for boolean synthesis in the context of
factored temporal synthesis. Finally, quantifier elimination is also a
fundamental operation in symbolic model checking [11] and partitioning
techniques have been explored in that context [10]. Therefore, exploring the
applicability of our dynamic-programming approach in that setting is also a
promising research direction.

####  6.0.1 Acknowledgements

This work was supported in part by NSF grants IIS-1527668, CCF-1704883,
IIS-1830549, CNS-2016656, DoD MURI grant N00014-20-1-2787, an award from the
Maryland Procurement Office, the Big-Data Private-Cloud Research
Cyberinfrastructure MRI-award funded by NSF under grant CNS-1338099 and by
Rice University’s Center for Research Computing (CRC).

## References

  * [1] Akshay, S., Arora, J., Chakraborty, S., Krishna, S., Raghunathan, D., Shah, S.: Knowledge compilation for boolean functional synthesis. In: 2019 Formal Methods in Computer Aided Design (FMCAD). pp. 161–169. IEEE (2019)
  * [2] Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What’s hard about boolean functional synthesis? In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 251–269. Springer (2018)
  * [3] Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: Boolean functional synthesis: hardness and practical algorithms. Formal Methods in System Design 57(1), 53–86 (2021)
  * [4] Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebric decision diagrams and their applications. Formal methods in system design 10(2), 171–206 (1997)
  * [5] Bellman, R.: Dynamic programming. Science 153(3731), 34–37 (1966)
  * [6] Bodlaender, H.L., Bonnet, É., Jaffke, L., Knop, D., Lima, P.T., Milanič, M., Ordyniak, S., Pandey, S., Suchỳ, O.: Treewidth is np-complete on cubic graphs (and related results). arXiv preprint arXiv:2301.10031 (2023)
  * [7] Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE TC 100(8), 677–691 (1986)
  * [8] Bryant, R.E., Heule, M.J.: Dual proof generation for quantified boolean formulas with a bdd-based solver. In: CADE. pp. 433–449 (2021)
  * [9] Bryant, R.E., Heule, M.J.: Generating extended resolution proofs with a bdd-based sat solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 76–93. Springer (2021)
  * [10] Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transistion relations. In: Proc. IFIP 10.5 Int’l Conference on Very Large Scale Integration. IFIP Transactions, vol. A-1, pp. 49–58. North-Holland (1991)
  * [11] Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and computation 98(2), 142–170 (1992)
  * [12] Dudek, J.M., Phan, V.H.N., Vardi, M.Y.: DPMC: weighted model counting by dynamic programming on project-join trees. In: Proc. 26 Int’l Conf. on Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, vol. 12333, pp. 211–230. Springer (2020)
  * [13] Dudek, J.M., Phan, V.H.N., Vardi, M.Y.: Procount: Weighted projected model counting with graded project-join trees. In: Li, C., Manyà, F. (eds.) Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12831, pp. 152–170. Springer (2021)
  * [14] Dudek, J.M., Phan, V.H., Vardi, M.Y.: ADDMC: weighted model counting with algebraic decision diagrams. In: AAAI. vol. 34, pp. 1468–1476 (2020)
  * [15] Fried, D., Tabajara, L.M., Vardi, M.Y.: BDD-based Boolean functional synthesis. In: Proc. 28th Int’l Conf. on Computer Aided Verification. Part II. Lecture Notes in Computer Science, vol. 9780, pp. 402–421. Springer (2016)
  * [16] Gogate, V., Dechter, R.: A complete anytime algorithm for treewidth. arXiv preprint arXiv:1207.4109 (2012)
  * [17] Golia, P., Roy, S., Meel, K.S.: Manthan: A data-driven approach for boolean function synthesis. In: International Conference on Computer Aided Verification. pp. 611–633. Springer (2020)
  * [18] Golia, P., Slivovsky, F., Roy, S., Meel, K.S.: Engineering an efficient boolean functional synthesis engine. In: 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). pp. 1–9. IEEE (2021)
  * [19] Hachtel, G.D., Somenzi, F.: Logic synthesis and verification algorithms. Springer Science & Business Media (2007)
  * [20] Hamann, M., Strasser, B.: Graph bisection with pareto-optimization. In: Goodrich, M.T., Mitzenmacher, M. (eds.) Proceedings of the Eighteenth Workshop on Algorithm Engineering and Experiments, ALENEX 2016, Arlington, Virginia, USA, January 10, 2016. pp. 90–102. SIAM (2016)
  * [21] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th annual Design Automation Conference. pp. 530–535 (2001)
  * [22] Narizzano, M., Pulina, L., Tacchella, A.: The QBFEVAL web portal. In: Proc. 10th European Conf. on Logics in Artificial Intelligence. Lecture Notes in Computer Science, vol. 4160, pp. 494–497. Springer (2006)
  * [23] Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9710, pp. 375–392. Springer (2016)
  * [24] Robertson, N., Seymour, P.D.: Graph minors. x. obstructions to tree-decomposition. Journal of Combinatorial Theory, Series B 52(2), 153–190 (1991)
  * [25] Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD). pp. 42–47. IEEE (1993)
  * [26] Somenzi, F.: CUDD: CU Decision Diagram Package Release 3.0.0. University of Colorado at Boulder (2015)
  * [27] Tabajara, L.M., Vardi, M.Y.: Factored boolean functional synthesis. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. pp. 124–131. IEEE (2017)
  * [28] Tabajara, L.M., Vardi, M.Y.: Partitioning techniques in ltlf synthesis. In: Int’l Joint Conference on Artificial Intelligence (2019)
  * [29] Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety ltl synthesis. In: Proc. 13th Int’l Haifa Verification Conference. Lecture Notes in Computer Science, vol. 10629, pp. 147–162. Springer (2017)
  * [30] Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic ltlf synthesis. In: Proc. 26th Int’l Joint Conference on Artificial Intelligence. pp. 1362–1369. ijcai.org (2017)

##  Appendix 0.A Proofs

###  0.A.1 Proof of Theorem. 3.1

###### Proof.

We first prove the correctness of post-valuations computed. _Case 1_ : If $n$
is a leaf in $\mathcal{T}$, $n\in\mathcal{L}(T)$, the returned
$\texttt{BV}_{\texttt{post}}(\mathcal{T},n)$ encodes $\gamma(n)$ in line 5,
which is the clause represented by $n$. This is the same BDD as
$\texttt{BV}_{\texttt{post}}(\mathcal{T},n)$ in Definition 6.

_Case 2_ : Otherwise, we just need to show in the loop in line 9-12, BDD
$\texttt{BV}_{\texttt{post}}(\mathcal{T},n)$ is always equivalent to the
conjunction $\bigwedge_{n^{\prime}\in
C(n)}\texttt{BV}_{\texttt{pre}}(\mathcal{T},n^{\prime})$. As in Def. 6, we
denote the represented boolean formula of BDD $B$ by $\langle B\rangle$. We
use induction and assume that by the end of every iteration,
$\langle\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)\rangle\equiv\bigwedge_{n^{\prime\prime}\in
C^{\prime}(n)}\langle\texttt{BV}_{\texttt{post}}(\mathcal{T},n^{\prime\prime})\rangle$,
where $C^{\prime}(n)$ is the set of all children nodes that have been
traversed by the end of the last iteration. In the base case,
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)=1\land\texttt{BV}_{\texttt{post}}(\mathcal{T},n^{\prime})$,
where $n^{\prime}$ is the first children node traversed. Hence it is returns
as defined. Specifically, if
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n^{\prime})==\llbracket 0\rrbracket$,
then the iteration is the last iteration since conjunction of boolean formulas
with $0$ is also $0$.

Next we prove the induction step. If in the new iteration the BDD
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n^{\prime})$ is not $0$, then it is
updated to the conjunction of $(\bigwedge_{n^{\prime\prime}\in
C^{\prime}(n)}\texttt{BV}_{\texttt{post}}(\mathcal{T},n^{\prime\prime}))\land\texttt{BV}_{\texttt{pre}}(\mathcal{T},n^{\prime})$,
exactly matching the inductive hypothesis. So this invariant is preserved in
this new iteration. If in the new iteration of $n^{\prime}$, the BDD
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n^{\prime})$ encodes $0$, the
conjunction in Def. 6 is also $0$, so the pre-valuation line 12 is consistent
with the inductive hypothesis. Hence by the end of every iteration of the loop
in lines 9-12, we have the invariant that
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)\equiv\bigwedge_{n^{\prime\prime}\in
C^{\prime}(n)}\texttt{BV}_{\texttt{post}}(\mathcal{T},n^{\prime\prime})$. Line
13 performs the operation of existential quantification in Def. 6. Hence we
have the correctness of Alg. 1.

Next we show the equivalence between the returned pre-valuations and its
definition. For leave nodes $n$, the pre-valuation computed in line 4
corresponds to Definition. 6. In the case of internal node,
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$ is returned either by the end of
the for-loop in lines 9-12, or returned whenever it is equal to $\llbracket
0\rrbracket$. We also know that $\texttt{BV}_{\texttt{post}}(\mathcal{T},n)$
is proved above to be equivalent to its definition, and the fact that a
conjunction with zero is always 0, in the sense of both boolean formulas and
BDDs. Therefore we are only left to show that the pre-valuation defined in
Definition. 6 is equivalent to $\texttt{pre-BV}(\mathcal{T},n)$ at the end of
Algorithm. 1. Since $\texttt{pre-BV}(\mathcal{T},n)$ is updated in line 10
only, it is equivalent to the conjunction of $\llbracket 1\rrbracket$ and
$\texttt{BV}_{\texttt{post}}(\mathcal{T},n^{\prime})$ for all $n^{\prime}\in
C(n)$, which is exactly as defined in its Definition. 6. Hence we complete the
proof.

∎

###  0.A.2 Proof of Theorem. 3.3

###### Proof.

First, we prove the first statement of Theorem 3.3. Suppose $(\exists_{y\in
Y}\hskip 2.84544pty)\varphi=1$, i.e., there is full realizability. We need to
show that $b=1$ throughout the for-loop in lines 10-16. i.e., We need to prove
that in all iterations, the algorithm never goes to line 14. That is, to show
that $\texttt{BV}_{\texttt{post}}(\mathcal{T}_{X},n)=1$ for all
$n\in\texttt{XLeaves}(\mathcal{T})$. By Definition 6 and Theorem 3.1, the
post-valuation of $Y$ internal nodes is equal to the conjunction of post-
valuations under it with its labelled $Y$ variables existentially quantified.
This is then equivalent to the conjunctions of all leaves in its descendants,
projecting out all variables labelled in its descendants. Since we assume full
realizability, all clauses represented by the leaves are satisfiable, and thus
the post-valuations of all the $Y$ internal nodes are equal to $1$, not to
mention the visited internal nodes in the uppermost level of
$\mathcal{I}_{Y}$.

To prove the other direction, assume that Algorithm 2 returns _fully
realizable_. Then line 17 must confirms, and it is equivalent to say
$\texttt{BV}_{\texttt{post}}(\mathcal{T}_{X},n)$ is always $1$. Then for all
internal nodes in $\texttt{XLeaves}(\mathcal{T})$, post-valuation is
$\llbracket 1\rrbracket$. Since all the leaves in the original graded project-
join tree $\mathcal{T}$ has one and only one ancestor in
$\texttt{XLeaves}(\mathcal{T})$, the conjunction of the post-valuations of all
$n\in\texttt{XLeaves}(\mathcal{T})$ is equivalent to $(\exists_{y\in Y}\hskip
2.84544pty)\varphi$ and to $1$. Hence $\varphi$ achieves full realizability.

Next, we prove that a returned _not realizable_ from Algorithm 2 is sufficient
condition for null realizability of $\varphi$. Suppose Algorithm 2 returns
_not realizable_. Then in line 11,
$\texttt{BV}_{\texttt{post}}(\mathcal{T}_{X},n)=\llbracket 0\rrbracket$. There
is some $Y$ internal node $n$ without parents in $\mathcal{I}_{Y}$, such that
its post-valuation in $\mathcal{T}_{X}$ is the $0$-BDD. Hence, by Def. 6, the
conjunction of post-valuations of its children node in $\mathcal{I}_{Y}$ is
$0$. Thus there does not exist $Y$ variables labelled by this node $n$, such
that the conjunction of clauses in its descendants is satisfiable. Thus, there
does not exist a set of boolean values for all the $Y$ variables, that
satisfies the conjunction of clauses in descendants of $n$. Moreover, the
conjunction of all clauses in $\varphi$ is not satisfiable. Thus, $\varphi$
does not achieve partial realizability in its domain and null realizability is
proved.

Hence we complete the proof for Theorem 3.3.

∎

###  0.A.3 Proof of Theorem. 3.2

This theorem follows from the definition of realizability set and Definition.
6:

###### Proof.

Let $\mathcal{T}$ be a graded project-join tree of CNF $\varphi(X,Y)$. Let
$X_{\texttt{leaves}}(\mathcal{T})$ be the set of highest $Y$ nodes. Denote
descendants of node $n$ by $D(n)$.

From Definition. 6,

$BV_{\texttt{pre}}(\mathcal{T},n)\equiv(\exists_{z\in V}z)\bigwedge_{l\in
D(n)\cap\mathcal{L}(\mathcal{T})}\gamma(l)$

where $V=\\{z\mid\exists m\in D(n)s.t.z\in\pi(m)\\}$. Then the realizability
set $R$ is defined to be

$R=\\{(x_{1}\ldots x_{m})\mid(\exists y_{1})\ldots(\exists
y_{n})s.t.\varphi(x_{1},\ldots,x_{m},y_{1},\ldots,y_{n})=1\\}=(\exists_{\forall
y\in Y}y)\bigwedge_{l\in\mathcal{L}(\mathcal{T})}\gamma(l).$

We also know that each $Y$ variable is labelled under one and only one highest
level $Y$ node, by definition of a graded project-join tree. Hence

$Y=\bigcup_{n\in X_{\texttt{leaves}}(\mathcal{T})}\left(\bigcup_{m\in
D(n)}\pi(m)\right).$

Therefore, the conjunction of pre-valuations for all $n\in
X_{\texttt{leaves}}(\mathcal{T})$, i.e.,
$\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$,
we can show:

$\displaystyle\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$
$\displaystyle\equiv$
$\displaystyle\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}(\exists_{z\in
V}z)\bigwedge_{l\in D(n)\cap\mathcal{L}(\mathcal{T})}\gamma(l)\texttt{ where
}V=\\{z\mid\exists m\in D(n)s.t.z\in\pi(m)\\}$ $\displaystyle\equiv$
$\displaystyle(\exists_{z\in
V^{\prime}}z)\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}\bigwedge_{l\in
D(n)\cap\mathcal{L}(\mathcal{T})}\gamma(l)$ $\displaystyle\texttt{ where
}V^{\prime}=\\{z\mid\exists n\in{X_{\texttt{leaves}}}(\mathcal{T}),\exists
m\in D(n)s.t.z\in\pi(m)\\}$ (by definition of graded project-join tree)
$\displaystyle\equiv$ $\displaystyle(\exists_{z\in
V^{\prime}}z)\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}\bigwedge_{l\in
D(n)\cap\mathcal{L}(\mathcal{T})}\gamma(l)$ $\displaystyle\texttt{ where
}V^{\prime}=\\{z\mid\exists m\in\mathcal{I}_{Y}s.t.z\in\pi(m)\\}$
$\displaystyle\equiv$ $\displaystyle(\exists_{z\in
Y}z)\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}\bigwedge_{l\in
D(n)\cap\mathcal{L}(\mathcal{T})}\gamma(l)$ $\displaystyle\equiv$
$\displaystyle(\exists
Y)\bigwedge_{n\in{X_{\texttt{leaves}}}(\mathcal{T})}\bigwedge_{l\in
D(n)\cap\mathcal{L}(\mathcal{T})}\gamma(l)$ $\displaystyle\equiv$
$\displaystyle(\exists
Y_{\varphi})\bigwedge_{l\in\mathcal{L}(\mathcal{T})}\gamma(l).$

Theorem 3.2 is proved. ∎

###  0.A.4 Proof of Theorem. 3.4

###### Proof.

Suppose Algorithm 3 returns _not realizable_. Then the post-valuation of the
root is $0$-BDD. By Definition 6, it is either a leave representing an
unsatisfiable clause, or the $X$ variables do not satisfy the conjunction of
all clauses in the tree. In the trivial former case it is obviously not
realizable.

In the latter case, since $\mathcal{T}_{X}$ is the output of Algorithm 2 where
all $Y$ internal nodes are eliminated, the post-valuation of these new leaves
remain the same in the updated tree $\mathcal{T}_{X}$. Taking existential
projections on an output variable only to the clauses where it has occurrences
in, is logically equivalent to quantifying it on the entire formula. The same
reasoning applied to their symbolic representations. Hence the conjunction of
the clauses in $\mathcal{T}_{X}$ with all $X$ variables quantified is
logically equivalent to $\varphi$ with all $X$ and $Y$ existentially
quantified. Hence, there do not exist $X$ and $Y$ variables that satisfy
$\varphi$. i.e., if Algorithm 3 returns _not realizable_ , there is null
realizability.

On the other hand, assume Algorithm 3 returns _partially realizable_. Then in
line 1 $\texttt{BV}_{\texttt{post}}(\mathcal{T}_{X},r_{x})$ is not $0$-BDD.
That is, the conjunction of leaves has satisfying set of variables labelled.
By analysis above, it is equivalent to satisfiability of the CNF formula
represented by the original tree $\mathcal{T}$ in Algorithm 2. That is, there
is partial realizability. Since null and partial realizability is
complementary to each other, we do not need to prove the reverse directions in
both cases. Hence the correctness of Theorem 3.4 is proved. ∎

###  0.A.5 Proof of Lemma. 3

###### Proof.

From the definition of of project-join tree, if $y\in\pi(m)$ then every clause
where $y$ appears must be in a leaf node that descends from $m$. Since $n$ is
not a descendant of $m$, then either no clauses containing $y$ have been
joined on the way to form $\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$, or (if
$m$ is a descendant of $n$ instead) $y$ has already been existentially
quantified. ∎

###  0.A.6 Proof of Theorem. 4.1

###### Proof.

We use $C(n)$ to denote the set of children of node $n$, $D(n)$ the set of
descendants of node $n$ (not including $n$ itself), and $L(n)\subseteq D(n)$
the set of descendants of $n$ that are leaves. We also use the notation
$Y_{n}=Y\cap\pi(n)$ for the set of variables synthesized in node $n$ and
$Y^{\prime}_{n}=\bigcup_{n^{\prime}\in D(n)}Y_{n}$ for the set of variables
synthesized in nodes that are descendants of $n$. Finally, we denote by
$W^{n}_{y}=W_{y}[y^{\prime}\mapsto W_{y^{\prime}}]_{y^{\prime}\in Y_{n}\cup
Y^{\prime}_{n}}$ the witness for variable $y$ after all witnesses synthesized
in $n$ or its descendants have been substituted into it. Note that if $y\in
Y_{m}$ where $m$ is not a descendant of $n$ (including when $m=n$) then
$W^{n}_{y}=W_{y}$ (by Lemma 3).

Assume that, for an arbitrary node $n$,
$\texttt{SolveEqn}(\pi(n),\texttt{BV}_{\texttt{pre}}(\mathcal{T},n))$ returns
a correct witness $W_{y}$ for every $y\in\pi(n)$. In other words, that
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)[y\mapsto W_{y}]_{y\in
Y_{n}}\equiv(\exists Y_{n})\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$. Recall
that both $W_{y}$ and $\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)[y\mapsto
W_{y}]_{y\in Y_{n}}$ can still be dependent not only on the $X$ variables, but
also on the $Y$ variables of nodes that $n$ descends from (but no other nodes,
as per Lemma 3).

We show by induction that the following holds for every node $n$:

$\displaystyle\left(\bigwedge_{c\in L(n)}\gamma(c)\right)[y\mapsto
W^{n}_{y}]_{y\in Y_{n}}$ $\displaystyle[y\mapsto W^{n}_{y}]_{y\in
Y^{\prime}_{n}}\equiv(\exists Y_{n})(\exists Y^{\prime}_{n})\bigwedge_{c\in
L(n)}\gamma(c).$

This expression states that $\\{W^{n}_{y}\mid y\in Y_{n}\cup
Y^{\prime}_{n}\\}$ are witnesses for $\bigwedge_{c\in L(n)}\gamma(c)$ (note
that these witnesses might still depend on $Y$ variables from ancestors of
$n$). If $n=r$ is the root of the tree, then $\bigwedge_{c\in
L(r)}\gamma(c)\equiv\varphi$ and $Y_{r}\cup Y^{\prime}_{r}=Y$, and so
$\varphi[y\mapsto W^{r}_{y}]_{y\in Y}\equiv(\exists Y)\varphi$. In other
words, $\\{W^{r}_{y}\mid y\in Y\\}$ are witnesses for the $Y$ variables. Note
that the $W^{r}_{y}$ are equivalent to the final witnesses returned in line 4.
Therefore, the witnesses returned by Algorithm 4 are correct. All that is left
is to prove (0.A.6).

##### Base case.

Assume $n$ is a leaf. In that case, $L(n)$, $Y_{n}$ and $Y^{\prime}_{n}$ are
all empty, and $\bigwedge_{c\in L(n)}\gamma(c)\equiv 1$. Therefore, (0.A.6)
holds vacuously.

##### Inductive step.

Assume $n$ is an internal node, and (0.A.6) holds for all of $n$’s children
$C(n)=\\{n_{1},\ldots,n_{k}\\}$. We will show that it holds for $n$ as well.
Note that we use the fact that, by early quantification,
$\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)\equiv(\exists
Y^{\prime}_{n})\bigwedge_{c\in L(n)}\gamma(c)$.

$\displaystyle(\exists Y_{n})(\exists Y^{\prime}_{n})\bigwedge_{c\in
L(n)}\gamma(c)$ $\displaystyle\equiv$ $\displaystyle(\exists
Y_{n})\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)$ $\displaystyle\equiv$
$\displaystyle\texttt{BV}_{\texttt{pre}}(\mathcal{T},n)[y\mapsto
W^{n}_{y}]_{y\in Y_{n}}$ (and by $W^{n}_{y}=W_{y}$) $\displaystyle\equiv$
$\displaystyle\left((\exists Y^{\prime}_{n})\bigwedge_{c\in
L(n)}\gamma(c)\right)[y\mapsto W^{n}_{y}]_{y\in Y_{n}}$ $\displaystyle\equiv$
$\displaystyle\left(\bigwedge^{k}_{i=1}(\exists Y_{n_{i}})(\exists
Y^{\prime}_{n_{i}})\bigwedge_{c\in L(n_{i})}\gamma(c)\right)$
$\displaystyle[y\mapsto W^{n}_{y}]_{y\in Y_{n}}$ $\displaystyle\equiv$
$\displaystyle\left(\bigwedge^{k}_{i=1}\left(\bigwedge_{c\in
L(n_{i})}\gamma(c)\right)[y^{\prime}\mapsto
W^{n_{i}}_{y^{\prime}}]_{y^{\prime}\in Y_{n_{i}}\cup
Y^{\prime}_{n_{i}}}\right)$ $\displaystyle[y\mapsto W^{n}_{y}]_{y\in Y_{n}}$
(by induction hypothesis) $\displaystyle\equiv$
$\displaystyle\left(\bigwedge^{k}_{i=1}\bigwedge_{c\in
L(n_{i})}\gamma(c)\right)[y^{\prime}\mapsto
W^{n_{1}}_{y^{\prime}}]_{y^{\prime}\in Y_{n_{1}}\cup
Y^{\prime}_{n_{1}}}\ldots$ $\displaystyle[y^{\prime}\mapsto
W^{n_{k}}_{y^{\prime}}]_{y^{\prime}\in Y_{n_{k}}\cup
Y^{\prime}_{n_{k}}}[y\mapsto W^{n}_{y}]_{y\in Y_{n}}$ (since the $L(n_{i})$
are disjoint) $\displaystyle\equiv$
$\displaystyle\left(\bigwedge^{k}_{i=1}\bigwedge_{c\in
L(n_{i})}\gamma(c)\right)[y\mapsto W^{n}_{y}]_{y\in Y_{n}}$
$\displaystyle[y^{\prime}\mapsto W^{n}_{y^{\prime}}]_{y^{\prime}\in
Y_{n_{1}}\cup Y^{\prime}_{n_{1}}}\ldots[y^{\prime}\mapsto
W^{n}_{y^{\prime}}]_{y^{\prime}\in Y_{n_{k}}\cup Y^{\prime}_{n_{k}}}$ (*)
$\displaystyle\equiv$ $\displaystyle\left(\bigwedge^{k}_{i=1}\bigwedge_{c\in
L(n_{i})}\gamma(c)\right)[y\mapsto W^{n}_{y}]_{y\in Y_{n}}[y^{\prime}\mapsto
W^{n}_{y^{\prime}}]_{y^{\prime}\in Y^{\prime}_{n}}$ (since $Y_{n_{1}}\cup
Y^{\prime}_{n_{1}}\cup\ldots\cup Y_{n_{k}}\cup
Y^{\prime}_{n_{k}}=Y^{\prime}_{n}$) $\displaystyle\equiv$
$\displaystyle\left(\bigwedge_{c\in L(n)}\gamma(c)\right)[y\mapsto
W^{n}_{y}]_{y\in Y_{n}}[y^{\prime}\mapsto W^{n}_{y^{\prime}}]_{y^{\prime}\in
Y^{\prime}_{n}}.$ (since $L(n_{1})\cup\ldots\cup L(n_{k})=L(n)$)

The step marked with (* ‣ 0.A.6) above merits a more detailed explanation. In
the step before, the substitution $[y\mapsto W^{n}_{y}]_{y\in Y_{n}}$ is
performed at the end, and therefore this substitution also affects the
witnesses $W^{n_{i}}_{y^{\prime}}$ from the child nodes (which might depend on
the variables $y\in Y_{n}$). When we move this substitution to the beginning,
to ensure equivalence we must also substitute $W^{n}_{y}$ into the
substitutions $[y^{\prime}\mapsto W^{n_{i}}_{y^{\prime}}]_{y^{\prime}\in
Y_{n_{i}}\cup Y^{\prime}_{n_{i}}}$, which updates $W^{n_{i}}_{y^{\prime}}$ to
$W^{n_{i}}_{y^{\prime}}[y\mapsto W^{n}_{y}]_{y\in Y_{n}}\equiv
W^{n}_{y^{\prime}}$. ∎

##  Appendix 0.B Synthesis in Factored RSynth

Let $\varphi=F_{1}\land\ldots\land F_{m}$ (each $F_{j}$ is a factor, for
example a clause or a cluster). We associate with the factor $F_{j}$ the set
$Y_{j}$ of the output variables that occur in $F_{j}$ but do not occur in a
factor $F_{i}$ with $i<j$. Equivalently speaking, the set $Y_{j}$ consists of
the variables from $F_{j}$ that only occur in factors $F_{j},\ldots,F_{m}$.
Moreover, since each $Y_{j}$ includes all variables that satisfy this
criterion, for all $1\leq j\leq m$, if a variable $y\in Y_{j}$, then it is
guaranteed that $y\not\in Y_{k}$ for $k\neq j$.

The intuition behind this definition is that an output variable $y\in Y_{j}$
does not depend on the formulas $F_{1},\ldots,F_{j-1}$. Thus, these clauses
can be ignored when constructing a witness for $y$. i.e., the values of
clauses in these other factors do not affect the function constructed for this
variable. We use the notation $\mathcal{F}_{j}$ to denote the BDD representing
the factor $F_{j}$, and $\exists Y_{j}$ to denote the existential
quantification of all variables $y\in Y_{j}$ as a block. We can then compute
realizability by using early quantification:

$\displaystyle B_{m-1}\equiv(\exists Y_{m})\mathcal{F}_{m}$ $\displaystyle
B_{m-2}\equiv(\exists Y_{m-1})(\mathcal{F}_{m-1}\land B_{m-1})$
$\displaystyle\ldots$ $\displaystyle B_{i}\equiv(\exists
Y_{i+1})(\mathcal{F}_{i+1}\land B_{i+1})$ $\displaystyle\ldots$ $\displaystyle
B_{1}\equiv(\exists Y_{2})(\mathcal{F}_{2}\land B_{2})$ $\displaystyle
B_{0}\equiv(\exists Y_{1})(\mathcal{F}_{1}\land B_{1})$

Note that, from the correctness of early quantification, we have that
$B_{i}\equiv(\exists Y_{i+1})\ldots(\exists
Y_{m})(\mathcal{F}_{i+1}\land\ldots\mathcal{F}_{m})$. Like before, $B_{0}$ is
equivalent to the realizability set $R_{\varphi}$. Note that this framework
already has some kind of tree structure. Each $\mathcal{F}_{j}$ corresponds to
a leaf, and each $B_{j}$ corresponds to an internal node, with children
$\mathcal{F}_{j-1}$ and $B_{j-1}$, and labeled by $Y_{j-1}$. $B_{0}$ is the
root of the tree. Similarly to how realizability was computed inside-out in
the monolithic case, in this case realizability is computed _bottom-up_ , from
the leaves to the root. Witness construction, which was computed outside-in in
the monolithic case, is in this case computed _top-down_ , from the root to
the leaves (witnesses in a single node can be computed as in the monolithic
procedure):

For all $y_{i}\in Y_{1}$, $g_{i}$ is computed from $\displaystyle\hskip
2.84544pt(\mathcal{F}_{1}\land B_{1}),$ For all $y_{i}\in Y_{2}$, $g_{i}$ is
computed from $\displaystyle\hskip 2.84544pt(\mathcal{F}_{2}\land
B_{2})[y_{j}\mapsto g_{j}]_{y_{j}\in Y_{1}},$ $\displaystyle\ldots$ For all
$y_{i}\in Y_{k}$, $g_{i}$ is computed from $\displaystyle\hskip
2.84544pt(\mathcal{F}_{k}\land B_{k})[y_{j}\mapsto g_{j}]_{y_{j}\in
Y_{1}\cup\ldots\cup Y_{k-1}},$ $\displaystyle\ldots$ For all $y_{i}\in
Y_{m-1}$, $g_{i}$ is computed from $\displaystyle\hskip
2.84544pt(\mathcal{F}_{m-1}\land B_{m-1})[y_{j}\mapsto g_{j}]_{y_{j}\in
Y_{1}\cup\ldots\cup Y_{m-2}},$ For all $y_{i}\in Y_{m}$, $g_{i}$ is computed
from $\displaystyle\hskip 2.84544pt(\mathcal{F}_{m}\land B_{m})[y_{j}\mapsto
g_{j}]_{y_{j}\in Y_{1}\cup\ldots\cup Y_{m-1}}.$

Note that, similarly to how in the monolithic case each witness depends on the
witnesses of the previous variables, in the factored case the witnesses of a
child depend on the witnesses of its ancestors. Parent nodes propagate
witnesses to their children, who then substitute them into
$(\mathcal{F}_{k}\land B_{k})$ before computing witnesses for their own
variables. These witnesses are then propagated to their own children. Note
that $(\mathcal{F}_{k}\land B_{k})$ corresponds to the pre-valuation from
Definition 6.

##  Appendix 0.C Space Performance Charts

(a) Realizability-Checking Phase Space Usage Comparison

(b) Synthesis Space Usage Comparison

Figure 5:

##  Appendix 0.D DPSynth vs. Manthan

We measure the time and space usage of experiments on the dataset selected
from QBFEVAL’16 to QBFEVAL’19. DPSynth and Manthan [17] each solves for some
benchmarks that the other does not solve.

As the overall picture of synthesis solving, DPSynth and Manthan each has
strength on some instances, but the number of benchmarks that only DPSynth
solves is larger than those solved only by Manthan. On the intersection of
solved sets, DPSynth takes less time usage.

Overall, DPSynth shows a better time performance. In order to compare the
running time, we compare against Manthan using the DPSynth _end-to-end
synthesis_ time, which is the sum of tree-decomposition time, compilation,
realizability-checking time, and synthesis time. For _partially realizable_
instances, since Manthan returns UNSAT for partially realizable benchmarks, we
compare with Manthan by measuring the _realizability time_ of DPSynth, which
is the sum of tree-decomposition, compilation and realizability-checking time.
This is illustrated in the table presented in Section 5 of formal text.

The results show a better performance in DPSynth running time, in both fully
and partially realizable cases. This shows the strength of the dynamic-
programming decision-diagram approach.

Benchmark | Manthan time (s) | DPSynth time (s) | Manthan / DPSynth time
---|---|---|---
mutex-2-s | 26.62365198 | 0.017328861 | 1536.376337
mutex-4-s | 70.10412574 | 0.057425382 | 1220.786407
qshifter_3 | 0.02080822 | 0.004227581 | 4.922015666
qshifter_4 | 0.035684586 | 0.011800355 | 3.024026444
qshifter_5 | 0.118482351 | 0.056386868 | 2.101240156
qshifter_6 | 0.548010349 | 0.290776052 | 1.884647465
qshifter_7 | 3.304552555 | 1.692991177 | 1.951901817
stmt1_145_146 | 1.481198549 | 0.007940356 | 186.5405719
stmt1_20_21 | 1.161505938 | 0.005571153 | 208.4857367
stmt1_60_61 | 138.0251365 | 1.923284128 | 71.7653385
stmt1_629_630 | 60.86966228 | 0.820687097 | 74.16914742
stmt1_787_788 | 92.2114253 | 1.340908081 | 68.76789439
stmt1_811_812 | 5.000648737 | 0.042724069 | 117.045236
stmt1_919_920 | 16.3737123 | 0.216405419 | 75.6622102
stmt11_643_645 | 13.83426762 | 0.148434139 | 93.20138689
stmt124_966_965 | 17.15093589 | 0.226107464 | 75.8530284
stmt16_0_1 | 0.078123331 | 0.021049437 | 3.711421406
stmt16_285_286 | 12.3903234 | 0.199766912 | 62.02390214
stmt16_47_48 | 127.7006507 | 1.851167077 | 68.98386012
stmt16_818_819 | 8.039676428 | 0.099669646 | 80.66323851
stmt16_950_951 | 21.96217847 | 0.321454774 | 68.32120797
stmt17_99_98 | 147.940861 | 2.241282086 | 66.00724733
stmt18_258_260 | 9.160577059 | 0.098143359 | 93.33873583
stmt2_480_551 | 16.77611017 | 0.226805481 | 73.9669522
stmt2_649_647 | 11.21149755 | 0.139258954 | 80.50827055
stmt2_649_723 | 11.58830237 | 0.14303965 | 81.01461639
stmt2_649_776 | 14.4783535 | 0.196231457 | 73.7820211
stmt21_326_327 | 22.5036993 | 0.357303104 | 62.98209853
stmt24_148_149 | 1.197834015 | 0.006430307 | 186.2794443
stmt24_292_293 | 9.379323483 | 0.109969875 | 85.28993493
stmt24_7_8 | 0.017041206 | 0.001758292 | 9.691909171
stmt24_765_766 | 18.09966111 | 0.220442702 | 82.10596653
stmt27_296_297 | 10.50176525 | 0.115043276 | 91.28534597
stmt27_946_955 | 20.3260808 | 0.247080786 | 82.26491881
stmt3_639_640 | 8.168511868 | 0.079512754 | 102.7320959
Benchmark | Manthan time (s) | DPSynth time (s) | Manthan / DPSynth time
---|---|---|---
stmt32_570_572 | 23.86345649 | 0.32441781 | 73.55778799
stmt37_941_942 | 129.7759182 | 1.517532121 | 85.51774058
stmt38_943_942 | 117.9836717 | 1.531322152 | 77.04693066
stmt41_118_131 | 9.311798096 | 0.22846856 | 40.75745956
stmt41_566_580 | 44.67906404 | 0.83791215 | 53.32189542
stmt41_738_737 | 17.30380273 | 0.214580042 | 80.64031756
stmt41_738_749 | 36.58995533 | 0.674991152 | 54.2080518
stmt44_435_436 | 12.76951456 | 0.144744236 | 88.22123018
stmt44_554_555 | 22.60296774 | 0.29673466 | 76.17232088
stmt44_554_604 | 23.51070952 | 0.307722947 | 76.40219799
stmt44_916_917 | 16.47536898 | 0.19140868 | 86.07430434
stmt7_33_34 | 14.49155951 | 0.934846089 | 15.50154584
stmt70_191_213 | 8.378497839 | 0.09022127 | 92.86610396
stmt70_495_501 | 22.71755934 | 0.314747484 | 72.1770959
stmt70_854_859 | 16.48648357 | 0.203281798 | 81.10162216
stmt72_696_721 | 17.04460955 | 0.204169481 | 83.4826511
stmt82_224_225 | 10.50310063 | 0.105692302 | 99.37431994
stmt86_889_890 | 21.63464522 | 0.284072161 | 76.15897717
stmt9_350_351 | 8.726649284 | 0.092352257 | 94.49308082
subtraction32 | 3.983768463 | 285.7623599 | 0.013940844
tree-exa10-10 | 0.580000877 | 0.001643786 | 352.8445171
tree-exa10-15 | 0.744118929 | 0.002058999 | 361.3983926
tree-exa10-20 | 0.94502902 | 0.002538212 | 372.3207598
tree-exa10-25 | 1.136503696 | 0.002991756 | 379.8784715
tree-exa10-30 | 1.398799896 | 0.00363048 | 385.2933761
factorization8 | 26.02147222 | 0.01355423 | 1919.804534
rankfunc37_signed_16 | 2.976966858 | 0.020192158 | 147.4318326
stmt137_903_911 | 18.31892133 | 0.2235378 | 81.94999382
stmt19_3_214 | 67.52295566 | 970.6645171 | 0.069563639
stmt19_66_214 | 84.54595137 | 148.8763251 | 0.567893863
stmt2_976_999 | 3228.63344 | 57.85746008 | 55.80323498
stmt21_5_134 | 47.65692377 | 14.28987617 | 3.335013067
stmt21_84_215 | 88.41444421 | 135.9611531 | 0.650291956
stmt27_16_97 | 53.51791215 | 9.510231213 | 5.627403893
stmt27_584_603 | 24.56984329 | 0.329176383 | 74.64035867