{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,16]],"date-time":"2025-12-16T12:50:25Z","timestamp":1765889425467,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031765537"},{"type":"electronic","value":"9783031765544"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_16","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:18:23Z","timestamp":1731410303000},"page":"279-287","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["PyQBF: A Python Framework for\u00a0Solving Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-5751-9975","authenticated-orcid":false,"given":"Mark","family":"Peyrer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7297-6000","authenticated-orcid":false,"given":"Maximilian","family":"Heisinger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-4494","authenticated-orcid":false,"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified Boolean formulas. In: Handbook of Satisfiability, pp. 1177\u20131221. IOS Press (2021)","DOI":"10.3233\/FAIA201015"},{"key":"16_CR2","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Bloqqer: blocked clause elimination for QBF (2015). https:\/\/fmv.jku.at\/bloqqer\/"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.S., Janota, M., Klieber, W.: On conflicts and strategies in QBF. LPAR 35, 28\u201341 (2015)","DOI":"10.29007\/4sk1"},{"key":"16_CR4","unstructured":"Chollet, F., et\u00a0al.: Keras. https:\/\/keras.io (2015)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Garcia-Contreras, I., Govind, V.K.H., Shoham, S., Gurfinkel, A.: Fast approximations of\u00a0quantifier elimination. In: Enea, C., Lal, A. (eds.) CAV 2023, Part II, pp. 64\u201386. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_4","DOI":"10.1007\/978-3-031-37703-7_4"},{"key":"16_CR7","unstructured":"Gario, M., Micheli, A.: Pysmt: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop 2015 (2015)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Harris, C.R., et al.: Array programming with Numpy. Nature 585(7825), 357\u2013362 (2020)","DOI":"10.1038\/s41586-020-2649-2"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Heisinger, M., Heisinger, S., Seidl, M.: Booleguru, the\u00a0propositional polyglot (short paper). In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024, Part I, pp. 315\u2013324. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_19","DOI":"10.1007\/978-3-031-63498-7_19"},{"key":"16_CR10","unstructured":"Heisinger, M., Seidl, M., Biere, A.: QuAPI: adding assumptions to non-assuming sat & qbf solvers. In: PAAR@ IJCAR (2022)"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 428\u2013437. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_26","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"16_CR12","unstructured":"Jakob, W.: Nanobind: tiny and efficient C++\/Python bindings (2022). https:\/\/github.com\/wjakob\/nanobind"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Janota, M.: Towards generalization in qbf solving via machine learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a032 (2018)","DOI":"10.1609\/aaai.v32i1.12208"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2016.01.004","volume":"234","author":"M Janota","year":"2016","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1\u201325 (2016)","journal-title":"Artif. Intell."},{"key":"16_CR15","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. In: Workshops at the Thirtieth AAAI Conference on Artificial Intelligence (2016)"},{"issue":"2\u20133","key":"16_CR16","doi-asserted-by":"publisher","first-page":"71","DOI":"10.3233\/SAT190077","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DEPQBF: a dependency-aware QBF solver. J. Satisfiabil. Boolean Model. Comput. 7(2\u20133), 71\u201376 (2010)","journal-title":"J. Satisfiabil. Boolean Model. Comput."},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 180\u2013208 (2019). https:\/\/doi.org\/10.1613\/JAIR.1.11529","DOI":"10.1613\/JAIR.1.11529"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Peyrer, M., Heisinger, M., Seidl, M.: PyQBF: a python framework for solving quantified boolean formulas (2024). https:\/\/doi.org\/10.5281\/zenodo.13341211","DOI":"10.5281\/zenodo.13341211"},{"key":"16_CR19","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1016\/j.artint.2019.04.002","volume":"274","author":"L Pulina","year":"2019","unstructured":"Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEval 2016 and QBFEval 2017). Artif. Intell. 274, 224\u2013248 (2019)","journal-title":"Artif. Intell."},{"key":"16_CR20","unstructured":"Pulina, L., Seidl, M., Heisinger, S.: QBFGallery (2023). https:\/\/qbf23.pages.sai.jku.at\/gallery\/"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: Caqe: a certifying QBF solver. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 136\u2013143. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified boolean formulas. In: 31st International Conference on Tools with Artificial Intelligence (ICTAI), pp. 78\u201384 (2019)","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Shukla, A., M\u00f6hle, S., Kauers, M., Seidl, M.: OuterCount: a first-level solution-counter for\u00a0quantified Boolean formulas. In: Buzzard, K., Kutsia, T. (eds.) CICM 2022, pp. 272\u2013284. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_19","DOI":"10.1007\/978-3-031-16681-5_19"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:36Z","timestamp":1737200316000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}