# Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability

Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, Laure

Brisoux-Devendeville

► To cite this version:

Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, Laure Brisoux-Devendeville. Minimiz-
ing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability. 30th
International Conference on Principles and Practice of Constraint Programming (CP 2024), Sep 2024,
Girona, Spain. 10.4230/LIPIcs.CP.2024.34 . hal-04699557

HAL Id: hal-04699557

https://hal.science/hal-04699557v1

Submitted on 17 Sep 2024

**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>
# Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability

Sami Cherif

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

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

MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Heythem Sattoutah

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

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

MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Chu-Min Li

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

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

MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Corinne Lucet

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

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

MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Laure Brisoux-Devendeville

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

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

MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

## Abstract

This paper explores the application of Maximum Satisfiability (Max-SAT) to the complex problem of conference session scheduling, with a particular focus on minimizing working-group conflicts within the context of the ROADEF conference, the largest French-speaking event aimed at bringing together researchers from various fields such as combinatorial optimization and operational research. A Max-SAT model is introduced then enhanced with new variables, and solved through state-of-the-art solvers. The results of applying our formulation to data from ROADEF demonstrate its ability to effectively compute session schedules, while enabling to reduce the number of conflicts and the maximum number of parallel sessions compared to the handmade solutions proposed by the organizing committees. These findings underscore the potential of Max-SAT as a valuable tool for optimizing conference scheduling processes, offering a systematic and efficient solution that ensures a smoother and more productive experience for attendees and organizers alike.

**2012 ACM Subject Classification** Computing methodologies → Planning and scheduling; Computing methodologies → Logic programming and answer set programming

**Keywords and phrases** Maximum Satisfiability, Scheduling, Modeling

**Digital Object Identifier** 10.4230/LIPIcs.CP.2024.34

**Category** Short Paper

**Supplementary Material** Other (Source Code, Data, Benchmark):
https://github.com/satoutahhaithem/ROADEF_SCHEDULING [12]
archived at swh:1:dir:7083377094f69163d37d30b77d740c72c562139d

## 1 Introduction

The Maximum Satisfiability (Max-SAT) problem is a natural optimization extension of the well-known satisfiability (SAT) problem [9]. While SAT consists in verifying whether all the clausal constraints in a given propositional formula can be satisfied by an assignment of the variables, the goal in Max-SAT shifts to determining the maximum number of clausal constraints that can be satisfied. Although Max-SAT is NP-hard, the last decade has known major breakthroughs in Max-SAT theory and solving. Indeed, SAT-based algorithms [2, 18, 27] are able to harness the power of modern SAT solvers and particularly their ability to effectively compute cores, i.e. unsatisfiable subsets of the formula. More

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

© Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville; licensed under Creative Commons License CC-BY 4.0

30th International Conference on Principles and Practice of Constraint Programming (CP 2024).

Editor: Paul Shaw; Article No. 34; pp. 34:1–34:11

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

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
recently, Branch and Bound algorithms for Max-SAT have also gained a huge leap in
competitiveness with respect to other approaches through the introduction of a foundational
learning process tailored to Max-SAT [11, 22, 23]. This was coupled with new insights and
understanding of Max-SAT proof theory, paving the way for efficient solver certification for
Max-SAT [7, 29].

These recent advancements have made Max-SAT a powerful formalism that can be used
to model and effectively solve many real-world problems. In particular, Max-SAT has been
used to tackle applications in various domains such as security [31], hardware and software
debugging [25], data analysis [8] and bio-informatics [19] among many others. In particular,
in the context of scheduling, Max-SAT has been used for tackling Curriculum-based Course
Timetabling in [4] and [14], mainly for optimizing isolated lectures or resources in the schedule.
It was also used in [10] to avoid idle time periods in the scheduling of bilateral meetings as
well as in [15] to solve staff scheduling problems while taking into account requested and
unpreferred shifts. A Max-SAT formulation for scheduling tasks in overloaded real-time
systems by enforcing task deadlines as soft constraints is introduced in [24]. More recently, an
iterative and incremental Max-SAT approach has been introduced to solve train scheduling
optimization problems in [20]. These successful applications show the high potential of
Max-SAT as an effective paradigm to solve problems in the context of scheduling and beyond.

In this paper, we address a conference scheduling problem through the lens of Max-SAT. In particular, we aim to tackle a problem which has arisen during the organization of the ROADEF conference, the largest French-speaking event aimed at bringing together researchers from various domains, mainly the combinatorial optimization and operational research communities. Our work addresses a crucial gap in the organization of the esteemed conference where, despite its status as a gathering of premier scheduling experts, the planning process remains reliant on manual efforts, requiring significant human and time resources, even after 25 editions. Our objective is thus to provide an effective way for optimizing the conference scheduling process, thus enhancing the overall experience for conference attendees and organizers alike. To this end, we introduce a Max-SAT model to minimize the working-group conflicts in the scheduling of parallel sessions during the conference. Furthermore, we show how our model can be enhanced by introducing new variables. Our experimental evaluation shows that our formulation offers a systematic and efficient solution to the intricate challenges associated with our problem, ensuring a smoother and more productive experience for attendees and organizers as it enables to reduce the number of conflicts as well as the maximum number of parallel sessions compared to the handmade solutions proposed by the organizing committees.

This paper is organized as follows. Section 2 includes the necessary definitions and
notations. The problem context and parameters are presented in Section 3. Our dedicated
Max-SAT model and its enhanced formulation are introduced in Section 4. An experimental
evaluation on data from ROADEF is presented in Section 5. Finally, we conclude and discuss
future work in Section 6.

2 Preliminaries

Let $V$ be the set of propositional variables. A literal $l$ is a variable $x \in V$ or its negation $\bar{x}$. A clause is a disjunction of literals. A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses. An assignment $\alpha : V \to \{\text{true, false}\}$ maps each variable to a Boolean value and can be represented as a set of literals. A literal $l$ is satisfied by an assignment $\alpha$ if $l \in \alpha$, else it is falsified by $\alpha$. A clause is satisfied by an assignment $\alpha$ if
at least one of its literals is satisfied by $\alpha$, otherwise it is falsified by $\alpha$. The cost of an assignment $\alpha$, denoted $cost_\alpha(\phi)$, is the number of clauses in the formula $\phi$ falsified by $\alpha$. Solving the (plain) Max-SAT problem [6] consists in determining the maximum number of clauses that can be satisfied by an assignment of a given CNF formula $\phi$ or, equivalently, the minimum number of clauses that each assignment must falsify, i.e. $opt(\phi) = \min_{\alpha} cost_\alpha(\phi)$. In our formulation, we will particularly rely on the partial Max-SAT problem [21], which is a well-known variant taking as input a partial CNF formula, i.e. a bipartite set of clauses $\phi = H \cup S$ where $H$ is the set of hard clauses that must be satisfied and $S$ is the set of soft clauses to be optimized as in plain Max-SAT. The goal thus shifts to computing $opt(S)$ such that all the clauses in $H$ are satisfied. Finally, we note that, in the subsequent Max-SAT formulation, we will use Pseudo-Boolean (PB) constraints which enforce a constant bound on a weighted sum of literals as in $(\sum_{i=1}^h a_i * l_i) \circ k$ where $a_i, k \in \mathbb{N}$ and $\circ \in \{\leq, =, \geq\}$. In the case where all literals in the sum are variables in $V$ and all the weights are set to 1 (and thus can be discarded), such constraints are more commonly referred to as cardinality constraints. PB and cardinality constraints can be efficiently encoded in CNF form [30] and are typically used in Max-SAT solvers to enforce relevant bounds during the search [21]. For instance, the sorting network encoding [16] enables to encode PB and cardinality constraints using $O(\sum_{i=1}^h a_i \log^2(\sum_{i=1}^h a_i))$ new variables and clauses, i.e. $O(h \log^2(h))$ for cardinality constraints as $m = h$. Independently, the cardinality network encoding [3] can be more suited for cardinality constraints as it is in $O(h \log^2(k))$ while the BDD encoding [1], which is in $O(h^3 \log(max_{1 \leq i \leq h} a_i))$, can be more suitable for PB constraints.

## 3 ROADEF Scheduling

The ROADEF<fnref n="1" /> conference is the largest French-speaking event aimed at bringing together researchers from various domains, including combinatorial optimization, operational research, constraint programming and industrial engineering. This event is organized annually and welcomes around 600 participants, with the aim to foster exchanges and collaborations between researchers and industry professionals, as well as to contribute to the training of young researchers and encourage them to present their work to the national community. ROADEF includes plenary sessions, tutorials in semi-plenary sessions, multiple parallel sessions, industrial experience feedback sessions and the ROADEF general assembly. The conference also involves many working groups consisting of researchers collaborating on a national and potentially international level on specific themes covered by the conference, with each parallel session usually being organized by one or more of these working groups. In this paper, we focus on the scheduling of ROADEF parallel sessions into available time slots while avoiding clashes among research working groups. This problem arises each year during the event organization as each parallel session is usually scheduled to occur simultaneously with others, potentially causing overlaps and conflicts. Indeed, such overlaps not only prevent researchers from assisting to the sessions organized by their respective working groups but they may also pose constraints regarding session chair assignments.

Let $S$ be the set of conference sessions, $G$ be the set of working groups and $C$ be the set of available slots<fnref n="2" />. A parallel session can be allocated to multiple slots with a different number of papers allocated to each slot. We denote $L$ the set of authorized quantity of papers that can be allocated to a specific slot for each parallel session. We set $n$ as the maximum number

<footnote n="1">¹ https://www.roadef.org/roadef-le-congres-annuel</footnote>

<footnote n="2">² To simplify, each session, slot, or working group is referred to by a unique natural number identifier.</footnote>
<table><caption>Table 1 Summary of ROADEF Data for the last four years. #X denotes the number of X.</caption><thead><tr><th>Year</th><th>2024</th><th>2023</th><th>2022</th><th>2021</th></tr></thead><tbody><tr><td>#Sessions</td><td>40</td><td>47</td><td>42</td><td>27</td></tr><tr><td>#Working-groups</td><td>20</td><td>24</td><td>24</td><td>17</td></tr><tr><td>#Slots</td><td>7</td><td>7</td><td>8</td><td>11</td></tr><tr><td>Paper range L</td><td>{3,4,5,6}</td><td></td><td>{3,4,5}</td><td></td></tr><tr><td>#Papers</td><td>307</td><td>358</td><td>311</td><td>182</td></tr></tbody></table>

of parallel sessions for the available slots, which is fixed each year depending on the available resources. Note that, in general, a higher value for this parameter entails more complex logistics and more resources to manage the parallel sessions. For each session $s \in S$, we denote $np(s)$ and $W(s) \subseteq G$ respectively the number of papers and the set of working groups associated to session $s$. Finally, for each slot $c \in C$, we denote $npMax(c)$ the maximum number of authorized papers for each parallel session in slot $c$.

For instance, in 2024, the 25th edition of ROADEF<fnref n="3" /> was organized over three days in the city of Amiens. The conference comprised 40 programmed sessions<fnref n="4" />. It also involved the participation of 20 distinct working groups. Over the course of the three-day conference, there were seven parallel session slots. The organizing committee has decided that each parallel session was required to host at least three papers and at most six. Indeed, since the allocated presentation and question time per paper is 20 minutes, a session with less than 3 papers, i.e. less than one hour, would be too short while, one with more than 6 would be too long since a break would be expected after 2 hours. The maximum number of parallel sessions per slot can go up to 15 with respect to the available resources and mainly the available rooms in the conference site. For the lack of space, we do not report the maximum number of authorized papers for each slot nor the values of $np(s)$ and $W(s)$ for $s \in S$. However, we mention that there were a total of 307 papers accepted in the 2024 edition, split over the different sessions. To give an example, for session $s = 40$ dedicated to constraint programming, we have $np(s) = 8$ and $W(s) = \{7, 15\}$. The summary of Data from ROADEF over the last four years is reported in Table 1. Finally, we note that additional constraints for specific sessions may arise. In particular, the chairs of session 34 in the 2024 edition requested to assign their session presentations on the last day of the conference covered by slots 5, 6 and 7.

# 4 Maximum Satisfiability for Conference Session Scheduling

## 4.1 Basic Model

Our aim is to minimize the conflicts among working groups in the conference schedule while respecting all the schedule-related constraints. We start first by defining our main variables. More specifically, we set two types of variables to represent the allocation of parallel sessions and to compute the conflicts as follows:

- $x_{(s,c,l)}$ is set to true if session $s \in S$ is allocated to slot $c \in C$ with $l \in L$ papers

- $y_{(s_1,s_2,c,g)}$ is set to true if there is a conflict in slot $c \in C$ for working group $g \in G$ associated to the pair of sessions $(s_1, s_2) \in S^2$ such that $s_1 < s_2$ and $g \in W(s_1) \cap W(s_2)$

<footnote n="3">³ https://roadef2024.sciencesconf.org/</footnote>

<footnote n="4">⁴ 50 parallel sessions were initially programmed in 2024 but 6 were canceled for lack of submissions and 4 were merged with other sessions for insufficient number of submissions.</footnote>
Since we want to reduce the number of group conflicts in the conference, we clearly need to minimize the number of satisfied y variables. We can therefore define the set of soft clauses accordingly as follows:

$$ \phi_{soft} = \bigwedge_{\substack{(s_1,s_2,c,g) \in S \times S \times C \times G \\ s_1 < s_2 \\ g \in W(s_1) \cap W(s_2)}} \overline{y(s_1,s_2,c,g)} $$

Next, we state the constraints that will be added to the hard clause set $\phi_{hard}$ of the formula:

- At most one quantity of papers can be chosen for each (session, slot) pair:

$$ \sum_{l \in L} x_{(s,c,l)} \leq 1 \quad \forall (s,c) \in S \times C \qquad (1) $$

- The subdivision of a session into slots covers all the papers in the session:

$$ \sum_{\substack{c \in C \\ l \in L}} x_{(s,c,l)} * l = np(s) \quad \forall s \in S \qquad (2) $$

- The allocation of a session to a slot c is valid if $npMax(c)$ is not exceeded:

$$ \bigwedge_{\substack{l \in L \\ l > npMax(c)}} \overline{x(s, c, l)} \quad \forall (s, c) \in S \times C \qquad (3) $$

- The maximum number of parallel sessions per slot is not exceeded:

$$ \sum_{\substack{s \in S \\ l \in L}} x_{(s,c,l)} \leq n \quad \forall c \in C \qquad (4) $$

- Two sessions associated to the same group and allocated to the same slot generate a conflict:

$$ \bigwedge_{(l_1, l_2) \in L^2} \overline{x_{(s_1, c, l_1)}} \lor \overline{x_{(s_2, c, l_2)}} \lor y_{(s_1, s_2, c, g)} \qquad (5) $$

$$ \forall (s_1, s_2, c, g) \in S^2 \times C \times G \text{ s.t } s_1 < s_2 \text{ and } g \in WG(s_1) \cap WG(s_2) $$

- Session-specific constraints such as the one which arose for session 34 in the 2024 edition can be written as follows:

$$ \bigwedge_{\substack{c \in C \\ l \in L}} \overline{x_{(34,c,l)}} \qquad (6) $$

## 4.2 Enhanced Model

In order to enhance our model, we first remark that Constraint (5) can be written differently as stated in the following proposition which can be easily proven by the distributive properties of logical conjunction and disjunction.

- **Proposition.** Constraint (5) is logically equivalent to the following constraint:

$$ (\bigwedge_{l \in L} \overline{x_{(s_1, c, l)}}) \lor (\bigwedge_{l \in L} \overline{x_{(s_2, c, l)}}) \lor y_{(s_1, s_2, c, g)} $$

$$ \forall (s_1, s_2, c, g) \in S^2 \times C \times G \text{ s.t } s_1 < s_2 \text{ and } g \in WG(s_1) \cap WG(s_2) $$
34:6 Minimizing Working-Group Conflicts in Conference Scheduling Through Max-SAT

As such, we can clearly observe that the information represented by the conjunctions in the clauses may occur redundantly in the constraint. Note that, for a given (session,slot) pair, these conjunctions represent the absence of a session from a given slot. Using these observations, we introduce new variables to our model as follows:

z(s,c) is set to true if session s ∈ S is not allocated to slot c ∈ C

To enforce the semantic meaning of these variables, we add the following constraint which can be easily rewritten in CNF form using the CNF rewriting of logical equivalence and the distributivity laws:

When a session is not allocated to a given slot, the corresponding z variable is set to true, otherwise to false:

$$z(s,c) \Leftrightarrow \bigwedge_{l \in L} \overline{x(s,c,l)} \quad \forall (s,c) \in S \times C \qquad (7)$$

Now, we can rewrite some of the previous constraints as shown below.

We can optimize the left-hand side of constraint (4) through the z variables as follows:

$$\sum_{s \in S} \overline{z(s,c)} \le n \quad \forall c \in C \qquad (4^*)$$

We can also simply remodel constraint (5) based on the rewriting established in the proposition above and by relying on the newly introduced z variables:

$$z(s_1,c) \lor z(s_2,c) \lor y(s_1,s_2,c,g) \quad \forall (s_1,s_2,c,g) \in S^2 \times C \times G, s_1 < s_2 \text{ and } g \in W(s_1) \cap W(s_2) \quad (5^*)$$

Finally, the z variables can be also used to effectively encode session-specific constraints as follows:

$$\bigwedge_{c \in C \setminus \{5,6,7\}} z(34,c) \qquad (6^*)$$

5 Experimental Evaluation

We have encoded our Max-SAT models<fnref n="5" /> using the PySAT<fnref n="6" /> library [17]. To compare our enhanced formulation to the basic model, we used the Sorting Network (SortN) encoding which is available for both PB and cardinality constraints in PySAT. Furthermore, to show that our enhanced model can be further improved, we also test a CardN+PBbest combination, with a cardinality encoding for cardinality constraints and the “best” option set for PB constraints in PySAT, which typically invokes the BDD encoding. Using data extracted from the last four years of ROADEF, we have generated a total of 72 instances, by choosing 7 varying values of n for each year. This enables us to not only minimize the number of working-group conflicts for a given n value but to also seek an optimal value for the maximum number of parallel sessions. The features of the generated instances in terms of number of variables and clauses are reported in Table 2. We have solved the generated instances using different state-of-the-art Max-SAT solvers including RC2 [18], OpenWBO (WBO) [26], MaxCDCL [23] and MaxHS [13]; all first-ranked solvers in previous Max-SAT evaluations.

<footnote n="5">⁵ Our code, data and benchmark are available in the following GitHub repository</footnote>

<footnote n="6">⁶ https://pysathq.github.io/</footnote>
<table><caption>Table 2 Summary of instance features and computed optimal values for the whole benchmark. # X denotes number of X. An interval is indicated when there are several values possible. For the sake of comparison, we report the values obtained through the handmade scheduling by the organizing committees between “()” in the last two rows.</caption><thead><tr><th rowspan="2">Year</th><th colspan="2">2024</th><th colspan="2">2023</th><th colspan="2">2022</th><th colspan="2">2021</th></tr><tr><th>SortN</th><th>CardN+PBbest</th><th>SortN</th><th>CardN+PBbest</th><th>SortN</th><th>CardN+PBbest</th><th>SortN</th><th>CardN+PBbest</th></tr></thead><tbody><tr><td><strong>Encoding</strong></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td><strong># Var</strong></td><td>45112</td><td>11007</td><td>49917</td><td>[12309-15235]</td><td>44212</td><td>[15810-12466]</td><td>44612</td><td>[9337-10173]</td></tr><tr><td><strong># Hard</strong></td><td>67754</td><td>20208</td><td>74926</td><td>[22640-27029]</td><td>65950</td><td>[26122-21106]</td><td>66807</td><td>[16209-17463]</td></tr><tr><td><strong># Soft</strong></td><td></td><td>308</td><td></td><td>518</td><td></td><td>880</td><td></td><td>264</td></tr><tr><td><strong># Conflicts</strong></td><td></td><td>4 (6)</td><td></td><td>9 (35)</td><td></td><td>29 (38)</td><td></td><td>0 (3)</td></tr><tr><td><strong>Optimum n</strong></td><td></td><td>10 (11)</td><td></td><td>13 (14)</td><td></td><td>11 (11)</td><td></td><td>5 (5)</td></tr></tbody></table>

For the sake of comparison, we have also implemented our models using OR-Tools to perform tests with the constraint programming solver CP-SAT [28]. The tests were performed on a machine equipped with an Intel Core i7 processor clocked at 3.80GHz, under Ubuntu 22.04. A timeout of 3600s was set for each instance. The results in terms of solving time are described in Table 3.

First, it is crucial to highlight the substantial enhancements our solutions have achieved over the manually crafted schedules by the organizing committees in recent years. More specifically, our models have remarkably enabled to improve both the number of conflicts and the management of parallel sessions. Indeed, for the years 2024 to 2021, our automated solutions reduced the number of working-group conflicts respectively by 2, 26, 9, and 3. This reduction emphasizes the relevance of our computational approach over traditional manual methods. Furthermore, our formulation has successfully decreased the maximum number of parallel sessions required in the 2024 and 2023 schedules, by reducing it from 11 to 10 in 2024 and from 14 to 13 in 2023. These results enable to significantly lessen the operational complexity and the resources required for organizing the conference and to ensure a smoother and more productive experience for attendees and organizers alike.

Next, we compare our enhanced formulation to the basic one. As showcased in Table 3, the comparison between the two models with Max-SAT solvers for a similar encoding (SortN) clearly supports the relevance of introducing *z* variables into the model. Across all years, the enhanced model consistently outperforms the basic one in terms of solving times. Notably, in terms of total solving time across all MaxSAT solvers, it achieves a gain of 62.9%, 67.2% and 44.7% respectively for years 2024, 2023 and 2021, with a total gain of 66.3% over the three years. In particular, the solving times were significantly improved for specific solvers as, for instance, more than 93% gain in solving time is achieved for the solver RC2 in 2023 with our enhanced formulation. Furthermore, the enhanced model's ability to produce better feasible solutions is particularly pronounced. Indeed, for the instances of 2023, the model not only enables the MaxCDCL solver to solve some instances within the timeout but also to achieve a feasible solution (which is optimal) for the remaining ones, unlike the basic model where it fails on all the instances. For the instances of 2022, although the optimal solutions are not found within the timeout<fnref n="7" />, it is crucial to emphasize that the enhanced model consistently improves the best feasible solutions compared to the basic model. In fact, the optimal values for the number of conflicts is in [27,29] with *n* = 11 showing that the enhanced model is able to achieve a tight optimal solution interval for 2022, with a feasible solution of 29 achieved by

<footnote n="7">⁷ Note that we did not change the internal behavior of the solvers and, in particular, MaxHS which may stop and return the best feasible solution before the timeout if it finds the problem hard to solve and does not manage to achieve optimality</footnote>
<figure><img src="image_14.png" /><figcaption>**Table 3** Solving times in seconds for the Basic Model with SortN and the Enhanced Model with SortN and CardN+PBbest. For each one, the best solving time for each instance is highlighted in bold. The best overall results for each instance are also underlined. T denotes the occurrence of a timeout. If the solver is not able to compute the optimal solution, the best obtained feasible solution is reported between “()” and, if a lower bound is provided, it is indicated between “[]”.</figcaption></figure>

<table><thead><tr><th rowspan="2">Year</th><th rowspan="2">n</th><th colspan="4">Basic Model</th><th rowspan="2">CP-SAT</th><th colspan="4">Enhanced Model</th><th colspan="4">Enhanced Model with CardN+PBbest</th></tr><tr><th>RC2</th><th>WBO</th><th>MaxCDCL</th><th>MaxHS</th><th>RC2</th><th>WBO</th><th>MaxCDCL</th><th>MaxHS</th><th>CP-SAT</th><th>RC2</th><th>WBO</th><th>MaxCDCL</th><th>MaxHS</th></tr></thead><tbody><tr><td rowspan="4">2024</td><td>15</td><td>3.428</td><td>7.811</td><td>5.358</td><td>16.086</td><td>26.800</td><td>1.259</td><td>1.180</td><td><strong>0.989</strong></td><td>17.933</td><td>7.683</td><td>0.767</td><td><strong>0.300</strong></td><td>0.467</td><td>9.925</td></tr><tr><td>14</td><td>3.054</td><td>12.095</td><td>5.716</td><td>46.308</td><td>26.291</td><td>1.300</td><td>1.130</td><td><strong>0.818</strong></td><td>14.633</td><td>6.677</td><td>0.716</td><td>0.301</td><td><strong>0.290</strong></td><td>11.236</td></tr><tr><td>13</td><td>3.288</td><td>6.989</td><td>5.591</td><td>46.206</td><td>20.622</td><td>1.199</td><td>1.404</td><td><strong>0.992</strong></td><td>18.585</td><td>7.713</td><td>0.770</td><td><strong>0.279</strong></td><td>0.353</td><td>12.476</td></tr><tr><td>12</td><td>3.540</td><td>6.036</td><td>5.147</td><td>95.241</td><td>22.691</td><td>1.315</td><td>1.742</td><td><strong>0.805</strong></td><td>20.607</td><td>10.056</td><td>0.718</td><td><strong>0.309</strong></td><td>0.313</td><td>5.972</td></tr><tr><td rowspan="4">2023</td><td>11</td><td>3.652</td><td>12.384</td><td>8.746</td><td>153.335</td><td>22.594</td><td>1.287</td><td>2.472</td><td><strong>1.100</strong></td><td>71.655</td><td>10.390</td><td>0.707</td><td>0.392</td><td>0.395</td><td>26.609</td></tr><tr><td>10</td><td><strong>9.902</strong></td><td>1398.111</td><td>511.043</td><td>869.119</td><td>88.831</td><td><strong>9.707</strong></td><td>341.225</td><td>150.416</td><td>271.440</td><td>35.460</td><td><strong>1.544</strong></td><td>411.766</td><td>213.257</td><td>500.964</td></tr><tr><td>17</td><td>197.515</td><td><strong>119.674</strong></td><td>T (-)</td><td>1187.325</td><td>T (-)</td><td><strong>9.687</strong></td><td>17.769</td><td>T (9)</td><td>357.906</td><td>T (9)</td><td>10.370</td><td><strong>6.136</strong></td><td>3371.304</td><td>353.515</td></tr><tr><td>16</td><td>355.627</td><td><strong>71.472</strong></td><td>T (-)</td><td>755.975</td><td>T (9)</td><td><strong>12.602</strong></td><td>20.701</td><td>3058.418</td><td>395.716</td><td>T (9)</td><td>12.145</td><td><strong>4.792</strong></td><td>2866.853</td><td>426.965</td></tr><tr><td rowspan="4">2022</td><td>15</td><td>139.625</td><td><strong>99.332</strong></td><td>T (-)</td><td>1106.281</td><td>T (9)</td><td><strong>23.467</strong></td><td>41.042</td><td>T (9)</td><td>408.854</td><td>T (9)</td><td>15.247</td><td><strong>6.696</strong></td><td>2686.484</td><td>405.923</td></tr><tr><td>14</td><td>107.202</td><td><strong>102.947</strong></td><td>T (-)</td><td>1036.948</td><td>T (9)</td><td><strong>14.011</strong></td><td>22.683</td><td>T (9)</td><td>413.160</td><td>T (9)</td><td>19.751</td><td><strong>6.706</strong></td><td>T (9)</td><td>417.693</td></tr><tr><td>13</td><td>250.308</td><td><strong>199.549</strong></td><td>T (-)</td><td>853.876</td><td>T (9)</td><td><strong>8.006</strong></td><td>14.962</td><td>3136.008</td><td>439.812</td><td>T (9)</td><td>8.733</td><td><strong>4.162</strong></td><td>T (9)</td><td>438.877</td></tr><tr><td>12</td><td>T (10)</td><td>T (-)</td><td>T (-)</td><td>T (28)[8]</td><td>T (-)</td><td>T (-)[10]</td><td>T (-)</td><td>T (-)</td><td>T (23)[8]</td><td>T (10)</td><td>T (10)</td><td>T (-)</td><td>T (-)</td><td>T (30)[9]</td></tr><tr><td rowspan="4">2021</td><td>16</td><td>T (-)[24]</td><td>T (127)</td><td><strong>T (29)</strong></td><td>385.625 (46)[18]</td><td><strong>T (29)</strong></td><td>T (-)[25]</td><td>T (146)</td><td><strong>T (29)</strong></td><td>496.061 (42)[22]</td><td><strong>T (29)</strong></td><td>T (-)[22]</td><td>T (83)</td><td><strong>T (29)</strong></td><td>1024.785 (40)[25]</td></tr><tr><td>15</td><td>T (-)[24]</td><td>T (161)</td><td><strong>T (29)</strong></td><td>380.048 (37)[26]</td><td><strong>T (29)</strong></td><td>T (-)[24]</td><td>T (134)</td><td><strong>T (29)</strong></td><td>322.627 (51)[18]</td><td><strong>T (29)</strong></td><td>T (-)[24]</td><td>T (58)</td><td><strong>T (29)</strong></td><td>1059.200 (33)[25]</td></tr><tr><td>14</td><td>T (-)[25]</td><td>T (196)</td><td><strong>T (29)</strong></td><td>T (37)[26]</td><td><strong>T (29)</strong></td><td>T (-)[27]</td><td>T (132)</td><td><strong>T (29)</strong></td><td>473.504 (38)[23]</td><td><strong>T (29)</strong></td><td>T (-)[24]</td><td>T (47)</td><td><strong>T (29)</strong></td><td><strong>448.613 (29)[23]</strong></td></tr><tr><td>13</td><td>T (-)[24]</td><td>T (222)</td><td><strong>T (29)</strong></td><td>392.299 (53)[18]</td><td><strong>T (29)</strong></td><td>T (-)[27]</td><td>T (146)</td><td><strong>T (29)</strong></td><td>348.256 (56)[17]</td><td><strong>T (29)</strong></td><td>T (-)[25]</td><td>T (50)</td><td><strong>T (29)</strong></td><td>330.284 (59)[18]</td></tr><tr><td rowspan="4">2021</td><td>12</td><td>T (-)[24]</td><td>T (324)</td><td><strong>T (29)</strong></td><td>856.923 (50)[24]</td><td><strong>T (29)</strong></td><td>T (-)[26]</td><td>T (135)</td><td><strong>T (29)</strong></td><td>980.692 (30)[25]</td><td><strong>T (29)</strong></td><td>T (-)[24]</td><td>T (71)</td><td><strong>T (29)</strong></td><td>328.658 (59)[18]</td></tr><tr><td>11</td><td>T (-)[25]</td><td>T (543)</td><td><strong>T (29)</strong></td><td>T (40)[27]</td><td><strong>T (29)</strong></td><td>T (-)[27]</td><td>T (436)</td><td><strong>T (29)</strong></td><td>713.466 (56)[18]</td><td><strong>T (29)</strong></td><td>T (-)[24]</td><td>T (287)</td><td><strong>T (29)</strong></td><td>650.517 (48)[18]</td></tr><tr><td>10</td><td>0.670</td><td>1.397</td><td><strong>0.503</strong></td><td>0.653</td><td>1.356</td><td>0.656</td><td>0.748</td><td>0.179</td><td><strong>0.132</strong></td><td>1.307</td><td>0.178</td><td>0.139</td><td>0.050</td><td><strong>0.027</strong></td></tr><tr><td>9</td><td>1.210</td><td>1.380</td><td><strong>0.276</strong></td><td>0.685</td><td>1.324</td><td>0.309</td><td>0.812</td><td>0.170</td><td><strong>0.155</strong></td><td>1.316</td><td>0.133</td><td>0.136</td><td>0.038</td><td><strong>0.026</strong></td></tr><tr><td>8</td><td>1.232</td><td>1.352</td><td><strong>0.437</strong></td><td>0.682</td><td>1.327</td><td>0.654</td><td>0.775</td><td><strong>0.278</strong></td><td>0.454</td><td>1.272</td><td>0.132</td><td>0.148</td><td>0.039</td><td><strong>0.030</strong></td></tr><tr><td>7</td><td>1.189</td><td>1.364</td><td><strong>0.262</strong></td><td>0.619</td><td>1.333</td><td>0.649</td><td>0.791</td><td><strong>0.256</strong></td><td>0.448</td><td>1.276</td><td>0.126</td><td>0.132</td><td>0.035</td><td><strong>0.030</strong></td></tr><tr><td>6</td><td>0.646</td><td>1.384</td><td><strong>0.414</strong></td><td>0.695</td><td>1.307</td><td>0.350</td><td>0.776</td><td><strong>0.281</strong></td><td>0.470</td><td>1.274</td><td>0.135</td><td>0.146</td><td>0.035</td><td><strong>0.031</strong></td></tr><tr><td>5</td><td>1.142</td><td>1.724</td><td><strong>0.425</strong></td><td>0.696</td><td>1.347</td><td>0.661</td><td>0.885</td><td><strong>0.279</strong></td><td>0.459</td><td>1.280</td><td>0.142</td><td>0.200</td><td>0.035</td><td><strong>0.027</strong></td></tr></tbody></table>
MaxCDCL. Overall, the results provide strong empirical evidence supporting the importance of introducing *z* variables in the scheduling model. This observation remains true for the CP-SAT solver which also shows superior performance with the enhanced formulation.

Note how CP-SAT achieves a timeout on all the instances of 2022 and 2023 both with the basic and enhanced models and does not manage to outperform the best MaxSAT solver in 2021 and 2024 for all the instances, which highlights the relevance of our MaxSAT approach in managing large-scale scheduling tasks. In addition, for the sake of enhancing MaxSAT solver performance, we have tested the CardN+PBbest combination with the enhanced model and we have obtained promising outcomes. Specifically, this combination demonstrates notable improvements in the best solving times compared to SortN, with a gain of 67.5%, 59.9% and 88.2% respectively for 2024, 2023 and 2021, thus averaging to more than 70% gain over the three years. Finally, note how the instances become particularly difficult for the smallest *n* within each year. In fact, the choices of the *n* values were not arbitrary as a formal lower bound can be established by calculating an upper bound of the number of papers for a given *n* as follows: $UBP_n = \sum_{c \in C} n * npMax(c)$. For instance, in 2024, we have $UBP_9 = 288 < \sum_{s \in S} np(s) = 307$ and, therefore, the set of hard constraints becomes unsatisfiable for *n* = 9 as it is impossible to schedule all the sessions so as to achieve the total amount of papers. In fact, we have also generated the instances for *n* = 9 in 2024, *n* = 11 in 2023, *n* = 10 in 2022 and *n* = 4 in 2021 totaling to 12 unsatisfiable instances. Unsurprisingly, while CP-SAT is able to prove the infeasibility of these instances, all the MaxSAT solvers failed within the timeout as these solvers are scarcely confronted to instances where the set of hard clauses is unsatisfiable [5]. This underscores the importance of enlarging the benchmarks in Max-SAT evaluations with such instances and, specifically, ones extracted from real-life scenarios such as ours to keep up the driving force in improving modern solvers.

# 6 Conclusion

In this paper, we addressed an optimization problem in conference session scheduling. More specifically, we presented a Max-SAT formulation for the minimization of working-group conflicts in the ROADEF conference, which we then enhanced by introducing new variables. Our results indicate that the number of conflicts and the maximum number of parallel sessions could be reduced and a scheduling could be computed in an effective time frame. Our work thus holds great promise in simplifying the scheduling task, streamlining logistics and optimizing resources in subsequent editions of the conference. As future work, we plan to expand our research by conducting experiments on additional datasets, both within and beyond the scope of ROADEF. Additionally, we aim to enhance our scheduling approach by incorporating considerations for author conflicts so as to develop a more comprehensive optimization framework that accounts for the intricate relationships among participants.

## 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, *14th International Conference on Theory and Applications of Satisfiability Testing - SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings*, volume 6695 of *Lecture Notes in Computer Science*, pages 61–75. Springer, 2011. doi:10.1007/978-3-642-21581-0_7.

2. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. *Artif. Intell.*, 196:77–105, 2013. doi:10.1016/J.ARTINT.2013.01.002.

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. doi:10.1007/978-3-642-02777-2_18.
34:10 Minimizing Working-Group Conflicts in Conference Scheduling Through Max-SAT

4 Roberto Javier Asín Achá and Robert Nieuwenhuis. Curriculum-based course timetabling with SAT and MaxSAT. *Ann. Oper. Res.*, 218(1):71–91, 2014. doi:10.1007/S10479-012-1081-X.

5 Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. MaxSAT Evaluation 2018: New Developments and Detailed Results. *J. Satisf. Boolean Model. Comput.*, 11(1):99–131, 2019. doi:10.3233/SAT190119.

6 Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiability. 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 929–991. IOS Press, 2021. doi:10.3233/FAIA201008.

7 Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified Core-Guided MaxSAT Solving. In Brigitte Pientka and Cesare Tinelli, editors, *Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings*, volume 14132 of *Lecture Notes in Computer Science*, pages 1–22. Springer, 2023. doi:10.1007/978-3-031-38499-8_1.

8 Jeremias Berg, Antti Hyttinen, and Matti Järvisalo. Applications of MaxSAT in Data Analysis. In Daniel Le Berre and Matti Järvisalo, editors, *Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018*, volume 59 of *EPiC Series in Computing*, pages 50–64. EasyChair, 2018. doi:10.29007/3QKH.

9 A. Biere, M. Heule, and H. van Maaren. *Handbook of Satisfiability: Second Edition*. Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://books.google.fr/books?id=dUAvEAAAQBAJ.

10 Miquel Bofill, Marc Garcia, Josep Suy, and Mateu Villaret. MaxSAT-Based Scheduling of B2B Meetings. In Laurent Michel, editor, *Integration of AI and OR Techniques in Constraint Programming - 12th International Conference, CPAIOR 2015, Barcelona, Spain, May 18-22, 2015, Proceedings*, volume 9075 of *Lecture Notes in Computer Science*, pages 65–73. Springer, 2015. doi:10.1007/978-3-319-18008-3_5.

11 Mohamed Sami Cherif, Djamal Habet, and André Abramé. Understanding the power of max-sat resolution through up-resilience. *Artif. Intell.*, 289:103397, 2020. doi:10.1016/J.ARTINT.2020.103397.

12 Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville. *ROADEF SCHEDULING*. Software, swhId: swh:1:dir:7083377094f69163d37d30b77d740c72c562139d (visited on 2024-08-16). URL: https://github.com/satoutahhaithem/ROADEF_SCHEDULING.

13 Jessica Davies and Fahiem Bacchus. Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. In Jimmy Ho-Man Lee, editor, *Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings*, volume 6876 of *Lecture Notes in Computer Science*, pages 225–239. Springer, 2011. doi:10.1007/978-3-642-23786-7_19.

14 Emir Demirovic and Nysret Musliu. MaxSAT-based large neighborhood search for high school timetabling. *Comput. Oper. Res.*, 78:172–180, 2017. doi:10.1016/J COR.2016.08.004.

15 Emir Demirovic, Nysret Musliu, and Felix Winter. Modeling and solving staff scheduling with partial weighted maxSAT. *Ann. Oper. Res.*, 275(1):79–99, 2019. doi:10.1007/S10479-017-2693-Y.

16 Niklas Eén and Niklas Sörensson. Translating Pseudo-Boolean Constraints into SAT. *J. Satisf. Boolean Model. Comput.*, 2(1-4):1–26, 2006. doi:10.3233/SAT190014.

17 Alexey Ignatiev, António Morgado, and João Marques-Silva. PySAT: A Python Toolkit for Prototyping with SAT Oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, *Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, 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 428–437. Springer, 2018. doi:10.1007/978-3-319-94144-8_26.
18 Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an Efficient MaxSAT Solver. *J. Satisf. Boolean Model. Comput.*, 11(1):53–64, 2019. doi:10.3233/SAT190116.

19 Gerold Jäger, Sharlee Climer, and Weixiong Zhang. The complete parsimony haplotype inference problem and algorithms based on integer programming, branch-and-bound and Boolean satisfiability. *J. Discrete Algorithms*, 37:68–83, 2016. doi:10.1016/J.JDA.2016.06.001.

20 Alexandre Lemos, Filipe Gouveia, Pedro T. Monteiro, and Inês Lynce. Iterative Train Scheduling under Disruption with Maximum Satisfiability. *J. Artif. Intell. Res.*, 79:1047–1090, 2024. doi:10.1613/JAIR.1.14924.

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. doi:10.3233/FAIA201007.

22 Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining clause learning and branch and bound for maxsat. In Laurent D. Michel, editor, *27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021*, volume 210 of LIPIcs, pages 38:1–38:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CP.2021.38.

23 Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Boosting branch-and-bound MaxSAT solvers with clause learning. *AI Commun.*, 35(2):131–151, 2022. doi:10.3233/AIC-210178.

24 Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, and Wenxin Yu. Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems. In Abhaya C. Nayak and Alok Sharma, editors, *PRICAI 2019: Trends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Cuvu, Yanuca Island, Fiji, August 26-30, 2019, Proceedings, Part I*, volume 11670 of Lecture Notes in Computer Science, pages 618–631. Springer, 2019. doi:10.1007/978-3-030-29908-8_49.

25 Hratch Mangassarian, Andreas G. Veneris, and Farid N. Najm. Maximum circuit activity estimation using pseudo-boolean satisfiability. *IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.*, 31(2):271–284, 2012. doi:10.1109/TCAD.2011.2169259.

26 Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A Modular MaxSAT Solver. In Carsten Sinz and Uwe Egly, editors, *Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings*, volume 8561 of Lecture Notes in Computer Science, pages 438–445. Springer, 2014. doi:10.1007/978-3-319-09284-3_33.

27 António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. *Constraints An Int. J.*, 18(4):478–534, 2013. doi:10.1007/S10601-013-9146-2.

28 Laurent Perron and Frédéric Didier. Cp-sat. URL: https://developers.google.com/optimization/cp/cp_solver/.

29 Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Proofs and Certificates for Max-SAT. *J. Artif. Intell. Res.*, 75:1373–1400, 2022. doi:10.1613/JAIR.1.13811.

30 Olivier Roussel and Vasco M. 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. doi:10.3233/FAIA201012.

31 Ahmad Shabani and Bijan Alizadeh. PMTP: A MAX-SAT-Based Approach to Detect Hardware Trojan Using Propagation of Maximum Transition Probability. *IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.*, 39(1):25–33, 2020. doi:10.1109/TCAD.2018.2889663.