Knowledge compilation languages as proof systems

TL;DR

This paper explores how knowledge compilation languages like decision DNNF can be adapted as proof systems for higher complexity problems such as #SAT and maxSAT, extending the framework beyond coNP.

Contribution

It demonstrates how to modify existing knowledge compilation languages to serve as proof systems for problems in the polynomial hierarchy, specifically #SAT and maxSAT.

Findings

Decision DNNF can be used as proof systems for #SAT and maxSAT.

The approach extends Cook-Reckhow proof systems to higher complexity classes.

Framework provides new tools for certifying solutions in complex problems.

Abstract

In this paper, we study proof systems in the sense of Cook-Reckhow for problems that are higher in the polynomial hierarchy than coNP, in particular, #SAT and maxSAT. We start by explaining how the notion of Cook-Reckhow proof systems can be apply to these problems and show how one can twist existing languages in knowledge compilation such as decision DNNF so that they can be seen as proof systems for problems such as #SAT and maxSAT.

Figures

Equations

$$\underset{\tau \models f}{\max }|\{y\in Y\mid \tau (y)=1\}|.$$

Full text

1 Introduction

Proof complexity studies the hardness of finding a certificate that a CNF formula is not satisfiable. A minimal requirement for such a certificate is that it should be checkable in polynomial time in its size, so that it is easier for an independent checker to assess the correctness of the proof than to redo the computation made by a solver. While proof systems have been implicitly used for a long time starting with resolution [11, 10], their systematic study has been initiated by Cook and Reckhow [7] who showed that unless $\NP=\coNP$, one cannot design a proof system where all unsatisfiable CNF have short certificates. Nevertheless, many unsatisfiable CNF may have short certificates if the proof system is powerful enough, motivating the study of how such systems, such as resolution [10] or polynomial calculus [5], compares in terms of succinctness (see [18] for a survey). More recently, proof sytems found practical applications as SAT solvers are expected – since 2013 – to output proof of unsatisfiability in SAT competitions to avoid implementation bugs.

While the proof systems implicitly defined by the execution trace of modern CDCL SAT solvers is fairly well understood [20], it is not the case for tools solving harder problems on CNF formulas such as $\#\textsf{-}\mathsf{SAT}$ and $\mathsf{Max}\textsf{-}\mathsf{SAT}$. For $\mathsf{Max}\textsf{-}\mathsf{SAT}$, a resolution-like system for $\mathsf{Max}\textsf{-}\mathsf{SAT}$ has been proposed by Bonet et al. [2] for which a compressed version has been used in a solver by Bacchus and Narodytska [17] but it is to the best of our knowledge the only such proof system. To the best of our knowledge, no proof system has been proposed for $\#\textsf{-}\mathsf{SAT}$.

In this short paper, we introduce new proof systems for $\#\textsf{-}\mathsf{SAT}$ and $\mathsf{Max}\textsf{-}\mathsf{SAT}$. Contrary to the majority of proof systems for $\textsf{-}\mathsf{SAT}$, our proof systems are not based on the iterative application of inference rules on the original CNF formula. In our proof systems, our certificates are restricted Boolean circuits representing the Boolean function computed by the input CNF formula. These restricted circuits originate from the field of knowledge compilation [9], whose primary focus is to study the succinctness and tractability of representations such as Read Once Branching Programs [23] or deterministic DNNF [8] and how CNF formula can be transformed into such representations. To use them as certificates for $\#\textsf{-}\mathsf{SAT}$, we first have to add some extra information in the circuit so that one can check in polynomial time that they are equivalent to the original CNF. The syntactic properties of the input circuits then allow to efficiently count the number of satisfying assignments, resulting in the desired proof system. Moreover, we observe that most tools doing exact model counting are already implicitly generating such proofs. Our result generalizes known connections between regular resolution and Read Once Branching Programs (see [13, Section 18.2]).

The paper is organized as follows. Section 2 introduces all the notions that will be used in the paper. Section 3 contains the definition of certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ that allows us to define our proof systems for $\#\textsf{-}\mathsf{SAT}$ and $\mathsf{Max}\textsf{-}\mathsf{SAT}$.

2 Preliminaries

Assignments and Boolean functions.

Let $X$ be a finite set of variables and $D$ a finite domain. We denote the set of functions from $X$ to $D$ as $D^{X}$. An assignment on variables $X$ is an element of $\{0,1\}^{X}$. A Boolean function $f$ on variables $X$ is an element of $\{0,1\}^{\{0,1\}^{X}}$, that is, a function that maps an assignment to a value in $\{0,1\}$. An assignment $\tau\in\{0,1\}^{X}$ such that $f(\tau)=1$ is called a satisfying assignment of $f$, denoted by $\tau\models f$. We denote by $\bot_{X}$ the Boolean function on variables $X$ whose value is always [math]. Given two Boolean functions $f$ and $g$ on variables $X$, we write $f\Rightarrow g$ if for every $\tau$, $f(\tau)\leq g(\tau)$.

CNF.

Let $X$ be a set of variable. A literal on variable $X$ is either a variable $x\in X$ or the negation $\neg x$ of a variable $x\in X$. A clause is a disjunction of literals. A conjunctive normal form formula, CNF for short, is a conjunction of clauses. A CNF naturally defines a Boolean function on variables $X$: a satisfying assignment for a CNF $F$ on variable $X$ is an assignment $\tau\in\{0,1\}^{X}$ such that for every clause $C$ of $F$, there exists a literal $\ell$ of $C$ such that $\tau(\ell)=1$ (where we define $\tau(\neg x):=1-\tau(x)$). We often identify a CNF with the Boolean function it defines.

The problem $\textsf{-}\mathsf{SAT}$ is the problem of deciding, given a CNF formula $F$, whether $F$ has a satisfying assignment. It is the generic $\NP$-complete problem [6]. The problem $\mathsf{UNSAT}$ is the problem of deciding, given a CNF formula $F$, whether $F$ does not have a satisfying assignment. It is the generic $\coNP$-complete problem.

Given a CNF $F$, we denote by $\#F=|\{\tau\mid\tau\models F\}|$ the number of solutions of $F$ and by $M(F)=\max_{\tau}|\{C\in F\mid\tau\models C\}|$ the maximum number of clauses of $F$ that can be simultaneously satisfied. The problem $\#\textsf{-}\mathsf{SAT}$ is the problem of computing $\#F$ given a CNF $F$ as input and the problem $\mathsf{Max}\textsf{-}\mathsf{SAT}$ is the problem of computing $M(F)$ given a CNF $F$ as input.

Cook-Reckhow proof systems.

Let $\Sigma,\Sigma^{\prime}$ be finite alphabets. A (Cook-Reckhow) proof system [7] for a language $L\subseteq\Sigma^{*}$ is a surjective polynomial time computable function $f:\Sigma^{\prime}\rightarrow L$. Given $a\in L$, there exists, by definition, $b\in\Sigma^{\prime}$ such that $f(b)=a$. We will refer to $b$ as being a certificate of $a$.

In this paper, we will mainly be interested in proof systems for the problems $\#\textsf{-}\mathsf{SAT}$ and $\mathsf{Max}\textsf{-}\mathsf{SAT}$, that is, we would like to design polynomial time verifiable proofs that a CNF formula has $k$ solutions or that at most $k$ clauses in the formula can be simultaneously satisfied. For the definition of Cook-Reckhow, this could translate to finding a proof system for the languages $\{(F,\#F)\mid F\text{ is a CNF}\}$ and $\{(F,M(F))\mid F\text{ is a CNF}\}$.

For example, a naive proof system for $\#\textsf{-}\mathsf{SAT}$ could be the following: a certificate that $F$ has $k$ solutions would be the list of the $k$ solutions together with a resolution proof that $F^{\prime}=F\wedge\bigwedge_{\tau\mid\tau\models F}C_{\tau}$ is not satisfiable where $C_{\tau}:=\bigvee_{\{x\mid\tau(x)=0\}}x\vee\bigvee_{\{\neg x\mid\tau(x)=1\}}\neg x$ is the clause such that the only non-satisfying assignment is $\tau$. One could then check in polynomial time that each of the $k$ assignments satisfies $F$ and that $F^{\prime}$ is indeed unsatisfiable and then output $(F,k)$. This proof system is however not very interesting as one can construct very simple CNF with exponentially many solutions: for example the empty CNF on $n$ variables has $2^{n}$ and will thus have a certificate of size at least $2^{n}$.

$\mathsf{dec}\textsf{-}\mathsf{DNNF}$.

A decision Decomposable Negation Normal Form circuit $D$ on variables $X$, $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ for short, is a directed acyclic graph (DAG) having exactly one node of indegree [math] called the source. Nodes of outdegree [math] are called the sinks and are labeled by [math] or $1$. The other nodes have outdegree $2$ and can be of two types:

• •

The decision nodes are labeled with a variable $x\in X$. One outgoing edge is labeled with $1$ and the other by [math], represented respectively as a solid and a dashed edge in our figures.

• •

The $\wedge$-nodes are labeled with $\wedge$.

Moreover, we have two other syntactic properties. We introduce a few notations before explaining them. If there is a decision node in $D$ labeled with variable $x$, we say that $x$ is tested in $D$. We denote by $\mathsf{var}(D)$ the set of variables tested in $D$. Given a node $\alpha$ of $D$, we denote by $D(\alpha)$ the $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ whose source is $\alpha$ and nodes are the nodes that can be reached in $D$ starting from $\alpha$. We also assume the following:

• •

Every $x\in X$ is tested at most once on every source-sink path of $D$.

• •

Every $\wedge$-gate of $D$ are decomposable, that is, for every $\wedge$-node $\alpha$ with successors $\beta,\gamma$ in $D$, it holds that $\mathsf{var}(D(\beta))\cap\mathsf{var}(D(\gamma))=\emptyset$.

Let $\tau\in\{0,1\}^{X}$. A source-sink path $P$ in $D$ is compatible with $\tau$ if and only if when $x$ is tested on $P$, the outgoing edge labeled with $\tau(x)$ is in $P$. We say that $\tau$ satisfies $D$ if only $1$-sinks are reached by paths compatible with $\tau$. A $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ and the paths compatible with the assignment $\tau(x)=\tau(y)=0,\tau(z)=1$ are depicted in bold red on Figure 1. Observe that a [math]-sink is reached so $\tau$ does not satisfy $D$. We will often identify a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ with the Boolean function it computes.

Observation 1

Given a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$ on variables $X$ and a source-sink path $P$ in $D$, there exists $\tau\in\{0,1\}^{X}$ such that $P$ is compatible with $\tau$. Indeed, by definition, every variable $x\in X$ is tested at most once in $P$, thus, if $x$ is tested on $P$ in a decision node $\alpha$ and $P$ contains the outgoing edge labeled with $v_{x}$, we can choose $\tau(x):=v_{x}$. The value of $\tau$ for a variable $x$ not tested on $P$ can be chosen arbitrarily.

The size of a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$, denoted by $\mathsf{size}(D)$ is the number of edges of the underlying graph of $D$.

Tractable queries.

The main advantage of representing a Boolean function with a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ is that it makes the analysis of the function easier. Given a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$, one can easily find a satisfying assignment by only following paths backward from $1$-sinks. Similarly, one can also count the number of satisfying assignments or find one satisfying assignment with the least number of variables set to $1$ etc. The relation between the queries that can be solved efficiently and the representation of the Boolean function has been one focus of Knowledge Compilation. See [9] for an exhaustive study of tractable queries depending on the representation. Let $f:2^{X}\rightarrow\{0,1\}$ be a Boolean function. In this paper, we will mainly be interested in solving the following problems:

• •

Model Counting Problem ($\mathsf{MC}$): return the number of satisfying assignment of $f$.

• •

Clause entailment ($\mathsf{CE}$): given a clause $C$ on variables $X$, does $f\Rightarrow C$?

• •

Maximal Hamming Weight ($\mathsf{HW}$): given $Y\subseteq X$, compute

[TABLE]

All these problems are tractable when the Boolean function is given as a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$:

Theorem 2.1 ([8, 14])

Given a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$, one can solve problems $\mathsf{MC},\mathsf{CE},\mathsf{HW}$ on the Boolean function represented by $D$ in linear time in $\mathsf{size}(D)$.

The tractability of $\mathsf{CE}$ on $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ has the following useful consequence:

Corollary 1

Given a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$ and a CNF formula $F$, one can check in time $O(\mathsf{size}(F)\times\mathsf{size}(D))$ whether $D\Rightarrow F$.

Proof

One simply has to check that for every clause $C$ of $F$, $D\Rightarrow C$, which can be done in polynomial time by Theorem 2.1.

3 Knowledge compilation based proof systems

Theorem 2.1 suggests that given a CNF $F$, one could use a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$ computing $F$ as a certificate for $\#\textsf{-}\mathsf{SAT}$. The proof system could then check the certificate as follows:

Compute the number $k$ of satisfying assignments of $D$. 2. 2.

Check whether $F$ is equivalent to $D$. 3. 3.

If so, return $(F,k)$.

While Step 1 can be done in polynomial time by Theorem 2.1, it turns out that Step 2 is not tractable:

Theorem 3.1

The problem of checking, given a CNF $F$ and an $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$ as input, whether $F\Rightarrow D$ is $\coNP$-complete.

Proof

The problem is clearly in $\coNP$. For completeness, there is a straightforward reduction to $\mathsf{UNSAT}$. Indeed, observe that a CNF $F$ on variables $X$ is not satisfiable if and only if $F\Rightarrow\bot_{X}$. Moreover, $\bot_{X}$ is easily represented as a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ having only one node: a [math]-labeled sink.

3.1 Certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$

The reduction used in the proof of Theorem 3.1 suggests that the $\coNP$-completeness of checking whether $F\Rightarrow D$ comes from the fact that $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ can succinctly represent $\bot$. In this section, we introduce restrictions of $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ called certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ for which one can check whether a CNF formula entails the certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$. The idea is to add information on [math]-sink to explain which clause would be violated by an assignment leading to this sink.

Our inspiration comes from a known connection between regular resolution and read once branching programs (i.e. a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ without $\wedge$-gate [1]) that appears to be folklore but we refer the reader to the book by Jukna [13, Section 18.2] for a thorough and complete presentation. It turns out that a regular resolution111A regular resolution proof is a resolution proof where, on each path, a variable is resolved at most once. proof of unsatisfiability of a CNF $F$ can be represented by a read once branching program $D$ whose sinks are labeled with clauses of $F$. Moreover, for every $\tau$, if a sink labeled by a clause $C$ is reached by a path compatible with $\tau$, then $C(\tau)=0$. We generalize this idea so that the function represented by a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ is not only an unsatisfiable CNF:

Definition 1

A certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$ on variables $X$ is a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ on variables $X$ such that every [math]-sink $\alpha$ of $D$ is labeled with a clause $C_{\alpha}$. $D$ is said to be correct if for every $\tau\in\{0,1\}^{X}$ such that there is a path from the source of $D$ to a [math]-sink $\alpha$ compatible with $\tau$, $C_{\alpha}(\tau)=0$.

Given a certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$, we denote by $Z(D)$ the set of [math]-sinks of $D$ and by $F(D)=\bigwedge_{\alpha\in Z(D)}C_{\alpha}$.

Intuitively, the clause labeling a [math]-sink is an explanation on why one assignment does not satisfy the circuit. The degenerated case where there are only [math]-sinks and no $\wedge$-gates corresponds to the characterization of regular resolution.

A crucial property of certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ is that their correctness can be tested in polynomial time:

Theorem 3.2

Given a certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$, one can check in polynomial time whether $D$ is correct.

Proof

By definition, $D$ is not correct if and only if there exists a [math]-sink $\alpha$, a literal $\ell$ in $C_{\alpha}$, an assignment $\tau$ such that $\tau(\ell)=1$ and a path in $D$ from the source to $\alpha$ compatible with $\tau$. By Observation 1, it is equivalent to the fact that there exists a path from the source to $\alpha$ that: either does not test the underlying variable of $\ell$ or contains the outgoing edge corresponding to $\tau(\ell)=1$ when the underlying variable of $\ell$ is tested.

In other words, $D$ is correct if and only if for every [math]-sink $\alpha$ and for every literal $\ell$ of $C_{\alpha}$ with variable $x$, every path from the source to $\alpha$ tests variable $x$ and contains the outgoing edge corresponding to an assignment $\tau$ such that $\tau(\ell)=0$.

This can be checked in polynomial time. Indeed, fix a [math]-sink $\alpha$ and a literal $\ell$ of $C_{\alpha}$. For simplicity, we assume that $\ell=x$ (the case $\ell=\neg x$ is completely symmetric). We have to check that every path from the source to $\alpha$ contains a decision node $\beta$ on variable $x$ and contains the outgoing edge of $\beta$ labeled with [math]. To check this, it is sufficient to remove all the edges labeled with [math], going out of a decision node on variable $x$ and test that the source and $\alpha$ are now in two different connected components of $D$, which can obviously be done in polynomial time. Running this for every [math]-sink $\alpha$ and every literal $\ell$ of $C_{\alpha}$ gives the expected algorithm.

The clauses labeling the [math]-sinks of a correct certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ naturally connect to the function computed by $D$:

Theorem 3.3

Let $D$ be a correct certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ on variables $X$. We have $F(D)\Rightarrow D$.

Proof

Observe that $F(D)\Rightarrow D$ if and only if for every $\tau\in\{0,1\}^{X}$, if $\tau$ does not satisfy $D$ then $\tau$ does not satisfy $F(D)$. Now let $\tau$ be an assignment that does not satisfy $D$. By definition, there exists a path compatible with $\tau$ from the source of $D$ to a [math]-sink $\alpha$ of $D$. Since $D$ is correct, $C_{\alpha}(\tau)=0$. Thus, $\tau$ does not satisfy $F(D)$ as $C_{\alpha}$ is by definition a clause of $F(D)$.

Corollary 2

Let $F$ be CNF formula and $D$ be a correct certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ such that every clause of $F(D)$ are also in $F$. Then $F\Rightarrow D$.

3.2 Proof systems

Proof system for $\#\textsf{-}\mathsf{SAT}$.

One can use certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ to define a proof system for $\#\textsf{-}\mathsf{SAT}$. The Knowledge Compilation based Proof System for $\#\textsf{-}\mathsf{SAT}$, $\mathsf{kcps}(\#\textsf{-}\mathsf{SAT})$ for short, is defined as follows: given a CNF $F$, a certificate that $F$ has $k$ satisfying assignments is a correct certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$ such that:

• •

every clause of $F(D)$ are clauses of $F$,

• •

$D$ computes $F$ and has $k$ satisfying assignments.

To check a certificate $D$, one has to check that $D$ is equivalent to $F$ and has indeed $k$ satisfying assignments, which can be done in polynomial time as follows:

• •

Check that $D$ is correct, which is tractable by Theorem 3.2.

• •

Check that $D\Rightarrow F$, which is tractable by Corollary 1 and that every clause of $F(D)$ are clauses of $D$. By Corollary 2, it means that $D\Leftrightarrow F$.

• •

Computes the number $k$ of solutions of $D$, which is tractable by Theorem 2.1.

• •

Returns $(F,k)$.

This proof system for $\#\textsf{-}\mathsf{SAT}$ is particularly well-suited for the existing tools solving $\#\textsf{-}\mathsf{SAT}$ in practice. Many of them such as sharpSAT [22] or cachet [21] are based on a generalization of DPLL for counting which is sometimes refered as exhaustive DPLL in the literature. It has been observed by Huang and Darwiche [12] that these tools were implicitly constructing a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ equivalent to the input formula. Tools such as c2d [19], D4 [15] or DMC [16] already exploit this connection and have the option to directly output an equivalent $\mathsf{dec}\textsf{-}\mathsf{DNNF}$. These solvers explore the set of satisfying assignments by branching on variables of the formula which correspond to a decision node and, when two variable independent components of the formula are detected, compute the number of satisfying assignments of both components and take the product, which corresponds to a decomposable $\wedge$-gate. When a satisfying assignment is reached, it corresponds to a $1$-sink. If a clause is violated by the current assignment, then it corresponds to a [math]-sink. At this point, the solvers could also label the [math]-sink by the violated clause which would give a correct certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$.

Proof system for $\mathsf{Max}\textsf{-}\mathsf{SAT}$.

As for $\#\textsf{-}\mathsf{SAT}$, one can exploit the tractability of many problems on $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ to define a proof system for $\mathsf{Max}\textsf{-}\mathsf{SAT}$. Given a CNF formula $F$, ket $\tilde{F}=\bigwedge_{C\in F}C\vee\neg s_{C}$ be the formula where each clause is augmented with a fresh selector variable. Let $S=\{s_{C}\mid C\in F\}$. Observe that $M(F)$ is exactly $\max_{\tau\models\tilde{F}}|\{s\in S\mid\tau(s)=1\}|$ since if $\tau\models\tilde{F}$ and $\tau(s_{C})=1$, then $\tau\models C$. By Theorem 2.1, if $\tilde{F}$ is represented by a $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$, then one can solve this problem in polynomial time in $\mathsf{size}(D)$. The proof system $\mathsf{kcps}(\mathsf{Max}\textsf{-}\mathsf{SAT})$ is defined as follows: given a CNF $F$, a certificate is a correct certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ $D$ with clauses in $\tilde{F}$ that computes $\tilde{F}$. The proof may be checked as before by checking both the correctness of $D$ and the fact that $D\Leftrightarrow\tilde{F}$. However, we are not aware of any tool solving $\mathsf{Max}\textsf{-}\mathsf{SAT}$ based on this technique and thus the implementation of such a proof system in existing tools may not be realistic. It will still be worth comparing this proof system with the resolution for $\mathsf{Max}\textsf{-}\mathsf{SAT}$ [2].

In general, we observe that we can use this idea to build a proof system $\mathsf{kcps}(Q)$ for any tractable problem $Q$ on $\mathsf{dec}\textsf{-}\mathsf{DNNF}$. This could for example be applied to weighted versions of $\#\textsf{-}\mathsf{SAT}$ and $\mathsf{Max}\textsf{-}\mathsf{SAT}$.

Combining proof systems.

An interesting feature of $\mathsf{kcps}$-like proof systems is that they can be combined with other proof systems for $\mathsf{UNSAT}$ to be made more powerful. Indeed, one could label the [math]-sink of the $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ with a clause $C$ that are not originally in the initial CNF $F$ but that is entailed by $F$, that is, $F\Rightarrow C$. In this case, Corollary 2 would still hold. The only thing that is needed to obtain a real proof system is that a proof that $F\Rightarrow C$ has to be given along the correct certified $\mathsf{dec}\textsf{-}\mathsf{DNNF}$, that is, a proof of unsatisfiability of $F\wedge\neg C$. Any proof system for $\mathsf{UNSAT}$ may be used here.

Lower bounds.

Lower bounds on the size of $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ representing CNF formulas may be directly lifted to lower bounds for $\mathsf{kcps}(\#\textsf{-}\mathsf{SAT})$ or $\mathsf{kcps}(\mathsf{Max}\textsf{-}\mathsf{SAT})$. There exists families of monotone $2$-CNF that cannot be represented as polynomial size $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ [1, 3, 4]. It directly gives the following corollary:

Corollary 3

There exists a family $(F_{n})_{n\in\mathbb{N}}$ of monotone $2$-CNF such that $F_{n}$ is of size $O(n)$ and any proof for $F_{n}$ in $\mathsf{kcps}(\#\textsf{-}\mathsf{SAT})$ and $\mathsf{kcps}(\mathsf{Max}\textsf{-}\mathsf{SAT})$ is of size at least $2^{\Omega(n)}$.

An interesting open question is to find CNF formulas having polynomial size $\mathsf{dec}\textsf{-}\mathsf{DNNF}$ but no small proof in $\mathsf{kcps}(\#\textsf{-}\mathsf{SAT})$.

4 Future work

In this paper, we have developed techniques based on circuits used in knowledge compilation to extend existing proof systems for tautology to harder problems. It seems possible to implement these systems into existing tools for $\#\textsf{-}\mathsf{SAT}$ based on exhaustive DPLL, which would allow these tools to provide an independently checkable certificate that their output is correct, the same way $\textsf{-}\mathsf{SAT}$-solvers returns a proof on unsatisfiable instances. It would be interesting to see how adding the computation of this certificate to existing solver impacts their performances. Another interesting direction would be to compare the power of $\mathsf{kcps}(\mathsf{Max}\textsf{-}\mathsf{SAT})$ with the resolution for $\mathsf{Max}\textsf{-}\mathsf{SAT}$ of Bonet et al. [2] and to see how such proof systems could be implemented in existing tools for $\mathsf{Max}\textsf{-}\mathsf{SAT}$. Finally, we think that a systematic study of other languages used in knowledge compilation such as deterministic DNNF should be done to see if they can be used as proof systems, by trying to add explanations on why an assignment does not satisfy the circuit.