PROOFS BEYOND
PROOFS BEYOND

PROOFS BEYOND
PROOFS BEYOND
 : 
Satisfiability and Optimization with Certificate Proofs Beyond Resolution
Satisfiability and Optimization with Certificate Proofs Beyond Resolution

A Project coordinated by IIIA.

Web page:

Principal investigator: 

Collaborating organisations:

Universitat Politècnica de Catalunya (UPC), Universitat de Lleida (UdL) and (Universitat Pompeu Fabra (UPF)

Universitat Politècnica de Catalunya (UPC), Universitat de Lleida (UdL) and (Universitat Pompeu Fabra (UPF)

Funding entity:

Ministerio de Ciencia e Innovación
Ministerio de Ciencia e Innovación

Funding call:

PNGEC - Programa Nacional de Generación del Conocimiento
PNGEC - Programa Nacional de Generación del Conocimiento

Funding call URL:

Project #:

PID2022-138506NB-C21
PID2022-138506NB-C21

Total funding amount:

157.125,00€
157.125,00€

IIIA funding amount:

Duration:

01/Sep/2023
01/Sep/2023
31/Aug/2026
31/Aug/2026

Extension date:

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.

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.

2024
Ilario Bonacina,  Maria Luisa Bonet,  & Jordi Levy (2024). Weighted, Circular and Semi-Algebraic Proofs. J. Artif. Intell. Res., 79, 447--482. https://doi.org/10.1613/JAIR.1.15075. [BibTeX]  [PDF]
2023
Eduardo Calò,  & Jordi Levy (2023). General Boolean Formula Minimization with QBF Solvers. Ismael Sanz, Raquel Ros, & Jordi Nin (Eds.), Artificial Intelligence Research and Development - Proceedings of the 25th International Conference of the Catalan Association for Artificial Intelligence, CCIA 2023, Món Sant Benet, Spain, 25-27 October 2023 (pp. 347--358). {IOS}Press. https://doi.org/10.3233/FAIA230705. [BibTeX]  [PDF]
Eduardo Calò,  Jordi Levy,  Albert Gatt,  & Kees Deemter (2023). Is Shortest Always Best? The Role of Brevity in Logic-to-Text Generation. Alexis Palmer, & José Camacho-Collados (Eds.), Proceedings of the The 12th Joint Conference on Lexical and Computational Semantics, *SEM@ACL 2023, Toronto, Canada, July 13-14, 2023 (pp. 180--192). Association for Computational Linguistics. https://doi.org/10.18653/V1/2023.STARSEM-1.17. [BibTeX]  [PDF]
Carlos Ansótegui,  Maria Luisa Bonet,  & Jordi Levy (2023). On the Density of States of Boolean Formulas. Ismael Sanz, Raquel Ros, & Jordi Nin (Eds.), Artificial Intelligence Research and Development - Proceedings of the 25th International Conference of the Catalan Association for Artificial Intelligence, CCIA 2023, Món Sant Benet, Spain, 25-27 October 2023 (pp. 369--382). {IOS}Press. https://doi.org/10.3233/FAIA230707. [BibTeX]  [PDF]
Ilario Bonacina,  Maria Luisa Bonet,  & Jordi Levy (2023). Polynomial Calculus for MaxSAT. Meena Mahajan, & Friedrich Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy (pp. 5:1--5:17). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2023.5. [BibTeX]  [PDF]
Thomas Bläsius,  Tobias Friedrich,  Andreas Göbel,  Jordi Levy,  & Ralf Rothenberger (2023). The impact of heterogeneity and geometry on the proof complexity of random satisfiability. Random Struct. Algorithms, 63, 885--941. https://doi.org/10.1002/RSA.21168. [BibTeX]  [PDF]
Jordi Levy
Tenured Scientist
Phone Ext. 431860

Ion Mikel Liberal
PhD Student