Proof Systems for Tensor-based Model Counting

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.

Authors

• Olaf Beyersdorff Friedrich-Schiller Universität Jena
• Joachim Giesen Friedrich-Schiller Universität Jena
• Andreas Goral Friedrich Schiller University Jena
• Tim Hoffmann
• Kaspar Kasche Friedrich Schiller University Jena
• Christoph Staudt Friedrich Schiller University Jena

Keywords

No keywords are indexed for this paper.