Semi-Algebraic Proof Systems for QBF

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Beyersdorff, Olaf, Bonacina, Ilario, Kasche, Kaspar, Mahajan, Meena, Spachmann, Luc Nicolas
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914150724141056
author Beyersdorff, Olaf
Bonacina, Ilario
Kasche, Kaspar
Mahajan, Meena
Spachmann, Luc Nicolas
author_facet Beyersdorff, Olaf
Bonacina, Ilario
Kasche, Kaspar
Mahajan, Meena
Spachmann, Luc Nicolas
contents We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF literature (strategy extraction) and from propositional proof complexity (size-degree relations and pseudo-expectation). We obtain a number of strong QBF lower bounds and separations between these systems, even when disregarding propositional hardness.
format Preprint
id arxiv_https___arxiv_org_abs_2511_08050
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Semi-Algebraic Proof Systems for QBF
Beyersdorff, Olaf
Bonacina, Ilario
Kasche, Kaspar
Mahajan, Meena
Spachmann, Luc Nicolas
Logic in Computer Science
Computational Complexity
Logic
03F20, 03D15
We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF literature (strategy extraction) and from propositional proof complexity (size-degree relations and pseudo-expectation). We obtain a number of strong QBF lower bounds and separations between these systems, even when disregarding propositional hardness.
title Semi-Algebraic Proof Systems for QBF
topic Logic in Computer Science
Computational Complexity
Logic
03F20, 03D15
url https://arxiv.org/abs/2511.08050