Skolem and Herbrand functions are important certificates validating the truth and falsity, respectively, of quantified Boolean formulas (QBFs). They are essential in various synthesis and verification applications. Recent advancement established a linear time extraction of Skolem/Herbrand functions from QBF consensus/resolution proofs. However, the obtained functions are often excessively large and improper for practical applications. To overcome this limitation, this paper characterizes various flexibilities of QBF certificates, and exploits them for certificate simplification. Experiments show substantial reduction on QBF certificates in terms of circuit size and depth, which are of primary concerns for synthesis applications.

Many computer science problems can be naturally and compactly expressed using quantified Boolean formulas (QBFs). Evaluating thetruth or falsity of a QBF is an important task, and constructing the corresponding model or countermodel can be as important and sometimes even more useful in practice. Modern search and learning based QBF solvers rely fundamentally on resolution and can be instrumented to produce resolution proofs, from which in turn Skolem-function models and Herbrand-function countermodels can be extracted. These (counter)models are the key enabler of various applications. Not until recently the superiority of long-distanceresolution (LQ-resolution) to short-distance resolution(Q-resolution) was demonstrated. While a polynomial algorithm exists for (counter)model extraction from Q-resolution proofs, it remains open whether it exists forLQ-resolution proofs. This paper settles this open problem affirmatively by constructing a linear-time extraction procedure. Experimental results show the distinct benefits of the proposed method in extracting high quality certificates from some LQ-resolution proofs that are not obtainable from Q-resolution proofs.

Through-silicon vias (TSVs) are required for transmitting signals among different dies for the 3-D integrated circuit (IC) technology. The significant silicon areas occupied by TSVs bring critical challenges for 3-D IC placement. Unlike most published 3-D placement works that only minimize the number of TSVs during placement due to the limitations in their techniques, this paper proposes a new 3-D cell placement algorithm that can additionally consider the sizes of TSVs and the physical positions for TSV insertion during placement. The algorithm consists of three stages: 1) 3-D analytical global placement with density optimization and whitespace reservation for TSVs; 2) TSV insertion and TSV-aware legalization; and 3) layer-by-layer detailed placement. In particular, the global placement is based on a novel weighted-average (WA) wirelength model, giving the first published model that can outperform the well-known log-sum-exp wirelength model theoretically and empirically. Also, a scheme is proposed to enhance the numerical stability of the WA wirelength model. Furthermore, 3-D routing can easily be accomplished by traditional 2-D routers since the physical positions of TSVs are determined during placement. Experimental results show the effectiveness of our algorithm. Compared with state-of-the-art 3-D cell placement works, our algorithm can achieve the best routed wirelength, TSV counts, and total silicon area, in shortest running time.

Through-silicon vias (TSVs) are required for transmitting signals among different dies for the three-dimensional integrated circuit (3D IC) technology. The significant silicon areas occupied by TSVs bring critical challenges for 3D IC placement. Unlike most published 3D placement works that only minimize the number of TSVs during placement due to the limitations in their techniques, this paper proposes a new 3D cell placement algorithm which can additionally consider the sizes of TSVs and the physical positions for TSV insertion during placement. The algorithm consists of three stages: (1) 3D analytical global placement with density optimization and whitespace reservation for TSVs, (2) TSV insertion and TSV-aware legalization, and (3) layer-by-layer detailed placement. In particular, the global placement is based on a novel weighted-average wirelength model, giving the first model in the literature that can outperform the well-known log-sum-exp wirelength model theoretically and empirically. Further, 3D routing can easily be accomplished by traditional 2D routers since the physical positions of TSVs are determined during placement. Compared with state-of-the-art 3D cell placement works, our algorithm can achieve the best routed wirelength, TSV counts, and total silicon area, in shortest running time.