8 Exact Synthesis of ESOP Forms
191
terms (k). The colors encode the decision results: green denotes satisfiable, blue
denotes unsatisfiable, and gray denotes unknown. For those k for which the conflict
limit of 10,000 was reached, we repeated synthesis with a much higher conflict limit
of 500,000 to understand what conflict limit would allow us to conclude the correct
result. The results for k = 7 and k = 8, however, remain unknown, i.e., we do not
know whether the constraints are satisfiable, because the conflict limit of 500,000
was also exceeded.
The downward search starts with 16 terms and systematically decreases the
number of terms. During the search, the conflict limit is reached with k = 13
for the first; the search procedure interprets this as potentially satisfiable, such that
the procedure proceeds until finally k = 4 is reached. For k = 4, the procedure
concludes unsatisfiability, terminates, and returns the smallest constructed ESOP
form with 9 terms determined during the search process.
The upward search procedure solves the constraint system with increasing
number of terms starting with 1. For k ≤ 4, the SAT-solver proves unsatisfiability
of the constraint system. For 5 ≤ k ≤ 8, the SAT-solver reaches the conflict limit,
which is interpreted as potentially unsatisfiable by our search procedure, such that
the search proceeds until k = 9. For k = 9 terms, the constraint system becomes for
the first time satisfiable and the corresponding ESOP form with 9 terms is returned.
Random We synthesized ESOP forms for randomly generated, incompletely
specified Boolean functions over 5, 6, 7, and 8 Boolean variables. Each bit in the
Boolean function and its care function was chosen by flipping a fair coin. In total, we
generated 100 Boolean functions for each number of Boolean variables. Table 8.2
summarizes the results for synthesizing ESOP forms. The first two columns list
the number of Boolean variables (Var.) and a fixed bound on the number of terms
(Terms). The rest of the table is organized as Table 8.1. Due to the symmetric
design of downward and upward search, they reached exactly the same minimal
ESOP forms. Overall downward search is slower due to the fact that unsatisfiability
is typically harder to prove and can only be concluded by the SAT-solver for
sufficiently small k. Consequently, the downward search procedure on average
analyzes many more cases before unsatisfiability is reached. In contrast, upward
search keeps searching until satisfiability is reached for the first time, which can
occur early in the search process.
Table 8.2 Synthesis of ESOP forms for randomly generated Boolean functions
Fixed-size
Downward search
Upward search
Var. Terms R
C k
T
R
C k
T
R
C k
T
5
16
100
0
8.58 0.11 s 100 0 3.34
1.35 s 100 0 3.34
0.12 s
6
16
99
1 11.32 0.42 s 100 0 5.62
24.70 s 100 0 5.62
15.99 s
7
32
86 14 24.91 3.71 s 100 0 17.96 276.70 s 100 0 17.96 210.02 s
8
96
79 21 54.35 19.64 s 100 0 45.41 2156.96 s 100 0 45.41 1151.75 s
191
terms (k). The colors encode the decision results: green denotes satisfiable, blue
denotes unsatisfiable, and gray denotes unknown. For those k for which the conflict
limit of 10,000 was reached, we repeated synthesis with a much higher conflict limit
of 500,000 to understand what conflict limit would allow us to conclude the correct
result. The results for k = 7 and k = 8, however, remain unknown, i.e., we do not
know whether the constraints are satisfiable, because the conflict limit of 500,000
was also exceeded.
The downward search starts with 16 terms and systematically decreases the
number of terms. During the search, the conflict limit is reached with k = 13
for the first; the search procedure interprets this as potentially satisfiable, such that
the procedure proceeds until finally k = 4 is reached. For k = 4, the procedure
concludes unsatisfiability, terminates, and returns the smallest constructed ESOP
form with 9 terms determined during the search process.
The upward search procedure solves the constraint system with increasing
number of terms starting with 1. For k ≤ 4, the SAT-solver proves unsatisfiability
of the constraint system. For 5 ≤ k ≤ 8, the SAT-solver reaches the conflict limit,
which is interpreted as potentially unsatisfiable by our search procedure, such that
the search proceeds until k = 9. For k = 9 terms, the constraint system becomes for
the first time satisfiable and the corresponding ESOP form with 9 terms is returned.
Random We synthesized ESOP forms for randomly generated, incompletely
specified Boolean functions over 5, 6, 7, and 8 Boolean variables. Each bit in the
Boolean function and its care function was chosen by flipping a fair coin. In total, we
generated 100 Boolean functions for each number of Boolean variables. Table 8.2
summarizes the results for synthesizing ESOP forms. The first two columns list
the number of Boolean variables (Var.) and a fixed bound on the number of terms
(Terms). The rest of the table is organized as Table 8.1. Due to the symmetric
design of downward and upward search, they reached exactly the same minimal
ESOP forms. Overall downward search is slower due to the fact that unsatisfiability
is typically harder to prove and can only be concluded by the SAT-solver for
sufficiently small k. Consequently, the downward search procedure on average
analyzes many more cases before unsatisfiability is reached. In contrast, upward
search keeps searching until satisfiability is reached for the first time, which can
occur early in the search process.
Table 8.2 Synthesis of ESOP forms for randomly generated Boolean functions
Fixed-size
Downward search
Upward search
Var. Terms R
C k
T
R
C k
T
R
C k
T
5
16
100
0
8.58 0.11 s 100 0 3.34
1.35 s 100 0 3.34
0.12 s
6
16
99
1 11.32 0.42 s 100 0 5.62
24.70 s 100 0 5.62
15.99 s
7
32
86 14 24.91 3.71 s 100 0 17.96 276.70 s 100 0 17.96 210.02 s
8
96
79 21 54.35 19.64 s 100 0 45.41 2156.96 s 100 0 45.41 1151.75 s