180
H. Riener et al.
for 1 ≤ i ≤ n and 1 ≤ j ≤ k. We say that k is the size of the ESOP form and call
each conjunction x
l 1,j
1 · · · x
l n,j
n , 1 ≤ j ≤ k, that appears in the ESOP form a product
term. The Boolean expression in (8.1) is often compactly notated as a list of words
l 1,1 · · · l n,1 l 1,2 · · · l n,2
. . .
l 1,k · · · l n,k ,
(8.3)
where each word l 1,j · · · l n,j is of fixed length n.
Distance of Product Terms Suppose that
u = x
l 1,p
1 · · · x
l n,p
n
and
v = x
l 1,q
1 · · · x
l n,q
n
(8.4)
are two product terms in n Boolean variables. We define the distance d(u, v) of u
and v as the number of different l i,j for 1 ≤ i ≤ n and j ∈ {p, q}, i.e.,
d(u, v) =
n
i=1
[l i,p = l i,q ],
(8.5)
where [.] denote the Iverson brackets. We say if d(u, v) = m, then u and v have
distance m or are m-distant.
ESOPs Describing Boolean Functions An ESOP form semantically describes
a (single-output) Boolean function f : B n → B, which maps assignments of
the Boolean variables x 1 , . . . , x n ∈ B to truth values f (x 1 , . . . , x n ) ∈ B. Each
assignment to all Boolean variables x 1 , . . . , x n is called a minterm and can be
interpreted as the decimal number
n
i=1 x i 2 i−1 when read as (x n · · · x 1 ) 2 .
A completely specified Boolean function f : B n → B over n Boolean variables
can be uniquely represented as a truth table, i.e., a word b 2 n S · · · b 1 of length 2 n ,
where b j = f (j − 1) for 1 ≤ j ≤ 2 n . An incompletely specified Boolean function
g : B n → B 3 can be represented by two completely specified Boolean functions
f : B n → B and c : B n → B, where f (x) = [g(x) = 1] and c(x) = [g(x) = −].
We call c the care function of g.
Two ESOP forms are semantically equivalent if they describe the same Boolean
function. An ESOP form with size k is minimal if and only if no semantically
equivalent ESOP form with fewer product terms exists. Minimal ESOP forms are in
general not unique.
8.3 SAT-Based Exact ESOP Synthesis
8.3.1 Exact Synthesis of ESOP Forms
Objective We aim for synthesizing minimal ESOP forms in n Boolean variables
when a completely specified Boolean function or incompletely specified Boolean
H. Riener et al.
for 1 ≤ i ≤ n and 1 ≤ j ≤ k. We say that k is the size of the ESOP form and call
each conjunction x
l 1,j
1 · · · x
l n,j
n , 1 ≤ j ≤ k, that appears in the ESOP form a product
term. The Boolean expression in (8.1) is often compactly notated as a list of words
l 1,1 · · · l n,1 l 1,2 · · · l n,2
. . .
l 1,k · · · l n,k ,
(8.3)
where each word l 1,j · · · l n,j is of fixed length n.
Distance of Product Terms Suppose that
u = x
l 1,p
1 · · · x
l n,p
n
and
v = x
l 1,q
1 · · · x
l n,q
n
(8.4)
are two product terms in n Boolean variables. We define the distance d(u, v) of u
and v as the number of different l i,j for 1 ≤ i ≤ n and j ∈ {p, q}, i.e.,
d(u, v) =
n
i=1
[l i,p = l i,q ],
(8.5)
where [.] denote the Iverson brackets. We say if d(u, v) = m, then u and v have
distance m or are m-distant.
ESOPs Describing Boolean Functions An ESOP form semantically describes
a (single-output) Boolean function f : B n → B, which maps assignments of
the Boolean variables x 1 , . . . , x n ∈ B to truth values f (x 1 , . . . , x n ) ∈ B. Each
assignment to all Boolean variables x 1 , . . . , x n is called a minterm and can be
interpreted as the decimal number
n
i=1 x i 2 i−1 when read as (x n · · · x 1 ) 2 .
A completely specified Boolean function f : B n → B over n Boolean variables
can be uniquely represented as a truth table, i.e., a word b 2 n S · · · b 1 of length 2 n ,
where b j = f (j − 1) for 1 ≤ j ≤ 2 n . An incompletely specified Boolean function
g : B n → B 3 can be represented by two completely specified Boolean functions
f : B n → B and c : B n → B, where f (x) = [g(x) = 1] and c(x) = [g(x) = −].
We call c the care function of g.
Two ESOP forms are semantically equivalent if they describe the same Boolean
function. An ESOP form with size k is minimal if and only if no semantically
equivalent ESOP form with fewer product terms exists. Minimal ESOP forms are in
general not unique.
8.3 SAT-Based Exact ESOP Synthesis
8.3.1 Exact Synthesis of ESOP Forms
Objective We aim for synthesizing minimal ESOP forms in n Boolean variables
when a completely specified Boolean function or incompletely specified Boolean