{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:00:10Z","timestamp":1743012010954,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031549670"},{"type":"electronic","value":"9783031549687"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-54968-7_12","type":"book-chapter","created":{"date-parts":[[2024,2,26]],"date-time":"2024-02-26T04:12:27Z","timestamp":1708920747000},"page":"133-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Implicit QBF Encodings for\u00a0Positional Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7404-348X","authenticated-orcid":false,"given":"Irfansha","family":"Shaik","sequence":"first","affiliation":[]},{"given":"Valentin","family":"Mayer-Eichberger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-0625","authenticated-orcid":false,"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9805-8291","authenticated-orcid":false,"given":"Abdallah","family":"Saffidine","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,2,27]]},"reference":[{"key":"12_CR1","unstructured":"Ansotegui, C., Gomes, C.P., Selman, B.: The Achilles\u2019 heel of QBF. In: AAAI 2005, pp. 275\u2013281 (2005). http:\/\/dl.acm.org\/citation.cfm?id=1619332.1619378"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"114","DOI":"10.3233\/ICG-2009-32218","volume":"32","author":"B Arneson","year":"2009","unstructured":"Arneson, B., Hayward, R., Henderson, P.: MoHex wins Hex tournament. ICGA J. 32(2), 114 (2009)","journal-title":"ICGA J."},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"CADE","author":"A Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjorner, N., Sofronie-Stokkermans, V. (eds.) CADE. LNCS, vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_10"},{"key":"12_CR4","unstructured":"Bonnet, \u00c9., Gaspers, S., Lambilliotte, A., R\u00fcmmele, S., Saffidine, A.: The parameterized complexity of positional games. In: ICALP 2017, pp. 90:1\u201390:14 (2017)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2016.06.033","volume":"644","author":"\u00c9 Bonnet","year":"2016","unstructured":"Bonnet, \u00c9., Jamain, F., Saffidine, A.: On the complexity of connection games. Theor. Comput. Sci. (TCS) 644, 2\u201328 (2016)","journal-title":"Theor. Comput. Sci. (TCS)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Boucher, S., Villemaire, R.: Quantified Boolean solving for achievement games. In: 44th German Conference on Artificial Intelligence (KI), pp. 30\u201343 (2021)","DOI":"10.1007\/978-3-030-87626-5_3"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Cashmore, M., Fox, M., Giunchiglia, E.: Planning as quantified Boolean formula. In: ECAI 2012, pp. 217\u2013222 (2012). https:\/\/doi.org\/10.3233\/978-1-61499-098-7-217","DOI":"10.3233\/978-1-61499-098-7-217"},{"key":"12_CR8","unstructured":"Diptarama, Yoshinaka, R., Shinohara, A.: QBF encoding of Generalized Tic-Tac-Toe. In: 4th IW on Quantified Boolean Formulas (QBF), pp. 14\u201326 (2016)"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-31866-5_23","volume-title":"ACG","author":"T Ederer","year":"2011","unstructured":"Ederer, T., Lorenz, U., Opfer, T., Wolf, J.: Modeling games with the help of quantified integer linear programs. In: van den Herik, H.J., Plaat, A. (eds.) ACG. LNCS, vol. 7168, pp. 270\u2013281. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-31866-5_23"},{"issue":"10","key":"12_CR10","doi-asserted-by":"publisher","first-page":"818","DOI":"10.1080\/00029890.1979.11994922","volume":"86","author":"D Gale","year":"1979","unstructured":"Gale, D.: The game of Hex and the Brouwer fixed-point theorem. Am. Math. Mon. 86(10), 818\u2013827 (1979)","journal-title":"Am. Math. Mon."},{"key":"12_CR11","unstructured":"Hartisch, M.: Quantified integer programming with polyhedral and decision-dependent uncertainty. Ph.D. thesis, Universit\u00e4t Siegen (2020)"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-030-65883-0_6","volume-title":"ACG","author":"M Hartisch","year":"2019","unstructured":"Hartisch, M., Lorenz, U.: A novel application for game tree search - exploiting pruning mechanisms for quantified integer programs. In: Cazenave, T., van den Herik, J., Saffidine, A., Wu, I.C. (eds.) ACG. LNCS, vol. 12516, pp. 66\u201378. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-65883-0_6"},{"key":"12_CR13","unstructured":"Hayward, R.B., Toft, B.: Hex, the full story. AK Peters\/CRC Press\/Taylor (2019)"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Hecking-Harbusch, J., Tentrup, L.: Solving QBF by abstraction. In: GandALF. EPTCS, vol. 277, pp. 88\u2013102 (2018). https:\/\/doi.org\/10.4204\/EPTCS.277.7","DOI":"10.4204\/EPTCS.277.7"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. (JAIR) 53, 127\u2013168 (2015)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-94144-8_12","volume-title":"SAT","author":"M Janota","year":"2018","unstructured":"Janota, M.: Circuit-based search space pruning in QBF. In: Beyersdorff, O., Wintersteiger, C. (eds.) SAT. LNCS, vol. 10929, pp. 187\u2013198. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_12"},{"key":"12_CR17","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. In: AAAI-16 Workshop on Beyond NP (2016)"},{"key":"12_CR18","unstructured":"Jung, J.C., Mayer-Eichberger, V., Saffidine, A.: QBF programming with the modeling language Bule. In: Proceedings SAT 2022. Schloss Dagstuhl-Leibniz (2022)"},{"issue":"3","key":"12_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. ENTCS 174(3), 45\u201356 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.12.022","journal-title":"ENTCS"},{"key":"12_CR20","unstructured":"Kautz, H.A., McAllester, D.A., Selman, B.: Encoding plans in propositional logic. In: Principles of Knowledge Representation and Reasoning (KR), pp. 374\u2013384 (1996)"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-319-63046-5_23","volume-title":"CADE","author":"F Lonsing","year":"2017","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE. LNCS, vol. 10395, pp. 371\u2013384. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_23"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-030-24258-9_14","volume-title":"SAT","author":"F Lonsing","year":"2019","unstructured":"Lonsing, F., Egly, U.: QRATPre+: effective QBF preprocessing via strong redundancy properties. In: Janota, M., Lynce, I. (eds.) SAT. LNCS, vol. 11628, pp. 203\u2013210. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_14"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Mayer-Eichberger, V., Saffidine, A.: Positional games and QBF: the corrective encoding. In: Theory and Applications of Satisfiability Testing (SAT), pp. 447\u2013463 (2020)","DOI":"10.1007\/978-3-030-51825-7_31"},{"key":"12_CR24","unstructured":"Mayer-Eichberger, V., Saffidine, A.: Positional games and QBF: a polished encoding. arXiv 2005.05098 (2023). https:\/\/doi.org\/10.48550\/arXiv.2005.05098"},{"key":"12_CR25","unstructured":"Pulina, L., Seidl, M., Shukla, A.: The 14th QBF solvers evaluation (QBFEVAL 2022) (2022). http:\/\/www.qbflib.org\/QBFEVAL22_PRES.pdf"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Proceedings FMCAD 2015, pp. 136\u2013143. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"12_CR27","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00288964","volume":"15","author":"S Reisch","year":"1981","unstructured":"Reisch, S.: Hex ist PSPACE-vollst\u00e4ndig. Acta Informatica 15, 167\u2013191 (1981)","journal-title":"Acta Informatica"},{"key":"12_CR28","unstructured":"Shaik, I.: Concise Encodings for Planning and 2-Player Games. Ph.D. thesis, Aarhus University (2023)"},{"key":"12_CR29","unstructured":"Shaik, I., Mayer-Eichberger, V., van de Pol, J., Saffidine, A.: Implicit state and goals in QBF encodings for positional games (extended version). arXiv 2301.07345 (2023). https:\/\/doi.org\/10.48550\/arXiv.2301.07345"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Shaik, I., van de Pol, J.: Classical planning as QBF without grounding. In: ICAPS, pp. 329\u2013337. AAAI Press (2022)","DOI":"10.1609\/icaps.v32i1.19817"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Shaik, I., van de Pol, J.: Concise QBF encodings for games on a grid. arXiv 2303.16949 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2303.16949","DOI":"10.48550\/ARXIV.2303.16949"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning, pp. 466\u2013483. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28"},{"issue":"1","key":"12_CR33","first-page":"3","volume":"11","author":"R Wimmer","year":"2019","unstructured":"Wimmer, R., Scholl, C., Becker, B.: The (D)QBF preprocessor HQSpre - underlying theory and its implementation. J. Satisf. Boolean Model. 11(1), 3\u201352 (2019)","journal-title":"J. Satisf. Boolean Model."}],"container-title":["Lecture Notes in Computer Science","Advances in Computer Games"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-54968-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,26]],"date-time":"2024-02-26T04:13:37Z","timestamp":1708920817000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-54968-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031549670","9783031549687"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-54968-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"27 February 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ACG","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Advances in Computer Games","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Siegen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"acg2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icga.org\/?page_id=3788","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}