Harnessing Maximum Satisfiability in Novel Approaches for
Solving Complex Facility Location Problems
PhD Project | UPJV | 2024
Harnessing Maximum Satisfiability in Novel Approaches for
Solving Complex Facility Location Problems
The propositional satisfiability (SAT) problem is at the heart of many sub-fields in
computer science including complexity theory and symbolic artificial intelligence [4]. It
consists in checking whether a given propositional formula in Conjunctive Normal Form
(CNF), i.e. in the form of a set of constraints called clauses, can be satisfied by an
assignment of the variables. SAT is the first problem that was proven NP-complete in
the literature [7]. It is also a fundamental formalism in constraint programming that
is used to model and solve a wide variety of academic and industrial problems. Conse-
quently, this problem, its variants and its extensions attract a large international research
community, with a dedicated conference1 and an annual prestigious competition2. The
Maximum Satisfiability (Max-SAT) problem is the natural optimization extension of
SAT [2, 19] where the goal shifts from determining the satisfiability of the given CNF
formula to computing the maximum number of clausal constraints that can be satisfied
by an assignment of the variables. Although Max-SAT is NP-hard, the last decade has
known major breakthroughs in Max-SAT theory and solving. Indeed, SAT-based algo-
rithms [1, 11, 15, 22] 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
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 foun-
dational learning process tailored to Max-SAT [17, 18]. These advancements were also
coupled with new insights and understanding of Max-SAT proof theory, paving the way
for efficient solver certification for Max-SAT [3, 24]. As such, algorithms dedicated to
Max-SAT are now able to solve large and complex instances within reasonable time,
making it a powerful formalism which can be used to model and solve many real-world
problems. The importance of this problem and the constant attention to inciting further
improvement in the empirical performance of its solvers is also attested by the annual
evaluations for Max-SAT3.
This PhD project is dedicated to studying classical location problems through the
lens of Maximum Satisfiability, namely the p-center problems and p-median problems.
The p-center problem (resp. p-median) is that of locating p facilities while minimizing
the maximal distance (resp. the total distance) to the demand points [5, 10]. Such
problems date back to the sixties [13] and have been extensively studied and solved
through different approaches which include, but are not limited to, linear programming
[6, 9, 12, 16], meta-heuristics [8, 20, 25], and genetic algorithms [14, 23]. Yet, to the
best of our knowledge, the only work which has studied these problems through the lens
of satisfiability is that of Liu and al. where an iterative approach through SAT and set
covering is used to solve the p-center problem [21]. Building upon this founding work, the
PhD candidate will explore novel methodologies to solve the studied problems through
Max-SAT. To this end, the candidate can take advantage of the expressiveness of Max-
SAT and particularly its known variants, such as partial Max-SAT which introduces a set
of ’hard’ clauses in the formula representing mandatory constraints that must be satisfied,
1International Conference on Theory and Applications of Satisfiability Testing (SAT)
2https://www.satcompetition.org/
3https://maxsat-evaluations.github.io/
1
or weighted Max-SAT which involves integer weights representing the penalty of falsifying
the clausal constraints. The candidate can therefore explore efficient direct encodings
of p-center and p-median problems to Max-SAT instances in order to solve them with
state-of-the-art solvers empowered with dedicated heursitics as well as hybrid approaches
combining Max-SAT-based methods with other optimization paradigms and/or machine-
learning techniques, opening up new avenues for addressing such problems. Preliminary
work showing the feasibility of the latter approach has been submitted to a national
conference.
The PhD will be partially funded by the ANR Massal’IA chair4. The significance of
this research is thus underscored by its potential impact on the strategic deployment of
infrastructure for electric vehicles, which is a key concern of Enedis, a major partner in the
chair. The introduced methods will be particularly applied and tested on data provided
by Enedis to connect charging points for electric vehicles at minimum cost so as to satisfy
the demand and to favor the use of clean energy. The methodologies developed in this
PhD project will therefore not only contribute to theoretical advancements in the field
of optimization but will also play a crucial role in supporting sustainable development
initiatives by tackling the complex logistic, infrastructural and environmental challenges
arising in the deployment of modern transportation infrastructure.
Localization: MIS laboratory (Modélisation, Information & Systèmes), University of
Picardie Jules Verne, 14 Quai de la Somme, Amiens.
Supervision: The PhD candidate will be integrated into the GOC (Graphs, Optimiza-
tion & Constraints) team of the MIS lab and will be co-supervised by Chu-Min Li and
Sami Cherif.
Duration: 3 years starting from October 2024 (Phd contract with salary in line with
public sector rates).
Prerequisites : Student with a Master’s degree in computer science (by the end of the
current academic year), good programming skills (Python, C/C++) and proficiency in
English. Prior knowledge in constraint programming would be highly appreciated.
Resources/Work environment: An office space, a computer and an access to com-
puting resources (MatricS UPJV platform) will be provided. Funding to attend summer
schools, conferences or workshops will be made available to the candidate. The candi-
date will also have opportunities for collaboration with other members of the MIS lab as
well as external researchers involved in the Massal’IA chair within the COALA team of
the LIS lab (Laboratoire Informatique & Systèmes UMR 7020, Aix-Marseille University).
Expected scientific outcomes: In terms of publications, the outcome of the project
is estimated up to 3 papers in good or top-tier AI conferences (IJCAI, ECAI, AAAI, CP,
SAT...) as well as a publication in a reputable AI journal (AIJ, JAIR, JSAT...).
Application : To apply, please send your resume and Master’s Degree transcripts to
<chu-min.li@u-picardie.fr> and <sami.cherif@u-picardie.fr>
4Propositional Reasoning for Large-Scale Optimization: Application to Clean Energy Mobility Issues
2
References
[1] C. Ansótegui, M. L. Bonet, and J. Levy. SAT-based MaxSAT algorithms. Artif.
Intell., 196:77–105, 2013.
[2] F. Bacchus, M. Järvisalo, and R. Martins. Maximum Satisfiabiliy. In A. Biere,
M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability - Second
Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages
929–991. IOS Press, 2021.
[3] J. Berg, B. Bogaerts, J. Nordström, A. Oertel, and D. Vandesande. Certified Core-
Guided MaxSAT Solving. In B. Pientka and C. 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.
[4] A. Biere, M. Heule, and H. van Maaren. Handbook of Satisfiability: Second Edition.
Frontiers in Artificial Intelligence and Applications. IOS Press, 2021.
[5] H. Calik, M. Labbé, and H. Yaman. p-Center Problems. Location science, pages
79–92, 2015.
[6] H. Calik and B. C. Tansel. Double bound method for solving the p-center location
problem. Computers & Operations Research, 40(12):2991–2999, Dec. 2013.
[7] S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the
Third Annual ACM Symposium on Theory of Computing, STOC ’71, page 151–158,
New York, NY, USA, 1971. Association for Computing Machinery.
[8] T. Cura. A parallel mayfly algorithm for the α-neighbor p-center problem. Appl.
Soft Comput., 144:110527, 2023.
[9] M. S. Daskin. Network and discrete location: models, algorithms, and applications.
Wiley-Interscience series in discrete mathematics and optimization. Wiley, New York
Chichester, 1995.
[10] M. S. Daskin and K. L. Maass. The p-Median Problem. In Location science, pages
21–45. Springer, 2015.
[11] J. Davies and F. Bacchus. Solving MAXSAT by Solving a Sequence of Simpler SAT
Instances. In J. H. 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.
[12] C. Duran-Mateluna, Z. Alès, S. Elloumi, and N. Jorquera-Bravo. Robust MILP
formulations for the two-stage weighted vertex p-center problem. Comput. Oper.
Res., 159:106334, 2023.
[13] S. L. Hakimi. Optimum locations of switching centers and the absolute centers and
medians of a graph. Operations research, 12(3):450–459, 1964.
[14] P. He, J. Hao, and Q. Wu. A hybrid genetic algorithm for the hamiltonian p-median
problem. Networks, 83(2):348–367, 2024.
3
[15] A. Ignatiev, A. Morgado, and J. Marques-Silva. RC2: an Efficient MaxSAT Solver.
J. Satisf. Boolean Model. Comput., 11(1):53–64, 2019.
[16] P. Ilhan. An efficient exact algorithm for the vertex p-center problem. Bilkent
University Technical Report, Sept. 2001.
[17] C. Li, Z. Xu, J. Coll, F. Manyà, D. Habet, and K. He. Combining clause learn-
ing and branch and bound for maxsat. In L. D. Michel, editor, 27th International
Conference on Principles and Practice of Constraint Programming, CP 2021, Mont-
pellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs,
pages 38:1–38:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
[18] C. Li, Z. Xu, J. Coll, F. Manyà, D. Habet, and K. He. Boosting branch-and-bound
MaxSAT solvers with clause learning. AI Commun., 35(2):131–151, 2022.
[19] C. M. Li and F. Manyà. MaxSAT, Hard and Soft Constraints. In A. Biere, M. Heule,
H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability - Second Edition,
volume 336 of Frontiers in Artificial Intelligence and Applications, pages 903–927.
IOS Press, 2021.
[20] W. Li, J. Gao, and Y. Mao. An α-risk appetite cost minimizing model for multi-
commodity capacitated p-hub median problem with time windows and uncertain
flows. Ann. Oper. Res., 333(1):79–121, 2024.
[21] X. Liu, Y. Fang, J. Chen, Z. Su, C. Li, and Z. Lü. Effective approaches to solve
p-center problem via set covering and SAT. IEEE Access, 8:161232–161244, 2020.
[22] A. Morgado, F. Heras, M. H. Liffiton, J. Planes, and J. Marques-Silva. Iterative
and core-guided MaxSAT solving: A survey and assessment. Constraints An Int.
J., 18(4):478–534, 2013.
[23] W. J. Pullan. A memetic genetic algorithm for the vertex p-center problem. Evol.
Comput., 16(3):417–436, 2008.
[24] M. Py, M. S. Cherif, and D. Habet. Proofs and Certificates for Max-SAT. J. Artif.
Intell. Res., 75:1373–1400, 2022.
[25] D. Ristic, N. Mladenovic, M. Ratli, R. Todosijevic, and D. Urosevic. Auxiliary data
structures and techniques to speed up solving of the p-next center problem: A VNS
heuristic. Appl. Soft Comput., 140:110276, 2023.
4
