Maximum Satisfiability Formulations for
Nonlinear Integer Programming

Zhifei Zheng[0000-0003-4061-7518], Sami Cherif[0000-0003-4646-9982]*, Rui Sá
Shibasaki[0000-0002-5561-4937], Chu-Min Li[0000-0002-6886-8434], and Jialu
Zhang[0009-0009-6184-4649]

Laboratoire MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
{zhifei.zheng,sami.cherif,rui.sa.shibasaki,chu-min.li,jialu.zhang}@u-picardie.fr

**Abstract.** This paper introduces novel Maximum Satisfiability (MaxSAT) formulations for the Nonlinear Integer Programming (NLIP) problems with discrete polynomial functions. We develop a generic framework based on three established integer encoding techniques from the literature. Our approach treats each polynomial term as an atomic unit and demonstrates how it can be efficiently encoded through compact representations of integer assignments. Additionally, we present two distinct decomposition methods based on the degrees of polynomial terms. This work lays a foundation for future research and has the potential to extend the applicability of modern MaxSAT solvers to a wider range of optimization problems.

# 1 Introduction

Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) are powerful formalisms with strong expressive ability under propositional logic. Given a propositional formula in Conjunctive Normal Form (CNF), SAT consists in deciding whether it is satisfiable [5]. MaxSAT is a natural optimization extension of SAT, in which the goal shifts to finding an assignment that maximizes the number of satisfied clausal constraints in the given formula (MinSAT is another optimization extension of SAT [22]). MaxSAT methodologies have been applied to solve problems in various domains, including hardware and software verification [15,28], planning and scheduling [7,30] and bio-informatics [13,14]. Empowered by pseudo-Boolean constraints, MaxSAT has been successfully applied to integer linear problems (ILP). However, existing literature has not extensively explored the capacity of MaxSAT to solve nonlinear integer programming problems (NLIP).

Like ILP, the NLIP problems are also frequently encountered in multiple domains, such as portfolio management, transportation, and network design [10, 17, 26]. These problems are usually difficult to solve, due to the integer variables and the nonlinearity of constraints. In this sense, here we propose an encoding scheme for modeling NILP problems as MaxSAT instances, so that state-of-art MaxSAT solvers can serve as an alternative approach to solve such problems.

<footnote>* Corresponding author</footnote>
In this paper, we particularly focus on NLIP problems with polynomial func-
tions, i.e., exponential, logarithmic and other non-polynomial functions are not
considered. Furthermore, we assume that the integer variables are bounded by
an integer constant. It is worth noting that, even considering these assumptions
the problem is already challenging, as shown by previous work in the literature.
Indeed, in [24], it was proven that the optimization of a degree-4 polynomial
function constrained to the set of integer lattice points of a convex polygon is
NP-hard. Additionally, it was shown in [18] that, if the variables are not bounded,
integer programming with quadratic constraints is *undecidable*, i.e., there cannot
exist a general algorithm to solve every instance of the problem.

Furthermore, in the literature, several works have proposed methods for
transforming pseudo-Boolean constraints into clauses, e.g., [1, 11, 25]. More re-
lated to our work, in [2], the authors discuss how to transform linear problems
with finite domains into equivalent SAT problems, and propose six different map-
ping methods. However, they do not consider the nonlinear case. Meanwhile, the
nonlinear situations are also of interest to the community of Satisfiability Mod-
ulo Theories (SMT). Classical nonlinear integer arithmetic (NIA) problems are
handled on a higher abstraction level, usually by simplifying problems into linear
forms, then conducting typical bit-blasting into CNF [8, 20]. To the best of our
knowledge, there is no work presenting an end-to-end formulation from Nonlin-
ear polynomial integer programming directly to MaxSAT. It is also worth noting
that, as pointed out in [27], the pseudo-Boolean field has not been as developed
as the satisfiability field, which is the reason why we develop our work through
the lens of MaxSAT.

The contribution of this paper is twofold. First, an encoding of high-order
nonlinear polynomial terms is formally described. Second, we propose a complete
encoding of polynomial NLIP problems to MaxSAT formulations. The encoding
of polynomial terms is based on well-known integer representations in the litera-
ture, namely the one-hot, unary, and binary representations. We first discuss how
these representations can be generalized to encode nonlinear terms, then study
the complexities of our models in terms of the number of variables and clauses
derived for such formulations. A complete MaxSAT formulation for NILP can al-
ready be obtained by the conjunction of clauses encoding each term individually.
Finally, we propose decomposition strategies that can reduce the complexity of
the final MaxSAT formulation in terms of the number of variables and clauses.

The remainder of this paper is organized as follows. Section 2 introduces the
fundamental definitions and notations of MaxSAT and NLIP. It also discusses
related work and proposes the generic framework for transforming NLIP into
MaxSAT formulations. Section 3 takes each polynomial term as an atomic unit,
using the three different representations to encode any given polynomial term.
Section 4 takes one step forward and decomposes the degree of the given poly-
nomial terms, therefore decreasing the complexity of the encodings. Finally, we
conclude and discuss future work in Section 5.
# 2 Preliminaries

## 2.1 Maximum Satisfiability

In this paper, we consider the most generic variant of MaxSAT, namely Weighted Partial MaxSAT [3,21]. This problem takes as input a bipartite weighted formula $\phi = H \cup S$, where $H$ is the set of hard clauses that must be satisfied as in SAT, and $S$ is the set of soft clauses, in which each clause $C$ is associated with an integer weight $C$. The objective of Weighted Partial MaxSAT is to obtain an assignment $\alpha$ that maximizes (resp. minimizes) the sum of the weight of satisfied (resp. falsified) soft clauses while satisfying all the hard clauses. Formally, let $cost_{\alpha}(\phi)$ denote the sum of weights of soft clauses in $\phi$ falsified by the assignment $\alpha$, Weighted Partial MaxSAT thus seeks for $\textit{optimum}(\phi) = \min_{\alpha} cost_{\alpha}(\phi)$.

In the following sections, we simply use MaxSAT to refer to the most generic version defined above. Note that in classical MaxSAT, weights are positive integers. However, within this paper, we allow the weight to be negative, since a negative weight can always be normalized to a positive one. In the remainder of this paper, we use $SatW_{\alpha}(\phi)$ to denote the sum of weights of clauses in $\phi$ satisfied by $\alpha$, which can be abbreviated as $SatW(\phi)$ when the context is clear. Additionally, we mention that previous literature introduces Pseudo-Boolean (PB) constraints [27], which can be formalized as $\sum_j w_j \cdot l_j \succ c$, where $w_j \in \mathbb{N}, c \in \mathbb{N}, l_j$ is a literal and $\succ \in \{=, >, \ge, <, \le\}$. When all the coefficients of literals are equal to one and can thus be omitted, we refer to such forms more commonly as cardinality constraints.

## 2.2 Nonlinear Integer Programming

In this section, we formally define NLIP and introduce the terminologies that will be used throughout this paper. Here, we consider the case where integer variables are bounded, i.e., the domain of variables is $V = \{0, 1, ..., ub\}$. Additionally, coefficients are also restricted to be integers, and the objective function and constraints are restricted to be polynomials.

**Definition 1 (Polynomial Term and High-order Term).** A term $T(X)$ of variables $X = (X_1, ..., X_n)$ is called a polynomial term if it can be written as: $T(X) = c \cdot \prod_{q \in Q} X_q^{k_q}$, where $c \in \mathbb{Z}, k_q \in \mathbb{N}, \forall q \in Q$ and $Q \subseteq \{1, ..., n\}$.

We refer to a term with only one variable (e.g., $X_1^2$) as a *pure term*, and a term with different variables (e.g., $X_1X_2$) as a *cross term*. We call $k = \sum_{q \in Q} k_q$ the order of $T(X)$. In particular, when $k \ge 2$, we refer to this term as a *high-order term*. If the context is clear, we abbreviate $T(X)$ as $T$. Using this notation, we can now formalize discrete nonlinear polynomial functions as follows:

**Definition 2 (Nonlinear Polynomial Function).** A discrete polynomial function $P(X)$ is nonlinear if it contains at least one high-order term.
**Definition 3 (Nonlinear Integer Programming).** A NLIP model with *n* integer variables and *l* constraints can be formalized as the following form [16,23]:

$$
\begin{array}{ll}
\max & f(\mathbf{X}) \hfill \text{(NLIP)} \\
\text{s.t.} & g_i(\mathbf{X}) \le b_i \quad i = 1, \dots, l \quad ; \mathbf{X} \in \mathbb{X}, \mathbb{X} \subseteq \{0, \dots, ub\}^n
\end{array}
$$

where *f* and all *g*<sub>*i*</sub> functions are polynomials and at least one of them is nonlinear,
and *ub* is a global upper bound of all variables.

2.3 Integer Encodings with MaxSAT

In this subsection, we introduce Boolean-variable-based representations of inte-
gers. Given a bounded natural integer variable $X \in \mathbb{N}$ such that $X \le ub$, where
$ub$ is a constant upper bound, a series of Boolean variables $x_i$ are used to repre-
sent $X$, with the following well-known methods: one-hot representation [12,19],
unary representation [4,6], and binary representation [11,31]. Note that one-hot,
unary, and binary representations correspond to Standard mapping (S), Full
regular mapping (FR), and Full logarithmic mapping (FL) in [2], respectively.

Given a natural number $X \le ub$, the one-hot representation and the unary
representation both use $ub + 1$ Boolean variables to represent $X$. In a one-hot
formulation, the bit with the index corresponding to the value of $X$ is assigned
to 1, and the other bits are assigned to 0. In the unary representation, the bits
with indexes smaller than or equal to the value of $X$ are assigned to 1, and
the other bits are assigned to 0. Note that, since $X \in \mathbb{N}$, 0 is an implicit lower
bound for $X$, $x_0$ is therefore fixed to 1 in the unary representation. On the other
hand, the binary representation uses $\lfloor \log_2 ub \rfloor + 1$ Boolean variables to represent
$X$. The bits that are true in the binary encoding of $X$ are assigned to 1, and
the other bits are assigned to 0. In this context, when representing the integer
variable $X_q \in \mathbf{X}$ ($q \in \{1, 2, \dots, n\}$), we denote the used Boolean variables as $x_r^{(q)}$,
where $r$ is the index of the encoding variables. We summarize the notations and
indexes used within this paper in Table 1. Hereafter, log denotes the logarithm
with base 2.

Based on the integer representations, we can transform the NLIP formula-
tion into a MaxSAT formulation. The objective function of NLIP is modeled as

<table><caption>Table 1: Summary of Notations</caption>
  <thead>
    <tr>
      <th colspan="2">Notation Description</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td rowspan="4">Sets and Numbers</td>
      <td>&#x2110;</td>
      <td>The set of natural numbers: {0, 1, 2, ...}</td>
    </tr>
    <tr>
      <td>&#x211B;</td>
      <td>The set of integer numbers: {... , -2, -1, 0, 1, 2, ...}</td>
    </tr>
    <tr>
      <td>ub</td>
      <td>The upper bound for all original integer variables</td>
    </tr>
    <tr>
      <td>V<sub>c</sub></td>
      <td>The value set V<sub>c</sub> = {0, 1, ..., |c|}, where c is a given constant</td>
    </tr>
    <tr>
      <td rowspan="5">Variables and Functions</td>
      <td>X</td>
      <td>An integer variable, where X &le; ub</td>
    </tr>
    <tr>
      <td>X&#x2080;</td>
      <td>A vector with all its components as integers</td>
    </tr>
    <tr>
      <td>T(X&#x2080;)</td>
      <td>A polynomial term on X&#x2080; (abbreviated as T&#x2080;)</td>
    </tr>
    <tr>
      <td>P(X&#x2080;)</td>
      <td>A nonlinear polynomial function on X&#x2080;</td>
    </tr>
    <tr>
      <td>x<sub>r</sub><sup>(q)</sup></td>
      <td>Boolean variables encoding X<sub>q</sub></td>
    </tr>
    <tr>
      <td rowspan="2">Indices</td>
      <td>q</td>
      <td>Index for the integer variables in a term</td>
    </tr>
    <tr>
      <td>r</td>
      <td>Index for Boolean variables encoding an integer variable</td>
    </tr>
  </tbody>
</table>
weighted soft clauses, and the NLIP constraints are modeled as hard clauses. Regarding the objective function, if all soft clauses are unit clauses with only one literal (which can always be ensured by replacing all non-unit clauses with literals and adding hard constraints to ensure the relation), each of them can be regarded as one term in the objective function, with their weights as the coefficients. Given an NLIP instance, a MaxSAT formulation is obtained by transforming the objective and constraints from functions to clauses. Indeed, in the next section, we show how this can be done by using integer encodings to represent any given polynomial term.

# 3 Atomic Formulations for Nonlinear Terms

Without loss of generality, we focus on the formulation of a polynomial term, with $m$ variables and the order of $k$, appearing in the objective function, formalized as $T(\mathbf{X}) = c \cdot \prod_{q=1}^{m} X_{q}^{k_q}$, where $\sum_{q=1}^{m} k_q = k$. All variables $X$ in the discussion are bounded within the finite set $V_{ub} = \{0, \dots, ub\}$. Although we develop the idea from the perspective of objective functions, the same procedure can be applied to transformations of constraint functions. Consequently, transforming the entire NILP reduces to encoding each polynomial term that appears in it. The one-hot, unary, and binary formulations are subsequently given in the following subsections 3.1, 3.2, and 3.3.

## 3.1 One-hot Formulation

Given a polynomial term $T$, the one-hot formulation ensures a direct mapping between each possible value of the term and its corresponding encoding. Considering the one-hot encoding of integer variables $X_q$, we have that $X_q = \sum_{r_q=0}^{ub} r_q \cdot x_{r_q}^{(q)}$, and therefore the product of $m$ integer variables produces the product of $m$ encoding variables $x$ for each possible permutation of values in $V_{ub}$, corresponding to the auxiliary variables $z_{r_1 \dots r_m}$. We present below the MaxSAT formulation (OH) for the polynomial term in the objective function, and we prove its soundness in Theorem 1.

### Soft Clauses

$$ (z_{r_1 \dots r_m}, c \cdot \prod_{q=1}^{m} r_q^{k_q}) \quad \forall (r_1, \dots, r_m) \in V_{ub}^m : c \cdot \prod_{q=1}^{m} r_q^{k_q} \neq 0 \quad (\text{OH-S}) $$

### Hard Clauses

$$ \bar{z}_{r_1 \dots r_m} \lor x_{r_q}^{(q)} \quad \forall q \in \{1, \dots, m\}, \forall (r_1, \dots, r_m) \in V_{ub}^m \quad (\text{OH-H1}) $$

$$ (\bigvee_{q=1}^{m} \bar{x}_{r_q}^{(q)}) \lor z_{r_1 \dots r_m} \quad \forall (r_1, \dots, r_m) \in V_{ub}^m \quad (\text{OH-H2}) $$

$$ \bigvee_{r \in V_{ub}} x_r^{(q)} \quad \forall q \in \{1, \dots, m\} \quad (\text{OH-H3}) $$

$$ \bar{x}_r^{(q)} \lor \bar{x}_{r'}^{(q)} \quad \forall q \in \{1, \dots, m\}, \forall (r, r') \in V_{ub}^2 : r < r' \quad (\text{OH-H4}) $$

OH uses the hard clauses OH-H1 to OH-H4 to construct the auxiliary structure supporting the direct mapping of fixed point values of the polynomial term.
The formulation first introduces a new series of auxiliary variables $z_{r_1...r_m}$ for any possible assignment $(r_1, ..., r_m) \in V_{ub}^m$. Equation OH-H1 together with OH-H2 is equivalent to $z_{r_1...r_m} \leftrightarrow \bigwedge_{q=1}^m x_{r_q}^{(q)} \quad \forall (r_1, ..., r_m) \in V_{ub}^m$. They link auxiliary variables $z$ with the original indicator variables $x$, ensuring that $z_{r_1...r_m}$ corresponds to the combination of certain $x$, i.e., the one-hot representation of $(r_1, ..., r_m)$. Equations OH-H3 and OH-H4 guarantee the structure of one-hot, ensuring that exactly one value can be taken for each variable $X_q$. Based on the structure obtained by hard clauses, Equation OH-S reformulates the polynomial term $T$ as weighted soft clauses, considering the validity of equality $SatW(OH-S)$ as proved in the following theorem.

**Theorem 1.** The OH formulation is sound and requires $O(ub^m)$ auxiliary variables, $O(m \cdot ub^m)$ clauses, and $O(ub^k)$-valued soft weights.

*Proof.* We prove the validity of the OH formulation by proving that $SatW_{\alpha}(OH-S)$ is equal to the original polynomial term $T(X)$, for a fixed values vector $X$ such that $X_q = \sum_{r_q=0}^{ub} r_q \cdot x_{r_q}^{(q)}$ where $q \in \{1, ..., |X|\}$, given by the assignment $\alpha$.

$$
\begin{align*}
SatW(OH-S) &= \sum_{r_1=0}^{ub} \cdots \sum_{r_m=0}^{ub} c \cdot \prod_{q=1}^{m} r_q^{k_q} \cdot z_{r_1 \cdots r_m} \\
&= \sum_{r_1=0}^{ub} \cdots \sum_{r_m=0}^{ub} c \cdot \prod_{q=1}^{m} (r_q^{k_q} \cdot x_{r_q}^{(q)}) \tag{by OH-H1 and OH-H2} \\
&= c \cdot \prod_{q=1}^{m} \sum_{r_q=0}^{ub} (r_q \cdot x_{r_q}^{(q)})^{k_q} \tag{by Distributivity} \\
&= c \cdot \prod_{q=1}^{m} \left( \sum_{r_q=0}^{ub} r_q \cdot x_{r_q}^{(q)} \right)^{k_q} \tag{by OH-H3 and OH-H4} \\
&= c \cdot \prod_{q=1}^{m} X_q^{k_q} = T(X) \tag{since $\sum_{r_q=0}^{ub} r_q \cdot x_{r_q}^{(q)} = X_q$}
\end{align*}
$$

Therefore, $\max SatW(OH-S) \Leftrightarrow \max T(X)$ and the formulation is sound. The complexity of the number of auxiliary variables $z_{r_1...r_m}$ is $O(ub^m)$. There are $O(ub^m)$ soft clauses and $O(m \cdot ub^m + ub^m + m \cdot ub^2) = O(m \cdot ub^m)$ hard clauses, so the overall number of clauses is bounded by $O(m \cdot ub^m)$. Finally, the upper bound of soft weights $c \cdot \prod_{q=1}^{m} r_q^{k_q}$ is $O(ub^k)$. $\square$

Note that, based on different situations of $T(X) = c \cdot \prod_{q=1}^{m} X_q^{k_q}$, different special cases can occur. Indeed, when all $k_q = 1$, the complexity of auxiliary variables and clauses in the OH formulation decreases to $O(ub^k)$ and $O(k \cdot ub^k)$. Also, half-reification should be performed when applicable: When $m = 1$, $T(X)$ reduces to a pure power term $T_{pure} = c \cdot X^k$, in which case there is no necessity to introduce auxiliary variables $z$. In this case, Equations OH-H1 and OH-H2 are omitted, and we replace the $z$ variables in OH-S by the original $x$ variables. When $c > 0$, Equation OH-H2 becomes redundant, whereas when $c < 0$, Equation OH-H1 becomes redundant.

## 3.2 Unary Formulation

In this subsection, we develop the unary formulation. In this case, the encoding variables $x$ serve as a counter for the encoded term. This allows us to decompose
the value of a given polynomial term $T(\mathbf{X})$ as the sum of a series of increments, namely, the difference ($\tilde{T}$).

The theory of differences can be traced back to the application of finite difference methods in numerical analysis [9, 29]. Differences are to discrete functions what derivatives are to continuous functions, as well as prefix sums are to discrete functions what integrals are to continuous functions. Differences provide a natural framework for decomposing discrete functions into incremental contributions used in the unary representation. Therefore, we apply the idea of difference and prefix sum on the polynomial term $T$. The difference of $T$ is defined as follows:

**Definition 4 (Difference of a polynomial term).** For a polynomial term $T(\mathbf{X}) = c \cdot \prod_{q=1}^{m} X_q^{k_q}$, its difference $\tilde{T}$ at point $\mathbf{X} = (r_1, \dots, r_m)$ is defined by:

$$ \tilde{T}(r_1, \dots, r_m) = \begin{cases} 0 & \text{if } \exists q \in \{1, \dots, m\} : r_q = 0 \\ \sum_{S \subseteq \{1, \dots, m\}} (-1)^{|S|} T(r'_1, \dots, r'_m) & \text{otherwise} \end{cases} $$

$$ \text{where } r'_q = r_q - 1 \text{ if } q \in S, \text{ and } r'_q = r_q \text{ if } q \in \{1, \dots, m\} \setminus S. $$

Based on the definition of difference and the structure of polynomial terms, Proposition 1 describes the scale of $\tilde{T}$ and Proposition 2 formally establishes an inductive form of the difference function for polynomial terms.

**Proposition 1.** Given $T(\mathbf{X})$ with the order of $k$, it holds that the order of $\tilde{T}(\mathbf{X})$ is smaller than $k$.

*Proof.* The set $\{1, \dots, m\}$ has $2^m$ different subsets. It is known that $2^{m-1}$ of them have odd cardinality ($|S|$ is odd) and $2^{m-1}$ of them have even cardinality ($|S|$ is even), therefore the coefficients of the highest-order terms will cancel out in the summation. $\square$

**Proposition 2.** Given a polynomial term $T(\mathbf{X}) = c \cdot \prod_{q=1}^{m} r_q^{k_q}$ and a fixed point $\mathbf{X} = (r_1, \dots, r_m)$ s.t. $X_q \neq 0, \forall q \in \{1, \dots, m\}$, we have $\tilde{T}(r_1, \dots, r_m) = (r_m^{k_m} - (r_m - 1)^{k_m}) \cdot \tilde{T}(r_1, \dots, r_{m-1})$, where $T(r_1, \dots, r_{m-1})$ is defined as $c \cdot \prod_{q=1}^{m-1} r_q^{k_q}$.

*Proof.* This can be proven by reasoning on the cases where $m \in S$ or $m \notin S$ separately as follows:

$$ \begin{aligned} \tilde{T}(r_1, \dots, r_m) &= \sum_{S \subseteq \{1, \dots, m\}} (-1)^{|S|} T(r'_1, \dots, r'_m) \\ &= \sum_{S \subseteq \{1, \dots, m-1\}} (-1)^{|S|} T(r'_1, \dots, r'_{m-1}) \cdot r_m^{k_m} + \sum_{S \subseteq \{1, \dots, m-1\}} (-1)^{|S|+1} T(r'_1, \dots, r'_{m-1}) \cdot (r_m - 1)^{k_m} \\ &= \tilde{T}(r_1, \dots, r_{m-1}) \cdot r_m^{k_m} - \tilde{T}(r_1, \dots, r_{m-1}) \cdot (r_m - 1)^{k_m} = (r_m^{k_m} - (r_m - 1)^{k_m}) \cdot \tilde{T}(r_1, \dots, r_{m-1}) \end{aligned} $$

$\square$

This recursive formula enables us to naturally compute the difference function for high-order terms and is also relevant in the later discussion. Knowing the definition of difference, we thus introduce the notion of its *prefix sum*.
**Definition 5 (Prefix difference sum of a polynomial term).** The prefix difference sum of $T(\mathbf{X})$ at point $\mathbf{X} = (X_1, \dots, X_m)$ is defined as:

$$ \mathrm{PreSum}_T(\mathbf{X}) = \sum_{r_1=1}^{X_1} \sum_{r_2=1}^{X_2} \cdots \sum_{r_m=1}^{X_m} \tilde{T}(r_1, \dots, r_m) $$

The following proposition reveals that the relationship between the prefix sum and difference is analogous to the integral and derivative.

**Proposition 3.** Let $T$ be a polynomial term. Then, $\mathrm{PreSum}_T(\mathbf{X}) = T(\mathbf{X})$.

*Proof.* This result can be proven by induction on the dimension $m$ of $\mathbf{X}$. When $m = 1$, $T(X) = T(X) - T(X - 1)$ and we have:

$$ \mathrm{PreSum}_T(X) = \sum_{r=1}^{X} (T(r) - T(r-1)) = T(X) - T(0) = T(X) $$

The proposition thus holds. We then prove that the case of $m + 1$ holds under the hypothesis that the case of $m$ holds. Given $\mathbf{X} = (X_1, \dots, X_{m+1})$, we have:

$$ \mathrm{PreSum}_T(\mathbf{X}) = \sum_{r_1=1}^{X_1} \cdots \sum_{r_m=1}^{X_m} \left( \sum_{r_{m+1}=1}^{X_{m+1}} \tilde{T}(r_1, \dots, r_{m+1}) \right) \quad \text{(by Definition 5)} $$

$$ = \sum_{r_1=1}^{X_1} \cdots \sum_{r_m=1}^{X_m} \left( \sum_{r_{m+1}=1}^{X_{m+1}} (r_{m+1}^{k_{m+1}} - (r_{m+1}-1)^{k_{m+1}}) \cdot \tilde{T}(r_1, \dots, r_m) \right) \quad \text{(by Proposition 2)} $$

$$ = \sum_{r_1=1}^{X_1} \cdots \sum_{r_m=1}^{X_m} \left( \tilde{T}(r_1, \dots, r_m) \cdot \sum_{r_{m+1}=1}^{X_{m+1}} (r_{m+1}^{k_{m+1}} - (r_{m+1}-1)^{k_{m+1}}) \right) $$

$$ = \left( \sum_{r_1=1}^{X_1} \cdots \sum_{r_m=1}^{X_m} \tilde{T}(r_1, \dots, r_m) \right) \cdot X_{m+1}^{k_{m+1}} $$

$$ = T(r_1, \dots, r_m) \cdot X_{m+1}^{k_{m+1}} = T(r_1, \dots, r_{m+1}) = T(\mathbf{X}) \quad \text{(by Inductive Hypothesis)} $$

□

Based on Proposition 3, we thus manage to construct the unary formulation (UNA) for any given $T = c \prod_{q=q_1}^{m} X_q^{k_q}$ as follows:

**Soft Clauses**

$$ (z_{r_1 \dots r_m}, \tilde{T}(r_1, \dots, r_m)) \quad \forall (r_1, \dots, r_m) \in \mathbf{V}_{ub}^m : \tilde{T}(r_1, \dots, r_m) \neq 0 \quad \text{(UNA-S)} $$

**Hard clauses**

$$ \bar{z}_{r_1 \dots r_m} \lor x_{rq}^{(q)} \quad \forall q \in \{1, \dots, m\}, \forall (r_1, \dots, r_m) \in \mathbf{V}_{ub}^m \quad \text{(UNA-H1)} $$

$$ \bigvee_{q=1}^{m} \bar{x}_{rq}^{(q)} \lor z_{r_1 \dots r_m} \quad \forall (r_1, \dots, r_m) \in \mathbf{V}_{ub}^m \quad \text{(UNA-H2)} $$

$$ \bar{x}_r^{(q)} \lor x_{r-1}^{(q)} \quad \forall q \in \{1, \dots, m\}, \forall r \in \mathbf{V}_{ub} \quad \text{(UNA-H3)} $$

Equations UNA-S to UNA-H3 make up the unary representation (UNA) for any polynomial term. The main structure remains similar to OH, with auxiliary variables $z_{r_1 \dots r_m}$ added in the same situation describing the combination of co-appearance of $x_{rq}^{(q)}$. Equations UNA-H1 and UNA-H2 align with OH-H1
and OH-H2, building the connection between auxiliary variables and original variables. UNA-H3 is equivalent to $x_r^{(q)} \to x_{r-1}^{(q)}$, ensuring the structure of unary representation. Finally, Equation UNA-S builds upon the two previous equations, transforming $T(\mathbf{X})$ into weighted soft clause based on the following proposition.

**Theorem 2.** The UNA formulation with Equations UNA-S to UNA-H3 is sound and requires $O(ub^m)$ auxiliary variables, $O(m \cdot ub^m)$ clauses, and $O(ub^{k-1})$-valued soft weights.

*Proof.* We prove the validity of the UNA formulation by proving that $SatW(UNA-S)$ is equal to the original polynomial term $T(\mathbf{X})$.

$$ 
\begin{aligned}
SatW(UNA-S) &= \sum_{r_1=1}^{ub} \sum_{r_2=1}^{ub} \cdots \sum_{r_m=1}^{ub} \tilde{T}(r_1, \dots, r_m) z_{r_1 \dots r_m} \\
&= \sum_{r_1=1}^{ub} \sum_{r_2=1}^{ub} \cdots \sum_{r_m=1}^{ub} \tilde{T}(r_1, \dots, r_m) \prod_{q=1}^{m} x_{r_m}^{(q)} \quad (\text{by UNA-H1 and UNA-H2}) \\
&= T(\mathbf{X}) \quad (\text{by UNA-S and Proposition 3})
\end{aligned}
$$

Therefore, $\max T(\mathbf{X}) \Leftrightarrow \max SatW(UNA-S)$ and the formulation is sound. There are $O(ub^m)$ introduced auxiliary variables, and there are $O(ub^m)$ soft clauses and $O(m \cdot ub^m + ub^m + m \cdot ub^m) = O(m \cdot ub^m)$ hard clauses. Based on Proposition 1, the corresponding weight $\tilde{T}(r_1, \dots, r_m)$ is within the scale of $O(ub^{k-1})$. $\square$

In MaxSAT solving, the soft weight scale of an instance is generally positively correlated to its difficulty. The most important benefit brought by the unary representation is the decrease of the scale of the soft weight. The unary representation ensures that the order of soft weight is always one less than the order of the term, i.e., reducing the soft weight scale from $O(ub^k)$ to $O(ub^{k-1})$. An interesting observation attached to this advantage is that for any separable quadratic function, e.g., $F = x_1^2 + x_2^2$, the soft weight would become a linear function of original variables, making the formulation much more tractable for applications.

## 3.3 Binary Formulation

Binary representation is the most compact encoding featuring the logarithmic projection of integer variables to Boolean bits. In this subsection, we expand the binary formulation at a term-level sense. Given any polynomial term $T(\mathbf{X}) = c \cdot \prod_{q=1}^{m} X_q^{k_q}$ where $\sum_{q=1}^{m} k_q = k$, the binary formulation reformulates this into $T(\mathbf{X}) = c \cdot \prod_{q=1}^{k} X_{\Omega(q)}$, where $\Omega$ is a mapping such that each original variable $X_q$ appears exactly $k_q$ times in the expanded product. This transforms a product with exponents into an equivalent product of $k$ individual variables. Based on this reformulation, we formulate $T$ as the following equation, denoted by $SatW(BIN-S)$ and proved by Theorem 3: $T(\mathbf{X}) = c \cdot \prod_{q=1}^{k} X_{\Omega(q)} = \sum_{(r_1, \dots, r_k) \in \mathbf{X}_{\log ub}^k} c \cdot 2^{\sum_{q=1}^{k} r_q \cdot z_{r_1 \dots r_k}}$, where $z_{r_1 \dots r_k}$ is the auxiliary variable introduced to represent the combination of any possible permutation of $x^{(\Omega(q))}$
representing $X_{\Omega}(q)$ in the binary representation. The binary formulation (BIN) is thus formalized as follows:

### Soft Clauses

$$ (z_{r_1 \dots r_k}, c \cdot 2^{\sum_{q=1}^k r_q}) \quad \forall (r_1, \dots, r_k) \in \mathbf{V}_{\log ub}^k \quad (\text{BIN-S}) $$

### Hard Clauses

$$ \bar{z}_{r_1 \dots r_k} \lor x_{r_q}^{(\Omega(q))} \quad \forall q \in \{1, \dots, k\}, \forall (r_1, \dots, r_k) \in \mathbf{V}_{\log ub}^k \quad (\text{BIN-H1}) $$

$$ (\bigvee_{q=1}^{k} \bar{x}_{r_q}^{(\Omega(q))}) \lor z_{r_1 \dots r_k} \quad \forall (r_1, \dots, r_k) \in \mathbf{V}_{\log ub}^k \quad (\text{BIN-H2}) $$

Equations BIN-S to BIN-H2 compose the binary formulation (BIN). The hard constraints BIN-H1 and BIN-H2 altogether are equivalent to $z_{r_1 \dots r_k} \leftrightarrow \bigwedge_{q=1}^k x_{r_q}^{(\Omega(q))}$. Note that, after rewriting the original index set as $\Omega$, duplicate $x_{r_q}^{(\Omega(q))}$ may appear within one clause of BIN-H2, and we only keep one of them. Based on the hard clauses, Equation BIN-S reformulates $T(\mathbf{X})$ as soft clauses, as proposed in the following theorem.

**Theorem 3.** The BIN formulation is sound and introduces auxiliary variables and clauses in the scale of $O((\log ub)^k)$ and $O(k \cdot (\log ub)^k)$, with the soft weight in the scale of $O(ub^k)$.

*Proof.* We prove the validity of the UNA formulation by proving that $SatW(\text{UNA} - \text{S})$ is equal to the original polynomial term $T(\mathbf{X})$ as follows:

$$
\begin{align*}
SatW(S) &= \sum_{(r_1, \dots, r_k) \in \mathbf{V}_{\log ub}^k} c \cdot 2^{\sum_{q=1}^k r_q} \cdot z_{r_1 \dots r_k} = \sum_{r_1=0}^{\lfloor \log ub \rfloor} \dots \sum_{r_k=0}^{\lfloor \log ub \rfloor} c \cdot 2^{\sum_{q=1}^k r_q} \cdot z_{r_1 \dots r_k} \\
&= c \cdot \sum_{r_1=0}^{\lfloor \log ub \rfloor} \dots \sum_{r_k=0}^{\lfloor \log ub \rfloor} \prod_{q=1}^k 2^{r_q} x_{r_q}^{(\Omega(q))} && \text{(by BIN-H1 and BIN-H1)} \\
&= c \cdot \prod_{q=1}^k \left( \sum_{r_q=0}^{\lfloor \log ub \rfloor} 2^{r_q} x_{r_q}^{(\Omega(q))} \right) && \text{(by Distributivity)} \\
&= c \cdot \prod_{q=1}^k X_{\Omega(q)} = T(\mathbf{X}) && \text{(since } \sum_{r_q=0}^{\lfloor \log ub \rfloor} 2^{r_q} \cdot x_{r_q}^{(\Omega(q))} = X_{\Omega(q)})
\end{align*}
$$

Therefore, $\max T(\mathbf{X}) \Leftrightarrow \max SatW(\text{BIN} - \text{S})$ and the formulation is sound. There are $O((\log ub)^k)$ $z_{r_1 \dots r_k}$ variables introduced as auxiliary variables, and there are $O((\log ub)^k)$ soft clauses and $O(k \cdot (\log ub)^k + (\log ub)^k) = O(k \cdot (\log ub)^k)$ hard clauses. The soft weight $c \cdot 2^{\sum_{q=1}^k r_q}$ is bounded within $O(ub^k)$. $\square$

The following example presents a polynomial term under the BIN.

**Example 1.** Suppose $T(\mathbf{X}) = X_1^2 X_2$ and $ub = 3$, we use Boolean variables $x^{(1)}$ to represent $X_1$ and $x^{(2)}$ to represent $X_2$ in the binary encoding. Since $\lfloor \log ub \rfloor = \lfloor \log 3 \rfloor = 1$, we need 2 Boolean variables for each integer variable, indexed by 0 and 1. Under binary representation, we rewrite $T(\mathbf{X}) = X_1 X_1 X_2$ and introduce auxiliary Boolean variables $z_{r_1 r_2 r_3} \quad \forall (r_1, r_2, r_3) \in \{0, 1\}^3$. Following equation BIN-S, we thus obtain the soft clauses:

$$ S = \{(z_{000}, 2^0), (z_{001}, 2^1), (z_{010}, 2^1), (z_{011}, 2^2), (z_{100}, 2^1), (z_{101}, 2^2), (z_{110}, 2^2), (z_{111}, 2^3)\} $$
and, from equations BIN-H1 and BIN-H2, we obtain the following hard clauses:

$$ \bar{z}_{r_1 r_2 r_3} \lor x_{r_1}^{(1)}, \quad \bar{z}_{r_1 r_2 r_3} \lor x_{r_2}^{(1)}, \quad \bar{z}_{r_1 r_2 r_3} \lor x_{r_3}^{(2)} \quad \forall (r_1, r_2, r_3) \in \{0, 1\}^3 \quad (\text{From BIN-H1}) $$

$$ \bar{x}_{r_1}^{(1)} \lor \bar{x}_{r_2}^{(1)} \lor \bar{x}_{r_3}^{(2)} \lor z_{r_1 r_2 r_3} \quad \forall (r_1, r_2, r_3) \in \{0, 1\}^3 \quad (\text{From BIN-H2}) $$

Therefore, we can represent $T$ as follows: $T(\mathbf{X}) = 2^0 \cdot z_{0,0,0} + 2^1 \cdot z_{0,0,1} + 2^1 \cdot z_{0,1,0} + 2^2 \cdot z_{0,1,1} + 2^1 \cdot z_{1,0,0} + 2^2 \cdot z_{1,0,1} + 2^2 \cdot z_{1,1,0} + 2^3 \cdot z_{1,1,1} = \text{SatW}(S)$

To verify the soundness of this representation, let's compute the value of $T$ for specific values of $X_1$ and $X_2$. For example, suppose $X_1 = 3 = 2^1 + 2^0$ and $X_2 = 2 = 2^1$. In binary encoding, this corresponds to $x_1^{(1)} = 1$, $x_0^{(1)} = 1$ for $X_1$ and $x_1^{(2)} = 1$, $x_0^{(2)} = 0$ for $X_2$. With these values, the variables $z_{0,0,0}$, $z_{0,0,1}$, $z_{0,1,0}$, $z_{0,1,1}$, $z_{1,0,0}$, $z_{1,0,1}$, $z_{1,1,0}$, and $z_{1,1,1}$ can be determined. More specifically, since $x_0^{(1)} = 1$, $x_0^{(2)} = 0$, we have $z_{0,0,0} = 0$. Similarly, since $x_0^{(1)} = 1$, $x_1^{(2)} = 1$, we have $z_{0,0,1} = 1$. Following this logic, we determine that $z_{0,1,1} = 1$, $z_{1,0,1} = 1$, and $z_{1,1,1} = 1$, while all other $z$ variables are 0. Therefore, we have: $T(X_1, X_2) = \sum_{r_1=0}^{1} \sum_{r_2=0}^{1} \sum_{r_3=0}^{1} 2^{r_1+r_2+r_3} \cdot z_{r_1 r_2 r_3} = 2 + 4 + 4 + 8 = 18$. This matches the actual value $X_1^2 X_2 = 3^2 \cdot 2 = 18$, confirming the soundness of BIN.

In Table 2, we summarize the complexities of the three presented representations. The three formulations offer different trade-offs in terms of advantages and disadvantages. The one-hot formulation provides a straightforward implementation but suffers from high complexity as the number of variables increases. The unary formulation's key advantage is its reduced soft weight scale, which generally improves the solvability of the resulting MaxSAT instance; however, it still maintains high complexity in terms of auxiliary variables and constraints. The binary formulation offers the most compact encoding with logarithmic scaling, but becomes more complex when dealing with high-order terms that contain only a few different variables. These characteristics guide the selection of appropriate encoding methods based on the specific structure of polynomial terms in practical applications. Despite the quantified complexity, it is also an important factor that the formulation should be compatible with the original semantic information of the problem being formulated. Additionally, it may be beneficial to introduce a mixture of representations when multiple variables appear in the same polynomial term, each with different semantic properties. Different representation methods can be selected to match the specific contextual meaning of each variable.

<table><caption>Table 2: Complexity Analysis of Different Atomic Formulations, where $m$ is the number of different variables in the term, $k \ge m$ is the order of the term and $ub$ is the upper bound of the integer variables</caption><thead><tr><th>Aspect</th><th>One-hot</th><th>Unary</th><th>Binary</th></tr></thead><tbody><tr><td>Auxiliary Variables</td><td>O(ub<sup>m</sup>)</td><td>O(ub<sup>m</sup>)</td><td>O((log ub)<sup>k</sup>)</td></tr><tr><td>Constraints</td><td>O(m &middot; ub<sup>m</sup>)</td><td>O(m &middot; ub<sup>m</sup>)</td><td>O(k &middot; (log ub)<sup>k</sup>)</td></tr><tr><td>Highest Soft Weight</td><td>O(ub<sup>k</sup>)</td><td>O(ub<sup>k-1</sup>)</td><td>O(ub<sup>k</sup>)</td></tr></tbody></table>
4 Order Decomposition: Beyond Atomic Handling

In this section, we develop the idea of decomposing any given polynomial term
$T(\mathbf{X}) = c \cdot \prod_{q=1}^{m} X_q^{k_q}$ from the perspective of its order $k = \sum_{q=1}^{m} k_q$. This idea
is invoked by the following two limitations of the atomic formulation: (i) The
atomic formulations are obtained with the complexity of an exponential level,
which is even the case for the most compact BIN formulation, which requires
$O((\log ub)^k)$ auxiliary variables and $O(k \cdot (\log ub)^k)$ clauses. (ii) The atomic for-
mulations cannot take advantage of the similar structure of multiple terms within
one NLIP. In this section, we present the idea of order-wise decomposition, which
is based on the BIN formulation and manages to improve these limitations.

In Section 3.3, we presented the BIN formulation that can formulate any
polynomial term under the form $T(\mathbf{X}) = c \prod_{i=1}^{k} X_{\Omega(i)}$. In the decomposition,
we regard $\Omega$ as a set of indices, i.e., $T(\mathbf{X}) = c \prod_{q \in \Omega} X_q$. The essence of decompo-
sition is to introduce auxiliary variables $y$ to represent the intermediate products,
therefore avoiding the exponential complexity produced by the combination of
all $k$ units. Algorithm 1 describes the whole process recursively. Its core idea is
to partition the set of variables into two smaller subsets, then recursively pro-
cess each subset, and finally combine their results. Specifically, when $\Omega$ contains
only one element $q$, it directly returns the corresponding Boolean variable $x^{(q)}$;
otherwise, it partitions $\Omega$ into two disjoint subsets $\Omega_1$ and $\Omega_2$, recursively calls
Decompose to obtain encodings for each subset, and finally merges the interme-
diate results through the Mul operation, avoiding the exponential complexity
that would arise from processing all possible variable combinations.

We then introduce the operation of multiplication Mul based on the BIN formulation. Given two integers A bounded by uba and B bounded by ubb, Mul is the operation obtaining the binary formulation of the product of the two integers. Suppose x⁽ª⁾ and x⁽ᵇ⁾ are two series of binary variables representing A and B with the binary encoding, Mul(x⁽ª⁾, x⁽ᵇ⁾) introduces a new series of Boolean variables y⁽ᵃ⁾ ∀r ∈ Vlog(uba·ubb) to encode the product A · B in binary representation. This operation is formalized through the following constraints.

<table><caption>**Algorithm 1:** Decompose(Ω)</caption>
  <thead>
    <tr>
      <th>Input:</th>
      <td>A set of variable indices Ω</td>
    </tr>
    <tr>
      <th>Output:</th>
      <td>Boolean encoding of the product of variables indexed by Ω</td>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>1</td>
      <td>if |Ω| = 1 with Ω = {q} then</td>
    </tr>
    <tr>
      <td>2</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;return x<sup>(q)</sup>;</td>
      <td>// Base case</td>
    </tr>
    <tr>
      <td>3</td>
      <td>else</td>
    </tr>
    <tr>
      <td>4</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;(Ω<sub>1</sub>, Ω<sub>2</sub>) ← Partition(Ω); // Split Ω into two disjoint subsets</td>
    </tr>
    <tr>
      <td>5</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;y<sup>(Ω<sub>1</sub>)</sup> ← Decompose(Ω<sub>1</sub>); // Recursively encode first part</td>
    </tr>
    <tr>
      <td>6</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;y<sup>(Ω<sub>2</sub>)</sup> ← Decompose(Ω<sub>2</sub>); // Recursively encode second part</td>
    </tr>
    <tr>
      <td>7</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;return Mul(y<sup>(Ω<sub>1</sub>)</sup>, y<sup>(Ω<sub>2</sub>)</sup>); // Combine using Mul operation</td>
    </tr>
    <tr>
      <td>8</td>
      <td>end</td>
    </tr>
  </tbody>
</table>
<figure><img src="image_1.png" /><figcaption>Fig. 1: Sequential decomposition (a) and binary decomposition (b) of polynomial term $T = X_1X_2X_3X_4X_5X_6X_7X_8$, and a decomposition plan (c) for the high-order polynomial function of $P(\mathbf{X}) = X_1X_2X_3X_4 + X_3X_4X_5X_6 + X_1X_2X_5X_6$.</figcaption></figure>

**Hard Constraints in Mul($x^{(a)}$, $x^{(b)}$)**

$$z_{r_a r_b}^{(ab)} \leftrightarrow (x_{r_a}^{(a)} \wedge x_{r_b}^{(b)}) \quad \forall (r_a, r_b) \in \mathbf{V}_{\log ub_a} \times \mathbf{V}_{\log ub_b} \quad (\text{Mul-1})$$

$$\sum_{r=0}^{\lfloor \log(ub_a \cdot ub_b) \rfloor} 2^r y_r^{(ab)} = \sum_{r_a=0}^{\lfloor \log ub_a \rfloor} \sum_{r_b=0}^{\lfloor \log ub_b \rfloor} 2^{r_a+r_b} z_{r_a r_b}^{(ab)} \quad (\text{Mul-2})$$

Equation Mul-1 rewrites Equation BIN-H1 and BIN-H2 in the constraint level, adding auxiliary variables $z_{r_a r_b}^{(ab)}$ and enforcing the link with original variables $x^{(a)}$ and $x^{(b)}$. Equation Mul-2 then aligns the value of variables $y^{(ab)}$ with the value embedded by $z^{(ab)}$. In the following context, we refer to Mul-1 and Mul-2 as $y^{(ab)} \leftarrow Mul(x^{(a)}, x^{(b)})$ and use this operation as a constraint in a higher level. The following proposition analyzes the complexity of Mul($x^{(a)}, x^{(b)}$), where PB($\#l, w_{max}$) is the scale of clauses number obtained through a PB encoding of $\sum_{i=1}^{\#l} w_i l_i \triangleright c$, with $\#l$ denoting the number of literals and $w_{max} = max_{1 \le i \le \#l} w_i$ representing the highest weight.

**Proposition 4.** Given two integers $A \le ub_a$ and $B \le ub_b$ encoded using $x^{(a)}$ and $x^{(b)}$ variables, the Mul($x^{(a)}, x^{(b)}$) operation introduces $O(PB(\log ub_a \cdot \log ub_b, ub_a \cdot ub_b))$ clauses.

*Proof.* The two series of auxiliary variables, $z^{(ab)}$ and $y^{(ab)}$, are in the scale of $O(\log ub_a \cdot \log ub_b)$ and $O(\log(ub_a \cdot ub_b)) = O(\log ub_a + \log ub_b)$ respectively, yielding the overall complexity of $O(\log ub_a \cdot \log ub_b)$. There are $O(\log(ub_a) \cdot \log(ub_b))$ clauses in Equation Mul-1. The scale of clauses in Mul-2 depends on the selection of Pseudo-Boolean encoding. The number of literals $\#l$ appearing in it is bounded by the numbers of $z^{(ab)}$ and $y^{(ab)}$, and the largest weight $w_{max}$ is bounded by $ub_a \cdot ub_b$. $\square$

Based on the operation of Mul, Decompose($\Omega$) can be performed as showcased in Algorithm 1, leaving the partition strategy (line 4) a degree of freedom. Figure 1 illustrates two different partitioning strategies, namely Sequential Decomposition (1a) and Binary Decomposition(1b): Sequential Decomposition always isolates one variable at a time, while Binary Decomposition recursively
divides the variable set into two roughly equal parts. Limited by space, here we
only formalize Sequential Decomposition in the following formulation.

Soft Clauses

$$
(y_r^{(1 \dots k)}, c \cdot 2^r) \qquad \forall r \in \mathbf{V}_{k \cdot \log ub} \qquad (\text{SD-S})
$$

Hard Constraints

$$
y^{(12)} \leftarrow Mul(x^{(1)}, x^{(2)}) \qquad (\text{SD-H1})
$$

$$
y^{(1 \dots \mathcal{K})} \leftarrow Mul(y^{(1, \dots, \mathcal{K}-1)}, x^{(\mathcal{K})}) \quad \forall \mathcal{K} \in \{3, \dots, k\} \quad (\text{SD-H2})
$$

Equations SD-S to SD-H2 comprise the Sequential Decomposition. The hard
constraints perform $k - 1$ times of Mul and subsequently encode $\prod_{q=1}^{\mathcal{K}} X_q$ by
$y^{(1 \dots \mathcal{K})}$. The soft clauses in SD-S are then built on the top level of variables $y_r^{(1 \dots k)}$.
The following theorem discusses the complexity of formulations for polynomial
terms obtained under the idea of decomposition.

**Theorem 4.** *Given a polynomial term* $T(X) = c \prod_{q \in \Omega} X_q$, *the decomposition-based formulation introduce clauses in the scale of* $O(k \cdot PB(k^2(\log ub)^2, ub^k))$.

*Proof.* There are always $k-1$ times of *Mul* operations, within each of them the upper bounds of both *ub*<sub>*a*</sub> and *ub*<sub>*b*</sub> are *ub*<sup>*k*</sup>, since all the intermediate products of ∏<sub>*q*∈Ω</sub> *X*<sub>*q*</sub> are bounded by *ub*<sup>*k*</sup>. Follow Proposition 4, the theorem holds. □

Note that often in the complexity of PB constraints, a Logarithmic function
is applied to the maximum weight $w_{max}$, leaving a non-exponential complexity
of the formulation. Theorem 4 holds for all decomposition-based formulations,
despite the selection of the partition strategy. Nevertheless, the flexibility left
by the partition strategy benefits the potential of different polynomial terms
sharing common structure, as an example given in Figure 1c.

5 Conclusion

In this paper, we have explored different MaxSAT-based formulations for non-linear polynomial integer programs. We first dive into this topic through the perspectives of the variable-wise polynomial representations, with three distinct encoding plans favoring different real-life scenarios, therefore, three formulations are proposed with a thorough discussion on their complexity. Then, we focus on the order-wise decomposition of polynomial terms, based on which formulations with compact complexity are obtained.

As future work, it would be interesting to continue exploring the other three
integer mapping ways proposed in [2], as well as refine the selection strategy of
representation/decomposition methods. Practically, a thorough implementation
of NLIP-MaxSAT formulations can be applied on different real-world problems,
therefore broadening the scope of application of SAT and MaxSAT modern tech-
nologies. We also hope to develop an API enabling the use of our non-linear
formulations, to be made available to the community.
## Acknowlegement

This work is partially supported by the ANR-24-CE23-6126 project (BforSAT) and by the ANR-19-CHIA0013-01 chair (MASSAL'IA), co-funded by the French national research agency and the French electricity distribution network operator Enedis.

## References

1. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Bdds for pseudo-boolean constraints - revisited. In Karem A. Sakallah and Laurent Simon, editors, *Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings*, volume 6695 of *Lecture Notes in Computer Science*, pages 61–75. Springer, 2011.

2. Carlos Ansótegui and Felip Manyà. Mapping problems with finite-domain variables into problems with boolean variables. In *SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings*, 2004.

3. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiability. In *Handbook of satisfiability*, pages 929–991. IOS Press, 2021.

4. Clark Barrett and Sergey Berezin. A proof-producing boolean search engine. *Program Commitee*, page 25, 2003.

5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. *Handbook of Satisfiability - Second Edition*, volume 336 of *Frontiers in Artificial Intelligence and Applications*. IOS Press, 2021.

6. Miquel Bofill, Jordi Coll, Marc Garcia, Jesús Giráldez-Cru, Gilles Pesant, Josep Suy, and Mateu Villaret. Constraint solving approaches to the business-to-business meeting scheduling problem. *J. Artif. Intell. Res.*, 74:263–301, 2022.

7. Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux Devendeville. Minimizing working-group conflicts in conference session scheduling through maximum satisfiability (short paper). In Paul Shaw, editor, *30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain*, volume 307 of *LIPIcs*, pages 34:1–34:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.

8. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Experimenting on solving nonlinear integer arithmetic with incremental linearization. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, *Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings*, volume 10929 of *Lecture Notes in Computer Science*, pages 383–398. Springer, 2018.

9. Richard Courant, Kurt Friedrichs, and Hans Lewy. Über die partiellen differenzengleichungen der mathematischen physik. *Mathematische annalen*, 100(1):32–74, 1928.

10. Marco A. Duran and Ignacio E. Grossmann. An outer-approximation algorithm for a class of mixed-integer nonlinear programs. *Math. Program.*, 39(3):337, 1987.

11. Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into SAT. *J. Satisf. Boolean Model. Comput.*, 2(1-4):1–26, 2006.
12. Allen Van Gelder. Another look at graph coloring via propositional satisfiability. *Discret. Appl. Math.*, 156(2):230-243, 2008.

13. Ana Graça, Inês Lynce, João Marques-Silva, and Arlindo L. Oliveira. Efficient and accurate haplotype inference by combining parsimony and pedigree information. In Katsuhisa Horimoto, Masahiko Nakatsui, and Nikolaj Popov, editors, *Algebraic and Numeric Biology - 4th International Conference, ANB 2010, Hagenberg, Austria, July 31- August 2, 2010, Revised Selected Papers*, volume 6479 of *Lecture Notes in Computer Science*, pages 38-56. Springer, 2010.

14. João Guerra and Inês Lynce. Reasoning over biological networks using maximum satisfiability. In Michela Milano, editor, *Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings*, volume 7514 of *Lecture Notes in Computer Science*, pages 941-956. Springer, 2012.

15. Aarti Gupta, Malay K. Ganai, and Chao Wang. Sat-based verification methods and applications in hardware verification. In Marco Bernardo and Alessandro Cimatti, editors, *Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures*, volume 3965 of *Lecture Notes in Computer Science*, pages 108-143. Springer, 2006.

16. Raymond Hemmecke, Matthias Köppe, Jon Lee, and Robert Weismantel. Nonlinear integer programming. In Michael Jünger, Thomas M. Liebling, Denis Naddef, George L. Nemhauser, William R. Pulleyblank, Gerhard Reinelt, Giovanni Rinaldi, and Laurence A. Wolsey, editors, *50 Years of Integer Programming 1958-2008 - From the Early Years to the State-of-the-Art*, pages 561-618. Springer, 2010.

17. Markowitz HM. Portfolio selection: efficient diversification of investments, 1959.

18. R. G. Jeroslow. There cannot be any algorithm for integer programming with quadratic constraints. *Operations Research*, 21(1):221-224, 1973.

19. Will Klieber and Gihwon Kwon. Efficient cnf encoding for selecting 1 from n objects. In *Proc. International Workshop on Constraints in Formal Verification*, page 14, 2007.

20. Gereon Kremer, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, *Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings*, volume 13385 of *Lecture Notes in Computer Science*, pages 95-105. Springer, 2022.

21. Chu Min Li and Felip Manyà. MaxSAT, Hard and Soft Constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, *Handbook of Satisfiability - Second Edition*, volume 336 of *Frontiers in Artificial Intelligence and Applications*, pages 903-927. IOS Press, 2021.

22. Chu-Min Li, Felip Manya, Zhe Quan, and Zhu Zhu. Exact minsat solving. In *International Conference on Theory and Applications of Satisfiability Testing (SAT-2010)*, pages 363-368, 2010.

23. Duan Li, Xiaoling Sun, et al. *Nonlinear integer programming*, volume 84. Springer, 2006.

24. Jesús A. De Loera, Raymond Hemmecke, Matthias Köppe, and Robert Weismantel. Integer polynomial optimization in fixed dimension. *Math. Oper. Res.*, 31(1):147-153, 2006.

25. Norbert Manthey, Tobias Philipp, and Peter Steinke. A more compact translation of pseudo-boolean constraints into CNF such that generalized arc consistency is
maintained. In Carsten Lutz and Michael Thielscher, editors, *KI 2014: Advances in Artificial Intelligence - 37th Annual German Conference on AI, Stuttgart, Germany, September 22-26, 2014. Proceedings*, volume 8736 of *Lecture Notes in Computer Science*, pages 123–134. Springer, 2014.

26. Panos M. Pardalos, Franz Rendl, and Henry Wolkowicz. The quadratic assignment problem: A survey and recent developments. In Panos M. Pardalos and Henry Wolkowicz, editors, *Quadratic Assignment and Related Problems, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, May 20-21, 1993*, volume 16 of *DIMACS Series in Discrete Mathematics and Theoretical Computer Science*, pages 1–42. DIMACS/AMS, 1993.

27. Olivier Roussel and Vasco Manquinho. Pseudo-boolean and cardinality constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, *Handbook of Satisfiability - Second Edition*, volume 336 of *Frontiers in Artificial Intelligence and Applications*, pages 1087–1129. IOS Press, 2021.

28. Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, and Karem A. Sakallah. Improved design debugging using maximum satisfiability. In *Formal Methods in Computer-Aided Design, 7th International Conference, FM-CAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings*, pages 13–19. IEEE Computer Society, 2007.

29. John C Strikwerda. *Finite difference schemes and partial differential equations*. SIAM, 2004.

30. Pavel Surynek. Lazy compilation of variants of multi-robot path planning with satisfiability modulo theory (SMT) approach. In *2019 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2019, Macau, SAR, China, November 3-8, 2019*, pages 3282–3287. IEEE, 2019.

31. Zhifei Zheng, Sami Cherif, and Rui Sa Shibasaki. Optimizing power peaks in simple assembly line balancing through maximum satisfiability. In *36th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2024, Herndon, VA, USA, October 28-30, 2024*, pages 363–370. IEEE, 2024.