{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:36Z","timestamp":1725664236605},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_126","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:51:14Z","timestamp":1330293074000},"page":"748-762","source":"Crossref","is-referenced-by-count":8,"title":["Partitioning methods for satisfiability testing on large formulas"],"prefix":"10.1007","author":[{"given":"Tai Joon","family":"Park","sequence":"first","affiliation":[]},{"given":"Allen","family":"Gelder","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"63_CR1","doi-asserted-by":"publisher","first-page":"1088","DOI":"10.1109\/43.310898","volume":"9","author":"P.K. Chan","year":"1994","unstructured":"P.K. Chan, M.D.F. Schlag, and J.Y. Zien. \u201cSpectral K-way ratio-cut partitioning\u201d. IEEE Transactions on Computer-Aided Design of Integrated Circuits and systems, 9:1088\u20131096, Sept. 1994.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and systems"},{"key":"63_CR2","first-page":"394","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. \u201cA Machine Program for Theorem-Proving\u201d. Communications of the Association for Computing Theroy, 5:394\u2013397, 1962.","journal-title":"Communications of the Association for Computing Theroy"},{"key":"63_CR3","unstructured":"W.E. Donath. \u201cLogic Partitioning\u201d. In in Physical Design Automation of VLSI systems, Benjamin\/Cummings, pages 65\u201386, 1988."},{"key":"63_CR4","first-page":"201","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. \u201cA Computing Procedure for Quantification Theory\u201d. Journal of the Association for Computing Theroy, 7:201\u2013215, 1960.","journal-title":"Journal of the Association for Computing Theroy"},{"key":"63_CR5","doi-asserted-by":"crossref","unstructured":"C. Fiduccia and R. Mattheyses. \u201cA linear-time heuristic for improving network partition\u201d. In In ACM IEEE 19th Design and Automation Conference Proceedings, pages 175\u2013181, June, 1982.","DOI":"10.1109\/DAC.1982.1585498"},{"key":"63_CR6","unstructured":"M. Garey and D.S. Johnson. \u201cComputers and Intractability: A Guide to Theory of NP-Completeness\u201d. M.H.Freeman, 1979."},{"key":"63_CR7","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0166-218X(93)90045-P","volume":"42","author":"G. Gallo","year":"1993","unstructured":"G. Gallo, G. Longo, and S. Pallottino. \u201cDirected Hypergraph and Applications\u201d. Discrete Applied Mathematics, 42:177\u2013201, 1993.","journal-title":"Discrete Applied Mathematics"},{"key":"63_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0743-1066(89)90009-5","volume":"7","author":"G. Gallo","year":"1989","unstructured":"G. Gallo and G. Urbani. \u201cAlgorithms for Testing the Satisfiability of Propositional Formulae\u201d. Journal of Logic Programming, 7:45\u201361, 1989.","journal-title":"Journal of Logic Programming"},{"key":"63_CR9","unstructured":"Andrew B. Kahng. \u201cNew Spectral Method for Ratio Cut Partitioning and Clustering\u201d. IEEE Trans. on CAD, 1991."},{"issue":"220","key":"63_CR10","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1126\/science.220.4598.671","volume":"13","author":"S. Kirkpatrick","year":"1983","unstructured":"S. Kirkpatrick, C. Gelatt, Jr., and M. Vecchi. \u201cOptimization by Simulated Annealing\u201d. Science, 13(220):671\u2013680, May, 1983.","journal-title":"Science"},{"key":"63_CR11","doi-asserted-by":"crossref","unstructured":"B.W. Kernighan and S. Lin. \u201cAn Efficient Heuristic Procedure for Partitioning Electrical Circuits\u201d. In Bell System Technical J., Feb. 1970.","DOI":"10.1002\/j.1538-7305.1970.tb01770.x"},{"key":"63_CR12","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee. \u201cTest Pattern Generation Using Boolean Satisfiability\u201d. IEEE Transactions on Computer-Aided Design, 11:4\u201315, January 1992.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"63_CR13","doi-asserted-by":"crossref","unstructured":"A. Van Gelder and Y.K. Tsuji. \u201cSatisfiability Testing with More Reasoning and Less Guessing\u201d. In D. S. Johnson and M. Trick, editors, Cliques, Coloring, and Satisfiability: Second DIMACS Implementation and Challenge., DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1995.","DOI":"10.1090\/dimacs\/026\/27"},{"key":"63_CR14","unstructured":"Y.C. Wei and C.K. Cheng. \u201cTowards Efficient Hierarchical Designs by Ratio Cut Partitioning\u201d. In IEEE Intl. Conf. on Computer-Aided Design, pages 298\u2013301, 1989."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_126.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:18Z","timestamp":1605647238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_126"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_126","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}