{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:39:51Z","timestamp":1737005991083,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425410"},{"type":"electronic","value":"9783540447986"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44798-9_24","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T17:16:15Z","timestamp":1178212575000},"page":"293-309","source":"Crossref","is-referenced-by-count":14,"title":["Using Combinatorial Optimization Methods for Quantification Scheduling"],"prefix":"10.1007","author":[{"given":"P.","family":"Chauhan","sequence":"first","affiliation":[]},{"given":"E.","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"S.","family":"Jha","sequence":"additional","affiliation":[]},{"given":"J.","family":"Kukula","sequence":"additional","affiliation":[]},{"given":"H.","family":"Veith","sequence":"additional","affiliation":[]},{"given":"D.","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in Symbolic Model Checking. In 28th ACM\/IEEE Design Automation Conference, 1991.","DOI":"10.1145\/127601.127702"},{"key":"24_CR2","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic Model Checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proceedings of the International Conference on Very Large Scale Int egration, Edinburgh, Scotland, August 1991."},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"885","DOI":"10.2307\/3214721","volume":"29","author":"C. J. P. Belisle","year":"1992","unstructured":"C. J. P. B\u2019elisle. Convergence theorems for a class of simulated annealing algorithms. Journal of Applied Probability, 29:885\u2013892, 1992.","journal-title":"Journal of Applied Probability"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/0020-0190(92)90140-Q","volume":"42","author":"T. N. Bui","year":"1992","unstructured":"T. N. Bui and C. Jones. Finding good approximate vertex and edge partitions is NP-hard. Information Processing Letters, 42:153\u2013159, 1992.","journal-title":"Information Processing Letters"},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Proceedings of International Conference on Computer-Aided Verification (CAV\u201999)","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings of International Conference on Computer-Aided Verification (CAV\u201999), number 1633 in Lecture Notes in Computer Science, pages 495\u2013499. Springer, July 1999."},{"key":"24_CR6","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"C.M. Fiduccia and R.M. Mattheyses. A linear time heuristic for improving network partitions. In 19th ACM\/IEEE Design Automation Conference, pages 175\u2013181, 1982.","DOI":"10.1109\/DAC.1982.1585498"},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-58179-0_63","volume-title":"Sixth Conference on Computer Aided Verification (CAV\u201994)","author":"D. Geist","year":"1994","unstructured":"D. Geist and I. Beer. Efficient Model Checking by automated ordering of transition relation partitions. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV\u201994), volume 818 of LNCS, pages 299\u2013310, Stanford, CA, USA, 1994. Springer-Verlag."},{"key":"24_CR9","unstructured":"Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., 1979."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"B. Hajek. A tutorial survey of theory and applications of simulated annealing. In Proc. 24th IEEE Conf. Decision and Control, pages 755\u2013760, 1985.","DOI":"10.1109\/CDC.1985.268599"},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1126\/science.220.4598.671","volume":"220","author":"S. Kirkpatrick","year":"1983","unstructured":"S. Kirkpatrick, C. D. Gelatt Jr., and M. P. Vecchi. Optimization by simulated annealing. Science, 220:671\u2013679, 1983.","journal-title":"Science"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Brian Kernighan and S. Lin. An efficient heuristic procedure for partitioning graphs. The Bell System Technical Journal, pages 291\u2013307, February 1970.","DOI":"10.1002\/j.1538-7305.1970.tb01770.x"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"In-Ho Moon, James H. Kukula, Kavita Ravi, and Fabio Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the 37th Design Automation Conference (DAC\u201900), pages 26\u201328, Los Angeles, June 2000.","DOI":"10.1145\/337292.337305"},{"issue":"6","key":"24_CR14","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1063\/1.1699114","volume":"21","author":"N. Metropolis","year":"1953","unstructured":"N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller. Equation of state calculations by fast computing machines. Journal of Chemical Phyics, 21(6):1087\u20131092, 1953.","journal-title":"Journal of Chemical Phyics"},{"key":"24_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-40922-X_6","volume-title":"Proceedings of the Formal Methods in Computer Aided Design (FMCAD\u201900)","author":"I.-H. Moon","year":"2000","unstructured":"In-Ho Moon and Fabio Somenzi. Border-block triangular form and conjunction schedule in image computation. In Warren A. Hunt Jr. and Steven D. Johnson, editors, Proceedings of the Formal Methods in Computer Aided Design (FMCAD\u201900), volume 1954 of LNCS, pages 73\u201390, November 2000."},{"key":"24_CR16","unstructured":"R.K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R.K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE\/ACM International Workshop on Logic Synthesis, Lake Tahoe, 1995. IEEE\/ACM."},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDDs. In Proceedings of the IEEE international Conference on Computer Aided Design (ICCAD), pages 130\u2013133, November 1990.","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"24_CR18","unstructured":"Bwolen Yang. Optimizing Model Checking Based on BDD Characterization. PhD thesis, Carnegie Mellon University, Computer Science Department, May 1999."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44798-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:57:26Z","timestamp":1736989046000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}