{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:02:01Z","timestamp":1777125721932,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540441205","type":"print"},{"value":"9783540461357","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46135-3_13","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T05:59:47Z","timestamp":1179208787000},"page":"185-199","source":"Crossref","is-referenced-by-count":47,"title":["Recovering and Exploiting Structural Knowledge from CNF Formulas"],"prefix":"10.1007","author":[{"given":"Richard","family":"Ostrowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9ric","family":"Gr\u00e9goire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Mazure","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lakhdar","family":"Sa\u00efs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"13_CR1","unstructured":"First international competition and symposium on satisfiability testing, March 1996. Beijing (China)."},{"key":"13_CR2","unstructured":"Yacine Boufkhad and Olivier Roussel. Redundancy in random sat formulas. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI\u201900), pages 273\u2013278, 2000."},{"key":"13_CR3","unstructured":"Ronen I. Brafman. A simplifier for propositional formulas with many binary clauses. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI\u201901), 2001."},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Journal of the Association for Computing Machinery, 5:394\u2013397, 1962.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201\u2013215, 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"13_CR6","unstructured":"Second Challenge on Satisfiability Testing organized by the Center for Discrete Mathematics and Computer Science of Rutgers University, 1993. http:\/\/dimacs.rutgers.edu\/Challenges\/ ."},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Olivier Dubois, Pascal Andr\u00e9, Yacine Boufkhad, and Jacques Carlier. Sat versus unsat. In D. S. Johnson and M. A. Trick, editors, Second DIMACS Challenge, DIMACS Series in Discrete Mathematics and Theorical Computer Science, American Mathematical Society, pages 415\u2013436, 1996.","DOI":"10.1090\/dimacs\/026\/20"},{"key":"13_CR8","unstructured":"Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-sat formulae. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI\u201901), volume 1, pages 248\u2013253, Seattle, Washington (USA), August 4\u201310 2001."},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0003-4843(76)90020-6","volume":"10","author":"B. Dunham","year":"1976","unstructured":"B. Dunham and H. Wang. Towards feasible solution of the tautology problem. Annals of Mathematical Logic, 10:117\u2013154, 1976.","journal-title":"Annals of Mathematical Logic"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Proceedings of International Joint Conference on Automated Reasoning (IJCAR\u201901), Siena, June 2001.","DOI":"10.1007\/3-540-45744-5_26"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R. G. Jeroslow","year":"1990","unstructured":"Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167\u2013187, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"13_CR12","unstructured":"Henry A. Kautz, David McAllester, and Bart Selman. Exploiting variable dependency in local search. In Abstract appears in \u201dAbstracts of the Poster Sessions of IJCAI-97\u201d, Nagoya (Japan), 1997."},{"key":"13_CR13","unstructured":"Oliver Kullmann. Worst-case analysis, 3-sat decision and lower bounds: Approaches for improved sat algorithms. In DIMACS Proceedings SAT Workshop, DIMACS Series in Discrete Mathematics and Theorical Computer Science, American Mathematical Society, 1996."},{"key":"13_CR14","unstructured":"Oliver Kullmann. New methods for 3-sat decision and worst-case analysis. Theoretical Computer Science, pages 1\u201372, 1997."},{"key":"13_CR15","unstructured":"J\u00e9rome Lang and Pierre Marquis. Complexity results for independence and definability in propositional logic. In Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR\u201998), pages 356\u2013367, Trento, 1998."},{"key":"13_CR16","volume-title":"Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001)","author":"D. Berre Le","year":"2001","unstructured":"Daniel Le Berre. Exploiting the real power of unit propagation lookahead. In Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001), Boston University, Massachusetts, USA, June 14th\u201315th 2001."},{"key":"13_CR17","unstructured":"Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI\u201997), pages 366\u2013371, Nagoya (Japan), August 1997."},{"key":"13_CR18","unstructured":"C. M. Li. Integrating equivalency reasoning into davis-putnam procedure. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI\u201900), pages 291\u2013296, 2000."},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Joao P. Marques-Silva. Algebraic simplification techniques for propositional satisfiability. In Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP\u20192000), September 2000.","DOI":"10.1007\/3-540-45349-0_45"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Shtrichman Oler. Tuning sat checkers for bounded model checking. In Proceedings of Computer Aided Verification (CAV\u201900), 2000.","DOI":"10.1007\/10722167_36"},{"key":"13_CR21","unstructured":"Antoine Rauzy, Lakhdar Sa\u00efs, and Laure Brisoux. Calcul propositionnel: vers une extension du formalisme. In Actes des Cinqui\u00e8mes Journ\u00e9es Nationales sur la R\u00e9solution Pratique de Probl\u00e8mes NP-complets (JNPC\u201999), pages 189\u2013198, Lyon, 1999."},{"key":"13_CR22","unstructured":"Workshop on theory and applications of satisfiability testing, 2001. http:\/\/www.cs.washington.edu\/homes\/kautz\/sat2001\/ ."},{"key":"13_CR23","unstructured":"Fifth international symposium on the theory and applications of satisfiability testing, May 2002. http:\/\/gauss.ececs.uc.edu\/Conferences\/SAT2002\/ ."},{"key":"13_CR24","unstructured":"Bart Selman, Henry A. Kautz, and David A. McAllester. Computational challenges in propositional reasoning and search. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI\u201997), volume 1, pages 50\u201354, Nagoya (Japan), August 1997."},{"key":"13_CR25","unstructured":"A. Van Gelder. Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution. Annals of Mathematics and Artificial Intelligence, 2002. to appear."},{"issue":"3\u20135","key":"13_CR26","first-page":"81","volume":"23","author":"J. P. Warners","year":"1999","unstructured":"Joost P. Warners and Hans van Maaren. A two phase algorithm for solving a class of hard satisfiability problems. Operations Research Letters, 23(3\u20135):81\u201388, 1999.","journal-title":"Operations Research Letters"},{"key":"13_CR27","unstructured":"L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proceedigns of ICCAD\u20192001, pages 279\u2013285, San Jose, CA (USA), November 2001."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming - CP 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46135-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T00:25:41Z","timestamp":1556411141000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46135-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441205","9783540461357"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-46135-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002]]}}}