This paper presents a heuristic polarity decision-making algorithm for solving Boolean satisfiability （SAT）. The algorithm inherits many features of the current state-of-the-art SAT solvers, such as fast BCP, clause...This paper presents a heuristic polarity decision-making algorithm for solving Boolean satisfiability （SAT）. The algorithm inherits many features of the current state-of-the-art SAT solvers, such as fast BCP, clause recording, restarts, etc. In addition, a preconditioning step that calculates the polarities of variables according to the cover distribution of Karnaugh map is introduced into DPLL procedure, which greatly reduces the number of conflicts in the search process. The proposed approach is implemented as a SAT solver named DiffSat. Experiments show that DiffSat can solve many ＂real-life＂ instances in a reasonable time while the best existing SAT solvers, such as Zchaff and MiniSat, cannot. In particular, DiffSat can solve every instance of Bart benchmark suite in less than 0.03 s while Zchaff and MiniSat fail under a 900 s time limit. Furthermore, DiffSat even outperforms the outstanding incomplete algorithm DLM in some instances.展开更多
This paper aims to explore RLC equivalent circuit synthesis method forreduced-order models of interconnect circuits obtained by Krylov subspace basedmodel order reduction (MOR) methods. To guarantee pure RLC equivalen...This paper aims to explore RLC equivalent circuit synthesis method forreduced-order models of interconnect circuits obtained by Krylov subspace basedmodel order reduction (MOR) methods. To guarantee pure RLC equivalent circuitscan be synthesized, both the structures of input and output incidence matrices and theblock structure of the circuit matrices should be preserved in the reduced-order models.Block structure preserving MOR methods have been well established. In this paper,we propose an embeddable Input-Output structure Preserving Order Reduction(IOPOR) technique to further preserve the structures of input and output incidencematrices. By combining block structure preserving MOR methods and IOPOR technique,we develop an RLC equivalent circuit synthesis method RLCSYN (RLC SYNthesis).Inline diagonalization and regularization techniques are specifically proposedto enhance the robustness of inductance synthesis. The pure RLC model, high modelingaccuracy, passivity guaranteed property and SPICE simulation robustness makeRLCSYN more applicable in interconnect analysis, either for digital IC design ormixedsignal IC simulation.展开更多
基金the National Natural Science Foundation of China (Grant Nos. 90207002, 90307017, 60773125 and 60676018)National Science Foundation (Grant Nos. CCR-0306298)+1 种基金China Postdoctoral Science Foundation (Grant No. KLH1202005)the Natural Science Foundation of Shanghai City (Grant No. 06ZR14016)
文摘This paper presents a heuristic polarity decision-making algorithm for solving Boolean satisfiability （SAT）. The algorithm inherits many features of the current state-of-the-art SAT solvers, such as fast BCP, clause recording, restarts, etc. In addition, a preconditioning step that calculates the polarities of variables according to the cover distribution of Karnaugh map is introduced into DPLL procedure, which greatly reduces the number of conflicts in the search process. The proposed approach is implemented as a SAT solver named DiffSat. Experiments show that DiffSat can solve many ＂real-life＂ instances in a reasonable time while the best existing SAT solvers, such as Zchaff and MiniSat, cannot. In particular, DiffSat can solve every instance of Bart benchmark suite in less than 0.03 s while Zchaff and MiniSat fail under a 900 s time limit. Furthermore, DiffSat even outperforms the outstanding incomplete algorithm DLM in some instances.
基金NSFC research project 90307017 and 60676018partly by the National Basic Research Program of China under the grant 2005CB321701+2 种基金partly by Cross-Century Outstanding Scholar’s fund of Ministry of Education of China,partly by the doctoral program foundation of Ministry of Education of China 20050246082partly by Shanghai Dawn Project 200601partly by the National Science Foundation(NSF)under Grant CCR-0306298.
文摘This paper aims to explore RLC equivalent circuit synthesis method forreduced-order models of interconnect circuits obtained by Krylov subspace basedmodel order reduction (MOR) methods. To guarantee pure RLC equivalent circuitscan be synthesized, both the structures of input and output incidence matrices and theblock structure of the circuit matrices should be preserved in the reduced-order models.Block structure preserving MOR methods have been well established. In this paper,we propose an embeddable Input-Output structure Preserving Order Reduction(IOPOR) technique to further preserve the structures of input and output incidencematrices. By combining block structure preserving MOR methods and IOPOR technique,we develop an RLC equivalent circuit synthesis method RLCSYN (RLC SYNthesis).Inline diagonalization and regularization techniques are specifically proposedto enhance the robustness of inductance synthesis. The pure RLC model, high modelingaccuracy, passivity guaranteed property and SPICE simulation robustness makeRLCSYN more applicable in interconnect analysis, either for digital IC design ormixedsignal IC simulation.
