{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:22Z","timestamp":1725557902387},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250517"},{"type":"electronic","value":"9783540322542"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32254-2_4","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T19:16:54Z","timestamp":1277234214000},"page":"46-58","source":"Crossref","is-referenced-by-count":4,"title":["SAT-Based Decision Procedures for Automated Reasoning: A Unifying Perspective"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[]},{"given":"Claudio","family":"Castellini","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Armando, A., Giunchiglia, F.: On tautology decision techniques: Complexity and implementation considerations. Technical Report 8911-08, IRST, Trento, Italy (1989)"},{"issue":"3\u20134","key":"4_CR2","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/BF01530803","volume":"8","author":"A. Armando","year":"1993","unstructured":"Armando, A., Giunchiglia, E.: Embedding Complex Decision Procedures inside an Interactive Theorem Prover. Annals of Mathematics and Artificial Intelligence\u00a08(3\u20134), 475\u2013502 (1993)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"Recent Advances in AI Planning","author":"A. Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"key":"4_CR4","first-page":"203","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI 1997\/IAAI 1997)","author":"R.J. Bayardo Jr.","year":"1997","unstructured":"Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI 1997\/IAAI 1997), Menlo Park, July 27\u201331, pp. 203\u2013208. AAAI Press, Menlo Park (1997)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M. B\u00f6hm","year":"1996","unstructured":"B\u00f6hm, M., Speckenmeyer, E.: A fast parallel SATsolver \u2013 efficient workload balancing. Annals of Mathematics and Artificial Intelligence\u00a017, 381\u2013400 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"4_CR7","unstructured":"Buro, M., Buning, H.: Report on a SAT competition. Technical Report 110, University of Paderborn, Germany (November 1992)"},{"key":"4_CR8","unstructured":"Castellini, C., Giunchiglia, E., Tacchella, A.: Improvements to sat-based conformant planning. In: ECP (2001)"},{"key":"4_CR9","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic \u2013 an Introduction","author":"B.F. Chellas","year":"1980","unstructured":"Chellas, B.F.: Modal Logic \u2013 an Introduction. Cambridge University Press, Cambridge (1980)"},{"key":"4_CR10","unstructured":"Chleq, N.: Efficient algorithms for networks of quantitative temporal constraints. In: Proceedings of CONSTRAINTS 1995, pp. 40\u201345 (April 1995)"},{"key":"4_CR11","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1998","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.R.: Introduction to Algorithms. MIT Press, Cambridge (1998)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"4_CR13","volume-title":"The Decision Problem: Solvable Classes of Quantificational Formulas","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., Goldfarb, W.D.: The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley Publishing Company, Reading (1979)"},{"volume-title":"SAT2000. Highlights of Satisfiability Research in the Year 2000","year":"2000","key":"4_CR14","unstructured":"Gent, I., Van Maaren, H., Walsh, T. (eds.): SAT2000. Highlights of Satisfiability Research in the Year 2000. IOS Press, Amsterdam (2000)"},{"key":"4_CR15","series-title":"LNAI","volume-title":"Automated Deduction - Cade-13","author":"F. Giunchiglia","year":"1996","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104. Springer, Heidelberg (1996)"},{"key":"#cr-split#-4_CR16.1","unstructured":"Giunchiglia, F., Sebastiani, R.: A SAT-based decision procedure for ALC. In: Proc. of the 5th International Conference on Principles of Knowledge Representation and Reasoning - KR 1996, Cambridge, MA, USA (November 1996);"},{"key":"#cr-split#-4_CR16.2","unstructured":"Also DIST-Technical Report 9607-08 and IRST-Technical Report 9601-02"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1012380814999","volume":"33","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Tacchella, A.: A subset-matching size-bounded cache for testing satisfiability in modal logics. Annals of Mathematics and Artificial Intelligence\u00a033, 39\u201367 (2001)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"4_CR18","unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R., Tacchella, A.: More evaluation of decision procedures for modal logics. In: Sixth International Conference on Principles of Knowledge Representation and Reasoning, KR 1998 (1998)"},{"issue":"2","key":"4_CR19","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1080\/11663081.2000.10510994","volume":"10","author":"E. Giunchiglia","year":"2000","unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R., Tacchella, A.: SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation. Journal of Applied Non Classical Logics\u00a010(2), 145\u2013172 (2000)","journal-title":"Journal of Applied Non Classical Logics"},{"key":"#cr-split#-4_CR20.1","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Giunchiglia, F., Tacchella, A.: SAT-Based Decision Procedures for Classical Modal Logics. Journal of Automated Reasoning (2000) (to appear);","DOI":"10.1007\/3-540-46238-4_9"},{"key":"#cr-split#-4_CR20.2","unstructured":"Reprinted in [Gent et al., 2000]"},{"key":"4_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45744-5_26","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A., Zambonin, D.: Evaluating search heuristics and optimization techniques in propositional satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, p. 347. Springer, Heidelberg (2001)"},{"key":"4_CR22","unstructured":"Giunchiglia, E.: Planning as satisfiability with expressive action languages: Concurrency, constraints and nondeterminism. In: Seventh International Conference on Principles of Knowledge Representation and Reasoning, KR 2000 (2000)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Gu, J., Purdom, P.W., Franco, J., Wah, B.W.: Algorithms for the satisfiability (sat) problem: A survey. Satisfiability Problem: Theory and Applications, 19\u2013153 (1997)","DOI":"10.1090\/dimacs\/035\/02"},{"key":"4_CR24","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Proc. ECAI 1992, pp. 359\u2013363 (1992)"},{"key":"4_CR25","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: planning, propositional logic and stochastic search. In: Proc. AAAI 1996, pp. 1194\u20131201 (1996)"},{"key":"4_CR26","first-page":"366","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997)","author":"C.M. Li","year":"1997","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), San Francisco, August 23\u201329, pp. 366\u2013371. Morgan Kaufmann Publishers, San Francisco (1997)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (June 2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"4_CR28","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"key":"4_CR29","unstructured":"Oddi, A., Cesta, A.: Incremental forward checking for the disjunctive temporal problem. In: Proceedings of the 14th European Conference on Artificial Intelligence (.0), Berlin, pp. 108\u2013112 (2000)"},{"issue":"3","key":"4_CR30","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"Prosser, P.: Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence\u00a09(3), 268\u2013299 (1993)","journal-title":"Computational Intelligence"},{"key":"4_CR31","unstructured":"Stergiou, K., Koubarakis, M.: Backtracking algorithms for disjunctions of temporal constraints. In: Proc. AAAI (1998)"},{"key":"4_CR32","unstructured":"Wolfman, S., Weld, D.: The LPSAT-engine & its application to resource planning. In: Proc. IJCAI 1999 (1999)"},{"key":"4_CR33","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Mechanizing Mathematical Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32254-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T09:37:33Z","timestamp":1559209053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32254-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250517","9783540322542"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32254-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}