{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:07:56Z","timestamp":1761620876794},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bf00881805","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:42:21Z","timestamp":1104133341000},"page":"359-383","source":"Crossref","is-referenced-by-count":65,"title":["Branching rules for satisfiability"],"prefix":"10.1007","volume":"15","author":[{"given":"J. N.","family":"Hooker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V.","family":"Vinay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Amini, M. M. and Racer, M.: A variable-depth-search heuristic for the generalized assignment problem,Management Science, to appear."},{"key":"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":"CR3","doi-asserted-by":"crossref","unstructured":"Cook, S. A.: The complexity of theorem-proving procedures, inProc. 3rd Annual ACM Symp. on the Theory of Computing, 1971, pp. 151?158.","DOI":"10.1145\/800157.805047"},{"key":"CR4","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, e-mail jc@research.att.com."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M. and Putnam, H.: A computing procedure for quantification theory,J. ACM 7 (1960), 201?215.","journal-title":"J. ACM"},{"key":"CR6","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, e-mail dubois@laforia.ibp.fr."},{"key":"CR7","unstructured":"Dubois, O., Andre, P., Boufkhad, Y., and Carlier, J.: SAT versus UNSAT, manuscript, Laforia, CNRS-Universit\u00e9 Paris 6, 4 place Jussieu, 75252 Paris cedex 05, France, 1993, e-mail dubois@laforia.ibp.fr."},{"key":"CR8","volume-title":"Infinite and Finite Sets","author":"P. Erd\u00f6s","year":"1975","unstructured":"Erd\u00f6s, P. and Lov\u00e1sz, L.: Problems and results on 3-chromatic hypergraphs and some related questions, inInfinite and Finite Sets, North-Holland, Amsterdam, 1975."},{"key":"CR9","volume-title":"Failed literals in the Davis-Putnam procedure for SAT","author":"T. W. Freeman","year":"1993","unstructured":"Freeman, T. W.: Failed literals in the Davis-Putnam procedure for SAT, manuscript, Computer and Information Science, University of Pennsylvania, Philadelphia, PA, 19104 USA, CA, 1993, freeman@gradient.cis.upenn.edu."},{"key":"CR10","unstructured":"Gallo, G. and Pretolani, D.: A new algorithm for the propositional satisfiability problem, report TR-3\/90, Dip. di Informatica, Universit\u00e1 di Pisa,Discrete Applied Mathematics, to appear."},{"key":"CR11","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 Urbani, G.: Algorithms for testing the satisfiability of propositional formulae,J. Logic programming 7 (1989), 45?61.","journal-title":"J. Logic programming"},{"key":"CR12","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 Stewart, W. R.: 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, pp. 207?249."},{"key":"CR13","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1287\/ijoc.6.4.423","volume":"6","author":"F. Harche","year":"1994","unstructured":"Harche, F., Hooker, J. N., and Thompson, G.: A computational study of sastifiability algorithms for propositional logic,ORSA J. Computing 6 (1994), 423?435. For more information contact J. Hooker, email jh38@andrew.cmu.edu.","journal-title":"ORSA J. Computing"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1287\/opre.42.2.201","volume":"42","author":"J. N. Hooker","year":"1994","unstructured":"Hooker, J. N.: Needed: An empirical science of algorithms,Operations Research 42 (1994), 201?212.","journal-title":"Operations Research"},{"key":"CR15","first-page":"123","volume":"1","author":"J. N. Hooker","year":"1990","unstructured":"Hooker, J. N. and Fedjki, C.: Branch and cut solution of inference problems in propositional logic,Annals of Mathematics and AI 1 (1990), 123?139.","journal-title":"Annals of Mathematics and AI"},{"key":"CR16","unstructured":"Iwama, K., Albeta, H., and Miyano, E.: Random generation of satisfiable and unsatisfiable CNF predicates, inProc. of 12th IFIP World Computer Congress, 1992, pp. 322?328. For further information contact Eiji Miyano, Dept. of Computer Science and Communication Engineering, Kyushu University, Fukuoka 812, Japan, e-mail miyano@csce.kyushu-u.ac.jp."},{"key":"CR17","first-page":"167","volume":"1","author":"R. Jeroslow","year":"1990","unstructured":"Jeroslow, R. and Wang, J.: Solving propositional satisfiability problems,Annals of Mathematics and AI 1 (1990), 167?187.","journal-title":"Annals of Mathematics and AI"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/BF01581082","volume":"57","author":"A. Kamath","year":"1992","unstructured":"Kamath, A., Karmarkar, N., Ramakrishnan, K., and Resende, M.: A continuous approach to inductive inference,Mathematical Programming 57 (1992), 215?238. For further information contact Mauricio Resende, AT&T Bell Laboratories, Murray Hill, NJ 07974 USA, e-mail mgcr@research.att.com.","journal-title":"Mathematical Programming"},{"key":"CR19","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 Rardin, R. L.: Controlled experimental design for statistical comparison of integer programming algorithms,Management Science 25 (1980), 1258?1271.","journal-title":"Management Science"},{"key":"CR20","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.:Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam, 1978."},{"key":"CR21","unstructured":"Mitterreiter, I. and Radermacher, F. J.: Experiments on the running time behavior of some algorithms solving propositional logic problems, manuscript, Forschungsinstitut f\u00fcr anwendungsorientierte Wissensverarbeitung, Ulm, Germany, 1991."},{"key":"CR22","volume-title":"Design and Analysis of Experiments","author":"R. G. Petersen","year":"1985","unstructured":"Petersen, R. G.:Design and Analysis of Experiments, Marcel Dekker, New York, 1985."},{"key":"CR23","unstructured":"Pretolani, D.: Efficiency and stability of hypergraph SAT algorithms, manuscript, Dip. di Informatica, Univ. di Pisa, Corso Itali 40, 56125 Pisa, Italy. For information on problems contact e-mail pretola@di.unipi.it."},{"key":"CR24","unstructured":"Spencer, J.:Ten Lectures on the Probabilistic Method, Regional Conference Series in Applied Mathematics52, Society for Industrial and Applied Mathematics, Philadelphia, PA, 1987."},{"key":"CR25","unstructured":"Van Gelder, A. and Tsuji, Y. K.: Satisfiability testing with more reasoning and less guessing, manuscript, University of California, Santa Cruz, CA, USA, 1994. For information on problems contact e-mail avg@cs.ucsc.edu or tsuji@cs.ucsc.edu."},{"key":"CR26","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?314.","journal-title":"Computers and Operations Research"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881805.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881805\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881805","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:54:25Z","timestamp":1586044465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881805"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF00881805"],"URL":"https:\/\/doi.org\/10.1007\/bf00881805","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}