{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:46:20Z","timestamp":1742913980799,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031712937"},{"type":"electronic","value":"9783031712944"}],"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-71294-4_4","type":"book-chapter","created":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:03:47Z","timestamp":1725631427000},"page":"64-81","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Binary Implication Hypergraphs for\u00a0the\u00a0Representation and\u00a0Simplification of\u00a0Propositional Formulae"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-6608-4051","authenticated-orcid":false,"given":"Jordina","family":"Franc\u00e8s de Mas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,7]]},"reference":[{"key":"4_CR1","unstructured":"Anders, M.: SAT preprocessors and symmetry. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, Haifa, Israel, 2\u20135 August 2022. LIPIcs, vol.\u00a0236, pp. 1:1\u20131:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.1"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121\u2013123 (1979). https:\/\/doi.org\/10.1016\/0020-0190(79)90002-4","DOI":"10.1016\/0020-0190(79)90002-4"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Ausiello, G., Laura, L.: Directed hypergraphs: introduction and fundamental algorithms - a survey. Theor. Comput. Sci. 658, 293\u2013306 (2017). https:\/\/doi.org\/10.1016\/j.tcs.2016.03.016","DOI":"10.1016\/j.tcs.2016.03.016"},{"key":"4_CR4","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Dechter, R., Kearns, M.J., Sutton, R.S. (eds.) Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence, Edmonton, Alberta, Canada, July 28 - August 1, 2002, pp. 613\u2013619. AAAI Press \/ The MIT Press (2002). http:\/\/www.aaai.org\/Library\/AAAI\/2002\/aaai02-092.php"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-63385-5_28","volume-title":"Computational Logic and Proof Theory","author":"L Bachmair","year":"1997","unstructured":"Bachmair, L.: Paramodulation, superposition, and simplification. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol. 1289, pp. 1\u20133. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63385-5_28"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Berre, D.L.: Exploiting the real power of unit propagation lookahead. Electron. Notes Discret. Math. 9, 59\u201380 (2001). https:\/\/doi.org\/10.1016\/S1571-0653(04)00314-2","DOI":"10.1016\/S1571-0653(04)00314-2"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing in SAT solving. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 391\u2013435. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200992","DOI":"10.3233\/FAIA336"},{"key":"4_CR8","unstructured":"Dau, F.: Mathematical logic with diagrams \u2013 based on the existential graphs of Peirce. Habilitation thesis. TU Darmstadt, Germany (2008). http:\/\/www.dr-dau.net\/Papers\/habil.pdf"},{"issue":"3","key":"4_CR9","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (JACM) 7(3), 201\u2013215 (1960)","journal-title":"J. ACM (JACM)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_5"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-72788-0_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"N E\u00e9n","year":"2007","unstructured":"E\u00e9n, N., Mishchenko, A., S\u00f6rensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272\u2013286. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72788-0_26"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Franc\u00e8s de Mas, J., Bowles, J.: A novel EGs-based framework for systematic propositional-formula simplification. In: Gl\u00fcck, R., Kafle, B. (eds.) Logic-Based Program Synthesis and Transformation, pp. 169\u2013187. Springer, Cham (2023). https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-45784-5_11","DOI":"10.1007\/978-3-031-45784-5_11"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Gallo, G., Longo, G., Pallottino, S., Nguyen, S.: Directed hypergraphs and applications. Discrete Appl. Math. 42(2), 177\u2013201 (1993). https:\/\/www.sciencedirect.com\/science\/article\/pii\/0166218X9390045P","DOI":"10.1016\/0166-218X(93)90045-P"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Haaswijk, W., Soeken, M., Mishchenko, A., Micheli, G.D.: SAT-based exact synthesis: encodings, topology families, and parallelism. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(4), 871\u2013884 (2020). https:\/\/doi.org\/10.1109\/TCAD.2019.2897703","DOI":"10.1109\/TCAD.2019.2897703"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F.: Alembic: an efficient algorithm for CNF preprocessing. In: Proceedings of the 44th Design Automation Conference, DAC 2007, San Diego, CA, USA, 4\u20138 June 2007, pp. 582\u2013587. IEEE (2007). https:\/\/doi.org\/10.1145\/1278480.1278628","DOI":"10.1109\/DAC.2007.375231"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-16242-8_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Heule","year":"2010","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 357\u2013371. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_26"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-21581-0_17","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"MJH Heule","year":"2011","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 201\u2013215. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_17"},{"issue":"2140","key":"4_CR18","doi-asserted-by":"publisher","first-page":"20180034","DOI":"10.1098\/rsta.2018.0034","volume":"377","author":"M Kinyon","year":"2019","unstructured":"Kinyon, M.: Proof simplification and automated theorem proving. Phil. Trans. R. Soc. A 377(2140), 20180034 (2019)","journal-title":"Phil. Trans. R. Soc. A"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Kulikov, A.S.: Improving circuit size upper bounds using SAT-solvers. In: Madsen, J., Coskun, A.K. (eds.) 2018 Design, Automation & Test in Europe Conference & Exhibition, DATE 2018, Dresden, Germany, 19\u201323 March 2018, pp. 305\u2013308. IEEE (2018). https:\/\/doi.org\/10.23919\/DATE.2018.8342026","DOI":"10.23919\/DATE.2018.8342026"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Lynce, I., Silva, J.P.M.: Probing-based preprocessing techniques for propositional satisfiability. In: 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2003), Sacramento, California, USA, 3\u20135 November 2003, p.\u00a0105. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/TAI.2003.1250177","DOI":"10.1109\/TAI.2003.1250177"},{"key":"4_CR21","unstructured":"MiniZinc: a high-level constraint modelling language that allows you to easily express and solve discrete optimisation problems. https:\/\/www.minizinc.org\/. Accessed 18 May 2024"},{"key":"4_CR22","unstructured":"Peirce, C.: Existential graphs: manuscript 514, with commentary by JF Sowa. Self-published by JF Sowa [online] (1909). http:\/\/www.jfsowa.com\/peirce\/ms514.htm"},{"key":"4_CR23","unstructured":"Piette, C., Hamadi, Y., Sais, L.: Vivifying propositional clausal formulae. In: Ghallab, M., et\u00a0al. (eds.) ECAI 2008 - 18th European Conference on Artificial Intelligence, Patras, Greece, 21\u201325 July 2008, Proceedings. Frontiers in Artificial Intelligence and Applications, vol.\u00a0178, pp. 525\u2013529. IOS Press (2008). https:\/\/doi.org\/10.3233\/978-1-58603-891-5-525"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Reger, G.: Better proof output for Vampire. In: Kov\u00e1cs, L., Voronkov, A. (eds.) Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, 2 July 2016. EPiC Series in Computing, vol.\u00a044, pp. 46\u201360. EasyChair (2016). https:\/\/doi.org\/10.29007\/5dmz","DOI":"10.29007\/5dmz"},{"key":"4_CR25","unstructured":"Roberts, D.D.: The existential graphs of Charles S. Peirce. Ph.D. thesis, University of Illinois at Urbana-Champaign (1963)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Roberts, D.D.: The Existential Graphs of Charles S. Peirce. Mouton (1973)","DOI":"10.1515\/9783110226225"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Shin, S.: Reconstituting beta graphs into an efficacious system. J. Log. Lang. Inf. 8(3), 273\u2013295 (1999). https:\/\/doi.org\/10.1023\/A:1008303204427","DOI":"10.1023\/A:1008303204427"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Soeken, M., et al.: Practical exact synthesis. In: Madsen, J., Coskun, A.K. (eds.) 2018 Design, Automation & Test in Europe Conference & Exhibition, DATE 2018, Dresden, Germany, 19\u201323 March 2018, pp. 309\u2013314. IEEE (2018). https:\/\/doi.org\/10.23919\/DATE.2018.8342027","DOI":"10.23919\/DATE.2018.8342027"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24"},{"issue":"186","key":"4_CR30","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1515\/semi.2011.060","volume":"2011","author":"JF Sowa","year":"2011","unstructured":"Sowa, J.F.: Peirce\u2019s tutorial on existential graphs. Semiotica 2011(186), 347\u2013394 (2011)","journal-title":"Semiotica"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-662-52993-5_8","volume-title":"Fast Software Encryption","author":"K Stoffelen","year":"2016","unstructured":"Stoffelen, K.: Optimizing S-Box implementations for several criteria using SAT solvers. In: Peyrin, T. (ed.) FSE 2016. LNCS, vol. 9783, pp. 140\u2013160. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-52993-5_8"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Thakur, M., Tripathi, R.: Linear connectivity problems in directed hypergraphs. Theor. Comput. Sci. 410(27-29), 2592\u20132618 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.02.038","DOI":"10.1016\/j.tcs.2009.02.038"},{"key":"4_CR33","unstructured":"The Coq Development Team: The Coq reference manual \u2014 release 8.18.0 (2023). https:\/\/coq.inria.fr\/doc\/"},{"key":"4_CR34","unstructured":"Vampire: an automatic theorem prover for first-order classical logic. https:\/\/vprover.github.io\/. Accessed 18 May 2024"},{"key":"4_CR35","unstructured":"Zeman, J.J.: The graphical logic of C. S. Peirce. Ph.D. thesis, The University of Chicago (1964)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71294-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:04:18Z","timestamp":1725631458000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71294-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031712937","9783031712944"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71294-4_4","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":"7 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/?page_id=63#lopstrppdp2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}