Author name cluster

Luc Nicolas Spachmann

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

SAT Conference 2025 Conference Paper

Semi-Algebraic Proof Systems for QBF

Olaf Beyersdorff
Ilario Bonacina
Kaspar Kasche
Meena Mahajan
Luc Nicolas Spachmann

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.

Details

MFCS Conference 2024 Conference Paper

Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree

Olaf Beyersdorff
Tim Hoffmann
Kaspar Kasche
Luc Nicolas Spachmann

We initiate an in-depth proof-complexity analysis of polynomial calculus (𝒬-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of 𝒬-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for 𝒬-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999). We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in 𝒬-PC. This leads to incomparability results for 𝒬-PC systems over different fields.

Details

SAT Conference 2023 Conference Paper

Proof Complexity of Propositional Model Counting

Olaf Beyersdorff
Tim Hoffmann
Luc Nicolas Spachmann

Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT'22). As demonstrated by Fichte et al. , the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MICE' that is polynomially equivalent to MICE. Our main result establishes an exponential lower bound for the number of proof steps in MICE' (and hence also in MICE) for a specific family of CNFs.

Details