# Exact Approaches for the Diverse Satisfiability Problem

Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, Chu-Min Li, Jialu Zhang

► To cite this version:

Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, Chu-Min Li, Jialu Zhang. Exact Approaches for the Diverse Satisfiability Problem. European Conference on Logics in Artificial Intelligence (JELIA 2025), Sep 2025, Kutaisi, France. hal-05268883

HAL Id: hal-05268883

https://u-picardie.hal.science/hal-05268883v1

Submitted on 19 Sep 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Exact Approaches for the Diverse
Satisfiability Problem

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.** Given a Conjunctive Normal Form (CNF) formula $\phi$ and a positive integer $k$, the problem of Diversity Satisfiability (Diverse SAT) consists in finding $k$ assignments satisfying $\phi$ while maximizing the sum of pairwise distances among them. Previous related works mainly focus on the design of heuristic algorithms, while this paper focuses on introducing exact methods. A quadratic integer programming (QIP) model is first proposed. Then, based on two novel weight functions, namely the direct weight (DW) and the incremental weight (IW), we reformulate the QIP models into two integer linear programming (ILP) models, which can also be adapted to Maximum Satisfiability (MaxSAT) instances. Extensive experiments were conducted to evaluate the efficiency of the proposed methods, showing that the proposed approaches are able to compute optimal solutions for the studied instances with linear models achieving superior performance.

# 1 Introduction

Propositional Satisfiability (SAT) is a decision problem that consists in determining whether a given CNF (Conjunctive Normal Form) formula can be satisfied by an assignment of the variables [6], also referred to as a model of the formula. SAT is the first problem proven to be NP-complete [8], and serves as a core engine in various real-life applications such as hardware and software verification [1,7], planning and scheduling [29,30] and bio-informatics [21,22], among many others. While the classical SAT problem requires finding a single model that satisfies a given CNF formula, many real-world applications demand multiple models with diverse heterogeneous structural characteristics. In such cases, relying on just one satisfying assignment may lead to incomplete analyses or missed insights.

One notable example arises in Bounded Model Checking (BMC) [1], where each SAT model represents a possible verification path. However, focusing on a single model increases the likelihood of overlooking corner-case bugs, as it may not capture the full spectrum of possible behaviors in the system under

<footnote>* Corresponding author</footnote>
verification. This limitation highlights the need to generate multiple diverse so-
lutions, thereby improving the robustness and completeness of debugging and
verification processes. Building upon this observation, Nadel introduced the Di-
verse Satisfiability (Diverse SAT) problem in [24] which, given a CNF formula,
seeks to identify *k* satisfying models that are as distinct as possible. The degree
of diversity is typically quantified by the sum of pairwise Hamming distances
between selected models, ensuring that each solution contributes to maximizing
structural variation. In the same paper, an incomplete method empowered by a
dedicated variable decision heuristic is proposed. More recently, [20] presents an
efficient local search algorithm for this problem.

Another closely related problem proposed in the literature is the Maximum
Hamming Distance problem for Constraint Satisfaction Problems (CSPs), first
introduced in [9] by Crescenzi and Rossi. This problem is restricted to finding
only two distinct models. As such, when the variables are binary, the problem
becomes essentially similar to Diverse SAT with *k* = 2. Since solving SAT with a
single model is already NP-complete, the Diverse SAT problem, which requires
identifying *k* diverse models, poses an even greater computational challenge. In
particular, for a given parameter *p*, Misra et al. [23] prove that, even in the
restricted case where *k* = 2, determining two models that differ in exactly (or
at least) *p* variables remains NP-hard. In [2], Angelsmark and Thapper provide
an upper bound of $O(1.7338^n)$ for solving Max-Hamming Distance 2-SAT (i.e.,
Diverse SAT with *k* = 2 where the given instance contains only clauses of length
2). More generally, they show that, for Max-Hamming Distance *l*-SAT, where *l*
is the maximum length of clauses in the given CNF formula, an upper bound
of $O((2a)^n)$ can be established, under the hypothesis that the underlying *l*-SAT
instance can be solved within $O(a^n)$ with a certain constant *a*.

In this paper, we focus on introducing exact approaches for Diverse Satisfia-
bility which, to the best of our knowledge, have not been explored in the litera-
ture. We propose two generic approaches, based on Quadratic Integer Programming (QIP) and linear Pseudo-Boolean programming. The latter can be easily transformed to Maximum Satisfiability (MaxSAT) models. Our QIP approach formulates the objective function in a quadratic way, and the linear Pseudo-Boolean/MaxSAT approach reformulates the objective as a linear combination of Boolean variables. This linear combination is based on two weight functions, namely Direct Weight (DW) and Incremental Weight (IW). The efficiency of the proposed approaches is also thoroughly evaluated in numerical experiments.

The remainder of this paper is structured as follows. Section 2 establishes
the formal definitions, notations, and theoretical foundations of Diverse SAT,
along with the introduction of the standard Quadratic Integer Programming
(QIP), linear programming and Maximum Satisfiability (MaxSAT) paradigms.
Section 3 introduces our exact approaches, including the QIP formulation, the
linear formulation, and the adapted MaxSAT formulation. Section 4 provides a
comprehensive analysis of our experimental results. Finally, Section 5 summa-
rizes our contributions and outlines directions for future research.
# 2 Preliminaries

## 2.1 (Diverse) Satisfiability

Let $X$ be a set of Boolean variables taking values in $\{True, False\}$ (or $\{1,0\}$). A literal $l$ is either a variable $x \in X$ or its negation $\bar{x}$. The positive literal $l = x$ is referred to as satisfied (falsified) when $x$ is True (False), while the negative literal $l = \bar{x}$ is satisfied (falsified) when $x$ is False (True). A clause $C$ is a disjunction ($\vee$) of literals and can be represented as a set of literals. For convenience, we can write $C$ as $C^+ \cup C^-$, where $C^+$ is the set of positive literals and $C^-$ is the set of negative literals. $C$ is satisfied if at least one of its literals is satisfied. A formula in Conjunctive Normal Form (CNF) is a conjunction ($\wedge$) of clauses. We often write a CNF $\phi$ with $m$ clauses as a set of clauses, e.g, $\phi = \{C_1, \dots, C_m\}$. It is satisfied if all of its clauses are satisfied. Given a CNF formula $\phi$ containing Boolean variables in $X$, the propositional Satisfiability (SAT) problem consists in determining whether there exists an assignment $\alpha : X \to \{True, False\}$ satisfying $\phi$. When such an assignment exists, it is called a model of $\phi$.

Hereafter, we formally introduce the notions of Hamming distance between two assignments, which equals the number of variables taking different values in the two assignments. Then, we formally define the notion of diversity for a set of assignments, which corresponds to the sum of pairwise Hamming distances among pairs of distinct assignments. This notion is necessary to the introduction of the diverse satisfiability problem.

**Definition 1 (Hamming Distance of Assignments).** Given a set of Boolean variables $X$ and two assignments $\alpha_1, \alpha_2$ of the variables in $X$, the Hamming distance between $\alpha_1$ and $\alpha_2$, denoted $\text{Dis}(\alpha_1, \alpha_2)$, is defined as follows:

$$ \text{Dis}(\alpha_1, \alpha_2) = |\{x \in X \mid \alpha_1(x) \neq \alpha_2(x)\}| = \sum_{x \in X} |\alpha_1(x) - \alpha_2(x)| $$

**Definition 2 (Diversity of Assignments).** Given a set of Boolean variables $X$ and a set $A = \{\alpha_1, \dots, \alpha_k\}$ of $k$ assignments of the variables in $X$, the diversity of $A$, denoted $\text{Div}(A)$ is defined as follows:

$$ \text{Div}(A) = \sum_{i=1}^{k-1} \sum_{j=i+1}^{k} \text{Dis}(\alpha_i, \alpha_j) \quad (1) $$

Given a CNF formula $\phi$ and an integer $k \ge 2$, the Diverse Satisfiability (Diverse SAT) problem thus consists in finding a set of $k$ models of $\phi$ with maximal diversity. More formally, we seek:

$$ A = \arg\max_{\substack{A \in \{0,1\}^{k \times |X|} \\ \forall \alpha \in A, \alpha \text{ model of } \phi}} \text{Div}(A) $$

In [24], Nadel introduces the notion of variable diversity, i.e., the number of its True assignments times the number of its False assignments, as formally defined below. This notion served as an online criteria to evaluate the devotion of a
single variable to the overall diversity quality, finally leading to the variable-based heuristic proposed by Nadel. We formalize the idea behind this design in Proposition 1 and present the corresponding formal proof, which was not explicitly described in [24].

**Definition 3 (Variable Diversity).** Given a set of Boolean variables X and a set A = {$\alpha_1, \dots, \alpha_k$} of k assignments of the variables in X. The diversity of x ∈ X in A, denoted Div(x, A), is defined as follows:

$$Div(x, A) = T(x, A) \cdot F(x, A)$$
$$\text{where } T(x, A) = |\{\alpha \in A | \alpha(x) = 1\}|, \text{ and } F(x, A) = |\{\alpha \in A | \alpha(x) = 0\}|.$$

**Proposition 1.** Given a set of Boolean variables X and a set A = {$\alpha_1, \dots, \alpha_k$} of k assignments of the variables in X, we have:

$$Div(A) = \sum_{x \in X} Div(x, A) \qquad (2)$$

*Proof.*

$$ 
\begin{align*}
Div(A) &= \sum_{i=1}^{k-1} \sum_{j=i+1}^{k} Dis(\alpha_i, \alpha_j) \\
&= \sum_{i=1}^{k-1} \sum_{j=i+1}^{k} |\{x \in X \mid \alpha_i(x) \neq \alpha_j(x)\}| \\
&= \sum_{i=1}^{k-1} \sum_{j=i+1}^{k} \sum_{\substack{x \in X: \\ \alpha_i(x) \neq \alpha_j(x)}} 1 \\
&= \sum_{x \in X} \sum_{i=1}^{k-1} \sum_{\substack{j=i+1: \\ \alpha_i(x) \neq \alpha_j(x)}}^{k} 1 \\
&= \sum_{x \in X} T(x, A) \cdot F(x, A) = \sum_{x \in X} Div(x, A)
\end{align*}
$$

□

## 2.2 Quadratic and Linear Integer Programming

Quadratic Integer Programming (QIP) enables to represent mathematical programming models with integer variables, a quadratic objective function and linear constraints. As defined in [27], below is the formal form of a QIP model:

$$ 
\begin{array}{ll}
(QIP) & \max_x x^\top H x + c^\top x \\
     & \text{s.t. } x \in \mathcal{P} \qquad x \in \mathbb{Z}^n
\end{array}
$$

where $H \in \mathbb{Q}^{n \times n}$ and is symmetric, $c \in \mathbb{Q}^n$, $\mathcal{P}$ is a polyhedron, represented as $\mathcal{P} = \{x : Ax \leq b\}$, $A \in \mathbb{Q}^{m \times n}$, $b \in \mathbb{Q}^m$. On the other hand, Integer Linear Programming is defined as a linear objective function and linear constraints over integer variables. When the variables are Boolean, it is commonly referred to as Linear Pseudo-Boolean (LPB) programming [12] and can be formalized as follows:

$$ 
\begin{array}{ll}
(LPB) & \max f(x_1, \dots, x_n) \\
     & \text{s.t. } f_j(x_1, \dots, x_n) \geq 0, \quad j \in \{1, \dots, m\} \quad x_i \in \{0, 1\}^n
\end{array}
$$

where $f(x_1, \dots, x_n) = \sum_{i=1}^{n} w_i \cdot x_i$ and $w_i \in \mathbb{Z}$ are integer weights.
## 2.3 Maximum Satisfiability

Maximum Satisfiability (MaxSAT) is a natural optimization extension of SAT (another optimization extension of SAT is MinSAT [18]). In this paper, we use its most generic version, namely Weighted Partial MaxSAT [4, 17]. This problem takes as input a bipartite weighted formula $\phi = H \cup S$, where $H$ is a set of hard clauses that must be satisfied as in SAT, and $S$ is a set of weighted soft clauses of the form $(C, W_C)$, in which $W_C$ is a positive integer weight associated with the clause $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$ satisfying all hard clauses in $H$, Weighted Partial MaxSAT seeks $optimum(\phi) = \min_{\alpha} cost_{\alpha}(\phi)$. In the rest of the paper, we use MaxSAT to refer to its Weighted Partial variant. Additionally, previous literature introduces Pseudo-Boolean (PB) constraints that can be efficiently encoded in CNF form [28]. These constraints take the following form:

$$ \sum_j a_j \cdot l_j \triangleright b \quad \text{where } a_j \in \mathbb{N}, b \in \mathbb{N}, l_j \text{ is a literal and } \triangleright \in \{=, \geq, \leq\}. $$

A special kind of Pseudo-Boolean constraint is referred to as a cardinality constraint when all the coefficients of literals are equal to one [28]. For the remainder of this paper, we distinguish between the cardinality constraints and Pseudo-Boolean constraints based on the presence of literal coefficients, i.e., formulations without coefficients are treated as cardinality constraints.

# 3 Formulations for Diverse Satisfiability

In this section, we present three distinct formulations for the Diverse SAT problem, namely the Quadratic Integer Programming formulation and two linear (Pseudo-Boolean) formulations. We start with a QIP formulation presented in Section 3.1, transforming the original optimization naturally into a quadratic objective function. In Section 3.2, we discuss the general idea of bridging the gap between the formulation with integer variables and quadratic objective, and the formulation with Boolean variables and linear objective, therefore leading to the two models proposed in Section 3.3. Finally, we showcase that the linear formulations can be adapted to MaxSAT in Section 3.4.

## 3.1 Quadratic Formulation for Diverse SAT

In this subsection, we present a QIP formulation for the Diverse SAT problem. This formulation is naturally based on Proposition 1, which expresses the diversity of a set of assignments as the sum of each variable's diversity. Based on this idea, we define a QIP model with the following two series of variables, where $K = \{1, \dots, k\}$ corresponds to the $k$ models and $N = \{1, \dots, n\}$ corresponds to the $n$ variables:
$$ \max \sum_{j \in N} O_j \cdot (k - O_j) \qquad (\text{QIP-0}) $$

subject to

$$ \sum_{\bar{x}_j \in C_h^-} (1 - V_{i,j}) + \sum_{x_j \in C_h^+} V_{i,j} \geq 1 \quad \forall (i, h) \in K \times M \qquad (\text{QIP-1}) $$

$$ O_j = \sum_{i=\{1, \dots, K\}} V_{i,j} \quad \forall j \in N \qquad (\text{QIP-2}) $$

$$ O_j \in \mathbb{N}^+, V_{i,j} \in \{0, 1\} \quad \forall (i, j) \in K \times N \qquad (\text{QIP-3}) $$

<caption>Fig. 1: The QIP model for Diverse SAT</caption>

- **Integer variables** $O_j \quad \forall j \in N$: the number of *True* assignments of the j-th variable among all the k models, i.e., $T(x_j, A)$.

- **Binary variables** $V_{i,j} \quad \forall (i,j) \in K \times N$: the Boolean value for the j-th variable of the i-th model, i.e., $\alpha_i(x_j)$.

We obtain the formulation shown in Fig. 1, denoted QP, and where $M = \{1, \dots, m\}$ corresponds to the $m$ clauses in the given CNF formula $\phi$. Equation QIP-0 is a reformulation of Proposition 1, dictating that the maximization objective, diversity, equals the sum of all variable diversity. Equation QIP-1 ensures that all of the constructed $k$ assignments in $A$ are feasible models of $\phi$. Equation QIP-2 links the Boolean variables $V$ and the integer variables $O$. This QIP formulation requires $O(k \cdot n)$ variables and $O(k \cdot m + n)$ constraints.

## 3.2 Bridging Quadratic and Linear Formulations

In the last subsection, the proposed QIP formulation naturally relies on integer variables along with a quadratic objective function, which matches the original form of Proposition 1. However, the quadratic term in the objective function leaves a heavy burden on the solving procedure. Therefore, in this subsection, we propose an alternative plan that transforms the QIP formulation into a linear formulation. For each original Boolean variable $x_j \in X$ in the given CNF formula $\phi$, we first introduce a series of auxiliary Boolean variables to represent the number of *True* assignments of $x_j$ throughout the $k$ models, i.e., $T(x_j, A)$. Note that the mapping relationship between the auxiliary Boolean variables and the integer $T(x_j, A)$ has to cooperate with the weight functions.

Next, we develop two distinct weight functions, namely *Direct Weight (DW)* and *Incremental Weight (IW)*, to reformulate the original quadratic objective term $Div(x_j, A) = T(x_j, A) \cdot (k - T(x_j, A))$. An illustration of the two weight functions for a scenario of $k = 10$ models is shown in Fig. 2. The first weight function *DW* directly associates each possible value of $T(x_j, A)$ with its corresponding contribution to diversity. The blue points distributed on the parabolic curve showcase that the diversity peak appears when the variables $x_j$ are assigned *True* in exactly half of the models. The second weight function *IW* takes an incremental approach, expressing $Div(x_j, A)$ as a sum of marginal contributions. The red points in Fig. 2 represent the change in the diversity value
<figure><img src="image_2.png" /><figcaption>Fig. 2: The two weight functions DW and IW for a scenario with $k = 10$ Models</figcaption></figure>

when $T(x_j, A)$ increases by one. Note that these incremental values become negative after the midpoint, reflecting the diminishing returns of additional True assignments beyond balanced distribution. Formally, considering $r = T(x_j, A)$, we define the DW function as follows:

$$ \mathcal{D}_r = r \cdot (k-r) \quad \forall r \in \{0, \dots, k\} $$

and the IW function as:

$$ \mathcal{I}_r = \mathcal{D}_r - \mathcal{D}_{r-1} = -2r + k + 1 \quad \forall r \in \{1, \dots, k\} $$

Note that for any $r \in \{1, \dots, k\}$, $\mathcal{D}_r = \sum_{r'=1}^{r} \mathcal{I}_{r'}$, which can be simply proven with a telescoping sum. These two distinct weight functions provide different but mathematically equivalent approaches to reformulate the original objective function, which is detailed in the following subsection.

## 3.3 Linear Formulations for Diverse SAT

**Direct Weight Formulation** We first present the formulation for Diverse SAT with DW, which is built upon the following variables, where $K = \{1, \dots, k\}$ and $N = \{1, \dots, n\}$:

- Binary variables $U_{j,r} \quad \forall (r, j) \in (\{0\} \cup K) \times N: U_{j,r}$ is set to 1 when the number of True assignments of the j-th variable among all the K models equals to r, and to 0 otherwise.

$$ \max \sum_{j=1}^{n} \sum_{r=0}^{k} \mathcal{D}_r \cdot U_{j,r} \qquad (\text{DW-0}) $$

subject to

$$ \sum_{\bar{x}_j \in C_h^-} (1 - V_{i,j}) + \sum_{x_j \in C_h^+} V_{i,j} \geq 1 \quad \forall (i, h) \in K \times M \qquad (\text{DW-1}) $$

$$ \sum_{r \in \{(0) \cup K\}} U_{j,r} = 1 \quad \forall j \in N \qquad (\text{DW-2}) $$

$$ \sum_{r \in \{(0) \cup K\}} r U_{j,r} = \sum_{i \in K} V_{i,j} \quad \forall j \in N \qquad (\text{DW-3}) $$

$$ V_{i,j} \in \{0, 1\}, U_{j,r} \in \{0, 1\} \quad \forall (i, j) \in K \times N, \forall (r, j) \in (\{0\} \cup K) \times N \qquad (\text{DW-4}) $$

<caption>Fig. 3: Linear model for Diverse SAT with Direct Weight (DW).</caption>
$$ \max \sum_{j=1}^{n} \sum_{r=0}^{k} \mathcal{I}_r \cdot U_{j,r} \qquad (\text{IW-0}) $$

subject to

$$ \sum_{\bar{x}_j \in C_h^-} (1 - V_{i,j}) + \sum_{x_j \in C_h^+} V_{i,j} \geq 1 \quad \forall (i, h) \in K \times M \qquad (\text{IW-1}) $$

$$ U_{j,r} \le U_{j,r-1} \quad \forall (r, j) \in (K \setminus \{1\}) \times N \qquad (\text{IW-2}) $$

$$ \sum_{r \in K} U_{j,r} = \sum_{i \in K} V_{i,j} \quad \forall j \in N \qquad (\text{IW-3}) $$

$$ V_{i,j} \in \{0, 1\}, U_{j,r} \in \{0, 1\} \quad \forall (i,j) \in K \times N, \forall (r,j) \in K \times N \qquad (\text{IW-4}) $$

<caption>Fig. 4: Linear model for Diverse SAT with Incremental Weight (IW).</caption>

- Binary variables $V_{i,j} \quad \forall (i,j) \in K \times N$: the Boolean value for the j-th variable of the i-th model, i.e., $\alpha_i(x_j)$.

Therefore, the formulation with the DW function $D_r = r \cdot (k - r)$ can be obtained as in Fig. 3, where $M = \{1, \dots, m\}$. Equation DW-0 formulates the objective function, where each term $D_r \cdot U_{j,r}$ indicates that there is a diversity contribution $D_r = r \cdot (k - r)$ when variable $x_j$ is assigned to True in exactly $r$ out of $k$ models. Equation DW-1 ensures that each model $\alpha_i$ satisfies the original CNF formula $\phi$, i.e., for each clause $C_h$ in $\phi$ and each model $\alpha_i$, at least one literal in the clause must be satisfied according to the variable assignments in $\alpha_i$. Equation DW-2 enforces a single number of True assignments of the j-th variable among the k models. Equation DW-3 establishes the mapping relationship between the $U_{j,r}$ and the actual model assignments $V_{i,j}$. There are $\mathcal{O}(k \cdot n)$ variables and $\mathcal{O}(k \cdot m + n)$ constraints in the formulation of DW.

**Incremental Weight Formulation** We develop another formulation for Diverse SAT using the IW function. The variables used in this formulation are:

- Binary variables $U_{j,r} \quad \forall (r, j) \in K \times N$: $U_{j,r}$ is set to 1 when the number of True assignments of the j-th variable among all the K models is larger than or equal to r, and to 0 otherwise.

- Binary variables $V_{i,j} \quad \forall (i,j) \in K \times N$: the Boolean value for the j-th variable of the i-th model, i.e., $\alpha_i(x_j)$.

The linear Pseudo-Boolean formulation with the IW function $\mathcal{I}_r = -2r+k+1$ is obtained as shown in Fig 4. The structure of IW remains similar to DW. Equation IW-0 formulates the incremental contribution of the True assignments of the j-th variable $x_j$ to the overall diversity. Equation IW-1 constrains the satisfiability of all obtained k models. Equation IW-2 ensures the order of the usage of $U_{j,r}$, which cooperates with IW-3 to establish the semantic information of $U_{j,r}$. The complexities in terms of the numbers of variables and constraints for IW are $\mathcal{O}(n \cdot k)$ and $\mathcal{O}(k \cdot (m + n))$, respectively.
<figure><img src="image_3.png" /><figcaption>Fig. 5: The MaxSAT Formulation for Diverse SAT with DW (a) and IW (b).</figcaption></figure>

## 3.4 MaxSAT Formulations

When focusing on the intrinsic requirement of Diverse SAT, one cannot omit the central task of obtaining Boolean satisfiability models - a task where MaxSAT might be intuitively better suited. In this subsection, we present the transformation from the previous linear formulations to MaxSAT. We reformulate the models in clause-like encodings along with PB/Cardinality constraints, as showcased in Figure 5. Additionally, we note that Equation (IW-0*) in the MaxSAT-IW model may contain negative weights, which does not fit in the original standard of MaxSAT. Therefore, it is transformed through the following equation:

$$ \left\{ \begin{array}{ll} (U_{j,i}, \mathcal{I}_r) & \mathcal{I}_r \ge 0, \\ (\bar{U}_{j,i}, -\mathcal{I}_r) & \mathcal{I}_r < 0, \end{array} \right. \quad \forall (r, j) \in K \times N \quad (\text{IW-0}) $$

An illustrative example is showcased below. This normalization technique allows us to represent the incremental weight function properly within the standard MaxSAT framework, which requires non-negative weights for all soft clauses.

**Example.** Suppose $k = 4$ and $n = 3$. According to the definition $\mathcal{I}_r = -2r + k + 1$, we have $\mathcal{I}_1 = 3$, $\mathcal{I}_2 = 1$, $\mathcal{I}_3 = -1$ and $\mathcal{I}_4 = -3$. For each variable $x_j$ where $j \in \{1, 2, 3\}$. Before normalization, the soft clause set is $S = \{(U_{j,1}, 3), (U_{j,2}, 1), (U_{j,3}, -1), (U_{j,4}, -3)\}$. After applying the normalization rule, we obtain $S = \{(U_{j,1}, 3), (U_{j,2}, 1), (\bar{U}_{j,3}, 1), (\bar{U}_{j,4}, 3)\}$. We can remark that the contribution of $x_j$ is formulated as $\text{obj}_{\text{ini}} = 3U_{j,1} + U_{j,2} - U_{j,3} - 3U_{j,4}$ before normalization, whereas it becomes $\text{obj}_{\text{norm}} = 3U_{j,1} + U_{j,2} + \bar{U}_{j,3} + 3\bar{U}_{j,4}$ after normalization. Since $\bar{U}_{j,r} = 1 - U_{j,r}$ for any Boolean variable, we can rewrite this as follows:

$$ \text{obj}_{\text{norm}} = 3U_{j,1} + U_{j,2} + (1 - U_{j,3}) + 3(1 - U_{j,4}) = 3U_{j,1} + U_{j,2} - U_{j,3} - 3U_{j,4} + 4 = \text{obj}_{\text{ini}} + 4 $$

As adding a constant to all objective values does not change the optimal solution of a MaxSAT problem, the normalized formulation is equivalent to the original one in terms of finding the optimal diverse set of models.

## 4 Experimental Results

In this section, we present the experimental results of the proposed approaches. The experimental protocol, including the experimental environment, benchmarks,
and solvers involved, is presented in Section 4.1. Section 4.2 reports the overall performance, and Section 4.3 compares the linear formulations empowered by the two distinct weight functions.

## 4.1 Experiment Protocol

All the experiments were conducted on the MatriCS platform<fnref n="1" />, with a CentOS 8.6 system equipped with an Intel Xeon E5-2680 v4 processor operating at a base frequency of 2.40 GHz with Turbo Boost capability up to 3.30 GHz. The cutoff time set for all methodologies is 7200 seconds. Our experiments involve state-of-the-art solvers in each category. The QIP formulation proposed in 3.1 is solved by CPLEX [14]. The experiments of linear formulations proposed in 3.3 were conducted by both CPLEX and the dedicated Pseudo-Boolean solver RoundingSAT<fnref n="2" /> [10]. The two MaxSAT formulations proposed in 3.4 are tested on the three MaxSAT solvers CASHWMaxSAT-DisjCom [26], WMaxCDCL [19], and MaxHS [25]. We note that these three MaxSAT solvers are respectively SAT-based, Branch-and-Bound-based, and ILP-based solvers, and were the winners of the exact track in previous MaxSAT Evaluations<fnref n="3" /> held respectively in 2024, 2023, 2021. To perform the CNF encoding, we used PySAT<fnref n="4" /> [15, 16], with cardinality constraints encoded by Cardinality Networks [3], which is capable of encoding a constraint of $N$-literal $K$-cardinality in $O(N \log^2 K)$ clauses and auxiliary variables. For the PB constraints, we select the mode of "Best" available in PySAT. Additionally, we establish a naive enumeration approach based on state-of-the-art SAT solver CaDiCal [5]. The implementation logic of this approach is simple, with the SAT solver launched iteratively for $k$ times and, after each iteration, a new clause is added to the formula to block the newly found satisfiable assignment. Once the $k$ rounds are finished, we suspend the program and calculate the diversity based on the obtained $k$ models.

The instances used in our experiment originate from three sources: there are 20 instances from the semiformal verification of hardware benchmark first proposed and used in [24], 88 instances from SATLIB<fnref n="5" /> [13] composing 5 families, and 181 instances from the Model Counting (MC) competition<fnref n="6" /> held in 2024 [11], making up the 7 distinct families involved in the experiment. We omit instances with more than 100,000 variables and instances where 10 models cannot be computed by CaDiCal within the cutoff time, therefore all instances used guarantee that more than 10 distinct models exist. The scales of these instances vary from 39 variables and 66 clauses to 84914 variables and 7490695 clauses. In Table 1, for each family, we list out the original source, the number of instances #Ins, the average number of variables #Var<sub>avg</sub> and clauses #CL<sub>avg</sub>, and the average length of clauses Len<sub>avg</sub>. Three different $k$ values, $k = 2, 5, 10$ are tested.

<footnote n="1">¹ https://www.matrics.u-picardie.fr</footnote>

<footnote n="2">² https://gitlab.com/MIAOresearch/software/roundingsat</footnote>

<footnote n="3">³ https://maxsat-evaluations.github.io/</footnote>

<footnote n="4">⁴ https://pysathq.github.io/</footnote>

<footnote n="5">⁵ https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html</footnote>

<footnote n="6">⁶ https://mccompetition.org/past iterations</footnote>
## 4.2 Overall Performance

Figure 6 provides a comprehensive view of each approach's accumulated number of solved instances within the time limit under $k = 2, 5, 10$. We can observe that all of the proposed approaches manage to obtain optimal solutions for a considerable number of instances, especially for the smaller $k$ value of 2. In particular, the linear formulations, empowered by both *DW* and *IW* weight functions, outperform QIP and achieve the best performances for all $k$ values. The advantage is even enlarged as the $k$ value increases, demonstrating good scalability of the linear approaches. Nevertheless, it is notable that in several cases, even though the QIP formulation with CPLEX manages to find the optimal value proven by some other solvers, it fails to prove its optimality, with 34, 31, and 19 instances, respectively, when $k = 2, 5, 10$. Despite the fact that CPLEX with QIP formulation falls behind the others, when cooperating with the linear formulations, CPLEX becomes the most powerful solver, obtaining the most optimal solutions in both the case of $k = 2$ and $k = 10$, whereas the solver CASHWMaxSAT achieves the best performance when $k = 5$.

Tables 2, 3, and 4 showcase the quality analysis of all the approaches tested for all the families within the benchmark, with $k = 2, 5, 10$, respectively. For each instance family, the diversity of the results obtained by the naive enumeration approach cooperating with CaDiCaL (CaDi.) is first reported. Consequently, the performances of the QIP approach empowered by CPLEX and the two linear models with two different weight functions (*DW* and *IW*) solved by CPLEX, RoundingSAT and the three MaxSAT solvers CASHWMaxSAT (CASH.), MaxHS and WMaxCDCL, are reported under the format `#OPT(tot_timeopt)[Divall]`, where `#OPT` represents the number of optimally solved instances within the cutoff time, `tot_timeopt` is the corresponding average runtime of these optimally solved cases and *Divall* the average diversity values

<figure><img src="image_4.png" /><figcaption>Fig. 6: Cumulative solved number of instances with respect to solving time in seconds for the proposed approaches.</figcaption></figure>
obtained for all instances in each family. In the cases where there is no feasible solution computed within the cutoff time, the diversity is regarded as 0 for the corresponding instance. Among all our approaches, the one with the highest number of optimally solved instances within the shortest time is reported in bold. Furthermore, the highest overall diversity $Div_{all}$ among all the approaches, including the naive enumeration cooperating with CaDiCaL, is underlined.

These tables present the performance in terms of the optimality solving capability of the approaches and their ability to compute more diverse solutions. Overall, these results demonstrate that the choice of solver and weight functions significantly impacts performance, with different combinations showing superior results depending on the given cases. In terms of diversity, for $k = 2, 5, 10$, the best diversity obtained by exact solvers is 3.70, 2.18, and 1.68 times better than the naive solution obtained by enumeration, when narrowing down the analysis scale to the cases with proven optimality, these data alter to 94, 57, and 9 times improvement. The substantial performance gap between the naive enumerator and the proposed exact approaches clearly demonstrates the inherent difficulty of the Diverse SAT, affirming the necessity of developing exact approaches for this challenging problem. We can also observe that with the increase of the value of $k$, for some instance families, the proposed exact approaches sometimes fail to obtain any feasible solutions within the cutoff time, which is especially the case for CPLEX-QIP and RoundingSAT. This might be owing to the fact that the internal goal of the exact solvers is to obtain the optimal solutions, so the incomplete intermediate result cannot fully reflect the solving process. For example, the *IW* empowered by CPLEX only manages to obtain 4 feasible results for the difficult family *hardware* when $k = 5$, but all of these results are optimal. Despite this perspective, the proposed approaches are still serving satisfying quality in the sub-optimal solutions, which showcases great robustness.

## 4.3 Direct vs Incremental Weight

To better understand the practical differences between the two proposed weight functions *DW* and *IW*, we conduct a detailed comparison of their performance across different instance families and solver configurations. Figure 7 showcases the runtime comparisons for the two different functions under $k = 2, 5, 10$. Each point in the illustrations corresponds to an instance, with its coordinates determined by the runtime using the two weight functions. When an instance cannot be solved within the cutoff time, the corresponding solving time is regarded as the cutoff time. Points below the diagonal indicate instances where *IW* performed better, while points above the diagonal are in favor of *DW*. We can observe that the distributions of points follow distinct trends when the value of $k$ varies. When $k = 2$, *DW* is comparable with *IW*, with 76%, 45%, 34%, 47%, and 55% points lying under or on the diagonal line with the solvers CPLEX, RoundingSAT, CASHWMaxSAT, MaxHS, and WMaxCDCL, respectively. As $k$ increases to 5 (10), we can find a trend where *IW* outperforms *DW* with the percentage of points of 70%, 64%, 63%, 71%, and 76% (67%, 54%, 73%, 61%, and 91%) lying
<table><caption>Table 1: Information of instances families.</caption><thead><tr><th>Family</th><th>Source</th><th>#Ins</th><th>#Var<sub>avg</sub></th><th>#CL<sub>avg</sub></th><th>Len<sub>avg</sub></th></tr></thead><tbody><tr><td>ais</td><td>SATLIB</td><td>4</td><td>155</td><td>2729</td><td>2.31</td></tr><tr><td>flat100+</td><td>SATLIB</td><td>30</td><td>425</td><td>1584</td><td>2.09</td></tr><tr><td>flat100-</td><td>SATLIB</td><td>30</td><td>155</td><td>561</td><td>2.09</td></tr><tr><td>hardware</td><td>[24]</td><td>20</td><td>49391</td><td>161547</td><td>2.41</td></tr><tr><td>logistics</td><td>SATLIB</td><td>4</td><td>1881</td><td>11682</td><td>2.55</td></tr><tr><td>mc2024</td><td>MC competition</td><td>181</td><td>6348</td><td>97255</td><td>3.00</td></tr><tr><td>morphed</td><td>SATLIB</td><td>20</td><td>500</td><td>3100</td><td>2.10</td></tr><tr><td>Total</td><td>-</td><td>289</td><td>7516</td><td>72727</td><td>2.69</td></tr></tbody></table>

<table><caption>Table 2: Experimental results for $k = 2$.</caption><thead><tr><th rowspan="2">Family</th><th> Enum. </th><th colspan="3"> CPLEX </th><th colspan="2"> RoundingSAT </th><th colspan="2"> MaxSAT (DW) </th><th colspan="2"> MaxSAT (IW) </th></tr><tr><th> CaDi. </th><th> QIP </th><th> DW </th><th> IW </th><th> DW </th><th> IW </th><th> CASH. </th><th> MaxHS WMaxCDCL </th><th> CASH. </th><th> MaxHS WMaxCDCL </th></tr></thead><tbody><tr><td> ais </td><td> [18] </td><td> 1(4)[6] </td><td> 4(49)[34] </td><td> <b> 4(15)[34] </b> </td><td> 1(41)[8] </td><td> 2(15)[13] </td><td> 2(2)[34] </td><td> 3(19)[34] </td><td> 4(1656)[34] </td><td> 2(2)[34] </td><td> 3(23)[34] </td><td> 3(73)[22] </td></tr><tr><td> flat100+ </td><td> [2] </td><td> 1(6685)[63] </td><td> 30(35)[283] </td><td> 30(24)[283] </td><td> <b> 30(0)[283] </b> </td><td> 30(0)[283] </td><td> 30(1)[283] </td><td> 30(16)[283] </td><td> 30(4)[283] </td><td> 30(1)[283] </td><td> 30(3)[283] </td><td> 30(6)[283] </td></tr><tr><td> flat100- </td><td> [2] </td><td> 23(291)[73] </td><td> 30(0)[103] </td><td> 30(0)[103] </td><td> 23(0)[82] </td><td> 22(0)[74] </td><td> <b> 30(0)[103] </b> </td><td> 30(0)[103] </td><td> 30(1)[103] </td><td> 30(0)[103] </td><td> 30(0)[103] </td><td> 30(1)[103] </td></tr><tr><td> hardware </td><td> [5483] </td><td> 0(-)[596] </td><td> 4(62)[1177] </td><td> 4(49)[1180] </td><td> 0(-)[0] </td><td> 4(194)[558] </td><td> <b> 4(9)[19705] </b> </td><td> 0(-)[18835] </td><td> 0(-)[0] </td><td> 4(11)[20556] </td><td> 0(-)[18381] </td><td> 0(-)[0] </td></tr><tr><td> logistics </td><td> [3] </td><td> 1(5531)[216] </td><td> <b> 3(19)[365] </b> </td><td> 3(36)[368] </td><td> 2(290)[136] </td><td> 2(3643)[148] </td><td> 2(57)[352] </td><td> 3(95)[364] </td><td> 2(166)[218] </td><td> 2(22)[362] </td><td> 2(152)[366] </td><td> 1(19)[218] </td></tr><tr><td> mc2024 </td><td> [579] </td><td> 32(671)[587] </td><td> 82(695)[845] </td><td> 87(542)[832] </td><td> 67(307)[464] </td><td> 67(273)[436] </td><td> <b> 89(364)[1965] </b> </td><td> 79(379)[2223] </td><td> 80(582)[493] </td><td> 87(295)[1980] </td><td> 79(426)[2177] </td><td> 75(379)[441] </td></tr><tr><td> morphed </td><td> [2] </td><td> 0(-)[0] </td><td> 20(3)[200] </td><td> <b> 20(1)[200] </b> </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 4(2739)[198] </td><td> 19(9)[200] </td><td> 20(1230)[200] </td><td> 2(525)[200] </td><td> 1(8)[200] </td><td> 0(-)[0] </td></tr></tbody><tfoot><tr><td> Total </td><td> [743] </td><td> 58(696)[426] </td><td> 173(339)[670] </td><td> <b> 178(271)[662] </b> </td><td> 123(172)[330] </td><td> 127(208)[351] </td><td> 161(270)[2654] </td><td> 164(188)[2755] </td><td> 166(472)[366] </td><td> 157(171)[2722] </td><td> 145(235)[2695] </td><td> 139(208)[320] </td></tr></tfoot></table>

<table><caption>Table 3: Experimental results for $k = 5$.</caption><thead><tr><th rowspan="2">Family</th><th> Enum. </th><th colspan="3"> CPLEX </th><th colspan="2"> RoundingSAT </th><th colspan="2"> MaxSAT (DW) </th><th colspan="2"> MaxSAT (IW) </th></tr><tr><th> CaDi. </th><th> QIP </th><th> DW </th><th> IW </th><th> DW </th><th> IW </th><th> CASH. </th><th> MaxHS WMaxCDCL </th><th> CASH. </th><th> MaxHS WMaxCDCL </th></tr></thead><tbody><tr><td> ais </td><td> [280] </td><td> 0(-)[50] </td><td> 1(5834)[119] </td><td> 1(2348)[124] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 1(1610)[323] </td><td> 1(429)[314] </td><td> <b> 1(337)[124] </b> </td><td> 1(1952)[322] </td><td> 1(500)[326] </td><td> 1(379)[124] </td></tr><tr><td> flat100+ </td><td> [32] </td><td> 0(-)[59] </td><td> 22(2578)[1493] </td><td> 29(910)[2160] </td><td> <b> 30(3)[2267] </b> </td><td> 29(2)[2173] </td><td> 30(63)[2267] </td><td> 29(469)[2249] </td><td> 28(452)[2173] </td><td> 30(9)[2267] </td><td> 30(99)[2267] </td><td> 29(619)[2267] </td></tr><tr><td> flat100- </td><td> [50] </td><td> 0(-)[595] </td><td> 30(72)[827] </td><td> 30(3)[827] </td><td> <b> 30(1)[827] </b> </td><td> 29(0)[787] </td><td> 30(4)[827] </td><td> 30(119)[827] </td><td> 30(69)[827] </td><td> 30(1)[827] </td><td> 30(11)[827] </td><td> 30(71)[827] </td></tr><tr><td> hardware </td><td> [42853] </td><td> 0(-)[1919] </td><td> 3(5664)[3850] </td><td> <b> 4(1107)[3850] </b> </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 0(-)[89368] </td><td> 0(-)[82752] </td><td> 0(-)[0] </td><td> 0(-)[8173] </td><td> 0(-)[100673] </td><td> 0(-)[0] </td></tr><tr><td> logistics </td><td> [38] </td><td> 0(-)[0] </td><td> 0(-)[995] </td><td> 0(-)[1608] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 0(-)[2622] </td><td> 0(-)[2604] </td><td> 0(-)[0] </td><td> 0(-)[2836] </td><td> 0(-)[2806] </td><td> 0(-)[486] </td></tr><tr><td> mc2024 </td><td> [5875] </td><td> 25(544)[1477] </td><td> 49(253)[2231] </td><td> 51(402)[3012] </td><td> 56(556)[1831] </td><td> 57(268)[2477] </td><td> 57(157)[11542] </td><td> 56(205)[12568] </td><td> 57(391)[1874] </td><td> 61(149)[5063] </td><td> <b> 61(140)[11308] </b> </td><td> 56(240)[1892] </td></tr><tr><td> morphed </td><td> [30] </td><td> 0(-)[87] </td><td> 0(-)[1977] </td><td> 3(3486)[1985] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 20(3064)[2000] </td><td> 0(-)[1855] </td><td> 0(-)[0] </td><td> <b> 20(272)[2000] </b> </td><td> 3(2055)[2000] </td><td> 0(-)[0] </td></tr></tbody><tfoot><tr><td> Total </td><td> [6660] </td><td> 25(544)[1132] </td><td> 105(896)[2057] </td><td> 118(544)[2624] </td><td> 116(269)[1468] </td><td> 115(134)[1859] </td><td> 138(535)[13913] </td><td> 116(250)[14086] </td><td> 116(322)[1487] </td><td> <b> 142(118)[4240] </b> </td><td> 125(148)[14552] </td><td> 116(292)[1514] </td></tr></tfoot></table>

<table><caption>Table 4: Experimental results for $k = 10$.</caption><thead><tr><th rowspan="2">Family</th><th> Enum. </th><th colspan="3"> CPLEX </th><th colspan="2"> RoundingSAT </th><th colspan="2"> MaxSAT (DW) </th><th colspan="2"> MaxSAT (IW) </th></tr><tr><th> CaDi. </th><th> QIP </th><th> DW </th><th> IW </th><th> DW </th><th> IW </th><th> CASH. </th><th> MaxHS WMaxCDCL </th><th> CASH. </th><th> MaxHS WMaxCDCL </th></tr></thead><tbody><tr><td> ais </td><td> [1226] </td><td> 0(-)[0] </td><td> 0(-)[211] </td><td> 0(-)[211] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 0(-)[1348] </td><td> 0(-)[1272] </td><td> 0(-)[0] </td><td> 0(-)[507] </td><td> 0(-)[1366] </td><td> 0(-)[0] </td></tr><tr><td> flat100+ </td><td> [179] </td><td> 0(-)[20] </td><td> 5(3667)[1487] </td><td> <b> 16(2714)[3905] </b> </td><td> 0(-)[0] </td><td> 4(3755)[1705] </td><td> 0(-)[8956] </td><td> 0(-)[8323] </td><td> 0(-)[0] </td><td> 0(-)[9350] </td><td> 6(3420)[9350] </td><td> 0(-)[0] </td></tr><tr><td> flat100- </td><td> [337] </td><td> 0(-)[1501] </td><td> 30(488)[3410] </td><td> <b> 30(42)[3410] </b> </td><td> 0(-)[0] </td><td> 3(4821)[385] </td><td> 2(1015)[3410] </td><td> 0(-)[3224] </td><td> 7(4273)[594] </td><td> 21(1343)[3410] </td><td> 27(798)[3410] </td><td> 0(-)[264] </td></tr><tr><td> hardware </td><td> [105280] </td><td> 0(-)[0] </td><td> 0(-)[14790] </td><td> 0(-)[15886] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 0(-)[7138] </td><td> 0(-)[330172] </td><td> 0(-)[0] </td><td> 0(-)[15137] </td><td> 0(-)[42646] </td><td> 0(-)[0] </td></tr><tr><td> logistics </td><td> [208] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 0(-)[1942] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 0(-)[9496] </td><td> 0(-)[9230] </td><td> 0(-)[0] </td><td> 0(-)[1892] </td><td> 0(-)[9975] </td><td> 0(-)[0] </td></tr><tr><td> mc2024 </td><td> [28953] </td><td> 12(34)[2719] </td><td> 25(304)[6481] </td><td> 25(52)[8808] </td><td> 24(306)[1271] </td><td> 27(539)[1900] </td><td> 21(515)[8254] </td><td> 23(389)[29240] </td><td> 21(244)[925] </td><td> 25(447)[13934] </td><td> <b> 32(461)[31744] </b> </td><td> 21(384)[703] </td></tr><tr><td> morphed </td><td> [168] </td><td> 0(-)[0] </td><td> <b> 8(5629)[7988] </b> </td><td> 7(4466)[7993] </td><td> 0(-)[0] </td><td> 0(-)[0] </td><td> 0(-)[7386] </td><td> 0(-)[6548] </td><td> 0(-)[0] </td><td> 0(-)[6796] </td><td> 0(-)[6371] </td><td> 0(-)[0] </td></tr></tbody><tfoot><tr><td> Total </td><td> [25504] </td><td> 12(34)[1861] </td><td> 68(1259)[6147] </td><td> <b> 78(990)[7958] </b> </td><td> 24(306)[796] </td><td> 34(1295)[1407] </td><td> 23(558)[7608] </td><td> 23(389)[42960] </td><td> 28(1251)[641] </td><td> 46(856)[11603] </td><td> 65(874)[24755] </td><td> 21(384)[468] </td></tr></tfoot></table>
<figure><img src="image_5.png" /><figcaption>Fig. 7: Runtime comparison in logarithmic scale of the two weight functions IW and DW for $k = 2, 5, 10$. The color of each point corresponds to the scale (number of clauses) of the instance.</figcaption></figure>

under or on the diagonal line respectively. Based on the results throughout all values of *k*, we observe the advantage of *IW* over *DW* as *k* increases.

# 5 Conclusion

In this paper, we proposed exact approaches for the Diverse Satisfiability problem, based on Quadratic Integer Programming (QIP) and linear programming models, the latter of which was naturally adapted to Max-SAT formulations. Both approaches formulate the objective of Diverse SAT from a variable-wise diversity perspective. While the QIP model enables formulate the objective more naturally, the two linear approaches rely on two distinct, well-designed weight functions, namely direct weight and incremental weight, which manage to take advantage of both ILP and MaxSAT solvers’ inherent capability for solving complex linear optimization problems. Extensive experiments across different values of the parameter number of models *k* demonstrate the efficiency of our proposed methodologies and particularly show the advantage of linear formulations over the QIP formulation, the incremental weight achieving the best performance as the instances’ scale increases. As future work, we aim to explore the potential of designing dedicated algorithms for Diverse SAT that transcend the limitations of end-to-end solving schemes while preserving the structure and objective representation from our proposed approaches. Additionally, as we conduct experiments on an increasingly broader range of datasets, we anticipate establishing more optimal solutions for benchmarks to benefit researchers interested in this problem domain, which will also facilitate the design and evaluation of more efficient heuristic and approximation algorithms for Diverse SAT.
## 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. This work was also granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne. "Plateforme MatriCS" is co-financed by the European Union with the European Regional Development Fund (FEDER) and the Hauts-De-France Regional Council among others.

## References

1. Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, and Alexander Nadel. Sat-based semiformal verification of hardware. In Roderick Bloem and Natasha Sharygina, editors, *Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23*, pages 25–32. IEEE, 2010.

2. Ola Angelsmark and Johan Thapper. Algorithms for the maximum hamming distance problem. In Boi Faltings, Adrian Petcu, François Fages, and Francesca Rossi, editors, *Recent Advances in Constraints, Joint ERCIM/CoLogNet International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2004, Lausanne, Switzerland, June 23-25, 2004, Revised Selected and Invited Papers*, volume 3419 of *Lecture Notes in Computer Science*, pages 128–141. Springer, 2004.

3. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In Oliver Kullmann, editor, *Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings*, volume 5584 of *Lecture Notes in Computer Science*, pages 167–180. Springer, 2009.

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

5. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, *Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions*, volume B-2020-1 of *Department of Computer Science Report Series B*, pages 51–53. University of Helsinki, 2020.

6. 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.

7. Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, *Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings*, volume 2988 of *Lecture Notes in Computer Science*, pages 168–176. Springer, 2004.

8. Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, *Proceedings of the 3rd Annual ACM Symposium on Theory of Computing*, pages 151–158. ACM, 1971.
9. Pierluigi Crescenzi and Gianluca Rossi. On the hamming distance of constraint satisfaction problems. *Theor. Comput. Sci.*, 288(1):85-100, 2002.

10. Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-boolean solving. In Jérôme Lang, editor, *Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden*, pages 1291-1299. ijcai.org, 2018.

11. Johannes K Fichte, Markus Hecher, and Arijit Shaw. Model counting competition data format (version 1.1), 2024.

12. PL Hammer Ivànescu and S Rudeanu. Boolean methods in operations research and related areas. *Oekonometrie und Unternehmensforschung* (, 7, 1968.

13. Holger H Hoos and Thomas Stützle. Satlib: An online resource for research on sat. *Sat*, 2000:283-292, 2000.

14. IBM Corporation. *IBM ILOG CPLEX Optimization Studio*, 2022.

15. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In *SAT*, pages 428-437, 2018.

16. Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible SAT technology. In *SAT*, pages 4:1-4:11, 2024.

17. 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.

18. 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.

19. Shuolin Li, Chu Min Li, Jordi Coll, Djamal Habet, Felip Manyà, and Kun He. Wmaxcdcl in maxsat evaluation 2024. *MaxSAT Evaluation 2024 Solver and Benchmark Descriptions*, pages 17-18, 2024.

20. Jiaxin Liang, Junping Zhou, and Minghao Yin. Diversat: A novel and effective local search algorithm for diverse SAT problem. In Toby Walsh, Julie Shah, and Zico Kolter, editors, *AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA*, pages 11290-11298. AAAI Press, 2025.

21. Inês Lynce and João Marques-Silva. SAT in bioinformatics: Making the case with haplotype inference. In Armin Biere and Carla P. Gomes, editors, *Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings*, volume 4121 of *Lecture Notes in Computer Science*, pages 136-141. Springer, 2006.

22. Panagiotis Manolios, Marc Galceran Oms, and Sergi Oliva Valls. Checking pedigree consistency with PCS. In Orna Grumberg and Michael Huth, editors, *Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings*, volume 4424 of *Lecture Notes in Computer Science*, pages 339-342. Springer, 2007.

23. Neeldhara Misra, Harshil Mittal, and Ashutosh Rai. On the parameterized complexity of diverse sat. *arXiv preprint arXiv:2412.09717*, 2024.

24. Alexander Nadel. Generating diverse solutions in SAT. 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 287-301. Springer, 2011.

25. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Maxhs in maxsat evaluation 2022. *MaxSAT Evaluation 2022*, page 35, 2022.
26. Shiwei Pan, Yiyuan Wang, Shaowei Cai, Jiangnan Li, Wenbo Zhu, and Minghao Yin. Cashwmaxsat-disjcad: Solver description. *MaxSAT Evaluation 2024 Solver and Benchmark Descriptions*, page 25, 2024.

27. Alberto Del Pia, Santanu S Dey, and Marco Molinaro. Mixed-integer quadratic programming is in np. *Mathematical Programming*, 162:225–240, 2017.

28. 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.

29. 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.

30. 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.