Author name cluster

Tim Hoffmann

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.

6 papers

2 author rows

AAAI Conference 2026 Conference Paper

Proof Systems for Tensor-based Model Counting

Olaf Beyersdorff
Joachim Giesen
Andreas Goral
Tim Hoffmann
Kaspar Kasche
Christoph Staudt

Solving the model counting problem #SAT, asking for the number of satisfying assignments of a propositional formula, has been explored intensively and has gathered its own community. While most existing solvers are based on knowledge compilation, another promising approach is through contraction in tensor hypernetworks. We perform a theoretical proof-complexity analysis of this approach. For this, we design two new tensor-based proof systems that we show to tightly correspond to tensor-based #SAT solving. We determine the simulation order of #SAT proof systems and prove exponential separations between the systems. This sheds light on the relative performance of different #SAT solving approaches.

PDF Details DOI

AAAI Conference 2026 Conference Paper

Proof Systems That Tightly Characterise Model Counting Algorithms

Olaf Beyersdorff
Tim Hoffmann
Kaspar Kasche

Several proof systems for model counting have been introduced in recent years, mainly in an attempt to model #SAT solving and to allow proof logging of solvers. We reexamine these different approaches and show that: (i) with moderate adaptations, the conceptually quite different proof models of the dynamic system MICE and the static system of annotated Decision-DNNFs are equivalent and (ii) they tightly characterise state-of-the-art #SAT solving. Thus, these proof systems provide a precise and robust proof-theoretic underpinning of current model counting. We also propose new strengthenings of these proof systems that might lead to stronger model counters.

PDF Details DOI

NeurIPS Conference 2025 Conference Paper

Exploiting Dynamic Sparsity in Einsum

Christoph Staudt
Mark Blacher
Tim Hoffmann
Lea Kasche
Olaf Beyersdorff
Joachim Giesen

Einsum expressions specify an output tensor in terms of several input tensors. They offer a simple yet expressive abstraction for many computational tasks in artificial intelligence and beyond. However, evaluating einsum expressions poses hard algorithmic problems that depend on the representation of the tensors. Two popular representations are multidimensional arrays and coordinate lists. The latter is a more compact representation for sparse tensors, that is, tensors where a significant proportion of the entries are zero. So far, however, most of the popular einsum implementations use the multidimensional array representation for tensors. Here, we show on a non-trivial example that, when evaluating einsum expressions, coordinate lists can be exponentially more efficient than multidimensional arrays. In practice, however, coordinate lists can also be significantly less efficient than multidimensional arrays, but it is hard to decide from the input tensors whether this will be the case. Sparsity evolves dynamically in intermediate tensors during the evaluation of an einsum expression. Therefore, we introduce a hybrid solution where the representation is switched on the fly from multidimensional arrays to coordinate lists depending on the sparsity of the remaining tensors. In our experiments on established benchmark einsum expressions, the hybrid solution is consistently competitive with or outperforms the better of the two static representations.

PDF 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 2024 Conference Paper

The Relative Strength of #SAT Proof Systems

Olaf Beyersdorff
Johannes Klaus Fichte
Markus Hecher
Tim Hoffmann
Kaspar Kasche

The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps (knowledge compilation proof system), MICE (model counting induction by claim extension), and CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.

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