LORENTZ GROUPS OF CYCLOTOMIC EXTENSIONS

Relativity and Reciprocity

Vadim Schechtman

March 16, 2021

Abstract

In this (mostly historical) note we show how a unified Kummer-Artin-Schreier
sequence from [W], [SOS] may be recovered from the relativistic velocity
addition law.

Introduction

In the beginning of XX-th century, almost at the same time, two articles have
appeared.

One of them has been published in Annalen der Physik, and became very
celebrated.

The other one appeared in Mathematischen Annalen; it received the prize from
the Königlische Gesellschaft der Wissenschaften zu Göttingen. It was written
by a number theorist Philipp Friedrich Furtwängler111”der zu den bedeutensten
Zahlentheoretiker seiner Zeit gehörte” (see [F], [H]) and contained a proof of
a reciprocity law for $l$-th powers envisioned by Hilbert, generalizing the
classical quadratic reciprocity.

Later on (see [SS]) it was remarked that the Furtwängler’s definitions contain
implicitly certain group scheme which approximates between the multiplicative
group $\mu_{p}$ of $p$-th roots of unity (the kernel of the Kummer map) and
its additive analogue $\alpha_{p}$ (the kernel of the Artin-Schreier map) (see
also [ST], Exercises 1 and 2).

The first mentioned paper is [E], where the author discusses the consequences
of the postulate that the speed of light $c$ remains constant in moving
frames.

It is based on what became known as a relativistic formula for velocity
addition.

In the present note we remark that a unified Kummer-Artin-Schreier group
scheme may be extracted from this addition formula, so as the case $c$ finite
(”Lorentzian”) corresponds to Kummer, whereas $c=\infty$ (”Galilean”)
corresponds to Artin-Schreier.

The reader may notice a connection between the relativistic addition formula
and symmetric functions described in 1.1.

Acknowledgement. This note was inspired by [B]. I am grateful to Y.Bazaliy,
J.Tapia and B.Toen for consultations.

§1. Relativistic velocity addition law

At the moment we will work over a ground commutative ring $k$; in 1.3 below we
will suppose that $k=\mathbb{R}$.

1.1. Velocity addition and symmetric functions. Denote

$None$ $u\oplus
v=u\oplus_{h}v=\frac{u+v}{1+h^{2}uv}=\frac{\sigma_{1}(u,v)}{1+h^{2}\sigma_{2}(u,v)}$

This operation is commutative (obvious) and associative:

$None$ $(u\oplus v)\oplus w=u\oplus(v\oplus
w)=\frac{\sigma_{1}(u,v,w)+h^{2}\sigma_{3}(u,v,w)}{1+h^{4}\sigma_{2}(u,v,w)}$

More generally,

$None$ $u\oplus v\oplus w\oplus
t=\frac{\sigma_{1}(u,v,w,t)+h^{2}\sigma_{3}(u,v,w,t)}{1+h^{2}\sigma_{2}(u,v,w,t)+h^{4}\sigma_{4}(u,v,w,t)},$

etc.

The operation $\oplus_{h}$ has the neutral element $0$, and the inverse
$u\mapsto-u$.

We get a rational group law to be denoted by $\mathbb{G}_{h}$. Thus
$\mathbb{G}_{h}=\operatorname{Spec}k[x]$, and the group law is a rational map

$\oplus_{h}:\
\mathbb{G}_{h}\times\mathbb{G}_{h}--\longrightarrow\mathbb{G}_{h}.$

1.2. Pseudo-orthogonal $2\times 2$-matrices. Let

$A(u)=A_{h}(u)=\left(\begin{matrix}1&-h^{2}u\\\ -u&1\end{matrix}\right).$

Note that $A_{0}(u)$ is just a lower triangular matrix.

Introduce a scalar product $(,)_{h}$ on $V=k^{2}$ by

$None$ $((a,b),(a^{\prime},b^{\prime}))_{h}=h^{2}aa^{\prime}-bb^{\prime}.$

Then the lines (or columns) of $A(u)$ are orthogonal with respect to this
scalar product, we can write

$A(u)\in O(2,(,)_{h}).$

We have

$None$ $A(u)A(v)=(1+h^{2}uv)A(u\oplus_{h}v).$

Taking determinants, we get

$a(u)a(v)=(1+h^{2}uv)a(u\oplus v)$

where

$a(u)=a_{h}(u)=\det A(u)=1-h^{2}u^{2}.$

In other words, the function

$b(u,v)=b_{h}(u,v)=1+h^{2}uv=\sigma_{0}(u,v)+h^{2}\sigma_{2}(u,v)$

is a coboundary:

$None$ $\frac{a(u\oplus v)}{a(u)a(v)}=\frac{1}{b(u,v)^{2}}.$

It follows that if we define

$B_{h}(u)=\frac{A_{h}(u)}{a_{h}(u)^{1/2}}$

then

$B_{h}(u)\in SO(2,(,)_{h})=\mathbb{L}_{h}\subset SL_{2}$

and

$None$ $B_{h}(u)B_{h}(v)=B_{h}(u\oplus_{h}v).$

For $h=0$ the matrices $B_{0}(u)=A_{0}(u)$ generate a group $\mathbb{L}_{0}$
of lower unipotent matrices isomorphic to $\mathbb{G}_{a}$.

Physical interpretation

Consider the relativistic $1|1$-dimensional space-time where the speed of
light is $c=1/h$. Denote

$L_{c}(u):=B_{h}(u).$

If $(x,t)$ are coordinates of an event in a frame at rest then

$\left(\begin{matrix}x^{\prime}\\\
t^{\prime}\end{matrix}\right)=L_{c}(u)\left(\begin{matrix}x\\\
t\end{matrix}\right)$

are its coordinates in the frame moving at the velocity $u$, cf. for example
[B].

1.3. Positivity. Let $k=\mathbb{R}$. Suppose that $h>0$, and let

$h=\frac{1}{c},\ c>0$

(so $c$ is the ”velocity of light”). Then $\oplus_{h}=\oplus_{c}$ gives rise
to a group law on

$I_{c}:=(-c,c),$

i.e. $I_{c}$ becomes a Lie group.

The arrow $\beta_{h}$ (see (2.1.2) below) is an isomorphism of real Lie groups

$I_{c}\overset{\sim}{\longrightarrow}\mathbb{R}_{>0}^{*}$

Thus we have got a family of embeddings of Lie groups

$\iota(c):\mathbb{R}_{>0}^{*}\overset{\sim}{\longrightarrow}I_{c}\hookrightarrow
SL_{2}(\mathbb{R})$

which degenerates in the limit $c\longrightarrow\infty$ to an oryspheric
(lower triangular) subgroup

$\mathbb{R}\overset{\sim}{=}U_{-}\hookrightarrow SL_{2}(\mathbb{R}).$

Replacing $c$ by $ic$ we get a family of compact tori

$S^{1}\overset{\sim}{=}T_{c}\hookrightarrow SL_{2}(\mathbb{R}).$

§2. Relation to $\mathbb{G}_{m}$

2.1.  We claim that for $h\in k^{*}$ the group law $\oplus_{h}$ is
(essentially) isomorphic to $\mathbb{G}_{m}$.

We have

$1+h\frac{u+v}{1+h^{2}uv}=\frac{(1+hu)(1+hv)}{1+h^{2}uv},$

therefore

$None$
$\frac{1+h(u\oplus_{h}v)}{\sqrt{a_{h}(u\oplus_{h}v)}}=\frac{1+hu}{\sqrt{a_{h}(u)}}\cdot\frac{1+hv}{\sqrt{a_{h}(v)}}$

This means that if we define

$\beta_{h}:\ \mathbb{L}_{h}\longrightarrow\mathbb{G}_{m}$

by

$None$
$\beta_{h}(u)=\frac{1+hu}{\sqrt{1-h^{2}u^{2}}}=\sqrt{\frac{1+hu}{1-hu}}$

(on the level of points) then $\beta_{h}$ is a morphism of group laws.

The inverse map

$\beta_{h}^{-1}:\ \mathbb{G}_{m}\longrightarrow\mathbb{L}_{h}$

is

$None$ $v\mapsto\frac{1}{h}\frac{v^{2}-1}{v^{2}+1},$

well defined if $h\in k^{*}$.

In fact we can get the Lorentz group law (1.1.1) by transfering the group law
from $\mathbb{G}_{m}$ using the maps $\phi_{h},\phi_{h}^{-1}$.

Relation to tori

The other way around, we can start from matrices $A_{h}(u)$.

We remark that $A_{h}(u)$ has eigenvalues $\lambda_{\pm}(u)=1\pm hu$ with
eigenvectors

$v_{\pm}=\left(\begin{matrix}\mp h\\\ 1\end{matrix}\right).$

This implies that

$C_{h}^{-1}A_{h}(u)C_{h}=\left(\begin{matrix}1+hu&0\\\
0&1-hu\end{matrix}\right)$

where

$C_{h}=\left(\begin{matrix}-h&h\\\ 1&1\end{matrix}\right).$

Therefore the subgroup $\mathbb{L}_{h}\subset SL_{2}$ is conjugated be means
of $C_{h}$ to the standard maximal torus, and the map $\beta_{h}$ is the
conjugation.

Thus we’ve got a family of tori which degenerates as $h\longrightarrow 0$ to
an oryspheric subgroup $\mathbb{L}_{0}=U_{-}$.

2.2. SOS group. Cf. [W], [SOS], [SS].

Let

$\mathbb{S}_{h}=\mathbb{G}^{\prime}_{h}=\operatorname{Spec}k[x,(1+hx)^{-1}]$

We have a morphism

$\alpha_{h}:\
\mathbb{S}_{h}\longrightarrow\mathbb{G}_{m}=\operatorname{Spec}k[z,z^{-1}],\
z\mapsto 1+hx$

which is an isomorphism of $h\in k^{*}$. On the level of points:

$\alpha_{h}(u)=1+hu,$ $\alpha^{-1}_{h}(v)=\frac{1}{h}(v-1).$

Using it we can transfer the group law on $\mathbb{G}_{m}$ to that on
$\mathbb{S}_{h}$. Since

$(1+hx)(1+hy)=1+h(x+y+hxy),$

the resulting group law on $\mathbb{S}_{h}$ will be (on the level of points)

$None$ $u\oplus^{\prime}_{h}v=u+v+huv$

which makes sense for any $h\in k$. The inverse:

$u\mapsto-\frac{u}{1+hu}.$

The Kummer map

For any $n\in\mathbb{Z}$ we have a group map

$n:\ \mathbb{G}_{m}\longrightarrow\mathbb{G}_{m},\ v\mapsto v^{n}.$

We define a group map

$\psi_{n}:\ \mathbb{S}_{h}\longrightarrow\mathbb{S}_{h^{n}}$

by transferring, so that the square

$\begin{matrix}\mathbb{S}_{h}&\overset{\psi_{n}}{\longrightarrow}&\mathbb{S}_{h^{n}}\\\
\alpha_{h}\downarrow&&\downarrow\alpha_{h^{n}}\\\
\mathbb{G}_{m}&\overset{n}{\longrightarrow}&\mathbb{G}_{m}\\\ \end{matrix}$

would be commutative, whence the formula

$None$ $\psi_{n}(u)=\frac{(hu+1)^{n}-1}{h^{n}},$

cf. [SOS].

2.3. The Kummer map for $\mathbb{L}_{h}$. We play the same game with
$\mathbb{L}_{h}$.

Namely a morphism of groups $\phi_{n}$ included into a commutative diagram

$\begin{matrix}\mathbb{L}_{h}&\overset{\phi_{n}}{\longrightarrow}&\mathbb{L}_{h^{n}}\\\
\beta_{h}\downarrow&&\downarrow\beta_{h^{n}}\\\
\mathbb{G}_{m}&\overset{n}{\longrightarrow}&\mathbb{G}_{m}\\\ \end{matrix}$

is defined by

$\phi_{n}(u)=\frac{1}{h^{n}}\frac{(1+nh)^{n}-(1-nh)^{n}}{(1+nh)^{n}+(1-nh)^{n}}.$

§3. Roots of unity and Artin-Schreier

In 3.1, 3.2 below we recall [SOS]; in 3.3 we describe its analogue for the
Lorentz group.

3.1. $p$-cyclotomic extension of $\mathbb{Q}_{p}$.  Together with [SOS]
consider a ring $k=\mathbb{Z}_{p}[\zeta_{p}]$, $\zeta=\zeta_{p}=e^{2\pi i/p}$,
$p$ being a prime number. Thus $k$ is the ring of integers in
$\mathbb{Q}_{p}(\zeta_{p})$.

Let $h=\zeta-1\in k$.

We have a totally ramified extension of degree $p-1$,

$\mathbb{Z}_{p}\subset k=\mathbb{Z}_{p}[y]/(1+y+\ldots+y^{p-1}),$

$k$ is a discrete valuation ring with a uniformising parameter $h$ and
quotient field $k/(h)=\mathbb{F}_{p}$, cf. [Se], Ch. IV, Prop. 17.

We have

$None$ $h^{p-1}=wp$

where $w\in k^{*}$ and

$None$ $w\equiv-1\mod h.$

3.1.1. Example. Let $p=3$; then:

$\zeta^{2}+\zeta+1=0,$ $h^{2}=(\zeta-1)^{2}=-3\zeta,$
$w=-\zeta=(1+\zeta)^{-1}=-1-h.$

(a) The group $\mathbb{S}_{h}$

3.2. Consider the map

$\psi_{p}:\ \mathbb{S}_{h}\longrightarrow\mathbb{S}_{h^{p}},$
$\psi_{p}(u)=\frac{(hu+1)^{p}-1}{h^{p}}$

Due to $(3.1.1)$ this map is defined over $k$.

On the other hand due to $(3.1.2)$ its special fiber

$\psi_{p,s}:=\psi_{p}\otimes_{k}\mathbb{F}_{p}:\mathbb{G}_{a,\mathbb{F}_{p}}\longrightarrow\mathbb{G}_{a,\mathbb{F}_{p}}$

coincides with the Artin-Schreier map

$\psi_{p,s}(u)=\wp(u):=u^{p}-u,$

cf. [SOS], (2.2.2), (2.2.3).

(b) The group $\mathbb{L}_{h}$

3.3. Similarly consider the map

$\phi_{p}:\ \mathbb{L}_{h}\longrightarrow\mathbb{L}_{h^{p}},$
$\phi_{p}(u)=\frac{1}{h^{p}}\frac{(1+ph)^{n}-(1-ph)^{n}}{(1+ph)^{n}+(1-ph)^{n}}.$

Again due to $(3.1.2)$ its special fiber at $h=0$ coincides with the Artin -
Schreier map.

§4. Remarks on $q$-deformed tori

In this Section we use our viewpoint to clarify somewhat the contents of
[MRT], 6.4.1.

4.1. Filtered circle. In [MRT], 6.4.1 the authors introduce an object
$\mathbf{S}^{1}_{\operatorname{Fil},\mathbb{Z}}$ which they call the ”filtered
circle over $\mathbb{Z}$”. They start with the formal group law
$\mathbb{S}_{h}$ (2.2.1) over $\mathbb{A}^{1}_{\mathbb{Z}}$ which they denote
$\mathbb{G}$, $h$ (their $\lambda$) being the coordinate along
$\mathbb{A}^{1}$.

Let $\mathcal{R}=\operatorname{Dist}(\mathbb{G})$ denote the algebra of
distributons - the dual to the algebra of functions on $\mathbb{G}$; it is a
filtered commutative and cocommutative Hopf algebra. They define a filtered
group scheme

$\mathbf{H}_{\mathbb{Z}}=\operatorname{Spec}(Rees(\mathcal{R}))$

where $Rees$ denotes the Rees construction. By definition
$\mathbf{S}^{1}_{\operatorname{Fil},\mathbb{Z}}$ is its classifying stack

$\mathbf{S}^{1}_{\operatorname{Fil},\mathbb{Z}}=B\mathbf{H}_{\mathbb{Z}}.$

This construction can be $q$-deformed. To do this, the authors remark that the
fiber at $h=1$, $\mathcal{R}_{1}=\operatorname{Dist}(\mathbb{G}_{1})$ is
isomorphic to the algebra of polynomials $f(x)\in\mathbb{Q}[x]$ such that
$f(\mathbb{Z})\subset\mathbb{Z}$ (I am grateful to B.Toen who explained to me
the above statement). The last algebra admits a $q$-deformation
$\mathcal{R}_{1,q}$ introduced in [HH].

This allows to define a $q$-deformation $\mathcal{R}_{q}$ of $\mathcal{R}$.

It was remarked in [HH] that the algebra $\mathcal{R}_{1,q}$ is isomorphic to
the standard Cartan subalgebra $K_{q}$ of the Lusztig’s divided power quantum
group $U_{q}\mathfrak{sl}_{2}$.

4.2. Lorentzian counterpart. We may replace in the above discussion
$\mathbb{S}_{h}$ by $\mathbb{L}_{h}$ which by definition lies inside $SL_{2}$;
so we consider a model $SL_{2,\mathbb{Z}}$ of $SL_{2}$ over $\mathbb{Z}$, and
$\\{\mathbb{L}_{h}\\}$ is a family of conjugated tori inside it.

We can consider a $q$-deformation of $\operatorname{Dist}(SL_{2,\mathbb{Z}})$,
i.e. the corresponding quantum group $U_{q}\mathfrak{sl}_{2}$, and it would be
natural to think that a family of quantum tori from 4.1 may be identified with
a $q$-deformation $\mathbb{L}_{h,q}\subset U_{q}\mathfrak{sl}_{2}$. However a
realization of this idea meets some difficulties at the moment.

4.3. Towards a filtered $S^{3}$. The Lie group $SL_{2}(\mathbb{C})$ is
homotopy equivalent to $SU(2)$ (the Weyl’s unitary trick) which is in turn
homeomorphic to the sphere $S^{3}$.

This rises a question whether the whole packet of [MRT] and [R] admits a
noncommutative ”quaternionic” version, with $S^{1}$ replaced by $S^{3}$, cf.
[Sch].

Literature

[E] A.Einstein, Zur Elektrodynamik bewegter Körper, Ann. der Physik 17 (1905),
891 - 921.

[F] Ph.Furtwängler, Über die Reziprotätsgesetze zwischen $l$-ten Potenzresten
in algebräischen Zahlkörpers, Abh. Königlischen Ges. Wiss. Göttingen 2 (1902),
Heft 3, 1 - 82; Math. Annalen 58 (1904), 1-50.

[B] Yaroslav Bazaliy, Three zoom talks on Special relativity, Toulouse
”Oxford” seminar, Fall 2020.

[GMS] I.M.Gelfand, R.A.Minlos, Z.Ya.Shapiro, Representations of the rotation
and Lorentz groups and their applications

[HH] Nate Harman, Sam Hopkins, Quantum integer-valued polynomials,
arXiv:1601.06110.

[H] Helmut Hasse, History of Class field thery, in: Algebraic Number Theory,
J.W.S.Cassels, A.Fröhlich (eds). 1967, 266-279.

[MRT] Tasos Moulinos, Marco Robalo, Bertrand Toen, A universal HKR
theorem, arXiv:1906.0011

[M] N.David Mermin, It’s about time

[R] Arpon Raksit, Hochschild homology and the derived de Rham complex
revisited, arXiv:2007.02576.

[Sch] V.Schechtman, Moufang loops and toric surfaces, arXiv:2102.12868.

[SOS] T.Sekiguchi, F.Oort, N.Suwa, On the deformation of Artin-Schreier to
Kummer, Ann. Sci. ENS 22 (1989), 345 - 375.

[Se] J.-P.Serre, Corps locaux

[ST] J.-P.Serre, J.Tate, Exercises, in: Algebraic Number Theory,
J.W.S.Cassels, A.Fröhlich (eds). 1967, 266-279.

[SS] Noriyuki Suwa, Tsutomu Sekiguchi, Théorie de Kummer-Artin-Schreier et
applications, J. Th. Nombr. de Bordeaux 7 (1995), 177-189.

[W] William C.Waterhouse, A unified Kummer-Artin-Schreier sequence, Math. Ann.
277 (1987), 447 - 451.


Department of Computer Science, Rice University, USA Department of Computer
Science, Rice University, USA Department of Computer Science, Rice University,
<EMAIL_ADDRESS><ccs2012> <concept>
<concept_id>10003752.10003809.10003635</concept_id> <concept_desc>Theory of
computation Graph algorithms analysis</concept_desc>
<concept_significance>300</concept_significance> </concept> </ccs2012>
[300]Theory of computation Fixed parameter tractability 2 Arxiv Arxiv 42

# DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving

Anastasios Kyrillidis  Moshe Y. Vardi  Zhiwei Zhang 111The author list has
been sorted alphabetically by last name; this should not be used to determine
the extent of authors’ contributions. Corresponding author: Zhiwei Zhang
(zhiwei@rice.edu).

###### Abstract

Boolean MaxSAT, as well as generalized formulations such as Min-MaxSAT and
Max-hybrid-SAT, are fundamental optimization problems in Boolean reasoning.
Existing methods for MaxSAT have been successful in solving benchmarks in CNF
format. They lack, however, the ability to handle 1) (non-CNF) hybrid
constraints, such as XORs and 2) generalized MaxSAT problems natively. To
address this issue, we propose a novel dynamic-programming approach for
solving generalized MaxSAT problems with hybrid constraints –called _Dynamic-
Programming-MaxSAT_ or DPMS for short– based on Algebraic Decision Diagrams
(ADDs). With the power of ADDs and the (graded) project-join-tree builder, our
versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT,
Min-MaxSAT, and MinSAT with hybrid constraints. Moreover, DPMS scales provably
well on instances with low width. Empirical results indicate that DPMS is able
to solve certain problems quickly, where other algorithms based on various
techniques all fail. Hence, DPMS is a promising framework and opens a new line
of research that invites more investigation in the future.

###### keywords:

Generalized MaxSAT Solving, Algebraic Decision Diagram, Dynamic Programming,
Non-CNF Boolean Constraints

###### category:

##  1 Introduction

The _Maximum Satisfiability_ Problem (MaxSAT) is the optimization version of
the fundamental Boolean satisfiability problem (SAT). MaxSAT asks for the
maximum number of constraints (maximum total weight in weighted setting) that
can be satisfied simultaneously by an assignment. For each assignment, the
number (total weight, in the weighted setting) of violated constraints is
often regarded as the _cost_ that should be minimized. MaxSAT finds abundant
applications in many areas [2], including scheduling [18], planning [31],
software debugging [15], hardware security [70] and explainable AI (XAI) [60]
. Ideally speaking, the constraints may be of any type, though formulas in
conjunctive normal form (CNF) are most studied both in theory and practice
[56]. In spite of the NP-hardness of MaxSAT, there has been dramatic progress
on the engineering side of (weighted-partial) Max-CNF-SAT solvers for
industrial instances [46].

Similar to SAT solvers, MaxSAT solvers can be classified into complete and
incomplete ones. A complete solver will return an assignment of optimal cost
with a guarantee (proof), while an incomplete algorithm only gives a “good"
assignment without a guarantee of optimality [33]. Complete (partial) MaxSAT
solvers constitute the majority of the MaxSAT solver family. Mainstream
techniques of complete MaxSAT solvers have been shifting from DPLL [25] and
Branch-and-Bound (B&B) [35] to iterative or core-guided CDCL-based approaches
[40, 29, 4]. Those methods have achieved remarkable performance on large-scale
benchmarks in CNF [7]. Most incomplete MaxSAT solvers are based on local
search (LS) and its variants. Local search is advantageous for quickly
exploring the assignment space and heuristically adapting constraint weights.
LS-based solvers can be surprisingly efficient in reaching a low-cost region
for large instances, which can be infeasible for complete solvers [39]. While
there was a performance gap between complete solvers and LS-based solvers on
industrial benchmarks, this gap has been encouragingly squeezed by recent work
[39]. Nevertheless, due to the incompleteness of those solvers, they are still
not the most preferable solvers in many applications despite their efficiency.

Regardless of the success of modern Max-CNF-SAT solvers, we point out that
their capability of handling more general problems is insufficient. In this
paper, we consider two important extensions of Max-CNF-SAT. The first one is
to generalize the type of constraints from CNF clauses to general (_hybrid_)
Boolean constraints [37] –e.g., cardinality constraints and XORs– yielding the
Max-hybrid-SAT problem. Max-hybrid-SAT offers strong expressiveness and
numerous applications; e.g., Max-XOR-SAT encodes problems in cryptanalysis
[48] and maximum-likelihood decoding [10]. In another direction, there are
problems that require Boolean optimization with uncertainty or adversarial
agent citeQMaxSAT. Thus, the second extension is to allow both $\min$ and
$\max$ operators to define the Min-MaxSAT problem, whose complexity falls into
$\Pi^{p}_{2}$-complete, which is likely harder than NP-hard [63]. Min-MaxSAT
acts as a useful encoding in combinatorial optimization [34] and conditional
scheduling [57].

Max-hybrid-SAT and Min-MaxSAT are less well studied compared with MaxSAT.
Furthermore, the dominating techniques in complete modern Max-CNF-SAT solvers
(SAT-based, B&B) are not easily applicable to generalized MaxSAT, due to their
dependency on the clausal formulation and the single type of optimization
operator ($\max$). Therefore, a versatile framework that handles different
variants of MaxSAT is desirable.

In this paper, we propose a novel, versatile, and general framework, called
_Dynamic-Programming-MaxSAT_ (DPMS). To our best knowledge, DPMS is the first
framework that is capable of natively handling all variants of MaxSAT
described above. This work is inspired by the success of symbolic dynamic
programming in model counting [21]. One of the theoretical contributions of
our work is to view MaxSAT as max-of-sum and borrow ideas from model counting
(sum-of-product). Though max-of-sum and sum-of-product look different, they
are both special cases of functional aggregate queries (FAQs) [1] and share
common properties such as early projection, which enables us to generalize the
approach of [21] to DPMS.

DPMS consists of two phases: 1) a planning phase where a project-join tree
[21] is constructed as a plan and 2) an execution phase, where constraint
combinations and variable eliminations are conducted according to this plan.
DPMS natively handles a variety of generalized problems, including weighted-
partial MaxSAT, Min-MaxSAT, and Max-hybrid-SAT. Hybrid constraints are handled
by DPMS via using _Algebraic Decision Diagrams_ (ADDs) to represent pseudo-
Boolean functions, while Min-MaxSAT formulations are handled by using _graded_
project-join trees [22] as plans for execution. Other under-researched
formulations such as MinSAT [5] and Max-MinSAT problems can also fit well in
our framework. In addition, DPMS explicitly leverages structural information
of instances by taking advantage of the development of tree decomposition
tools [66, 67]. As a result, DPMS scales polynomially on instances with
bounded width.

We developed a software tool implementing the DPMS framework. We demonstrate
in the experiment section that on problems with hybrid constraints and low
width, DPMS outperforms start-of-the-art MaxSAT and pseudo-Boolean solvers
equipped with CNF encodings. We also show that DPMS can be significantly
enhanced by applying ideas from other discrete optimization methods such as
branch-and-bound. Therefore, we believe that DPMS opens a promising research
branch that awaits new ideas and improvements.

##  2 Related Work

###  2.1 Dynamic Programming and MaxSAT

Dynamic programming (DP) is widely used in Boolean reasoning problems such as
satisfiability checking [30, 51], Boolean synthesis [24], and model counting
[32]. In practice, the DP-based model counter, ADDMC [20] tied for the first
place in the weighted track of the 2020 Model Counting Competition [23]. ADDMC
was further enhanced to DPMC [21] by decoupling the planning phase from the
execution phase. DPMC uses project-join trees to enclose various planning
details such as variable ordering, making the planning phase a black box which
can be applied across different Boolean optimization problems. Notwithstanding
the success of DP-based model-counters, the practical potential of DP has not
been deeply investigated in the MaxSAT community yet, though in [58] the
authors built a proof-of-concept DP-based MaxSAT solver and tested it on a
limited range of instances.

###  2.2 Existing Approaches for Solving General MaxSAT and How DPMS Compares

First, hybrid constraints are admitted by DPMS via using ADDs to represent
pseudo-Boolean functions. ADDs can compactly express many useful types of
constraints besides disjunctive clauses, such as XOR and cardinality
constraints. There exist other approaches for handling specific Max-hybrid-SAT
problems; e.g., using stochastic local search in an incomplete Max-XOR-SAT
solver [49] and applying UNSAT-based approaches for Max-PB-SAT [45]. We are
not aware, however, of the existence of a general solver for hybrid
constraints. Alternatively, Max-hybrid-SAT can be reduced to group MaxSAT [27]
by CNF encodings [55]. Each hybrid constraint is first encoded to a group of
disjunctive clauses. A new block variable is introduced for each group such
that if the original hybrid constraint is violated, the corresponding group
can only contribute one violated clause. Then, the group MaxSAT problem can be
solved either as is, or further reduced to weighted MaxSAT. Those approaches,
however, suffer from $i)$ significant increment of the problem size due to
encodings, and $ii)$ the uncertain performance of choosing a specific
encoding. In contrast, DPMS does not involve new variables, constraints, or
encoding selection.

Second, DPMS naturally handles Min-MaxSAT by using a graded project-join tree
as the plan for execution, which is also applied in [22] for projected model
counting. Graded project-join trees enforce the order of variable elimination
restricted by the order of $\min$ and $\max$, while the execution phase
remains the same as that on an ungraded tree. There exists a line of research
that uses $d$-DNNF compilation with the _constrained_ property [54], which is
similar to the graded tree in our work. Nevertheless, their approach only
applies to CNF formulas, and the constrained property is not always enforced.
In [44, 28], the authors studied the more general problem, Quantified MaxSAT,
which falls to the complexity class PSPACE-complete. They did not exploit,
however, the specific properties of Min-MaxSAT.

##  3 Notations and Preliminaries

###  3.1 Pseudo-Boolean Functions

######  Definition 3.1.

A pseudo-Boolean function $F$ over a variable set $X=\\{x_{1},\cdots,x_{n}\\}$
is a mapping from the Boolean cube $\mathbb{B}^{X}$ to the real domain
$\mathbb{R}$.

We use $\mathbb{B}^{X}$ to denote both the power set of $X$ as well as the set
of all assignments of a pseudo-Boolean function. I.e., an assignment
$b\in\mathbb{B}^{X}$ is a subset of $X$. Below we list several operations on
pseudo-Boolean functions.

######  Definition 3.2.

(Sum) Let $F$, $G:\mathbb{B}^{X}\to\mathbb{R}$ be two pseudo-Boolean
functions. The sum of $F$ and $G$, denoted by $F+G$, is defined by
$(F+G)({b})=F({b})+G({b})$ for all ${b}\in\mathbb{B}^{X}$.

######  Definition 3.3.

(Optimization) Let $F$ be a pseudo-Boolean function, $x\in X$ be a variable.
The maximization of $F$ w.r.t. $x$, denoted by
$\mathop{\max}\limits_{x}F:\mathbb{B}^{X\setminus\\{x\\}}\to\mathbb{R}$, is
defined by

$(\mathop{\max}\limits_{x}F)({b})=\mathop{\max}\\{F({b}\cup\\{x\\}),F({b})\\},\text{\,for
all ${b}\in\mathbb{B}^{X\setminus\\{x\\}}$.}$

The maximization operation can be extended to be w.r.t. a set $S\subseteq X$
of variables, denoted by

$\mathop{\max}_{S}F:\mathbb{B}^{X\setminus
S}\to\mathbb{R}:(\mathop{\max}\limits_{S}F)({b}_{1})=\mathop{\max}\limits_{{b}_{2}\in\mathbb{B}^{S}}F({b}_{1}\cup{b}_{2}),\text{\,\,
for all ${b}_{1}\in\mathbb{B}^{X\setminus S}$.}$

The minimization of $F$ w.r.t. $x$ (resp., $S$) is defined similarly. After
optimization, $x$ (resp., variables in $S$) is (are) eliminated from the
domain of resulting function. We also define the $\operatorname*{arg\,max}$ of
$F$ w.r.t. $x$, denoted by
$\operatorname*{arg\,max}_{x}F:\mathbb{B}^{X\setminus\\{x\\}}\to\mathbb{B}^{\\{x\\}}$,
for all ${b}\in\mathbb{B}^{X\setminus\\{x\\}}$:

$\displaystyle(\mathop{\operatorname*{arg\,max}}\limits_{x}F)({b})=\begin{cases}\\{x\\}&\text{\,\,\,if
$F({b}\cup\\{x\\})\geq F({b})$},\\\
\emptyset&\text{\,\,\,otherwise.}\end{cases}$

######  Definition 3.4.

(Derivative)  Let $F$ be a pseudo-Boolean function and $x\in X$ be a variable.
The derivative of $F$ w.r.t. $x$, denoted by
$\nabla_{x}F:\mathbb{B}^{X\setminus\\{x\\}}\to\mathbb{R}$, is defined by
$\nabla_{x}F({b})=F({b}\cup\\{x\\})-F({b}),\text{\,\,for all
${b}\in\mathbb{B}^{X\setminus\\{x\\}}$.}$ We say $x$ is _irrelevant_ w.r.t.
$F$, if $\nabla_{x}F\equiv 0$.

######  Definition 3.5.

(Sign)  Let $F$ be a pseudo-Boolean function. The sign of $F$, denoted by
$\texttt{sgn}F:\mathbb{B}^{X}\to\\{0,1\\}$, equals $1$ if $F({b})\geq 0$ and
$0$ otherwise, for all ${b}\in\mathbb{B}^{X}$.

###  3.2 MaxSAT, Max-hybrid-SAT and Min-MaxSAT

We consider the conjunctive form over a set of variables $X$, i.e.,
$f(X)=c_{1}(X)\wedge c_{2}(X)\wedge\dots\wedge c_{m}(X)$, where each $c_{i}$
is a Boolean constraint. If each constraint of $f$ is a disjunctive clause,
then $f$ is in the well-known CNF format. Traditional MaxSAT asks the maximum
number of constraints satisfied simultaneously by an assignment of $X$.
Weighted MaxSAT attaches a real number as the weight to each constraint and
seeks for the maximum total weight of satisfied constraints.

Formally, MaxSAT can be written as an optimization problem on pseudo-Boolean
functions. Let the constraint set of $f$ be $C_{f}$ and $w:C_{f}\to\mathbb{R}$
be a constraint weight function. For each formula in conjunctive form, we can
construct an objective function as follows. For each $c\in C_{f}$ and
assignment ${b}\in\mathbb{B}^{X}$, we overload an indicator function to $c$:
$c(b)=w(c)$ if $b$ satisfies $c$ and $0$ otherwise. Note that the constraint
weight is included in the indicator function. Then the objective function is
defined as follows.

######  Definition 3.6.

(Objective function) Let $f$ be a conjunctive formula over $X$ with constraint
set $C_{f}$. Then the objective function w.r.t. $f$, denoted by $F_{f}$ is
defined as:

$F_{f}({b})=\sum_{c\in C_{f}}{c({b})},\,\,\text{for all
${b}\in\mathbb{B}^{X}$.}$

######  Definition 3.7.

(MaxSAT) Using the notation in Definition 3.6, the MaxSAT problem is to
compute the value of:

$\mathop{\max}\limits_{X}F_{f}=\mathop{\max}\limits_{{b}\in\mathbb{B}^{X}}\sum_{c\in
C_{f}}{c({b})}.$

It is often desirable to also obtain a Boolean assignment, called a maximizer,
${b}^{\star}\in\mathbb{B}^{X}$ such that
$F_{f}({b}^{\star})=\mathop{\max}_{X}F_{f}$.

In this work, the constraints of a formula are not limited to clauses,
yielding the _Max-hybrid-SAT problem_. Specifically, each constraint can be of
a type listed in Table 1.

Type |  | Example |  | Size of ADD
---|---|---|---|---
CNF clause |  | $x_{1}\vee\neg x_{2}$ |  | $O(l)$
XOR |  | $x_{1}\oplus x_{2}\oplus x_{3}$ |  | $O(l)$
cardinality |  |  $\sum\limits_{i=1}^{5}x_{i}\geq 3$ |  | $O(l^{2})$
pseudo-Bool. |  | $3x_{1}+5x_{2}-6x_{3}\geq 2$ |  | $O(M\cdot l)$
Table 1:  Types of constraints considered in this work. In the third column, $l$ is # variables in the constraint and $M$ is the largest magnitude of coefficients in the PB constraint. ADD Operation |  | Complexity
---|---|---
$\texttt{sum}(A_{1},A_{2})$ |  | $O(|A_{1}|\cdot|A_{2}|)$
$\nabla_{x}A$ / $\max_{x}A$ / $\min_{x}A$ |  | $O(|A|^{2})$
$\texttt{sgn}(A)$ |  | $O(|A|\cdot\log(|A|))$
Table 2: Complexity of some ADD operations

By analogy with QBF [62] in satisfiability checking, MaxSAT can be generalized
by allowing both $\min$ and $\max$ operators.

######  Definition 3.8.

(Min-MaxSAT) For $f$ in Boolean conjunctive form over $X\cup Y$, where
$\\{X,Y\\}$ is a partition of all variables. The Min-MaxSAT problem is to
compute:

$\mathop{\min}\limits_{X}\mathop{\max}\limits_{Y}F_{f}=\mathop{\min}\limits_{{b_{1}}\in\mathbb{B}^{X}}\mathop{\max}\limits_{{b_{2}}\in\mathbb{B}^{Y}}\sum_{c\in
C_{f}}{c({b_{1}}\cup{b_{2}})}.$

The maximizer is a function $\mathcal{M}:\mathbb{B}^{X}\to\mathbb{B}^{Y}$ such
that
$F_{f}({b_{1}}\cup\mathcal{M}({b_{1}}))=\mathop{\max}_{{b_{2}}\in\mathbb{B}^{Y}}F_{f}({b_{1}}\cup{b_{2}})$
for all ${b_{1}}\in\mathbb{B}^{X}$.

The value
$\mathop{\min}_{{b_{1}}\in\mathbb{B}^{X}}\mathop{\max}_{{b_{2}}\in\mathbb{B}^{Y}}F({b_{1}},{b_{2}})$
equals $\theta$ is interpreted as: for every assignment of $X$, there is
always an assignment of $Y$ such that at least $\theta$ constraints are
satisfied. Note that the MinSAT problem [5], which asks for an assignment that
satisfies minimum number of constraints, is a special case of Min-MaxSAT.

When both $\min$ and $\max$ are applied, the order of operators becomes
critical. Within a prefix, two adjacent operators of different type
($\max$-$\min$ or $\min$-$\max$) is called an _alternation_ [28]. MaxSAT has
zero alternation, while a Min-MaxSAT instance has one. General cases with more
than one alternation is beyond the scope of this paper.

###  3.3 Algebraic Decision Diagrams

Algebraic Decision Diagram (ADD) [8] can be seen as an extension of (reduced,
ordered) _Binary Decision Diagrams_ (BDDs) [12] to the real domain for
representing pseudo-Boolean functions in a point-value style. An ADD is a
directed acyclic graph, where each terminal node is associated with a real
value. The size of an ADD is usually defined by the number of nodes. ADD
supports multiple operations in polynomial time w.r.t. the ADD size [69], as
Table 2 shows.

##  4 Theoretical Framework

###  4.1 Solving MaxSAT by DP and Project-Join Trees

Our symbolic approach for solving the MaxSAT problem in Definition 3.7 is
based on applying two operations on pseudo-Boolean functions: sum and
optimization. In the general case, all optimization operations have to be
conducted after all sum operations are completed. Nevertheless, sometimes it
is possible and advantageous to apply optimization before sum. This is enabled
by exploiting the structure of the conjunctive form and is called _early
optimization_.

######  Proposition 4.1.

(Early Optimization) Let $F$, $G$: $\mathbb{B}^{X}\to\mathbb{R}$ be two
pseudo-Boolean functions and $x\in X$ be a variable. If $\nabla_{x}G\equiv 0$,
then we have $\mathop{\max}_{x}(F+G)\equiv(\mathop{\max}_{x}F)+G.$ A similar
result holds for the $\min$ operator.

In particular, if a variable $x$ only appears in a part of the additive
objective function, then we only need to eliminate $x$ in components where $x$
is relevant.

Early elimination of variables, which reduces the problem size, has been
proven successful and critical for other symbolic tasks. Since in MaxSAT, all
variables are under the same operator ($\max$), theoretically the order of
variable elimination can be arbitrary. In practice, however, the order of
variable elimination is observed as crucial, potentially leading to
exponential differences in running time [13]. Therefore, an efficient
algorithm needs to strategically choose the next variable to eliminate and
numerous heuristics have been designed for finding a good order as a plan of
execution [14]. A recent work called DPMC decouples the planning phase from
the execution phase for solving the model counting problem. In the planning
phase, a _project-join tree_ is constructed as an execution plan. During the
execution phase, constraints are joined using the product, and variables are
eliminated according to the project-join tree. In this work, we reuse project-
join trees for solving generalized MaxSAT problems.

######  Definition 4.2.

(Project-join tree) [21] For a tree $T$, let $V(T)$ and $L(T)$ be the set of
nodes and leaves of $T$, respectively. Let $f$ be a conjunctive formula over
$X$. A project-join tree of $f$ is a tuple $\mathcal{T}=(T,r,\gamma,\pi)$,
where $T$ is a tree with root $r\in V(T)$, $\gamma:L(T)\to C_{f}$ is a
bijection between the leaves of $T$ and the (indicator functions of)
constraints of $f$, and $\pi:V(T)\setminus L(T)\to 2^{X}$ is a labeling
function on internal nodes. $\mathcal{T}$ must also satisfy

  1. 1.

$\\{\pi(v):v\in V(T)\setminus L(T)\\}$ is a partition of $X$.

  2. 2.

For each internal node $v\in V(T)\setminus L(T)$, a variable $x\in\pi(v)$, and
a constraint $c\in C_{f}$ that contains variable $x$, the leaf node
corresponding to $c$, i.e., $\gamma^{-1}(c)$, must be a descendant of $v$ in
$T$.

The idea of using a project-join tree for solving MaxSAT is as follows. Each
leaf of the tree corresponds to an original constraint, stored by $\gamma$.
Each internal node $v$ corresponds to the pseudo-Boolean function obtained by
summing (join) all sub-functions from the children of $v$ and eliminating all
variables attached to the node $v$ by maximization (project). This idea is
formalized as the _valuation_.

######  Definition 4.3.

(Valuation) For a project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$, a node
$v\in V(T)$, the valuation of $v$, which is a pseudo-Boolean function denoted
by $\mathcal{F}_{v}^{\mathcal{T}}$, is defined as:

$\displaystyle\mathcal{F}_{v}^{\mathcal{T}}=\begin{cases}\gamma(v)&\text{if
$v\in L(T)$},\\\
\mathop{\max}\limits_{\pi(v)}\sum\limits_{u\in\texttt{children}(v)}\mathcal{F}_{u}^{\mathcal{T}}&\text{if
$v\not\in L(T)$}.\end{cases}$

The valuation of the root $r$ gives the answer to the MaxSAT problem.

######  Theorem 4.4.

Let $\mathcal{T}$ be a project-join tree, then we have

$\mathcal{F}_{r}^{\mathcal{T}}=\mathop{\max}\limits_{X}F_{f}=\mathop{\max}\limits_{{b}\in\mathbb{B}^{X}}\sum_{c\in
C_{f}}{c({b})}$

A project-join tree, which can be viewed as an encapsulation of many planning
details, e.g., cluster ordering, guides the execution of a DP-based approach
[21]. Since building a project-join tree only depends on the incidence graph
[61] of a formula, we use the tree constructor from DPMC as a black box for
solving MaxSAT.

###  4.2 Using ADDs to Express Pseudo-Boolean Functions

Solving Max-hybrid-SAT symbolically as discussed above requires the data
structure for pseudo-Boolean functions to have $i$) the support of efficient
functional addition and maximization; $ii$) the expressiveness of different
types of constraints. ADD is a promising candidate, compared, for example,
with truth table and polynomial representation such as Fourier expansions
[50]. In terms of size, ADDs are usually more compact than other
representations due to redundancy reduction. In particular, ADDs can
succinctly encode a number of useful types of constraints (some examples are
listed in Table 1 [36, 38]). Moreover, ADDs support several important
operations efficiently, as Table 2 shows. ADDs also own well-developed
packages such as CUDD [64] and Sylvan [68].

Summing up all ADDs corresponding to initial constraints in $C_{f}$–without
early variable eliminations–already provides a complete algorithm for MaxSAT.
To see this, note that after summing all ADDs obtained from $C_{f}$, the
terminal nodes of the monolithic ADD represent the cost of all assignments.
Therefore, one just needs to find the terminal value of the monolithic ADD
with the largest value by maximizing over this ADD. Using the sum operation
first, however, can lead to a potential exponential blow-up of the ADD size.
Thus, early optimization introduced above has to be involved in order to
alleviate the explosion.

At each internal node $v$ of the project-join tree, we need to compute the
corresponding valuation $\mathcal{F}_{v}^{\mathcal{T}}$. We first sum up sub-
valuations from the children of $v$ to get an ADD $A$. Then we iteratively
_apply_ $\max$ w.r.t. variables attached on $v$, i.e., $\pi(v)$, to $A$. This
method naturally follows Definition 4.3 and is shown in Algorithm 2. Line 2
and 2 are for constructing the maximizer, with details provided later.

Input : A conjunctive formula $f$ with set of constraints $C_{f}$

Output : The value of $\max_{X}F_{f}$ and a maximizer ${b}^{\star}$

1 $\mathcal{T}=(T,r,\gamma,\pi)\leftarrow$constructProjectJoinTree$(C_{f})$

2 $\mathcal{S}\leftarrow$ an empty stack

3 $answer\leftarrow\texttt{computeValuation}(\mathcal{T},r,\mathcal{S})$

4 $b^{\star}\leftarrow\texttt{constructMaximizer}(\mathcal{S})$

return $answer,{b}^{\star}$

Algorithm 1 DPMS$(f)$

Input : A project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$, a node $v\in
V(T)$, a stack $\mathcal{S}$ for constructing the maximizer.

Output : An ADD representation of $\mathcal{F}^{\mathcal{T}}_{v}$

1 if  _$v\in L(T)$ _ then return $\texttt{compileADD}(\gamma(v))$;

2
$A\leftarrow\sum\limits_{u\in\texttt{children(v)}}\texttt{computeValuation}(\mathcal{T},u,\mathcal{S})$

3 for  _$x\in\pi(v)$_ do

4 /* For maximizer generation */

5 $G_{x}\leftarrow\texttt{sgn}(\nabla_{x}A)$

6 $\mathcal{S}$.push$((x,G_{x}))$

7 $A\leftarrow\mathop{\max}_{x}A$ // Eliminate $x$

8

9return $A$

Algorithm 2 computeValuation$(\mathcal{T},v,\mathcal{S})$

Inspired by _Basic Algorithm_ of pseudo-Boolean optimization [16], we consider
an alternative of computing the same output with Alg. 2. The theory of Basic
Algorithm and practical comparisons between Alg. 2 and the alternative can be
found in the appendix.

###  4.3 Solving Min-MaxSAT by Graded Trees

In MaxSAT, only the $\max$ operator is used. Nevertheless, since it is equally
expensive to compute $\max$ and $\min$ for the symbolic approach, adapting
techniques described above for solving the Min-MaxSAT problem in Definition
3.8 is desirable. In MaxSAT, the order of eliminating variables can be
arbitrary, while that in Min-MaxSAT is restricted. More specifically, a
variable under $\min$ can be eliminated only after all variables under $\max$
are eliminated. In terms of the project-join tree, roughly speaking, in every
branch, a node attached with $\min$ variables must be “higher" than all nodes
attached with $\max$ variables. This requirement can be satisfied by the
_graded_ project-join tree, originally used for _projected model counting_
[22].

######  Definition 4.5.

(Graded project-join tree) [22] Let $X,Y$ be a partition of all variables. A
project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$ is called ($X$-$Y$) graded if
there exists $I_{X}$, $I_{Y}\subseteq V(T)\setminus L(T)$, such that:

  1. 1.

$I_{X},I_{Y}$ is a partition of internal nodes $V(T)\setminus L(T)$.

  2. 2.

For each internal node $v\in V(T)\setminus L(T)$, if $v\in I_{X}$, then
$\pi(v)\subseteq X$; if $v\in I_{Y}$ then $\pi(v)\subseteq Y$.

  3. 3.

For every pair of internal nodes $(u,v)$ such that $u\in I_{x}$ and $v\in
I_{Y}$, $u$ is not a descendant of $v$ in $T$.

Constructing a graded project-join tree also only depends on the incidence
graph of a formula. Thus we can apply existing graded project-join tree
builders to our Min-MaxSAT problem, where $X$ is the set of $\min$ variables
and $Y$ is the set of $\max$ variables [22].

We note that DPMS can easily handle also Max-MinSAT problems by making $X$ the
set of $max$ variables and $Y$ the set of $min$ variables. In contrast,
adapting state-of-the-art MaxSAT and PB solvers to solve Max-MinSAT can be
nontrivial.

###  4.4 Constructing the Maximizer

MaxSAT often asks also for the maximizer ${b}^{\star}$ such that
$F_{f}({b}^{\star})=\mathop{\max}_{X}F_{f}$ [41]. In DPMS, the maximizer is
constructed recursively in the reverse order of variable elimination, based on
the following proposition.

######  Proposition 4.6.

For a pseudo-Boolean function $F$ and a variable $x\in X$, if $b^{\star}$ is a
maximizer of $\max_{x}F$, then
$\\{(\operatorname*{arg\,max}_{x}F)(b^{\star})\\}\cup b^{\star}$ is a
maximizer of $F$.

In the following proposition, we show that the $\operatorname*{arg\,max}$ of a
pseudo-Boolean function is the sgn of the derivative.

######  Proposition 4.7.

For a pseudo-Boolean function $F:\mathbb{B}^{X}\to\mathbb{R}$ and a variable
$x$, we have, for all ${b}\in\mathbb{B}^{X\setminus\\{x\\}}$:
$\mathop{\operatorname*{arg\,max}}_{x}F({b})$ equals $\\{x\\}$ if
$\texttt{sgn}\nabla_{x}F({b})=1$ and $\emptyset$ otherwise.

The idea of generating a maximizer in DPMS by Algorithm 2 and 3 is as follows.
In Algorithm 2, suppose when a variable $x$ is eliminated, variables in
$S\subseteq X$ have already been summed-out. Then $\nabla_{x}A$ is equivalent
to $\nabla_{x}\max_{S}F$ (see the proof of Theorem 4.8). Therefore, by
Proposition 4.7, the $0$-$1$ ADD $G_{x}=\texttt{sgn}(\nabla_{x}A)$ computed in
Line 2, is the ADD representation of
$\operatorname*{arg\,max}_{x}(\max_{S}F)$. By Proposition 4.6, with $G_{x}$,
finding a maximizer of $max_{S}F$ can be reduced to that of
$(max_{S\cup\\{x\\}}F)$, a smaller problem. As variable-ADD pairs get pushed
into the stack in Line 2, the ADD in the pair relies on fewer and fewer
variables. In particular, when the last variable, say $x_{l}$ is eliminated,
then $G_{x_{l}}$ is a constant $0$-$1$ ADD indicating the value of $x_{l}$ in
the maximizer. The stack $\mathcal{S}$ will pop variables in the reverse order
of variable elimination. In Algorithm 3, a maximizer is iteratively built
based on Proposition 4.6. Similar idea of building a maximizer can be found in
_Basic Algorithm_ of pseudo-Boolean optimization [16].

Input : A stack $\mathcal{S}$ of $|X|$ variable-ADD pairs

Output : ${b}^{\star}$ such that $F_{f}({b}^{\star})=\mathop{\max}_{X}F_{f}$

1 $b^{\star}\leftarrow\emptyset$

2 while  _$\mathcal{S}$ is not empty_ do

3 $(x,G_{x})\leftarrow\mathcal{S}.\texttt{pop}()$

4 if  _$G_{x}(b^{\star})=1$_ then $b^{\star}\leftarrow b^{\star}\cup\\{x\\}$ ;

5

6return ${b}^{\star}$

Algorithm 3 $\texttt{constructMaximizer}(\mathcal{S})$

######  Theorem 4.8.

Algorithm 3 correctly returns a maximizer.

In Min-MaxSAT, the maximizer is a function from variables under $\min$ to
those under $\max$, which is similar to Skolem functions in 2-QBF [9].
Synthesizing such a maximizer could be non-trivial for non-symbolic methods.
In DPMS, this can be done by Algorithm 3 but only $\max$ variables are pushed
into the stack $\mathcal{S}$.

###  4.5 The Complexity of DPMS

For a (graded) project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$, we define the
_size_ of a node $v$, $size(v)$, to be # variables in the valuation
$\mathcal{F}_{v}^{\mathcal{T}}$, plus # variables eliminated in $v$. The width
of a tree $\mathcal{T}$, $width(\mathcal{T})$, is defined to be $\max_{v\in
V(T)}size(v)$. Roughly speaking, $width(\mathcal{T})$ is the maximum #
variables in a single ADD during the execution. The width is an upper bound of
the _treewidth_ of the incidence graph of the formula. It is well known that
the running time of DP-based approaches can be bounded by a polynomial over
the input size on problems with constant width [26].

######  Theorem 4.9.

If the project-join tree (resp. graded project-join tree) builder returns a
tree with width $k$, then DPMS solves the MaxSAT (resp. Min-MaxSAT) problem in
time $O(k\cdot 2^{k}\cdot|f|)$, where $|f|$ is the size of the conjunctive
formula.

Hence, DPMS exhibits the potential of exploiting the low-width property of
instances, as shown later in Section 5.

###  4.6 An Optimization of DPMS: Pruning ADDs by Pre-Computed Bounds

The main barrier to the efficiency of DPMS is the explosive size of the
intermediate ADDs. We alleviate this issue by pruning ADDs via pre-computed
bounds of the optimal cost. The idea is, if we know that a partial assignment
can not be extended to a maximizer, then it is safe to prune the corresponding
branch from all intermediate ADDs. This idea can be viewed as applying branch-
and-bound [35] to ADDs. For a MaxSAT instance, suppose we obtain an upper
bound of the cost of the maximizer, say $U$. Then for each individual ADD $A$,
if the value of a terminal node $v$ indicates that the cost of the
corresponding partial assignment in $A$ already exceeds $U$, then it is
impossible to extend this partial assignment to a maximizer. In this case, we
set the value of $v$ to $-\infty$, which provides two advantages. First, the
number of terminal values in $A$ is reduced, which usually decreases the ADD
size. Second, the partial assignment w.r.t. $v$ is “blocked" globally by
summing $A$ with other ADDs in the rest execution of the algorithm. In the
experiment section, we show that using a relatively good bound significantly
enhances DPMS.

One can obtain $U$ in several ways. One way is to run an incomplete local
search solver within a time limit. Another way is to read $U$ directly from
the problem instance, e.g., the total weight of soft constraints of a partial
MaxSAT instance.

##  5 Empirical Results

We aim to answer the following research questions:

RQ1. Can DPMS outperform state-of-the-art MaxSAT and pseudo-Boolean solvers on
certain problems?

RQ2. How do pre-computed bounds and ADD pruning improve the performance of
DPMS?

RQ3. How does DPMS perform on real-life benchmarks?

To answer the three research questions above, we designed three experiments,
respectively. The first two experiments used synthetic and random hybrid
formulas, respectively. The third experiment gathered instances from Boolean
reasoning competitions.

We included 10 state-of-the-art MaxSAT solvers and 3 pseudo-Boolean (PB)
solvers in comparison, which cover a wide range of techniques such as SAT-
based, MIP, and B&B. We list all the solver competitors below.

#### 10 MaxSAT solvers

  * •

7 Competitors from MaxSAT Evaluation 2021: MaxHS [17], CashWMaxSAT, EvalMaxSAT
[6], OpenWBO [47], UwrMaxSAT [53], Exact, and Pacose [52].

  * •

MaxCDCL [42], a recent MaxSAT solver based on B&B and CDCL.

  * •

ILPMaxSAT [3], an Integer-Linear-Programming-based MaxSAT solver.

  * •

GaussMaxHS [65], a CNF-XOR MaxSAT solver which accepts hard XOR constraints.

#### 3 Pseudo-Boolean solvers

  * •

NAPS [59], winner of the WBO Track of PB competition 16.

  * •

WBO [47], a PB solver that accepts .wbo and .pbo format.

  * •

CuttingCore [19], a recent PB solver based on core-guided search and cutting
planes reasoning.

#### 1 QBF solver

  * •

DepQBF [43], medal winner of QBF evaluations.

Since MaxSAT and PB solvers used in comparison can not handle Max-hybrid-SAT
format, we reduce those hybrid instances to _group MaxSAT_ according to [27].
Then, in order to compare DPMS with MaxSAT and PB solvers, group MaxSAT
problems were further reduced to weighted MaxSAT and pseudo-Boolean
optimization problems by adding _block variables_.

All experiments were run on single CPU cores of a Linux cluster at 2.60-GHz
and with 16 GB of RAM. We implemented DPMS borrowing from the DPMC [21] and
ProCount [22] code base. DPMC’s default setting was used as the default
settings for DPMS. FlowCutter [66] was used as the tree builder. Time limit
was set to be 400 seconds unless specified.

Experiment 1: Evaluation on low-width Chain Max-Hybrid-SAT instances. We
generated the following unweighted “chain” formulas with certain width. A
formula with number of variables $n$ and width parameter $k$ contains
$(n-k+1)$ constraints, where the $i$-th constraint exactly contains variables
in $\\{x_{i},x_{i+1},\cdots,x_{i+k-1}\\}$. Every constraint is either an XOR
with random polarity or a cardinality constraint with random right-hand-side,
each with probability 0.5. It is easy to show that the width of such formulas
is $k$. For $n\in\\{100,200,400,600,800,1000,1200\\}$,
$k\in\\{5,10,15,20,25,30\\}$, we generated $20$ chain formulas with $n$
variables and width $k$. Total number of instances: 840.

Figure 1: Results on 840 hybrid chain formulas describied in Experiment 1.
(Best viewed online) The results of some solvers are presented in the figure.
# solved instances of other solvers are: Exact (169), Uwrmaxsat (163), OpenWBO
(162), MaxHS (75) and CashwMaxSAT (8). DPMS outperformed all solvers in
comparison and significantly improved the VBS.

Answer to RQ1. The overall results of Experiment 1 are shown in Figure 1,
where the _virtual best solver_ (VBS) and VBS without DPMS are also plotted.
On the low-width hybrid MaxSAT instances, DPMS solved 727 out of 840
instances, significantly more than all other MaxSAT and PB solvers in
comparison and the VBS (396) of them. The results indicate that DPMS exhibits
promising performance on hybrid low-width instances. Meanwhile, state-of-the-
art solvers fail to leverage the low-width property and are considerably
slowed down by explosive CNF/PB encodings.

Experiment 2: Evaluation on General Random Max-Hybrid-SAT instances. In this
experiment, we generated random CARD-XOR and PB-XOR instances. For
$n\in\\{50,75,100\\}$, $\alpha_{C},\alpha_{X}\in\\{0.3,0.4,\cdots,1\\}$,
$k\in\\{5,7\\}$, we generated $20$ instances with $n$ variables,
$(\alpha_{C}\cdot n)$ random $k$-cardinality (resp. PB) constraints and
$(\alpha_{X}\cdot n)$ random $k$-XOR constraints. Totally number of instances:
15360.

Generally, the width of pure random instances grows as the number of variables
increases. Previous research indicates that high-width problems can be hard
for DP-based algorithms [21]. Therefore, we do not expect DPMS to outperform
its competitors on the full set of benchmarks. Instead, we aim to show how ADD
pruning can greatly enhance the performance of DPMS. SATLike [39], a pure
local search MaxSAT solver, was used to provide an upper bound of cost. For
each instance, we ran SATLike for 10 seconds (included in the total running
clock time) and used the best bound found for ADD pruning. This combination of
DPMS and SATLike is called DPMS + LS.

|  | DPMS |  | DPMS + LS
---|---|---|---|---
# Solved instances |  | 581 |  | 4385
# Avg. width of solved instances |  | 29.1 |  | 38.2
Avg. reduction of largest ADD size ($\times$) |  | 1 |  | 43.6
Avg. Speed-up ($\times$) |  | 1 |  | 3.86

Table 3: Comparison between DPMS and DPMS + LS on random benchmarks. The
average width of all instances is 45.7. The average approximation ratio given
by the pure local search solver SATLike is 1.21. ADD pruning makes DPMS+LS
solve considerably more instances than DPMS and increase the width DPMS can
handle.

Answer to RQ2. The comparison between DPMS and DPMS + LS is shown in Table 3.
The average approximation ratio of the upper bound provided by running SATLike
for 10 seconds is 1.21. With the help of SATLike and ADD pruning, DPMS + LS
solved significantly more instances (4385) than DPMS (581). DPMS + LS can also
handle instances with higher width (38.2) compared with DPMS (29.1). Moreover,
DPMS + LS provides notable acceleration ($3.86\times$) and reduction of space
usage ($43.6\times$). Therefore, we conclude that ADD pruning is an effective
optimization of DPMS.

Experiment 3: Min-MaxSAT, MaxSAT-PB-SAT, and MaxSAT instances from
competitions. In this experiment, we aim to check whether DPMS can help solve
real-life problems.

To our best knowledge, there are neither Min-MaxSAT benchmarks nor
implementations of Min-MaxSAT solvers publicly available. Thus, we gathered
853 instances from 2-QBF ($\forall\exists$) Track of recent QBF Evaluations
(10, 16, 17, 18) and compared DPMS with DepQBF, a state-of-the-art QBF solver,
though Min-MaxSAT is harder than QBF-SAT.

We also run DPMS on PB-WBO and MaxSAT instances from recent competitions. The
PB-WBO instances are from the latest pseudo-Boolean Competition (PB’16),
Weighted Boolean Optimization (WBO) Track, with the time limit set to 1800
seconds. Those instances can be viewed as weighted partial Max-PB-SAT
problems. The MaxSAT instances are from MaxSAT evaluation 2021 (MSE’21),
Completed Weighted Track with the time limit set to 300 seconds. Most
instances of those competitions are considerably large-size.

Answer to RQ3. The results on Min-MaxSAT instances are listed in Table 4. On
all 853 2-QBF instances, the tree builder succeeded on 125 instances and DPMS
solved 90 of them. All successfully built graded project-join trees have width
smaller than 100. DPMS is faster than DepQBF on 48 instances (Row 6) with
$15.7\times$ acceleration (Row 8). Furthermore, there are in total 39
instances uniquely solved by DPMS in the evaluation (Row 9). Moreover, all
these 39 instances were solved in less than 10% of the time limit while DepQBF
timed out.

The results of MaxSAT and PB evaluations are shown in Table 5. DPMS with
bounds given by local search solved 94 instances (623 in total) for MaxSAT
instances. On Max-PB-SAT instances, DPMS with trivial bounds solved 97
instances (1059 in total). Instances solved by DPMS have lower average
treewidth ($<40$) and a relatively short running time ($7$s for Max-PB-SAT and
$23.6$s for MaxSAT). DPMS is in general, however, not yet competitive on real-
life MaxSAT and PB instances when compared with solvers from competitions.

Row | # Instances |
---|---|---
1 | Total | 853
2 | Tree builder succeed | 125
3 | Avg. width of Row 2 | 58.8
4 | Solved by DPMS | 90
5 | Avg. width of Row 4 | 47.8
6 | DPMS is faster than DepQBF | 48
7 | Avg. width of Row 6 | 62.6
8 |  Avg. acce. ($\times$) of Row 6 | 15.7
9 | Solved Uniquely by DPMS | 39
10 | Avg. width of Row 9 | 67.1
11 | Avg. time (s) of Row 9 | 4.13

Table 4: Performance of DPMS on Min-MaxSAT instances, compared with DepQBF.
DPMS was capable of solving 39 instances where DepQBF timed out.

Row | #instances | PB-WBO (DPMS+Trivial) |  | MaxSAT (DPMS+LS)
---|---|---|---|---
1 | Total | 1059 |  | 623
2 | Tree builder succeed | 181 |  | 116
3 | Avg. width of Row 2 | 44.8 |  | 43.2
4 | Solved by DPMS | 97 |  | 94
5 | Avg. width of Row 4 | 28.4 |  | 38.2
6 | Avg. running time (s) of Row 4 | 7.0 |  | 23.6

Table 5: Performance of DPMS on PB-WBO and MaxSAT instances from competitions.
Instances solved by DPMS on average are low-width. The average running time of
solved instances is also relatively low.

Summary. We demonstrated that DPMS can beat a comprehensive set of state-of-
the-art solvers on synthetic hybrid low-width instances. ADD pruning greatly
enhances the performance of DPMS. On Min-MaxSAT problems, DPMS captures the
structural properties of some instances which are difficult for other
algorithms to exploit. DPMS is not yet competitive against specialized solvers
on real-life MaxSAT and PB instances. Overall, the versatility of handling
various formulations as well as encouraging performance on certain benchmarks
make DPMS a promising framework.

##  6 Conclusion and Future Directions

In this work, we proposed a novel and versatile ADD-based framework called
DPMS for natively handling a number of generalized MaxSAT problems such as
Max-hybrid-SAT and Min-MaxSAT. We leverage the similarity between max-of-sum
and sum-of-product to apply the project-join-tree-based approaches in MaxSAT
solving. ADD enables hybrid constraints, while graded trees enable Min-Max
formulations. Theoretical analysis indicates that DPMS scales polynomially on
instances with bounded width. We implemented our method based on the DPMC code
base. Empirical results demonstrate that DPMS outperforms state-of-the-art
MaxSAT and PB solvers on synthetic hybrid MaxSAT instances with low width.
Experiments also showed that DPMS can be significantly accelerated by branch-
and-bound and ADD pruning. We believe DPMS opens a new research branch and
leads to many interesting future directions. For example, handling instances
with alternation larger than $2$, i.e., general Quantified-MaxSAT [44],
parallelizing DPMS by alternative tree decomposition tools and DD packages
such as Sylvan [68], and integrating other optimization techniques into this
dynamic programming framework.

## References

  * [1] Mahmoud Abo Khamis, Hung Q. Ngo, and Atri Rudra.  Faq: Questions asked frequently.  PODS ’16, 2016.
  * [2] Haifa Alkasem and Mohamed Menai.  Stochastic local search for partial max-sat: an experimental evaluation.  AI Review, 2021.
  * [3] Carlos Ansótegui and Joel Gabas.  Solving (weighted) partial maxsat with ilp.  In CPAIOR, volume 13, pages 403–409, 2013.
  * [4] Carlos Ansótegui, Frédéric Didier, and Joel Gabàs.  Exploiting the structure of unsatisfiable cores in maxsat.  IJCAI, pages 283–289, 2015.  URL: https://www.ijcai.org/Abstract/15/046.
  * [5] Josep Argelich, Chu-Min Li, Felip Manyà, and Zhu Zhu.  Minsat versus maxsat for optimization problems.  In CP 2013, 2013.
  * [6] Florent Avellaneda.  A short description of the solver evalmaxsat.  MaxSAT Evaluation, 2020.
  * [7] Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors.  MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, volume B-2020-2 of Department of Computer Science Report Series B.  Department of Computer Science, University of Helsinki, Finland, 2020\.
  * [8] R.Iris Bahar, Erica Frohm, Charles Gaona, Gary Hachtel, Enrico Macii, Abelardo Pardo, and Fabio Somenzi.  Algebraic decision diagrams and their application.  Formal Metthods in System Design, 10, 1997.
  * [9] V. Balabanov, J. Jiang, C. Scholl, A. Mishchenko, and R. Brayton.  2qbf: Challenges and solutions.  In SAT, 2016.
  * [10] E. Berlekamp, R. McEliece, and H. van Tilborg.  On the inherent intractability of certain coding problems (corresp.).  IEEE Transactions on Information Theory, 24(3):384–386, 1978.  doi:10.1109/TIT.1978.1055873.
  * [11] Endre Boros and Peter L. Hammer.  Pseudo-boolean optimization.  Discrete Applied Mathematics, 123(1):155–225, 2002.  URL: https://www.sciencedirect.com/science/article/pii/S0166218X01003419, doi:https://doi.org/10.1016/S0166-218X(01)00341-9.
  * [12] R. E. Bryant.  Binary decision diagrams and beyond: enabling technologies for formal verification.  In ICCAD, 1995.
  * [13] Arie M. C.A. Koster, Hans L. Bodlaender, and Stan P.M. van Hoesel.  Treewidth: Computational experiments.  Electronic Notes in Discrete Mathematics, 8:54–57, 2001.  URL: https://www.sciencedirect.com/science/article/pii/S1571065305800782, doi:https://doi.org/10.1016/S1571-0653(05)80078-2.
  * [14] Mark Chavira and Adnan Darwiche.  Compiling bayesian networks using variable elimination.  In IJCAI, pages 2443–2449, 2007.  URL: http://ijcai.org/Proceedings/07/Papers/393.pdf.
  * [15] Yibin Chen, Sean Safarpour, Joao Marques-Silva, and Andreas Veneris.  Automated design debugging with maximum satisfiability.  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2010.
  * [16] Yves Crama, Pierre Hansen, and Brigitte Jaumard.  The basic algorithm for pseudo-boolean programming revisited.  Discrete Applied Mathematics, 29(2):171–185, 1990.  URL: https://www.sciencedirect.com/science/article/pii/0166218X9090142Y, doi:https://doi.org/10.1016/0166-218X(90)90142-Y.
  * [17] Jessica Davies.  Solving MaxSAT by decoupling optimization and satisfaction.  PhD thesis, University of Toronto, 2013.
  * [18] Emir Demirović, Nysret Musliu, and Felix Winter.  Modeling and solving staff scheduling with partial weighted maxsat.  Annals of Operations Research, 275, 04 2019.  doi:10.1007/s10479-017-2693-y.
  * [19] Jo Devriendt, Stephan Gocht, Emir Demirovic, Jakob Nordström, and Peter J Stuckey.  Cutting to the core of pseudo-boolean optimization: Combining core-guided search with cutting planes reasoning.  In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages 3750–3758, 2021.
  * [20] Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi.  ADDMC: Weighted Model Counting with Algebraic Decision Diagrams.  arXiv e-prints, page arXiv:1907.05000, July 2019.  arXiv:1907.05000.
  * [21] Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi.  DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees.  2020\.
  * [22] Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi.  Procount: Weighted projected model counting with graded project-join trees.  In SAT, 2021.
  * [23] Johannes K. Fichte, Markus Hecher, and Florim Hamiti.  The Model Counting Competition 2020.  arXiv e-prints, page arXiv:2012.01323, December 2020.  arXiv:2012.01323.
  * [24] Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi.  Bdd-based boolean functional synthesis.  In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, pages 402–421, Cham, 2016. Springer International Publishing.
  * [25] Zhaohui Fu and Sharad Malik.  On solving the partial max-sat problem.  In Theory and Applications of Satisfiability Testing - SAT 2006, 2006.
  * [26] Robert Ganian, Petr Hliněný, and Jan Obdržálek.  Better algorithms for satisfiability problems for formulas of bounded rank-width.  arXiv e-prints, 2010.
  * [27] Federico Heras, Antonio Morgado, and Joao Marques-Sliva.  Maxsat-based encodings for group maxsat.  Ai Communications, 28:195–214, 01 2015.  doi:10.3233/AIC-140636.
  * [28] Alexey Ignatiev, Mikoláš Janota, and Joao Marques-Silva.  Quantified maximum satisfiability: a core-guided approach.  07 2013.  doi:10.1007/978-3-642-39071-5_19.
  * [29] Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva.  Rc2: an efficient maxsat solver.  Journal on Satisfiability, Boolean Modeling and Computation, 11:53–64, 09 2019.  doi:10.3233/SAT190116.
  * [30] Jean-Pierre Jouannaud and Mark Stickel.  Ordered binary decision diagrams and the davis-putnam procedure.  06 1996.  doi:10.1007/BFb0016843.
  * [31] Farah Juma, Eric I. Hsu, and Sheila A. McIlraith.  Preference-based planning via maxsat.  In Canadian Conference on AI, 2012.
  * [32] Philippe Jégou, Hanan Kanso, and Cyril Terrioux.  Improving exact solution counting for decomposition methods.  In 2016 IEEE 28th International Conference on Tools with Artificial Intelligence (ICTAI), pages 327–334, 2016.  doi:10.1109/ICTAI.2016.0057.
  * [33] Henry A. Kautz, Ashish Sabharwal, and B. Selman.  Incomplete algorithms.  In Handbook of Satisfiability, 2009.
  * [34] Ker-I Ko and Chih-Long Lin.  On the Complexity of Min-Max Optimization Problems and their Approximation.  Springer US, Boston, MA, 1995.  doi:10.1007/978-1-4613-3557-3_15.
  * [35] Adrian Kuegel.  Improved exact solver for the weighted max-sat problem.  In POS-10. Pragmatics of SAT, 2012.
  * [36] Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Y. Vardi, and Zhiwei Zhang.  FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints.  In AAAI 20, 2020.
  * [37] Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Y. Vardi, and Zhiwei Zhang.  Solving hybrid boolean constraints in continuous space via multilinear fourier expansions.  Artificial Intelligence, 299:103559, 2021.  URL: https://www.sciencedirect.com/science/article/pii/S0004370221001107, doi:https://doi.org/10.1016/j.artint.2021.103559.
  * [38] Anastasios Kyrillidis, Moshe Y. Vardi, and Zhiwei Zhang.  On Continuous Local BDD-Based Search for Hybrid SAT Solving.  AAAI 21, 2020.
  * [39] Zhendong Lei and Shaowei Cai.  Solving (weighted) partial maxsat by dynamic local search for sat.  In IJCAI-18, pages 1346–1352, 7 2018.
  * [40] Chu Min Li and Felip Manya.  Maxsat, hard and soft constraints.  In Handbook of satisfiability, pages 903–927. IOS Press, 2021.
  * [41] Chu-Min Li and Felip Manyà.  Maxsat, hard and soft constraints.  Frontiers in Artificial Intelligence and Applications, 185, 01 2009\.  doi:10.3233/978-1-58603-929-5-613.
  * [42] Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He.  Combining clause learning and branch and bound for maxsat.  In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021.
  * [43] Florian Lonsing and Uwe Egly.  DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL.  page arXiv:1702.08256, 2017.  arXiv:1702.08256.
  * [44] Amol Dattatraya Mali.  On quantified weighted MAX-SAT.  Decision Support Systems, 2005.  URL: https://www.sciencedirect.com/science/article/pii/S0167923604000302, doi:https://doi.org/10.1016/j.dss.2003.12.004.
  * [45] Vasco M. Manquinho, Ruben Martins, and I. Lynce.  Improving unsatisfiability-based algorithms for boolean optimization.  In SAT, 2010.
  * [46] Joao Marques-Silva, Ines Lynce, and Sharad Malik.  Chapter 4: Conflict-driven clause learning SAT solvers.  Frontiers in Artificial Intelligence and Applications. IOS Press BV, 2021\.  doi:10.3233/FAIA200987.
  * [47] Ruben Martins, Vasco Manquinho, and Inês Lynce.  Open-wbo: A modular maxsat solver,.  In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing – SAT 2014, 2014.
  * [48] Mitsuru Matsui.  Linear cryptanalysis method for des cipher.  In Advances in Cryptology — EUROCRYPT ’93, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.
  * [49] Mark J Minichiello.  Solving max-xor-sat problems with stochastic local search.  2001\.
  * [50] Ryan O’Donnell.  Analysis of Boolean Functions.  New York, NY, USA, 2014.
  * [51] Guoqiang Pan and Moshe Y. Vardi.  Symbolic techniques in satisfiability solving.  In Enrico Giunchiglia and Toby Walsh, editors, SAT 2005, pages 25–50, Dordrecht, 2006. Springer Netherlands.
  * [52] Tobias Paxian, Sven Reimer, and Bernd Becker.  Pacose: an iterative sat-based maxsat solver.  MaxSAT Evaluation 2018, page 20, 2018.
  * [53] Marek Piotrów.  Uwrmaxsat: Efficient solver for maxsat and pseudo-boolean problems.  In 2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI), pages 132–136, 2020.  doi:10.1109/ICTAI50040.2020.00031.
  * [54] Thammanit Pipatsrisawat and Adnan Darwiche.  A new d-dnnf-based bound computation algorithm for functional e-majsat.  pages 590–595, 01 2009.
  * [55] S. Prestwich.  CNF Encodings, Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications, 2009.
  * [56] Steven Prestwich.  Cnf encodings.  Frontiers in Artificial Intelligence and Applications, 2009.
  * [57] Jussi Rintanen.  Constructing conditional plans by a theorem-prover.  JAIR, 1999.
  * [58] Sigve Hortemo Sæther, Jan Arne Telle, and Martin Vatshelle.  Solving# sat and maxsat by dynamic programming.  Journal of Artificial Intelligence Research, 54:59–82, 2015.
  * [59] Masahiko Sakai and Hidetomo Nabeshima.  Construction of an robdd for a pb-constraint in band form and related techniques for pb-solvers.  IEICE Transactions on Information and Systems, E98.D(6):1121–1127, 2015.  doi:10.1587/transinf.2014FOP0007.
  * [60] Masahiro Sakai.  BNN verification dataset for MaxSAT Evaluation 2020.  MaxSAT Evaluation 2020, page 37, 2020.
  * [61] Marko Samer and Stefan Szeider.  Constraint satisfaction with bounded treewidth revisited.  Journal of Computer and System Sciences, 2010.  URL: https://www.sciencedirect.com/science/article/pii/S0022000009000300, doi:https://doi.org/10.1016/j.jcss.2009.04.003.
  * [62] Horst Samulowitz and Fahiem Bacchus.  Using SAT in QBF.  2005\.
  * [63] Marcus Schaefer and Christopher Umans.  Completeness in the polynomial-time hierarchy a compendium.  Sigact News - SIGACT, 33, 01 2002.
  * [64] Fabio Somenzi.  CUDD: CU Decision Diagram Package Release 3.0.0, 2015.
  * [65] Mate Soos and Kuldeep S Meel.  Gaussian elimination meets maximum satisfiability.  In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 18, pages 581–587, 2021.
  * [66] Ben Strasser.  Computing tree decompositions with flowcutter: Pace 2017 submission.  2017\.
  * [67] Hisao Tamaki.  Positive-instance driven dynamic programming for treewidth.  Journal of Combinatorial Optimization, 37(4):1283–1311, 2019.
  * [68] Tom Van Dijk and Jaco Van De Pol.  Sylvan: Multi-core decision diagrams.  In Tools and Algorithms for the Construction and Analysis of Systems, 2015.
  * [69] Ingo Wegener.  Bdds—design, analysis, complexity, and applications.  Discrete Applied Mathematics, 2004.  URL: https://www.sciencedirect.com/science/article/pii/S0166218X0300297X, doi:https://doi.org/10.1016/S0166-218X(03)00297-X.
  * [70] Changjian Zhang, Ruben Martins, Marijn J H Heule, and Eunsuk Kang.  Automated synthesis of minimal hardware exploits with Checkmate and MaxSAT solver.  MaxSAT Evaluation 2020, page 49, 2020.

##  Appendix A The Basic Algorithm and an Alternative of Algorithm 2

In this section, we show an alternative algorithm based on _Basic Algorithm_
that computes the same output as Algorithm 2. We first introduce Basic
Algorithm of pseudo-Boolean optimization, whose idea is shown in Theorem A.1.

######  Theorem A.1.

(Maximize-out a variable by substitution) [11, 16] For a pseudo-Boolean
function $F:\mathbb{B}^{X}\to\mathbb{R}$ and a variable $x$. Then we have, for
all ${b}\in\mathbb{B}^{X\setminus\\{x\\}}$:

$\begin{split}\mathop{\max}\limits_{x}F({b})=F({b}\cup\operatorname*{arg\,max}_{x}F({b})))\end{split}$

Note that $F({b}\cup\operatorname*{arg\,max}_{x}F({b})))$ can be viewed as
substituting $x$ by $\operatorname*{arg\,max}_{x}F({b})$ in $F$.

Theorem A.1 looks similar with Proposition 4.6. In fact, Theorem A.1 is a
generalization of Proposition 4.6 to all assignments rather than just the
maximizer. One interesting property of Basic Algorithm in our case is, a
variable can be eliminated only by substitution without the sum operation
222Though the derivatives still need to be summed, as we will see later. The
derivatives are, however, with smaller size than the original ADD.. Therefore,
substituting $x$ by $\operatorname*{arg\,max}_{x}F$ can be done separately in
each individual ADDs. The pseudo-Boolean $\operatorname*{arg\,max}_{x}F$ is in
fact computed by $G_{x}$ in the algorithm (see Lemma C.5 and its proof in
below). Based on the above, we show a variant of Algorithm 2, namely Algorithm
4 below. Note that the valuation of each node in Algorithm 4 is no longer an
ADD as in Algorithm 2, but a set of ADDs, whose sum is equivalent with the
resulting ADD in Algorithm 2.

Algorithm 4 works as follows. By Proposition 4.7, the
$\operatorname*{arg\,max}$ operator can be implemented by the sgn of
derivative, i.e., $G_{x}$ in the algorithm. Since $F_{f}$ is an additive
objective function, its derivative $\nabla_{x}F$ can be computed by first
obtaining the derivatives for all additive components and then summing up
these derivatives (the $G_{x}$ in Algorithm 2 and 4 are equivalent).
Afterwards, Algorithm 4 substitutes $x$ by $G_{x}$ in all ADDs of sub-
valuations (Compose$(A,x,G_{x})$) and returns the set $A_{v}$.

Input : A project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$, a node $v\in
V(T)$, a stack $\mathcal{S}$ for constructing the maximizer.

Output : A set of ADDs, whose sum is equivalent to
$\mathcal{F}^{\mathcal{T}}_{v}$

1 if  _$v\in L(T)$ _ then return { compileADD$(\gamma(v))\\}$ // $v$ is a
leaf;

2 for  _$u\in\texttt{children}(v)$_ do

3 $A_{u}\leftarrow\texttt{computeValuation}(\mathcal{T},u,\mathcal{S})$

4

5for  _$x\in\pi(v)$_ do

6 $D\leftarrow\texttt{ZeroADD}$

7 for  _$u\in\texttt{children}(v)$_ do

8 for  _$A\in A_{u}$_ do

9 $D\leftarrow D+\nabla_{x}A$

10

11 $G_{x}\leftarrow\texttt{sgn}(D)$

12 $\mathcal{S}.\texttt{push}((x,G_{x}))$

13 for  _$u\in\texttt{children}(v)$_ do

14 for  _$A\in A_{u}$_ do

15 $A\leftarrow\texttt{Compose}(A,x,G_{x})$

16

return $\bigcup_{u\in\texttt{children(v)}}A_{u}$

Algorithm 4 computeValuation$(\mathcal{T},v,\mathcal{S})$ (By the Basic
Algorithm)

The original Basic Algorithm [11, 16] uses heuristics for deciding a variable
elimination order, instead of a project-join tree. Algorithm 4 can be viewed
as a combination of Basic Algorithm and the project-join-tree-based approach.
Note that Algorithm 4 does not compute the sum of ADDs from the sub-
valuations, though it does compute the sum of derivatives. Instead, it stores
the valuations by an additive decomposition, which is a set of ADDs.
Therefore, Algorithm 4 provides the potential of parallelizing the symbolic
approach.

We compare in practice, the efficiency of Algorithm 2 and 4 used in Algorithm
1 on a subset of benchmarks used in evaluation, which contains 100 relatively
small instances. We track in Table 6 the running time and the maximum number
of nodes in a valuation during the computation. 333In Algorithm 4, the number
of ADD nodes in a valuation is the sum of nodes in the additive decomposition.
According to the results, Algorithm 2 introduced in the main paper outperforms
Algorithm 4 based on Basic Algorithm. On average, Algorithm 2 uses about $1/3$
of the running time and $1/18$ the number of nodes compared with Algorithm 4.
Therefore, the additive decomposition used in Algorithm 4 is generally less
efficient.

Algorithm |  |  Alg. 2 |  |  Alg. 4 (Basic Algorithm)
---|---|---|---|---
Avg. Running Time (s) |  | 1.94 |  | 7.53
Avg. Maximum # Nodes |  | 52450 |  | 497642
Avg. Speed-up ($\times$) compared with Alg. 4 |  | 3.4 |  | 1
Avg. Reduction ($\times$) of Maximum # Nodes compared with Alg. 4 |  | 18.4 |  | 1
Table 6: Comparison between Algorithm 2 and Algorithm 4. On average, Algorithm
2 uses about $1/3$ of the running time and $1/18$ the number of nodes compared
with Algorithm 4. Therefore, the additive decomposition used in Algorithm 4 is
generally less efficient.

##  Appendix B Different Implementations of $\max$ on ADDs

Although the performance of Algorithm 4 is generally worse than Algorithm 2,
the idea of maximization by substitution (composition) provides an alternative
way of implementing $max$, i.e.,

$\max_{x}F\equiv F_{|x\leftarrow G_{x}}\equiv
F_{|x\leftarrow\operatorname*{arg\,max}_{x}F}.$ (B.1)

Instead, the $\max$ in Algorithm 2 is done by

$\max_{x}F\equiv\max\\{F_{|x\leftarrow 1},F_{|x\leftarrow 0}\\},$ (B.2)

where computing $G_{x}$ is not needed.

Generally, $\max$ by Equation (B.2) is faster than Equation (B.1), if a
maximizer is not needed (computing the maximizer require the computation of
$G_{x}$ for each variable $x$). However, when generating a maximize is
necessary, then $G_{x}$ can be used in both variable elimination in Equation
(B.1) and maximizer generation, which makes Equation (B.1) more efficient than
Equation (B.2) for implementing $\max$. Therefore, in the implementation of
DPMS, we use Equation (B.2) to implement $\max$ when a maximizer is not needed
for better efficiency, and use Equation (B.1) otherwise.

##  Appendix C Technical Proofs

###  C.1 Proof of Proposition 4.1

Since $\nabla_{x}G\equiv 0$, we have $G(b\cup\\{x\\})=G(b)$ for all
$b\in\mathbb{B}^{n}$.

Therefore, for all $b\in\mathbb{B}^{X}$, we have

$\displaystyle\mathop{\max}_{x}(F+G)(b)$ $\displaystyle=$ $\displaystyle
max\\{F(b\cup\\{x\\})+G(b\cup\\{x\\}),F(b)+G(b)\\}$ $\displaystyle=$
$\displaystyle max\\{F(b\cup\\{x\\}),F(b)\\}+G(b)$ $\displaystyle=$
$\displaystyle\mathop{\max}_{x}F(b)+G(b)$

Thus we have $\mathop{\max}\limits_{x}(F+G)\equiv\mathop{\max}\limits_{x}F+G$.
∎

###  C.2 Proof of Theorem 4.4

######  Proof Sketch.

This proof is an adaption of the proof of Theorem 2 in [21]. The idea is to
figure out the non-recursive interpretation of the valuation
$\mathcal{F}_{v}^{\mathcal{T}}$ (Lemma C.3) from the recursive definition of
valuation. Structural induction on the project-join tree is frequently used in
the proof.

First, we define some useful notations:

Given a project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$ and a node $v$,
denote by $T(v)$ the subtree rooted at $v$. We define the set $\Phi(v)$ of
constraint that correspond to the leaves of $T(v)$:

$\displaystyle\Phi(v)\equiv\begin{cases}\\{\gamma(v)\\}&\text{if $v\in
L(T)$}\\\
\bigcup_{u\in\texttt{children}(v)}\Phi(u)&\text{otherwise}\end{cases}$

We also define the set $P(v)$ of all variables to project in the subtree
$T(v)$:

$\displaystyle P(v)\equiv\begin{cases}\emptyset&\text{if $v\in L(T)$}\\\
\bigcup_{u\in\texttt{children}(v)}P(u)\cup\pi(v)&\text{otherwise}\end{cases}$

Note that for the root $r$, we have $\Phi(r)=C_{f}$ and $P(r)=X$. The
following two lemmas will be used later.

######  Lemma C.1.

For a tree $T$ and an internal node $v$, let $u_{1},u_{2}$ be two distinct
children of $v$. Then we have

$P(u_{1})\cap P(u_{2})=\emptyset$

######  Proof.

First node that the subtree with root $u_{1}$ and the subtree with root
$u_{2}$ do not share nodes. In other words, we have

$V(T(u_{1}))\cap V(T(u_{2}))=\emptyset$

This is true because otherwise we will have a loop in a tree, which is
impossible.

Assume $P(u_{1})\cap P(u_{2})\neq\emptyset$ and there exists $x\in
P(u_{1})\cap P(u_{2})$. Then by the definition of $P$, there exist two
distinct internal nodes $o_{1}\in V(T(u_{1}))$ and $o_{2}\in V(T(u_{2}))$,
such that $x\in\pi(o_{1})$ and $x\in\pi(o_{2})$. However, this contradicts
with the property of the project-join tree: $\\{\pi(v):v\in V(T)\setminus
L(T)\\}$ is a partition of the variable set $X$. ∎

######  Lemma C.2.

For a tree $T$ and an internal node $v$, let $u_{1},u_{2}$ be two distinct
children of $v$. Then we have

$\Phi(u_{1})\cap\Phi(u_{2})=\emptyset.$

######  Proof.

Suppose there exists $c\in\Phi(u_{1})\cap\Phi(u_{2})$, then by the definition
of $\Phi$, the leaf node corresponding to $c$, i.e., $\gamma^{-1}(c)$ must be
a descendant of both $u_{1}$ and $u_{2}$, which conflicts with the fact that
$V(T(u_{1}))\cap V(T(u_{2}))=\emptyset,$ proved in the proof of Lemma C.1. ∎

Then, in order to prove Theorem 4.4, we first propose and prove the following
invariant Lemma.

######  Lemma C.3.

After all valuations are computed, we have for each node $v\in V(T)$,

$\mathcal{F}_{v}^{\mathcal{T}}\equiv\mathop{\max}\limits_{P(v)}\sum_{c\in\Phi(v)}c$

######  Proof.

We prove Lemma C.3 by structural induction.

For the basis case, $v\in L(T)$, we have $\Phi(v)=\gamma(v)$ and
$P(v)=\emptyset$. By Definition 4.3,

$\mathcal{F}_{v}^{\mathcal{T}}=\gamma(v)=\mathop{\max}\limits_{P(v)}\sum_{c\in\Phi(v)}c$

trivially holds.

For the inductive step, i.e., $v\in V(T)\setminus L(T)$.

By induction hypothesis, for all $u\in\texttt{children}(v)$, we have

$\mathcal{F}_{u}^{\mathcal{T}}\equiv\mathop{\max}\limits_{P(u)}\sum_{c\in\Phi(u)}c$

Then

$\displaystyle\mathcal{F}_{v}^{\mathcal{T}}$ $\displaystyle\equiv$
$\displaystyle\mathop{\max}\limits_{\pi(v)}\sum\limits_{u\in\texttt{children}(v)}\mathcal{F}_{u}^{\mathcal{T}}\text{\,\,\,\,\,\,\,(Definition
\ref{defn:valuation})}$ $\displaystyle\equiv$
$\displaystyle\mathop{\max}\limits_{\pi(v)}\sum\limits_{u\in\texttt{children}(v)}\mathop{\max}\limits_{P(u)}\sum_{c\in\Phi(u)}c\text{\,\,\,\,\,\,\,(inducton
hypothesis)}$ $\displaystyle\equiv$
$\displaystyle\mathop{\max}\limits_{P(v)}\sum\limits_{u\in\texttt{children}(v)}\sum_{c\in\Phi(u)}c\text{\,\,\,\,\,\,\,(by
Lemma \ref{lemma:Ppartition} and undoing early maximization multiple times)}$
$\displaystyle\equiv$
$\displaystyle\mathop{\max}\limits_{P(v)}\sum_{c\in\Phi(v)}c\text{\,\,\,\,\,\,\,(Lemma
\ref{lemma:Phipartition} )}$

∎

Now we are ready to prove Theorem 4.4. For the root $r$ of the project-join
tree, we have

$\displaystyle\mathcal{F}_{r}^{\mathcal{T}}=\mathop{\max}\limits_{P(r)}\sum_{c\in\Phi(r)}c=\mathop{\max}\limits_{X}\sum_{c\in
C_{f}}c=\mathop{\max}\limits_{X}F_{f}$

∎

###  C.3 Proof of Proposition 4.6

$\displaystyle F(\\{\operatorname*{arg\,max}_{x}F(b^{\star})\\}\cup
b^{\star})$ $\displaystyle=$
$\displaystyle\max\\{F(b^{\star}\cup\\{x\\}),F(b^{\star})\\}$ $\displaystyle=$
$\displaystyle\max_{x}F(b^{\star})$ $\displaystyle=$
$\displaystyle\max_{X\setminus\\{x\\}}\max_{x}F$ $\displaystyle=$
$\displaystyle\max_{X}F$

###  C.4 Proof of Proposition 4.7

This proposition can be easily proved by observing that $F({b}\cup\\{x\\})\geq
F({b})$ is equivalent with $\nabla_{x}F(b)\geq 0$ by Definition 3.3 and 3.4. ∎

###  C.5 Proof of Theorem 4.8

######  Proof Sketch.

The proof keeps track of the “active" ADDs during the computation. To do this,
we slightly change Algorithm 2 to have a set $Q$ to contain “active" ADDs.
Then we show that, suppose at a moment variables in $S$ have been eliminated,
the sum of currently active ADDs equals the pseudo-Boolean function
$max_{S}F_{f}$. As a result, the $G_{x}$ computed in Algorithm 2 is the
$\operatorname*{arg\,max}_{x}$ of $max_{S}F_{f}$, which is what we need to
extend a maximizer by appending the value of $x$. When the last variable
$x_{l}$ is eliminated, $G_{x_{l}}$ will be a length-$1$ maximizer containing
the value of $x_{l}$. In Algorithm 3, a maximizer is iteratively built from
length-$1$ to length-$|X|$ by the reverse order of variable, which is enforced
by the stack $\mathcal{S}$. For example, $x_{l}$ will be the first variable
popped in Algorithm 3.

For a formula $f$, recall the objective function is defined as

$F_{f}({b})=\sum_{c\in C_{f}}{c({b})},$

for all $b\in\mathbb{B}^{X}$.

Input : A project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$, a node $v\in
V(T)$, a stack $\mathcal{S}$ for constructing the maximizer.

Output : An ADD representing of the valuation of $v$, i.e.,
$\mathcal{F}^{\mathcal{T}}_{v}$

1 if  _$v\in L(T)$ _ then return $\texttt{compileADD}(\gamma(v))$;

2 $A\leftarrow\texttt{ZeroADD}$

3 for  _$u\in\texttt{children}(v)$_ do

4 $A^{\prime}=\texttt{computeValuation}(\mathcal{T},u,\mathcal{S})$

5 $Q.remove(A^{\prime})$

6 $A\leftarrow A+A^{\prime}$

7

8$Q.insert(A)$

9 for  _$x\in\pi(v)$_ do

10 /* For maximizer generation */

11 $G_{x}\leftarrow\texttt{sgn}(\nabla_{x}A)$

12 $\mathcal{S}$.push$((x,G_{x}))$

13 /* Eliminate $x$ */

14 $Q.remove(A)$

15 $A\leftarrow\mathop{\max}_{x}A$

16 $Q.insert(A)$

17

return $A$

Algorithm 5 computeValuation $(\mathcal{T},v,\mathcal{S})$ (modified, for
proof of Lemma C.4 )

In order to complete this proof, we slightly modified Algorithm 2 to Algorithm
5. Compared with Algorithm 2, Algorithm 5 uses a set $Q$ of ADDs to keep track
of the “active" valuations. Initially, $Q$ is the set of the ADDs of all
constraints. Despite of the set $Q$, Algorithm 5 computes the same valuation
with Algorithm 2. During the execution of Algorithm 5, we have the following
lemma, saying that the sum of ADDs in $Q$ is the ADD representation of the
pseudo-Boolean function $\max_{S}F_{f}$, where $S$ is the set of variables
that already have been eliminated.

######  Lemma C.4.

In Algorithm 5, before Line 5, a variable-ADD pair $(x,G_{x})$ is pushed into
the stack $\mathcal{S}$, suppose the variable-ADD pairs for variables in $S$
($S\subseteq X$ and $x\not\in S$) have been pushed into the stack
$\mathcal{S}$, then we have

$\sum_{D\in Q}D=\max_{S}F_{f}.$

######  Proof.

We prove by induction with the order of variable elimination.

Basis case: Before the first variable is pushed, $\sum_{A\in Q}=\sum_{c\in
C_{f}}=F_{f}$ by initialization of $Q$.

For the inductive step, suppose in the iteration where $x$ will be eliminated,
while the previous variable eliminated is $x^{\prime}$. By induction
hypothesis, before $x^{\prime}$ is eliminated, we have

$\sum_{D\in Q}D=max_{S\setminus\\{x\\}}F_{f}$

Between the moment before executing Line 5 in the iteration of $x^{\prime}$
and Line 5 in the iteration of $x$, the set $Q$ may be changed by:

  1. 1.

Line 5 and 5 in the iteration of $x^{\prime}$, where $A$ is replaced by
$max_{x^{\prime}}A$ in $Q$. Since $A$ is the only ADD in $Q$ that contains
$x$, after the replacement, we have

$\sum_{D\in Q}D=max_{S}F_{f}.$

  2. 2.

Line 5 and 5 in Algorithm 5, where several ADDs in $Q$ is replaced by their
sum (note that when an ADD is removed from $Q$, it must have been inserted
into $Q$ Line 5 in the recursive call to computeValuation). However, this
operation does not change the pseudo-Boolean function $\sum_{D\in Q}D$.

Therefore before $x$ is eliminated, we have $\sum_{D\in Q}D=max_{S}F_{f}.$ ∎

We first prove the following loop invariants regarding Algorithm 2 and 3.

######  Lemma C.5.

In Algorithm 2, after Line 2 is executed, i.e., $G_{x}$ is computed, suppose
the variable-ADD pairs for variables in $S$ ($S\subseteq X$ and $x\not\in S$)
have been pushed into the stack $\mathcal{S}$, then we have

$G_{x}=\operatorname*{arg\,max}_{x}(\max_{S}F_{f}).$

######  Proof.

Note that $G_{x}$ in Algorithm 2 and 5 is equivalent. Therefore, we prove the
result for Algorithm 5 and it also holds for Algorithm 2.

According to Lemma C.4, we know that before Line 5 of Algorithm 5, the
following holds:

$\sum_{D\in Q}D=max_{S}F_{f}$

Since $\mathcal{T}$ is a project-join tree and $x$ will be eliminated in this
iteration, $A$ is the only ADD in $Q$ that contains $x$. Therefore

$G_{x}=\texttt{sgn}(\nabla_{x}A)=\texttt{sgn}(\nabla_{x}\max_{S}F_{f})$

By Proposition 4.7, $G_{x}$ is the ADD representation of
$\operatorname*{arg\,max}_{x}(max_{S}F_{f})$. ∎

######  Lemma C.6.

When a variable-ADD pair $(x,G_{x})$ is popped in Algorithm 3, suppose the
variable-ADD pairs for variables in $S$ ($S\subseteq X$ and $x\not\in S$) are
still in the stack $\mathcal{S}$, then after the execution of Line 3 of
Algorithm 3, we have $b^{\star}$ is a maximizer of $\max_{S}F_{f}$.

######  Proof.

We prove by induction on the loop of Algorithm 3.

Basis case: Before entering the loop, $b^{\star}=\emptyset$ and $S=X$. The
$b^{\star}$, i.e., the empty set is a trivial maximizer of the scalar
$max_{X}F_{f}$.

Inductive step: Consider the iteration where $(x,G_{x})$ is popped. By
inductive hypothesis, the $b^{\star}$ before Line 3 is a maximizer of
$max_{S\cup\\{x\\}}F_{f}=max_{x}max_{S}F_{f}$. After $(x,G_{x})$ is popped, by
Lemma C.5, we have $G_{x}=\operatorname*{arg\,max}_{x}(\max_{S}F_{f})$. By
Proposition 4.6, we have $b^{\star}\cup
G_{x}(b^{\star})=b^{\star}\cup\\{\operatorname*{arg\,max}_{x}(\max_{S}F_{f})(b^{\star})\\}$
is a maximizer of $max_{S}F_{f}$. ∎

Now we are able to prove Theorem 4.6. Given Lemma C.6, Theorem 4.6 directly
follows by consider the last variable popped from the stack: $S=\emptyset$ and
$b^{\star}$ is a maximizer of $F_{f}$. ∎

###  C.6 Proof of Theorem 4.9

######  Proof Sketch.

We first formally define the width of a (graded) project-join tree and the
size of a formula. Then we analyze each operation of Algorithm 1 and prove
again by structural induction that the running time of all three types of
operations is bounded by $O(k\cdot 2^{k}\cdot|f|)$.

To prove this theorem, we first define the $width$ of a (graded) project-join
tree formally. For each constraint $c\in C(f)$, define Vars$(c)$ to be the set
of variables appearing in $c$.

For each node $v\in V(T)$, $\texttt{Vars}(v)$ is defined as follows:

$\displaystyle\texttt{Vars}(v)\equiv\begin{cases}\texttt{Vars}(\gamma(v))&\text{if
$v\in L(T)$}\\\
\big{(}\bigcup_{u\in\texttt{children}(v)}\texttt{Vars}(u)\big{)}\setminus\pi(v)&\text{otherwise}\end{cases}$

The size of a node $v$, $size(v)$ is defined to be $|\texttt{Vars}(v)|$ if $v$
is a leaf, and $|\texttt{Vars}(v)\cup\pi(v)|$ if $v$ is an internal node.

The _width_ of a (graded) project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$,
denoted by $width(\mathcal{T})$, is defined as

$width(\mathcal{T})\equiv\max_{v\in V(T)}size(v).$

For a node $v$ in the project-join tree, we define the sub-formula associated
with $v$, denoted by $f_{v}$ as follows:

$\displaystyle f(v)\equiv\begin{cases}\gamma(v)&\text{if $v\in L(T)$}\\\
\bigwedge_{u\in\texttt{children}(v)}f_{u}&\text{otherwise}\end{cases}$

For a conjunctive formula $f$, we define the size of $f$, denoted by $|f|$, by
the sum of the number of variables in all constraints.

We prove the following statement by structural induction:

######  Lemma C.7.

For a (graded) project-join tree $\mathcal{T}=(T,r,\gamma,\pi)$ and a node
$v\in V(T)$, if $width(\mathcal{T})\leq k$, then
computeValuation$(\mathcal{T},v,\mathcal{S})$ terminates in
$O(k2^{k}|f_{u}|)$.

######  Proof.

We prove this lemma by structural induction.

For the basis case, $v\in L(T)$, we have $f_{v}=$compileADD$(\gamma(v))$ and
the running time of computeValuation is that of
$\texttt{compileADD}(\gamma(v))$. Since $width(\mathcal{T})\leq k$, we know
that $\gamma(v)$ has at most $k$ variables. Assume that given an assignment,
the value of a constraint can be determined in $O(|\gamma(v)|)$, which is true
for most types of constraints. Then $\texttt{compileADD}(\gamma(v))$ can be
done in $O(k\cdot 2^{k}\cdot|f_{v}|)$ by simply building the binary decision
tree $(O(2^{k}\cdot|f_{v}|))$ and reduce it ($O(k\cdot 2^{k})$).

For the inductive step, i.e., $v\in V(T)\setminus L(T)$.

By induction hypothesis, for all $u\in\texttt{children}(v)$, we have
computeValuation$(\mathcal{T},u,\mathcal{S})$ terminates in
$O(k2^{k}|f_{u}|)$.

Next we analyze the computation done in Algorithm 2. The overall observation
is that the number of variables in the ADD $A$ during the execution of the
algorithm is always bounded by $k$, given $width(\mathcal{T})\leq k$.
Therefore the size of an intermediate (reduced, ordered) ADD is always bounded
by $O(2^{k})$.

  1. 1.

Line 2 calls computeValuation on all children of $v$. By the induction
hypothesis, the total time is bounded by

$\sum_{u\in\texttt{children}(v)}O(k2^{k}|f_{u}|)=O(k2^{k}|f_{v}|)$

Note that $|f_{v}|=\sum_{u\in\texttt{children}(v)}|f_{u}|$ by Lemma C.2.

  2. 2.

Line 2 also sums up all intermediate ADDs provided by its children. Since the
$width$ of $\mathcal{T}$ is bounded by $k$, the number of variables of two
ADDs for summing are at most $k$. Thus sum can be done in $O(k\cdot 2^{k})$ by
simply enumerating all possible $2^{k}$ assignments, building a Boolean
decision tree and reduce it. Therefore, the total time is bounded by
$O(|\texttt{children}(v)|\cdot k\cdot 2^{k})$. Note that
$|\texttt{children}(v)|=\sum_{u\in\texttt{children}(v)}1\leq\sum_{u\in\texttt{children}(v)}|f_{u}|=|f_{v}|$.
Thus the total time is also bounded by $O(k\cdot 2^{k}|f_{v}|)$.

  3. 3.

Line 2 and 2 push $\texttt{sgn}(\nabla_{x}A)$ to the stack for generating the
maximizer. The complexity of computing $\nabla_{x}A$ and sgn$(\nabla_{x}A)$
are both $O(k\cdot 2^{k})$. Since variables in $\pi(v)$ are eliminated, the
total time is bounded by $O(|\pi(v)|\cdot k\cdot 2^{k})$. We have

$|\pi(v)|\leq\big{|}\bigcup_{u\in\texttt{children}(v)}\texttt{Vars}(f_{u})\big{|}\leq\sum_{u\in\texttt{children}(v)}|\texttt{Vars}(f_{u})|\leq\sum_{u\in\texttt{children}(v)}|f_{u}|=|f_{v}|.$

Thus the total time is also bounded by $O(k\cdot 2^{k}|f_{v}|)$.

Hence, the total time of $1$-$3$ above is still bounded by $O(k\cdot
2^{k}\cdot|f_{v}|)$. ∎

We are ready to complete the proof of Theorem 4.9. By Lemma 2,
computeValuation$(\mathcal{T},r,\mathcal{S})$ terminates in

$O(k\cdot 2^{k}|f_{r}|)=k\cdot 2^{k}|f|$

.

Finally, the running time of Algorithm 3 for building the maximizer is bounded
by $O(n\cdot k)=O(|f|\cdot k)$.

Therefore, the total running time of Algorithm 1 is bounded by $O(k\cdot
2^{k}\cdot|f|)$. ∎