Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR23-129 | 21st August 2023 15:49

Understanding Nullstellensatz for QBFs


Authors: Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla
Publication: 5th September 2023 12:29
Downloads: 149


QBF proof systems are routinely adapted from propositional logic along with adjustments for the new quantifications. Existing are two main successful frameworks, the reduction and expansion frameworks, inspired by QCDCL [Zhang et al. ICCAD.'2002] and CEGAR solving [Janota et al. Artif. Intell.'2016] respectively. However, the reduction framework, while immensely useful in line-based proof systems, is not refutationally complete for static proof systems.

Nullstellensatz (NS, [Beame et al. FOCS.'1994]) is a well known static propositional proof system, inspired by Hilbert's theorem [Hilbert Math. Ann.'1893] of the same name. It falls into the category of algebraic proof systems such as the Polynomial Calculus [Book, Krají?ek Cam. Uni.'2019, p.162] or the Ideal Proof System (IPS,[Grochow et al. J. ACM.'2018]). In this paper, we initiate the study of the NS proof system for QBFs using the existing expansion ($\forall$Exp) framework and a new "$\forall$Strat" framework. We introduce four new static QBF refutation systems: $\forall$Exp+NS, $\forall$Exp+NS', $\forall$Strat+NS and $\forall$Strat+NS', which use NS and a more powerful version of NS (NS') with twin variable encoding that allows it to simulate tree-like resolution without an exponential blowup.

We explore relationships among the proposed systems and analyse their proof sizes for a few well-known hard QBF-families. We find that $\forall$Exp+NS' and $\forall$Strat+NS' are incomparable. This result is in line with the incomparability result between ?Exp+Res and Q-Res [Beyersdorff et al. STACS.'2015].

ISSN 1433-8092 | Imprint