ALLSAT compressed with wildcards.
Part 2: All k−models of a Binary Decision Diagram

arXiv:1703.08511v2 [] 23 Aug 2017

Marcel Wild

ABSTRACT: Given a Binary Decision Diagram of a Boolean function ϕ in n variables all N many
k-ones models of ϕ can be enumerated in time polynomial in n and N . Although this only guarantees
polynomial total time enumeration one-by-one, in practice compression (using wildcards) is often
possible.

1

Introduction

More details about the mini-series, whose “Part 2” is the present article, can be found in [W,
Sec.9.3]. Other than that [W] will not be relevant here. In the sequel we merely assume a basic
familiarity Boolean functions [CH] and with BDD’s, as e.g. provided in [K].
In Section 2 we review the standard methods for calculating the cardinality of the model set
Mod(ϕ) from a BDD of a Boolean function ϕ : {0, 1}n → {0, 1}, respectively for enumerating (=
generating) the whole of Mod(ϕ) in compressed form. Here “compressed” means using the don’tcare symbol “2” which e.g. in the 012-row (1, 1, 2, 0, 1) signifies that both bitstrings (1, 1, 0, 0, 1)
and (1, 1, 1, 0, 1) are allowed. Let Mod(ϕ, k) := {x ∈ Mod(ϕ) : |x| = k}, where |x| denotes
the number of bits xi = 1 of the bitstring x. As shown (as an Exercise) in [K] all cardinalities
|Mod(ϕ, k)| can be retrieved elegantly as the coefficients of a polynomial which can be calculated
fast recursively. A slight notational improvement of this nice but little known result is presented
in Section 3.
Section 4, the article’s main contribution, aims to not just count but enumerate Mod(ϕ, k)
in polynomial∗ total time. This is noteworthy, even if enumeration was one-by-one, because
in other contexts polynomial total time enumeration of models doesn’t automatically carry
over to the k-element models. However, our enumeration of Mod(ϕ, k) can again be carried
out in compressed fashion: Beyond the don’t-care symbol 2 we use the wildcard gt gt · · · gt
which means “exactly t many 1’s in this area”. Thus the 012g-row (g2 , 0, 1, g2 , g2 ) is the set
{(1, 0, 1, 1, 0), (1, 0, 1, 0, 1), (0, 0, 1, 1, 1)}.
The practical relevance of it all e.g. concerns optimization. To fix ideas, suppose Mod(ϕ) (provided by a BDD) is the family of all hitting sets of a set system. Often only small hitting sets
are sought. The smallest k for which Mod(ϕ, k) is non-empty can be determined fast beforehand
using the method of Section 3. Then, with the picked k, all k-models can be delivered using the
∗
More specifically in time O(p(n, N )) where p(n, N ) is a polynomial in n and the number N = M od(ϕ, k) of
k-models. Observe that p(n, N ) is independent of k.

1

main algorithm of Section 4 (specifically: the third method). The compact representation of
Mod(ϕ, k) via 012g-rows facilitates a potential further pruning (=optimization) of Mod(ϕ, k).
While real-life applications are intended for future research, the numerical experiments in Section† 5 provide evidence of our method’s potential.

Calculating |Mod(ϕ)| and Mod(ϕ) from a BDD of ϕ

2

Consider the BDD in Figure 1 which defines the Boolean function ψ : {0, 1}10 → {0, 1}. Here
the node x1 is the root and all nodes other than ⊥ and > are called branching nodes. Recall
how one decides whether or not a bitstring like
u = (u1 , u2 , u3 , u4 , u5 , u6 , u7 , u8 , u9 , u10 ) := (0, 0, 1, 1, 0, 1, 0, 1, 0, 0)
belongs to Mod(ψ). Start at the root x1 in Figure 1. Because u1 = 0, go down on the dashed
line to the 0-son x3 . From there, because of u3 = 1, branch on the solid line and visit the 1-son
x8 . Finally, in view of u8 = 1, the solid line brings us to >, which signals that u ∈ Mod(ψ). In
all of this the values ui for i 6∈ {1, 3, 8} were irrelevant.
For many purposes we need a shelling of a given BDD from below, i.e. we keep pruning, in any
order, the minimal branching nodes of the BDD until we reach the empty set. For instance,
upon relabelling the nodes in Figure 1 we get, a, b, c, d, e, f in Figure 2 as one of several shellings
from below.

Figure 1

Figure 2

x1

f
d

x4

x3

e

x7
x8

x7

⊥

c
b

a

⊤

⊥

⊤

For any Boolean function ϕ = ϕ(x1 , · · · , xn ) and any branching node α of a given BDD of ϕ,
we let var(α) be the index of the variable coupled to α. Thus if ϕ = ψ then var(e) = 3 and
†

The author awaits BDD-savvy collaboration before embarking on this systematically.

2

var(a) = var(c) = 7. For any ϕ and α we denote by ϕα the unique Boolean function defined by
the induced BDD with root α. Thus ϕα = ϕα (xj , xj+1 , · · · , xn ) where j = var(α).
2.1 As to calculating |Mod(ϕ)|, suppose we know the acception probability p that a random
bitstring u = (u1 , · · · , un ) will be accepted by the BDD of ϕ = ϕ(x1 , · · · , xn ), i.e. the probability
that u ∈ Mod(ϕ). Then obviously
(1)

|Mod(ϕ)| = p · 2n .

As is well known‡ , p is readily calculated as follows. Let β and γ be the 0-son and 1-son of some
branching node α. If p(α), p(β), p(γ) are the acception probabilities of ϕα , ϕβ , ϕγ respectively
then obviously
(2)

p(α) = 21 p(β) + 12 (γ)

Inductively applying (2) based on any shelling of the BDD yields p. Thus for ϕ = ψ and the
shelling in Figure 2 we have p(a) = p(b) = 12 , p(c) = 0+ 41 = 14 , p(d) = 12 + 18 = 58 , p(e) = 14 + 14 = 12
9
and finally p = p(f ) = 12 p(d) + 12 p(e) = 16
. Therefore (1) implies
(3)

|Mod(ψ)| =

9
16

· 210 = 576.

2.2 As to calculating the model set Mod(ϕ) itself, it is well-known [CH, p.48] and easy to see
that the paths from the root of the BDD to > yield at once the terms of an orthogonal§ DNF for
ϕ. For instance the path x1 → x3 → x8 → > in Figure 1 yields the term x1 ∧x3 ∧x8 . This in turn
matches the 012-row (0, 2, 1, 2, 2, 2, 2, 1, 2, 2) which is a handy shorthand for Mod(x1 ∧ x3 ∧ x8 ),
i.e. for the set of 27 many bitstrings y ∈ {0, 1}10 satisfying y1 = 0 and y3 = y8 = 1. One verifies
ad hoc that there are four paths from x1 to > in Figure 1. Correspondingly
(4)

Mod(ψ) = (0, 2, 0, 2, 2, 2, 0, 2, 2, 2) ] (0, 2, 1, 2, 2, 2, 2, 1, 2, 2)
] (1, 2, 2, 0, 2, 2, 2, 2, 2, 2) ] (1, 2, 2, 1, 2, 2, 1, 1, 2, 2).

Here and henceforth we denote disjoint union by ] as opposed to ∪.

Calculating |Mod(ϕ, k)| from a BDD of ϕ

3

As opposed to calculating |Mod(ϕ)| like in Section 2, it is lesser known how to get the cardinalities
Nk := |Mod(ϕ, k)|. We present the method of [K, Exercise 25]; without proof but with trimmed
notation. Namely, additionally to our definition of var(α) for branching nodes α, it will be handy
to set var(>) := n + 1. As in [K] we pack the unknown values Nk in a generating function
(5)

G(z) = G(z, ϕ) :=

n
X

Nk z k .

k=0
‡

See e.g. Algorithm C in [K, p.7]. It directly calculates |Mod(ϕ)| rather than p but works along the same
lines.
§
By definition an orthogonal DNF, also called exclusive sum of products, has the property that the model set of
any two distinct terms are disjoint [CH, chapter 7]. In our situation disjointness occurs because each y ∈ Mod(ϕ)
determines a unique path from x1 to >.

3

For all branching nodes α put Gα (z) := G(z, ϕα ), as well as G⊥ (z) := 0 and G> (z) := 1. Let
α, β, γ be such that β and γ are the 0-son and 1-son of α respectively (possibly β ∈ {⊥, >} or
γ ∈ {⊥, >}). Putting α = var(α), β = var(β), γ = var(γ) it is shown¶ in [K] that
(6)

Gα (z) = (1 + z)β−α−1 Gβ (z) + z(1 + z)γ−α−1 Gγ (z).

Using (6) let us calculate G(z) = G(z, ψ) = G(z, ψf ):
(7)

Ga (z) = (1 + z)11−7−1 G> (z) + z(1 + z)ir G⊥ (z) = (1 + z)3 · 1 + 0 = (1 + z)3
Gb (z) = (1 + z)ir G⊥ (z) + z(1 + z)11−8−1 G> (z) = z(1 + z)2
..
.
Gf (z) = (1 + z)3−1−1 Ge (z) + z(1 + z)4−1−1 Gd (z) = · · · =
1 + 8z + 30z 2 + 70z 3 + 113z 4 + 132z 5 + 113z 6 + 70z 7 + 30z 8 + 8z 9 + z 10

As it must be, the coefficients add up to 576. That they happen to be symmetric is irrelevant.

4

Enumerating Mod(ϕ, k) from a BDD of ϕ

We describe three methods to achieve the task in the title, the first in 4.1, the second in 4.2,
and the third (the article’s core) in 4.3.
4.1 The first method proceeds as follows. Enumerate Mod(ϕ) as shown in Section 2 and sieve
Mod(ϕ, k) from it. Thus if ϕ = ψ and k = 4 then from the four 012-rows that constitute
Mod(ψ) = Mod(ψf ) in (4) one reads off that
(8)

Mod(ψ, 4) = (0, g4 , 0, g4 , g4 , g4 , 0, g4 , g4 , g4 ) ] (0, g2 , 1, g2 , g2 , g2 , g2 , 1, g2 , g2 )
] (1, g3 , g3 , 0, g3 , g3 , g3 , g3 , g3 , g3 ) ] (1, 0, 0, 1, 0, 0, 1, 1, 0, 0)

Generally the gadget (gt , gt , · · · , gt ) means “exactly t digits 1 in this area”. Here t ≥ 1 and
the number of symbols gt must be strictly larger than t; thus instead of (g3 , g3 , g3 ) we stick to
(1, 1, 1), and (g4 , g4 , g4 ) is nonsense anyway. From (8) it follows that
(9)

|Mod(ψ, 4)| =

7
4



+

7
2



+

8
3



+ 1 = 113,

which matches the coefficient at z 4 in (7).
Representing Mod(ϕ, k) with the first method works well when the number of 012-rows r that
constitute Mod(ϕ) is small. However, it can be that r ∩ Mod(ϕ, k) = ∅, for instance r ∩
Mod(ψ, 8) = ∅ for r = (0, 2, 0, 2, 2, 2, 0, 2, 2, 2) in (4). If many rows r have an empty intersection
¶

If say β =⊥ (similarly for γ =⊥) then β = var(⊥) is undefined. In this case we replace the exponent β − α − 1
in (6) by the acronym ir (= irrelevant), in view of the fact that Gβ (z) = 0 anyway.

4

with Mod(φ, k) then the procedure becomes inefficient.
4.2 The second method was kindly pointed out to me by Fabio Somenzi. Let B1 be our given
BDD with model set Mod(ϕ). Construct a second BDD B2 whose models are exactly the kones bitstrings in {0, 1}n . This is straightforward (see Figure 3 for n = 7, k = 3) and costs
O(nk) = O(n2 ).
Figure 3

x1
x2
x3

x2
x3

x4

x3
x4

x5

x4
x5

x6

x5
x6

x7
⊤

⊥

Building the conjunction B3 of B1 and B2 has polynomial compexity, and evidently the model set
of B3 equals Mod(ϕ, k). This seems like a crisp polynomial total time procedure to the k-models
of ϕ. Trouble is, B3 may be much larger than B1 (never mind ’polynomial’). Furthermore, the
models of B3 necessarily get enumerated one-by-one because, as opposed to 2.2, no proper
012-row can possibly consist entirely of k-models.
4.3 Our third method runs in polynomial total time while simultaneously (as opposed to 4.2)
compressing the model set. In a nutshell the four-fold subdivision of 4.3 is as follows. In 4.3.1
we recursively compute a cardinality set of the “first kind”, i.e.
(10)

card1(α) := {i ∈ [0, n] : Mod(ϕα , i) 6= ∅}

for each node α of the BDD of ϕ. (For integers 0 ≤ u < v we put [u, v] := {u, u + 1, · · · , v].)
Observe that Mod(ϕ, k) = ∅ if and only if k 6∈ card1(α) for the root α of the BDD. In this case our
task to enumerate Mod(ϕ, k) is accomplished. If Mod(ϕ, k) 6= ∅ then the second step (in 4.3.2)
applies. It demands that we set up the schedule for a subsequent enumeration of Mod(ϕ, k). This
schedule points out, for each branching node α, the “second kind” cardinality set card2(α) of all
cardinalities i for which Mod(ϕα , i) needs to be constructed. Necessarily card2(α) ⊆ card1(α).
We illustrate in detail the instance M od(ϕ, k) = M od(ψ, 4) where, remember, ψ matches Figure
1. In 4.3.3 follows the explicit construction of Mod(ϕ, k) according to the schedule. In 4.3.4 the
complexity of it all is assessed in a Theorem.
5

4.3.1 We put j + S := {j + i : i ∈ S} for any set of integers, in particular j + ∅ = ∅. It is obvious
that card1(α) as defined in (10) can be obtained recursively. For instance, if ϕ = ψ and α = e
then a glance at Figures 1 and 2 shows that
(11)

card1(e) =

3
[

5
[

(j + card1(a)) ∪

j=0

(j + card1(b))

j=1

Shelling the BDD of ϕ from below and using type (11) recursion thus delivers all sets card1(α).
Spelling it out for ϕ = ψ we get:
(12)

card1(a) = [0, 3],

card1(b) = [1, 3] (by inspection)

card1(c) = 1 + card1(b) = [2, 4]
card1(d) = [0, 6] ∪ (1 + [2, 4]) ∪ (2 + [2, 4]) ∪ (3 + [2, 4]) = [0, 7]
card1(e) = (0 + [0, 3]) ∪ · · · ∪ (3 + [0, 3]) ∪ (1 + [1, 3]) ∪ · · · ∪ (5 + [1, 3]) = [0, 8]
card1(f ) = (0 + [0, 8]) ∪ (1 + [0, 8]) ∪ (1 + [0, 7]) ∪ (2 + [0, 7]) ∪ (3 + [0, 7]) = [0, 10]
4.3.2 Consider first ϕ = ψ = ψf and k = 4. From Figure 1 and 2 it is clear that each
u ∈ Mod(ψe , 4) yields a concatenated model (0, 0) × u ∈ Mod(ψf , 4) = Mod(ψ, k). Similarly
u ∈ Mod(ψe , 3) triggers (0, 1) × u ∈ Mod(ψf , 4). In other words, u ∈ Mod(ψe ) induces a
cardinality 4 model of ψf iff |u| ∈ {3, 4}. Accordingly we put card2(e) = [3, 4], and by the same
token card2(d) = [1, 3]. One may think that card2(c) = [0, 2] because u ∈ Mod(ϕc ) can only
trigger v ∈ Mod(ϕd ) with |v| ∈ [1, 3] when |u| ∈ [0, 2]. Trouble is that card1(c) = [2, 4] by (12),
and so we conclude
card2(c) = [0, 2] ∩ [2, 4] = [2].
Calculating card2(b) leads to another twist because node b has two upper covers c and e. The
cardinality interval of ϕb -models that is useful (in the obvious sense) for card2(c) = [2] is [1];
and the cardinality interval useful for card2(e) = {3, 4} is [0, 3]. Consequently
(13)

card2(b) = ([1] ∪ [0, 3]) ∩ card1(b)

(12)
=

[1, 3].

In general, suppose that a BDD of ϕ is known and all numbers card1(α) have been calculated.
The cardinalities card2(α) are then obtained by shelling the BDD from above and by proceeding
as in (13). There is no harm spelling it out once more. Thus card2(α) is obtained by treating
each upper neighbour β of α as follows. Determine (in obvious ways as illustrated) the set S(β)
of cardinalities of “hypothetic” ϕα -models u for which u could be used to construct a ϕβ -model
of a sought cardinality (i.e. belonging to card2(β)). If S is the union of all S(β)’s then evidently
each k ∈ S is a “useful cardinality”, yet constructing ϕα -models u with |u| 6∈ S would be a
waste. On the other hand, there may be numbers k ∈ S such that no ϕα -model u has |u| = k.
Therefore card2(α) = S ∩ card1(α) is both: all we need and all we can get.
Figure 4 displays the schedule, i.e. all sets card2(α), for ϕ = ψ. (In view of k = 4 we have to
put card2(f ) := {4}.)

6

Figure 4

f {4}
d [1,3]
e [3,4]

c {2}

[1,3] b
[0,3] a

⊥

⊤

4.3.3 Taking again ϕ = ψ let us show how processing the schedule of ψ in Figure 4 from belowk
yields a systematic (i.e. not as in (8)) compression of Mod(ψ, 4). For instance Mod(ψb , [1, 3]) is
defined as Mod(ψb , 1) ∪ Mod(ψb , 2) ∪ Mod(ψb , 3).
Mod(ψa , [0, 3]) = (0, 0, 0, 0) ∪ (0, g1 , g1 , g1 ) ∪ (0, g2 , g2 , g2 ) ∪ (0, 1, 1, 1)
Mod(ψb , [1, 3]) = (1, 0, 0) ∪ (1, g1 , g1 ) ∪ (1, 1, 1)
Mod(ψc , 2)

= (1) × Mod(ψb , 1) = (1, 1, 0, 0)

Mod(ψd , [1, 3]) = (0, g1 , g1 , g1 , g1 , g1 , g1 ) ∪ (0, g2 , g2 , g2 , g2 , g2 , g2 )
∪
k

(0, g3 , g3 , g3 , g3 , g3 , g3 ) ∪ ((1, 0, 0) × Mod(ψc , 2))

Any shelling from below of the branch-nodes will do; we take a, b, c, d, e, f .

7

Mod(ψe , [3, 4]) = (0, 0, 0, 0) × Mod(ψa , 3) ∪ (0, g1 , g1 , g1 ) × Mod(ψa , 2)
∪

(0, g2 , g2 , g2 ) × Mod(ψa , 1) ∪ (0, 1, 1, 1) × Mod(ψa , 0)

∪

(0, g1 , g1 , g1 ) × Mod(ψa , 3) ∪ (0, g2 , g2 , g2 ) × Mod(ψa , 2)

∪

(0, 1, 1, 1) × Mod(ψa , 1)

∪

(1, 0, 0, 0, 0) × Mod(ψb , 2)

∪

(1, g1 , g1 , g1 , g1 ) × Mod(ψb , 1)

∪

(1, 0, 0, 0, 0) × Mod(ψb , 3)

∪

(1, g1 , g1 , g1 , g1 ) × Mod(ψb , 2)

∪

(1, g2 , g2 , g2 , g2 ) × Mod(ψb , 1)

Table 1 rearranges the pieces in order to have a weight-trimmed representation of Mod(ψd , [1, 3]).
Table 2 does the same for Mod(ψe , [3, 4]).
x4

x5

x6

x7

x8

x9

x10

weight

0
0
0
1

g1
g2
g3
0

g1
g2
g3
0

g1
g2
g3
1

g1
g2
g3
1

g1
g2
g3
0

g1
g2
g3
0

1
2
3
3

Table 1: Weight-trimmed representation of Mod(ψd , [1, 3])
x3

x4

x5

x6

x7

x8

x9

x10

weight

0
0
0
0
1
1
0
0
0
1
1
1

0
g1
g2
1
0
g1
g1
g2
1
0
g1
g2

0
g1
g2
1
0
g1
g1
g2
1
0
g1
g2

0
g1
g2
1
0
g1
g1
g2
1
0
g1
g2

0
0
0
0
0
g1
0
0
0
0
g1
g2

1
g2
g1
0
1
1
1
g2
g1
1
1
1

1
g2
g1
0
g1
0
1
g2
g1
1
g1
0

1
g2
g1
0
g1
0
1
g2
g1
1
g1
0

3
3
3
3
3
3
4
4
4
4
4
4

Table 2: Weight-trimmed representation of Mod(ψe , [3, 4])
Concatenating suitable 012g-valued rows with matching 012g-valued rows in Tables 1 or 2 yields
the desired compressed representation of Mod(ψ, 4):
8

x1
0

x2
1

x3
0

x4
0

x5
0

x6
0

x7
0

x8
1

x9
1

x10
1

card
1

0

1

0

g1

g1

g1

0

g2

g2

g2

3
1

0

1

0

g2

g2

g2

0

g1

g1

g1

3
2

0

1

0

1

1

1

0

0

0

0

1

0

1

1

0

0

0

0

1

g1

g1

2
1

0

1

1

g1

g1

g1

g1

1

0

0

4
1

0

0

0

g1

g1

g1

0

1

1

1

3
1

0

0

0

g2

g2

g2

0

g2

g2

g2

0

0

0

1

1

1

0

g1

g1

g1

3
1

0

0

1

0

0

0

0

1

1

1

1

0

0

1

g1

g1

g1

g1

1

g1

g1

0

0

1

g2

g2

g2

g2

1

0

0

4
2

1

1

1

0

g1

g1

g1

g1

g1

g1

6
1

1

g1

g1

0

g2

g2

g2

g2

g2

g2

1

0

0

0

g3

g3

g3

g3

g3

g3

6
3

1

0

0

1

0

0

1

1

0

0

1

 3
2

 3
1

(0, 1) × Mod(ψe , 3)





 3

3
2

2



4
1

(0, 0) × Mod(ψe , 4)

 2
1




2
1

 6
2

(1, 1, 1) × Mod(ψd , 1)
(1, g1 , g1 ) × Mod(ψd , 2)


(1, 0, 0) × Mod(ψd , 3)

Table 3: Systematic compression of Mod(ψ, 4) (as opposed to (8))
Adding up the cardinalities of the 012g-valued rows in Table 3 yields 1+
which matches (7) and (9).

3
2

 3
2

+· · ·+

6
3



+1 = 113

Here’s why it works for general Boolean functions ϕ with a known BDD. We argued already
that the sets card2(α) in the schedule are both sufficient and non-redundant. The anchor being
evident, suppose by induction that node α has β and γ as 0-son and 1-son respectively, and that
both Mod(ϕβ , card2(β)) = r10 ] r20 ] · · · and Mod(ϕβ , card2(γ)) = r1 ] r2 ] · · · are represented
as disjoint unions of 012g-rows. Concatenating suitable 012g-rows with matching rows ri0 or ri
yields rows rj such that rj ⊆ Mod(ϕα , card2(α)). These rows rj are again mutually disjoint:
For instance in Table 3 any two rows constituting {0, 1} × Mod(ψe , 3) are disjoint because
by induction the rows constituting Mod(ψe , 3) are disjoint. And each row in (say) (0, 1) ×
Mod(ψe , 3) is disjoint to each row in (0, 0) × Mod(ψe , 4) since (0, 1) ∩ (0, 0) = ∅. Furthermore,
the disjoint union of the rows rj exhausts Mod(ϕα , card2(α)) by the careful definition of card2(β)

9

and card2(γ).
4.3.4 What remains to be done is assessing the complexity of the algorithm. Note that in the
Theorem below the constant within O(...) is independent of k.

Theorem: There is an algorithm which achieves the following. For any Boolean function
ϕ : {0, 1}n → {0, 1} given by a BDD with s branching nodes, and any fixed k ∈ [n], it
calculates Mod(ϕ, k) as a disjoint union of N many 012g-rows in time O(s2 n2 log n + N sn).

Proof. Adding two integers ≤ n costs O(log n), whence calculating a set of type j + S in 4.1
costs O(n log n). As illustrated by (11) calculating card1(α) from card1(β) and card1(γ) (where
(β, γ) are the 0-son and 1-son of α) hence costs O(n2 log n). Thus getting all sets card1(α) costs
O(sn2 log n). As we shall now see, getting all sets card2(α) is more expensive. Consider a fixed
node α and a fixed upper cover β. A moment’s thought shows that calculating the set S(β) (as
defined in 4.3) costs O(n2 log n) (since each i ∈ card2(β) causes work O(n log n)). The number
of sets S(β) (for α fixed) can only be bounded by s, which brings us to O(sn2 log n). Uniting
all sets S(β) and intersecting the result with card1(α) yields card2(α) and brings the cost to
O(sn2 log n) + O(sn) = O(sn2 log n). Thus getting all sets card2(α) costs O(s2 n2 log n).
Let β, γ be the sons of the branching node α. Then the compressed representation of Mod(ϕα , card2(α))
can be calculated from the representations of Mod(ϕβ , card2(β)) and Mod(ϕγ , card2(γ)) in time
O(N n); this is evident from the comments made about ϕ = ψ. It follows that the whole
algorithm runs in total time O(s2 n2 log n) + sO(N n). 

References
[CH] Y. Crama, P.L. Hammer, Boolean Functions, Enc. of Math. Appl. 142, Cambridge
University Press 2011.
[K] D.E. Knuth, The Art of Computer Programming, Pre-Fascicle 1B, A draft of Section 7.1.4:
Binary Decision Diagrams.
[W] M. Wild, ALLSAT compressed with wildcards. Part 1: Converting CNF’s to orthogonal
DNF’s, submitted.

10

