All reports by Author Luc Nicolas Spachmann:

__
TR24-038
| 27th February 2024
__

Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann#### Polynomial Calculus for Quantified Boolean Logic: Lower Bounds through Circuits and Degree

__
TR24-030
| 22nd February 2024
__

Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann#### Proof Complexity of Propositional Model Counting

Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann

We initiate an in-depth proof-complexity analysis of polynomial calculus (Q-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of Q-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for Q-PC, similar in ... more >>>

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 ...
more >>>