Proof Systems for Tensor-based Model Counting
Olaf Beyersdorff, Joachim Giesen, Andreas Goral, Tim Hoffmann, Kaspar Kasche, Christoph Staudt
Abstract
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.
BibTeX
@inproceedings{aaai2026_proofsystemsfort,
title = {Proof Systems for Tensor-based Model Counting},
author = {Olaf Beyersdorff and Joachim Giesen and Andreas Goral and Tim Hoffmann and Kaspar Kasche and Christoph Staudt},
booktitle = {AAAI 2026},
year = {2026}
}