{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:59:24Z","timestamp":1756994364661},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540587156"},{"type":"electronic","value":"9783540490548"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58715-2_143","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:42:11Z","timestamp":1330256531000},"page":"426-437","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Branching rules for satisfiability"],"prefix":"10.1007","author":[{"given":"J. N.","family":"Hooker","sequence":"first","affiliation":[]},{"given":"V.","family":"Vinay","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"35_CR1","unstructured":"Amini, M. M., and M. Racer, A variable-depth-search heuristic for the generalized assignment problem, to appear in Management Science."},{"key":"35_CR2","series-title":"Technical report","volume-title":"Report on a SAT competition","author":"H. B\u00f6hm","year":"1992","unstructured":"B\u00f6hm, H., Report on a SAT competition, Technical report No. 110, Universit\u00e4t Paderborn, Germany, 1992."},{"key":"35_CR3","unstructured":"Crawford, J., problems contributed to DIMACS. For information contact Crawford at AT&T Bell Laboratories, 600 Mountain Ave., Murray Hill, NJ 07974-0636 USA, email jc@research.att.com."},{"key":"35_CR4","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., and H. Putnam, A computing procedure for quantification theory, Journal of the ACM 7 (1960) 201\u2013215.","journal-title":"Journal of the ACM"},{"key":"35_CR5","unstructured":"Dubois, O., problems contributed to DIMACS. For information contact Dubois at Laforia, CNRS-Universit\u00e9 Paris 6, 4 place Jussieu, 75252 Paris cedex 05, France, email dubois@laforia.ibp.fr."},{"key":"35_CR6","unstructured":"Dubois, O., P. Andre, Y. Boufkhad and J. Carlier, SAT versus UNSAT, manuscript, Laforia, CNRS-Universit\u00e9 Paris 6, 4 place Jussieu, 75252 Paris cedex 05, France, email dubois@laforia.ibp.fr, 1993."},{"key":"35_CR7","volume-title":"Infinite and Finite Sets","author":"P. Erd\u00f6s","year":"1975","unstructured":"Erd\u00f6s, P., and L. Lov\u00e1sz, Problems and results on 3-chromatic hypergraphs and some related questions, in Infinite and Finite Sets (North-Holland, Amsterdam) 1975."},{"key":"35_CR8","unstructured":"Gallo, G., and D. Pretolani, A new algorithm for the propositional satisfiability problem, report TR-3\/90, Dip. di Informatica, Universit\u00e1 di Pisa, to appear in Discrete Applied Mathematics."},{"key":"35_CR9","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0743-1066(89)90009-5","volume":"7","author":"G. Gallo","year":"1989","unstructured":"Gallo, G., and G. Urbani, Algorithms for testing the satisfiability of propositional formulae, Journal of Logic programming\n7 (1989) 45\u201361.","journal-title":"Journal of Logic programming"},{"key":"35_CR10","first-page":"207","volume-title":"The Traveling Salesman Problem: A Guided Tour of Combinatorial Optimization","author":"B. L. Golden","year":"1985","unstructured":"Golden, B. L., and W. R. Stewart, Empirical analysis of heuristics, in Lawler, Lenstra, Rinnooy Kan and Schmoys, eds., The Traveling Salesman Problem: A Guided Tour of Combinatorial Optimization (Wiley, New York, 1985) 207\u2013249."},{"key":"35_CR11","unstructured":"Harche, F., J. N. Hooker and G. Thompson, A computational study of sastifiability algorithms for prepositional logic, to appear in ORSA Journal on Computing. For more information contact J. Hooker, email jh38@andrew.cmu.edu."},{"key":"35_CR12","unstructured":"Hooker, J. N., Needed: An empirical science of algorithms, to appear in Operations Research."},{"key":"35_CR13","first-page":"123","volume":"1","author":"J. N. Hooker","year":"1990","unstructured":"Hooker, J. N., and C. Fedjki, Branch and cut solution of inference problems in propositional logic, Annals of Mathematics and AI\n1 (1990) 123\u2013139.","journal-title":"Annals of Mathematics and AI"},{"key":"35_CR14","unstructured":"Iwama, K., H. Albeta and E. Miyano, Random generation of satisfiable and unsatisfiable CNF predicates, Proceedings of 12th IFIP World Computer Congress (1992) 322\u2013328. For further information contact Eiji Miyano, Dept. of Computer Science and Communication Engineering, Kyushu University, Fukuoka 812, Japan, email miyano@csce.kyushu-u.ac.jp."},{"key":"35_CR15","first-page":"167","volume":"1","author":"R. Jeroslow","year":"1990","unstructured":"Jeroslow, R., and J. Wang, Solving propositional satisfiability problems, Annals of Mathematics and AI\n1 (1990) 167\u2013187.","journal-title":"Annals of Mathematics and AI"},{"key":"35_CR16","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/BF01581082","volume":"57","author":"A. Kamath","year":"1992","unstructured":"Kamath, A., N. Karmarkar, K. Ramakrishnan, and M. Resende, A continuous approach to inductive inference, Mathematical Programming\n57 (1992) 215\u2013238. For further information contact Mauricio Resende, AT&T Bell Laboratories, Murray Hill, NJ 07974 USA, email mgcr@research.att.com.","journal-title":"Mathematical Programming"},{"key":"35_CR17","doi-asserted-by":"crossref","first-page":"1258","DOI":"10.1287\/mnsc.25.12.1258","volume":"25","author":"B. W. Lin","year":"1980","unstructured":"Lin, B. W., and R. L. Rardin, Controlled experimental design for statistical comparison of integer programming algorithms, Management Science\n25 (1980) 1258\u20131271.","journal-title":"Management Science"},{"key":"35_CR18","unstructured":"Loveland, D. W., Automated Theorem Proving: A Logical Basis (North-Holland, 1978)."},{"key":"35_CR19","unstructured":"Mitterreiter, I., and F. J. Radermacher, Experiments on the running time behavior of some algorithms solving propositional logic problems, manuscript, Forschungsinstitut f\u00fcr anwendungsorientierte Wissensverarbeitung, Ulm, Germany, 1991."},{"key":"35_CR20","volume-title":"Design and Analysis of Experiments","author":"R. G. Petersen","year":"1985","unstructured":"Petersen, R. G., Design and Analysis of Experiments (M. Dekker, New York, 1985)."},{"key":"35_CR21","unstructured":"Pretolani, D., Centre de recherche sur les transports, 3535 Queen Mary, Suite 430, Montr\u00e9al, Qu\u00e9bec H3V 1H8, Canada, email daniele@crt.umontreal.ca."},{"key":"35_CR22","unstructured":"Spencer, J., Ten Lectures on the Probabilistic Method, Regional Conference Series in Applied Mathematics 52, (Society for Industrial and Applied Mathematics, Philadelphia, 1987)."},{"key":"35_CR23","unstructured":"Van Gelder, A., and Y. K. Tsuji, problems contributed to DIMACS. For information contact them at University of California, Santa Cruz, CA USA, email avg@cs.ucsc.edu or tsuji@cs.ucsc.edu."},{"key":"35_CR24","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/0305-0548(90)90007-T","volume":"90","author":"J. M. Wilson","year":"1990","unstructured":"Wilson, J. M., Compact normal forms in propositional logic and integer programming formulations, Computers and Operations Research. 90 (1990) 309\u2013314.","journal-title":"Computers and Operations Research"}],"container-title":["Lecture Notes in Computer Science","Foundation of Software Technology and Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58715-2_143","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:17:00Z","timestamp":1578507420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58715-2_143"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540587156","9783540490548"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-58715-2_143","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"1 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}