{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:29Z","timestamp":1740123329931,"version":"3.37.3"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T00:00:00Z","timestamp":1691020800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T00:00:00Z","timestamp":1691020800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100004663","name":"Ministry of Science and Technology, Taiwan","doi-asserted-by":"publisher","award":["MOST 111-2221-E-002-182"],"award-info":[{"award-number":["MOST 111-2221-E-002-182"]}],"id":[{"id":"10.13039\/501100004663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,9]]},"DOI":"10.1007\/s10817-023-09670-6","type":"journal-article","created":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T06:02:06Z","timestamp":1691042526000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Resolution Proof System for Dependency Stochastic Boolean Satisfiability"],"prefix":"10.1007","volume":"67","author":[{"given":"Yun-Rong","family":"Luo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Che","family":"Cheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,8,3]]},"reference":[{"key":"9670_CR1","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/j.tcs.2013.12.020","volume":"523","author":"V Balabanov","year":"2014","unstructured":"Balabanov, V., Chiang, H.-J.K., Jiang, J.-H.R.: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86\u2013100 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"9670_CR2","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L., Schmidt, R.A., Suda, M.: Lifting QBF resolution calculi to DQBF. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 490\u2013499 (2016). Springer","DOI":"10.1007\/978-3-319-40970-2_30"},{"key":"9670_CR3","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s10817-020-09560-1","volume":"65","author":"O Beyersdorff","year":"2021","unstructured":"Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Building strategies into QBF proofs. J. Autom. Reason. 65, 125\u2013154 (2021)","journal-title":"J. Autom. Reason."},{"key":"9670_CR4","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"9670_CR5","doi-asserted-by":"crossref","unstructured":"Blinkhorn, J., Peitl, T., Slivovsky, F.: Davis and Putnam meet Henkin: solving DQBF with resolution. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 30\u201346 (2021)","DOI":"10.1007\/978-3-030-80223-3_4"},{"key":"9670_CR6","doi-asserted-by":"crossref","unstructured":"Chen, P.-W., Huang, Y.-C., Jiang, J.-H.R.: A sharp leap from quantified Boolean formula to stochastic Boolean satisfiability solving. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 35, pp. 3697\u20133706 (2021)","DOI":"10.1609\/aaai.v35i5.16486"},{"key":"9670_CR7","doi-asserted-by":"crossref","unstructured":"Cheng, C., Jiang, JHR.: Lifting (D)QBF Preprocessing and Solving Techniques to (D)SSAT. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 37, pp. 3906\u20133914 (2023)","DOI":"10.1609\/aaai.v37i4.25504"},{"key":"9670_CR8","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res."},{"key":"9670_CR9","unstructured":"Fichte, JK., Hecher, M., Roland, V.: Proofs for Propositional Model Counting. 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) (2022)"},{"key":"9670_CR10","doi-asserted-by":"crossref","unstructured":"Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified Boolean formulae. In: 2013 IEEE 31st International Conference on Computer Design (ICCD), pp. 396\u2013403 (2013)","DOI":"10.1109\/ICCD.2013.6657071"},{"key":"9670_CR11","first-page":"167","volume":"30","author":"L Henkin","year":"1961","unstructured":"Henkin, L.: Some remarks on infinitely long formulas. J. Symb. Log. 30, 167\u2013183 (1961)","journal-title":"J. Symb. Log."},{"key":"9670_CR12","doi-asserted-by":"crossref","unstructured":"Heule, MJH.: Proofs of Unsatisfiability. Handbook of Satisfiability, pp. 635\u2013668. IOS Press, Amsterdam, Netherlands (2021)","DOI":"10.3233\/FAIA200998"},{"key":"9670_CR13","doi-asserted-by":"crossref","unstructured":"Hsieh, C.-H., Jiang, J.-H.R.: Encoding probabilistic graphical models into stochastic Boolean satisfiability. In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, pp. 1834\u20131842 (2022)","DOI":"10.24963\/ijcai.2022\/255"},{"key":"9670_CR14","first-page":"1","volume":"4","author":"J Johannsen","year":"2008","unstructured":"Johannsen, J., Hoffmann, J., Buss, S.R.: Resolution trees with lemmas: resolution refinements that characterize DLL algorithms with clause learning. Log. Methods Comput. Sci. 4, 1\u201318 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"9670_CR15","doi-asserted-by":"crossref","unstructured":"Lee, N.-Z., Jiang, J.-H.R.: Dependency stochastic Boolean satisfiability: A logical formalism for NEXPTIME decision problems with uncertainty. In: Proceedings of the AAAI Conference on Artificial Intelligence, pp. 3877\u20133885 (2021)","DOI":"10.1609\/aaai.v35i5.16506"},{"issue":"8","key":"9670_CR16","doi-asserted-by":"publisher","first-page":"1202","DOI":"10.1109\/TC.2018.2807431","volume":"67","author":"N-Z Lee","year":"2018","unstructured":"Lee, N.-Z., Jiang, J.-H.R.: Towards formal evaluation and verification of probabilistic design. IEEE Trans. Comput. 67(8), 1202\u20131216 (2018)","journal-title":"IEEE Trans. Comput."},{"key":"9670_CR17","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1023\/A:1017584715408","volume":"27","author":"M Littman","year":"2001","unstructured":"Littman, M., Majercik, S., Pitassi, T.: Stochastic Boolean satisfiability. J. Autom. Reason. 27, 251\u2013296 (2001)","journal-title":"J. Autom. Reason."},{"key":"9670_CR18","unstructured":"Majercik, S.M., Boots, B.: DC-SSAT: A divide-and-conquer approach to solving stochastic satisfiability problems efficiently. In: Proceedings of National Conference on Artificial Intelligence, pp. 416\u2013422 (2005)"},{"key":"9670_CR19","unstructured":"Majercik, S.M., Littman, M.L.: MAXPLAN: a new approach to probabilistic planning. In: Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems, pp. 86\u201393 (1998)"},{"issue":"1\u20132","key":"9670_CR20","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0004-3702(02)00379-X","volume":"147","author":"SM Majercik","year":"2003","unstructured":"Majercik, S.M., Littman, M.L.: Contingent planning under uncertainty via stochastic satisfiability. Artif. Intell. 147(1\u20132), 119\u2013162 (2003)","journal-title":"Artif. Intell."},{"issue":"2","key":"9670_CR21","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0022-0000(85)90045-5","volume":"31","author":"CH Papadimitriou","year":"1985","unstructured":"Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288\u2013301 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"7\u20138","key":"9670_CR22","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","volume":"41","author":"G Peterson","year":"2001","unstructured":"Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Comput. Math. Appl. 41(7\u20138), 957\u2013992 (2001)","journal-title":"Comput. Math. Appl."},{"key":"9670_CR23","doi-asserted-by":"crossref","unstructured":"Reichl, F.-X., Slivovsky, F., Szeider, S.: Certified DQBF solving by definition extraction. In: Theory and Applications of Satisfiability Testing \u2013 SAT 2021, pp. 499\u2013517 (2021)","DOI":"10.1007\/978-3-030-80223-3_34"},{"key":"9670_CR24","unstructured":"Salmon, R., Poupart, P.: On the relationship between satisfiability and Markov decision processes. In: Proceedings of The 35th Uncertainty in Artificial Intelligence Conference, vol. 115, pp. 1105\u20131115 (2020)"},{"key":"9670_CR25","doi-asserted-by":"crossref","unstructured":"Scholl, C., Wimmer, R.: Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications. Theory and Applications of Satisfiability Testing \u2013 SAT 2018, pp. 3\u201316 (2018)","DOI":"10.1007\/978-3-319-94144-8_1"},{"key":"9670_CR26","doi-asserted-by":"crossref","unstructured":"Teige, T., Fr\u00e4nzle, M.: Generalized Craig interpolation for stochastic Boolean satisfiability problems with applications to probabilistic state reachability and region stability. Log. Methods Comput. Sci. 8(2) (2012)","DOI":"10.2168\/LMCS-8(2:16)2012"},{"key":"9670_CR27","doi-asserted-by":"crossref","unstructured":"Teige, T., Fr\u00e4nzle, M.: Resolution for stochastic Boolean satisfiability. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 625\u2013639 (2010)","DOI":"10.1007\/978-3-642-16242-8_44"},{"key":"9670_CR28","doi-asserted-by":"crossref","unstructured":"Tseitin, GS.: On the Complexity of Derivation in Propositional Calculus, Automation of reasoning: 2: Classical papers on computational logic 1967\u20131970, Springer, pp. 466\u2013483 (1983)","DOI":"10.1007\/978-3-642-81955-1_28"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09670-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09670-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09670-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,18]],"date-time":"2023-12-18T10:47:26Z","timestamp":1702896446000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09670-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,3]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["9670"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09670-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,8,3]]},"assertion":[{"value":"30 November 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 May 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 August 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing financial or non-financial interests in conducting this research.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"26"}}