rq_{\beta}(b,c)>\frac{1}{\xi}\left(k-\frac{b+c}{4}-\frac{s_{max}-1}{s_{max}}E_{0}\right),$
$\displaystyle(4^{\prime})\ \
0<\frac{1}{\xi}\left(k-\frac{b+c}{4}-\frac{s_{max}-1}{s_{max}}E_{0}\right)<b,$
over $\displaystyle k>0\ \,\mbox{and}\,\ 0<b<c.$

The new objective function is decreasing in $k$. This implies that the maximum
is achieved by taking $k=rq_{\beta}(b,c)$ in (1’), which entails a recovery
adjustment equal to

$\frac{rq_{\beta}(b,c)-rq_{\beta}(b,c)+E_{0}}{\frac{E_{0}}{s_{max}}}=s_{max}.$

In this case, condition (2’) is automatically satisfied. We need to show when
there exist $0<b<c$ satisfying all the remaining conditions, namely (3’) and
(4’), under $k=rq_{\beta}(b,c)$. We focus on the case
$\beta\geq\frac{\alpha}{2}$. In this case, setting
$\lambda=\sqrt{\frac{\alpha-\beta}{2\alpha}}\in(0,\frac{1}{2}]$, we can write
$q_{\beta}(b,c)=(1-\lambda)b+\lambda c$. Condition (3’) can equivalently be
written as

$\left((1-\xi)r(1-\lambda)-\frac{1}{4}\right)b+\left((1-\xi)r\lambda-\frac{1}{4}\right)c<\frac{s_{max}-1}{s_{max}}E_{0}.$

This holds for all $0<b<c$ provided that the two expressions multiplying $b$
and $c$ are both negative, i.e.

$r\leq\frac{1}{4}\frac{1}{(1-\lambda)(1-\xi)}.$ (23)

Similarly, condition (4’) is equivalent to

$\frac{s_{max}-1}{s_{max}}E_{0}-\left(r(1-\lambda)-\frac{1}{4}\right)b<\left(r\lambda-\frac{1}{4}\right)c<\frac{s_{max}-1}{s_{max}}E_{0}.$

For every $b>0$, this holds for a suitable $c>0$ provided that the expression
in parenthesis multiplying $b$ and the expression multiplying $c$ are both
strictly positive, i.e.

$r>\frac{1}{4\lambda}.$ (24)

To ensure that $c$ can be taken to satisfy $c>b$, it suffices to impose the
bound $b<\frac{1}{r\lambda-\frac{1}{4}}\frac{s_{max}-1}{s_{max}}E_{0}$. This
shows that we can indeed find $0<b<c$ satisfying (3’) and (4’) under
$k=rq_{\beta}(b,c)$ provided that (23) and (24) hold. ∎

###  A.14 Proof of Proposition 18

###### Proof.

We rely on Lemma 5.6 in tasche1999risk. To this effect, the random variables

$X^{1}=-(\Delta E^{1}_{1}+(1-r_{j})L^{1}_{1}),\dots,X^{N}=-(\Delta
E^{N}_{1}+(1-r_{j})L^{N}_{1})$

have to satisfy the so-called (S)-Assumption in that paper. This stipulates
some requirements on the joint distribution of the above random variables,
namely:

  * •

$X^{1},\dots,X^{N}$ are integrable and continuously distributed;

  * •

the conditional distribution of $X^{1}$ given $X^{2},\dots,X^{N}$ has a
density $\phi$;

  * •

$x^{1}\mapsto\phi(x^{1},x^{2},\dots,x^{N})$ is continuous for all
$x^{2},\dots,x^{N}\in\mathbb{R}$;

  * •

the maps
$\Phi_{1},\dots,\Phi_{N}:\mathbb{R}\times\mathbb{R}\setminus\\{0\\}\times\mathbb{R}^{N-1}\to\mathbb{R}$
defined by

$\Phi_{1}(x^{1},u_{1},\dots,u_{N})=E_{P}\left(\phi\bigg{(}u_{1}^{-1}\bigg{(}x^{1}-\sum_{i=2}^{N}u_{i}X^{i}\bigg{)},X^{2},\dots,X^{N}\bigg{)}\right),$
$\Psi_{l}(x^{1},u_{1},\dots,u_{N})=E_{P}\left(X^{l}\phi\bigg{(}u_{1}^{-1}\bigg{(}x^{1}-\sum_{i=2}^{N}u_{i}X^{i}\bigg{)},X^{2},\dots,X^{N}\bigg{)}\right),\
\ \ l=2,\dots,N,$

are finite valued and continuous;

  * •

for every
$u=(u_{1},\dots,u_{N})\in\mathbb{R}\setminus\\{0\\}\times\mathbb{R}^{N-1}$ we
have

$E_{P}\left(\phi\bigg{(}u_{1}^{-1}\bigg{(}q_{\alpha_{j}}(u)-\sum_{i=2}^{N}u_{i}X^{i}\bigg{)},X^{2},\dots,X^{N}\bigg{)}\right)>0,$

where $q_{\alpha_{j}}(u)=\inf\\{x\in\mathbb{R}\,;\
\mathbb{P}(\sum_{i=1}^{N}u_{i}X^{i}\leq x)\geq 1-\alpha_{j}\\}$.

Now, fix $i=1,\dots,N$ and for every $k=1,\dots,n+1$ consider the convex
(hence, continuous) function $f^{i,k}:\mathbb{R}\to\mathbb{R}$ defined by
setting

$f^{i,k}(h)={\rm AV@R}_{\alpha_{k}}(\Delta E_{1}+(1-r_{k})L_{1}+h(\Delta
E^{i}_{1}+(1-r_{k})L_{1}^{i})).$

By assumption we have that

$f^{i,j}(0)>\max_{k=1,\dots,n+1,\,\,k\neq j}f^{i,k}(0).$

It follows from continuity that there exists $\varepsilon>0$ such that

$f^{i,j}(h)>\max_{k=1,\dots,n+1,\,\,k\neq j}f^{i,k}(h).$

for every $h\in(-\varepsilon,\varepsilon)$. As a result,

${\rm RecAV@R}_{\gamma}(\Delta E_{1}+h\Delta
E^{i}_{1},L_{1}+hL^{i}_{1})=\max_{k=1,\dots,n+1}f^{i,k}(h)=f^{i,j}(h)$

for every $h\in(-\varepsilon,\varepsilon)$. This immediately yields

$\frac{d}{dh}{\rm RecAV@R}_{\gamma}(\Delta E_{1}+h\Delta
E^{i}_{1},L_{1}+hL^{i}_{1})_{|_{h=0}}=\frac{df^{i,j}}{dh}(0).$

Since the (S)-Assumption holds, we infer from Theorem 4.4 in tasche1999risk
that

$\frac{df^{i,j}}{dh}(0)=-E\big{(}\Delta
E^{i}_{1}+(1-r_{j})L^{i}_{1}\,|\,\Delta E_{1}+(1-r_{j})L_{1}\leq-{\rm
V@R}_{\alpha_{j}}(\Delta E_{1}+(1-r_{j})L_{1})\big{)}.$

This delivers the desired statement. ∎

###  A.15 Proof of Theorem 19

###### Proof.

Set
$\Delta^{n}=\\{(\theta^{1},\dots,\theta^{n+1})^{\top}\in[0,\infty)^{n+1}\,;\
\sum_{i=1}^{n+1}\theta^{i}=1\\}$. We first observe that

$\max_{i=1,\dots,n+1}\;\inf_{v\in\mathbb{R}}\;\Psi^{i}(\bm{x},v)\;=\;\max_{\bm{\theta}\in\Delta^{n}}\;\inf_{v\in\mathbb{R}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v).$

Now arguing as in the proof of Theorem 1 of ZhuFu09 one shows that there
exists a nonempty, closed, bounded interval $\mathcal{B}$ (which depends on
$\bm{x}$) such that

$\max_{\bm{\theta}\in\Delta^{n}}\;\inf_{v\in\mathbb{R}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v)\;=\;\max_{\bm{\theta}\in\Delta^{n}}\;\min_{v\in\mathcal{B}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v).$
(25)

More precisely, note that for every $i=1,\dots,n+1$ the function $\Psi^{i}$ is
convex in $v$. We know from the classical results by Rockafellar and Uryasev
RU00 and Rockafellar and Uryasev RU02 that $\Psi^{i}$ attains its minimum in a
(nonempty) closed bounded interval $[q^{-}_{i},q^{+}_{i}]$ (where the extremes
are given by the lower, respectively, upper $\alpha_{i}$ quantiles of
$\sum_{k=1}^{K}x^{k}R^{k}-r_{i}Z$). At this point, the critical observation is
that any convex combination of the functions $\Psi^{1},\dots,\Psi^{n+1}$ also
attains its minimum in a (nonempty) closed bounded interval which is included
in the closed bounded interval

$\mathcal{B}=\left[\min_{i=1,\dots,n+1}\;q^{-}_{i},\max_{i=1,\dots,n+1}\;q^{+}_{i}\right].$

This can be easily established by induction on $n$. It is key to note that
${\mathcal{B}}$ does not depend on the particular convex combination chosen.
This yields (25). Now, observe that the function
$(\bm{\theta},v)\mapsto\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v)$ is linear
in $\bm{\theta}$, convex in $v$, and continuous in both variables. Thus, by a
classical minimax theorem, see, e.g., Theorem 1 in fan1953minimax, it follows
that

$\max_{\bm{\theta}\in\Delta^{n}}\;\min_{v\in\mathcal{B}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v)\;=\;\min_{v\in\mathcal{B}}\;\max_{\bm{\theta}\in\Delta^{n}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v)\;=\;\min_{v\in\mathbb{R}}\;\max_{\bm{\theta}\in\Delta^{n}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v).$

In the last step, the inequality $\geq$ follows from
$\mathcal{B}\subseteq\mathbb{R}$ while the inequality $\leq$ is a consequence
of the minimax inequality

$\max_{\bm{\theta}\in\Delta^{n}}\;\inf_{v\in\mathbb{R}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v)\;\leq\;\inf_{v\in\mathbb{R}}\;\max_{\bm{\theta}\in\Delta^{n}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v).$

Finally, observe that

$\min_{v\in\mathbb{R}}\;\max_{\bm{\theta}\in\Delta^{n}}\;\sum_{i=1}^{n+1}\theta^{i}\Psi^{i}(\bm{x},v)\;=\;\min_{v\in\mathbb{R}}\;\max_{i=1,\dots,n+1}\;\Psi^{i}(\bm{x},v).$

This delivers the desired minimax equality. ∎

##  Appendix B Complementary Figures

Figure 5: The loss probability $\mathbb{P}(\Delta E_{1}<0)$ as a function of
$\rho$ (left) for $\tau=1$ (green) and $\tau=5$ (red) and as a function of
$\tau$ (right) for $\rho=0.1$ (red) and $\rho=0.9$ (green).

Figure 6: The regulatory risk measure $\rho_{reg}(E_{1})$ as a function of
$\rho$ (left) for $\tau=1$ (green) and $\tau=5$ (red) and as a function of
$\tau$ (right) for $\rho=0.1$ (red) and $\rho=0.9$ (green).

Figure 7: The solvency ratio $\frac{E_{0}}{\rho_{reg}(\Delta E_{1})}$ as a
function of $\rho$ (left) for $\tau=1$ (green) and $\tau=5$ (red) and as a
function of $\tau$ (right) for $\rho=0.1$ (red) and $\rho=0.9$ (green).

Figure 8: The recovery adjustment $\mathop{\rm RecAdj}\nolimits(\beta,r)$ for
$\beta=\beta_{max}=0.25\%$ and $r=r_{min}=50\%$ as a function of $\rho$ (left)
for $\tau=1$ (green) and $\tau=5$ (red) and as a function of $\tau$ (right)
for $\rho=0.1$ (red) and $\rho=0.9$ (green).

Figure 9: The recovery adjustment $\mathop{\rm RecAdj}\nolimits(\beta,r)$ for
$\beta=\beta_{min}=0.1\%$ and $r=r_{max}=90\%$ as a function of $\rho$ (left)
for $\tau=1$ (green) and $\tau=5$ (red) and as a function of $\tau$ (right)
for $\rho=0.1$ (red) and $\rho=0.9$ (green).

## References

  * [1] Acerbi Tasche2002acerbi2002coherence Acerbi, Carlo Dirk Tasche 2002, ‘On the coherence of expected shortfall’, Journal of Banking & Finance 26(7), 1487–1503.
  * [2] Aliprantis Border2006aliprantis06 Aliprantis, Charalambos D. Kim C. Border 2006, Infinite Dimensional Analysis: a Hitchhiker’s Guide, Springer, Berlin; London.
  * [3] [Altman et al.]Altman, Brady, Resti Sironi2005altman2005link Altman, Edward I, Brooks Brady, Andrea Resti Andrea Sironi 2005, ‘The link between default and recovery rates: Theory, empirical evidence, and implications’, The Journal of Business 78(6), 2203–2228.
  * [4] [Artzner et al.]Artzner, Delbaen, Eber Heath1999ADEH99 Artzner, Philippe, Freddy Delbaen, Jean-Marc Eber David Heath 1999, ‘Coherent measures of risk’, Mathematical Finance 9(3), 203–228.
  * [5] [Artzner et al.]Artzner, Delbaen Koch-Medina2009adk2009 Artzner, Philippe, Freddy Delbaen Pablo Koch-Medina 2009, ‘Risk measures and efficient use of capital’, ASTIN Bulletin 39(1), 101–116.
  * [6] Aumann Serrano2008aumann2008economic Aumann, Robert J Roberto Serrano 2008, ‘An economic index of riskiness’, Journal of Political Economy 116(5), 810–836.
  * [7] Basel Committee on Banking Supervision1988BaselI Basel Committee on Banking Supervision 1988, ‘International convergence of capital measurement and capital standards’.  Available on the webpage of the Bank of International Settlement: https://www.bis.org.
  * [8] Bauer Zanjani2013bauer2013capital Bauer, Daniel George H. Zanjani 2013, Capital allocation and its discontents, in ‘Handbook of Insurance’, Springer, pp. 863–880.
  * [9] Bauer Zanjani2016bauer2016marginal Bauer, Daniel George H. Zanjani 2016, ‘The marginal cost of risk, risk measures, and capital allocation’, Management Science 62(5), 1431–1457.
  * [10] Ben-Tal Teboulle1987BT87 Ben-Tal, Aharon Marc Teboulle 1987, ‘Penalty functions and duality in stochastic programming via $\phi$-divergence functionals’, Mathematics of Operations Research 12(2), 224–240.
  * [11] Ben-Tal Teboulle2007BT07 Ben-Tal, Aharon Marc Teboulle 2007, ‘An old-new concept of convex risk measures: The optimized certainty equivalent’, Mathematical Finance 17(3), 449–476.
  * [12] [Bernard et al.]Bernard, Rüschendorf, Vanduffel Wang2017bernard2017risk Bernard, Carole, Ludger Rüschendorf, Steven Vanduffel Ruodu Wang 2017, ‘Risk bounds for factor models’, Finance and Stochastics 21(3), 631–659.
  * [13] [Bernard et al.]Bernard, Jiang Wang2014bernard2014risk Bernard, Carole, Xiao Jiang Ruodu Wang 2014, ‘Risk aggregation with dependence uncertainty’, Insurance: Mathematics and Economics 54, 93–108.
  * [14] [Biagini et al.]Biagini, Fouque, Frittelli Meyer-Brandis2019BFFM19 Biagini, Francesca, Jean-Pierre Fouque, Marco Frittelli Thilo Meyer-Brandis 2019, ‘A unified approach to systemic risk measures via acceptance sets’, Mathematical Finance 29(1), 329–367.
  * [15] [Bielecki et al.]Bielecki, Cialenco Pitera2017bc17 Bielecki, Tomasz R., Igor Cialenco Marcin Pitera 2017, ‘A survey of time consistency of dynamic risk measures and dynamic performance measures in discrete time’, Probability, Uncertainty and Quantitative Risk 2(1), 1–52.
  * [16] [Bielecki et al.]Bielecki, Cialenco Zhang2014bielecki2014dynamic Bielecki, Tomasz R, Igor Cialenco Zhao Zhang 2014, ‘Dynamic coherent acceptability indices and their applications to finance’, Mathematical Finance 24(3), 411–441.
  * [17] [Bignozzi et al.]Bignozzi, Burzoni Munari2020bignozzi2020risk Bignozzi, Valeria, Matteo Burzoni Cosimo Munari 2020, ‘Risk measures based on benchmark loss distributions’, Journal of Risk and Insurance 87(2), 437–475.
  * [18] [Brown et al.]Brown, Giorgi Sim2012brown2012aspirational Brown, David B, Enrico De Giorgi Melvyn Sim 2012, ‘Aspirational preferences and their representation by risk measures’, Management Science 58(11), 2095–2113.
  * [19] [Cai et al.]Cai, Liu Wang2018cai2018asymptotic Cai, Jun, Haiyan Liu Ruodu Wang 2018, ‘Asymptotic equivalence of risk measures under dependence uncertainty’, Mathematical Finance 28(1), 29–49.
  * [20] [Castagnoli et al.]Castagnoli, Cattelan, Maccheroni, Tebaldi Wang2021castagnoli2021star Castagnoli, Erio, Giacomo Cattelan, Fabio Maccheroni, Claudio Tebaldi Ruodu Wang 2021, ‘Star-shaped risk measures’, arXiv preprint arXiv:2103.15790 .
  * [21] [Chen et al.]Chen, Iyengar Moallemi2013chen2013axiomatic Chen, Chen, Garud Iyengar Ciamac C. Moallemi 2013, ‘An axiomatic approach to systemic risk’, Management Science 59(6), 1373–1388.
  * [22] Cherny Madan2009cherny2009 Cherny, Alexander Dilip Madan 2009, ‘New measures for performance evaluation’, The Review of Financial Studies 22(7), 2571–2606.
  * [23] Christiansen Niemeyer2014christiansen2014 Christiansen, Marcus C. Andreas Niemeyer 2014, ‘Fundamental definition of the solvency capital requirement in Solvency II’, ASTIN Bulletin 44(3), 501–533.
  * [24] [Dhaene et al.]Dhaene, Tsanakas, Valdez Vanduffel2012dhaene2012optimal Dhaene, Jan, Andreas Tsanakas, Emiliano A Valdez Steven Vanduffel 2012, ‘Optimal capital allocation principles’, Journal of Risk and Insurance 79(1), 1–28.
  * [25] Drapeau Kupper2013drapeau2013risk Drapeau, Samuel Michael Kupper 2013, ‘Risk preferences and their robust representation’, Mathematics of Operations Research 38(1), 28–62.
  * [26] Duffie Singleton1999duffie1999modeling Duffie, Darrell Kenneth J Singleton 1999, ‘Modeling term structures of defaultable bonds’, The review of financial studies 12(4), 687–720.
  * [27] [Embrechts et al.]Embrechts, Puccetti Rüschendorf2013embrechts2013model Embrechts, Paul, Giovanni Puccetti Ludger Rüschendorf 2013, ‘Model uncertainty and var aggregation’, Journal of Banking & Finance 37(8), 2750–2764.
  * [28] [Embrechts et al.]Embrechts, Liu Wang2018embrechts2018quantile Embrechts, Paul, Haiyan Liu Ruodu Wang 2018, ‘Quantile-based risk sharing’, Operations Research 66(4), 936–949.
  * [29] Fan1953fan1953minimax Fan, Ky 1953, ‘Minimax theorems’, Proceedings of the National Academy of Sciences of the United States of America 39(1), 42.
  * [30] [Farkas et al.]Farkas, Koch-Medina Munari2014farkas2014beyond Farkas, Walter, Pablo Koch-Medina Cosimo Munari 2014, ‘Beyond cash-additive risk measures: when changing the numéraire fails’, Finance and Stochastics 18(1), 145–173.
  * [31] [Feinstein et al.]Feinstein, Rudloff Weber2017FRW17 Feinstein, Zachary, Birgit Rudloff Stefan Weber 2017, ‘Measures of systemic risk’, SIAM Journal on Financial Mathematics 8(1), 672–708.
  * [32] Filipović Svindland2008filipovic2008optimal Filipović, Damir Gregor Svindland 2008, ‘Optimal capital and risk allocations for law-and cash-invariant convex functions’, Finance and Stochastics 12(3), 423–439.
  * [33] Föllmer Schied2002FS02 Föllmer, Hans Alexander Schied 2002, ‘Convex measures of risk and trading constraints’, Finance and Stochastics 6(4), 429 – 447.
  * [34] Föllmer Schied2016FS Föllmer, Hans Alexander Schied 2016, Stochastic finance – An introduction in discrete time, Graduate Textbook Series, 4th edn, De Gruyter, Berlin.
  * [35] [Föllmer et al.]Föllmer, Schied Weber2009FSW09 Föllmer, Hans, Alexander Schied Stefan Weber 2009, Robust preferences and robust portfolio choice, in ‘Handbook of Numerical Analysis’, Springer, pp. 29–89.
  * [36] Föllmer Weber2015FW15 Föllmer, Hans Stefan Weber 2015, ‘The axiomatic approach to risk measurement for capital determination’, Annual Review of Financial Economics 7, 301–337.
  * [37] Foster Hart2009foster2009operational Foster, Dean P Sergiu Hart 2009, ‘An operational measure of riskiness’, Journal of Political Economy 117(5), 785–814.
  * [38] Frittelli Gianin2002frittelli2002 Frittelli, Marco Emanuela Rosazza Gianin 2002, ‘Putting order in risk measures’, Journal of Banking & Finance 26(7), 1473–1486.
  * [39] [Gao et al.]Gao, Leung, Munari Xanthos2018gao2018fatou Gao, Niushan, Denny Leung, Cosimo Munari Foivos Xanthos 2018, ‘Fatou property, representations, and extensions of law-invariant risk measures on general Orlicz spaces’, Finance and Stochastics 22(2), 395–415.
  * [40] Glasserman2013glasserman2013 Glasserman, Paul 2013, Monte Carlo methods in financial engineering, Vol. 53, Springer Science & Business Media.
  * [41] [Guo et al.]Guo, Bauer Zanjani2020bauer2020 Guo, Qiheng, Daniel Bauer George H. Zanjani 2020, ‘Capital allocation techniques: Review and comparison’, Variance .  To appear.
  * [42] [Guo et al.]Guo, Jarrow Zeng2009guo2009modeling Guo, Xin, Robert A Jarrow Yan Zeng 2009, ‘Modeling the recovery rate in a reduced form model’, Mathematical Finance: An International Journal of Mathematics, Statistics and Financial Economics 19(1), 73–97.
  * [43] [Hamm et al.]Hamm, Knispel Weber2020HaKnWe20 Hamm, Anna-Maria, Thomas Knispel Stefan Weber 2020, ‘Optimal risk sharing in insurance networks’, European Actuarial Journal 10(1), 203–234.
  * [44] [Ivashina et al.]Ivashina, Iverson Smith2016ivashina2016ownership Ivashina, Victoria, Benjamin Iverson David C Smith 2016, ‘The ownership and trading of debt claims in chapter 11 restructurings’, Journal of Financial Economics 119(2), 316–335.
  * [45] [Jankowitsch et al.]Jankowitsch, Nagler Subrahmanyam2014jankowitsch2014determinants Jankowitsch, Rainer, Florian Nagler Marti G Subrahmanyam 2014, ‘The determinants of recovery rates in the us corporate bond market’, Journal of Financial Economics 114(1), 155–177.
  * [46] Jones2000Jones Jones, David 2000, ‘Emerging problems with the Basel Capital Accord: Regulatory capital arbitrage and related issues’, Journal of Banking & Finance 24(1), 35 – 58.
  * [47] [Jouini et al.]Jouini, Schachermayer Touzi2006Jouini2006 Jouini, Elyès, Walter Schachermayer Nizar Touzi 2006, Law invariant risk measures have the Fatou property, in S.Kusuoka A.Yamazaki, eds, ‘Advances in Mathematical Economics’, Springer Japan, Tokyo, pp. 49–71.
  * [48] Kalkbrener2005kalkbrener2005axiomatic Kalkbrener, Michael 2005, ‘An axiomatic approach to capital allocation’, Mathematical Finance: An International Journal of Mathematics, Statistics and Financial Economics 15(3), 425–437.
  * [49] [Khieu et al.]Khieu, Mullineaux Yi2012khieu2012determinants Khieu, Hinh D, Donald J Mullineaux Ha-Chin Yi 2012, ‘The determinants of bank loan recovery rates’, Journal of Banking & Finance 36(4), 923–933.
  * [50] Koch-Medina Munari2016koch2016unexpected Koch-Medina, Pablo Cosimo Munari 2016, ‘Unexpected shortfalls of expected shortfall: Extreme default profiles and regulatory arbitrage’, Journal of Banking & Finance 62, 141–151.
  * [51] [Kromer et al.]Kromer, Overbeck Zilch2016kromer2013systemic Kromer, Eduard, Ludger Overbeck Katrin Zilch 2016, ‘Systemic risk measures on general measurable spaces’, Mathematical Methods of Operations Research 84(2), 323–357.
  * [52] Li Wang2019PELVEwang Li, Hanson Ruodu Wang 2019, ‘Pelve: Probability equivalent level of var and es’, SSRN preprint SSRN:3489566 .
  * [53] Markowitz1952Markowitz52 Markowitz, Harry Max 1952, ‘Portfolio selection’, The Journal of Finance 7(1), 77–91.
  * [54] Nelsen2007nelsen2007 Nelsen, Roger B. 2007, An introduction to copulas, Springer Science & Business Media.
  * [55] Rockafellar Uryasev2000RU00 Rockafellar, R. Tyrrell Stanislav Uryasev 2000, ‘Optimization of conditional value-at-risk’, Journal of Risk 2(3), 21–41.
  * [56] Rockafellar Uryasev2002RU02 Rockafellar, R. Tyrrell Stanislav Uryasev 2002, ‘Conditional value-at-risk for general loss distributions’, Journal of Banking $\&$ Finance 26, 1443–1471.
  * [57] Rosazza Gianin Sgarra2013gianin2013acceptability Rosazza Gianin, Emanuela Carlo Sgarra 2013, ‘Acceptability indexes via $g$-expectations: an application to liquidity risk’, Mathematics and financial economics 7(4), 457–475.
  * [58] Tasche2000tasche1999risk Tasche, Dirk 2000, ‘Risk contributions and performance measurement’, Report – Lehrstuhl für mathematische Statistik, TU München pp. 1–26.
  * [59] Tasche2004tasche2004allocating Tasche, Dirk 2004, Allocating portfolio economic capital to sub-portfolios, in A.Dev, ed., ‘Economic capital: a practitioner guide’, Risk Books London, pp. 275–302.
  * [60] Tasche2008tasche2007capital Tasche, Dirk 2008, Capital allocation to business units and sub-portfolios: the Euler principle, in A.Resti, ed., ‘Pillar II in the New Basel Accord: The Challenge of Economic Capital’, Risk Books London, pp. 423–453.
  * [61] The European Parliament and the Council of the European Union2002aSolvencyIb The European Parliament and the Council of the European Union 2002a, ‘Directive 2002/13/EC of the European Parliament and of the Council of 5 March 2002 amending Council Directive 73/239/EEC as regards the solvency margin requirements for non-life insurance undertakings’.
  * [62] The European Parliament and the Council of the European Union2002bSolvencyIa The European Parliament and the Council of the European Union 2002b, ‘Directive 2002/83/EC of the European Parliament and of the Council of 5 November 2002 concerning life assurance’.
  * [63] Wang Zitikis2020wang2020axiomatic Wang, Ruodu Ričardas Zitikis 2020, ‘An axiomatic foundation for the expected shortfall’, Management Science .
  * [64] Weber2018weber_solvency2017 Weber, Stefan 2018, ‘Solvency II, or How to Sweep the Downside Risk Under the Carpet’, Insurance: Mathematics and Economics 82, 191–200.
  * [65] Zhu Fukushima2009ZhuFu09 Zhu, Shushang Masao Fukushima 2009, ‘Worst-case conditional value-at-risk with application to robust portfolio management’, Operations Research 57(5), 1155–1168.
  * [66]


A Graphical Algorithm]A Graphical Algorithm for Formulae with Small Clause Density

Tuomas Laakkonen

Some street
United Kingdom

Konstantinos Meichanetzidis

Some street
United Kingdom

John van de Wetering

University of Amsterdam
Some street
The Netherlands

We study the counting version of the Boolean satisfiability problem using the ZH-calculus, a graphical language originally introduced to reason about quantum circuits. Using this we find a natural extension of which we call $\sSAT_\pm$, where variables are additionally labelled by phases, which is GapP-complete.
Using graphical reasoning, we find a reduction from to $\stwoSAT_\pm$ in the ZH-calculus.
We observe that the DPLL algorithm for can be adapted to $\stwoSAT_\pm$ directly and hence that Wahlström's $O^*(1.2377^n)$ upper bound applies to $\stwoSAT_\pm$ as well. Combining this with our reduction from to $\stwoSAT_\pm$ gives us novel upper bounds in terms of clauses and variables that are better than $O^*(2^n)$ for small clause densities of $\frac{m}{n} < 2.25$. This is to our knowledge the first non-trivial upper bound for that is independent of clause size. Our algorithm improves on Dubois' upper bound for $\skSAT$ whenever $\frac{m}{n} < 1.85$ and $k \geq 4$, and the Williams' average-case analysis whenever $\frac{m}{n} < 1.21$ and $k \geq 6$. We also obtain an unconditional upper bound of $O^*(1.88^m)$ for $\#\textbf{4SAT}$ in terms of clauses only, and find an improved bound on $\#\textbf{3SAT}$ for $1.2577 < \frac{m}{n} \leq \frac{7}{3}$.
Our results demonstrate that graphical reasoning can lead to new algorithmic insights, even outside the domain of quantum computing that the calculus was intended for.

§ INTRODUCTION

A graphical calculus is a language consisting of diagrams that can be transformed according to specific graphical rewrite rules. Usually these diagrams correspond to some underlying mathematical object that would be hard to reason about directly—like a matrix, tensor, relation or some combinatorial object—and the rewrite rules preserve the semantics of this interpretation.
There are for instance graphical calculi for linear algebra <cit.>, for studying concurrency <cit.>, and for finite-state automata <cit.>.

Most relevant for this paper are the graphical calculi developed for studying quantum computing. The ZX-calculus <cit.> can represent arbitrary linear maps between any number of qubits, and has different versions of rewrite rules that are complete (meaning the rules can prove any true equality) for various relevant fragments of quantum computing <cit.>.
It has seen use in a variety of areas like optimising quantum computations <cit.>, more effectively classically simulating quantum computations <cit.>, and several others like <cit.>; see <cit.> for a review.

There are a number of variations on the ZX-calculus that include different or additional generators <cit.>. The one we will use is the ZH-calculus <cit.>.
The ZH-calculus has turned out to be useful in a variety of areas <cit.>, but in particular it has been shown to naturally encode Boolean satisfiability and counting problems <cit.>. We will build on this representation to show that this perspective leads to better algorithms for formulae that have a low number of clauses.

The Boolean satisfiability problem () is to determine whether a given Boolean formula has a satisfying assignment of variables. As one of the canonical examples of an -complete problem, has received an extraordinary amount of attention, with many non-trivial algorithms and heuristics being known.
There are several approaches to worst-case upper bounds for solving instances, which can be phrased in terms of some relevant parameters for a Boolean formula $f:\B^n\to \B$ in conjunctive normal form: its number of variables $n$, the maximum clause size $k$, the number of clauses $m$, the clause density $\delta:=\frac{m}{n}$, and the maximal number of clauses a variable participates in.
For instance, for fixed $k$, there are bounds $O^*(c_k^n)$ where $c_k<2$ <cit.>, although do note that $c_k\to 2$ for large $k$ as would be expected from the Strong Exponential Time Hypothesis (SETH).
A classic result of Monien and Speckenmeyer from 1980 <cit.> states that can be solved in $O^*(2^{\frac{m}{3}})$ time (independent of $k$), which was improved to $O^*(2^{0.3090m})$ by Hirsch <cit.> and then to $O^*(2^{0.3033m})$ by Yamamoto <cit.>. This hence implies a better than $O^*(2^n)$ runtime for clause densities $\delta < 3.297$, regardless of $k$.
While it has been shown that for large $k$ and large $\delta$ any upper bounds for must converge to the same limit <cit.>, which is suspected to be $O^*(2^n)$, these results show that for small $k$ and arbitrary $\delta$ or vice-versa, better bounds are possible.

In this paper we will study the problem , which doesn't ask whether a Boolean formula has a solution, but rather how many solutions it has. This is hence not a decision problem, but a counting problem. It is complete for the complexity class , which is the `counting version' of . is believed to be a significantly harder problem than . For instance, a consequence of Toda's theorem <cit.> is that the entire polynomial hierarchy is contained in $\textbf{P}^{\sSAT}$.
As it is a complete problem for , it has applications in a variety of areas. For instance, tensor-network contraction (when suitably formalised) is in  <cit.>. also has applications in the field of artificial intelligence, where it is usually referred to as model counting <cit.>.
Note that while for the problem only becomes hard for $k\geq 3$, for , the problem is already hard for $k=2$, and in fact $\stwoSAT$ is -complete <cit.>.

We can again phrase the known upper bounds to in terms of $n$, $k$, $m$ and $\delta$, although for much less is known. Similarly to , good bounds are known for small $k$ — $O^*(1.2377^n)$ for $k = 2$ <cit.>, and $O^*(1.6423^n)$ for $k = 3$ <cit.>. There are also bounds known for arbitrary (but fixed) $k$ in the worst-case setting <cit.> and the average-case setting <cit.>. These bounds converge to $O^*(2^n)$ in the large $k$ limit, as is to be expected (assuming SETH). Unlike , bounds in terms of $m$ are not known for independent of $k$, but only for $k = 2$, $O^*(1.1710^{m})$ <cit.>, and $k = 3$, $O^*(1.4142^{m})$ <cit.>.

In this paper we establish, to the best of our knowledge, the first algorithm for $\sSAT$ that is better than brute-force for low clause density, independent of the clause size $k$. Specifically, we prove the following theorem:

Given a CNF formula $f:\B^n\to \B$, we can count the number of satisfying assignments
$$\#\{\vec x\in \B^n\,|\, f(\vec x) = 1\}$$
in time $O^*(1.2377^{n + m_{\geq 3}})$, where $m_{\geq 3}$ is the number of clauses of width at least three.
In particular, for clause density $\delta < 2.2503$, this gives a better than $O^*(2^n)$ bound, independent of maximal clause size $k$.

The worst-case bound for our algorithm we find improves the best-known bound for a variety of different parameters. We summarise this in Tables <ref> and <ref>. Note that these tables also contain our results based on a more fine-grained analysis of #3SAT and #4SAT that is presented in Sections <ref> and <ref>.

Problem     Previous Best     New Bound     Relevant Densities     Underlying Algorithm
$\skSAT$ for $k > 4$     $O^*(c_k^n)$, $c_k \to 2$ <cit.>     $O^*(1.2377^{n + m})$     $\delta < 2.2503$ (as $k \to \infty$)     <cit.>

$\#\textbf{3SAT}$     $O^*(1.6423^n)$ <cit.>     $O^*(1.6350^n)$     $1.2577 < \delta \leq \frac{7}{3}$     <cit.> <cit.>

$\#\textbf{4SAT}$     $O^*(1.9274^n)$ <cit.>     $O^*(1.8803^m)$     $\delta < 1.0370$     <cit.>

The different bounds obtained in this paper, along with the corresponding best previous bounds, and the underlying algorithm on which they are based. The given relevant densities are the intervals where our bounds are valid and improve on the previous bound.

Improvement on     $k$     2     3     4     5     6     7     8     9     10

Average-Case     $\delta$     –     –     –     –     –     $<0.968$     $<1.106$     $<1.207$     $<1.288$

Best prev. algorithm        <cit.>     <cit.>     <cit.>     <cit.>     <cit.>     <cit.>     <cit.>     <cit.>     <cit.>

Worst-Case     $\delta$     –     $<2.333^*$     $<2.077$     $<2.170$     $<2.212$     $<2.231$     $<2.241$     $<2.246$     $<2.248$

Best prev. algorithm        <cit.>     <cit.> <cit.>     <cit.>     <cit.>     <cit.>     <cit.>     <cit.>     <cit.>     <cit.>

The maximum densities $\delta$ at which our upper bound improves on other bounds, as dependent on $k$. We include average and worst-case bounds, both of which converge to $\delta = 2.2503$ as $k$ increases. Entries marked with `–' are where our bound is always worse. The entry marked `$*$' uses the alternate bound presented in Section <ref> and only improves on the previous best when also $\delta > 1.2577$.

While the bound of Theorem <ref> is only effective at low densities, this is sufficient for many real-world use cases – in particular, for the unweighted instances from the Model Counting Competition 2020 <cit.>, we found that we improve on the previous best worst-case bound for 88% of instances, and the average-case bound for 45% of instances as shown in Figure <ref>.

The measured values of $k$ and $\delta$ for instances used in the Model Counting Competition 2020 <cit.>. The shaded regions represent the area where our bound is better than previous bounds in the worst and average-case regimes, assuming that $m = m_{\geq 3}$. The value of $k$ is taken as the 90th percentile of clause widths to avoid few large clauses biasing the result in our favour. Assuming the constant factors in all algorithms are equal, our bound is better for 88% of instances in the worst-case and 45% of instances in the average-case. Note this may not align with the shaded regions since $m \neq m_{\geq 3}$ in practice.

Assuming SETH, our results indicate that the `hardest' density of must be some $\delta > 2.2503$. As far as we aware this is the first known bound on where the hardest clause density of lies.

Our results are based on two observations.
The first observation is that the standard CDP algorithm <cit.> for solving can actually solve a more general problem that we dub $\sSAT_{\pm}$. In this problem, variables $x_i$ are labelled by a $\phi_{i} = \pm 1$ phase that determines whether a solution to $f$ should be added or subtracted to the total, as determined by $\prod_{\vec x}\phi_{i}^{x_i}$.
The second observation is that we can translate an arbitrary instance into a $\stwoSAT_{\pm}$ instance. This removes the dependence on maximal clause size $k$ from our problem, and means we can use the known upper bounds to that apply directly to the problem $\stwoSAT_{\pm}$ as well.

We found this last observation by writing a instance as a ZH-diagram as
described by de Beaudrap et al. <cit.>.
We extend their methods by relaxing the conditions on the types of diagrams we consider, which shows that ZH-diagrams also naturally represent $\sSAT_\pm$ instances. The translation from a instance into a $\stwoSAT_\pm$ instance then follows from a known rewrite rule of the related ZX$\Delta$-calculus <cit.>.
We also find that $\sSAT_\pm$ is in fact complete for the complexity class GapP <cit.>, which is closed under negation.

In Section <ref> we recall the definition of the ZH-calculus, how to encode instances as ZH-diagrams, and how the CDP algorithm for solving works.
Then in Section <ref> we present our main results: we show how to interpret CDP graphically inside the ZH-calculus, we find a graphical reduction from to and one from to $\stwoSAT_{\pm}$ that is more efficient. We end with a complexity analysis of combining this reduction with the CDP algorithm, modified to work for $\stwoSAT_{\pm}$.
In Section <ref> we study some variations on our algorithm: Section <ref> presents a new bound of $O^*(1.8803^{m})$ for #4SAT that is only in terms of clauses, which is better than our other bound when $\delta<0.51$; Section <ref> gives a modified algorithm for #3SAT that is better for certain densities; and Section <ref> presents the problem of where variables are labelled by arbitrary complex numbers, which we conjecture might be helpful for future improvements.
We end with some concluding remarks in Section <ref>.

§ PRELIMINARIES

§.§ The ZH Calculus

The ZH-calculus is a graphical calculus originally introduced for reasoning about quantum computing <cit.>.
We will however motivate it by its close relation to Boolean logic.
Namely, we will show how the generators of the calculus naturally arise from the lifting of Boolean functions to linear maps. This lifting is used widely with tensor network techniques to solve the $\sSAT$ problem <cit.> and related problems such as weighted model counting <cit.>. Let us consider the following mapping $\mathbb{B} \to \mathbb{C}^2$:

\begin{equation}
\mathrm{False} \mapsto \begin{pmatrix} 1 \\ 0 \end{pmatrix} \qquad\qquad\mathrm{True} \mapsto \begin{pmatrix} 0 \\ 1 \end{pmatrix}
\end{equation}

A pair of Booleans $\mathbb{B}^2$ is then mapped via the tensor product to $\mathbb{C}^2\otimes \mathbb{C}^2$. Operations on Booleans then correspond to linear maps on these basis states. To express Boolean functions that are encoded in conjunctive normal form, we will need the encodings of the AND and NOT gates, as well as a way of copying an input value. These can be encoded in the following maps:

\begin{equation}
\begin{aligned}
&\mathrm{AND} &\mapsto \begin{pmatrix} 1 & 1 & 1 & 0 \\ 0 & 0 & 0 & 1 \end{pmatrix} & \quad&\mathrm{NOT} \mapsto \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix} \\ &\mathrm{COPY} &\mapsto \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 0 & 0 & 1 \end{pmatrix}
\end{aligned}
\end{equation}

These operators, together with the identity map $\mathrm{I} : x \mapsto x$ and swap map $\mathrm{SWAP} : (a, b) \mapsto (b, a)$, are sufficient to express any CNF formula. These are represented by:

\begin{equation}
\mathrm{I} \mapsto \begin{pmatrix} 1 & \cdots & 0 \\ \vdots & \ddots & \vdots \\ 0 & \cdots & 1 \end{pmatrix} \qquad \mathrm{SWAP} \mapsto \begin{pmatrix} 1 & 0 & 0 & 0\\ 0 & 0 & 1 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \end{pmatrix}
\end{equation}

By composing and tensoring these matrices together, we can represent any CNF formula.
For example, the function $f(x_1, x_2) = (x_1 \land \lnot x_2) \lor \lnot x_1$ can be expressed as

\begin{equation}
\mathrm{NOT} \circ \mathrm{AND} \circ (\mathrm{I} \otimes (\mathrm{NOT} \circ \mathrm{AND})) \circ (\mathrm{COPY} \otimes \mathrm{NOT})
\end{equation}

since $x \lor y = \lnot (\lnot x \land \lnot y)$, so we have $\mathrm{OR} = \mathrm{NOT} \circ \mathrm{AND} \circ (\mathrm{NOT} \otimes \mathrm{NOT})$. We will represent these operations graphically as a tensor network. In the tensor network, every wire will represent a Boolean value, and we use shapes with input and output wires to express the matrices in the network:

\begin{equation}
\tikzfig{zhcalculus_defs}
\end{equation}

Connecting all output wires of one matrix to input wires of another encodes a matrix multiplication, and placing two matrices side by side encodes their tensor product. Inputs and outputs left unconnected represent inputs and outputs of the linear map. We can then represent the identity and swap maps very naturally as:

\begin{equation}
\tikzfig{zhcalculus_identswap}
\end{equation}

We can further equip our diagrams with two more generators, called the cup and the cap:

\begin{equation}
\tikzfig{tensornetworkcup} \qquad\qquad \tikzfig{tensornetworkcap}
\end{equation}

These obey several symmetries, called the yanking equations:

\begin{equation}
\tikzfig{tensornetworkyank}
\end{equation}

Because of these symmetries, we can see that the value corresponding to a tensor network doesn't depend on the exact combination of swaps, identities, caps and cups, so long as the same outputs of each box are connected to the same inputs of other boxes. We call this property (weak) only connectivity matters (OCM).

The copy and NOT operations also obey some additional symmetries (called flexsymmetry <cit.>),

\begin{equation}
\tikzfig{zhcalculus_copynotsymm}
\end{equation}

which imply that there is no reason to distinguish between inputs and outputs for these operations. Furthermore, we can generalise the copy operation to have multiple inputs and outputs as follows:

\begin{equation}
\tikzfig{zhcalculusgen_zspider}\ \  =\ \ \begin{pmatrix}
1 & 0 & \cdots & 0 & 0\\
0 & 0 &  & 0 & 0\\
\vdots & & \ddots & &\vdots \\
0 & 0 & & 0 & 0 \\
0 & 0 & \cdots & 0 & 1
\end{pmatrix}
\end{equation}

This maintains its flexsymmetry:

\begin{equation}
\tikzfig{zhcalculus_zflex}
\end{equation}

If all the generators in the diagram are flexsymmetric, then we can treat the diagram as an undirected graph. However, the AND operation is not flexsymmetric:

\begin{equation}
\tikzfig{zhcalculus_andnflex}
\end{equation}

In order to symmetrise this operation, we introduce a new generator, the H-box. This generator is labelled with a complex value $a \in \mathbb{C}$, is flexsymmetric, and is encoded as follows:

\begin{equation}
\tikzfig{zhcalculusgen_hbox} = ~\begin{pmatrix}
1 & 1 & \cdots & 1 & 1\\
1 & 1 &  & 1 & 1\\
\vdots & & \ddots & &\vdots \\
1 & 1 & & 1 & 1 \\
1 & 1 & \cdots & 1 & a
\end{pmatrix}
\end{equation}

\begin{equation}
\tikzfig{zhcalculus_hflex}
\end{equation}

If no value of $a$ is specified, we will assume that $a = -1$. Note that an H-box with no inputs or outputs represents just the scalar $a$, and thus these multiply as you would expect:

\begin{equation}
\tikzfig{scalar_multiply}
\end{equation}

Then we can decompose the AND gate in terms of H-boxes:

\begin{equation}
\tikzfig{zhcalculus_hboxand}
\end{equation}

This yields the following representation of the example function $f$ from before:

\begin{equation}
\tikzfig{zhcalculus_example}
\end{equation}

All tensor networks composed of H-boxes and Z-spiders are called ZH-diagrams. Since ZH-diagrams consist only of flexsymmetric generators connected by wires that obey the yanking equations, we can treat the whole diagram as an undirected graph, as the order, direction, and any arbitrary bends in the wires do not affect the underlying tensor. We call this property strong OCM. For this reason we will from now on sometimes write diagrams from bottom-to-top as well, if the notion of input and output is not important.

This can all be made formal by viewing ZH-diagrams as morphisms in a compact closed PROP, i.e. a monoidal category where the objects are natural numbers (corresponding to the number of wires), and the tensor is addition. Their interpretation into linear maps is then given by a strong monoidal functor into a suitable category of linear maps. This level of formality won't however be needed for our purposes.

It will be useful to introduce some additional derived generators.
We represent X-spiders by grey dots and define them by:

\begin{equation}
\tikzfig{zhcalculus_xspider}
\end{equation}

Note then that single-legged X-spiders correspond to the true and false states:

\begin{equation}
\tikzfig{zhcalculus_xspider_truth}
\end{equation}

In case the legs point backwards,
then they represent assertions that a logic operation has the given outcome. We also define a generalisation of the Z-spider that is labelled with a phase $\alpha \in \mathbb{C}$ (assumed to be $\alpha = 0$ if not specified):

\begin{equation}
\tikzfig{zhcalculusgen_zspiderphase} ~~=~~ \tikzfig{zhcalculusgen_zspiderphase2}
\end{equation}

While ZH-diagrams are just a graphical notation for linear maps, they come equipped with a set of rewrites rules known as the ZH-calculus, originally introduced by Backens and Kissinger <cit.>. The subset of rules we use in this paper is as follows:

\begin{equation}
\tikzfig{zhcalculusrules}
\end{equation}

These rules can be applied locally to a part of a larger diagram (this can be formalised in the framework of double-pushout rewriting <cit.>), and together form a quotient relation on the category of ZH-diagrams that respects the interpretation functor into the category of linear maps (i.e. the rules are sound with respect to these semantics).
In addition these rules are complete: if the maps represented by two ZH-diagrams are equal, then the two diagrams can be transformed into each other using just applications of these rules.

Note that the rules SF$_Z$ and I$_Z$ together say that Z-spiders form a Frobenius algebra, while the rules BA$_Z$ and BA$_H$ can be framed as stating it is an interacting bialgebra <cit.> with the Frobenius X-spider and the (almost) Frobenius H-box.

Finally, because ZH-diagrams describe matrices, addition for diagrams with the same number of inputs and outputs can be defined as the addition of the underlying matrices. For example, labelled Z-spiders can be written as the following sum:

\begin{equation}
\label{zspidersum}
\tikzfig{zhcalculusgen_zspidersum}
\end{equation}

These two terms correspond to the two non-zero entries in the top-left and bottom-right corner of the matrix.

§.§ Embedding $\sSAT$ in ZH-Diagrams

Following the technique of de Beaudrap, Kissinger, and Meichanetzidis <cit.>, since $a \lor b = \lnot (\lnot a \land \lnot b)$, we can represent a general CNF formula $f(\vec{x}) = \bigwedge_{i = 0}^{m} \bigvee_{j = 0}^{k_i} l_{ij}$ as a ZH-diagram using the embedding described above as

\begin{equation}
\tikzfig{satembed_cnfdiagram}
\end{equation}

where the Z-spiders on the left copy the input variables as many times as needed, then $G$ is a permutation of wires and NOT gates connecting the appropriate inputs (perhaps negated) to each clause on the right. Every clause is then combined to form the final output. In order to represent the number of satisfying solutions to the formula $f$, note that using an X-spider to assert that the final output is true converts the diagram into a number zero or one depending on if a given set of inputs is satsifying, since:

\begin{equation}
\tikzfig{satembed_postsel_reason}
\end{equation}

Therefore, we just need a way to sum over all inputs. In particular, we have the following equality

\begin{equation}
\tikzfig{diagramsum_zspider}
\end{equation}

and since tensor addition distributes over the tensor product (as addition distributes over scalar multiplication), we can see that

\begin{equation}
\tikzfig{diagramsum_zspiders}
\end{equation}

Thus since the tensor product of Z-spiders is a sum over all possible combinations of X-spiders, and thus all possible combinations of truth values, we have the following:

\begin{equation}
\tikzfig{satembed_cnfdiagram_postsel}
\end{equation}

This diagram can be simplified further into the form obtained in <cit.>:

\begin{equation}
\scalebox{0.8}{\tikzfig{satembed_cnfdiagram_final}}
\end{equation}

To give an example, suppose $f(\vec{x}) = (x_1 \lor x_3) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2 \lor x_3)$, then the corresponding $\sSAT$ ZH-diagram is given by the following, noting that we can cancel adjacent NOT gates:

\begin{equation}
\tikzfig{satembed_cnfdiagram_example}
\end{equation}

And we can see that any diagram containing Z-spiders, NOT gates, and zero-labelled H-boxes such that Z-spiders and H-boxes are never connected to other generators of the same type, either directly or through NOT gates, represents a $\sSAT$ instance.

Note that a complete graphical calculus for was introduced recently in <cit.>. However, the semantics of their diagrams directly correspond to a matrix of True or False values, and hence cannot represent instances directly. In this sense it is similar to the modified ZH-diagrams of <cit.> where they set $2=1$ and consider diagrams over the Boolean semi-ring.

§.§ The CDP algorithm for #SAT

The Counting David-Putnam (CDP) algorithm is an algorithm for solving $\sSAT$ that was first introduced in 1999 <cit.>, as an extension of the DPLL algorithm <cit.> for $\SAT$ solving. It is essentially an optimised depth-first search over all possible assignments of variables in a Boolean formula. The algorithm is based on the following two rules:

Unit Propagation: The following rewrite holds for any clauses $A_i$ and $B_i$ not containing some literal $x$:

\begin{equation}
\begin{aligned}
x &\land (A_1 \lor x) \land \cdots \land (A_n \lor x) \\ &\land (B_1 \lor \lnot x) \land \cdots \land (B_m \lor \lnot x) \\ & = B_1 \land \cdots \land B_n
\end{aligned}
\end{equation}

This can be applied to a formula when it contains a clause of only one literal $x$, and it removes all clauses which will become true because $x$ must be true and removes $x$ from all clauses in which it is required to be false. Note that often, the application of this rule will create more clauses of size one, causing a chain of cancellations.

Variable Branching: For any variable $x$ appearing in a formula $f$, the number of satisfying assignments of $f$ is the sum of the numbers of satisfying assignments for

\begin{equation}
f_1 = f \land x \qquad \text{and} \qquad f_2 = f \land \lnot x
\end{equation}

since in each such assignment, either $x$ or $\lnot x$.

The CDP algorithm, given in Algorithm <ref>, applies these two rules recursively until either a contradiction occurs and so the formula is unsatisfiable, or the formula has no clauses remaining, in which case the number of satisfying assignments is $2^n$. Clearly, at each recursive step, the formulas to be considered have fewer variables than at the previous steps, so this procedure terminates.

This works better in practice than naively checking every assignment because the chains of cancellations described above can eliminate many variables, thus removing whole branches from the computation tree. Additionally, the substitution of the assignment into the formula is done incrementally via unit propagation, rather than repeated for every assignment.

The CDP <cit.> algorithm for solving $\sSAT$.
A CNF formula $f$ with $n$ variables and $m$ clauses.
The value of $\#\{ \vec{x} \in \{0, 1\}^n \mid f(\vec{x}) = 1 \}$.
$f$ contains the clauses $x$ and $\lnot x$ for some variable $x$

$f$ has no clauses remaining

Apply unit propagation to $f$ until it is no longer possible.
Pick a variable $x$ that occurs in $f$ and generate $f_1 = f \land x$ and $f_2 = f \land \lnot x$.
$\mathrm{CDP}(f_1) + \mathrm{CDP}(f_2)$

§ RESULTS

We will use the following derived rewrite rule repeatedly in the remainder of the paper:

\begin{equation}
\label{satembed_zerostate}
\tikzfig{satembed_zerostate}
\end{equation}

As well as a further rule describing the interaction between states and Z-spiders:

\begin{equation}
\label{satembed_copy}
\tikzfig{satembed_copy}
\end{equation}

§.§ Interpreting CDP diagrammatically

To interpret CDP diagrammatically we will first see how the two rules apply to the ZH-diagrams for $\sSAT$ instances detailed in Section <ref>:

The following diagrammatic equivalent to the unit propagation rule holds (without loss of generality, we assume the literal to be propagated is not negated):

\begin{equation}
\tikzfig{dpll_unitprop_overview}
\end{equation}

It can be read as follows - on the left-hand side, the zero H-box with one leg is the clause with a single non-negated literal $x$, the H-boxes on the left represent the clauses $B_i \lor \lnot x$ while the H-boxes on the right represent the clauses $A_i \lor x$. On the right-hand side, we see that the clauses $B_i$ remain, while the clauses $A_i \lor x$ have been removed entirely. Because the variable $x$ is now no longer mentioned, the Z-spider representing it is also removed.

First, note that

\begin{equation}
\label{dpll_statepush}
\tikzfig{dpll_unitprop_proof2}
\end{equation}

and so we have that

\begin{equation}
\tikzfig{dpll_unitprop_proof}
\end{equation}

which completes the proof.

The following diagrammatic equivalent to the variable branching rule holds:

\begin{equation*}
\tikzfig{dpll_branch_statement}
\end{equation*}

On the left-hand side, we have a variable connected to arbitrary clauses, whereas on the right-hand side we have two terms, each with a clause of one literal introduced onto the variable.

This follows from writing the Z-spider as a sum

\begin{equation}
\label{dpll_ksat_statepush}
\tikzfig{dpll_branch_proof1}
\end{equation}

and applying the $SF_Z$ rule to the central spider:

\begin{equation}
\tikzfig{dpll_branch_proof2}
\end{equation}

Modifications of the CDP algorithm are used extensively in practice, with some of the best solvers like sharpSAT <cit.> and Cachet <cit.> making use of this technique. All the best-known theoretical upper bounds on runtime are based on careful analysis of this algorithm. Note that we left the choice of variable to branch on unspecified - choosing this wisely is crucial to obtaining good runtimes, as we will see in the next section.

§.§ Reduction from $\sSAT$ to $\stwoSAT$

Valiant <cit.> showed that $\stwoSAT$ is -complete, which implies that there is a polynomial-time Turing reduction from $\sSAT$ to $\stwoSAT$. Since good upper bounds are known for $\stwoSAT$, reducing $\sSAT$ to $\stwoSAT$ is one strategy to obtain better than brute-force bounds that are independent of $k$. However, the polynomial-time reduction guaranteed by -completeness maps instances with $n$ variables and $m$ clauses to instances with $O(nm)$ variables, which destroys any advantage we could have gained from faster $\stwoSAT$ algorithms. Instead we will present a much simpler exponential-time reduction that follows naturally from our diagrammatic representation and produces instances with only $n + \frac{m}{2}$ variables.

The following diagrammatic equivalence holds:

\begin{equation}
\tikzfig{dpll_neg_kclause}
\end{equation}

This directly generalises the $\mathrm{BW}$ axiom of the $\Delta\mathrm{ZX}$-calculus <cit.>.

We can see the following

\begin{equation}
\tikzfig{dpll_neg_kclause_proof}
\end{equation}

which completes the proof.

This lemma allows us to remove clauses with degree greater than two, at the cost of introducing extra Z-spiders. If we applied this to every clause in a $\sSAT$ diagram with $n$ variables and $m$ clauses, we would have a diagram with $n + m$ spiders and furthermore, with the exception of $\pi$-phases on $m$ of these spiders, this diagram would represent a $\stwoSAT$ instance. Therefore, to reduce $\sSAT$ to $\stwoSAT$, we could write such a diagram as a sum of diagrams that remove these $\pi$-phases, and evaluate each of the diagrams of the sum with the $\stwoSAT$ oracle. In particular, we can apply the following decomposition recursively

\begin{equation}
\tikzfig{dpll_neg_pisplit}
\end{equation}

and since each decomposition removes two $\pi$-phases, we will end up with $2^{\frac{m}{2}}$ diagrams. We can also see that each of these diagrams will have only $n + \frac{m}{2}$ Z-spiders (and thus, $n + \frac{m}{2}$ variables), since:

\begin{equation}
\tikzfig{dpll_neg_pisplit2}
\end{equation}

Therefore, if we were to use Wahlström's $O^*(1.2377^{\mathrm{variables}})$ upper bound for $\stwoSAT$ to evaluate each of these diagrams, we would end up with a total runtime of $O^*(2^{\frac{m}{2}} 1.2377^{n + \frac{m}{2}}) = O^*(2^{0.3068n + 0.6538m})$.

§.§ Reduction from $\sSAT$ to $\stwoSAT_\pm$

However, we can do better and avoid the overhead of writing such diagrams as sums by relaxing our definition of $\sSAT$ to permit $\pi$-phases appearing on the Z-spiders (variables). Note that we have the following

\begin{equation}
\tikzfig{dpll_pm_signflip}
\end{equation}

which implies that these diagrams are the same as $\sSAT$ instances, but the sign is flipped whenever a variable corresponding to a Z-spider with a $\pi$-phase is assigned to be true. Therefore, the overall sign of the diagram for a particular assignment of variables is given by the parity of the assignment of such variables. We can extend the $\sSAT$ problem as follows to handle this natively.

The problem $\sSAT_\pm$ is defined as follows. Given a CNF formula $f(x_1, \dots, x_n)$ with $n$ variables and $m$ clauses, and a set $N \subseteq \{1, \dots, n\}$, compute the quantity

\begin{equation}
\sSAT_\pm(f, N) = \sum_{\substack{\vec{x} \in \mathbb{B}^n \\ \text{even }N\text{-parity}}}f(\vec{x}) ~~- \sum_{\substack{\vec{x} \in \mathbb{B}^n \\ \text{odd }N\text{-parity}}}f(\vec{x})
\end{equation}

where a vector $\vec{x} \in \mathbb{B}^n$ has even or odd $N$-parity if $\bigoplus_{i \in N} x_i = 0$ or $1$, respectively.

$\sSAT_\pm$ is GapP-complete

See Appendix <ref>.

Since $\sSAT_\pm$ is in GapP, which is strictly harder than #P (for instance, GapP is the closure of #P under subtraction <cit.>), it may seem that an upper bound for this problem is guaranteed to be worse. However, this is not the case, as the following diagrammatic arguments show that the DPLL algorithm can be easily adapted to handle the sign change as Algorithm <ref>.

The following diagrammatic equivalent to the variable branching rule holds for variables with $\pi$-phases:

\begin{equation}
\tikzfig{dpll_neg_branch}
\end{equation}

This follows from the sum

\begin{equation}
\tikzfig{dpll_neg_branch_proof}
\end{equation}

together with the proof of Lemma <ref>.

The following diagrammatic equivalent to the unit propagation rule holds for variables with $\pi$-phases:

\begin{equation}
\tikzfig{dpll_neg_unitprop}
\end{equation}

This follows from the identities

\begin{equation}
\tikzfig{dpll_neg_unitprop_proof}
\end{equation}

together with the proof of Lemma <ref>.

The $\mathrm{CDP}_\pm$ algorithm solving $\sSAT_\pm$.
A CNF formula $f$ with $n$ variables and $m$ clauses, and a set of variables $N \subseteq \{1, \dots, n\}$.
The value of $\sSAT_\pm(F, N)$.

$f$ contains an empty clause
$f$ has no clauses

Pick $i \in \{1, \dots, n\}$ according to some strategy.
$f_1 \gets \operatorname{Unit-Propagate}(f \land \lnot x_i)$
$f_2 \gets \operatorname{Unit-Propagate}(f \land x_i)$
$i \in N$
$\mathrm{CDP}_\pm(f_1, N) - \mathrm{CDP}_\pm(f_2, N)$

$\mathrm{CDP}_\pm(f_1, N) + \mathrm{CDP}_\pm(f_2, N)$

With a smart choice of the variables to branch on, the worst-case runtime of Algorithm <ref> can be bounded in exactly the same way as the regular $\mathrm{CDP}$. In particular, this means that the $O^*(1.2377^{\mathrm{variables}})$ bound of Wahlström <cit.> can be adapted directly. Therefore, by applying Lemma <ref> to any $\sSAT$ diagram and then applying $\mathrm{CDP}_\pm$ to the resulting diagram directly, we can evaluate $\sSAT$ instances in time $O^*(1.2377^{n + m}) = O^*(2^{0.3068n + 0.3068m})$, which is certainly better than the bound given by decomposing into a sum of diagrams. We will refer to this method, given in Algorithm <ref>, as $\mathrm{CDP}_\pm^{\to 2}$.

The $\mathrm{CDP}^{\to 2}_\pm$ algorithm for $\sSAT_\pm$.
A CNF formula $f$ with $n$ variables and $m$ clauses, and a set of variables $N \subseteq \{1, \dots, n\}$.
The value of $\sSAT_\pm(F, N)$.

Generate $f'$ by applying Lemma <ref> to every clause in $f$ of width at least three.

Given a CNF formula $f:\B^n\to \B$, we can count the number of satisfying assignments $\#\{\vec x\in \B^n\,|\, f(\vec x) = 1\}$ in time $O^*(1.2377^{n + m_{\geq 3}})$, where $m_{\geq 3}$ is the number of clauses of width at least three.

Apply the algorithm $\mathrm{CDP}_\pm^{\to 2}$ to $f$ using Wahlström's <cit.> $O^*(1.2377^{\mathrm{variables}})$ algorithm for $\stwoSAT$. $m_{\geq 3}$ new (negative) variables will be created by applying Lemma <ref>, so the overall runtime is $O^*(1.2377^{n + m_{\geq 3}})$.

It remains to ask, when is $\mathrm{CDP}_\pm^{\to 2}$ actually useful? First, note that if only positive variables are picked for branching, the action of $\mathrm{CDP}_\pm$ on a translated $\sSAT$ diagram is exactly the same as the action of regular $\mathrm{CDP}$ on the original diagram. Therefore, we would only expect gains when decomposing some of the negative variables (i.e clauses), and thus it is natural to suspect that this bound will only be useful for instances with few clauses.

§.§ Complexity analysis

For instances with a fixed maximum density $\delta_{max}$, and assuming the worst-case of $m_{\geq 3} = m$, we have that $m \leq n\delta_{max}$, and so the runtime of $\mathrm{CDP}_\pm^{\to 2}$ is bounded by $O^*(2^{0.3068(1 + \delta_{max})n})$. Firstly, we can see that this is better than the naive $O^*(2^n)$ whenever $\delta_{max} < 2.2503$. Since this is independent of $k$, it means that for any $\delta_{max} < 2.2503$ and sufficiently large $k$, this beats both the worst-case bound of Dubois <cit.> and the average-case bound of Williams <cit.>.

Concretely, $\mathrm{CDP}_\pm^{\to 2}$ is better than the average-case bounds of Williams <cit.> whenever $\delta_{max} < 1.217$ and $k \geq 6$, and better than the worst-case bounds of Dubois <cit.> whenever $k \geq 3$ and $\delta_{max} < 1.858$. The exact bounds for each $k$ are given in Table <ref>. Clearly, $\mathrm{CDP}_\pm^{\to 2}$ offers no improvement on $\stwoSAT$, but it is also not directly applicable to $\#\textbf{3SAT}$ - when $\delta < 1.6$, the $O^*(1.4142^{m})$ bound of Zhou et al <cit.> is sharper, and when $\delta \geq 1.6$ the $O^*(1.6423^n)$ bound of Kutzkov <cit.> is sharper.

For $\SAT$, it has been shown that there is a phase transition in the satisfiability of a random formula as $\delta$ passes some threshold. Instances with densities near this threshold are known to be hard to solve, and it is known that this threshold scales exponentially with $k$ <cit.>. However, no bound is known for the equivalent `hardest' density in $\sSAT$. Assuming SETH, our result indicates that the `hardest' density of $\sSAT$ must be some $\delta > 2.2503$, since otherwise $\sSAT$ (and hence $\SAT$) could be solved in time better than $O^*(2^n)$.

§ VARIATIONS ON THE MAIN RESULT

§.§ Bounding $\#\textbf{4SAT}$ in terms of clauses

Noting that $\mathrm{CDP}_\pm^{\to 2}$ maps a $\sSAT$ instance of $m$ clauses to a $\stwoSAT$ instance of at most $km$ clauses (with negative variables), and applying the upper bound of $O^*(1.1710^{m})$ on $\stwoSAT$ found by Wang and Gu <cit.>, we can bound the runtime of $\mathrm{CDP}_\pm^{\to 2}$ purely in terms of clauses, not mentioning variables, as $O^*(1.1710^{km})$. This does not offer any improvement over known bounds for $k = 2$ or $k = 3$, and for $k > 4$, it is worse than the naive $O^*(2^{m})$ upper bound (which follows from branching on all the negative variables, so that there are no clauses left in the diagram). However, for $k = 4$, this yields a time of $O^*(1.8803^{m})$, which is better than $O^*(1.2377^{n + m})$ whenever $\delta < 0.51$.

§.§ An algorithm for low-density $\#\textbf{3SAT}$ instances

In the previous section, we noted that $\mathrm{CDP}^{\to 2}_\pm$ can't beat existing bounds for $\#\textbf{3SAT}$ on its own. This is because we have to assume that $m = m_{\geq 3}$ in the worst-case. However, we can use a technique introduced by Kutzkov <cit.> to take advantage of the extra structure afforded by $\#\textbf{3SAT}$ and introduce extra branching steps which allow us to assume that $m_{\geq 3} < m$.

Assume we have some $\#\textbf{3SAT}$ instance $f$. Every time we branch on a variable $x$ that occurs in $d$ 3-clauses in $f$, in both branches at least $d$ 3-clauses are eliminated (since each clause will be totally removed in one branch and become a 2-clause in the other). If we know that the density of 3-clauses in $f$ is $\delta_3$, then the average number of 3-clauses a variable is connected to (its average 3-degree) is $3\delta_3$. Therefore, whenever $d - 1 < 3\delta_3 \leq d$, there must exist a variable with 3-degree at least $d$, and so by branching on the variable with the highest 3-degree, we remove at least $d$ 3-clauses.

Following Kutzkov <cit.>, suppose $x$ is the number of variables needed to reduce $\delta_3$ to at most $\frac{d - 1}{3}$ by repeatedly branching on the variable with the highest 3-degree. Then we need

\begin{equation}
\frac{d}{3}n - d x \leq \frac{d - 1}{3}(n - x)
\end{equation}

thus $x \leq \frac{n}{2d + 1}$, so in the limit of large $n$, we have $x = \frac{n}{2d + 1}$ in the worst case, and $n - \frac{n}{2d + 1}$ variables remain unassigned. Therefore, the number of variables we need to branch on to reduce $\delta_3$ to at most $\frac{2}{3}$ is:

\begin{equation}
\label{n23def}
n_{2/3} = n - n \prod_{i = 3}^d\left(1 - \frac{1}{2i + 1}\right)
\end{equation}

Since $m_{\geq 3} = \delta_3n$, after performing this branching on $n_{2/3}$ variables, we will have $2^{n_{2/3}}$ instances, each with $m_{\geq 3} \leq \frac{2}{3}(n - n_{2/3})$, so these can be evaluated with $\mathrm{CDP}_\pm^{\to 2}$. This strategy, formalised as Algorithm <ref>, therefore has an overall time bound of:

\begin{equation}
\begin{aligned}
O^*(2^{n_{2/3}}) &O^*(1.2377^{(n - n_{2/3}) + m_{\geq 3}}) \\
&\leq O^*(2^{n_{2/3}}) O^*(1.2377^{(n - n_{2/3})(1 + \frac{2}{3})}) \\
&= O^*(2^{0.5128n + 0.4872n_{2/3}})
\end{aligned}
\end{equation}

In order to calculate the running-time bound for a given maximum $\delta_3$, we can plug $d = \lceil3\delta_3\rceil$ into Equation (<ref>) to calculate $n_{2/3}$ as a fraction of $n$. For example, if $\delta_3 < \frac{5}{3}$ then $d = 5$ and $n_{2/3} = 0.3074n$, yielding a time of $O^*(2^{(0.5128 + 0.4872\cdot 0.3074)n}) = O^*(1.5829^n)$. Suppose then that $\delta = \delta_3$ (i.e the worst-case), then this bound is better than the bound of Zhou <cit.> whenever $\delta > 1.2577$ (i.e $d \geq 4$ but not $d = 3$, comparing the $O^*(1.5463^n)$ complexity for $d = 4$ to Zhou's $O^*(1.4142^m)$ to find the exact cutoff point) and the $O^*(1.6423^n)$ bound of Kutzkov <cit.> whenever $\delta \leq \frac{7}{3}$ (i.e for $d \leq 7$), yielding complexities of $O^*(1.5463^n)$ ($d = 4$) to $O^*(1.6350^n)$ ($d = 7$) respectively. It is possible this bound could be extended to a yield an improved bound on general $\#\textbf{3SAT}$ using a case analysis similar to Kutzkov's, but this is quite complicated so we postpone exploring this to future work.

The algorithm $\mathrm{CDP}_\pm^{3 \to 2}$ for solving $\#\textbf{3SAT}$.
A CNF formula $f$ with $n$ variables and $m$ clauses, and a set of variables $N \subseteq \{1, \dots, n\}$.
The value of $\sSAT_\pm(F, N)$.
$\delta_3 > \frac{2}{3}$
Pick $x$ in $f$ with maximal 3-degree.
$f_1 \gets \operatorname{Unit-Propagate}(f \land \lnot x_i)$
$f_2 \gets \operatorname{Unit-Propagate}(f \land x_i)$
$\mathrm{CDP}_\pm^{3 \to 2}(f_1) + \mathrm{CDP}_\pm^{3 \to 2}(f_2)$

$\mathrm{CDP}^{\to 2}_\pm(f)$

§.§ Solving #SAT with arbitrary phases

While allowing $\pi$-phases on variables has allowed us to find a simple reduction from $\sSAT$ to $\stwoSAT_\pm$ which can be solved with $\mathrm{CDP}_\pm$, the CDP algorithm easily extends to arbitrary phases in the same way as Algorithm <ref>. Indeed let us define a generalization of the $\sSAT$ problem, $\sSAT_\mathcal{A}$ - this is exactly the weighted model counting problem where the weights are restricted to $\mathcal{A}$.

The problem $\sSAT_\mathcal{A}$ for $\mathcal{A} \subseteq \mathbb{C} \setminus \{0\}$ is defined as follows. Given a CNF formula $f(x_1, \dots)$ with $n$ variables and $m$ clauses and a vector $A \in \mathcal{A}^n$, compute the quantity:

\begin{equation}
\sSAT_\mathcal{A}(f, A) = \sum_{\vec{x} \in \mathbb{B}^n} \left(\prod_{i = 1}^n A_i^{x_i}\right) f(\vec{x})
\end{equation}

It is easy to see then that $\sSAT = \sSAT_{\{1\}}$, and $\sSAT_\pm = \sSAT_{\{1, -1\}}$: let $A_j = -1$ if $j \in N$ and $A_j = 1$ otherwise. In this model, ZH-diagrams for $\sSAT$ instances with phases $\alpha_j$ on the variables correspond to $A_j = e^{i\alpha_j}$, and the variable branching and unit propagation rules generalise from Equation (<ref>). The advantage of working with this problem is that by expanding $\mathcal{A}$, we are afforded additional rewriting rules. Moving from $\{1\}$ to $\{1, -1\}$ allowed us to rewrite arbitrary arity zero-labelled H-boxes into arity two H-boxes. Further expanding this to $\{\frac{k}{2} \mid k \in \mathbb{Z}\}$ allows us the following rule, removing (up to a scalar) any variables that only occur once in a formula:

\begin{equation}
\tikzfig{extension_absorb}
\end{equation}

This is a limited form of pure-literal elimination, a rewrite rule that is usually only valid in $\SAT$ and not $\sSAT$. From this we can obtain a trivial $O^*(1.4565^n)$ upper bound on the complexity of $\stwoSAT$ by applying this simplification to the formula recursively (after unit propagation in the CDP algorithm, i.e between lines 7 and 8 of Algorithm <ref>), and noting that every variable has degree at least two. Therefore, across the two branches at least two neighbouring vertices are eliminated, thus bounding the runtime by the recurrence $T(n) = \max\{2T(n - 2), T(n - 1) + T(n - 3)\}$. This is because in one possibility, the branching variable and one neighbour is eliminated in each branch, whereas the other possibility is that only the branching variable is eliminated in one branch, and in the other branch, both of its neighbours as well. Solving this recurrence relation yields a time bound of $O^*(1.4565^n)$. This is nowhere near as good as the current best bounds, but improves on early bounds such as <cit.>, while being much simpler. Therefore, an interesting avenue for further research would be investigating how this approach of weighting variables could be used to simplify $\sSAT$ instances or find upper bounds on runtime.

The $\mathrm{CDP}_\mathcal{A}$ algorithm for solving $\sSAT_\mathcal{A}$.
A CNF formula $f$ with $n$ variables and $m$ clauses, and $A \in \mathcal{A}^n$.
The value of $\sSAT_\mathcal{A}(F, A)$.

$f$ contains an empty clause
$f$ has no clauses

Pick $i \in \{1, \dots, n\}$ according to some strategy.
$f_1 \gets \operatorname{Unit-Propagate}(f \land \lnot x_i)$
$f_2 \gets \operatorname{Unit-Propagate}(f \land x_i)$
$\mathrm{CDP}_\mathcal{A}(f_1, A) + A_i\mathrm{CDP}_\mathcal{A}(f_2, A)$

§ CONCLUSION

In this paper, we used the ZH-calculus to study the $\sSAT$ problem and produced an upper bound which does not depend on the clause width $k$. We believe bounds of this kind were previously only known for the decision variant $\SAT$ <cit.>. The bound is less than $O^*(2^n)$ whenever the clause density $\delta=\frac{n}{m}$ is smaller than $2.2503$, suggesting that the `hardest' density of $\sSAT$ problems must be some $\delta > 2.2503$, assuming the strong exponential time hypothesis. We achieve this by rephrasing the $\sSAT$ problem in terms of ZH-diagrams, and generalising known rewrite rules to give a reduction from $\sSAT$ to $\stwoSAT_\pm$, a weighted variant of $\sSAT$ that can be solved with Wahlstöm's <cit.> variant of the CDP algorithm <cit.>. We also produce an explicit bound $O^*(1.8803^m)$ in terms of clauses for $\#\textbf{4SAT}$ using a result of Wang and Gu <cit.>, which was previously only known for $\stwoSAT$ and $\#\textbf{3SAT}$ <cit.>, and improve on the upper bound for $\#\textbf{3SAT}$ for $1.2577 < \delta < \frac{7}{3}$. A summary of all the bounds obtained in this paper is presented in Table <ref>. We suggest extending this technique of reducing $\sSAT$ to weighted $\sSAT$ as an avenue of future research, as well as improving the bound on $\#\textbf{3SAT}$ to all densities using the techniques of Kutzkov <cit.>.

Our results show that graphical calculi, even those originally meant for a different domain like quantum computing, can lead to concrete algorithmic improvements in areas where significant research has already been done. An interesting question then is in which other domains we can make improvements by framing the problem using graphical reasoning.

§.§.§ Acknowledgements
The majority of this work was done while TL was a student at the University of Oxford, and the results are also presented in his Master thesis <cit.>.
JvdW acknowledges funding from the European Union's Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 101018390.

§ ADDITIONAL LEMMAS

The following diagrammatic equivalence holds:

\begin{equation}
\tikzfig{satembed_postsel_statement}
\end{equation}

This follows from Lemma 2.28 in <cit.> and Equation (<ref>).

The following diagram equivalence holds:

\begin{equation}
\tikzfig{completeness_zh0tof}
\end{equation}

This is translated from a quantum circuit identity of Ng and Wang <cit.> and is a generalization of the rules $\mathrm{HT}$ and $\mathrm{BW}$ from the $\Delta\mathrm{ZX}_\pi$-calculus <cit.>, a system for describing tensor networks that is closely related to ZH-calculus.

This can be verified by concrete calculation of the matrices.

The following diagram equivalence holds:

\begin{equation}
\tikzfig{completeness_zh0tofident}
\end{equation}

This can be verified by concrete calculation of the matrices.

The following diagram equivalence holds for all $n \geq 0$:

\begin{equation}
\tikzfig{completeness_zh0tofgen}
\end{equation}

We proceed by induction on $n$. For the case of $n = 0$:

\begin{equation}
\tikzfig{completeness_zh0tof0}
\end{equation}

For the case of $n = k + 1$, assuming the result holds for $k$:

\begin{equation}
\tikzfig{completeness_zh0tofkp1}
\end{equation}

§ PROOF THAT $\SSAT_\PM$ IS GAPP-COMPLETE

$\sSAT_\pm$ is GapP-hard.

Suppose there is a problem $M$ in GapP, then the aim is to compute $\mathrm{gap}_M = \#M - \#\overline{M}$ where $\#M$ ($\#\overline{M}$) is the number of accepting (rejecting) paths of a non-deterministic Turing machine $M$. Clearly $\#M$ and $\#\overline{M}$ are both in #P. Because the Cook-Levin reduction from NP to SAT is parsimonius, $\sSAT$ is #P-complete, and there exist CNF formulae $f_M$ and $f_{\overline{M}}$ such that $\sSAT(f_M) = \#M$ and $\sSAT(f_{\overline{M}}) = \#\overline{M}$. Define the following formula:

\begin{align*}
f_{M - \overline{M}} &= \left(\bigwedge_{i = 1}^{m_M} C_M^i \lor z\right) \land \left(\bigwedge_{j = 1}^{n_M} \lnot x_M^j \lor \lnot z\right) \\
&\land \left(\bigwedge_{i = 1}^{m_{\overline{M}}} C_{\overline{M}}^i \lor \lnot z\right) \land \left(\bigwedge_{j = 1}^{n_{\overline{M}}} \lnot x_{\overline{M}}^j \lor z\right) \\
\end{align*}

where $C_M^i$ ($C_{\overline{M}}^i$) and $x_M^j$ ($x_{\overline{M}}^j$) are the clauses and variables of $f_M$ ($f_{\overline{M}}$) respectively, and $z$ is a fresh variable. When $z$ is false, $f_{M - \overline{M}}$ reduces to

\begin{equation*}
f_{M - \overline{M}} \land \lnot z = \left(\bigwedge_{i = 1}^{m_M} C_M^i\right) \land \left(\bigwedge_{j = 1}^{n_{\overline{M}}} \lnot x_{\overline{M}}^j\right) = f_M \land \left(\bigwedge_{j = 1}^{n_{\overline{M}}} \lnot x_{\overline{M}}^j\right)
\end{equation*}

which has exactly $\sSAT(f_M) = \#M$ satisfying solutions, and likewise with $z$ true, we have

\begin{equation*}
f_{M - \overline{M}} \land z = f_{\overline{M}} \land \left(\bigwedge_{j = 1}^{n_{M}} \lnot x_{M}^j\right)
\end{equation*}

which has exactly $\sSAT(f_{\overline{M}}) = \#\overline{M}$ satisfying solutions. Finally let $N = \{z\}$, then an assignment of $f_{M - \overline{M}}$ has odd or even N-parity exactly when $z$ is true or false respectively. Therefore,

\begin{align*}
\sSAT_\pm(f_{M - \overline{M}}, N) &=
\sum_{\Substack{\vec{x} \in \mathbb{B}^n \\ \text{even }N\text{-parity}}}f_{M - \overline{M}}(\vec{x}) - \sum_{\Substack{\vec{x} \in \mathbb{B}^n \\ \text{odd }N\text{-parity}}}f_{M - \overline{M}}(\vec{x}) \\
&= \sSAT(f_{M - \overline{M}} \land \lnot z) - \sSAT(f_{M - \overline{M}} \land z) \\
&= \sSAT(f_M) - \sSAT(f_{\overline{M}}) \\ &= \#M - \#\overline{M} = \mathrm{gap}_M
\end{align*}

so there is a polynomial-time counting reduction from GapP to $\sSAT_\pm$, and it must be GapP-hard.

$\sSAT_\pm$ is in GapP.

Let $f$, $N$ be an instance of $\sSAT_\pm$ with variables $x_i$, then clearly we have that

\begin{align*}
\sSAT_\pm(f, N) &=
\sum_{\Substack{\vec{x} \in \mathbb{B}^n \\ \text{even }N\text{-parity}}}f(\vec{x}) - \sum_{\Substack{\vec{x} \in \mathbb{B}^n \\ \text{odd }N\text{-parity}}}f(\vec{x}) \\
&= \sSAT\left(f \land \lnot \left(\bigoplus_{i \in N} x_i\right)\right) \\
&- \sSAT\left(f \land \left(\bigoplus_{i \in N} x_i\right)\right)
\end{align*}

since $g = 1 \iff g$ and $g = 0 \iff \lnot g$, so $\lnot (\bigoplus_{i \in N} x_i)$ is the same as asserting even N-parity (and likewise odd N-parity). But GapP is the closure of #P under subtraction, so $\sSAT_\pm(f, N)$ is in GapP.

$\sSAT_\pm$ is GapP-complete.

This follows from Lemmas <ref> and <ref>.