A polynomial threshold function (PTF) is defined as the sign of a polynomial $p\colon\bool^n\to\mathbb{R}$. A PTF circuit is a Boolean circuit whose gates are PTFs. We study the problems of exact and (promise) approximate counting for PTF circuits of constant depth.

Satisfiability (#SAT). We give the first zero-error randomized algorithm ... more >>>

A fundamental problem in circuit complexity is to find explicit functions that require large depth to compute. When considering the natural DeMorgan basis of $\{\text{OR},\text{AND}\}$, where negations incur no cost, the best known depth lower bounds for an explicit function in NP have the form $(3-o(1))\log_2 n$, established by H{\aa}stad ... more >>>

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

In this paper we present a new proof system framework CLIP (Cumulation Linear Induction Proposition) for propositional model counting. A CLIP proof firstly involves a circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of ... more >>>

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 slight adaptations, the conceptually quite different proof models of the dynamic system MICE ... more >>>