182
H. Riener et al.
8.3.2 SAT-Based Exact Synthesis Procedure
In this section, we propose a SAT-based exact synthesis approach for ESOP
forms. The approach is based on ideas from Knuth [15] (originally proposed by
Kamath et al. [14]) and our previous work on learning two-level patches to correct
combinational Boolean circuits [24]. Our approach synthesizes an ESOP form for
the Boolean function in Example 8.1 in less than a second. We formalize the search
problem as a series of Boolean constraint satisfaction problems—one for each
possible ESOP size k (starting with k = 1) and employ a decision procedure for
Boolean satisfiability to decide the satisfiability of the constraints. The constraints
are constructed in such a way that they are satisfiable if and only if an ESOP form
with k product terms exists and each satisfying assignment corresponds to an ESOP
form with k product terms. If the constraints are unsatisfiable, then no ESOP form
restricted to k product terms, that is equivalent to the provided Boolean function,
exists. By systematically solving the constraint satisfaction problem for increasing
values of the size parameter k, a minimal ESOP form is guaranteed to be found.
Formulation of the Constraint Satisfaction Problem Suppose that f : B n
3 →
B is a (single-output) Boolean function over n Boolean variables. We formulate
the problem of finding an ESOP form equivalent to f with k product terms as a
constraint satisfaction problem in propositional logic using 2nk Boolean variables,
p = p 1,1 , . . . , p k,n and q = q 1,1 , . . . , q k,n , where n is the number of Boolean
variables of f , k is the size of the ESOP form, and
p j,l = [x l in product term j ] and q j,l = [ ¯
x l in product term j ]
(8.11)
for 1 ≤ j ≤ k and 1 ≤ l ≤ n.
For each assignment x 1 · · · x n ∈ B n
3 of the Boolean function f with the
corresponding output value f (x 1 , . . . , x n ) = b, we introduce k auxiliary Boolean
variables z = z 1 , . . . , z k and add k · n + k clauses
k
j =1
n
l=1
¯
z j ∨ ITE(x i , ¯
q j,l , ¯
p j,l )
and
k
j =1
z j ∨
n
l=1
ITE(x i , q j,l , p j,l )
,
(8.12)
which ensure that if and only if z j = 1, then the j -th product term evaluates to 1 for
assignment x 1 · · · x n . The if-then-else-operator is defined as
ITE(x i , v j,l , u j,l ) =
⎧
⎪ ⎪ ⎨
⎪ ⎪ ⎩
v j,l ,
if x i = 1
u j,l ,
if x i = 0
f alse, otherwise
(8.13)
H. Riener et al.
8.3.2 SAT-Based Exact Synthesis Procedure
In this section, we propose a SAT-based exact synthesis approach for ESOP
forms. The approach is based on ideas from Knuth [15] (originally proposed by
Kamath et al. [14]) and our previous work on learning two-level patches to correct
combinational Boolean circuits [24]. Our approach synthesizes an ESOP form for
the Boolean function in Example 8.1 in less than a second. We formalize the search
problem as a series of Boolean constraint satisfaction problems—one for each
possible ESOP size k (starting with k = 1) and employ a decision procedure for
Boolean satisfiability to decide the satisfiability of the constraints. The constraints
are constructed in such a way that they are satisfiable if and only if an ESOP form
with k product terms exists and each satisfying assignment corresponds to an ESOP
form with k product terms. If the constraints are unsatisfiable, then no ESOP form
restricted to k product terms, that is equivalent to the provided Boolean function,
exists. By systematically solving the constraint satisfaction problem for increasing
values of the size parameter k, a minimal ESOP form is guaranteed to be found.
Formulation of the Constraint Satisfaction Problem Suppose that f : B n
3 →
B is a (single-output) Boolean function over n Boolean variables. We formulate
the problem of finding an ESOP form equivalent to f with k product terms as a
constraint satisfaction problem in propositional logic using 2nk Boolean variables,
p = p 1,1 , . . . , p k,n and q = q 1,1 , . . . , q k,n , where n is the number of Boolean
variables of f , k is the size of the ESOP form, and
p j,l = [x l in product term j ] and q j,l = [ ¯
x l in product term j ]
(8.11)
for 1 ≤ j ≤ k and 1 ≤ l ≤ n.
For each assignment x 1 · · · x n ∈ B n
3 of the Boolean function f with the
corresponding output value f (x 1 , . . . , x n ) = b, we introduce k auxiliary Boolean
variables z = z 1 , . . . , z k and add k · n + k clauses
k
j =1
n
l=1
¯
z j ∨ ITE(x i , ¯
q j,l , ¯
p j,l )
and
k
j =1
z j ∨
n
l=1
ITE(x i , q j,l , p j,l )
,
(8.12)
which ensure that if and only if z j = 1, then the j -th product term evaluates to 1 for
assignment x 1 · · · x n . The if-then-else-operator is defined as
ITE(x i , v j,l , u j,l ) =
⎧
⎪ ⎪ ⎨
⎪ ⎪ ⎩
v j,l ,
if x i = 1
u j,l ,
if x i = 0
f alse, otherwise
(8.13)