The satisfiability problem (or, more generally, the constraint satisfaction problem) and MaxSAT (or, more generally, the problem of constrained optimization) are two of the most relevant problems for computer science and artificial intelligence. Despite the tremendous advances of the last decades, there is a feeling among experts that radically new ideas may be necessary for further progress beyond the current barriers. In this grant, we propose to surpass the known intrinsic limitations of the Resolution proof system, the still dominant method in the area, by studying and implementing stronger proof systems for propositional logic.
One of the leading motivations for this grant is to contribute to the ongoing building of bridges between the theoretical and practical sides of the area. We plan to continue the theoretical study of algebraic and semi-algebraic proof systems such as Polynomial Calculus, Sherali- Adams, and Sums-of-Squares, as well as their more practical implementation aspects. This study could lead to a new generation of SAT and MaxSAT solvers beyond Resolution, and to new algorithmic methods for constraint satisfaction problems and their variants. While any proof of completeness of the proof systems implicitly carries with it an automating algorithm, further investigation is needed when it comes to bringing these algorithms to practice. For Sherali-Adams and Sums-of-Squares, the theoretical algorithms are based on linear
programming and semi-definite programming, respectively. For Polynomial Calculus, the algorithm is based on Groebner bases. Is the full strength of these general methods needed for automation of real instances? What types of constraints can be solved efficiently by these methods? Answering these types of questions is only possible through the collaboration of leading researchers in the theoretical and practical aspects of SAT, CSP, and optimization. We believe that this proposal can contribute to establishing the required synergy of methods.
The research team is composed of professors from four institutions: the University of Lleida (UdL), the Technical University of Catalonia (UPC), the Spanish Research Council (CSIC), and the University Pompeu Fabra (UPF). The project is structured into two subprojects, one focussed on the foundational aspects, and the other one focussed on the applied ones. The team is distributed across the subprojects according to expertise. We have identified six objectives, three of which are more applied, the rest more theoretical, and all of them appear to be interconnected. This is reflected in the composition of the working teams, but also in the past collaborations and joint publications.