{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,16]],"date-time":"2025-12-16T12:49:02Z","timestamp":1765889342340,"version":"3.40.5"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Recent approaches on verification and reasoning solve SAT and QBF encodings using state-of-the-art SMT solvers, as it \u201cmakes implementation much easier\u201d. The ease-of-use of these solvers make SAT and QBF solvers less visible to users of solvers\u2014who are maybe from different research communities\u2014potentially not exploiting the power of state-of-the-art tools. In this work, we motivate the need to build bridges over the widening solver-gap and introduce <jats:sc>Booleguru<\/jats:sc>, a tool to convert between formats for logic formulas. It makes SAT and QBF solvers more accessible by using techniques known from SMT solvers, such as advanced Python interfaces like Z3Py and easily generatable languages like SMT-LIB, integrating them to our conversion tool. We then introduce a language to manipulate and combine multiple formulas, optionally applying transformations for quickly prototyping encodings. <jats:sc>Booleguru<\/jats:sc>\u2019s advanced scripting capabilities form a programming environment specialized for Boolean logic, offering a more efficient way to develop novel problem encodings.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_19","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"315-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Booleguru, the\u00a0Propositional Polyglot (Short Paper)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7297-6000","authenticated-orcid":false,"given":"Maximilian","family":"Heisinger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7630-2791","authenticated-orcid":false,"given":"Simone","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,7,1]]},"reference":[{"key":"19_CR1","unstructured":"Amendola, G., Ricca, F., Truszczynski, M.: A generator of hard 2QBF formulas and ASP programs. In: Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (2018)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"19_CR3","unstructured":"Barret, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6, May 2021. www.SMT-LIB.org"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-80223-3_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"O Beyersdorff","year":"2021","unstructured":"Beyersdorff, O., Pulina, L., Seidl, M., Shukla, A.: QBFFam: a tool for generating QBF families from proof complexity. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 21\u201329. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_3"},{"key":"19_CR5","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report\u00a011\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/LRA.2023.3280830","volume":"8","author":"E Bonnah","year":"2023","unstructured":"Bonnah, E., Nguyen, L., Hoque, K.A.: Motion planning using hyperproperties for time window temporal logic. IEEE Robot. Autom. Lett. 8, 1\u20138 (2023)","journal-title":"IEEE Robot. Autom. Lett."},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"19_CR8","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":"19_CR9","doi-asserted-by":"publisher","unstructured":"Hecking-Harbusch, J., Tentrup, L.: Solving QBF by abstraction. In: Electronic Proceedings in Theoretical Computer Science (2018). https:\/\/doi.org\/10.4204\/eptcs.277.7","DOI":"10.4204\/eptcs.277.7"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"Heisinger, S., Heisinger, M., Rebola-Pardo, A., Seidl, M.: Quantifier shifting for quantified boolean formulas revisited. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings. LNCS, vol. 14739, pp. 325\u2013343, Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_20","DOI":"10.1007\/978-3-031-63498-7_20"},{"key":"19_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-031-42753-4_20","volume-title":"Intelligent Computer Mathematics","author":"S Heisinger","year":"2023","unstructured":"Heisinger, S., Seidl, M.: True crafted formula families for benchmarking quantified satisfiability solvers. In: Dubois, C., Kerber, M. (eds.) CICM 2023. LNCS, vol. 14101p, pp. 291\u2013296. Springer-Verlag, Berlin, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-42753-4_20"},{"key":"19_CR12","unstructured":"Ierusalimschy, R.: Programming in Lua. Roberto Ierusalimschy (2006)"},{"key":"19_CR13","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. In: AAAI Workshop: Beyond NP. AAAI Technical report, vol. WS-16-05. AAAI Press (2016)"},{"key":"19_CR14","unstructured":"Parr, T.: The definitive ANTLR 4 reference. The Definitive ANTLR 4 Reference, pp. 1\u2013326 (2013)"},{"key":"19_CR15","unstructured":"Paszke, A., et al.: Pytorch: an imperative style, high-performance deep learning library. In: Advances in Neural Information Processing Systems, vol. 32, pp. 8024\u20138035. Curran Associates, Inc. (2019)"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Peham, T., Brandl, N., Kueng, R., Wille, R., Burgholzer, L.: Depth-optimal synthesis of Clifford circuits with SAT solvers (2023)","DOI":"10.1109\/QCE57702.2023.00095"},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Saaltink, C., Nicoletti, S.M., Volk, M., Hahn, E.M., Stoelinga, M.: Solving queries for Boolean fault tree logic via quantified sat. In: Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, pp. 48\u201359. FTSCS 2023, Association for Computing Machinery (2023). https:\/\/doi.org\/10.1145\/3623503.3623535","DOI":"10.1145\/3623503.3623535"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Schwarzov\u00e1, T., Strejcek, J., Major, J.: Reducing acceptance marks in Emerson-lei automata by QBF solving. In: 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, Alghero, Italy. LIPIcs, vol.\u00a0271, pp. 23:1\u201323:20 (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.23","DOI":"10.4230\/LIPICS.SAT.2023.23"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Seidl, M., Lonsing, F., Biere, A.: qbf2epr: a tool for generating EPR formulas from QBF. In: Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, June 30\u2013July 1, 2012. EPiC Series in Computing, vol.\u00a021, pp. 139\u2013148. EasyChair (2012). https:\/\/doi.org\/10.29007\/2B5D","DOI":"10.29007\/2B5D"},{"key":"19_CR20","doi-asserted-by":"publisher","unstructured":"The pandas development team: pandas-dev\/pandas: Pandas, February 2020. https:\/\/doi.org\/10.5281\/zenodo.3509134","DOI":"10.5281\/zenodo.3509134"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Virtanen, P., et al.: SciPy 1.0 Contributors: SciPy 1.0: Fundamental Algorithms for Scientific Computing in Python. Nature Methods, pp. 261\u2013272 (2020). https:\/\/doi.org\/10.1038\/s41592-019-0686-2","DOI":"10.1038\/s41592-019-0686-2"},{"issue":"1","key":"19_CR22","doi-asserted-by":"publisher","first-page":"221","DOI":"10.3233\/SAT190123","volume":"11","author":"T Weber","year":"2019","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019). https:\/\/doi.org\/10.3233\/SAT190123","journal-title":"J. Satisf. Boolean Model. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:30Z","timestamp":1747592250000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_19","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":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}