--- title: "Weighted, Circular and Semi-Algebraic Proofs (Abstract Reprint)" authors: - "Ilario Bonacina" - "Maria Luisa Bonet" - "Jordi Levy" doi: "10.24963/ijcai.2024/947" url: "https://ijcai.org/proceedings/2024/947" pdf: "https://ijcai.org/proceedings/2024/0947.pdf" venue: "Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence" year: 2024 pages: "8475-8475" track: "Journal Track" keywords: - "Journal Track: Journal Track" --- # Weighted, Circular and Semi-Algebraic Proofs (Abstract Reprint) Ilario Bonacina, Maria Luisa Bonet, Jordi Levy *Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence*, pages 8475-8475. DOI: [10.24963/ijcai.2024/947](https://doi.org/10.24963/ijcai.2024/947) ## Abstract In recent years there has been an increasing interest in studying proof systems stronger than Resolution, with the aim of building more efficient SAT solvers based on them. In defining these proof systems, we try to find a balance between the power of the proof system (the size of the proofs required to refute a formula) and the difficulty of finding the proofs. In this paper we consider the proof systems circular Resolution, Sherali-Adams, Nullstellensatz and Weighted Resolution and we study their relative power from a theoretical perspective. We prove that circular Resolution, Sherali-Adams and Weighted Resolution are polynomially equivalent proof systems. We also prove that Nullstellensatz is polynomially equivalent to a restricted version of Weighted Resolution. The equivalences carry on also for versions of the systems where the coefficients/weights are expressed in unary. The practical interest in these systems comes from the fact that they admit efficient algorithms to find proofs in case these have small width/degree. ## Full text ## Weighted, Circular and Semi-Algebraic Proofs (Abstract Reprint) Ilario Bonacina1 , Maria Luisa Bonet1 and Jordi Levy2 1 UPC Universitat Politecnica de Catalunya 2 Artificial Intelligence Research Institute (IIIA) bonacina@cs.upc.edu, bonet@cs.upc.edu, levy@iiia.csic.es Abstract Reprint. This is an abstract reprint of a journal by [Bonacina et al., 2024]. ## Abstract In recent years there has been an increasing interest in studying proof systems stronger than Resolution, with the aim of building more efficient SAT solvers based on them. In defining these proof systems, we try to find a balance between the power of the proof system (the size of the proofs required to refute a formula) and the difficulty of finding the proofs. In this paper we consider the proof systems circular Resolution, Sherali-Adams, Nullstellensatz and Weighted Resolution and we study their relative power from a theoretical perspective. We prove that circular Resolution, Sherali-Adams and Weighted Resolution are polynomially equivalent proof systems. We also prove that Nullstellensatz is polynomially equivalent to a restricted version of Weighted Resolution. The equivalences carry on also for versions of the systems where the coefficients/weights are expressed in unary. The practical interest in these systems comes from the fact that they admit efficient algorithms to find proofs in case these have small width/degree. ## References 1. [Bonacina et al., 2024] Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Weighted, circular and semi-algebraic proofs. J. Artif. Intell. Res., 79:447-482, 2024.