{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:30Z","timestamp":1725568170495},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_7","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"75-89","source":"Crossref","is-referenced-by-count":13,"title":["Optimizing a BDD-Based Modal Solver"],"prefix":"10.1007","author":[{"given":"Guoqiang","family":"Pan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Areces, C., Gennari, R., Heguiabehere, J., de Rijke, M.: Tree-based heuristics in modal theorem proving. In: Proc. of the ECAI 2000 (2000)"},{"key":"7_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/3-540-45744-5_8","volume-title":"Automated Reasoning","author":"F. Baader","year":"2001","unstructured":"Baader, F., Tobies, S.: The inverse method implements the automata approach for modal satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 92\u2013106. Springer, Heidelberg (2001)"},{"key":"7_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal logic. Camb. Univ. Press, Cambridge (2001)"},{"issue":"8","key":"7_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. On Comp.\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. On Comp."},{"key":"7_CR5","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. Technical report, Dipartmento di Imformatica e Sistemistica, Universita de Roma (1999)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Coarfa, C., Demopoulos, D.D., San Miguel Aguirre, A., Subramanian, D., Vardi, M.Y.: Random 3-SAT: The plot thickens. In: Proc. of the Int. Conf. on Constraint Prog. (2000)","DOI":"10.1007\/3-540-45349-0_12"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Journal of the ACM"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"7_CR9","unstructured":"Gent, I., Walsh, T.: Beyond NP: The QSAT phase transition. In: AAAI: 16th National Conference on Artificial Intelligence. AAAI \/ MIT Press (1999)"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1006\/inco.1999.2850","volume":"162","author":"F. Giunchiglia","year":"2000","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from prepositional decision procedure - the case study of modal K(m). Inf. and Comp.\u00a0162, 158\u2013178 (2000)","journal-title":"Inf. and Comp."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Gupta, A., Yang, Z., Ashar, P., Zhang, L., Malik, S.: Partition-based decision heuristics for image computation using SAT and BDDs. In: ICCAD, pp. 286\u2013292 (2001)","DOI":"10.1109\/ICCAD.2001.968635"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J.Y. Halpern","year":"1992","unstructured":"Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence\u00a054, 319\u2013379 (1992)","journal-title":"Artificial Intelligence"},{"key":"7_CR13","unstructured":"Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. Technical report, Universit\u00e4t Bern, Switzerland (1996)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/10722086_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.: MSPASS: modal reasoning by translation and first order resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol.\u00a01847, pp. 67\u201371. Springer, Heidelberg (2000)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Kamhi, G., Fix, L.: Adaptive variable reordering for symbolic model checking. In: ICCAD 1998, pp. 359\u2013365 (1998)","DOI":"10.1145\/288548.289054"},{"issue":"3","key":"7_CR16","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R.E. Ladner","year":"1977","unstructured":"Ladner, R.E.: The computational complexity of provability in systems of modal prepositional logic. SIAM J. Comput.\u00a06(3), 467\u2013480 (1977)","journal-title":"SIAM J. Comput."},{"key":"7_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified Boolean formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/10722086_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"F. Massacci","year":"2000","unstructured":"Massacci, F., Donini, F.M.: Design and results of TANCS-2000. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol.\u00a01847, pp. 52\u201356. Springer, Heidelberg (2000)"},{"key":"7_CR19","volume-title":"Handbook of Automated Reasoning","author":"H.J. Ohlbach","year":"1999","unstructured":"Ohlbach, H.J., Nonnengart, A., de Rijke, M., Gabbay, D.M.: Encoding two-valued nonclassical logics in classical logic. In: Handbook of Automated Reasoning. Elsevier, Amsterdam (1999)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Pan, G.: BDD-based decision procedures for modal logic K, Master\u2019s Thesis, Rice University (2002)","DOI":"10.1007\/3-540-45620-1_2"},{"key":"7_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/3-540-45620-1_2","volume-title":"Automated Deduction - CADE-18","author":"G. Pan","year":"2002","unstructured":"Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for K. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 16\u201330. Springer, Heidelberg (2002)"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Patel-Schneider, P.F., Horrocks, I.: DLP and FaCT. In: Analytic Tableaux and Related Methods, pp. 19\u201323 (1999)","DOI":"10.1007\/3-540-48754-9_3"},{"key":"7_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/3-540-45744-5_40","volume-title":"Automated Reasoning","author":"P.F. Patel-Schneider","year":"2001","unstructured":"Patel-Schneider, P.F., Sebastiani, R.: A new system and methodology for generating random modal formulae. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 464\u2013468. Springer, Heidelberg (2001)"},{"issue":"2","key":"7_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"20","author":"V.R. Pratt","year":"1980","unstructured":"Pratt, V.R.: A near-optimal method for reasoning about action. Journal of Computer and System Sciences\u00a020(2), 231\u2013254 (1980)","journal-title":"Journal of Computer and System Sciences"},{"key":"7_CR25","first-page":"323","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Constructing conditional plans by a theorem-prover. J. of A. I. Res.\u00a010, 323\u2013352 (1999)","journal-title":"J. of A. I. Res."},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD 1993, pp. 42\u201347 (1993)","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-45578-7_9","volume-title":"Principles and Practice of Constraint Programming - CP 2001","author":"A. San Miguel Aguirre","year":"2001","unstructured":"San Miguel Aguirre, A., Vardi, M.Y.: Random 3-SAT and BDDs: The plot thickens further. In: Walsh, T. (ed.) CP 2001. LNCS, vol.\u00a02239, p. 121. Springer, Heidelberg (2001)"},{"key":"7_CR28","unstructured":"Schmidt, R.A.: Optimised Modal Translation and Resolution. PhD thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (1997)"},{"issue":"1-2","key":"7_CR29","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman, B., Mitchell, D.G., Levesque, H.J.: Generating hard satisfiability problems. Artificial Intelligence\u00a081(1-2), 17\u201329 (1996)","journal-title":"Artificial Intelligence"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 247\u2013263. Springer, Heidelberg (2000)"},{"key":"7_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L.J. Stockmeyer","year":"1977","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theo. Comp. Sci.\u00a03, 1\u201322 (1977)","journal-title":"Theo. Comp. Sci."},{"key":"7_CR32","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G. Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artificial intelligence\u00a0131, 39\u201354 (2001)","journal-title":"Artificial intelligence"},{"key":"7_CR33","unstructured":"Tacchella, A.: *SAT system description. In: Collected Papers from (DL 1999). CEUR (1999)"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","volume-title":"Algorithms and Computation","author":"S. Tani","year":"1993","unstructured":"Tani, S., Hamaguchi, K., Yajima, S.: The complexity of the optimal variable ordering problems of shared binary decision diagrams. In: Ng, K.W., Balasubramanian, N.V., Raghavan, P., Chin, F.Y.L. (eds.) ISAAC 1993. LNCS, vol.\u00a0762. Springer, Heidelberg (1993)"},{"key":"7_CR35","unstructured":"van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: What makes modal logic so robustly decidable. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models, pp. 149\u2013183. AMS (1997)","DOI":"10.1090\/dimacs\/031\/05"},{"issue":"2","key":"7_CR37","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1145\/371316.371511","volume":"2","author":"A. Voronkov","year":"2001","unstructured":"Voronkov, A.: How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Comp. Logic\u00a02(2), 182\u2013215 (2001)","journal-title":"Comp. Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,12]],"date-time":"2021-11-12T18:07:31Z","timestamp":1636740451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}