# On the Complexity of Enumerating Prime Implicants
from Decision-DNNF Circuits

Alexis de Colnet1 &Pierre Marquis1,2 1Univ. Artois, CNRS, Centre de Recherche
en Informatique de Lens (CRIL), F-62300 Lens, France
2Institut Universitaire de France {decolnet<EMAIL_ADDRESS>
###### Abstract

We consider the problem Enum$\cdot\textit{IP}$ of enumerating prime implicants
of Boolean functions represented by decision decomposable negation normal form
(dec-DNNF) circuits. We study Enum$\cdot\textit{IP}$ from dec-DNNF within the
framework of enumeration complexity and prove that it is in OutputP, the class
of output polynomial enumeration problems, and more precisely in IncP, the
class of polynomial incremental time enumeration problems. We then focus on
two closely related, but seemingly harder, enumeration problems where further
restrictions are put on the prime implicants to be generated. In the first
problem, one is only interested in prime implicants representing subset-
minimal abductive explanations, a notion much investigated in AI for more than
three decades. In the second problem, the target is prime implicants
representing sufficient reasons, a recent yet important notion in the emerging
field of eXplainable AI, since they aim to explain predictions achieved by
machine learning classifiers. We provide evidence showing that enumerating
specific prime implicants corresponding to subset-minimal abductive
explanations or to sufficient reasons is not in OutputP.

##  1 Introduction

Prime implicants are a key concept when dealing with Boolean functions since
the notion has been introduced seven decades ago Quine (1952). Within AI,
prime implicants (or the dual concept of prime implicates) have been
considered for modeling and solving a number of problems, including compiling
knowledge Reiter and de Kleer (1987) and generating explanations of various
kinds. This is the case in logic-based abductive reasoning (see e.g., Selman
and Levesque (1990); Eiter and Gottlob (1995)), a form of inference required
in a number of applications when the available knowledge base is incomplete
(e.g., in medicine) and because of such an incompleteness, it cannot alone
explain the observations that are made about the state of the world. Abduction
gave rise to much research in AI for the past three decades, especially
because it is closely connected to other reasoning settings, including truth
maintenance de Kleer (1986), assumption-based reasoning and closed-world
reasoning (see e.g., Marquis (2000) for a survey). Formally, the explanations
one looks for are terms over a preset alphabet (composed of the so-called
abducible variables, e.g., representing diseases) such that the manifestations
that are reported (e.g., some symptoms) are logical consequences of the
background knowledge when completed by such a term. In order to avoid trivial
explanations, one also asks those terms to be consistent with the knowledge
base. Explanations that are the less demanding ones from a logical standpoint
(i.e., subset-minimal ones) can be characterized as specific prime implicants.
More recently, deriving explanations justifying why certain predictions have
been made has appeared as essential for ensuring trustworthy Machine Learning
(ML) technologies Miller (2019); Molnar (2019). In the research area of
eXplainable AI (XAI), recent work has shown how ML classifiers of various
types (including black boxes) can be associated with Boolean circuits (alias
transparent or “white” boxes), exhibiting the same input-output behaviours
Narodytska et al. (2018); Shih et al. (2018a, 2019). Thanks to such mappings,
XAI queries about classifiers can be delegated to the corresponding circuits.
The notion of sufficient reason of an instance given a Boolean function $f$
modeling a binary classifier has been introduced in Darwiche and Hirth (2020).
Given an instance $a$ ($a$ simply is an assignment, i.e., a vector of truth
values given to each of the $n$ variables) such that $f(a)=1$ (resp.
$f(a)=0$), a sufficient reason for $a$ is a subset-minimal partial assignment
$a^{\prime}$ which is coherent with $a$ (i.e., $a$ and $a^{\prime}$ give the
same values to the variables that are assigned in $a^{\prime}$) and which
satisfies the property that for every extension $a^{\prime\prime}$ of
$a^{\prime}$ we have $f(a^{\prime\prime})=1$ (resp. $f(a^{\prime\prime})=0$).
The features assigned in $a^{\prime}$ (and the way they are assigned) can be
viewed as explaining why $a$ has been classified by $f$ as a positive (or as a
negative) instance.

Whatever the way prime implicants are used, generating them is in general a
computationally demanding task, for at least two reasons. On the one hand,
deriving a single prime implicant of a Boolean function represented by a
propositional formula (or circuit) is NP-hard since such a formula is
satisfiable when it has a prime implicant, and it is valid precisely when this
prime implicant is the empty term. On the other hand, a source of complexity
is the number of prime implicants that may prevent from computing them all.
Indeed, it is well-known that the number of prime implicants of a Boolean
function can be exponential in the number of variables of the function, and,
for many representations of the function, also exponential in the size of the
representation (just consider the parity function as a matter of example). In
more detail, the number of prime implicants of a Boolean function can be
larger than the number of assignments satisfying the function Dunham and
Fridshal (1959); there also exist families of Boolean functions over $n$
variables having $\Omega(\frac{3^{n}}{n})$ prime implicants Chandra and
Markowsky (1978).

In this paper, we focus on the issue of _enumerating prime implicants of a
Boolean function represented by a decision decomposable negation normal form
circuit (alias a dec-DNNF circuit)_. The question is to determine whether such
prime implicants _can be enumerated “efficiently”_ , which is obviously not
the case when the circuit considered is unconstrained (as explained above, in
such a case, computing a single prime implicant is already hard). This
question is important for all the problems listed previously, when prime
implicants represent explanations: since they are typically too numerous to be
computed as a whole, it makes sense to derive them in an incremental way, with
some performance guarantees in the generation; this lets the user who asked
for an explanation deciding what to do after each derivation, namely to stop
the enumeration process since he/she is satisfied by the explanation that has
been provided, or alternatively to ask for a further explanation.

The dec-DNNF language Oztok and Darwiche (2014); Darwiche (2001) and its
subsets FBDD (free binary decision diagrams) Gergov and Meinel (1994), OBDD
(ordered binary decision diagrams) Bryant (1986) and even DT (the set of all
binary decision trees over Boolean variables, see e.g., (Wegener, 2000,
Chapter 2)) appear at first sight as good candidates for representing the
function in the perspective of enumerating “efficiently” its prime implicants.
Indeed, they are known as tractable representation languages (they support in
polynomial time many queries and transformations from the so-called knowledge
compilation map Darwiche and Marquis (2002); Koriche et al. (2013)).

The main contribution of the paper is as follows. We give a polynomial
incremental time algorithm for enumerating the prime implicants of a Boolean
function $f$ represented by a dec-DNNF circuit $\Sigma$. Given $\Sigma$ and a
positive integer $k$, this algorithm returns $k$ prime implicants of $\Sigma$
in $O(poly(k+|\Sigma|))$ time, or returns all prime implicants of $\Sigma$ if
there are fewer than $k$. This shows that enumerating prime implicants from
dec-DNNF is in the enumeration complexity class IncP Strozecki (2019). We also
provide evidence showing that enumerating specific prime implicants
corresponding to subset-minimal abductive explanations or to sufficient
reasons is not in OutputP: on the one hand, computing a single subset-minimal
abductive explanation from an OBDD circuit or a decision tree is NP-hard; on
the other hand, the existence of an output polynomial time algorithm for
enumerating sufficient reasons from an OBDD circuit or a decision tree would
lead to an output polynomial time algorithm for enumerating the minimal
transversals of a hypergraph, thus answering a long-standing question related
to monotone dualization Eiter et al. (2008).

The rest of the paper is organized as follows. We start with some
preliminaries (Section 2) where the language of dec-DNNF circuits and the
framework used to study enumeration problems are presented. We formally define
the problem Enum$\cdot\textit{IP}$ of enumerating prime implicants. Then in
Section 3 we show that generating the set of _all_ prime implicants from a
dec-DNNF circuit is feasible in output polynomial time. From there, we show in
Section 4 that Enum$\cdot\textit{IP}$ from dec-DNNF is in fact in IncP and
point out a polynomial incremental time enumeration algorithm. Finally, in
Section 5 we focus on subset-minimal abductive explanations and sufficient
reasons and show that for each of the two cases, the enumeration issue is
seemingly harder than in the case when all prime implicants are considered.
All the proofs are reported in a final appendix.

##  2 Preliminaries

A Boolean function over $n$ variables $x_{1},\dots,x_{n}$ is a mapping $f$
from $\\{0,1\\}^{n}$ to $\\{0,1\\}$. The set of variables of $f$ is denoted by
$var(f)$. The assignments to $var(f)$ mapped to $1$ by $f$ are called
_satisfying assignments_ of $f$. A literal upon variable $x$ is either $x$ or
its negation $\overline{x}$ and a _term_ is a conjunction of literals. We
often omit the conjunction symbols when writing terms, for instance we may
shorten $a\land\overline{c}$ into $a\,\overline{c}$. We define the _empty_
term $t_{\emptyset}$ as the term over zero literal. The empty term verifies
$t\land t_{\emptyset}=t$ for every term $t$. Given
$\ell\in\\{x,\overline{x}\\}$, we denote by $f|\ell$ the Boolean function over
$var(f)\setminus\\{x\\}$ whose satisfying assignments coincide with that of
$f\land\ell$. We use the usual symbols $\land$, $\lor$, $\neg$, $\models$ to
denote conjunction, disjunction, negation, and entailment. Given a set $S$ of
terms, $\max(S,\models)$ denotes the subset of terms of $S$ that do not entail
another term in $S$. An _implicant_ of a Boolean function $f$ is a term $t$
whose satisfying assignments also satisfy $f$, i.e., $t\models f$. An
implicant $t$ is _prime_ when no term $t-\ell$ obtained by removing a literal
$\ell$ from $t$ is an implicant of $f$.

###  2.1 Compilation Languages

Compilation languages are often seen as classes of circuits. Let $PS$ be a
countable set of propositional variables. A circuit in _negation normal form_
(NNF) is a directed acyclic graph (DAG) whose leaves are labelled with $0$
(_false_), $1$ (_true_), or a literal built upon $x\in PS$, and whose internal
nodes are labelled with $\land$ or $\lor$ connectives; we call them
$\land$-nodes and $\lor$-nodes. An NNF circuit computes a Boolean function
over the variables appearing in it. For $v$ a node of an NNF circuit $\Sigma$,
$var(v)$ denotes the set of variables labelling leaves under $v$ in $\Sigma$
and $\Sigma_{v}$ denotes the subcircuit of $\Sigma$ rooted at $v$. The
language of _decomposable_ NNF (DNNF) contains the NNF circuits where
$\land$-nodes are decomposable, that is, the children $v_{1},\dots,v_{m}$ of
every $\land$-node $v$ are such that $var(v_{i})\cap var(v_{j})=\emptyset$ for
all $i\neq j$. The language of _deterministic, decomposable_ NNF (d-DNNF)
contains the DNNF circuits $\Sigma$ where $\lor$-nodes are deterministic, that
is, the children $v_{1},\dots,v_{m}$ of every $\lor$-node $v$ are such that
$\Sigma_{v_{i}}\wedge\Sigma_{v_{j}}$ is inconsistent for all $i\neq j$.
Finally, the language of _decision_ DNNF (dec-DNNF) is that of circuits whose
leaves are labelled with $0$, $1$, or a literal built upon $x\in PS$, and
whose internal nodes are decision nodes and $\land$-nodes. Whenever $n$ is a
decision node labelled by variable $x$ in a dec-DNNF circuit $\Sigma$, the
circuit $\Sigma_{n}$ given by  $x$$u$$v$ is viewed as a compact representation
of the d-DNNF circuit  $\lor$$\land$$\land$$\overline{x}$$x$$u$$v$ (see
Definition 2.6 and Figure 2 in Darwiche and Marquis (2002)).

Thus, a decision node $n$ is labelled by a variable and has two children: the
0-child (node $u$ on the previous picture) and the 1-child (node $v$ on the
previous picture). If $n$ is labelled by $x$ and $\Sigma_{u}$ (resp.
$\Sigma_{v}$) represents the function $f_{0}$ (resp. $f_{1}$), then
$\Sigma_{n}$ represents the function $(\overline{x}\land f_{0})\lor(x\land
f_{1})$. For instance, Figure 1(a) gives a dec-DNNF circuit whose deepest
decision node computes $(\overline{s}\land 1)\lor(s\land p)$. It is worth
mentioning that all Boolean functions on finitely many variables can be
represented in dec-DNNF, or indeed in any of its subsets like FBDD, OBDD, and
DT.

Let $\Sigma$ be a dec-DNNF circuit. The size of $\Sigma$, denoted by
$|\Sigma|$ is its number of edges. From a dec-DNNF circuit $\Sigma$, one can
easily derive in polynomial time a dec-DNNF circuit equivalent to $\Sigma$
where every $\land$-node has exactly two children. Since it is computationally
harmless, for the sake of simplicity, our enumeration algorithms suppose that
the dec-DNNF circuits satisfy this condition, so that their size is at most
twice their number of nodes. In the same vein, we suppose that our dec-DNNF
circuits have been _reduced_ , i.e., every node $v$ in $\Sigma$ such that
$\Sigma_{v}$ computes the 0 function reduces to a leaf labelled by $0$.
Testing the satisfiability of a dec-DNNF circuit is feasible in linear time
Darwiche and Marquis (2002), so reducing a dec-DNNF circuit also is a
polynomial-time operation.

###  2.2 Enumeration Complexity

We now recall some enumeration complexity classes as described in Strozecki
(2019). Let $V$ be an alphabet and let $A$ be a binary predicate in
$V^{*}\times V^{*}$. Given an instance $x\in V^{*}$ (the input), $A(x)$ (the
set of solutions) denotes the set of all $y\in V^{*}$ such that $A(x,y)$. The
enumeration problem Enum$\cdot A$ is the function mapping $x$ to $A(x)$.
Enum$\cdot A$ is in the class EnumP if for every $y\in A(x)$, $|y|$ is
polynomial in $|x|$, and if deciding whether $y$ is in $A(x)$ is in P. EnumP
does not capture the complexity of _computing_ the set of solutions $A(x)$, it
serves more as a counterpart of NP for enumeration problems.

The model used for the enumeration of solutions is the random access machine
(RAM) model. See Strozecki (2019) for details on why RAM have been chosen for
this task. A RAM solves Enum$\cdot A$ if, for all $x$, it returns a sequence
$y_{1},\dots,y_{m}$ of pairwise distinct elements such that
$\\{y_{1},\dots,y_{m}\\}=A(x)$. Enum$\cdot A$ is in OutputP if there is a RAM
solving Enum$\cdot A$ in time $O(poly(|x|+|A(x)|))$ on every input $x$.
OutputP is a relevant enumeration class when the whole set of solutions is
explicitly asked for. For instance, the dualization of a monotone CNF formula
$\phi$ is the task of generating a DNF formula equivalent to $\phi$. Because
of the monotony condition on $\phi$, the terms used in any smallest DNF
formula equivalent to $\phi$ are precisely its prime implicants. Thus, the
dualization problem boils down to enumerating _all_ the prime implicants of
$\phi$.

For other applications, computing only a fixed number of solutions may be
enough. A RAM solves Enum$\cdot A$ in incremental time $f(t)g(n)$ if on every
$x$, it runs in time time $O(f(t)g(|x|))$ and returns a sequence
$y_{1},\dots,y_{t}$ of $t$ pairwise distinct elements of $A(x)$ when
$t\leq|A(x)|$, and the whole set $A(x)$ when $t>|A(x)|$. Enum$\cdot A$ is in
IncP if there is a RAM that solves $A$ in incremental time $O(t^{a}n^{b})$ for
some constants $a$ and $b$. IncP has a characterization that uses the function
problem AnotherSol$\cdot A$ which, given $x$ and $S\subseteq A(x)$, returns
$y\in A(x)\setminus S$ when $S\neq A(x)$, and false otherwise.

$h$$e$$e$$\land$$\land$$b$$\,\overline{p}$$\overline{s}$$\overline{b}$$s$$\overline{p}$$1$$p$
(a) A dec-DNNF circuit

$h$$v_{0}\\!:$$e$$e$$v_{1}\\!:$$\land$$\land$$b$$v_{2}\\!:$$\,\overline{p}$$\overline{s}$$\overline{b}$$s$$v_{3}\\!:$$\overline{p}$$1$$p$$S_{3}=\emptyset$$S_{0}=\\{h\,\overline{e}\,b\,\overline{p}\,,\,\,h\,\overline{p}\,\overline{s}\,,\,\,\overline{e}\,\overline{p}\,\overline{s}\\}$$S_{2}=\\{b\,\overline{p}\,,\,\,\overline{p}\,\overline{s}\\}$$S_{1}=\\{\overline{e}\,b\,\overline{p}\,,\,\,\overline{p}\,\overline{s}\\}$
(b) A path followed in MissingIP

$h$$v_{0}\\!:$$e$$e$$v_{1}\\!:$$\land$$\land$$b$$v_{2}\\!:$$\,\overline{p}$$\overline{s}$$\overline{b}$$s$$v_{3}\\!:$$\overline{p}$$1$$p$$h\,\overline{e}\,\overline{b}\,\overline{s}\in\textit{IP}(\Sigma_{v_{0}})$$\overline{s}\in\textit{IP}(\Sigma_{v_{3}})$$\overline{e}\,\overline{b}\,\overline{s}\in\textit{IP}(\Sigma_{v_{1}})$$\overline{b}\,\overline{s}\in\textit{IP}(\Sigma_{v_{2}})$
(c) Propagation of an implicant

Figure 1: Generation of a new prime implicant from a dec-DNNF circuit

######  Proposition 1 (Strozecki (2019)).

A problem Enum$\cdot A$ in EnumP is in IncP if and only if AnotherSol$\cdot A$
is in FP.

Note that OutputP is thought to be distinct from IncP Strozecki (2019).

##  3 Enum$\cdot$IP from dec-DNNF is in OutputP

Let us first consider the problem of enumerating the prime implicants of a
Boolean function $f$ given as a dec-DNNF circuit $\Sigma$, for short the prime
implicants of $\Sigma$. Let $\textit{IP}(\Sigma,t)$ be the binary predicate
representing the relation that $t$ is a prime implicant of $\Sigma$. Then
$\textit{IP}(\Sigma)$ denotes the set of prime implicants of $\Sigma$. We
extend the notation $\textit{IP}(\cdot)$ to any Boolean function $f$. To be
able to speak of prime implicants enumeration from circuits other than dec-
DNNF ones we write “Enum.IP from $L$” with $L$ the language $\Sigma$ belongs
to.

We start with a couple of easy results. First of all, since there is a linear-
time procedure to verify that a term is an implicant of a dec-DNNF circuit,
there is a polynomial-time algorithm to decide whether a given a term is a
prime implicant of a dec-DNNF circuits, thus:

######  Proposition 2.

Enum$\cdot\textit{IP}$ from dec-DNNF is in EnumP.

In addition, it is known that Enum$\cdot\textit{IP}$ from OBDD is in OutputP
Madre and Coudert (1991), and it is almost straightforward to extend this
result to dec-DNNF. To make it precise, let us briefly describe the output
polynomial construction of $\textit{IP}(\Sigma)$ for $\Sigma$, a dec-DNNF
circuit. The construction is based on the three following, folklore
propositions (for the sake of completeness, a proof for each of them is
nonetheless reported as a supplementary material).

######  Proposition 3.

Let $f$ and $g$ be Boolean functions, then $\textit{IP}(f\land
g)=\max(\\{t\land t^{\prime}\mid
t\in\textit{IP}(f),\,t^{\prime}\in\textit{IP}(g)\\},\models).$ Furthermore if
$var(f)\cap var(g)=\emptyset$, then $\textit{IP}(f\land g)=\\{t\land
t^{\prime}\mid t\in\textit{IP}(f),\,t^{\prime}\in\textit{IP}(g)\\}.$

######  Proposition 4.

Let $f$ a Boolean function, let $x$ be a variable, and let
$\ell\in\\{x,\overline{x}\\}$. Consider $t\in\textit{IP}(f|\ell)$. If
$t\models f|\overline{\ell}$, then $t\in\textit{IP}(f)$, otherwise
$t\land\ell\in\textit{IP}(f)$.

######  Proposition 5.

Let $f$ be a Boolean function and let $x$ be a variable.

$\displaystyle\textit{IP}(f)=$ $\displaystyle\\{t\land\overline{x}\mid
t\in\textit{IP}(f|\overline{x}),\,t\not\models f|x\\}$ $\displaystyle\cup$
$\displaystyle\\{t\land x\mid t\in\textit{IP}(f|x),\,t\not\models
f|\overline{x}\\}$ $\displaystyle\cup$
$\displaystyle\textit{IP}(f|\overline{x}\land f|x)$

Note that $t\in\textit{IP}(f|\overline{x})$ (resp. $\textit{IP}(f|x)$) entails
$f|x$ (resp. $f|\overline{x})$ if and only if $t$ is subsumed by some term in
$\textit{IP}(f|\overline{x}\land f|x)$. As a consequence, from
$\textit{IP}(f|\overline{x})$ and $\textit{IP}(f|x)$, one can construct
$\textit{IP}(f|\overline{x}\land f|x)$ in polynomial time thanks to
Proposition 3 and we use it to derive $\textit{IP}(f)$ thanks to Proposition
5.

We also have that (see the algorithm for conditioning a prime implicant
representation provided in Darwiche and Marquis (2002)):

######  Proposition 6.

Let $f$ a Boolean function and let $x$ be a variable, then
$|\textit{IP}(f)|\geq\max(|\textit{IP}(f|\overline{x})|,|\textit{IP}(f|x)|)$.

Consider now a dec-DNNF circuit $\Sigma$ and an internal node $v$ with two
children $u$ and $w$. If the sets $\textit{IP}(\Sigma_{u})$ and
$\textit{IP}(\Sigma_{w})$ are provided, then $\textit{IP}(\Sigma_{v})$ is
obtained in polynomial time using Proposition 3 if $v$ is a decomposable
$\land$-gate, and using Proposition 5 if $v$ is a decision node. Furthermore,
in both cases, we have
$|\textit{IP}(\Sigma_{v})|\geq\max(|\textit{IP}(\Sigma_{u})|,|\textit{IP}(\Sigma_{w})|)$.
These observations lead to a simple algorithm that generates
$\textit{IP}(\Sigma)$ by computing the sets $\textit{IP}(\Sigma_{v})$ for
every node $v$ of $\Sigma$ considered in a bottom-up way. Since constructing
the set of prime implicants for any node given that of its children is
tractable, since this set is smaller than $|\textit{IP}(\Sigma)|$, and since
it is computed only once, the algorithm runs in time
$O(poly(|\Sigma|+|\textit{IP}(\Sigma)|))$. Thus, we get:

######  Proposition 7.

Enum$\cdot\textit{IP}$ from dec-DNNF is in OutputP.

######  Example 1.

We give the construction of the sets of prime implicants for the nodes
$v_{1},v_{2},v_{3}$ in the dec-DNNF circuit $\Sigma$ represented on Figure
1(b).

  * $v_{3}$:

the sets of prime implicants of the children are
$\textit{IP}(1)=\\{t_{\emptyset}\\}$ and $\textit{IP}(p)=\\{p\\}$. Using
Proposition 5 we have that $\overline{s}\land t_{\emptyset}=\overline{s}$ and
$\Sigma_{v_{3}}|s=p$, so $\overline{s}\land
t_{\emptyset}\not\models\Sigma_{v_{3}}|s$ showing that
$\overline{s}\in\textit{IP}(\Sigma_{v_{3}})$. We also have that
$\Sigma_{v_{3}}|\overline{s}=1$, so $s\,p\models\Sigma_{v_{3}}|\overline{s}$
showing that $s\,p\not\in\textit{IP}(\Sigma_{v_{3}})$. Finally, we have that
$\textit{IP}(\Sigma_{v_{3}}|s\land\Sigma_{v_{3}}|\overline{s})=\\{p\\}$ by
Proposition 3, so $\textit{IP}(\Sigma_{v_{3}})=\\{\overline{s},p\\}$.

  * $v_{2}$:

the sets of prime implicants of the children are
$\textit{IP}(\overline{p})=\\{\overline{p}\\}$ and
$\textit{IP}(\Sigma_{v_{3}})$ so we compute
$\textit{IP}(\Sigma_{v_{2}})=\\{b\,\overline{p},\overline{b}\,\overline{s},\overline{b}\,p,\overline{p}\,\overline{s}\\}$

  * $v_{1}$:

the sets of prime implicants of the children are
$\textit{IP}(\overline{p}\land\overline{s})=\\{\overline{p}\,\overline{s}\\}$
and $\textit{IP}(\Sigma_{v_{2}})$ so we compute
$\textit{IP}(\Sigma_{v_{1}})=\\{\overline{e}\,\overline{b}\,p,\overline{e}\,b\,\overline{p},\overline{e}\,\overline{b}\,\overline{s},\overline{p}\,\overline{s}\\}$

##  4 Enum$\cdot$IP from dec-DNNF is in IncP

We now investigate Enum$\cdot$IP from dec-DNNF from the incremental
enumeration perspective. Based on Proposition 1, we design a tractable
algorithm AnotherIP for solving the problem AnotherSol$\cdot\textit{IP}$, thus
showing that Enum$\cdot\textit{IP}$ from dec-DNNF is in IncP.

###  4.1 Solving the decision variant of AnotherSol$\cdot$IP

We first consider the decision variant of AnotherSol$\cdot\textit{IP}$ from
dec-DNNF: given a dec-DNNF circuit $\Sigma$ and a set
$S\subseteq\textit{IP}(\Sigma)$, return _false_ if and only if
$S\neq\textit{IP}(\Sigma)$. Recall from the discussion preceding Proposition 7
that there is a bottom-up procedure for generating all prime implicants of the
dec-DNNF circuit $\Sigma$. To address the decision variant of
AnotherSol$\cdot\textit{IP}$ on inputs $\Sigma$ and $S$, a reverse, top-down
search is performed, assuming that $S$ is $\textit{IP}(\Sigma)$ until finding
a contradiction.

Before defining what a contradiction means in this setting, a few notations
are useful. For $t$ a term and $X$ a set of variables, $t_{X}$ denotes the
restriction of $t$ to variables in $X$. Note that if $X$ and $var(t)$ are
disjoint, then $t_{X}$ is the empty term $t_{\emptyset}$.

######  Proposition 8.

Let $\Sigma$ be a dec-DNNF circuit and let $S\subseteq\textit{IP}(\Sigma)$. If
the root of $\Sigma$ is an $\land$-node, let $u$ and $w$ be its children and
let $S_{u}=\\{t_{var(\Sigma_{u})}\mid t\in S\\}$ and
$S_{w}=\\{t_{var(\Sigma_{w})}\mid t\in S\\}$. Then
$S_{u}\subseteq\textit{IP}(\Sigma_{u})$ and
$S_{w}\subseteq\textit{IP}(\Sigma_{w})$ hold, and

$\displaystyle S=\textit{IP}(\Sigma)\text{ iff }$ $\displaystyle
S_{u}=\textit{IP}(\Sigma_{u})\text{ and }S_{w}=\textit{IP}(\Sigma_{w})$ and
$\displaystyle S=\\{t_{u}\land t_{w}\mid t_{u}\in S_{u},t_{w}\in S_{w}\\}.$

######  Proposition 9.

Let $\Sigma$ be a dec-DNNF circuit whose root is a decision node labelled by
$x$. Let $u$ be its 0-child and $w$ be its 1-child. Given
$S\subseteq\textit{IP}(\Sigma)$, let $S_{u}=\\{t\mid t\land\overline{x}\in
S\\}\cup(S\cap\textit{IP}(\Sigma_{u}))$, $S_{w}=\\{t\mid t\land x\in
S\\}\cup(S\cap\textit{IP}(\Sigma_{w}))$ and $S^{\prime}=\\{t\mid t\in
S,x\not\in var(t)\\}$. Then $S_{u}\subseteq\textit{IP}(\Sigma_{u})$ and
$S_{w}\subseteq\textit{IP}(\Sigma_{w})$ hold, and

$\displaystyle S=\textit{IP}(\Sigma)\text{ iff }$ $\displaystyle
S_{u}=\textit{IP}(\Sigma_{u})\text{ and }S_{w}=\textit{IP}(\Sigma_{w})$ and
$\displaystyle S^{\prime}=\max(\\{t_{u}\land t_{w}\mid t_{u}\in
S_{u},\,t_{w}\in S_{w}\\},\models).$

Let $v$ be the root of the dec-DNNF circuit $\Sigma$ and let
$S\subseteq\textit{IP}(\Sigma)$. We say that we have a _contradiction_ at node
$v$ when

  * (c1)

$S=\emptyset$ while $\Sigma$ is satisfiable, or

  * (c2)

$v$ is a decision node, $S_{u}=\textit{IP}(\Sigma_{u})$ and
$S_{w}=\textit{IP}(\Sigma_{w})$, but $S^{\prime}\neq\max(\\{t_{u}\land
t_{w}\mid t_{u}\in S_{u},\,t_{w}\in S_{w}\\},\models)$, or

  * (c3)

$v$ is a decomposable $\land$-node and $S_{u}=\textit{IP}(\Sigma_{u})$ and
$S_{w}=\textit{IP}(\Sigma_{w})$ but $S\neq\\{t_{u}\land t_{w}\mid t_{u}\in
S_{u},t_{w}\in S_{w}\\}$.

A contradiction guarantees that $S\neq\textit{IP}(\Sigma)$. The contradiction
(c1) is easy to check. Contradictions (c2) and (c3) on the other hand require
to show that $S_{u}=\textit{IP}(\Sigma_{u})$ and
$S_{w}=\textit{IP}(\Sigma_{w})$. When $v$ is an internal node, with children
$u$ and $w$, if there is no contradiction (c1) at $v$, we use Propositions 8
and 9 to build from $S$ two sets $S_{u}$ and $S_{w}$ that we recursively
compare to $\textit{IP}(\Sigma_{u})$ and $\textit{IP}(\Sigma_{w})$. Either the
recursion ends under $u$ or $w$ on a contradiction, in which case
$S\neq\textit{IP}(\Sigma)$, or it stops by itself (i.e., when reaching the
leaves of the circuit), which shows that $S_{u}=\textit{IP}(\Sigma_{u})$ and
$S_{w}=\textit{IP}(\Sigma_{w})$, and then we can check whether there is
contradiction (c2) (resp. (c3)) at node $v$ if it is a decision node (resp.
decomposable node). If there is none, then $S=\textit{IP}(\Sigma)$.

The procedure is given by Algorithm MissingIP. The inputs are a dec-DNNF
circuit $\Sigma$, a set $S\subseteq\textit{IP}(\Sigma)$ and a path $P$ in
$\Sigma$ (which will be useful later). A function $\lambda$ mapping the nodes
of $\Sigma$ to integers is used for memoization purposes. Initially
$\lambda(v)=-1$ for every node $v$, but $\lambda(v)$ may be assigned a non-
negative value at some point. More precisely, the first time a call
MissingIP$(\Sigma_{v},S,P)$ returns false, we learn that
$S=\textit{IP}(\Sigma_{v})$ and set $\lambda(v)$ to $|S|$. Then for each later
call MissingIP$(\Sigma_{v},S^{\prime},P^{\prime})$ with
$S^{\prime}\subseteq\textit{IP}(\Sigma_{v})$, we check whether
$S^{\prime}=\textit{IP}(\Sigma_{v})$ by verifying that
$\lambda(v)=|S^{\prime}|$.

######  Proposition 10.

Given a reduced dec-DNNF circuit $\Sigma$ and $S\subseteq\textit{IP}(\Sigma)$,
MissingIP$(\Sigma,S,\emptyset)$ runs in time $O(poly(|S|+|\Sigma|))$, and it
returns false if and only if $S=\textit{IP}(\Sigma)$.

Promises: $\Sigma$ is reduced, $S\subseteq\textit{IP}(\Sigma)$

1 Let $v$ be the root of $\Sigma$ and let $P^{\prime}\leftarrow P\cup(v)$

2 if $\lambda(v)=|S|$ then return false

3 if  _$S=\emptyset$_ then

4 if $v$ is labelled by $0$ then set $\lambda(v)$ to 0, return false

5 else return (GenerateIP($\Sigma$), $P^{\prime}$)

6 end if

7if  _$v$ is a $\land$-node with children $u$ and $w$_ then

8 Build $S_{u}$ and $S_{w}$ as in Proposition 8

9 $r\leftarrow\texttt{MissingIP}(\Sigma_{u},S_{u},P^{\prime})$

10 if $r\neq\textit{false}$ then return $r$

11 $r\leftarrow\texttt{MissingIP}(\Sigma_{w},S_{w},P^{\prime})$

12 if $r\neq\textit{false}$ then return $r$

13 $S^{*}\leftarrow\\{t_{u}\land t_{v}\mid t_{u}\in S_{u},t_{w}\in S_{w}\\}$

14 if $S\neq S^{*}$ then for any $t\in S^{*}\setminus S$ return
$(t,P^{\prime})$

15

16 else if  _$v$ is a decision node with children $u$ and $w$_ then

17 Build $S_{u}$, $S_{w}$, $S^{\prime}$ as in Proposition 9

18 $r\leftarrow\texttt{MissingIP}(\Sigma_{u},S_{u},P^{\prime})$

19 if $r\neq\textit{false}$ then return $r$

20 $r\leftarrow\texttt{MissingIP}(\Sigma_{w},S_{w},P^{\prime})$

21 if $r\neq\textit{false}$ then return $r$

22 $S^{*}\leftarrow\max(\\{t_{u}\land t_{w}\mid t_{u}\in S_{u},t_{w}\in
S_{w}\\},\models)$

23 if $S^{*}\neq S^{\prime}$ then for any $t\in S^{*}\setminus S^{\prime}$
return $(t,P^{\prime})$

24 end if

Set $\lambda(v)$ to $|S|$ and return false

Algorithm 1 MissingIP$(\Sigma,S,P)$

###  4.2 Augmenting an incomplete subset of IP$(\Sigma)$

We build upon MissingIP so that, when $S\neq\textit{IP}(\Sigma)$, we also
return a prime implicant in $\textit{IP}(\Sigma)\setminus S$. The idea is to
use the path $P$ to keep track of the ancestor nodes that were visited before
reaching a contradiction and to use $P$ to construct a prime implicant in
$\textit{IP}(\Sigma)\setminus S$. As an example, consider calling
MissingIP$(\Sigma,S_{0},\emptyset)$ with $\Sigma$ the dec-DNNF circuit of
Figure 1(a) and
$S_{0}=\\{h\,\overline{e}\,b\,\overline{p},\,h\,\overline{p}\,\overline{s},\,\overline{e}\,\overline{p}\,\overline{s}\\}$
a set of prime implicants of $\Sigma$. Figure 1(b) shows a scenario when
MissingIP$(\Sigma,S_{0},\emptyset)$ calls
MissingIP$(\Sigma_{v_{1}},S_{1},(v_{0}))$, which calls in
turnMissingIP$(\Sigma_{v_{2}},S_{2},(v_{0},v_{1}))$, which finally calls
MissingIP$(\Sigma_{v_{3}},S_{3},(v_{0},v_{1},v_{2}))$. Since $S_{3}=\emptyset$
and $\Sigma_{v_{3}}$ is reduced and different from $0$, the algorithm has
reached a contradiction (c1) at node $v_{3}$ and has not returned _false_ ,
thus indicating that $S_{0}\neq\textit{IP}(\Sigma)$. MissingIP has followed
the path $P=(v_{0},v_{1},v_{2},v_{3})$ to reach that contradiction and has
kept it in memory. This path $P$ can then be used to generate a prime
implicant in $\textit{IP}(\Sigma)\setminus S_{0}$. First MissingIP returns the
path $P$ to $v_{3}$ as well as a prime implicant of $\Sigma_{v_{3}}$, say it
is $\overline{s}$. Then we construct a prime implicant of $\Sigma_{v_{2}}$
upon $\overline{s}$, here since $v_{3}$ is the 0-child of $v_{2}$ and since
$\overline{s}$ does not entail the 1-child of $v_{2}$ we obtain
$\overline{b}\,\overline{s}\in\textit{IP}(\Sigma_{v_{2}})$. Then we construct
a prime implicant of $\Sigma_{v_{1}}$ upon $\overline{b}\,\overline{s}$, here
since since $v_{2}$ is the 0-child of $v_{1}$ and since
$\overline{b}\,\overline{s}$ does not entail the 1-child of $v_{1}$ we obtain
$\overline{e}\,\overline{b}\,\overline{s}\in\textit{IP}(\Sigma_{v_{1}})$.
Repeating the step one more time leads to
$h\,\overline{e}\,\overline{b}\,\overline{s}\in\textit{IP}(\Sigma_{v_{0}})=\textit{IP}(\Sigma)$.
The procedure is illustrated in Figure 1(c). In this example, for generating a
new prime implicant of $\Sigma$, we have created $t\in\Sigma_{v_{3}}\setminus
S_{3}$ and augmented it using Proposition 4 as we travelled backwards along
$P$. We say that we have _propagated_ $t$ along the path $P$.

Accordingly, the algorithm AnotherIP to generate a new prime implicant breaks
into two steps. First MissingIP$(\Sigma,S,P)$ searches for a contradiction. It
returns $false$ if $S=\textit{IP}(\Sigma)$ or a pair $(t,P)$ with $P$ the path
followed to reach a node $v$ where a contradiction has been found (like
$v_{3}$ in the example), and $t$ a prime of $\Sigma_{v}$ that could not be
derived from $S$. The procedure GenerateIP is used to generate $t$. GenerateIP
runs in polynomial time thanks to linear-time implicant check on dec-DNNF
circuits. Finally PropagateIP is called to propagate $t$ along the path $P$.

Promise: $\Sigma$ is satisfiable

1 Find a satisfying assignment $a$ of $\Sigma$

2 Let $t=\bigwedge_{a(x)=1}x\land\bigwedge_{a(x)=0}\overline{x}$

3 while  _there is $\ell\in t$ such that $t-\ell\models\Sigma$_ do

4 Remove $\ell$ from $t$

5 end while

Return $t$

Algorithm 2 GenerateIP$(\Sigma)$

The next proposition shows the correctness of AnotherIP:

Promise: $\Sigma$ is reduced, its root is $v_{0}$, $P$ is a path in $\Sigma$

1 if $|P|=1$ then return $t$

2 if  _$v_{i-1}$ is a $\land$-node with children  $u$ and  $w$_ then

3 if $v_{i}=u$ then $t^{\prime}\leftarrow\texttt{GenerateIP}(\Sigma_{w})$

4 if $v_{i}=w$ then $t^{\prime}\leftarrow\texttt{GenerateIP}(\Sigma_{u})$

5

6else if  _$v_{i-1}$ is a decision node for variable $x$ with 0-child $u$ and
1-child $w$_ then

7 if  _$v_{i}=u$_ then

8 if $t\models\Sigma_{w}$ then $t^{\prime}\leftarrow t_{\emptyset}$ else
$t^{\prime}\leftarrow\overline{x}$

9 else

10 if $t\models\Sigma_{u}$ then $t^{\prime}\leftarrow t_{\emptyset}$ else
$t^{\prime}\leftarrow x$

11

12 end if

$\texttt{Propagate}(\Sigma,t\land t^{\prime},(v_{0},\dots,v_{i-1}))$

Algorithm 3 Propagate$(\Sigma,t,P=(v_{0},\dots,v_{i}))$

Promise: $\Sigma$ is reduced, $S\subseteq\textit{IP}(\Sigma)$

1 $r\leftarrow\texttt{MissingIP}^{*}(\Sigma,S,\emptyset)$

2 if $r=false$ then return $false$

else if $r=(t,P)$ then return $\texttt{Propagate}(\Sigma,t,P)$

Algorithm 4 AnotherIP$(\Sigma,S)$

######  Proposition 11.

Let $\Sigma$ be a reduced dec-DNNF circuit and let
$S\subseteq\textit{IP}(\Sigma)$. AnotherIP$(\Sigma,S)$ runs in time
$O(poly(|S|+|\Sigma|))$. It returns false if $S=\textit{IP}(\Sigma)$,
otherwise it returns a prime implicant of $\Sigma$ that does not belong to in
$S$.

On this basis, the existence of a polynomial incremental time enumeration of
prime implicants for dec-DNNF circuits can be easily established:

######  Proposition 12.

Enum$\cdot\textit{IP}$ from dec-DNNF is in IncP.

##  5 Enumerating Specific Prime Implicants

For some applications, enumerating all prime implicants of $f$ makes sense,
even though there can be exponentially many. We have already mentioned the
dualization of monotone CNF formulae as an example. In this section, we
describe two problems that ask for generating only specific prime implicants,
representing respectively subset-minimal abductive explanations and sufficient
reasons.

To illustrate the two notions we use the function $f$ computed by the dec-DNNF
circuit of Figure 1(a) as a toy example. $f$ encodes a very incomplete
characterization of human-like creatures in Tolkien’s Middle Earth based on
four physical attributes: presence of beard and facial hair ($b$), small size
($s$), human-like skin ($h$), pointy ears ($p$), plus the indication of
whether the creature is enrolled in the armies of evil ($e$). We imagine that
there are only seven possible creatures: hobbits
($h\,\overline{b}\,p\,s\,\overline{e}$), elves
($h\,\overline{b}\,p\,\overline{s}\,\overline{e}$), dwarfs
($h\,b\,\overline{p}\,s\,\overline{e}$), men and women
($h\ast\overline{p}\,\overline{s}\,\ast$),111$\ast$ denotes that both choices
are possible for the variable, typically here humans may fight for evil,
humans and ents may or may not have beards, and orcs have a wide range of
size. ents ($\overline{h}\ast\overline{p}\,\overline{s}\,\overline{e}$), orcs
($\overline{h}\,\overline{b}\,p\ast e$) and trolls
($\overline{h}\,\overline{b}\,\overline{p}\,\overline{s}\,e$). The satisfying
assignments of $f$ describe these creatures. Its prime implicants are the
smallest combinations of attributes which guarantee the existence of a
creature in our Middle Earth.

###  5.1 Abductive Explanations

Abductive explanations (see e.g., Selman and Levesque (1990); Eiter and
Gottlob (1995)) can be defined as follows:

######  Definition 1 (Abductive explanation).

Given a Boolean function $f$ over variables $X$, a subset $H\subseteq X$, and
a term $m$ on $X\setminus H$, an _abductive explanation_ is a term $t$ on $H$
such that $f\land t$ is satisfiable and $f\land t\models m$.

The abduction problem asks whether an abductive explanation $t$ exists for the
input $(f,H,m)$.

######  Example 2.

Consider our toy example. We look for combinations of physical attributes that
guarantee that the creature is evil. This is an abduction problem with
$H=\\{h,b,p,s\\}$ and $m=e$. For instance the term $\overline{h}\land p$ is an
abductive explanation because there exist creatures with pointy ears and a
skin that is not human-like, and all of them are evil (in this case only the
orcs fit this description).

It is easy to see that an abductive explanation $t$ is in fact an implicant of
$\neg f\lor m$ with the conditions that $f\land t$ is satisfiable and that $t$
is restricted to variables in $H$ (the abducibles). Furthermore, since
abduction is not a truth-preserving form of inference, one is often interested
in generating subset-minimal abductive explanations only (i.e., the logically
weakest abductive explanations); they correspond to the _prime_ implicants of
$\neg f\lor m$ such that $f\land t$ is satisfiable and $t$ is restricted to
variables in $H$.

Obviously enough, the abduction problem we focus on (the existence of an
abductive explanation) is the same, would we consider subset-minimal abductive
explanations or not. Indeed, deciding whether an abductive explanation exists
is equivalent to deciding whether a subset-minimal abductive explanation
exists. Unfortunately, the condition that only variables in $H$ are allowed in
abductive explanations is already too demanding from an enumeration
perspective.

######  Proposition 13.

Unless ${\sf P}={\sf NP}$, there is no polynomial-time algorithm which, given
an OBDD circuit or a decision tree computing a function $f$ over $X$ and a set
$Y\subseteq X$, decides whether $f$ has an implicant $t$ with $var(t)\subseteq
Y$.

###  5.2 Sufficient Reasons

The notion of sufficient reason222This concept is also referred to as
“abductive explanations” Ignatiev et al. (2019, 2020); in the following, we
stick to “sufficient reason” to avoid any confusion with the (distinct)
concept of abductive explanations as discussed in the previous section.
Darwiche and Hirth (2020) (aka prime implicant explanation Shih et al.
(2018b)) is defined as follows:

######  Definition 2 (Sufficient reason).

Given a Boolean function $f$, let $a$ be any assignment to a superset of
$var(f)$. A _sufficient reason_ for $a$ is a prime implicant $t$ of $f$ (resp.
$\neg f$) such that $a$ satisfies $t$, provided that $a$ satisfies $f$ (resp.
$\neg f$). The set of all sufficient reasons for $a$ given $f$ is denoted by
$\textit{SR}(f,a)$ (resp. $\textit{SR}(\neg f,a)$) when $a$ satisfies $f$
(resp. $\neg f$).

######  Example 3.

Consider again our toy example. There is no creature which is small, has
human-like skin, pointy ears, no facial hair, and is evil. Finding the reasons
of why such a creature cannot exist, means finding sufficient reasons for the
assignment $a$ defined by $a(h)=a(p)=a(s)=a(e)=1$ and $a(b)=0$ given $\neg f$.
In this case $h\,p\,e\in SR(\neg f,a)$ explains why such a creature cannot
exist: there are no creatures that are evil and have both human-like skin and
pointy ears, but there are such creatures that are non-evil (hobbits and
elves), and there are evil creatures that have pointy ears (orcs) or human-
like skin (men). There are other sufficient reasons for $a$ given $\neg f$,
for instance $h\,s\,e\in SR(\neg f,a)$.

We define the problem Enum$\cdot\textit{SR}$ similarly to
Enum$\cdot\textit{IP}$. A couple of results about the complexity of computing
sufficient reasons have been pointed out for the past few years. Obviously
enough, when no assumption is made on the representation of $f$, computing a
single sufficient reason for an assignment $a$ is already NP-hard (for pretty
much the same reasons as for the prime implicant case, i.e., $f$ is valid iff
for any $a$, the unique sufficient reason for $a$ given $f$ is the empty
term). Furthermore, the number of sufficient reasons for an assignment $a$
given $f$ can be exponential in the number of variables even when $f$ is
represented in DT Audemard et al. (2021). Contrary to abductive explanations,
it is computationally easy to generate a single sufficient reason from
$\textit{SR}(\Sigma,a)$ when $\Sigma$ is an OBDD circuit or a decision tree
representing $f$. A greedy algorithm can be used to this end: if $a$ satisfies
$\Sigma$ (resp. $\neg\Sigma$), then start with the canonical term having $a$
as its unique satisfying assignment and remove literals from this term while
ensuring that it still is an implicant of $\Sigma$ (resp. $\neg\Sigma$), until
no more literal can be removed. In addition, when $\Sigma$ is in DT, we can
generate in polynomial time a monotone CNF formula $\Psi$ such that
$\textit{IP}(\Psi)=\textit{SR}(\Sigma,a)$ (see Darwiche and Marquis (2021) for
details), and then take advantage of a quasi-polynomial time algorithm for
enumerating the elements of $\textit{IP}(\Psi)$ Gurvich and Khachiyan (1999).
Contrastingly, deciding whether a preset number of sufficient reasons for a
given $a$ exists is intractable (NP-hard), even when the Boolean function $f$
is monotone (see Theorem 3 in Marques-Silva et al. (2021)).

In the following, we complete those results by providing evidence that
Enum$\cdot SR$ from any language among dec-DNNF, OBDD, or DT is a difficult
problem, despite the fact that those languages are quite convenient for many
reasoning tasks Darwiche and Marquis (2002); Koriche et al. (2013).

Let us first give an inductive computation of $\textit{SR}(\Sigma,a)$ similar
to that of $\textit{IP}(\Sigma)$.

######  Proposition 14.

Let $f$ and $g$ be Boolean functions with $var(f)\cap var(g)=\emptyset$ and
let $a$ be a truth assignment to a superset of $var(f)\cup var(g)$, then
$\textit{SR}(f\land g,a)=\\{t\land t^{\prime}\mid
t\in\textit{SR}(f,a),\,t^{\prime}\in\textit{SR}(g,a)\\}$.

######  Proposition 15.

Let $f$ be a Boolean function, let $a$ be a truth assignment to a superset of
$var(f)$ and let $x\in var(f)$. If $a$ satisfies the literal $\ell$ on
variable $x$ then

$\displaystyle\textit{SR}(f,a)$ $\displaystyle=\\{t\land\ell\mid
t\in\textit{SR}(f|\ell,a),\,t\not\models f|\overline{\ell}\\}$
$\displaystyle\cup\,\textit{SR}(f|\overline{x}\land f|x,a).$

By Proposition 6,
$|\textit{IP}(f)|\geq\max(|\textit{IP}(f|\overline{x})|,|\textit{IP}(f|x)|)$.
In a sense this means that using $\textit{IP}(f|\overline{x})$ and
$\textit{IP}(f|x)$ to generate $\textit{IP}(f)$ is not a waste of resources
since all these implicants are kept in some form through $\textit{IP}(f)$.
This led to our output polynomial procedure to generate $\textit{IP}(f)$ for
OBDD and more generally for dec-DNNF circuits. On the other hand, it is not
guaranteed that $\textit{SR}(f,a)$ is larger than $\textit{SR}(f|x,a)$ and
$\textit{SR}(f|\overline{x},a)$ so there is no straightforward adaptation of
this procedure from Enum$\cdot IP$ to Enum$\cdot SR$.

######  Example 4.

Let $\Sigma$ be the dec-DNNF circuit of Figure 1(a). Consider the dec-DNNF
circuit $\Sigma_{v_{1}}$ rooted at node $v_{1}$, as spotted in Figure 1(b).
The assignment $a$ to $\\{b,e,p,s\\}$ defined by $a(b)=a(e)=1$ and
$a(p)=a(s)=0$ satisfies $\Sigma_{v_{1}}$. Recall that the set
$\textit{IP}(\Sigma_{v_{1}})$ has been constructed in Example 1 and observe
that $\textit{SR}(\Sigma_{v_{1}},a)=\\{\overline{p}\,\overline{s}\\}$. Now the
0-child of $v_{1}$ is $v_{2}$ and looking at the set
$\textit{IP}(\Sigma_{v_{2}})$ constructed in Example 1, we see that
$\textit{SR}(\Sigma_{v_{2}},a)=\\{\overline{p}\,\overline{s},b\,\overline{p}\\}$.
Since $\Sigma_{v_{2}}=\Sigma_{v_{1}}|\overline{e}$, we have that
$|\textit{SR}(\Sigma_{v_{1}},a)|<\max(|\textit{SR}(\Sigma_{v_{1}}|\overline{e},a)|,|\textit{SR}(\Sigma_{v_{1}}|e,a)|)$.

Actually, we give evidence that enumerating sufficient reasons from dec-DNNF,
and even from OBDD or DT, is not in OutputP by reducing to it the problem of
enumerating the minimal transversals of a hypergraph, a well-known problem
whose membership to OutputP is a long-standing question. Formally:

######  Proposition 16.

If Enum$\cdot\textit{SR}$ from OBDD is in OutputP or Enum$\cdot\textit{SR}$
from DT is in OutputP, then enumerating the minimal transversals of a
hypergraph is in OutputP.

##  6 Conclusion

Most applications of prime implicants for Boolean function analysis use only a
fraction of the many prime implicants a Boolean function may have. Especially,
in the context of logic-based abduction, subset-minimal assumptions to be
added to the available background knowledge in order to be able to derive some
given manifestations are looked for; in the propositional case, they
correspond to specific prime implicants. Furthermore, in an eXplainable AI
perspective, specific prime implicants known as sufficient reasons are used to
explain the predictions of machine learning algorithms.

In our work, we have studied the enumeration of general and specific prime
implicants of Boolean functions represented as dec-DNNF circuits. It was known
that these circuits enable efficient reasoning on Boolean functions. Our
results show that when it comes to prime implicants enumeration, dec-DNNF
circuits have benefits as well as limitations. Our take-home message is that,
while dec-DNNF circuits enable enumerating general prime implicants in
incremental polynomial time, there are strong pieces of evidence against the
existence of any output-polynomial time procedure for enumerating specific
prime implicants from dec-DNNF circuits. More precisely, if a procedure for
enumerating subset-minimal abductive explanations were to exist, then ${\sf
P}={\sf NP}$ would follow. Similarly, if there were an output-polynomial time
algorithm for enumerating sufficient reasons from dec-DNNF circuits, then the
enumeration of the minimal transversals of a hypergraph would be in OutputP.
Though this is considered unlikely in enumeration complexity, we think that
proving a stronger statement would be a valuable contribution. We let this
task open for future research.

## Acknowledgments

Many thanks to the anonymous reviewers for their comments and insights. This
work has benefited from the supports of the PING/ACK project
(ANR-18-CE40-0011) and of the AI Chair EXPEKCTATION (ANR-19-CHIA-0005-01) of
the French National Research Agency. It was also partially supported by
TAILOR, a project funded by EU Horizon 2020 research and innovation programme
under GA No 952215.

## References

  * Audemard et al. [2021] G. Audemard, S. Bellart, Louenas Bounia, F. Koriche, J.-M. Lagniez, and P. Marquis.  On the explanatory power of decision trees.  CoRR, abs/2108.05266, 2021.
  * Bryant [1986] R. E. Bryant.  Graph-based algorithms for Boolean function manipulation.  IEEE Transactions on Computers, C-35(8):677–692, 1986.
  * Chandra and Markowsky [1978] A.K. Chandra and G. Markowsky.  On the number of prime implicants.  Discrete Mathematics, 24:7–11, 1978.
  * Darwiche and Hirth [2020] A. Darwiche and A. Hirth.  On the reasons behind decisions.  In Proc. of ECAI’20, pages 712–720, 2020.
  * Darwiche and Marquis [2002] A. Darwiche and P. Marquis.  A knowledge compilation map.  J. Artif. Intell. Res., 17:229–264, 2002.
  * Darwiche and Marquis [2021] A. Darwiche and P. Marquis.  On quantifying literals in Boolean logic and its applications to explainable ai.  J. Artif. Intell. Res., 72:285–328, 2021.
  * Darwiche [2001] A. Darwiche.  Decomposable negation normal form.  Journal of the Association for Computing Machinery, 48(4):608–647, 2001.
  * de Kleer [1986] J. de Kleer.  An assumption-based tms.  Artificial Intelligence, 28:127–167, 1986.
  * Dunham and Fridshal [1959] B. Dunham and B. Fridshal.  The problem of simplifying logical expressions.  Journal of Symbolic Logic, 1959.
  * Eiter and Gottlob [1995] Th. Eiter and G. Gottlob.  The complexity of logic-based abduction.  Journal of the ACM, 42(1):3–42, 1995.
  * Eiter et al. [2008] Th. Eiter, K. Makino, and G. Gottlob.  Computational aspects of monotone dualization: A brief survey.  Discret. Appl. Math., 156(11):2035–2049, 2008.
  * Gergov and Meinel [1994] J. Gergov and C. Meinel.  Efficient analysis and manipulation of OBDDs can be extended to FBDDs.  IEEE Transactions on Computers, 43(10):1197–1209, 1994.
  * Gurvich and Khachiyan [1999] V. Gurvich and L. Khachiyan.  On generating the irredundant conjunctive and disjunctive normal forms of monotone Boolean functions.  Discret. Appl. Math., 96-97:363–373, 1999.
  * Ignatiev et al. [2019] A. Ignatiev, N. Narodytska, and J. Marques-Silva.  Abduction-based explanations for machine learning models.  In Proc. of AAAI’19, pages 1511–1519, 2019.
  * Ignatiev et al. [2020] A. Ignatiev, N. Narodytska, N. Asher, and J. Marques-Silva.  On relating ’why?’ and ’why not?’ explanations.  CoRR, abs/2012.11067, 2020.
  * Kavvadias et al. [1993] D. J. Kavvadias, Ch. H. Papadimitriou, and M. Sideri.  On horn envelopes and hypergraph transversals.  In Proc. of ISAAC ’93, pages 399–405, 1993.
  * Koriche et al. [2013] F. Koriche, J.-M. Lagniez, P. Marquis, and S. Thomas.  Knowledge compilation for model counting: Affine decision trees.  In Proc. of IJCAI’13, pages 947–953, 2013.
  * Madre and Coudert [1991] J.-C. Madre and O. Coudert.  A logically complete reasoning maintenance system based on a logical constraint solver.  In Proc. of IJCAI’91, pages 294–299, 1991.
  * Marques-Silva et al. [2021] J. Marques-Silva, Th. Gerspacher, M. C. Cooper, A. Ignatiev, and N. Narodytska.  Explanations for monotonic classifiers.  In Proc. of ICML’21, pages 7469–7479, 2021.
  * Marquis [1993] P. Marquis.  Skeptical abduction.  Int. J. Artif. Intell. Tools, 2(4):511–540, 1993.
  * Marquis [2000] P. Marquis.  Consequence finding algorithms, volume 5 of Handbook on Defeasible Reasoning and Uncertainty Management Systems, chapter 2, pages 41–145.  Kluwer Academic Publisher, 2000.
  * Miller [2019] T. Miller.  Explanation in artificial intelligence: Insights from the social sciences.  Artificial Intelligence, 267:1–38, 2019.
  * Molnar [2019] Ch. Molnar.  Interpretable Machine Learning - A Guide for Making Black Box Models Explainable.  Leanpub, 2019.
  * Narodytska et al. [2018] N. Narodytska, S. Prasad Kasiviswanathan, L. Ryzhyk, M. Sagiv, and T. Walsh.  Verifying properties of binarized deep neural networks.  In Proc. of AAAI’18, pages 6615–6624, 2018.
  * Oztok and Darwiche [2014] U. Oztok and A. Darwiche.  On compiling CNF into Decision-DNNF.  In Proc. of CP’14, pages 42–57, 2014.
  * Quine [1952] W.V.O. Quine.  The problem of simplifying truth functions.  American Mathematical Monthly, 59:521–531, 1952.
  * Reiter and de Kleer [1987] R. Reiter and J. de Kleer.  Foundations of assumption-based truth maintenance systems: preliminary report.  In Proc. of AAAI’87, pages 183–188, 1987.
  * Selman and Levesque [1990] B. Selman and H. Levesque.  Abductive and default reasoning: a computational core.  In Proc. of AAAI’90, pages 343–348, 1990.
  * Shih et al. [2018a] A. Shih, A. Choi, and A. Darwiche.  Formal verification of Bayesian network classifiers.  In Proc. of PGM’18, pages 427–438, 2018.
  * Shih et al. [2018b] A. Shih, A. Choi, and A. Darwiche.  A symbolic approach to explaining Bayesian network classifiers.  In Proc. of IJCAI’18, pages 5103–5111, 2018.
  * Shih et al. [2019] A. Shih, A. Choi, and A. Darwiche.  Compiling Bayesian networks into decision graphs.  In Proc. of AAAI’19, pages 7966–7974, 2019.
  * Strozecki [2019] Y. Strozecki.  Enumeration complexity.  Bull. EATCS, 129, 2019.
  * Wegener [2000] Ingo Wegener.  Branching Programs and Binary Decision Diagrams.  SIAM, 2000.

## Appendix: Proofs

######  Proposition 2.

Enum$\cdot\textit{IP}$ from dec-DNNF is in EnumP.

###### Proof.

Direct from the fact that dec-DNNF is a sublanguage of _deterministic_ DNNF
(d-DNNF) and d-DNNF supports polynomial time implicant check Darwiche and
Marquis [2002]. ∎

######  Proposition 3.

Let $f$ and $g$ be Boolean functions, then $\textit{IP}(f\land
g)=\max(\\{t\land t^{\prime}\mid
t\in\textit{IP}(f),\,t^{\prime}\in\textit{IP}(g)\\},\models).$ Furthermore if
$var(f)\cap var(g)=\emptyset$, then $\textit{IP}(f\land g)=\\{t\land
t^{\prime}\mid t\in\textit{IP}(f),\,t^{\prime}\in\textit{IP}(g)\\}.$

###### Proof.

A proof of $\textit{IP}(f\land g)=\max(\\{t\land t^{\prime}\mid
t\in\textit{IP}(f),\,t^{\prime}\in\textit{IP}(g)\\},\models)$ can be found
e.g., in Marquis [1993].

In the case where $var(f)\cap var(g)=\emptyset$, the terms in $\textit{IP}(f)$
contain only variables from $var(f)$ and the terms in $\textit{IP}(g)$ contain
only variables from $var(g)$. We denote $lit(f)=\\{x,\overline{x}\mid x\in
var(f)\\}$. Let $t_{f},t^{\prime}_{f}\in\textit{IP}(f)$ and
$t_{g},t^{\prime}_{g}\in\textit{IP}(g)$ such that $t_{f}\land t_{g}\models
t^{\prime}_{f}\land t^{\prime}_{g}$. Looking at terms as sets of literals this
means that $t^{\prime}_{f}\cup t^{\prime}_{g}\subseteq t_{f}\cup t_{g}$. But
then $t^{\prime}_{f}\subseteq t_{f}$ since $(t_{f}\cup t_{g})\cap
lit(f)=t_{f}$ and $(t^{\prime}_{f}\cup t^{\prime}_{g})\cap
lit(f)=t^{\prime}_{f}$. This means that $t_{f}\models t^{\prime}_{f}$ and
therefore $t_{f}=t^{\prime}_{f}$. A similar argument gives that
$t_{g}=t^{\prime}_{g}$. This shows that when $var(f)\cap var(g)=\emptyset$,
$\textit{IP}(f\land g)=\max(\\{t\land t^{\prime}\mid
t\in\textit{IP}(f),\,t^{\prime}\in\textit{IP}(g)\\},\models)=\\{t\land
t^{\prime}\mid t\in\textit{IP}(f),\,t^{\prime}\in\textit{IP}(g)\\}$. ∎

######  Proposition 4.

Let $f$ a Boolean function, let $x$ be a variable, and let
$\ell\in\\{x,\overline{x}\\}$. Consider $t\in\textit{IP}(f|\ell)$. If
$t\models f|\overline{\ell}$ then $t\in\textit{IP}(f)$, otherwise
$t\land\ell\in\textit{IP}(f)$.

###### Proof.

Suppose $t\models f|\overline{\ell}$. Then $t$ is an implicant of $f$ since
$t\models(f|\overline{x}\land f|x)\models((\overline{x}\land
f|\overline{x})\lor(x\land f|x))\equiv f$. To prove that it is prime let
$t^{\prime}$ be a strict subterm of $t$ and assume $t^{\prime}\models f$. We
have $x\not\in var(t)$ since $x\not\in var(f|\ell)$, so
$t^{\prime}|\ell=t^{\prime}$. If $t^{\prime}\models f$ then
$t^{\prime}=t^{\prime}|\ell\models f|\ell$ and $t$ is not a prime implicant of
$f|\ell$, a contradiction.

Suppose $t\not\models f|\overline{\ell}$. Then $t\land\ell$ is an implicant of
$f$ since $t\land\ell\models(\ell\land f|\ell)\models((\overline{x}\land
f|\overline{x})\lor(x\land f|x))\equiv f$. To prove that it is prime, let
$t^{\prime}$ be a strict subterm of $t\land\ell$ and assume $t^{\prime}\models
f$. If $\ell\not\in t^{\prime}$ then $t^{\prime}=t^{\prime}|\ell\models
f|\ell$ and $t$ is not a prime implicant of $f|\ell$, a contradiction. If
however $\ell\in t^{\prime}$, then write
$t^{\prime}=t^{\prime\prime}\land\ell$ and observe that
$t^{\prime\prime}=t^{\prime}|\ell\models f|\ell$, so $t$ is not a prime
implicant of $f|\ell$, another contradiction. ∎

######  Proposition 5.

Let $f$ be a Boolean function and let $x$ be a variable.

$\displaystyle\textit{IP}(f)=$ $\displaystyle\\{t\land\overline{x}\mid
t\in\textit{IP}(f|\overline{x}),\,t\not\models f|x\\}$ $\displaystyle\cup$
$\displaystyle\\{t\land x\mid t\in\textit{IP}(f|x),\,t\not\models
f|\overline{x}\\}$ $\displaystyle\cup$
$\displaystyle\textit{IP}(f|\overline{x}\land f|x)$

###### Proof.

We derive $\\{t\land\overline{x}\mid
t\in\textit{IP}(f|\overline{x}),t\not\models f|x\\}\cup\\{t\land x\mid
t\in\textit{IP}(f|x),t\not\models f|\overline{x}\\}\subseteq\textit{IP}(f)$
from Proposition 4.

Now we show that $\textit{IP}(f|\overline{x}\land
f|x)\subseteq\textit{IP}(f)$. Let $t\in\textit{IP}(f|\overline{x}\land f|x)$,
then $t\models f|\overline{x}$ and $t\models f|x$. Since $x\not\in
var(f|\overline{x})\cup var(f|x)$ we have that $x\not\in var(t)$. First we
prove that $t$ is an implicant of $f$. If we had $t\not\models f$ then
$t|\overline{x}\not\models f|\overline{x}$ or $t|x\not\models f|x$ would hold,
but $t|\overline{x}=t|x=t$ so $t\models f$. Now to prove that it is a prime
implicant. Let $\ell\in t$ and let $t^{\prime}$ be the term $t$ deprived from
$\ell$. If $t^{\prime}\models f$ were to hold then so would
$t^{\prime}|\overline{x}\models f|\overline{x}$ and
$t^{\prime}|\overline{x}\models f|x$. But since
$t^{\prime}|\overline{x}=t^{\prime}|x=t^{\prime}$, this would mean that
$t^{\prime}\models f|\overline{x}\land f|x$ and therefore $t$ would not be a
prime implicant of $f|\overline{x}\land f|x$, a contradiction. This shows that
$\textit{IP}(f|\overline{x}\land f|x)\subseteq\textit{IP}(f)$.

We have established that

$\displaystyle\textit{IP}(f)\supseteq$ $\displaystyle\\{t\land\overline{x}\mid
t\in\textit{IP}(f|\overline{x}),\,t\not\models f|x\\}$ $\displaystyle\cup$
$\displaystyle\\{t\land x\mid t\in\textit{IP}(f|x),\,t\not\models
f|\overline{x}\\}$ $\displaystyle\cup$
$\displaystyle\textit{IP}(f|\overline{x}\land f|x)$

and now we show the reverse inclusion. Let $t\in\textit{IP}(f)$. Assume
$t=t_{0}\land\overline{x}$. $t\models f$ implies that $t|\overline{x}\models
f|\overline{x}$, or in other words, that $t_{0}\models f|\overline{x}$. If
$t_{0}$ was not a prime implicant of $f|\overline{x}$, that is, if there was
$t^{\prime}_{0}\subset t_{0}$ such that $t^{\prime}_{0}\models
f|\overline{x}$, then we would also have
$t^{\prime}_{0}\land\overline{x}\models f$ and therefore $t$ would not be a
prime implicant of $f$. So $t_{0}\in\textit{IP}(f|\overline{x})$. Now if
$t_{0}\models f|x$ then we would have $t_{0}\models f|\overline{x}\land
f|x\models f$, so $t$ would not be a prime implicant of $f$, a contradiction.
This shows that if $\overline{x}$ is in $t$, then
$t\in\\{t_{0}\land\overline{x}\mid
t_{0}\in\textit{IP}(f|\overline{x}),t_{0}\not\models f|x\\}$. A symmetrical
proof gives that if $x$ is in $t$, then $t\in\\{t_{1}\land x\mid
t_{1}\in\textit{IP}(f|x),t_{1}\not\models f|\overline{x}\\}$.

Finally if neither $x$ nor $\overline{x}$ is in $t$, then
$t=t|\overline{x}\models f|\overline{x}$ and $t=t|x\models f|x$, and therefore
$t\models f|\overline{x}\land f|x$. Now if $t$ was not a prime implicant of
$f|\overline{x}\land f|x$ then there would be some $t^{\prime}\subset t$ in
$\textit{IP}(f|\overline{x}\land f|x)$. Since $\textit{IP}(f|\overline{x}\land
f|x)\subseteq\textit{IP}(f)$, this would mean that $t$ is not a prime
implicant of $f$, a contradiction. So $t\in\textit{IP}(f|\overline{x}\land
f|x)$.

We have established that

$\displaystyle\textit{IP}(f)\subseteq$ $\displaystyle\\{t\land\overline{x}\mid
t\in\textit{IP}(f|\overline{x}),\,t\not\models f|x\\}$ $\displaystyle\cup$
$\displaystyle\\{t\land x\mid t\in\textit{IP}(f|x),\,t\not\models
f|\overline{x}\\}$ $\displaystyle\cup$
$\displaystyle\textit{IP}(f|\overline{x}\land f|x)$

thus finishing the proof. ∎

######  Proposition 6.

Let $f$ a Boolean function and let $x$ be a variable, then
$|\textit{IP}(f)|\geq\max(|\textit{IP}(f|\overline{x})|,|\textit{IP}(f|x)|)$.

###### Proof.

Let $\ell\in\\{\overline{x},x\\}$. It is shown in Darwiche and Marquis [2002]
that $\textit{IP}(f|\ell)=\max(\\{t|\ell\mid t\in\textit{IP}(f)\\},\models)$.
So $|\textit{IP}(f|\ell)|=|\max(\\{t|\ell\mid
t\in\textit{IP}(f)\\},\models)|\leq|\\{t|\ell\mid
t\in\textit{IP}(f)\\}|=|\textit{IP}(f)|$. ∎

######  Proposition 7.

Enum$\cdot\textit{IP}$ from dec-DNNF is in OutputP.

###### Proof.

Given a dec-DNNF circuit $\Sigma$, we construct $\textit{IP}(\Sigma)$ by
visiting every node $v$ of $\Sigma$ in a bottom-up order while computing
$\textit{IP}(\Sigma_{v})$. We start from the leaves. If $v$ is labelled by a
literal $\ell$ then $\textit{IP}(\Sigma_{v})=\\{\ell\\}$, if it is labelled by
$0$ then $\textit{IP}(\Sigma_{v})=\emptyset$, and if it is labelled by $1$
then $\textit{IP}(\Sigma_{v})=\\{t_{\emptyset}\\}$ where $t_{\emptyset}$ is
the term containing no literal.

Now let $v$ be an internal node of $\Sigma$ and let $u$ and $w$ be its
children. Since we visit the nodes in depth-first order,
$\textit{IP}(\Sigma_{u})$ and $\textit{IP}(\Sigma_{w})$ have already been
computed. If $v$ is a decomposable $\land$-node then using Proposition 3 we
compute $\textit{IP}(\Sigma_{v})=\\{t_{u}\land t_{w}\mid
t_{u}\in\textit{IP}(\Sigma_{u}),t_{w}\in\textit{IP}(\Sigma_{w})\\}$ in time
$O(|\textit{IP}(\Sigma_{u})|\times|\textit{IP}(\Sigma_{w})|)=O(|\textit{IP}(\Sigma)|^{2})$.
Observe that
$|\textit{IP}(\Sigma_{v})|\geq\max(|\textit{IP}(\Sigma_{u})|,|\textit{IP}(\Sigma_{w})|)$.

If $v$ is a decision node for the variable $x$ whose 0- and 1-children are $u$
and $w$, respectively, then we compute $\textit{IP}(\Sigma_{v})$ from
$\textit{IP}(\Sigma_{u})$ and $\textit{IP}(\Sigma_{w})$ using Proposition 5.
Since dec-DNNFs support linear-time implicant check,
$\\{t\land\overline{x}\mid
t\in\textit{IP}(\Sigma_{u}),t\not\models\Sigma_{w}\\}$ and $\\{t\land x\mid
t\in\textit{IP}(\Sigma_{w}),t\not\models\Sigma_{u}\\}$ are build in time
polynomial in $|\Sigma|+|\textit{IP}(\Sigma_{u})|+|\textit{IP}(\Sigma_{w})|$.
As for $\textit{IP}(\Sigma_{u}\land\Sigma_{w})$, we build it in time
polynomial in $|\textit{IP}(\Sigma_{u})|+|\textit{IP}(\Sigma_{w})|$ using
Proposition 3. Observe that, by Proposition 6, there is again
$|\textit{IP}(\Sigma_{v})|\geq\max(|\textit{IP}(\Sigma_{u})|,|\textit{IP}(\Sigma_{w})|)$.

When we reach the root node $r$ we compute
$\textit{IP}(\Sigma_{r})=\textit{IP}(\Sigma)$. Since for every node $v$ with
children $u$ and $w$ we have that
$|\textit{IP}(\Sigma_{v})|\geq\max(|\textit{IP}(\Sigma_{u})|,|\textit{IP}(\Sigma_{w})|)$,
we also have that $|\textit{IP}(\Sigma_{v})|\leq|\textit{IP}(\Sigma)|$ for
every $v$. We build $\textit{IP}(\Sigma_{v})$ only once and the time spent on
each node $v$ to build $\textit{IP}(\Sigma_{v})$ given
$\textit{IP}(\Sigma_{u})$ and $\textit{IP}(\Sigma_{w})$ is polynomial in
$|\Sigma|+|\textit{IP}(\Sigma)|$. Summing over all nodes we get that the time
needed to build $\textit{IP}(\Sigma)$ is also polynomial in
$|\Sigma|+|\textit{IP}(\Sigma)|$. ∎

######  Proposition 8.

Let $\Sigma$ be a dec-DNNF circuit and let $S\subseteq\textit{IP}(\Sigma)$. If
the root of $\Sigma$ is an $\land$-node, let $u$ and $w$ be its children and
let $S_{u}:=\\{t_{var(\Sigma_{u})}\mid t\in S\\}$ and
$S_{w}:=\\{t_{var(\Sigma_{w})}\mid t\in S\\}$. Then
$S_{u}\subseteq\textit{IP}(\Sigma_{u})$ and
$S_{w}\subseteq\textit{IP}(\Sigma_{w})$ hold, and

$\displaystyle S=\textit{IP}(\Sigma)$ $\displaystyle\text{ iff
}S_{u}=\textit{IP}(\Sigma_{u})\text{ and }S_{w}=\textit{IP}(\Sigma_{w})$
$\displaystyle\text{ and }S=\\{t_{u}\land t_{v}\mid t_{u}\in S_{u},t_{v}\in
S_{v}\\}.$

###### Proof.

If $S=\textit{IP}(\Sigma)$ then by Proposition 3 $S=\\{t_{u}\land t_{v}\mid
t_{u}\in\textit{IP}(\Sigma_{u}),t_{v}\in\textit{IP}(\Sigma_{v})\\}$ so
$\textit{IP}(\Sigma_{u})=\\{t_{var(\Sigma_{u})}\mid t\in S\\}=S_{u}$ and
$\textit{IP}(\Sigma_{v})=\\{t_{var(\Sigma_{v})}\mid t\in S\\}=S_{v}$ and thus
$S=\\{t_{u}\land t_{v}\mid t_{u}\in S_{u},t_{v}\in S_{v}\\}$.

If $S\neq\textit{IP}(\Sigma)$, let $t^{*}\in\textit{IP}(\Sigma)\setminus S$
and let $t^{*}_{u}=t^{*}_{var(\Sigma_{u})}$ and
$t^{*}_{v}=t^{*}_{var(\Sigma_{v})}$. By Proposition 3, $t^{*}_{u}$ (resp.
$t^{*}_{v}$) is in $\textit{IP}(\Sigma_{u})$ (resp.
$\textit{IP}(\Sigma_{v})$), so either $t^{*}_{u}\not\in S_{u}$ or
$t^{*}_{v}\not\in S_{v}$and we are done, or $t^{*}_{u}\in S_{u}$ and
$t^{*}_{v}\in S_{v}$ in which case $\\{t_{u}\land t_{v}\mid t_{u}\in
S_{u},t_{v}\in S_{v}\\}\neq S$ since $t^{*}_{u}\land t^{*}_{v}$ is in
$\\{t_{u}\land t_{v}\mid t_{u}\in S_{u},t_{v}\in S_{v}\\}$ but not in $S$. ∎

######  Proposition 9.

Let $\Sigma$ be a dec-DNNF circuit whose root is a decision node labelled by
$x$ and whose 0- and 1-child are $u$ and $w$. Given
$S\subseteq\textit{IP}(\Sigma)$, let $S_{u}=\\{t\mid t\land\overline{x}\in
S\\}\cup(S\cap\textit{IP}(\Sigma_{u}))$, $S_{w}=\\{t\mid t\land x\in
S\\}\cup(S\cap\textit{IP}(\Sigma_{w}))$, $S^{\prime}=\\{t\mid t\in
S,var(x)\not\in var(t)\\}$. Then $S_{u}\subseteq\textit{IP}(\Sigma_{u})$ and
$S_{w}\subseteq\textit{IP}(\Sigma_{w})$ hold, and

$\displaystyle S=\textit{IP}(\Sigma)\text{ iff }$ $\displaystyle
S_{u}=\textit{IP}(\Sigma_{u})$ and $\displaystyle
S_{w}=\textit{IP}(\Sigma_{w})$ and $\displaystyle
S^{\prime}=\max(\\{t_{u}\land t_{w}\mid t_{u}\in S_{u},\,t_{w}\in
S_{w}\\},\models).$

###### Proof.

For convenience we denote $S^{*}=\max(\\{t_{u}\land t_{w}\mid t_{u}\in
S_{u},\,t_{w}\in S_{w}\\},\models)$.

First we prove that $S_{w}\subseteq\textit{IP}(\Sigma_{w})$ (the proof that
$S_{u}\subseteq\textit{IP}(\Sigma_{u})$ is analogous). Clearly
$S\cap\textit{IP}(\Sigma_{w})\subseteq\textit{IP}(\Sigma_{w})$ so we just need
to show that $\\{t\mid t\land x\in S\\}\subseteq\textit{IP}(\Sigma_{w})$. Let
$t\land x$ be in $S$, then $t\land x\models\Sigma$. $t$ is an implicant of
$\Sigma_{w}$ since $t\equiv(t\land x)|x\models\Sigma|x\equiv\Sigma_{w}$. Now
if there exists $t^{\prime}\neq t$ such that $t\models
t^{\prime}\models\Sigma_{w}$ then $t\land x\models t^{\prime}\land
x\models\Sigma$ holds, and therefore $t\land x$ is not a prime implicant of
$\Sigma$, a contradiction. So $\\{t\mid t\land x\in
S\\}\subseteq\textit{IP}(\Sigma_{w})$.

Second we prove that $S_{w}\neq\textit{IP}(\Sigma_{w})$ implies
$S\neq\textit{IP}(\Sigma)$ (the proof is similar for
$S_{u}\neq\textit{IP}(\Sigma_{u})$). Assume there exists
$t\in\textit{IP}(\Sigma_{w})\setminus S_{w}$. If $t\models\Sigma_{u}$ then $t$
is in $\textit{IP}(\Sigma)$ by Proposition 4. But $t$ cannot be in $S$ for
otherwise it would be in $S\cap\textit{IP}(\Sigma_{w})\subseteq S_{w}$. This
shows that $S\neq\textit{IP}(\Sigma)$ in this case. If however
$t\not\models\Sigma_{u}$ then $t\land x$ is in $\textit{IP}(\Sigma)$ by
Proposition 4. But $t\land x$ cannot be in $S$ for otherwise $t$ would be in
$\\{\tau\mid\tau\land x\in S\\}\subseteq S_{w}$. So again
$S\neq\textit{IP}(\Sigma)$.

Now we prove that $(S^{\prime}\neq
S^{*})\Rightarrow(S\neq\textit{IP}(\Sigma))$. We may assume that
$S_{u}=\textit{IP}(\Sigma_{u})$ and $S_{w}=\textit{IP}(\Sigma_{w})$, otherwise
$S\neq\textit{IP}(\Sigma)$ holds regardless of $S^{\prime}=S^{*}$. Since
$\Sigma_{u}\equiv\Sigma|\overline{x}$ and $\Sigma_{w}=\Sigma|x$ we have that
$S^{*}=\max(\\{t_{u}\land t_{w}\mid
t_{u}\in\textit{IP}(\Sigma|\overline{x}),\,t_{w}\in\textit{IP}(\Sigma|x)\\},\models)=\textit{IP}(\Sigma|\overline{x}\land\Sigma|x)$
by Proposition 3. Now $S=S^{\prime}\cup\\{t\mid t\in S,\overline{x}\in
t\\}\cup\\{t\mid t\in S,x\in t\\}$ so, by Proposition 5, if
$S=\textit{IP}(\Sigma)$ then $S^{\prime}$ corresponds to the set
$\textit{IP}(\Sigma|\overline{x}\land\Sigma|x)$. So

$(S^{\prime}\neq
S^{*})\Rightarrow(S^{\prime}\neq\textit{IP}(\Sigma|\overline{x}\land\Sigma|x))\Rightarrow(S\neq\textit{IP}(\Sigma))$

Now for the other direction, assume there exists
$t\in\textit{IP}(\Sigma)\setminus S$. First suppose that $t=t^{\prime}\land
x$. On the one hand $t^{\prime}$ is in
$\textit{IP}(\Sigma|x)=\textit{IP}(\Sigma_{w})$. On the other hand
$t^{\prime}$ is clearly not in $\\{\tau\mid\tau\land x\in S\\}$, and since it
is not an implicant of $\Sigma$, it is not in $S\cap\textit{IP}(\Sigma_{w})$
either. This means that $t^{\prime}\in\textit{IP}(\Sigma_{w})\setminus S_{w}$
and therefore $S_{w}\neq\textit{IP}(\Sigma_{w})$. In the case where
$t=t^{\prime}\land\overline{x}$, a similar proof gives that
$S_{u}\neq\textit{IP}(\Sigma_{u})$. It remains to consider the situation where
neither $x$ nor $\overline{x}$ is in $t$. By Proposition 5, $t$ is contained
in $\textit{IP}(\Sigma|\overline{x}\land\Sigma|x)$. As before, we can assume
that $S_{u}=\textit{IP}(\Sigma_{u})$ and $S_{w}=\textit{IP}(\Sigma_{w})$. We
have already explained that this assumption yields
$S^{*}=\textit{IP}(\Sigma|\overline{x}\land\Sigma|x)$. Since $t$ is not in $S$
and $\overline{x}\not\in t$ and $x\not\in t$, we have that $t\not\in
S^{\prime}$. So $t\in S^{*}\setminus S^{\prime}$, and therefore $S\neq S^{*}$.
∎

Promise: $\Sigma$ is satisfiable

1 Find a satisfying assignment $a$ of $\Sigma$

2 Let $t$ be the corresponding term:
$t=\bigwedge_{a(x)=1}x\land\bigwedge_{a(x)=0}\overline{x}$

3 while  _there is $\ell\in t$ such that $t-\ell\models\Sigma$_ do

4 Remove $\ell$ from $t$

5 end while

return $t$

Algorithm 5 GenerateIP$(\Sigma)$

######  Proposition 10.

Given a reduced dec-DNNF circuit $\Sigma$ and $S\subseteq\textit{IP}(\Sigma)$,
MissingIP$(\Sigma,S,\emptyset)$ runs in time $O(poly(|S|+|\Sigma|))$, and it
returns false if and only if $S=\textit{IP}(\Sigma)$.

###### Proof.

Soundness: We prove soundness by induction on the depth of $\Sigma$ using
Propositions 8 and 9.

If $\Sigma$ has depth 1 then it is a single node $v$ labelled by 0, 1 or a
literal $\ell$. The promise states that $S\subseteq\textit{IP}(\Sigma)$. If
$v$ is labelled by 0, then $S$ must be $\emptyset$ and the algorithm returns
false at line 4. If $v$ is is labelled by 1 then either
$S=\\{t_{\emptyset}\\}=\textit{IP}(1)$ and the algoritm returns false at line
24, or $S=\emptyset$ and the algorithm returns $(1,(v))$ at line 5. Finally if
$v$ is labelled by $\ell$, either $S=\\{\ell\\}=\textit{IP}(\ell)$ and the
algorithm returns false at line 24, or $S=\emptyset$ and the algorithm returns
$(\ell,(v))$ at line 5. In all cases the algorithm returns false if and only
if $S=\textit{IP}(\Sigma)$, and it sets $\lambda(v)$ to
$|\textit{IP}(\Sigma_{v})|$ before returning false.

Now if $\Sigma$ has depth more than 1, its root node $v$ is either a
decomposable $\land$-node or a decision node. Since $\Sigma$ is reduced, it
cannot be unsatisfiable, so if $S=\emptyset$ the algorithm returns $(t,(v))$
with $t\in\textit{IP}(\Sigma)$ at line 5. From now on we suppose that
$S\neq\emptyset$. If $v$ is a decomposable $\land$-node with children $u$ and
$w$. By Proposition 8, since we are promised that
$S\subseteq\textit{IP}(\Sigma)$, we have that $\textit{IP}(\Sigma)=S$ if and
only if $\textit{IP}(\Sigma_{u})=S_{u}$ and $\textit{IP}(\Sigma_{w})=S_{w}$
and we can construct $S$ from $S_{u}$ and $S_{w}$ as shown in Proposition 8
($S_{u}$ and $S_{w}$ defined as in Proposition 8). By induction
$\textit{IP}(\Sigma_{u})\neq S_{u}$ or $\textit{IP}(\Sigma_{w})\neq S_{w}$ if
and only if the output of $\texttt{MissingIP}(\Sigma_{u},S_{u},\ast)$ or
$\texttt{MissingIP}(\Sigma_{w},S_{w},\ast)$ is distinct from false. So if
$\textit{IP}(\Sigma_{u})\neq S_{u}$ or $\textit{IP}(\Sigma_{w})\neq S_{w}$, a
return statement occurs line 9 or 12. Otherwise, it possible that
$\textit{IP}(\Sigma_{u})=S_{u}$ or $\textit{IP}(\Sigma_{w})=S_{w}$ but that
$S$ can not be constructed from $S_{u}$ and $S_{w}$, then the return statement
of line 14 is triggerd. So if $S\neq\textit{IP}(\Sigma)$, then lines 8-14
return something that is not false. And if $S=\textit{IP}(\Sigma)$, then no
return call is triggered lines 8-14 and the algorithm returns false at line 24
after setting $\lambda(v)$ to
$|S|=|\textit{IP}(\Sigma)|=|\textit{IP}(\Sigma_{v})|$.

If $v$ is a decision node for variable $x$ with 0-child $u$ and 1-child $w$.
By Proposition 9, since we are promised that $S\subseteq\textit{IP}(\Sigma)$,
we have that $\textit{IP}(\Sigma)=S$ if and only if
$\textit{IP}(\Sigma_{u})=S_{u}$ and $\textit{IP}(\Sigma_{w})=S_{w}$ and
$S^{\prime}=S^{*}$ with $S_{u}$, $S_{w}$ and $S^{\prime}$ defined as in
Proposition 9 and $S^{*}$ defined line 21. By induction
$\textit{IP}(\Sigma_{u})=S_{u}$ and $\textit{IP}(\Sigma_{w})=S_{w}$ if and
only if the output of $\texttt{MissingIP}(\Sigma_{u},S_{u},\ast)$ or
$\texttt{MissingIP}(\Sigma_{w},S_{w},\ast)$ is distinct from false. So if
$S\neq\textit{IP}(\Sigma)$, then lines 16-22 return something that is not
false. And if $S=\textit{IP}(\Sigma)$, then no return call is triggered lines
16-22 and the algorithm returns false at line 24 after setting $\lambda(v)$ to
$|S|=|\textit{IP}(\Sigma)|=|\textit{IP}(\Sigma_{v})|$.

Running time: Consider the time spent in $\texttt{MissingIP}(\Sigma,S,P)$
before a return statement or a recursive call is triggered. The procedure may
end at line 2 or 4 in $O(1)$ time. It can also end line 5, in which case it
has to compute a prime implicant of $\Sigma$ using GenerateIP, which runs in
time $O(poly(|\Sigma|))$. Now if the algorithm has not returned lines 2, 4 or
5, most of the running time is spent building sets of terms from $S$ lines 8,
13, 16 and 21. Building $S_{u}$ and $S_{w}$ line 8 only requires projecting
the terms in $S$ onto $var(\Sigma_{u})$ and $var(\Sigma_{w})$, which takes
time $O(|S|)$. Constructing the set $S^{*}$ at line 13 takes
$O(|S_{u}|\times|S_{w}|)=O(|S|^{2})$ time. At line 16, $S^{\prime}$ can
clearly be obtained in time $O(|S|)$ and $S_{u}$ and $S_{w}$ are obtained in
time $O(poly(|S|+|\Sigma|))$ thanks to polynomial-time prime implicant check
on dec-DNNF circuits. Finally the set $S^{*}$ at line 21 is constructed in
$O(|S_{u}|\times|S_{w}|)=O(|S|^{2})$ and compared to $S^{\prime}$ in time
$O(poly(|S|)$. So before a return statement or a recursive call is triggered,
the algorithm spends $O(poly(|S|+|\Sigma|)$ time. One can observe that
$|S_{u}|$, $|S_{w}|$ are fewer than $|S|$, so for every node $v$ in $\Sigma$,
a call $\texttt{MissingIP}(\Sigma_{v},S^{\prime},*)$ takes
$O(poly(|S|+|\Sigma|))$ time before triggering a return statement or a
recursive call. Thanks to memoization – implemented via $\lambda$ – the
$O(poly(|S|+|\Sigma|))$ time procedure is done only once per node. So the
total running time of the algorithm is also in $O(poly(|S|+|\Sigma|))$. ∎

######  Proposition 11.

Let $\Sigma$ be a reduced dec-DNNF circuit and let
$S\subseteq\textit{IP}(\Sigma)$. AnotherIP$(\Sigma,S)$ runs in time
$O(poly(|S|+|\Sigma|))$. It returns false if $S=\textit{IP}(\Sigma)$,
otherwise it returns a prime implicant of $\Sigma$ that does not belong to
$S$.

###### Proof.

Soundness. First AnotherIP$(\Sigma,S)$ calls MissingIP$(\Sigma,S,\emptyset)$.
Soundness of MissingIP has been established in Proposition 10 so if
$S=\textit{IP}(\Sigma)$ then MissingIP$(\Sigma,S,\emptyset)$ returns false and
so does AnotherIP$(\Sigma,S)$.

Now let us assume that MissingIP$(\Sigma,S,\emptyset)$ has not returned false
but the pair $(t,P)$ with $P=(v_{0},\dots,v_{m})$ a path from $v_{0}$ (the
root of $\Sigma$) to $v_{m}$ and $t$ a term. Use the notation
$P_{i}=(v_{0},\dots,v_{i-1})$ for all $1\leq i\leq m$. Then calling
MissingIP$(\Sigma,S,\emptyset)$ has triggered a sequence of recursive calls
MissingIP$(\Sigma_{v_{1}},S_{1},P_{1})$,
MissingIP$(\Sigma_{v_{2}},S_{2},P_{2})$,$\dots$,MissingIP$(\Sigma_{v_{m}},S_{m},P_{m})$.
A contradiction has been found during the last step:
MissingIP$(\Sigma_{v_{m}},S_{m},P_{m})$ ended line 5 for a contradiction of
type (c1), or line 20 for a contradiction of type (c2), and returned $(t,P)$
with $t$ some term that we claim is in $\textit{IP}(\Sigma_{v_{m}})\setminus
S_{m}$.

######  Claim 1.

$t\in\textit{IP}(\Sigma_{v_{m}})\setminus S_{m}$.

###### Proof.

This is clear if MissingIP$(\Sigma_{v_{m}},S_{m},P_{m})$ ends line 5. Now if
it ends line 20, then $v_{m}$ is a decision node for $x$ with 0-child $u$ and
1-child $w$. The sets $S_{u}$, $S_{w}$, $S^{\prime}$ and $S^{*}$ have been
generated and that it has been shown that $S_{u}=\textit{IP}(\Sigma_{u})$ and
$S_{w}=\textit{IP}(\Sigma_{w})$ (otherwise a return statement line 16 or 18
would have been triggered). So
$S^{*}=\textit{IP}(\Sigma_{u}\land\Sigma_{w})=\textit{IP}(\Sigma_{v_{m}}|\overline{x}\land\Sigma_{v_{m}}|x)$
by Proposition 3. We have $t\in S^{*}\setminus S^{\prime}$ so it is clear that
$x\not\in var(t)$. Furthermore $S^{\prime}$ contains all terms from $S_{m}$ in
which neither $x$ nor $\overline{x}$ appears, so $t\in S^{*}\setminus
S^{\prime}$ really means that $t\in S^{*}\setminus
S_{m}=\textit{IP}(\Sigma_{v_{m}}|\overline{x}\land\Sigma_{v_{m}}|x)\setminus
S_{m}\subseteq\textit{IP}(\Sigma_{v_{m}})\setminus S_{m}$. ∎

Now AnotherIP$(\Sigma,S)$ returns the result Propagate$(\Sigma,t,P)$. To prove
that the output is a term in $\textit{IP}(\Sigma)\setminus S$, it is
sufficient to show that, for every $1\leq i\leq m$, if
$t_{i}\in\textit{IP}(\Sigma_{v_{i}})\setminus S_{i}$ then
Propagate$(\Sigma,t_{i},P_{i})$ calls Propagate$(\Sigma,t_{i-1},P_{i-1})$ with
$t_{i-1}\in\textit{IP}(\Sigma_{v_{i-1}})\setminus S_{i-1}$. The rest is an
easy induction (with $S_{0}=S$ and $\Sigma_{v_{0}}=\Sigma$).

######  Claim 2.

Let $t_{i}\in\textit{IP}(\Sigma_{v_{i}})\setminus S_{i}$ with $i\geq 1$ then
Propagate$(\Sigma,t_{i},P_{i})$ does a recursive call
Propagate$(\Sigma,t_{i-1},P_{i-1})$ with
$t_{i-1}\in\textit{IP}(\Sigma_{v_{i-1}})\setminus S_{i-1}$.

###### Proof.

Propagate$(\Sigma,t_{i},P_{i})$ calls Propagate$(\Sigma,t_{i}\land
t^{\prime},P_{i-1})$. Let $t_{i-1}=t_{i}\land t^{\prime}$. We need to show
that it is in $\textit{IP}(\Sigma_{v_{i-1}})\setminus S_{i-1}$. First assume
that $v_{i-1}$ is a decomposable $\land$-node with children $v_{i}$ and $w$,
then $t^{\prime}$ is obtained line 4 and clearly
$t^{\prime}\in\textit{IP}(\Sigma_{w})$. By Proposition 3, $t_{i}\land
t^{\prime}\in\textit{IP}(\Sigma_{v_{i}}\land\Sigma_{w})=\textit{IP}(\Sigma_{v_{i-1}})$.
By construction $S_{i}=\\{t_{var(\Sigma_{v_{i}})}\mid t\in S_{i-1}\\}$. If
$t_{i}\land t^{\prime}$ was in $S_{i-1}$ then its restriction $t_{i}$ to
$var(\Sigma_{v_{i}})$ would be $S_{i}$, a contradiction. So $t_{i}\land
t^{\prime}\not\in S_{i-1}$.

Now suppose $v_{i-1}$ is a decision node for $x$ with 0-child $u$ and 1-child
$w$. Let $v_{i}$ be $u$ (the case $v_{i}=w$ is analogous). By construction
$S_{i}=S_{u}$. $t^{\prime}$ is obtained line 7 and, by Proposition 4,
$t_{i}\land t^{\prime}\in\textit{IP}(\Sigma_{v_{i-1}})$. To prove that
$t_{i}\land t^{\prime}\not\in S_{i-1}$, first assume that
$t_{i}\models\Sigma_{w}$. Then $t^{\prime}$ is the empty term $t_{\emptyset}$.
So $t_{i}\land t^{\prime}=t_{i}$ and $t_{i}\in\textit{IP}(\Sigma_{v_{i-1}})$.
If $t_{i}$ was in $S_{i-1}$ then we would have $t_{i}\in
S_{i-1}\cap\textit{IP}(\Sigma_{v_{i}})\subseteq S_{i}$, a contradiction. So
when $t_{i}\models\Sigma_{w}$, we have $t_{i}\land
t^{\prime}\in\textit{IP}(\Sigma_{v_{i-1}})\setminus S_{i-1}$. Now if
$t_{i}\not\models\Sigma_{w}$, then $t_{i}\land
t^{\prime}=t_{i}\land\overline{x}$ and $t_{i}\land\overline{x}$ is not in
$S_{i-1}$ for otherwise we would have
$t_{i}\in\\{\tau\mid\tau\land\overline{x}\in S_{i-1}\\}\subseteq S_{i}$. So
again we have $t_{i}\land t^{\prime}\in\textit{IP}(\Sigma_{v_{i-1}})\setminus
S_{i-1}$. ∎

Running time. It has already been proved in Proposition 10 that
Missing($\Sigma$,$S$,$\emptyset$) runs in time $O(poly(|S|+|\Sigma|)$. As for
Propagate$(\Sigma,t,P)$, $|P|$ recursive calls are made and the cost between
two consecutive recursive calls is either one call to GenerateIP line 3 or 4,
or one implicant check line 7 or 9. An implicant test on a dec-DNNF takes
linear time and GenerateIP makes at most $|var(\Sigma)|$ such tests, so it
runs in time $O(poly(|\Sigma|))$. Thus Propagate$(\Sigma,t,P)$ runs in time
$O(|P|\times poly(|\Sigma|))=O(poly(|\Sigma|))$. ∎

######  Proposition 12.

Enum$\cdot\textit{IP}$ from dec-DNNF is in IncP.

###### Proof.

Using Proposition 11, $k$ prime implicants of $\Sigma$ can be generated in
time $O(poly(k+|\Sigma|))$ by simply calling AnotherIP$(\Sigma,S)$ $k$ times,
each time adding to $S$ the new prime implicant that has been computed. This
shows that Enum$\cdot\textit{IP}$ from dec-DNNF is in IncP. ∎

######  Proposition 13.

Unless ${\sf P}={\sf NP}$, there is no polynomial-time algorithm which, given
an OBDD circuit or a decision tree computing a function $f$ over $X$ and a set
$Y\subseteq X$, decides whether $f$ has an implicant $t$ with $var(t)\subseteq
Y$.

###### Proof.

Let $\phi$ be a CNF formula with $m$ clauses $c_{1},\dots,c_{m}$. Create $m$
fresh variables $z_{1},\dots,z_{m}$. Let $B_{1},\dots,B_{m}$ be OBDD circuits
respecting the same variable ordering and computing $c_{1},\dots,c_{m}$,
respectively. These OBDD circuits can be computed in polynomial time (and can
even be chosen in DT). Define now the OBDD circuits
$B^{(i)}=(\overline{z_{i}}\land B_{i})\lor(z_{i}\land B^{(i+1)})$ for $1\leq
i\leq m$, with $B^{(m+1)}=1$. $B^{(1)}$ is an OBDD circuit on
$\\{z_{1},\dots,z_{m}\\}\cup var(\phi)$ built in polynomial time from $\phi$
and whose size is in $O(|\phi|)$.

######  Claim 3.

An implicant $t$ of $B^{(1)}$ such that $var(t)\subseteq var(\phi)$ exists if
and only if $\phi$ is satisfiable.

###### Proof.

For the first direction assume the implicant exists. $t$ is an implicant of
$B^{(1)}=(\overline{z_{1}}\land B_{1})\lor(z_{1}\land B^{(2)})$. Since
$z_{1}\not\in var(t)$, we have $t\models B_{1}\equiv c_{1}$ and $t\models
B^{(2)}$. Following the same line of reasoning with $B^{(2)}$ instead of
$B^{(1)}$ we also have that $t\models B_{2}\equiv c_{2}$ and $t\models
B^{(3)}$. And we repeat the argument until reaching, $t\models c_{1}$,
$t\models c_{2}$, $\dots$, $t\models c_{m}$, $t\models B^{(m+1)}=1$. So indeed
$t\models\phi$ and then $\phi$ is satisfiable.

For the other direction assume $\phi$ is satisfiable. Then there exists an
implicant $t$ of $\phi$ with $var(t)\subseteq var(\phi)$. Let $a$ be a truth
assignment to $var(\phi)\cup\\{z_{1},\dots,z_{m}\\}$ that satisfies $t$. If
$a(z_{i})=1$ for all $i\in\\{1,\dots,m\\}$, then $B^{(1)}|a\equiv
B^{(2)}|a\equiv\dots\equiv B^{(m+1)}|a\equiv 1$. Otherwise let $j$ be the
smallest integer such that $a(z_{j})=0$. Then $B^{(1)}|a\equiv
B^{(2)}|a\equiv\dots\equiv B^{(j)}|a\equiv B_{j}|a\equiv c_{j}|a$. Since $t$
is an implicant of $\phi$, we have that $t\models c_{j}$, so $c_{j}|a\equiv
1$. Thus every assignment $a$ that satisfies $t$ also satisfies $B^{(1)}$, in
other words $t$ is an implicant of $B^{(1)}$. ∎

So if the algorithm from the proposition statement exists, we can run it on
inputs $B^{(1)}$ and $Y=var(\phi)$ to decide in polynomial time whether $\phi$
is satisfiable.

Finally note that if one had chosen to represent $B_{1},\dots,B_{m}$ as
decision trees from DT (which is also feasible in polynomial time), then
$B^{(1)}$ would be an element of DT. So the statement also holds for DT. ∎

######  Proposition 14.

Let $f$ and $g$ be Boolean functions with $var(f)\cap var(g)=\emptyset$ and
let $a$ be a truth assignment to a superset of $var(f)\cup var(g)$, then
$\textit{SR}(f\land g,a)=\\{t\land t^{\prime}\mid
t\in\textit{SR}(f,a),\,t^{\prime}\in\textit{SR}(g,a)\\}$.

###### Proof.

Comes from Proposition 3:

$\displaystyle\textit{SR}(f\land g,a)=\\{\tau\in\textit{IP}(f\land g)\mid
a\textup{ satisfies }\tau\\}$ $\displaystyle=\\{t\land t^{\prime}\mid
t\in\textit{IP}(f),t^{\prime}\in\textit{IP}(g),a\textup{ satisfies }t\land
t^{\prime}\\}$ $\displaystyle=\\{t\land t^{\prime}\mid
t\in\textit{IP}(f),t^{\prime}\in\textit{IP}(g),a\textup{ satisfies both
}t\textup{ and }t^{\prime}\\}$ $\displaystyle=\\{t\land t^{\prime}\mid
t\in\textit{SR}(f,a),\,t^{\prime}\in\textit{SR}(g,a)\\}$

∎

######  Proposition 15.

Let $f$ be a Boolean function, let $a$ be a truth assignment to a superset of
$var(f)$ and let $x\in var(f)$. If $a$ satisfies the literal $\ell$ on
variable $x$ then

$\displaystyle\textit{SR}(f,a)$ $\displaystyle=\\{t\land\ell\mid
t\in\textit{SR}(f|\ell,a),\,t\not\models f|\overline{\ell}\\}$
$\displaystyle\cup\,\textit{SR}(f|\overline{x}\land f|x,a).$

###### Proof.

Comes from Proposition 5:

$\displaystyle\textit{SR}(f,a)=$ $\displaystyle\\{t\in\textit{IP}(f)\mid
a\textup{ satisfies }t\\}$ $\displaystyle=$
$\displaystyle\\{t\land\overline{\ell}\mid
t\in\textit{IP}(f|\overline{\ell}),\,t\not\models f|\ell,a\textup{ satisfies
}t\\}$ $\displaystyle\cup\\{t\land\ell\mid
t\in\textit{IP}(f|\ell),\,t\not\models f|\overline{\ell},a\textup{ satisfies
}t\\}$ $\displaystyle\cup\\{t\in\textit{IP}(f|\overline{x}\land
f|x)\mid,a\textup{ satisfies }t\\}$ $\displaystyle=$
$\displaystyle\\{t\land\ell\mid t\in\textit{SR}(f|\ell,a),\,t\not\models
f|\overline{\ell}\\}$ $\displaystyle\cup\textit{SR}(f|\overline{x}\land
f|x,a).$

∎

######  Proposition 16.

If Enum$\cdot\textit{SR}$ from OBDD is in OutputP or Enum$\cdot\textit{SR}$
from DT is in OutputP, then enumerating the minimal transversals of a
hypergraph is in OutputP.

###### Proof.

The proof leans on the proof of Theorem 2 in Kavvadias et al. [1993]. Let
$\mathcal{H}$ be an hypergraph. Vertices are identified by integers
$1,\dots,n$ and associated to variables $x_{1},\dots,x_{n}$. Let
$tr(\mathcal{H})$ be the set of transversals of $\mathcal{H}$ and let
$tr_{\textup{min}}(\mathcal{H})$ be the set of minimal transversals of
$\mathcal{H}$. For each $S\subseteq\\{1,\dots,n\\}$ of vertices let $a_{S}$ be
the assignment such that $a_{S}(x_{i})=0$ if and only if $i\in S$, and let
$\gamma_{S}=\bigvee_{i\in S}\overline{x_{i}}$. Observe that $a_{S}$ satisfies
$\gamma_{S^{\prime}}$ if and only if $S\cap S^{\prime}\neq\emptyset$. Let $f$
be the function whose satisfying assignments are exactly the $a_{H}$ for
$H\in\mathcal{H}$. Denote by $sat(f)$ the set of satisfying assignments of
$f$.

Now we have the following:

$\displaystyle f\models\gamma_{S}$ $\displaystyle\Leftrightarrow\forall
H\in\mathcal{H},a_{H}\textup{ satisfies }\gamma_{S}$
$\displaystyle\Leftrightarrow\forall H\in\mathcal{H},H\cap S\neq\emptyset$
$\displaystyle\Leftrightarrow S\textup{ is a transversal of }\mathcal{H}$

This means that the set of implicates of $f$ containing only negative literals
is $\\{\gamma_{T}\mid T\in tr(\mathcal{H})\\}$, and that the set of prime
implicates of $f$ containing only negative literals is $\\{\gamma_{T}\mid T\in
tr_{\textup{min}}(\mathcal{H})\\}$. Since the prime implicants of $\neg f$ are
exactly the negation of the prime implicates of $f$, we get that the set of
prime implicants of $\neg f$ containing only positive literals is
$\\{\bigwedge_{i\in T}x_{i}\mid T\in tr_{\textup{min}}(\mathcal{H})\\}$.
Observe that $a_{\emptyset}$ is the assignment that set all $x_{i}$ to 1 and
that

$\textit{SR}(\neg f,a_{\emptyset})=\left\\{\bigwedge\nolimits_{i\in
T}x_{i}\mid T\in tr_{\textup{min}}(\mathcal{H})\right\\}.$

From $\mathcal{H}$ we construct $sat(f)$ in polynomial time. Then from
$sat(f)$ we construct in polynomial time an OBDD circuit $B$ equivalent to
$f$. Then we obtain an OBDD $B^{\prime}$ equivalent to $\neg f$ by switching
the 0-sink and the 1-sink of $B$. Given the bijection between
$\textit{SR}(B^{\prime},a_{\emptyset})$ and $tr_{\textup{min}}(\mathcal{H})$,
any algorithm for enumerating sufficient reasons from OBDD can be run with
inputs $B^{\prime}$ and $a_{\emptyset}$ to enumerate the minimal transversals
of $\mathcal{H}$. So if Enum$\cdot\textit{SR}$ from OBDD is in OutputP then
enumerating the minimal transversals of a hypergraph is in OutputP.

Finally, note that from $sat(f)$ one can construct a decision tree
representing $f$ in polynomial time (instead of an OBDD circuit), and that
negating such a decision tree boils down to turning 0-leaves into 1-leaves and
vice-versa. So the statement also holds for Enum$\cdot\textit{SR}$ from DT. ∎