{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T06:45:45Z","timestamp":1791269145709,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":56,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540602996","type":"print"},{"value":"9783540447887","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60299-2_31","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:14:59Z","timestamp":1330262099000},"page":"515-532","source":"Crossref","is-referenced-by-count":11,"title":["Polynomial restrictions of SAT: What can be done with an efficient implementation of the Davis and Putnam's procedure?"],"prefix":"10.1007","author":[{"given":"Antoine","family":"Rauzy","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"31_CR1","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0020-0190(87)90200-6","volume":"24","author":"V. Arvind","year":"1987","unstructured":"V. Arvind and S. Biswas. An O(n2) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes horn sentences. Information Processing Letters, 24:67\u201369, 1987.","journal-title":"Information Processing Letters"},{"key":"31_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0196-6774(80)90007-3","volume":"1","author":"B. Aspvall","year":"1980","unstructured":"B. Aspvall. Recognizing Disguised NR(1) Instances of the Satisfiability Problem. Journal of Algorithms, 1:97\u2013103, 1980.","journal-title":"Journal of Algorithms"},{"issue":"3","key":"31_CR3","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"B. Aspvall, M. Plass, and R. Tarjan. A Linear Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulae. Information Processing Letter, 8(3):121\u2013123, 1979.","journal-title":"Information Processing Letter"},{"key":"31_CR4","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0743-1066(91)90006-B","volume":"10","author":"G. Ausiello","year":"1990","unstructured":"G. Ausiello and G. Italiano. On-Line Algorithms for Polynoinially Solvable Satisfiability Problems. Journal of Logic Programming, 10:69\u201390, 1990.","journal-title":"Journal of Logic Programming"},{"key":"31_CR5","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1016\/S0019-9958(82)90439-9","volume":"55","author":"A. Blass","year":"1982","unstructured":"A. Blass and Y. Gurevitch. On the unique satisfiability problem. Information and Control, 55:80\u201388, 1982.","journal-title":"Information and Control"},{"key":"31_CR6","first-page":"139","volume-title":"Two algorithms for constraints system solving in propositional calculus and their implementation in prologIII","author":"J.M. Bo\u00ef","year":"1990","unstructured":"J.M. Bo\u00ef and A. Rauzy. Two algorithms for constraints system solving in propositional calculus and their implementation in prologIII. In P. Jorrand and V. Sugrev, editors, Proceedings Artificial Intelligence IV Methodology, Systems, Applications (AIMSA'90), pages 139\u2013148. North-Holand, September 1990. Alba-Varna bulgarie."},{"key":"31_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF01531068","volume":"1","author":"E. Boros","year":"1990","unstructured":"E. Boros, Y. Crama, and P.L. Hammer. Polynomial-time inference of all implications for Horn and related formulae. Annals of Mathematics and Artificial Intelligence, 1:21\u201332, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"31_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1137\/S0097539792228629","volume":"23","author":"E. Boros","year":"1994","unstructured":"E. Boros, Y. Crama, P.L. Hammer, and M. Saks. A complexity index for satisfiability problems. SIAM Journ. Comp., 23:45\u201349, 1994.","journal-title":"SIAM Journ. Comp."},{"key":"31_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0166-218X(94)90033-7","volume":"55","author":"E. Boros","year":"1994","unstructured":"E. Boros, P.L. Hammer, and X. Sun. Recognition of q-Horn formulae in linear time. Discrete Applied Mathematics, 55:1\u201313, 1994.","journal-title":"Discrete Applied Mathematics"},{"key":"31_CR10","volume-title":"Annals of Mathematics and Artificial Intelligence, volume 1","author":"V. Chandru","year":"1990","unstructured":"V. Chandru, C.R. Coulard, P.L. Hammer, M. Montanez, and X. Sun. On renamable Horn and generalized Horn functions. In Annals of Mathematics and Artificial Intelligence, volume 1. J.C. Baltzer AG, Scientific Publishing Company, Basel Switzerland, 1990."},{"key":"31_CR11","unstructured":"P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the Really Hard Problems Are. In Proceedings of the International Joint Conference of Artificial Intelligence, IJCAI'91, 1991."},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"V. Chv\u00e1tal and B. Reed. Miks gets some (the odds are on his side). In Proceedings of the 33rd IEEE Symp. on Foundations of Computer Science, pages 620\u2013627, 1992.","DOI":"10.1109\/SFCS.1992.267789"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"S.A. Cook. The Complexity of Theorem Proving Procedures. In Proceedings of the 3rd Ann. Symp. on Theory of Computing, ACM, pages 151\u2013158, 1971.","DOI":"10.1145\/800157.805047"},{"key":"31_CR14","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/0004-3702(94)90021-3","volume":"65","author":"M.C. Cooper","year":"1994","unstructured":"M.C. Cooper, D.A. Cohen, and P.G. Jeavons. Characterizing Tractable Constraints. Artificial Intelligence, 65:347\u2013361, 1994.","journal-title":"Artificial Intelligence"},{"key":"31_CR15","unstructured":"J.M. Crawford and L.D. Anton. Experimental results on the crossover point in satisfiability problems. In Proceedings of the Eleventh National Conference on Artificial Intelligence (Washington, D.C., AAAI'1993), pages 21\u201327, 1993."},{"key":"31_CR16","first-page":"394","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. JACM, 5:394\u2013397, 1962.","journal-title":"JACM"},{"key":"31_CR17","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A Computing Procedure for Quantification Theory. JACM, 7:201\u2013215, 1960.","journal-title":"JACM"},{"key":"31_CR18","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W.F. Dowling","year":"1984","unstructured":"W.F. Dowling and J.H. Gallier. Linear-time Algorithms for Testing the Satisfiablity of Propositional Horn Formulae. J. Logic Programming, 3:267\u2013284, 1984.","journal-title":"J. Logic Programming"},{"key":"31_CR19","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0166-218X(90)90020-D","volume":"26","author":"O. Dubois","year":"1990","unstructured":"O. Dubois. On the r,s-SAT satisfiability problem and a conjecture of Tovey. Discrete Applied Mathematics, 26:51\u201360, 1990.","journal-title":"Discrete Applied Mathematics"},{"key":"31_CR20","unstructured":"O. Dubois, P. Andr\u00e9, Y. Boufkhad, and J. Carlier. SAT versus UNSAT, 1994. Position paper, DIMACS chalenge on Satisfiability Testing, to appear."},{"key":"31_CR21","unstructured":"O. Dubois and J. Carlier. Sur le probl\u00e8me de satisfiabilit\u00e9. Communication at the Barbizon Workshop on SAT, October 1991."},{"key":"31_CR22","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1137\/0205048","volume":"5","author":"S. Even","year":"1976","unstructured":"S. Even, A. Itai, and A. Shamir. On the Complexity of Timetable and Multicommodity Flow Problems. SIAM J. Comput., 5:691\u2013703, 1976.","journal-title":"SIAM J. Comput."},{"key":"31_CR23","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0020-0190(88)90113-5","volume":"29","author":"G. Gallo","year":"1988","unstructured":"G. Gallo and M.G. Scutella. Polynomially Solvable Satisfiability Problems. Information Processing Letters, 29:221\u2013227, 1988.","journal-title":"Information Processing Letters"},{"key":"31_CR24","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. Algorithms for Testing the Satisfiablity of Propositional Formulae. Journal of Logic Programming, 7:45\u201361, 1989.","journal-title":"Journal of Logic Programming"},{"key":"31_CR25","volume-title":"Computer and Intractability: A Guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"M.R. Garey and D.S. Johnson. Computer and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Fransisco, 1979."},{"key":"31_CR26","unstructured":"I.P. Gent and T. Walsh. The SAT Phase Transition. In A.G. Cohn, editor, Proceedings of 11th European Conference on Artificial Intelligence, ECAI'94, pages 105\u2013109. Wiley, 1994."},{"key":"31_CR27","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0743-1066(91)90015-H","volume":"11","author":"M. Ghallab","year":"1991","unstructured":"M. Ghallab and E. Escalada-Imaz. A linear control algorithm for a class of rule-based systems. Journal of Logic Programming, 11:117\u2013132, 1991.","journal-title":"Journal of Logic Programming"},{"key":"31_CR28","unstructured":"A. Goerdt. A treshold for unsatifiability. In I.M. Havel and V. Koubek, editors, Proceedings of Mathematical Foundations of Computer Science, MFCS'92, pages 264\u2013272, August 1994."},{"key":"31_CR29","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/0166-218X(85)90068-X","volume":"12","author":"P. Hansen","year":"1985","unstructured":"P. Hansen and B. Jaumard. Uniquely solvable quadratic boolean equations. Discrete Applied Mathematics, 12:147\u2013154, 1985.","journal-title":"Discrete Applied Mathematics"},{"key":"31_CR30","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0304-3975(94)90015-9","volume":"124","author":"J.-J. Hebrard","year":"1994","unstructured":"J.-J. Hebrard. A linear algorithm for renaming a set of clauses as a Horn set. Theoretical Computer Science, 124:343\u2013350, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"31_CR31","doi-asserted-by":"publisher","first-page":"590","DOI":"10.1145\/321850.321857","volume":"21","author":"L. Henschen","year":"1974","unstructured":"L. Henschen and L. Wos. Unit refutations and Horn sets. JACM, 21(4):590\u2013605, October 1974.","journal-title":"JACM"},{"key":"31_CR32","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0743-1066(93)90018-C","volume":"15","author":"J.N. Hooker","year":"1993","unstructured":"J.N. Hooker. Solving the Incremental Satisfiability Problem. Journal of Logic Programming, 15:177\u2013186, 1993.","journal-title":"Journal of Logic Programming"},{"key":"31_CR33","first-page":"41","volume":"2","author":"S. Jeannicot","year":"1988","unstructured":"S. Jeannicot, L. Oxusoff, and A. Rauzy. \u00c9valuation S\u00e9mantique en Calcul Propositionnel. Revue d'Intelligence Artificielle, 2:41\u201360, 1988.","journal-title":"Revue d'Intelligence Artificielle"},{"key":"31_CR34","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R.J. Jeroslow","year":"1990","unstructured":"R.J. Jeroslow and J. Wang. Solving Propositional Satisfiability Problems. Annals of Mathematics and Artificial Intelligence, 1:167\u2013188, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"31_CR35","doi-asserted-by":"crossref","unstructured":"D.S. Johnson. A Catalog of Complexity Classes. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume A. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88071-0.50007-2"},{"key":"31_CR36","doi-asserted-by":"crossref","unstructured":"D.E. Knuth. Nested Satisfiability. Acta Informatica, 28, 1990.","DOI":"10.1007\/BF02983372"},{"issue":"1","key":"31_CR37","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee. Test Pattern Generation Using Boolean Satisfiability. IEEE Transactions on Computer-Aided Design, 11(1):4\u201315, January 1992.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"31_CR38","unstructured":"T. Larrabee and Y. Tsuji. Evidence for a satisfiability threshold for random 3cnf formulas. In H. Hirsh and al., editors, Proceedings of Spring Symposium on Artificial Intelligence and NP-Hard Problems (Stanford CA 1993), pages 112\u2013118, 1993."},{"issue":"1","key":"31_CR39","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H.R. Lewis","year":"1978","unstructured":"H.R. Lewis. Renaming a Set of Clauses as a Horn Set. JACM, 25(1):134\u2013135, 1978.","journal-title":"JACM"},{"key":"31_CR40","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0020-0190(89)90229-9","volume":"30","author":"G. Lindhorst","year":"1989","unstructured":"G. Lindhorst and F. Shahroki. On renaming a set of clauses as a Horn set. Information Processing Letters, 30:289\u2013293, 1989.","journal-title":"Information Processing Letters"},{"key":"31_CR41","unstructured":"D. Loveland. Automated Theorem Proving: A Logical Basis. North Holland, 1978."},{"key":"31_CR42","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0743-1066(93)90015-9","volume":"15","author":"E.L. Lozinskii","year":"1993","unstructured":"E.L. Lozinskii. A simple test improves checking satisfiability. Journal of Logic Programming, 15:99\u2013111, 1993.","journal-title":"Journal of Logic Programming"},{"key":"31_CR43","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(85)90096-1","volume":"21","author":"H. Mannila","year":"1985","unstructured":"H. Mannila and K. Mehlorn. A fast algorithm for renaming a set of clauses as a Horn set. Information Processing Letters, 21:269\u2013272, 1985.","journal-title":"Information Processing Letters"},{"key":"31_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","volume":"29","author":"M. Minoux","year":"1988","unstructured":"M. Minoux. LTUR: A Simplified Linear-Time Unit Resolution Algorithm for Horn Formulae and its Computer Implementation. Information Processing Letter, 29:1\u201312, 1988.","journal-title":"Information Processing Letter"},{"key":"31_CR45","unstructured":"D. Mitchell, B. Selman, and H. Levesque. Hard and Easy Distributions of SAT Problems. In Proceedings Tenth National Conference on Artificial Intelligence (AAAI'92), 1992."},{"key":"31_CR46","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","volume":"10","author":"B. Monien","year":"1985","unstructured":"B. Monien and E. Speckenmeyer. Solving Satisfiability in Less than 2n Steps. Discrete Applied Math., 10:287\u2013295, 1985.","journal-title":"Discrete Applied Math."},{"issue":"8","key":"31_CR47","first-page":"241","volume":"25","author":"R. Petreschi","year":"1991","unstructured":"R. Petreschi and B. Simeone. Experimental Comparison on 2-Satisfiability Algorithms. RAIRO Recherche Op\u00e9rationelle, 25:241\u2013264, 8 1991.","journal-title":"RAIRO Recherche Op\u00e9rationelle"},{"key":"31_CR48","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0020-0190(93)90178-C","volume":"48","author":"D. Pretolani","year":"1993","unstructured":"D. Pretolani. A linear time algorithm for unique Horn satisfiability. Information Processing Letters, 48:61\u201366, 1993.","journal-title":"Information Processing Letters"},{"key":"31_CR49","unstructured":"A. Rauzy. On the Complexity of the Davis and Putnam's Procedure on Some Polynomial Sub-Classes of SAT. Technical Report 806-94, LaBRI, URA CNRS 1304, Universit\u00e9 Bordeauxl, 9 1994."},{"key":"31_CR50","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0743-1066(90)90026-2","volume":"8","author":"M.G. Scutella","year":"1990","unstructured":"M.G. Scutella. A Note on Dowling and Gallier's Top-Down Algorithm for Propositional Horn Satisfiability. Journal of Logic Programming, 8:265\u2013273, 1990.","journal-title":"Journal of Logic Programming"},{"key":"31_CR51","unstructured":"B. Selman, H. Levesque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proceedings of the 10th National Conference on Artificial Intelligence (AAAI'92), 1992."},{"key":"31_CR52","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"R.E. Tarjan. Depth First Search and Linear Graph Algorithms. SIAM J. Comput., 1:146\u2013160, 1972.","journal-title":"SIAM J. Comput."},{"key":"31_CR53","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0166-218X(84)90081-7","volume":"8","author":"C. A. Tovey","year":"1984","unstructured":"C. A. Tovey. A Simplified NP-complete Satisfiability Problem. Discrete Applied Mathematics, 8:85\u201389, 1984.","journal-title":"Discrete Applied Mathematics"},{"key":"31_CR54","unstructured":"A. van Gelder. Linear Time Unit Resolution for Propositional Formulas \u2014 in Prolog, Yet. submitted to the Journal of Logic Programming, 1994."},{"key":"31_CR55","first-page":"1","volume":"59","author":"S. Yamasaki","year":"1983","unstructured":"S. Yamasaki and S. Doshita. The satisfiability problem for a class consisting of horn sentences and some non-horn sentences in propositional logic. Information and Computation, 59:1\u201312, 1983.","journal-title":"Information and Computation"},{"key":"31_CR56","unstructured":"R. Zabih and D. Mac Allester. A rearrangement search strategy for determining propositional satisfiability. In Proceedings of the National Conference on Artificial Intelligence, AAAI'88, pages 155\u2013160, 1988."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2014 CP '95"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60299-2_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:57:58Z","timestamp":1605628678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60299-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602996","9783540447887"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/3-540-60299-2_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}