Mots-Clés

Intelligence artificielle, Satisfiabilité Maximum, Maximum Colourful Subtree, mass spectrometry

Description

The Maximum Satisfiability (Max-SAT) problem is a natural optimization extension of the well-known Satisfiability (SAT) problem. SAT is a decision problem which simply 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 [2]. On the other hand, in Max-SAT, we are interested in computing the maximum number of clausal constraints that can be satisfied in the given CNF formula. Algorithms dedicated to Max-SAT are now able to solve large instances within reasonable time, making it a powerful formalism which can be used to model and solve many real-world and academic problems. Examples of industrial applications include planning and scheduling, explainable AI, verification and security, bio-informatics as well as hardware and software debugging among many others [1]. In this internship, we will be interested in solving the Maximum Colorful Subtree problem through maximum satisfiability. This problem consists in finding the induced colorful subtree of maximum weight, within a node-colored and edge-weighted directed acyclic graph (DAG). Finding this tree is an NP-hard problem [5]. This problem has been extensively studied in order to model the process of Collision-Induced Dissociation (CID) of small molecules in a mass spectrometer, and has been solved through different approaches, including Dynamic Programming, Integer Linear Programming, and heuristic algorithms [3, 4, 6]. Yet, to the best of our knowledge, this problem has not been studied through the lens of satisfiability. During the internship, the student is expected to perform a thorough literature review of the algorithms solving the Maximum Colorful Subtree problem for modeling molecular fragmentation trees. These problems will then be modeled into Max-SAT instances and solved through dedicated algorithms. Finally, a thorough experimental evaluation and comparison with other methods in the literature are also expected.