ALLSAT compressed with wildcards. Part 4: An invitation for
C-programmers

arXiv:1712.00751v1 [] 3 Dec 2017

Marcel Wild

Abstract The model set of a general Boolean function in CNF is calculated in a
compressed format, using wildcards. This novel method can be explained in very
visual ways. Preliminary comparison with existing methods (BDD’s and ESOPs)
looks promising but our algorithm begs for a C encoding which would render it
comparable in more systematic ways.

1

Introduction

By definition for us an ALLSAT problem is the task to enumerate all models of a Boolean function
ϕ = ϕ(x1 , ..., xt ), often given by a CNF C1 ∧ . . . Cs with clauses Ci . The Boolean functions can
be of a specific kind (e.g. Horn formulae), or they can be general Boolean functions . The bit
’Part 4’ in the title refers to a planned series of articles dedicated to the use of wildcards in this
context. Two articles concern general Boolean functions ϕ : {0, 1}t → {0, 1}; one1 is Part 1, the
other Part 4 in front of you.
While much research has been devoted to SATISFIABILITY, the ALLSAT problem commanded
less attention. The seemingly first systematic comparison of half a dozen methods is carried out
in the article of Toda and Soh [TS]. It contains the following, unsurprising, finding. If there are
billions of models then the algorithms that put out their models one-by-one, stand no chance
against the only competitor offering compression. The latter is a method of Toda (referenced
in [TS]) that is based on Binary Decision Diagrams (BDD); see [K] for an introduction to
BDD’s. Likewise the method propagated in the present article has the potential for compression.
Whereas BDDs achieve their compression using the common don’t-care symbol * (to indicate
bits free to be 0 or 1), our method employs three further kinds of wildcards, and is entirely
different from BDDs. Referring to these wildcards we call it the men-algorithm. In a nutshell,
the men-algorithm retrieves the model set M od(ϕ) by imposing one clause after the other:
(1)

{0, 1}t ⊇ M od(C1 ) ⊇ M od(C1 ∧ C2 ) ⊇ · · · ⊇ M od(C1 ∧ . . . ∧ Cn ) = M od(ϕ)

The Section break up is as follows. In Section 2 the overall LIFO stack framework for achieving
(1) is explained. Actually the intermediate stages of shrinking {0, 1}t to M od(ϕ) don’t quite
1

The approaches taken in Part 1 and 4 are quite different, except for the common LIFO framework (discussed
in Section 2). Part 1 also contains a tentative account of the planned topics in the series, and it reviews wildcardrelated previous publications of the author. The appeal of Part 4 is its no-fuzz approach (for Theorems look in
Part 1) and its strong visual component.

1

match the n + 1 idealized stages in (1); what stages occur instead will emerge in Subsection 2.3.
Section 3 starts with a well-known Boolean tautology, which for k = 2 is x1 ∨x2 ↔ x1 ∨(x1 ∧x2 ).
Generally the k terms to the right of ↔ are mutually exclusive, i.e. their model sets are disjoint.
The problem of keeping systems ri of bitstrings disjoint upon imposing clauses on them, is the
core technical difficulty of the present article. The main tools are wildcards and the above
tautology. While in Section 3 only positive, or only negative clauses are considered (leading to
dual kinds of wildcards), both kinds occur together in Section 4. This requires a third type of
wildcard, which in turn makes the systems ri more intricate. Fortunately (Section 5) this doesn’t
get out of hand. Being able to alternately impose positive clauses like x1 ∨x2 and negative clauses
like x3 ∨ x4 ∨ x5 , doesn’t enable one to impose the mixed clause x1 ∨ x2 ∨ x3 ∨ x4 ∨ x5 . But
it certainly helps (Section 6). In Section 7 we carry out by hand the men-algorithm on some
random moderate-size Boolean functions, and observe that the compression achieved compares
favorably to BDD’s and ESOP’s. We calculate the latter two by using the commands expr2bdd
of Python and BooleanConvert of Mathematica. Of course only systematic2 experiments will
show the precise benefits and deficiencies of both methods.

2

The overall LIFO-stack framework

2.1 For the time being it suffices to think of a 012men-row as a row (=vector) r that contains
some of the symbols, 0, 1, 2, m, e, n. Any such r of length t represents a certain set of length t
bitstrings (which will be fully explained and motivated in later Sections). As a sneak preview, the
number of length 10 bitstrings represented by r = (2, m, e, m, 1, n, e, e, 1, n) is 84. We say that
r is ϕ-infeasible with respect to a Boolean function ϕ if no bitstring in r satisfies ϕ. Otherwise
r is called ϕ-feasible. If all bitstrings in r satisfy a Boolean formula ψ then we say that r fulfills
ψ.
2.2 The input of the men-algorithm is any Boolean function ϕ : {0, 1}t → {0, 1} given in CNF
format C1 ∧ C2 ∧ . . . ∧ Cs . Its output is the model set M od(ϕ), i.e. the set of bitstrings x
with ϕ(x) = 1. Here M od(ϕ) comes as a disjoint union of 012men-rows. The basic supporting
data-structure is a good old Last-In-First-Out (LIFO) stack, filled with (changing) 012men-rows.
Suppose by induction3 we obtained a LIFO stack as shown in Figure 1a (thus each ∗ is one of
the symbols 0, 1, 2, m, e, n). If there is no ambiguity we may simply speak of rows instead of
012men-rows.
2

The men-algorithm awaits implementation in either high-end Mathematica-code or in C. As to Mathematica,
this remains the only programming language I master. If any reader wants to implement the men-algorithm with
C, she is more than welcome to seize this offer on a silver tablet. The benefit (as opposed to pointless coding
efforts with Mathematica) is that the men-algorithm coded in C becomes comparable to the methods evaluated
in [TS], and likely others.
3
At the beginning the only 012men-row in the stack is (2, 2, ..., 2), thus the powerset {0, 1}t , see (1).

2

r

=

*

*

*

*

*

*

*

C5

*

*

*

*

*

*

*

C5

*

*

*

*

*

*

*

C5

*

*

*

*

*

*

*

C4

*

*

*

*

*

*

*

C4

*

*

*

*

*

*

*

C3

*

*

*

*

*

*

*

C2

*

*

*

*

*

*

*

C2

Figure 1a: LIFO stack before imposing C5

r2

=

*

*

*

*

*

*

*

C6

r4

=

*

*

*

*

*

*

*

C14

*

*

*

*

*

*

*

C5

*

*

*

*

*

*

*

C5

*

*

*

*

*

*

*

C4

*

*

*

*

*

*

*

C4

*

*

*

*

*

*

*

C3

*

*

*

*

*

*

*

C2

*

*

*

*

*

*

*

C2

Figure 1b: LIFO stack after imposing C5

The top row r fulfills C1 ∧ ... ∧ C4 , but not yet C5 , which hence is the pending clause. Similarly
the other rows have pending clauses as indicated. To ’impose’ C5 upon r means replacing r
by a few successor rows ri (called the sons of r) whose union is disjoint and contains exactly4
those bitstrings in r that satisfy C5 . Therefore each ri fulfills C5 in the sense of 2.1, but some
ri may incidently fullfil C6 as well (and perhaps even C7 ). We come back to that in a in a
moment but first handle the more serious issue that some ri ’s may be ϕ-infeasible. Fortunately
this can be detected as follows. Translate ri into a Boolean CNF σ. (As a sneak preview, if
ri = (e, 0, e, 1, e), then σ = (x1 ∨ x3 ∨ x5 ) ∧ x2 ∧ x4 .) Evidently ri is ϕ-infeasible, if and only if
ϕ ∧ σ is insatisfiable. This can be determined with any off-the-shelf SAT-solver5 .
The infeasible rows ri are cancelled. For the remaining feasible rows rj it is very easy to
determine their pending clause. This is because for any 012men-row r and any given clause C it
is straightforward (Section 6.2) to check whether or not r fulfills C. For instance, suppose r in
Figure 1a decomposes as r = r1 ] r2 ] r3 ] r4 such that r1 is infeasible, r2 has pending clause C6 ,
r3 is final, r4 has pending clause C14 . Then r1 gets kicked, r3 is output (or stored elsewhere),
and r2 , r4 (in any order) take the place or r. Nothing happens to the other rows in the LIFO
stack, see Figure 1b. This finishes the imposition of C upon r.
2.3 By induction at all stages the union U of all final rows and of all rows in the LIFO stack
is disjoint and contains M od(ϕ). (Recall Footnote 3.) Whenever the pending clause of any top
row r has been imposed on r, the new set U has shrunk. Hence the procedure ends in finite time.
More specifically, when the LIFO stack becomes empty, the set U equals the disjoint union of
all final rows, which in turn equals M od(ϕ). See Section 6 for carrying out all of this with a
concrete Boolean function ϕ.
4
This is the truly novel ingredient of the men-algorithm, as opposed to oldie-but-goldie LIFO and SAT-solvers.
Sections 3 to 6 deliver the fine details of how the sons ri get calculated. We will gradually increase the complexity
of r, and make ample use of pictures throughout. As to ’few successor rows’, in 6.2 we shall see that the number
of sons is at most the number of variables of the imposed clause.
5
All methods evaluated in [TS] use SAT-Solvers one way or another. Our use seems to be particularly economic,
but that could be author’s bias.

3

3

The Flag of Bosnia and how it befriends competing wildcards

3.1 The Flag of Bosnia6 (FoB) features a white main diagonal, the lower triangle is blue, and
the upper triangle yellow. Using 0, 1, 2 as colors the two (out of 3! imaginable) FoBes we care
about are rendered in Figure 2 and 3. Here Type 1 and 0 refer to the color of the diagonal.

1
0
0
0

2
1
0
0

2
2
1
0

2
2
2
1

Figure 2: FoB of Type 1

0
1
1
1

2
0
1
1

2
2
0
1

2
2
2
0

Figure 3: FoB of Type 0.

The FoB of Type 1 visualizes in obvious ways the tautology
(2)

(x1 ∨ x2 ∨ x3 ∨ x4 ) ↔ x1 ∨ (x1 ∧ x2 ) ∨ (x1 ∧ x2 ∧ x3 ) ∨ (x1 ∧ x2 ∧ x3 ∧ x4 )

The dimension 4 × 4 generalizes to any k × k, but only k ≥ 2 will be relevant. It is essential that
the four clauses on the right in (2) are mutually disjoint, i.e. their conjunction is insatisfiable.
Such DNFs are also known as exclusive sums of products (ESOP). Equation (2) (for any k ≥ 2)
is the key for many methods that transform (=orthogonalize) an arbitrary DNF into an ESOP;
see [B,p.327]. It will be essential for us as well, only that we are concerned with orthogonalizing
CNF’s into (fancy kinds of) ESOP’s.
As in previous publications we prefer to write 2 instead of the more common don’t-care symbol
*. Thus e.g. the 012-row (2, 0, 1, 2, 1) by definition is the set of bitstrings
{(0, 0, 1, 0, 1), (0, 0, 1, 1, 1), (1, 0, 1, 0, 1), (1, 0, 1, 1, 1)}.
In particular, in view of (2) the model set of x1 ∨ x2 ∨ x3 ∨ x4 is the disjoint union of the four
012-rows constituting the FoB in Figure 2. This is confirmed by a row-wise cardinality count:
8 + 4 + 2 + 1 = 24 − 1.
Dually the FoB of Type 0 visualizes the tautology
(3)

(x1 ∨ x2 ∨ x3 ∨ x4 ) ↔ x1 ∨ (x1 ∧ x2 ) ∨ (x1 ∧ x2 ∧ x3 ) ∨ (x1 ∧ x2 ∧ x3 ∧ x4 )

3.2 Slightly more creative than writing 2 instead of *, is it to replace the whole FoB in
Figure 2 by the single wildcard (e, e, e, e) which by definition7 is the set of all length 4 bitstrings x = (x1 , x2 , x3 , x4 ) with ’at least one 1’. In other words, only (0,0,0,0) is forbidden. The e symbols need not8 be contiguous. Thus e.g (1, e, 0, e) is the set of bitstrings
{(1, 1, 0, 0), (1, 0, 0, 1), (1, 1, 0, 1)}. If several e-wildcards occur, they need to be distinguished
6

Strictly speaking Bosnia should be Bosnia-Herzegowina, but this gets too clumsy. Other national flags, such
as the previously used Flag of Papua, have similar patterns but miss out on relevant details.
7
Surprisingly, this idea seems to be new. Information to the contrary is welcome. The definition generalizes
to tuplets (e, e..., e) of length t ≥ 2. For simplicity we sometimes strip (e, e, ..., e) to ee...e. Observe that a single
e (which we forbid) would amount to 1.
8
But for better visualization we strive to have them contiguous in more complicated examples.

4

by subscripts. For instance9 r1 in Figure 4 represents the model set of the CNF
(x1 ∨ x2 ∨ x3 ∨ x4 ) ∧ (x5 ∨ x6 ∨ x7 ∨ x8 ).

(4)

The fewest number of disjoint 012-rows required to represent r1 seems to be a hefty sixteen;
they are obtained by ’multiplying out’ two FoBes of Type 1.
3.3 So far ee...e can be viewed as the slender enemy of the sluggish FoB in Figure 2. But can
the e-formalism handle overlapping clauses? It is here where the FoB reputation gets restored,
but the FoB needs to reinvent itself as a ’Meta-FoB’. To fix ideas, let F := M od(C1 ∧ C2 ∧ C3 ) ⊆
M od(C1 ∧ C2 ) = r1 , where
C1 ∧ C2 ∧ C3 := (x1 ∨ x2 ∨ x3 ∨ x4 ) ∧ (x5 ∨ x6 ∨ x7 ∨ x8 ) ∧ (x3 ∨ x4 ∨ x5 ∨ x6 ).

(5)

We claim that F is the disjoint union of the two e-rows r2 and r3 in Figure 4a, and shall refer to
the framed part as a Meta-FoB (of dimensions 2 × 2). Specifically, the bitstrings (x3 , x4 , x5 , x6 )
satisfying the overlapping clause x3 ∨x4 ∨x5 ∨x6 are collected in (e, e, e, e) and come in two sorts.
The ones with x3 = 1 or x4 = 1 are collected in (e, e, 2, 2), and the other ones are in (0, 0, e, e).
These two quadruplets constitute, up to some adjustments, the two rows of our Meta-FoB.
The first adjustment is that the right half of (e, e, 2, 2) gets erased by the left part of the
old constraint (e2 , e2 , e2 , e2 ) in r1 . The further adjustments do not concern the shape of the
Meta-FoB per se, but rather are repercussions caused by the Meta-FoB outside of it. Namely,
(e1 , e1 , e1 , e1 ) in r1 splits into (2, 2, e, e) (left half of r2 ) and (e1 , e1 , 0, 0) (left part of r3 ). It
should be clear why (e2 , e2 , e2 , e2 ) in r2 transforms differently: It stays the same in r2 (as
noticed already), and it becomes (e, e, 2, 2) in r3 . Because of its diagonal entries (shaded) our
Meta-FoB is10 a Meta-FoB of Type 1, e.

1

r1

=

r2

=

r3

=

2

3

4

5

6

7

8

1

2

3

4

5

6

7

8

e1 e1 e1 e1 e2 e2 e2 e2

e1 e1 e1 e1 e2 e2 e2 e2

2

2

e

e e 2 e2 e2 e2

2

e1 e1

0

0

e1 e1 e1 0

e

e

2

2

Figure 4a: Meta-FoB of Type 1, e

2

2

1 e 2 e2 e2 e2
1

2

2

2

Fig. 4b: Small Meta-FoB of Type 1, e

3.4 In dual fashion we define a second wildcard (n, n, ..., n) as the set of all bitstrings (of length
equal to the number of n0 s) that have ’at least one 0’. The definition of n-row is the obvious
one. Mutatis mutandis the same arguments as above show that by using a dual Meta-FoB of
Type 0, n one can impose (n, n, ..., n) upon disjoint constraints (ni , ni , ..., ni ). See Figure 5 which
shows that the model set of
9

As for 012-rows, not all symbols 0, 1, 2, e need to occur in a 012e-row.
Generally the lengths of the diagonal entries e..e match the cardinalities of the traces of the overlapping
clause. For instance, imposing x4 ∨ x5 instead of x3 ∨ x4 ∨ x5 ∨ x6 triggers the Meta-FoB of Type 1, e in Figure 4b.
We keep the terminology Type 1, e despite the fact that all diagonal entries are 1. (Because Type 1 is reserved
for the kind in Figure 2.)
10

5

(x1 ∨ x2 ∨ x3 ∨ x4 ) ∧ (x5 ∨ x6 ∨ x7 ∨ x8 ) ∧ (x3 ∨ x4 ∨ x5 ∨ x6 )

(5’)

can be represented as disjoint union of the two n-rows r2 and r3 .
1

r1

=

r2

=

r3

=

2

3

4

5

6

7

8

n1 n1 n1 n1 n2 n2 n2 n2
2

2

n

n n 2 n2 n2 n2

n1 n1

1

1

n

n

2

2

Figure 5: Meta-FoB of Type 0, n
3.5 It is compelling to use a third11 kind of wildcard (m, m, . . . , m) := (e, e, . . . , e)∩(n, n, . . . , n).
In other words, (m, m, . . . , m) is the set of all bitstrings with ’at least one 1 and at least one 0’.
This gadget will come in handy soon. The definition of a 012men-row is the obvious one.

4

Positive and negative clauses simultaneously

New issues arise if nnnn (or dually eeee) needs to be imposed on distinct types of wildcards, say
n1 n1 n1 n1 and e1 e1 e1 e1 as occuring in the en-row r1 in Figure 6. More precisely, let n1 n1 n1 n1
model C1 = x1 ∨ x2 ∨ x3 ∨ x4 , let e1 e1 e1 e1 model C2 = x5 ∨ x6 ∨ x7 ∨ x8 , and nnnn model the
overlapping clause C3 = x3 ∨x4 ∨x5 ∨x6 . We need to sieve the model set F := M od(C1 ∧C2 ∧C3 )
from r1 := M od(C1 ∧ C2 ). To do so split r1 as r1 = r1 (+) ] r1 (−), where
r1 (+) := {x ∈ r1 : x satisfies x3 ∨ x4 } = {x ∈ r1 : x3 = 0 or x4 = 0} and
r1 (−) := {x ∈ r1 : x violates x3 ∨ x4 } = {x ∈ r1 : x3 = x4 = 1}.
Evidently r1 (+) = r2 and r1 (−) = r20 , and so r1 = r2 ] r20 . From r2 ⊆ F follows
(6)

F = r2 ] {x ∈ r20 : x satisfies C3 }

11

The choice of letters n and m stems from ’nul’ and ’mixed’ respectively. The letter e stems from ’eins’ which
is German for ’one’.

6

1

r1

=

r2

=

r2 ′

=

r2

=

r3
r4

2

3

4

5

6

7

8

n1 n1 n1 n1 e1 e1 e1 e1
2

2

n

n e 1 e1 e1 e1

n1 n1

1

1 e 1 e1 e1 e1

2

2

n

n e 1 e1 e1 e1

=

n1 n1

1

1

0

=

n1 n1

1

1

m m

0 e 1 e1
2

2

Figure 6: Meta-FoB of Type 0, n, m
For instance x = (0, 0, 1, 1, 1, 1, 1, 1) is in r20 but does not satisfy C3 . Recalling from 3.5 the
definition of mm...m a moment’s thought shows that the rightmost set in (6) is the disjoint
union of r3 and r4 in Figure 6. The framed part in Figure 6 constitutes a Meta-FoB of Type
0, n, m (which generalizes Type 0, n).
While ee...e and nn...n are duals of each other, mm...m is selfdual. Hence unsurprisingly also
ee...e can be imposed on distinct types of wildcards by virtue of a Meta-FoB of Type 1, e, m. See
Figure 7 where the imposed ee...e matches x3 ∨ x4 ∨ x5 ∨ x6 .
1

2

3

4

5

6

7

8

r1

=

n1 n1 n1 n1 e1 e1 e1 e1

r2

=

n1 n1

1

r3

=

2

2

m m e1 e1 e1 e1

r4

=

2

2

0

1 e 1 e1 e1 e1
0

e

e

2

2

Figure 7: Meta-FoB of Type 1, e, m

5

Imposing a positive or negative clause upon a 012men-row

Now that we have three wildcards the problem arises how to impose nn...n or ee...e upon a
men-row. Fortunately Meta-FoBes of Type 0, n, m respectively 1, e, m still suffice to do this. In
Figure 8 the imposition of x3 ∨ x4 ∨ x6 ∨ x7 · · · ∨ x14 (thus nn...n of length 11) upon the men-row
r1 is carried out. This boils down to the imposition of the shorter clause x6 ∨ x7 · · · ∨ x14 since

7

each x ∈ r1 has x3 = x4 = 1. We omit the details of why the Meta-FoB of Type 0, n, m,
and its repercussions outside, look the way they look12 . This, for the most part, should be
self-explanatory in view of our deliberations so far.
1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

r1

=

m1

m1

1

1

n

n

n

2

2

m1

m1

m2

e

e

e

e

m2

m2

r2

=

m1

m1

1

1

2

n

n

2

2

m1

m1

m2

e

e

e

e

m2

m2

r3

=

m1

m1

1

1

0

1

1

n

n

m1

m1

m2

e

e

e

e

m2

m2

r4

=

e1

e1

1

1

0

1

1

1

1

0

0

m2

e

e

e

e

m2

m2

r5

=

2

2

1

1

0

1

1

1

1

m

m

m2

e

e

e

e

m2

m2

r6

=

n1

n1

1

1

0

1

1

1

1

1

1

0

e

e

e

e

e2

e2

r7

=

n1

n1

1

1

0

1

1

1

1

1

1

1

0

0

e

e

n2

n2

r8

=

n1

n1

1

1

0

1

1

1

1

1

1

1

m

m

2

2

n2

n2

Figure 8: Another Meta-FoB of Type 0, n, m
Imposing the corresponding positive clause x3 ∨ x4 ∨ · · · ∨ x14 upon r1 would be trivial since
each bitstring x in r1 satisfies this clause in view of x3 = x4 = 1. Energetic readers may enjoy
imposing the shorter clause x6 ∨ · · · ∨ x14 (thus ee...e) upon r1 by virtue of a Meta-FoB of Type
1, e, m.

6

Handling general (=mixed) clauses

In contrast, we dissuade13 imposing mm...m upon r1 by virtue of some novel Meta-FoB. That’s
because what matters isn’t imposing mm...m, but rather our honed skill (Section 5) to either
impose ee...e or nn...n. This skill, as well as a clever ad hoc maneuver, will suffice to impose
any mixed clause upon any 012men-row. As opposed to Section 3 to 5 we won’t show how to
impose a mixed clause within an isolated environment, but rather within a toy example that
refreshes the LIFO framework of Section 2.
6.1 Let us thus embark on the compression of the model set of the CNF with clauses

(7) C1 = x1 ∨ x2 ∨ x3 , C2 = x4 ∨ x5 ∨ x6 ∨ x7 , C3 = x8 ∨ x9 ∨ x10 ,
C4 = x2 ∨ x3 ∨ x4 ∨ x5 ∨ x6 ∨ x7 ∨ x8 ∨ x9 , C5 = x1 ∨ x3 ∨ x4 ∨ x6 ∨ x7
12

Notice that x6 ∨ x7 · · · ∨ x14 has 9 literals whereas the induced Meta-FoB has 7 rows. Generally speaking the
shaded rectangles in any Meta-FoB arising from imposing a positive or negative clause upon r, are of dimensions
1 × t (any t ≥ 1 can occur) and 2 × 2. This implies that the number of rows in such a Meta-FoB (=number of sons
of r) is at most the number of literals in that clause. Although imposing a mixed clause is more difficult (Section
6), it is easy to see that the number of literals remains an upper bound to the number of sons.
13
More precisely, the dissuasion concerns our present focus on arbitrary CNFs. For special types of CNFs, e.g.
such that the presence of xi ∨ xj ∨ · · · ∨ xk implies the presence of xi ∨ xj ∨ · · · ∨ xk , it would be a different story.

8

It is clear that r1 in Figure 9 compresses the model set of C1 ∧ C2 ∧ C3 . Hence the pending
clause14 of r1 is C4 . In order to sieve F := M od(C1 ∧ C2 ∧ C3 ∧ C4 ) from r1 let us split r1 as
r1 = r1 (+) ] r1 (−) where

(8) r1 (+) := {x ∈ r1 : x satisfies x2 ∨ x3 ∨ x4 ∨ x5 } and
r1 (−) := {x ∈ r1 : x violates x2 ∨ x3 ∨ x4 ∨ x5 }.

Then we have r1 (+) ⊆ F, and hence (akin to (6))
(9)

F = r1 (+) ] {x ∈ r1 (−) : x satisfies x6 ∨ x7 ∨ x8 ∨ x9 }.

Trouble is, as opposed to (6), both systems of bitstrings in (9) are tougher to rewrite as disjoint
union of 012men-rows.
6.1.1 Enter the ’ad hoc maneuver’ mentioned above: Roughly speaking both bitstring systems
temporarily morph into ’overloaded’ 012men-rows. The latter get transformed, one after the
other (in 6.1.2 and 6.1.3), in disjoint collections of (ordinary) 012men-rows.
Two definitions are in order. If in a 012men-row r we bar any symbols, then the obtained
overloaded Type A row by definition consists of the bitstrings in r that feature at least on 0
on a barred location. It follows that r1 (+) equals the overloaded Type A row r2 in Figure 8.
Similarly, if in a row r we encircle, respectively decorate with stars, nonempty disjoint sets of
symbols, then the obtained overloaded Type B row by definition consists of the bitstrings in r
that feature 1’s at the encircled locations, and feature at least one 1 on the starred locations.
It follows that the rightmost set in (9) equals the overloaded Type B r3 in Figure 8. (We shall
see that merely starring, without encircling, also comes up. The definition of such an overloaded
Type C row is likewise.)
6.1.2 As to transforming r2 and r3 , we first turn to r2 , while carrying along the overloaded row
r3 . Transforming r2 simply amounts to impose the negative part x2 ∨ x3 ∨ x4 ∨ x5 of clause C4
upon r1 , and hence works with the Meta-FoB of Type 0, n, m that stretches over r4 to r6 . As
to r5 , it fulfills C5 (since each x ∈ C5 has x4 = 0), and so is final and leaves the LIFO stack (see
Section 2).
6.1.3 As to transforming r3 , the first step is to replace the encircled symbols by 1’s and to record
the ensuing repercussions. Some starred symbols may change in the process but they must keep
their star. The resulting overloaded Type C row still represents the same set of bitstrings r3 .
The second step is to impose the positive part x6 ∨ x7 ∨ x8 ∨ x9 of C4 by virtue of a Meta-FoB,
see r7 to r9 in Figure 9.
14

That some pending clauses in Figure 9 are rendered boldface merely indicates that such a clause is currently
being imposed.

9

1

2

3

4

5

6

7

r1 = n 1 n 1 n 1 e

e

e

e n 2 n2 n2 C4

r2 = n 1 n 1 n 1 e

e

e

e n2 n 2 n 2 C 4

r3 = n 1 n 1 n 1 e

e

e

*

e* n* 2 n* 2 n2 C4

r4 =

2 n 1 n1 e

e

e

e n 2 n2 n2 C5

r5 =

0

1

1

0

e

e

n

n

n

r6 =

0

1

1 m m 2

2

n

n

n C5

*

*

*

*

n2 C4

0

r3 = n 1 n 1 n 1 e

e

e

r4 =

2 n 1 n1 e

e

e

r6 =

0

8

e n

9

2

n

10

2

final

e n 2 n2 n2 C5

1

1 m m 2

2

n

n

n C5

1

*

*

*

*

n C4

r3 =

0

1

1

1 2

r4 =

2 n 1 n1 e

r6 =

0

1

1 m m 2

2

n

n

n C5

r7 =

0

1

1

1

1

e

e

n

n

n C5

r8 =

0

1

1

1

1

0

0

1

1

0

final

r9 =

0

1

1

1

1

0

0 m m 2

final

e

e

2

n

n

e n 2 n2 n2 C5

Figure 9: The men-algorithm in action. Snapshots of the LIFO stack.
6.1.4 In likewise fashion the algorithm proceeds (Figure 10). In particular r10 , r11 are overloaded
rows of Type A and B. The men-algorithm ends after the last row in the LIFO stack, here the
final row r17 , gets removed.

10

1

3

4

6

7

2

5

8

9

10

r4

=

2 n1 e

e

e n 1 e n 2 n2 n2 C5

r5

=

0

1

m

2

2

1

m

n

n

n C5

r7

=

0

1

1

1

1

e

e

n

n

n C5

2 n1 e

e

e n1 e n 2 n2 n2 C5

r10 =

r11 = 2

*

n1

e

e

e

n1 e n 2 n2 n2 C5

r5

=

0

1

m

2

2

1

m

n

n

n C5

r7

=

0

1

1

1

1

e

e

n

n

n C5

r12 =

2

0

e

e

e

2

e

n

n

n

final

r13 =

2

1

0

0

0

0

1

n

n

n

final

r14 =

2

1

m m m

0

2

n

n

n

final

r11 = 2* n1

e

e

e

n1 e n 2 n2 n2 C5

r5

=

0

1

m

2

2

1

m

n

n

n C5

r7

=

0

1

1

1

1

e

e

n

n

n C5

r11 =

1

1

1

1

1

0

2

n

n

n

r5

=

0

1

m

2

2

1

m

n

n

n C5

r7

=

0

1

1

1

1

e

e

n

n

n C5

r15 =

0

1

0

2

2

1

1

n

n

n

r16 =

0

1

1 n 1 n1 1

0 n 2 n2 n2

r7

=

0

1

1

1

1

e

e

n

n

n C5

r7

=

0

1

1

1

1

e

e

n

n

n C5

r17 =

0

1

1

1

1

m m

n

n

n

final

final
final

final

Figure 10: Further snapshots of the LIFO stack.
Altogether there are ten (disjoint) final rows r5 , r8 , r9 , r12 , r13 , r14 , r11 , r15 , r16 , r17 . Their
union is M od(ϕ), which hence is of cardinality

11

|M od(ϕ)| = 21 + 1 + 4 + 420 + 14 + 168 + 14 + 28 + 21 + 14 = 695
6.2 Here we justify the claim made in 2.3 that checking whether a 012men-row r fulfills a clause
C is straightforward. Indeed, focusing on the most elaborate case of a mixed clause C the
following holds.

(10) If C = x1 ∨ · · · ∨ xs ∨ xs+1 ∨ · · · ∨ xt and r = (a1 , .., as , as+1 , .., at , . . .) then r fulfills C iff
one of these cases occurs:
(i) For some 1 ≤ j ≤ s one has aj = 1;
(ii) {1, . . . , s} contains the position-set of a full e-wildcard or full m-wildcard;
(iii) For some s + 1 ≤ j ≤ t one has aj = 0;
(iv) {s + 1, . . . , t} contains the position-set of a full n-wildcard or full m-wildcard;

Proof of (10). It is evident that each of (i) to (iv) individually implies that all bitstrings x ∈ r
satisfy C. Conversely suppose that (i) to (iv) are false. We must pinpoint a bitstring in r that
violates C. To fix ideas, consider r of length 18 and the clause C = x1 ∨ · · · ∨ x6 ∨ x7 ∨ · · · ∨ x13 .
(For readibility the disjunctions ∨ are omitted in Figure 11.) Properties (i) to (iv) are false15
for C. Accordingly one checks that rvio ⊆ r and that each x ∈ rvio violates C.
C

= x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13

r

=

2

1

e

n1

n1

m1

m1

m1

e

n2

n2

m2

m2

m2

m2

e

n1

n1

rvio =

1

1

1

1

1

1

0

0

0

0

0

0

0

e2

e2

2

n1

n1

Figure 11: The men-row r does not fulfill clause C.

7

Comparison with BDD’s and ESOP’s

We reiterate from Section 1 that the men-algorithm has not yet been implemented. That’s why
we content ourselves to take two medium-size random CNFs and hand-calculate what the menalgorithm does with them. We compare the outcome with two competing paradigms; ESOP’s
in 7.2, and BDD’s in 7.3. But first we warm up in 7.1 by looking how ESOP and BDD handle
M od(µt ) for µt = (x1 ∨ · · · ∨ xt ) ∧ (x1 ∨ · · · ∨ xt ). Recall that the men-algorithm achieves optimal
compression here: M od(µt ) = {(m, m, . . . , m)}.
7.1 One verifies at once that the BDD on the left in Figure 12 yields the function µ5 . As
for any BDD, each nonleaf node A yields ’its own’ Boolean function. (The Boolean function
commonly coupled to the whole BDD is obtained by letting A be the root.) For instance, there
15
For instance the position-set {6, 7, 8} of m1 m1 m1 is neither contained in {1, . . . , s} nor in {s + 1, . . . , t}. That
it is contained in their union is irrelevant.

12

are two nodes labelled with x2 . The left, call it A, yields a Boolean function α(x2 , x3 , x4 , x5 )
whose model set is the disjoint union of the four 012-rows in the top square in the Table on the
right. For instance, the bitstring (0, 0, 1, 0) belongs to (0, 0, 1, 2), and indeed it triggers (in the
usual way, [K]) a path that leads from A to >. Similarly the right node labelled x2 yields some
Boolean function β(x2 , x3 , x4 , x5 ) whose model set is the disjoint union of the four 012-rows in
the bottom square in the Table on the right. It is now evident that whole Table represents the
model set of the whole BDD, thus M od(µ5 ).
Generally each BDD naturally induces an ESOP; this has been previously observed, e.g. in
[B,p.327]. The converse does not16 hold. Furthermore an easy induction of the above kind
shows that the number of nodes in a BDD is a lower bound to the number of 012-rows it brings
forth.
x1
x2

x2

x3

x3

x4

x4

x5

⊥

x5

⊤

1

2

3

4

5

0
0
0
0
1
1
1
1

1

2

2

2

0

1

2

2

0

0

1

2

0

0

0

1

0

2

2

2

1

0

2

2

1

1

0

2

1

1

1

0

Figure 12: Each BDD readily yields an ESOP
7.2 Consider this random17 CNF:

(11) ϕ1 = (x5 ∨ x7 ∨ x10 ∨ x2 ∨ x4 ) ∧ (x1 ∨ x2 ∨ x9 ∨ x7 ∨ x5 )
∧ (x2 ∨ x3 ∨ x7 ∨ x4 ∨ x9 ) ∧ (x8 ∨ x9 ∨ x10 ∨ x4 ∨ x9 )

Table 13 shows the fourteen rows that the men-algorithm produces to compresses M od(ϕ1 ).
One reads off that |M od(ϕ1 )| = 16 + 48 + · · · + 18 = 898.
16

The author didn’t manage to find out whether the particular ESOP-algorithm used in Mathematica stems
from a BDD. In any case, for all Boolean functions of type µt it yields the same 012-rows as the BDD of µt .
17
More specifically, all clauses have 3 positive and 2 negative literals, which were randomly chosen (but avoiding
xi ∨ xi ) from a set of 20 literals.

13

1

2

3

4

5

6

7

8

9

10

2

0

1

1

1

2

0

2

1

2

16

2

0

e

1

0

2

e

2

1

2

48

n

1

n

0

1

2

1

2

2

2

48

1

1

1

0

1

2

1

e

e

e

14

0

0

2

2

1

2

1

2

1

2

32

1

0

0

2

1

2

1

2

2

2

32

1

0

1

2

1

2

1

e

e

e

28

n

1

n

1

e

2

e

2

2

e

168

1

1

1

1

2

2

2

2

2

1

32

1

1

1

1

e1

2

e1

e2

e2

0

18

n1

2

n1

0

n2

2

n2

2

2

2

288

1

2

1

0

n2

2

n2

e

e

e

84

n1

0

n1

1

n2

2

n2

2

0

2

72

1

0

1

1

n2

2

n2

e

0

e

18

Table 13: Applying the men-algorithm to ϕ1 in (11).
Using the Mathematica-command BooleanConvert[***,"ESOP"] transforms (11) to an ESOP
(x4 ∧ x9 ) ∨ (x1 ∧ x4 ∧ x8 ∧ x9 ) ∨ · · ·, which amounts to a union (2, 2, 2, 0, 2, 2, 2, 2, 1, 2)∪
(1, 2, 2, 0, 2, 2, 2, 1, 0, 2) ∪ · · · of 23 disjoint 012-rows. We note that the ESOP algorithm is quite
sensitive18 to the order of clauses. Incidentally the 23 rows above stem from one of the optimal
permutations of clauses; the worst would yield 36 rows. Adding the random clause (x5 ∨ x6 ∨
x8 ∨ x3 ∨ x9 ) to ϕ1 triggers twenty six 012men-rows, but between 27 and 56 many 012-rows with
the ESOP-algorithm.
The second example in (12) has longer clauses, all of them either positive or negative (for ease
of hand-calculation). Long clauses make our wildcards more effective still.

(12) ϕ2 = (x3 ∨ x4 ∨ x6 ∨ x7 ∨ x9 ∨ x14 ∨ x15 ∨ x16 ∨ x17 ∨ x18 )
∧ (x3 ∨ x5 ∨ x8 ∨ x9 ∨ x11 ∨ x12 ∨ x13 ∨ x14 ∨ x15 ∨ x17 )
∧ (x1 ∨ x4 ∨ x5 ∨ x6 ∨ x9 ∨ x12 ∨ x14 ∨ x15 ∨ x17 ∨ x18 )
∧ (x1 ∨ x2 ∨ x3 ∨ x8 ∨ x11 ∨ x13 ∨ x14 ∨ x16 ∨ x17 ∨ x18 )
∧ (x2 ∨ x3 ∨ x7 ∨ x8 ∨ x11 ∨ x13 ∨ x14 ∨ x16 ∨ x17 ∨ x18 )

Table 14 shows the ten rows the men-algorithm uses to compress M od(ϕ2 ). In contrast the
ESOP-algorithm uses between 85 and 168 many 012-rows, depending on the order of the clauses.
18

And so is the men-algorithm, but stuck with hand-calculation we didn’t experiment with that.

14

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

e2

2

0

0

e2

0

e1

2

0

2

2

e2

2

0

0

e1

0

0

2

e2

0

e1

2

e1

e2

e2

0

2

e2

2

e2

0

0

e2

0

0

3

024

2

2

0

2

2

2

2

2

0

2

2

2

2

0

0

2

0

1

4

096

2

e2

e2

2

2

2

e2

e2

e1

2

e2

2

e2

0

e1

e2

0

e2

48 960

e

2

1

e

e

e

2

2

0

2

2

e

2

0

0

2

0

e

8

2

2

2

2

2

2

2

2

2

2

2

2

2

m

2

2

m

2

131 072

n2

n2

n2

2

2

2

2

n2

n1

2

n2

2

n2

1

n1

n2

1

n2

48 960

2

2

0

2

2

2

2

2

1

2

2

2

2

1

1

2

1

2

8

192

2

2

1

2

2

2

2

n

1

2

n

2

n

1

1

2

1

2

7

168

n2

n2

1

2

n1

2

2

1

1

2

1

n1

1

1

1

n2

1

n2

672

064

720

Table 14: Applying the men-algorithm to ϕ2 in (12).
7.3 As to BDD’s, the BDD coupled to ϕ1 in (11) has 27 nodes. Recall that hence the ESOP
induced by it has 19 at least 27 terms (=012-rows). Adding the clause (x5 ∨ x6 ∨ x8 ∨ x3 ∨ x9 )
to ϕ1 pushes the BDD size to 42. The BDD of ϕ2 in (12) has 102 nodes.

References
[B] E. Boros, Orthogonal forms and shellability, Section 7 in: Boolean Fuctions (ed. Y. Crama,
P.L. Hammer), Enc. Math. Appl. 142, Cambridge University Press 2011.
[K] D. Knuth, The art of computer programming, Volume 4 (Preprint), Section 7.14: Binary
decision diagrams, Addison-Wesley 2008.
[TS] Takahisa Toda and Takehide Soh. 2016. Implementing Efficient All Solutions SAT Solvers.
J. Exp. Algorithmics 21, Article 1.12 (2016), 44 pages. DOI: https://doi.org/10.1145/2975585
[W] M. Wild, ALLSAT compressed with wildcards. Part 1: Converting CNFs to orthogonal
DNFs, preliminary version is on ResearchGate.

19

As seen in 7.1 in order to find the exact number of 012-rows one needs to know the actual BDD, not just its
size. This is planned in a later version of the article, when certain problems with Python’s handling of BDD’s
are sorted out. For the same reason the author hasn’t experimented yet with different variable orders. As is well
known [K], they heavily influence the size of the BDD.

15

