{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:39:47Z","timestamp":1725493187456},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441908"},{"type":"electronic","value":"9783540457572"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45757-7_25","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T17:50:39Z","timestamp":1192902639000},"page":"296-307","source":"Crossref","is-referenced-by-count":16,"title":["Dependent and Independent Variables in Propositional Satisfiability"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Biere et al., 1999. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 99), 1999.","DOI":"10.21236\/ADA360973"},{"key":"25_CR2","unstructured":"Buro and Buning, 1992. M. Buro and H. Buning. Report on a SAT competition. Technical Report 110, University of Paderborn, Germany, November 1992."},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Cimatti et al., 2002a. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An opensource tool for symbolic model checking. In Proc. CAV, 2002. To appear.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"25_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/3-540-45988-X_5","volume-title":"Integrating BDD-based and SAT-based symbolic model checking","author":"A. Cimatti","year":"2002","unstructured":"Cimatti et al., 2002b. A. Cimatti, E. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. Integrating BDD-based and SAT-based symbolic model checking. In A. Armando, editor, Proceedings of the 4rd International Workshop on Frontiers of Combining Systems (FroCoS 2002), volume 2309 of Lecture Notes in Computer Science, pages 49\u201356. Springer-Verlag, 2002."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Copty et al., 2001. Fady Copty, Limor Fix, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, and Moshe Vardi. Benefits of bounded model checking at an industrial setting. In Proc. 13th International Computer Aided Verification Conference (CAV), 2001.","DOI":"10.1007\/3-540-44585-4_43"},{"key":"25_CR6","unstructured":"Crawford and Baker, 1994. James M. Crawford and Andrew B. Baker. Experimental results on the application of satisfiability algorithms to scheduling problems. In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI-94), volume 2, pages 1092\u20131097, Seattle, Washington, USA, August 1994. AAAI Press\/MIT Press."},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Davis et al., 1962. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.","DOI":"10.1145\/368273.368557"},{"key":"25_CR8","unstructured":"Dubois and Dequen, 2001. Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In Bernhard Nebel, editor, Proceedings of the seventeenth International Conference on Artificial Intelligence (IJCAI-01), pages 248\u2013253, San Francisco, CA, August 4\u201310 2001. Morgan Kaufmann Publishers, Inc."},{"key":"25_CR9","unstructured":"Ernst et al., 1997. Michael Ernst, Todd Millstein, and Daniel Weld. Automatic SATcompilation of planning problems. In Proc. IJCAI-97, 1997."},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Giunchiglia and Sebastiani, 1999. E. Giunchiglia and R. Sebastiani. Applying the Davis-Putnam procedure to non-clausal formulas. In Evelina Lamma and Paola Mello, editors, Proceedings of AI*IA\u201999: Advances in Artificial Intelligence, LNAI 2175, pages 84\u201394. Springer Verlag, 1999.","DOI":"10.1007\/3-540-46238-4_8"},{"key":"25_CR11","unstructured":"Giunchiglia et al., 1998. E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the rest will follow: Exploiting determinism in planning as satisfiability. In Proc. AAAI, 1998."},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Giunchiglia et al., 2001. Enrico Giunchiglia, Marco Maratea, Armando Tacchella, and Davide Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Proc. of the International Joint Conference on Automated Reasoning (IJCAR\u20192001), LNAI 2083, 2001.","DOI":"10.1007\/3-540-45744-5_26"},{"key":"25_CR13","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"J. 1990","year":"1990","unstructured":"Jeroslow and Wang, 1990. 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":"25_CR14","unstructured":"Kautz and Selman, 1998. Henry Kautz and Bart Selman. BLACKBOX: A new approach to the application of theorem proving to problem solving. In Working notes of the Workshop on Planning as Combinatorial Search, held in conjunction with AIPS-98, 1998."},{"key":"25_CR15","unstructured":"Li and Anbulagan, 1997. Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pages 366\u2013371, San Francisco, August 23\u201329 1997. Morgan Kaufmann Publishers."},{"key":"25_CR16","unstructured":"Li, 2000. Chu Min Li. Integrating equivalence reasoning into Davis-Putnam procedure. In Proc. AAAI, 2000."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Massacci and Marraro, 2000. Massacci and Marraro. Logical cryptanalysis as a SAT problem. JAR: Journal of Automated Reasoning, 24, 2000.","DOI":"10.1023\/A:1006326723002"},{"key":"25_CR18","unstructured":"Moore and McCabe, 1993. D. S. Moore and G. P. McCabe. Introduction to the Practice of Statistics. W. H. Freeman and Co., 1993."},{"key":"25_CR19","unstructured":"Pretolani, 1993. Daniele Pretolani. Satisfiability and Hypergraphs. PhD thesis, Universit\u00e0 di Pisa, 1993."},{"key":"25_CR20","unstructured":"Selman et al., 1997. Bart Selman, Henry Kautz, and David McAllester. Ten challenges in propositional reasoning and search. In Proc. IJCAI-97, pages 50\u201354, 1997."},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Shtrichman, 2000. O. Shtrichman. Tuning SAT checkers for bounded model-checking. In Proc. 12th International Computer Aided Verification Conference (CAV), 2000.","DOI":"10.1007\/10722167_36"},{"issue":"4","key":"25_CR22","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"U. 1995","year":"1995","unstructured":"Urquhart, 1995. Alasdair Urquhart. The complexity of propositional proofs. The Bulletin of Symbolic Logic, 1(4):425\u2013467, December 1995.","journal-title":"The Bulletin of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45757-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:07:50Z","timestamp":1556921270000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45757-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441908","9783540457572"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-45757-7_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}