$|\partial_{d}\tilde{p}(\xi^{\prime},\xi_{d})|\geq
2|\xi_{d}|-C_{1}|\xi|^{2}\geq|\xi_{d}|\qquad\text{if
}\frac{|\xi^{\prime}|}{2}\leq|\xi_{d}|\leq 2|\xi^{\prime}|.$

In the last inequality we used $|\xi_{d}|\leq|\xi|\leq c\leq\frac{1}{5C_{1}}$.
Hence, by strict monotonicity, all solutions of $\tilde{p}(\xi)=0$ in
$B_{c}(0)$ are given by $\xi_{d}=\psi_{1}(\xi^{\prime})$ or
$\xi_{d}=-\psi_{2}(\xi^{\prime})$ for positive functions $\psi_{1},\psi_{2}$
that, by the implicit function theorem, are even smooth away from the origin.
Taking the gradients on each part of the equations
$\tilde{p}(\xi^{\prime},\psi_{1}(\xi^{\prime}))=0$ and
$\tilde{p}(\xi^{\prime},-\psi_{2}(\xi^{\prime}))=0$ we find the claimed
properties

$\psi_{1}(\xi^{\prime})=|\xi^{\prime}|-r_{1}(\xi^{\prime}),\quad\psi_{2}(\xi^{\prime})=|\xi^{\prime}|+r_{2}(\xi^{\prime})\quad\text{with
}|\partial^{\alpha}r_{i}(\xi^{\prime})|\lesssim_{\alpha}|\xi^{\prime}|^{2-|\alpha|}.$

It remains to check the validity of (48). This is straight-forward for
$|\xi_{d}|\leq\frac{|\xi^{\prime}|}{2}$ or $|\xi_{d}|\geq 2|\xi^{\prime}|$
where the factor
$(\xi_{d}-|\xi^{\prime}|+r_{1}(\xi^{\prime}))(\xi_{d}+|\xi^{\prime}|+r_{2}(\xi^{\prime}))$
does not vanish. In the case $\frac{|\xi^{\prime}|}{2}\leq|\xi_{d}|\leq
2|\xi^{\prime}|$ and $\xi_{d}>0$ we obtain by the same arguments as in
Subsection 5.1

$\frac{\tilde{p}(\xi)}{(\xi_{d}-\psi_{1}(\xi^{\prime}))(\xi_{d}+\psi_{2}(\xi^{\prime}))}=\frac{\int_{0}^{1}\partial_{d}\tilde{p}(\xi^{\prime},\psi_{1}(\xi^{\prime})+t(\xi_{d}-\psi_{1}(\xi^{\prime}))dt}{\xi_{d}+\psi_{2}(\xi^{\prime})}$

with
$\int_{0}^{1}\partial_{d}\tilde{p}(\xi^{\prime},\psi_{1}(\xi^{\prime})+t(\xi_{d}-\psi_{1}(\xi^{\prime}))\,dt=O(|\xi_{d}|)$,
and the claim follows by $|\xi_{d}-\psi_{2}(\xi^{\prime})|\gtrsim|\xi|$. The
claim for the derivatives follows from the above display by induction. The
case $\xi_{d}<0$ is treated analogously. $\Box$

###  6.2. Estimates for perturbed cone multiplier

With $(\mathfrak{m}_{\alpha}f)\widehat{(}\xi)=m^{-\alpha}(\xi)\hat{f}(\xi)$ a
Fourier multiplier in $L^{p}(\mathbb{R}^{d})$ for $1<p<\infty$ by Mikhlin’s
theorem, the above parametric representation suggests to analyze the
generalized cone multiplier

$(\mathcal{C}^{\alpha}f)\widehat{(}\xi)=\frac{1}{\Gamma(1-\alpha)}\frac{\beta(\xi)\hat{f}(\xi)}{((\xi_{d}-|\xi^{\prime}|+r_{1}(\xi^{\prime}))(\xi_{d}+|\xi^{\prime}|+r_{2}(\xi^{\prime}))^{\alpha}_{+}},$

which is again defined by analytic continuation for $\alpha\geq 1$. As
provided in Subsection 6.1 for singular non-degenerate points, we suppose that

$r_{i}\in
C^{\infty}(\mathbb{R}^{d-1}\backslash\\{0\\}),\quad|\partial^{\alpha}r_{i}(\xi^{\prime})|\lesssim_{\alpha}|\xi^{\prime}|^{2-|\alpha|}\qquad(i=1,2,\alpha\in\mathbb{N}_{0}^{d})$

and $\beta\in C^{\infty}_{c}(B(0,c))$ satisfies $\beta(\xi)=1$ for
$|\xi|\leq\frac{c}{2}$ for $c$ as in Proposition 6.2. We suppose that $c=1$ to
lighten the notation. The aim of this section is to show that
$\mathcal{C}^{\alpha}:L^{p}(\mathbb{R}^{d})\to L^{q}(\mathbb{R}^{d})$ is
bounded for exponents $p,q$ as described below. To explain
$\mathcal{C}^{\alpha}$ _a priori_ in the distributional sense, we suppose that
$f\in\mathcal{S}$ with $0\notin\text{supp}(\hat{f})$. As we prove estimates
independent of the Fourier support, $\mathcal{C}^{\alpha}$ extends by density.

######  Proposition 6.3.

Let $1/2<\alpha<d/2$. Then $\mathcal{C}^{\alpha}$ has the same mapping
properties as the Bochner-Riesz operator $T^{\alpha}$ from Theorem 1.3 (i) for
$k=d-2$.

The proposition generalizes Lee’s result [35, Theorem 1.1] for $\alpha>1/2$:
Fourier supports and perturbations of the cone including the singular point
are covered and the space dimension is not restricted to $d=3$. As we obtain
the same conditions on $(p,q)$ as Lee, which he showed to be sharp in the case
$d=3$, the conditions in Proposition 6.3 are clearly sharp. It seems likely
that by bilinear restriction the result can be improved as in [35] for
$\alpha<\frac{1}{2}$.

To reduce the estimates to Theorem 1.3, we apply a Littlewood-Paley
decomposition. Let $\beta_{l}(\xi)=\beta_{0}(2^{l}\xi)$ with
$\text{supp}(\beta_{0})\subseteq B(0,2)\backslash B(0,1/2)$ and

$\sum_{l\geq 0}\beta_{l}\cdot\beta=\beta.$

We define

$(\mathcal{C}_{l}^{\alpha}f)\widehat{(}\xi)=\frac{1}{\Gamma(1-\alpha)}\frac{\beta_{l}(\xi)\beta(\xi)\hat{f}(\xi)}{((\xi_{d}-|\xi^{\prime}|+r_{1}(\xi^{\prime}))(\xi_{d}+|\xi^{\prime}|+r_{2}(\xi^{\prime}))^{\alpha}_{+}}.$

We have the following consequence of Littlewood-Paley theory:

######  Lemma 6.4.

Assume that there are $1<p<2<q<\infty$ and $r_{1}\in\\{1,p\\}$ and
$r_{2}\in\\{q,\infty\\}$ such that

$\|C_{l}^{\alpha}f\|_{L^{q,r_{2}}(\mathbb{R}^{d})}\leq
C\|f\|_{L^{p,r_{1}}(\mathbb{R}^{d})}$

holds for all $l\in\mathbb{N}_{0}$. Then

$\|\mathcal{C}^{\alpha}f\|_{L^{q,r_{2}}(\mathbb{R}^{d})}\lesssim
C\|f\|_{L^{p,r_{1}}(\mathbb{R}^{d})}.$

###### Proof.

We write by the square function estimate, which also holds in Lorentz spaces,
see, e.g. [30, Lemma 3.2], and Minkowski’s inequality (note that
$L^{\frac{q}{2},\infty}$ is normable because $q>2$)

$\displaystyle\|\mathcal{C}^{\alpha}f\|_{L^{q,r_{2}}(\mathbb{R}^{d})}\lesssim\big{\|}\big{(}\sum_{l\geq
0}|\mathcal{C}^{\alpha}_{l}f|^{2}\big{)}^{\frac{1}{2}}\big{\|}_{L^{q,r_{2}}(\mathbb{R}^{d})}\lesssim\big{(}\sum_{l\geq
0}\|\mathcal{C}_{l}^{\alpha}f\|_{L^{q,r_{2}}(\mathbb{R}^{d})}^{2}\big{)}^{\frac{1}{2}}.$

By hypothesis and noting that
$\mathcal{C}_{l}^{\alpha}f=\mathcal{C}_{l}^{\alpha}\big{(}\sum_{|l^{\prime}-l|\leq
2}\beta_{l^{\prime}}(D)f\big{)}$, we find

$\displaystyle\big{(}\sum_{l\geq
0}\|\mathcal{C}_{l}^{\alpha}f\|^{2}_{L^{q,r_{2}}(\mathbb{R}^{d})}\big{)}^{\frac{1}{2}}\lesssim\big{(}\sum_{l^{\prime}\geq
0}\|\beta_{l^{\prime}}(D)f\|^{2}_{L^{p,r_{1}}(\mathbb{R}^{d})}\big{)}^{\frac{1}{2}}\lesssim\|f\|_{L^{p,r_{1}}(\mathbb{R}^{d})}.$

Notice that the ultimate estimate is dual to the previous display. $\Box$

We are ready for the proof of Proposition 6.3.

###### Proof of Proposition 6.3.

We use scaling to reduce to unit frequencies:

$\displaystyle\mathcal{C}_{l}^{\alpha}f(x)$
$\displaystyle=\frac{1}{\Gamma(1-\alpha)}\int_{\mathbb{R}^{d}}\frac{e^{ix.\xi}\beta_{l}(\xi)\hat{f}(\xi)}{((\xi_{d}-|\xi^{\prime}|+r_{1}(\xi^{\prime}))(\xi_{d}+|\xi^{\prime}|+r_{2}(\xi^{\prime}))^{\alpha}_{+}}\,d\xi$
$\displaystyle=\frac{2^{-dl}}{\Gamma(1-\alpha)}\int_{\mathbb{R}^{d}}\frac{e^{ix.2^{-l}\zeta}\beta_{0}(\zeta)\hat{f}(2^{-l}\zeta)}{((2^{-l}\zeta_{d}-2^{-l}|\zeta^{\prime}|+r_{1}(2^{-l}(\zeta^{\prime}))(2^{-l}\zeta_{d}+2^{-l}|\zeta^{\prime}|+r_{2}(2^{-l}\zeta^{\prime}))^{\alpha}_{+}}d\zeta$
$\displaystyle=\frac{2^{2\alpha
l-dl}}{\Gamma(1-\alpha)}\int_{\mathbb{R}^{d}}\frac{e^{i2^{-l}x.\zeta}\beta_{0}(\zeta)\hat{f}_{l}(\zeta)}{((\zeta_{d}-|\zeta^{\prime}|+r_{1,l}(\zeta^{\prime}))(\zeta_{d}+|\zeta^{\prime}|+r_{2,l}(\zeta^{\prime}))^{\alpha}_{+}}d\zeta,$

where $\hat{f}_{l}(\zeta)=\hat{f}(2^{-l}\zeta)$,
$r_{i,l}(\zeta^{\prime})=2^{l}r_{i}(2^{-l}\zeta^{\prime})$, $\xi=2^{-l}\zeta$.
We therefore consider the operator

$S_{l}^{\alpha}g(y)=\frac{1}{\Gamma(1-\alpha)}\int_{\mathbb{R}^{d}}\frac{e^{iy.\xi}\beta_{0}(\xi)\hat{g}(\xi)}{((\xi_{d}-|\xi^{\prime}|+r_{1,l}(\xi^{\prime}))(\xi_{d}+|\xi^{\prime}|+r_{2,l}(\xi^{\prime}))^{\alpha}_{+}}d\xi.$

With $\text{supp}(\beta_{0})\subseteq B(0,2)\backslash B(0,1/2)$, the subsets
of $\text{supp}(\beta_{0})$ where the factors
$\xi_{d}-|\xi^{\prime}|+r_{1,l}(\xi^{\prime})$ and
$\xi_{d}+|\xi^{\prime}|+r_{2,l}(\xi^{\prime})$ vanish are separated. We write

$\beta_{0}(\xi)=\beta_{0}(\xi)(\gamma_{0}(\xi)+\gamma_{1}(\xi)+\gamma_{2}(\xi))$

with $\gamma_{i}\in C^{\infty}_{c}(\mathbb{R}^{d})$ and
$\text{supp}(\gamma_{0})\subseteq\\{\xi\in\mathbb{R}^{d}:|\xi_{d}|\not\sim|\xi^{\prime}|\\}$,
$\text{supp}(\gamma_{i})\subseteq\\{\xi\in\mathbb{R}^{d}:(-1)^{i+1}\xi_{d}\sim|\xi^{\prime}|\\}$
for $i=1,2$. Correspondingly, we consider the operators $S_{l,i}^{\alpha}$
with

$\big{(}S^{\alpha}_{l,i}h\big{)}\widehat{(}\xi)=\frac{1}{\Gamma(1-\alpha)}\frac{\gamma_{i}(\xi)\beta_{0}(\xi)\hat{h}(\xi)}{((\xi_{d}-|\xi^{\prime}|+r_{1,l}(\xi^{\prime}))(\xi_{d}+|\xi^{\prime}|+r_{2,l}(\xi^{\prime}))^{\alpha}_{+}}.$

Clearly, $S_{l,0}^{\alpha}$ is bounded from $L^{p}(\mathbb{R}^{d})\to
L^{q}(\mathbb{R}^{d})$ for $1\leq p\leq q\leq\infty$ as the kernel is a
Schwartz function. We shall only estimate $S_{l,1}^{\alpha}$ as
$S_{l,2}^{\alpha}$ is treated _mutatis mutandis_ :

$(S_{l,1}^{\alpha}h)\widehat{(}\xi)=\frac{1}{\Gamma(1-\alpha)}\frac{\gamma_{1}(\xi)\beta_{0}(\xi)\hat{h}(\xi)}{((\xi_{d}-|\xi^{\prime}|+r_{1,l}(\xi^{\prime}))(\xi_{d}+|\xi^{\prime}|+r_{2,l}(\xi^{\prime}))^{\alpha}_{+}}.$

With $m(\xi)=\xi_{d}+|\xi^{\prime}|+r_{2,l}(\xi^{\prime})\gtrsim\xi_{d}$ for
$\xi\in\text{supp}(\beta_{1})\cap\text{supp}(\beta)$ and
$|\partial^{\alpha}m(\xi)|\lesssim 1$, by Young’s inequality it is enough to
consider $\tilde{S}^{\alpha}_{l,1}$ given by

$(\tilde{S}^{\alpha}_{l,1}g)\widehat{(}\xi)=\frac{1}{\Gamma(1-\alpha)}\frac{\gamma_{1}(\xi)\beta_{0}(\xi)\hat{g}(\xi)}{(\xi_{d}-|\xi^{\prime}|+r_{1,l}(\xi^{\prime}))^{\alpha}_{+}}.$

To this operator, we can apply the estimates of Theorem 1.3 for $k=d-2$ since
in each point of the perturbed cone $d-2$ principal curvatures are bounded
from below in modulus uniformly with respect to $k$. Moreover, the rescaled
surfaces $\\{\zeta_{d}=\mp|\zeta^{\prime}|+r_{i,l}(\zeta^{\prime})\\}$ can be
approximated with the cone in any $C^{N}$-norm. As a consequence,
$S_{k}^{\alpha}$ has the mapping properties described in Theorem 1.3 (i) for
$\frac{1}{2}<\alpha<\frac{d}{2}$ with a uniform mapping constant. From

$\mathcal{C}_{l}^{\alpha}f(x)=2^{2\alpha l-3l}S_{l}^{\alpha}f_{l}(2^{-l}x)$

we conclude

$\displaystyle\|\mathcal{C}_{l}^{\alpha}f\|_{L^{q}(\mathbb{R}^{d})}$
$\displaystyle=2^{2\alpha
l-dl}\|(S_{l}^{\alpha}f_{l})(2^{-l}\cdot)\|_{L^{q}(\mathbb{R}^{d})}$
$\displaystyle\lesssim 2^{2\alpha
l-dl}2^{\frac{dl}{q}}\|S_{l}^{\alpha}f_{l}\|_{L^{q}(\mathbb{R}^{d})}$
$\displaystyle\lesssim 2^{2\alpha
l-dl}2^{\frac{dl}{q}}\|f_{l}\|_{L^{p}(\mathbb{R}^{d})}$
$\displaystyle=2^{2\alpha
l+\frac{dl}{q}-\frac{dl}{p}}\|f\|_{L^{p}(\mathbb{R}^{d})}.$

Given that the conditions on $p,q$ imply $2\alpha+\frac{d}{q}-\frac{d}{p}\leq
0$, we obtain the desired uniform estimates for any fixed
$l\in\mathbb{N}_{0}$. Hence, an application of Lemma 6.4 finishes the proof
for $p\neq 1$, $q\neq\infty$ because of $p<2<q$. If $p>1,q=\infty$, we can
find $q^{*}<\infty$ such that the conditions hold for $(p,q^{*})$. This is
true because $\frac{1}{p}-\frac{1}{q}=1-\frac{1}{q*}>\frac{2\alpha}{d}$ for
large enough $q^{*}$. Take $\chi$ a cut-off function with $\chi=1$ on
$\text{supp}(\beta)$. Then, by bounded frequencies and Young’s inequality,

$\displaystyle\|\mathcal{C}^{\alpha}f\|_{L^{\infty}(\mathbb{R}^{d})}$
$\displaystyle\lesssim\|\langle\mathcal{C}^{\alpha}f\|_{L^{q*}(\mathbb{R}^{d})}$
$\displaystyle=\|\mathcal{C}^{\alpha}(\chi(D)f)\|_{L^{q*}(\mathbb{R}^{d})}$
$\displaystyle\lesssim\|\chi(D)f\|_{L^{p}(\mathbb{R}^{d})}$
$\displaystyle\lesssim\|f\|_{L^{p}(\mathbb{R}^{d})}$

The case $p=1,q<\infty$ is dual and thus proved as well. The proof is
complete.

$\Box$

###  6.3. Estimates for approximate solutions close to the singular points

In this section we prove Proposition 2.4 by showing the corresponding
$L^{p}$-$L^{q}$-bounds for

$A_{\delta}f(x)=\int_{\mathbb{R}^{3}}\frac{e^{ix.\xi}\beta(\xi)}{\tilde{p}(\xi)+i\delta}\hat{f}(\xi)\,d\xi,$

where $\tilde{p}$, after some translation and dilation, has the form

(49) $\tilde{p}(\xi)=\xi_{3}^{2}-\xi_{1}^{2}-\xi_{2}^{2}+g(\xi)\text{ with
}|\partial^{\alpha}g(\xi)|\leq C_{\alpha}|\xi|^{3-|\alpha|}$

and $\text{supp}(\beta)\subset B(0,c)$ with $c$ as in Proposition 6.2. Roughly
speaking, this guarantees that the surface $\\{\tilde{p}(\xi)=0\\}$ looks like
a cone in $B(0,c)$. Due to the singularity at the origin, this seems
problematic, but can be remedied by Littlewood-Paley decomposition.

We proceed similar as above. Let $\beta_{0}\in C^{\infty}_{c}(\mathbb{R}^{3})$
with $\text{supp }(\beta_{0})\subseteq\\{c/2\leq|\xi|\leq 2c\\}$ and
$\beta_{\ell}(\xi)=\beta_{0}(2^{\ell}\xi)$, $\ell\geq 1$, such that

$\sum_{\ell\geq
0}\beta_{\ell}\cdot\beta_{13}(\xi)=\beta_{13}(\xi)\quad(\xi\neq 0).$

We further set
$\tilde{\beta}_{\ell}(\xi)=\beta_{\ell-1}(\xi)+\beta_{\ell}(\xi)+\beta_{\ell+1}(\xi)$.
As in the previous section, we have the following lemma by Littlewood-Paley
theory and Minkowski’s inequality:

######  Lemma 6.5.

Let $1<p\leq 2\leq q<\infty$, $r_{1}\in\\{1,p\\}$, and
$r_{2}\in\\{q,\infty\\}$. Suppose that

(50)
$\left\|\int_{\mathbb{R}^{3}}\frac{\hat{f}(\xi)\beta_{\ell}(\xi)e^{ix.\xi}}{p(\xi)+i\delta}d\xi\right\|_{L^{q,r_{2}}(\mathbb{R}^{3})}\leq
C\|\tilde{\beta}_{\ell}(D)f\|_{L^{p,r_{1}}(\mathbb{R}^{3})}$

holds for $C$ independent of $\ell$ and $\delta\neq 0$. Then we have

$\|A_{\delta}f\|_{L^{q,r_{2}}(\mathbb{R}^{3})}\lesssim\|f\|_{L^{p,r_{1}}(\mathbb{R}^{3})}.$

We prove (50) for $\ell=0$ and see how the remaining estimates follow by
rescaling as in the previous subsection. In the first step we localize to the
singular set: Let

$\beta_{0}=\beta_{0}(\beta_{01}+\beta_{02}),\quad\beta_{0i}\in
C^{\infty}_{c}(\mathbb{R}^{3})$

with

$\displaystyle\text{supp }(\beta_{01})$
$\displaystyle\subseteq\\{\xi\in\mathbb{R}^{3}:\,|\xi_{3}|\sim|\xi^{\prime}|\\},$
$\displaystyle\text{supp }(\beta_{02})$
$\displaystyle\subseteq\\{\xi\in\mathbb{R}^{3}:\,|\xi_{3}|\ll|\xi^{\prime}|,\,|\xi^{\prime}|\ll|\xi_{3}|\\}.$

We start with noting that in the support of $\beta_{0}\beta_{02}$ we find
$|p(\xi)|\gtrsim c^{2}$ and uniform boundedness of

$\left\|\int_{\mathbb{R}^{3}}\frac{\hat{f}(\xi)e^{ix.\xi}\beta_{0}\beta_{02}}{p(\xi)+i\delta}d\xi\right\|_{L^{q}(\mathbb{R}^{3})}\lesssim\|f\|_{L^{p}(\mathbb{R}^{3})}$

is immediate from Young’s inequality as the kernel is a Schwartz function.
We turn to the estimate of the contribution close to the vanishing set of $p$:
Let $\chi(\xi)=\beta_{0}(\xi)\beta_{01}(\xi)$. We follow the arguments of
Section 5.2: We decompose

$\frac{\chi(\xi)}{p(\xi)+i\delta}=\mathfrak{R}(\xi)+i\mathfrak{I}(\xi).$

These multipliers will be estimated by Fourier restriction-extension estimates
for the level sets of $p$ given by Theorem 1.3 for $k=d-2=1$, $\alpha=1$. To
carry out the program of Section 5.2, we need to change to generalized polar
coordinates $\xi=\xi(p,q)$ in $\text{ supp }(\chi)$. We can suppose that this
is possible as $|\nabla p(\xi)|\gtrsim c>0$ for $p(\xi)=0$, $|\xi|\sim c$,
after making the support of $\beta_{01}$ closer to the characteristic set, if
necessary. Furthermore, with graph parametrizations
$(\xi^{\prime},\psi(\xi^{\prime}))$ of
$\\{\xi\in\text{supp}(\chi)\,:\,p(\xi)=t\\}$ uniform in $t\in(-t_{0},t_{0})$,
$t_{0}$ chosen small enough, Theorem 1.3 yields uniform bounds. Also note that
Lemma 5.2 applies with $k=1$. This finishes the proof of (47) for $\ell=0$. We
show the bounds for $\ell\geq 1$ by rescaling. A change of variables gives

(51)
$\begin{split}&\quad\int_{\mathbb{R}^{3}}\frac{e^{ix.\xi}\beta_{\ell}(\xi)\hat{f}(\xi)}{p(\xi)+i\delta}d\xi\\\
&=2^{-3\ell}\int_{\mathbb{R}^{3}}\frac{e^{i2^{-\ell}x.\zeta}\beta_{0}(\zeta)\hat{f}(2^{-\ell}\zeta)}{2^{-2\ell}\zeta_{3}^{2}-2^{-2\ell}\zeta_{1}^{2}-2^{-2\ell}\zeta_{2}^{2}+g(2^{-\ell}\zeta)+i\delta}d\zeta\qquad(\zeta=2^{\ell}\xi)\\\
&=2^{-\ell}\int_{\mathbb{R}^{3}}\frac{e^{i2^{-\ell}x.\zeta}\beta_{0}(\zeta)\hat{f}_{\ell}(\zeta)}{\zeta_{3}^{2}-\zeta_{1}^{2}-\zeta_{2}^{2}+2^{2\ell}g(2^{-\ell}\zeta)+i2^{2\ell}\delta}d\zeta\qquad(\hat{f}_{\ell}(\zeta)=\hat{f}(2^{-\ell}\zeta)).\end{split}$

Let
$p_{\ell}(\zeta)=\zeta_{3}^{2}-\zeta_{1}^{2}-\zeta_{2}^{2}+2^{2\ell}g(2^{-\ell}\zeta)$,
$\delta_{\ell}=2^{2\ell}\delta$. Recall that
$|\partial^{\alpha}g(\xi)|\lesssim|\xi|^{3-|\alpha|}$, which previously
allowed to carry out the proof for $\ell=0$ for $c$ chosen small enough
depending on finitely many $C_{\alpha}$ in (49). Furthermore, we find

(52)
$\|\int_{\mathbb{R}^{3}}\frac{e^{ix.\xi}\beta_{0}(\zeta)\hat{h}(\zeta)}{p_{\ell}(\zeta)+i\delta_{\ell}}d\zeta\|_{L^{q}(\mathbb{R}^{3})}\lesssim\|h\|_{L^{p}(\mathbb{R}^{3})}$

with implicit constant independent of $\ell\geq 1$ choosing $c$ small enough
depending only on finitely many $C_{\alpha}$. Hence, taking (51) and (52)
together, gives

$\begin{split}\big{\|}\int_{\mathbb{R}^{3}}\frac{e^{ix.\xi}\beta_{\ell}(\xi)\hat{f}(\xi)}{p(\xi)+i\delta}d\xi\big{\|}_{L^{q}(\mathbb{R}^{3})}&\lesssim
2^{\frac{3\ell}{q}-\ell}\big{\|}\int_{\mathbb{R}^{3}}\frac{e^{ix.\zeta}\beta_{0}(\zeta)\hat{f}_{\ell}(\zeta)}{p_{\ell}(\zeta)+i\delta_{\ell}}d\zeta\big{\|}_{L^{q}(\mathbb{R}^{3})}\\\
&\lesssim 2^{\frac{3\ell}{q}-\ell}\|f_{\ell}\|_{L^{p}(\mathbb{R}^{3})}\\\
&\lesssim
2^{2\ell-\frac{3\ell}{p}+\frac{3\ell}{q}}\|f\|_{L^{p}(\mathbb{R}^{3})}.\end{split}$

Hence, Lemma 6.5 applies for $p\neq 1$ and $q\neq\infty$ because for our
choice of $p$ and $q$ we find $\frac{2}{3}\leq\frac{1}{p}-\frac{1}{q}$. For
$q=\infty$ or $p=1$, we use that frequencies are compactly supported to reduce
to $p\neq 1$ and $q\neq\infty$ like at the end of the proof of Proposition
6.3. The proof of Proposition 2.4 is complete. $\Box$

## Acknowledgements

Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research
Foundation) - Project-ID 258734477 - SFB 1173. We would like to thank Roland
Schnaubelt (KIT) for useful remarks on the invariance of Maxwell’s equations
in media under change of basis. The involved computations for the Fresnel
surface and its visualization in Figure 2 were performed by using MAPLETM.

## Note on published version

This version of the article has been accepted for publication, after peer
review (when applicable) but is not the Version of Record and does not reflect
post-acceptance improvements, or any corrections. The Version of Record is
available online at: http://dx.doi.org/10.1007/s00023-021-01144-y.

## References

  * [1] J.-G. Bak, D. McMichael, and D. Oberlin.  $L^{p}$-$L^{q}$ estimates off the line of duality.  J. Austral. Math. Soc. Ser. A, 58(2):154–166, 1995.
  * [2] Jong-Guk Bak.  Sharp estimates for the Bochner-Riesz operator of negative order in ${\bf R}^{2}$.  Proc. Amer. Math. Soc., 125(7):1977–1986, 1997.
  * [3] Jöran Bergh and Jörgen Löfström.  Interpolation spaces. An introduction.  Springer-Verlag, Berlin-New York, 1976.  Grundlehren der Mathematischen Wissenschaften, No. 223.
  * [4] Denis Bonheure, Jean-Baptiste Casteras, and Rainer Mandel.  On a fourth-order nonlinear Helmholtz equation.  J. Lond. Math. Soc. (2), 99(3):831–852, 2019.
  * [5] Lennart Börjeson.  Estimates for the Bochner-Riesz operator with negative index.  Indiana Univ. Math. J., 35(2):225–233, 1986.
  * [6] Jean Bourgain.  Estimations de certaines fonctions maximales.  C. R. Acad. Sci. Paris Sér. I Math., 301(10):499–502, 1985\.
  * [7] Jean Bourgain and Larry Guth.  Bounds on oscillatory integral operators based on multilinear estimates.  Geom. Funct. Anal., 21(6):1239–1295, 2011.
  * [8] Anthony Carbery, Andreas Seeger, Stephen Wainger, and James Wright.  Classes of singular integral operators along variable lines.  J. Geom. Anal., 9(4):583–605, 1999.
  * [9] Jean-Baptiste Castéras and Juraj Földes.  Existence of traveling waves for a fourth order Schrödinger equation with mixed dispersion in the Helmholtz regime.  arXiv e-prints, page arXiv:2103.11440, March 2021.
  * [10] Yonggeun Cho, Youngcheol Kim, Sanghyuk Lee, and Yongsun Shim.  Sharp $L^{p}$-$L^{q}$ estimates for Bochner-Riesz operators of negative index in $\mathbb{R}^{n}$, $n\geq 3$.  J. Funct. Anal., 218(1):150–167, 2005.
  * [11] Lucrezia Cossetti and Rainer Mandel.  A limiting absorption principle for Helmholtz systems and time-harmonic isotropic Maxwell’s equations.  arXiv e-prints, page arXiv:2009.05087, September 2020.
  * [12] Gaston Darboux.  Leçons sur la théorie générale des surfaces. III, IV.  Les Grands Classiques Gauthier-Villars. [Gauthier-Villars Great Classics]. Éditions Jacques Gabay, Sceaux, 1993.
  * [13] László Erdős and Manfred Salmhofer.  Decay of the Fourier transform of surfaces with vanishing curvature.  Math. Z., 257(2):261–294, 2007.
  * [14] Charles Fefferman.  Inequalities for strongly singular convolution operators.  Acta Math., 124:9–36, 1970.
  * [15] Richard P. Feynman, Robert B. Leighton, and Matthew Sands.  The Feynman lectures on physics. Vol. 2: Mainly electromagnetism and matter.  Addison-Wesley Publishing Co., Inc., Reading, Mass.-London, 1964.
  * [16] Kuno Fladt and Arnold Baur.  Analytische Geometrie spezieller Flächen und Raumkurven.  Friedr. Vieweg & Sohn, Braunschweig, 1975.  Sammlung Vieweg, Band 136.
  * [17] J. Ginibre and G. Velo.  On a class of nonlinear Schrödinger equations. I. The Cauchy problem, general case.  J. Functional Analysis, 32(1):1–32, 1979.
  * [18] Ron Goldman.  Curvature formulas for implicit curves and surfaces.  Comput. Aided Geom. Design, 22(7):632–658, 2005.
  * [19] Loukas Grafakos.  Classical Fourier analysis, volume 249 of Graduate Texts in Mathematics.  Springer, New York, third edition, 2014.
  * [20] Michael Greenblatt.  The asymptotic behavior of degenerate oscillatory integrals in two dimensions.  J. Funct. Anal., 257(6):1759–1798, 2009.
  * [21] Michael Greenblatt.  Estimates for Fourier transforms of surface measures in $\mathbb{R}^{3}$ and PDE applications.  Rev. Mat. Iberoam., 32(2):419–446, 2016.
  * [22] Allan Greenleaf.  Principal curvature and harmonic analysis.  Indiana Univ. Math. J., 30(4):519–537, 1981.
  * [23] Larry Guth, Jonathan Hickman, and Marina Iliopoulou.  Sharp estimates for oscillatory integral operators via polynomial partitioning.  Acta Math., 223(2):251–376, 2019.
  * [24] Susana Gutiérrez.  A note on restricted weak-type estimates for Bochner-Riesz operators with negative index in ${\bf R}^{n},\ n\geq 2$.  Proc. Amer. Math. Soc., 128(2):495–501, 2000.
  * [25] Susana Gutiérrez.  Non trivial $L^{q}$ solutions to the Ginzburg-Landau equation.  Math. Ann., 328(1-2):1–25, 2004.
  * [26] Lars Hörmander.  The analysis of linear partial differential operators. I.  Classics in Mathematics. Springer-Verlag, Berlin, 2003.  Distribution theory and Fourier analysis, Reprint of the second (1990) edition [Springer, Berlin; MR1065993 (91m:35001a)].
  * [27] Isroil A. Ikromov, Michael Kempe, and Detlef Müller.  Estimates for maximal functions associated with hypersurfaces in $\mathbb{R}^{3}$ and related problems of harmonic analysis.  Acta Math., 204(2):151–271, 2010.
  * [28] Isroil A. Ikromov and Detlef Müller.  Uniform estimates for the Fourier transform of surface carried measures in $\mathbb{R}^{3}$ and an application to Fourier restriction.  J. Fourier Anal. Appl., 17(6):1292–1332, 2011.
  * [29] Isroil A. Ikromov and Detlef Müller.  Fourier restriction for hypersurfaces in three dimensions and Newton polyhedra, volume 194 of Annals of Mathematics Studies.  Princeton University Press, Princeton, NJ, 2016.
  * [30] Eunhee Jeong, Yehyun Kwon, and Sanghyuk Lee.  Uniform Sobolev inequalities for second order non-elliptic differential operators.  Adv. Math., 302:323–350, 2016.
  * [31] Markus Keel and Terence Tao.  Endpoint Strichartz estimates.  Amer. J. Math., 120(5):955–980, 1998.
  * [32] H. Knörrer.  Die Fresnelsche Wellenfläche.  In Arithmetik und Geometrie, volume 3 of Math. Miniaturen, pages 115–141. Birkhäuser, Basel, 1986.
  * [33] Yehyun Kwon and Sanghyuk Lee.  Sharp resolvent estimates outside of the uniform boundedness range.  Comm. Math. Phys., 374(3):1417–1467, 2020.
  * [34] L. D. Landau and E. M. Lifschitz.  Lehrbuch der theoretischen Physik (“Landau-Lifschitz”). Band VIII.  Akademie-Verlag, Berlin, fifth edition, 1990.  Elektrodynamik der Kontinua. [Electrodynamics of continua].
  * [35] Sanghyuk Lee.  Some sharp bounds for the cone multiplier of negative order in ${\mathbb{R}}^{3}$.  Bull. London Math. Soc., 35(3):373–390, 2003.
  * [36] Otto Liess.  Decay estimates for the solutions of the system of crystal optics.  Asymptotic Anal., 4(1):61–95, 1991.
  * [37] Walter Littman.  Fourier transforms of surface-carried measures and differentiability of surface averages.  Bull. Amer. Math. Soc., 69:766–770, 1963.
  * [38] D. H. Phong and E. M. Stein.  The Newton polyhedron and oscillatory integral operators.  Acta Math., 179(1):105–152, 1997.
  * [39] Robert Schippa.  Resolvent estimates for time-harmonic maxwell’s equations in the partially anisotropic case.
  * [40] Christopher D. Sogge.  Oscillatory integrals and spherical harmonics.  Duke Math. J., 53(1):43–65, 1986.
  * [41] Elias M. Stein.  Harmonic analysis: real-variable methods, orthogonality, and oscillatory integrals, volume 43 of Princeton Mathematical Series.  Princeton University Press, Princeton, NJ, 1993.  With the assistance of Timothy S. Murphy, Monographs in Harmonic Analysis, III.
  * [42] T. Tao.  A sharp bilinear restrictions estimate for paraboloids.  Geom. Funct. Anal., 13(6):1359–1384, 2003.
  * [43] Peter A. Tomas.  A restriction theorem for the Fourier transform.  Bull. Amer. Math. Soc., 81:477–478, 1975.
  * [44] A. N. Varčenko.  Newton polyhedra and estimates of oscillatory integrals.  Funkcional. Anal. i Priložen., 10(3):13–38, 1976.
  * [45] L. Wisewell.  Kakeya sets of curves.  Geom. Funct. Anal., 15(6):1319–1362, 2005.


11institutetext: Vanderbilt University, Nashville TN 37235, USA 11email:
<EMAIL_ADDRESS>University of Southern
California, Los Angeles, CA 90089, USA

# EduSAT: A Pedagogical Tool for Theory and Applications of Boolean
Satisfiability

Yiqi Zhao 11 2 2 0009-0007-4283-6358 Ziyan An 11 0000-0002-1083-0011
Meiyi Ma 11 0000-0001-6916-8774 Taylor Johnson 11 0000-0001-8021-9923

###### Abstract

Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are
widely used in automated verification, but there is a lack of interactive
tools designed for educational purposes in this field. To address this gap, we
present EduSAT, a pedagogical tool specifically developed to support learning
and understanding of SAT and SMT solving. EduSAT offers implementations of key
algorithms such as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and the
Reduced Order Binary Decision Diagram (ROBDD) for SAT solving. Additionally,
EduSAT provides solver abstractions for five NP-complete problems beyond SAT
and SMT. Users can benefit from EduSAT by experimenting, analyzing, and
validating their understanding of SAT and SMT solving techniques. Our tool is
accompanied by comprehensive documentation and tutorials, extensive testing,
and practical features such as a natural language interface and SAT and SMT
formula generators, which also serve as a valuable opportunity for learners to
deepen their understanding. Our evaluation of EduSAT demonstrates its high
accuracy, achieving 100% correctness across all the implemented SAT and SMT
solvers. We release EduSAT as a python package in .whl file, and the source
can be identified at https://github.com/zhaoy37/SAT_Solver.

###### Keywords:

Boolean Satisfiability Satisfiability Modulo Theories NP-completeness.

##  1 Introduction

Formal verification is a critical field with a focus to prove or disprove the
safety, liveness, and other properties of a system using mathematical
techniques such as induction. It is widely applied to circuit design [1],
autonomous vehicles [2], and operating systems [3], etc. Many solutions to
verification problems relate to the solutions of Boolean Satisfiability
Problems (SAT) and its variant, Satisfiability Modulo Theories (SMT). Bounded
Model Checking (BMC) of a discrete system, for instance, can be encoded as an
equivalent SAT problem and solved with a domain specific solver such as Z3
[4]. Furthermore, by the Cook-Levin Theorem, SAT is NP-complete, which
suggests that problems that are in NP, such as graph coloring, can be reduced
to a SAT problem by a deterministic Turing Machine in polynomial time.

Despite the significance of SAT and SMT, we observe a lack of open-source
solvers for SAT problems with a pedagogical purpose not to mention
demonstrations of how some classical NP-complete problems are encoded into SAT
or SMT formulations. One of the most commonly used SMT solver is Z3 [4], which
is based on DPLL and incorporates quantifier instatiation using E-matching and
relevancy propagation, etc. Despite that the codes from Z3 are available for
public use, Z3 is designed for efficient solutions in real-life circumstances
without a focus on the educational value. Other state-of-the-art SMT solvers
include CVC4 (Cooperating Validity Checker) [5], which is also based on
DPLL(T) and uses simplex method for its arithmetic, and Yices 2 [6], which
uses a SAT solver with CDCL approach. LearnSAT [7], in comparison, is an
educational tool that introduces techniques for SAT solving through the
language of prolog. Despite the conciseness of logic programming, most
students undergoing Computer Science educations are more exposed to and most
oftenly use procedural and object-oriented programming paradigms. To bridge
this gap and guide users through the object-oriented designs, we introduce
EduSAT, a python-based Boolean Satisfiability Solver with support for SMT over
integer predicates, corresponding formula generators and natural language
interfaces, as well as extensions for solvers of 5 NP-complete problems (apart
from SMT and SAT). We also introduce an interactive tutorial built in jupyter
notebook and documentations in github.

We present the architecture of our educational tool in Figure 1.

Figure 1: Architecture of EduSAT

##  2 Tool Details

SAT refers to the problem to determine if there exists a model to a Boolean
formula $P$ such that the model evaluates to true. SMT, on the other hand,
extends the acceptable formula, $P$ to many-sorted formulas. In EduSAT, we
only consider formulas with integer variables with the following operators:
$+,-,\times,//,>,<,\leq,\geq,=$, where $//$ represents integer division. For
SMT problems, we also limit our solvers to a finite search space specified by
the user and guarantee correctness only in this range, since the focus is in
introducing the solving techniques.

###  2.1 SAT Solving

We implement two SAT solvers, the DPLL solver and the ROBDD solver. The DPLL
solver uses recursive backtracking with heuristics revolving around assignment
decidings and deducings. We focus on 3 heuristics specifically: Early
termination refers to terminating the algorithm if any realization of an atom
leads to True or False of a SAT formula in the search process. Unit clauses
refers to the simplification of the SAT formula left with one literal via
realizing that literal. Pure literals refers to that if all appearances of a
symbol in a negation normal form of the SAT formula have the same sign across
the clause, we can guess that the symbol is True (for positive symbol) or
False (for negative symbol) in assigning during recursive backtracking.

The ROBDD solver provides an ordered canonical form of logic representation
with a directed acyclic graph that consists of multiple decision nodes, two
terminal nodes, and the corresponding edges. The terminal nodes in a ROBDD
represent the constants true $\top$ and false $\bot$, the decision nodes
represent variables or parameters, and the edges $E\in\\{low,high\\}$
represent the assignment of truth values to variables, where the low edges
represent the assignment of false, and the high edges represent the assignment
of true. The construction of a ROBDD from a Binary Decision Tree follows the
elimination rule and isomorphic rule [8], such that there are no redundant
nodes with identical sub-trees, and all terminal nodes are combined.

###  2.2 SMT Solving and NP-complete Problems

In SMT solving, we first encode each arithmetic clause appeared in an SMT
problem as an atom of a SAT problem, which is solved accordingly using the
aforementioned SAT solvers. We then substitute all possible realizations of
the SAT problem to construct a Constraint Satisfaction Problem (CSP)
equivalent to the SMT formula and allow it to be solved through 2 methods:
recursive backtracking and min-conflicts. In recursive backtracking, the
solver performs an exhaustive search for the valuations of the SMT variables
over a user-specified range. In min-conflicts, the algorithm first randomly
initializes the values for the set of all SMT variables. While the assignment
does not satisfy the formula, the algorithm randomly picks a variable from all
the SMT variables that result in conflict(s), and find the value that best
reduces the conflicts associated with that variable to update the assignment.
The algorithm terminates when an assignment is found to satisfy the SMT
formula or when the maximum number of iteration steps is achieved. Please note
that the algorithm may report unsatisfiability even if there exists a solution
if the maximum iteration steps is not sufficiently large (which rarely occurs
for a large number of iterations). However, this approach can be faster than
the naive backtracking approach when applied to some of our NP-complete
problem solver(s) such as the N-queens problem solver.

With the implemented SMT solvers, we create NP-complete problem solver
abstractions for 5 problems listed in Figure 1. For example, in the N-queens
problem, given an n by n sized chess board, the algorithm is asked to place n
queens on the board such that no two queens attack each other. We encode this
as an equivalent SMT problem: Each SMT variable represents a column, and the
assignmnent to that variable represents the row index of the queen in that
column. Then, in the SMT clause, the solver is supported with representations
that no two queens can be in the same row and no two queens can be in the same
diagonal. We solve the SMT problem accordingly to find the solution to the
N-queens problem.

##  3 Evaluations

In this section, we demonstrate the accuracy and the efficiency of the SAT
solvers. Due to the space limitation, we leave other evaluations (on the SMT
solver for instance) in the GitHub repository.

###  3.1 Evaluation on the SAT Solvers

####  3.1.1 DPLL Solver

All evaluations for the DPLL Solver were conducted on an Apple M1 Pro chip
with 16 GB memory. In terms of efficiency, we evaluated how the effects of the
number of formulas solved and the difference between single vs. multiple
solutions affected the speed of the DPLL solver through controlled experiment
trials. In each experimental trial, we generated random Boolean logic trees
(with chance of not node, and node and or node held constant at 0.1, 0.45, and
0.45 respectively) and provided solutions to such trees using both a naive
tabular solution (recursive backtracking without heuristic) and the DPLL
solver with heuristics and compared the performances.

In terms of the accuracy, we evaluated the solutions provided by both the
naive solver and the solver with heuristics directly using the evaluation
feature of the logic trees instead of formula simplifications performed by the
solver. For the cases of unsatisfiability and the completeness of solutions
(when it comes to inquiries of multiple solutions), we cross checked the
results generated by the DPLL solver and by the naive recursive backtracking
solver.

We observe 100% accuracy for both of the naive solver and the solver with
heuristics for all trials we performed. Moreover, the solver with heuristics
outperform the naive solver in terms of efficiency in all trials we performed.
We demonstrate the evaluation results (in terms of efficiency) in Table 1. All
time units are in seconds.

Table 1: Efficiency of the DPLL Solver with Varying Number of Formulas

No. Formulas Single or not No. Variables Depth Solving Time (No Heuristic)
Solving Time (Heuristic) 10 Single 5 8 0.0064 0.0016 100 Single 5 8 0.072
0.014 1000 Single 5 8 0.76 0.15 10 Multiple 5 8 0.025 0.0032 100 Multiple 5 8
0.17 0.034 1000 Multiple 5 8 1.74 0.35

####  3.1.2 ROBDD Solver

All experiments were performed on an Intel Core i9-10850K CPU running at
3.60GHz. The accuracy and efficiency of the ROBDD SAT solver were evaluated
using the same format as DPLL. To measure efficiency, we recorded the runtime
from the conversion of a BDT to a ROBDD to the completion of finding all SAT
solutions. To evaluate accuracy, we generated different numbers of logic
formulas with varying numbers of variables and depths, then verified the
solutions provided by the ROBDD solver by substituting them back into the
formulas. Table 2 presents the evaluation results.

Table 2: ROBDD solver with varying number of formulas, variables, and depth.

Formulas Parameters Depth Single Solution (s) Multiple Solutions (s) Accuracy
(Single) Accuracy (Multiple) 10 5 5 0.0027 0.0030 100% 100% 10 5 6 0.0027
0.0033 100% 100% 10 5 7 0.0028 0.0035 100% 100% 10 3 3 0.0011 0.0009 100% 100%
100 3 3 0.0090 0.0100 100% 100% 1000 3 3 0.1000 0.1075 100% 100%

Note that for multiple solutions tasks, we find all possible solutions to a
logic formula, while for single solution tasks, we always provide the shortest
and simplest solutions. We observe a slight increase in runtime for multiple
solution tasks compared to single solution tasks. It is also evident that the
total solving time generally increases as the number of formulas and the depth
increase, which is as expected. We note that the ROBDD solver achieved 100%
accuracy in both the single solution task and the multiple solution task.

##  4 An Illustrative Case Study on ROBDD

We present visual demonstrations of the ROBDD functionality in Fig.3 and
Fig.3. Specifically, they showcase the ROBDD with different parameter orders
for a complex formula,
$f(x_{0},x_{1},x_{2},x_{3},x_{4},x_{5},x_{6},x_{7})=((x_{0}\wedge
x_{1})\vee(x_{2}\wedge x_{3})\vee(x_{4}\wedge x_{5})\vee(x_{6}\wedge x_{7}))$.
Although our tool offers truth table visualizations, we find that truth tables
become significantly less efficient as the number of parameters increases.
Overall, the visualization of ROBDDs provides a clear and concise
understanding of the logic formula structure, making it easier for users to
identify potential issues with their logic.

Figure 2: Variable order: $x_{0},\ldots x_{7}$.

Figure 3: Variable order: $x_{7},\ldots x_{0}$.

##  5 Conclusion

We construct a pedagogical tool, EduSAT, for SAT solving and its applications.
We introduce essential concepts such as DPLL, ROBDD, recursive backtracking in
SMT solving, min-conflicts, as well as methodologies for solving NP-complete
problems via SMT formulations. The tool achieves a high accuracy and
efficiency. At the same time, we implement detailed documentations, tutorials,
and interactive components such as the natural language interface and the
ROBDD visual demonstrations to allow better understanding from the users.

## References

  * [1] Jain, J., Narayan, A., Fujita, M., Sangiovanni-Vincentelli, A.: Formal verification of Combinational Circuits. In: Proceedings 10th International Conference on VLSI Design. (1997)
  * [2] Kamali, M., Dennis, L., McAree, O., Fisher, M., Veres, S.: Formal verification of autonomous vehicle platooning. Science of Computer Programming. 148, 88-106, (2017). https://doi.org/10.1016/j.scico.2017.05.006.
  * [3] Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S. In: sel4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd symposium on Operating sytems principles. (2009)
  * [4] de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. Tools and Algorithms for the Construction and Analysis of Systems. 337-340, (2008). https://doi.org/10.1007/978-3-540-78800-3_24
  * [5] Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: International Conference on Computer Aided Verification 2011, LNCS, vol. 6806. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14
  * [6] Dutertre, B.: Yices 2.2. In: International Conference on Computer Aided Verification 2014, LNCS, vol. 8559. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-319-08867-9_49
  * [7] Mordechai, B.: LearnSAT: A SAT Solver for Education. In: International Conference on Theory and Applications of Satisfiability Testing 2013, LNCS, vol. 7962. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_30
  * [8] Andersen, Henrik Reif. ”An introduction to binary decision diagrams.” Lecture notes, available online, IT University of Copenhagen (1997): 5.