Combinatorial problems that arise naturally in many domains (scheduling and planning, software and hardware verification, knowledge compilation, probabilistic modeling, bioinformatics, energy systems, smart cities, social networks, computational sustainability, etc) can be encoded as a satisfiability problem (SAT) or one of its variants (CSP, MaxSAT,...). This large family of computational problems has been intensively studied, both from a practical and theoretical perspective.

Regarding practice, in the last decade, there has been a tremendous success in solving industrial combinatorial problems through Constraint Programming techniques, such as Satisfiability (SAT) solvers. Proof systems lie at the heart of state-of-the-art SAT/CSP/MaxSAT solving. In particular, CDCL SAT solvers contain, implicitly, a resolution engine that, once a conflict is found, learns anew clause that represents the reason of the conflict. From a practical perspective, the main goal of this proposal is to build new SAT solvers based on proof systems that are more powerful than resolution. We hope that this can have a great impact in practice since, in turn, it could boost MaxSAT solvers and other successful approaches using SAT technology such as Satisfiability Modulo Theories. However, to make this step it is necessary to automatize a better understanding and exploitation of the structure of Real-World problems maybe through the application of Machine Learning (ML) techniques, which is another of the main themes of our work. In particular, we will study how to combine Deep learning and Reinforcement learning ML techniques, complex networks analysis and more powerful proof systems, creating a yet unexplored synergy between Machine Learning and proof systems for Constraint Programming.

From a theoretical perspective, proof systems also play a major role. Indeed, several very powerful and general algorithmic principles based on solving (linear of semidefinite) relaxations of SAT (and more generally CSP instances), such as Lovasz-Schrijver, Sherali-Adams and the Lasserre hierarchies are naturally associated to proof systems. In several particular domains, it is not possible to go beyond these proof systems and, indeed, it is quite conceivable that many of the problems that are still resisting classification could be solved by some of them. However, the reach of these approaches is still not fully understood. Improving our understanding is the main theoretical goal of the proposal. On one hand, we plan to extend the study of current proof systems to new CSPs, such as the family of Promise CSPs, recently introduced. Promise CSPs have received a lot of attention and constitute one of the most natural steps (after non-uniform CSPs were completely classified in 2017) to push further the so-called algebraic approach in the study of computational problems. Secondly, we plan to investigate new variants of existing proof systems towards the ultimate goal of expanding our toolkit of algorithmic approaches to be able to tackle many of the solvable CSPs of interest that still resist attack.