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