8 Exact Synthesis of ESOP Forms
183
with v j,l ∈ {q j,l , ¯
q j,l } and u j,l ∈ {p j,l , ¯
p j,l }, respectively. One additional XORconstraint
⎛
⎝
k
j =1
z j
⎞
⎠ = b
(8.14)
per assignment guarantees that an odd number of z j s evaluates to 1 if b = 1 and an
even number if b = 0.
This constraint satisfaction problem is satisfiable if and only if an ESOP form
of size k exists and each satisfying assignment ˆ
p 1,1 , . . . , ˆ
p k,n and ˆ
q 1,1 , . . . , ˆ
q k,n
corresponds to one possible implementation.
Translating XOR-Constraints to CNF All XOR-constraints in the constraint
satisfaction problem are, by construction, formulated over disjoint sets of Boolean
variables such that techniques like Gaussian elimination are not effective. Instead,
we translate each XOR-constraint first into an equivalent XOR-clause by flipping
one of the Boolean variables if and only if b = 0, i.e.,
(z 1 ⊕ · · · ⊕ z k ) = b =⇒
z 1 ⊕ · · · ⊕ z k , if b = 1
z 1 ⊕ · · · ⊕ ¯
z k , if b = 0.
(8.15)
Then, we select two literals l a , l b from the XOR-clause and apply the Tseitin
transformation to generate four clauses (¯ z a ∨ ¯
z b ∨ ¯
u), (z a ∨ z b ∨ ¯
u), (z a ∨ ¯
z b ∨ u),
(¯ z a ∨ z b ∨ u) with the newly introduced Boolean variable u and repeat this process
until only one literal is left which is added as a unit clause.
SAT-Based Exact ESOP Synthesis The overall exact synthesis procedure is
sketched in Algorithm 3. The function MakeCSP constructs the constraint satisfaction problem ϕ in the Boolean variables p, q, z for a given Boolean function f
and size parameter k as described above. The function SAT refers to the invocation
of a decision procedure for the Boolean satisfiability problem, usually called a
SAT-solver, and is assumed to decide the satisfiability of ϕ and, if satisfiable,
to also provide a satisfying assignment ˆ
p and ˆ
q for variables p and q. The
Algorithm 3 SAT-based exact ESOP synthesis
input : a (possibly incompletely-specified) Boolean function f
output: a minimal ESOP functionally equivalent to f
for k ← 1, 2, . . . do
ϕ(p, q, z) ← MakeCSP(k,f );
if ˆ
p, ˆ
q |= SAT(∃z : ϕ(p, q, z)) then
return MakeESOP( ˆ
p, ˆ
q);
end
end
183
with v j,l ∈ {q j,l , ¯
q j,l } and u j,l ∈ {p j,l , ¯
p j,l }, respectively. One additional XORconstraint
⎛
⎝
k
j =1
z j
⎞
⎠ = b
(8.14)
per assignment guarantees that an odd number of z j s evaluates to 1 if b = 1 and an
even number if b = 0.
This constraint satisfaction problem is satisfiable if and only if an ESOP form
of size k exists and each satisfying assignment ˆ
p 1,1 , . . . , ˆ
p k,n and ˆ
q 1,1 , . . . , ˆ
q k,n
corresponds to one possible implementation.
Translating XOR-Constraints to CNF All XOR-constraints in the constraint
satisfaction problem are, by construction, formulated over disjoint sets of Boolean
variables such that techniques like Gaussian elimination are not effective. Instead,
we translate each XOR-constraint first into an equivalent XOR-clause by flipping
one of the Boolean variables if and only if b = 0, i.e.,
(z 1 ⊕ · · · ⊕ z k ) = b =⇒
z 1 ⊕ · · · ⊕ z k , if b = 1
z 1 ⊕ · · · ⊕ ¯
z k , if b = 0.
(8.15)
Then, we select two literals l a , l b from the XOR-clause and apply the Tseitin
transformation to generate four clauses (¯ z a ∨ ¯
z b ∨ ¯
u), (z a ∨ z b ∨ ¯
u), (z a ∨ ¯
z b ∨ u),
(¯ z a ∨ z b ∨ u) with the newly introduced Boolean variable u and repeat this process
until only one literal is left which is added as a unit clause.
SAT-Based Exact ESOP Synthesis The overall exact synthesis procedure is
sketched in Algorithm 3. The function MakeCSP constructs the constraint satisfaction problem ϕ in the Boolean variables p, q, z for a given Boolean function f
and size parameter k as described above. The function SAT refers to the invocation
of a decision procedure for the Boolean satisfiability problem, usually called a
SAT-solver, and is assumed to decide the satisfiability of ϕ and, if satisfiable,
to also provide a satisfying assignment ˆ
p and ˆ
q for variables p and q. The
Algorithm 3 SAT-based exact ESOP synthesis
input : a (possibly incompletely-specified) Boolean function f
output: a minimal ESOP functionally equivalent to f
for k ← 1, 2, . . . do
ϕ(p, q, z) ← MakeCSP(k,f );
if ˆ
p, ˆ
q |= SAT(∃z : ϕ(p, q, z)) then
return MakeESOP( ˆ
p, ˆ
q);
end
end