Propositional Reasoning for Large-Scale Optimization. Application to Clean Energy Mobility Issues – Massal'IA

The propositional satisfiability problem (SAT) is fundamental in many fields of Computer Science and particularly in Artificial Intelligence. Thanks to its high reasoning capabilities, SAT is a very competitive generic problem-solving approach that is often applied to solve decision problems in various areas such as hardware and software verification, bioinformatics, cryptography, planning, and even outperforms dedicated solvers for such problems. This solving ability is the result of the advanced solving techniques incorporated in the modern SAT solvers based on Conflict Driven Clause Learning (CDCL), which solve very efficiently industrial instances with millions of variables and several tens of millions of clauses. Meanwhile, machine learning techniques begins to be used in SAT solving, resulting in a powerful branching heuristic in SAT solvers.

Given the success of SAT on decision problems, the scientific community started to explore, about 20 years ago, the potential of Max-SAT formalisms to become a competitive approach to process optimization. The efforts devoted to Max-SAT have led to the development of a new generation of Max-SAT solvers, as well as their application in solving some practical optimization problems in areas such as design debugging of digital circuits and protein alignment.

There are two classes of Max-SAT solvers: branch-and-bound (BnB) solvers, which consider as lower bounds the number of detected disjoint inconsistent subsets, and are good on random and some crafted instances; and SAT-based solvers, which solve Max-SAT by solving a sequence of SAT instances with a CDCL SAT solver, and are specially good on industrial instances. Despite the spectacular progress made by such solvers, the two classes are developed separately, i.e. there is no SAT solver calling in BnB solvers and there is no BnB in SAT-based solvers. In summary, we are in a scenario where SAT-based problem solving is highly competitive on decision problems, and Max-SAT-based approaches have been proposed for optimization problems. Max-SAT is a consolidated research line, but the performance of the solvers needs to be improved for large scale real applications containing complex data.

The first objective of this project is to propose an approach, allowing to hybrid BnB Max-SAT solvers and SAT-based Max-SAT solvers. In such a solver, SAT solvers will be called iteratively to compute a lower bound after branching. Thus, the strengths of BnB and SAT-based approaches can be combined. The second objective is to use machine learning to design powerful branching heuristics in the hybrid Max-SAT solvers. The third objective is to apply the new solvers to a real industrial applications. For this purpose, we should use and develop AI tools (machine learning, Bayesian networks, etc.) to design a data model, from which we can derive Max-SAT instances encoding the industrial problem, so that the solution given by a Max-SAT solver is a good solution of the industrial problem.

A major partner, Enedis, will be involved in this ambitious perspective. Their goal is to help develop electric mobility in Aix-Marseille Provence Metropolis (AMPM) firstly, in the Provence-Alpes-Côte d’Azur Region of France secondly and in France thirdly. This is a very complex issue, because it concerns transport (public transport networks, individual mobility) and environment (pollution, production and exploitation of clean energy), leading to the production and manipulation of complex information, sometimes with uncertainty, and that evolve over time, with large amounts of data that are often difficult to exploit. In addition, there are hard combinatorial optimization problems to solve. The scientific issue we will address in this context is central in AI: proposing new models for representing this complex information and designing new reasoning methods for solving and optimizing under the Max-SAT formalization of these models.