Interpolating functions from large Boolean relations

Boolean relations are an important tool in system synthesis and verification to characterize solutions to a set of Boolean constraints. For physical realization as hardware, a deter-ministic function often has to be extracted from a relation. Prior methods however are unlikely to handle large problem instances. From the scalability standpoint this paper demon-strates how interpolation can be exploited to extend deter-minization capacity. A comparative study is performed on several proposed computation techniques. Experimental re-sults show that Boolean relations with thousands of variables can be effectively determinized and the extracted functional implementations are of reasonable quality. 1