Application of Indexed Partition Calculus in Logic Synthesis of Boolean Functions for FPGAs

Application of Indexed Partition Calculus in Logic Synthesis of Boolean Functions for FPGAsFunctional decomposition of Boolean functions specified by cubes proved to be very efficient. Most popular decom-position methods are based on blanket calculus. However computation complexity of blanket manipulations strongly depends on number of function's variables, which prevents them from being used for large functions of many input and output variables. In this paper a new concept of indexed partition is proposed and basic operations on indexed partitions are defined. Application of this concept to logic synthesis based on functional decomposition is also discussed. The experimental results show that algorithms based on new concept are able to deliver good quality solutions even for large functions and does it many times faster than the algorithms based on blanket calculus.

Some remarks on the partition calculus of ordinals

One of the early partition relation theorems which include ordinals was the observation of Erdös and Rado [7] that if κ = cf(κ) > ω then the Dushnik–Miller theorem can be sharpened to κ→(κ, ω + 1)2. The question on the possible further extension of this result was answered by Hajnal who in [8] proved that the continuum hypothesis implies ω1 ↛ (ω1, ω + 2)2. He actually proved the stronger result ω1 ↛ (ω: 2))2. The consistency of the relation κ↛(κ, (ω: 2))2 was later extensively studied. Baumgartner [1] proved it for every κ which is the successor of a regular cardinal. Laver [9] showed that if κ is Mahlo there is a forcing notion which adds a witness for κ↛ (κ, (ω: 2))2 and preserves Mahloness, ω-Mahloness of κ, etc. We notice in connection with these results that λ→(λ, (ω: 2))2 holds if λ is singular, in fact λ→(λ, (μ: n))2 for n < ω, μ < λ (Theorem 4).In [11] Todorčević proved that if cf(λ) > ω then a ccc forcing can add a counter-example to λ→(λ, ω + 2)2. We give an alternative proof of this (Theorem 5) and extend it to larger cardinals: if GCH holds, cf (λ) > κ = cf (κ) then < κ-closed, κ+-c.c. forcing adds a counter-example to λ→(λ, κ + 2)2 (Theorem 6).Erdös and Hajnal remarked in their problem paper [5] that Galvin had proved ω2→(ω1, ω + 2)2 and he had also asked if ω2→(ω1, ω + 3)2 is true. We show in Theorem 1 that the negative relation is consistent.