{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:41:08Z","timestamp":1742978468661,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377051"},{"type":"electronic","value":"9783031377068"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Given a specification as a Boolean relation between inputs and outputs, Boolean functional synthesis generates a function, called a Skolem function, for each output in terms of the inputs such that the specification is satisfied. In general, there may be many possibilities for Skolem functions satisfying the same specification, and criteria to pick one or the other may vary from specification to specification.<\/jats:p><jats:p>In this paper, we develop a technique to represent the space of Skolem functions in a criteria-agnostic form that makes it possible to subsequently extract Skolem functions for different criteria. Our focus is on identifying such a form and on developing a compilation algorithm for this form. Our approach is based on a novel counter-example guided strategy for existentially quantifying a subset of variables from a specification in negation normal form. We implement this technique and compare our performance with those of other knowledge compilation approaches for Boolean functional synthesis, and show promising results.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_19","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"367-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Counterexample Guided Knowledge Compilation for\u00a0Boolean Functional Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2471-5997","authenticated-orcid":false,"given":"S.","family":"Akshay","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7527-7675","authenticated-orcid":false,"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[]},{"given":"Sahil","family":"Jain","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Jacobs, S., et al.: The second reactive synthesis competition (SYNTCOMP 2015). In: Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015, pp. 27\u201357 (2015)","DOI":"10.4204\/EPTCS.202.4"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTLf synthesis. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, 19\u201325 August 2017, pp. 1362\u20131369 (2017)","DOI":"10.24963\/ijcai.2017\/189"},{"issue":"2","key":"19_CR3","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/s10009-004-0179-0","volume":"7","author":"R Alur","year":"2005","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic computational techniques for solving games. Int. J. Softw. Tools Technol. Transf. 7(2), 118\u2013128 (2005). https:\/\/doi.org\/10.1007\/s10009-004-0179-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"5\u20136","key":"19_CR4","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. STTT 15(5\u20136), 497\u2013518 (2013)","journal-title":"STTT"},{"issue":"5\u20136","key":"19_CR5","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-22110-1_12","volume-title":"Computer Aided Verification","author":"V Balabanov","year":"2011","unstructured":"Balabanov, V., Jiang, J.-H.R.: Resolution proofs and skolem functions in QBF evaluation and applications. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 149\u2013164. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_12"},{"issue":"1","key":"19_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.-H.R.: Unified QBF certification and its applications. Form. Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Niemetz","year":"2012","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430\u2013435. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_33"},{"issue":"6","key":"19_CR9","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/1809028.1806632","volume":"45","author":"V Kuncak","year":"2010","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. SIGPLAN Not. 45(6), 316\u2013329 (2010)","journal-title":"SIGPLAN Not."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Jo, S., Matsumoto, T., Fujita, M.: Sat-based automatic rectification and debugging of combinational circuits with lut insertions. In: Proceedings of the 2012 IEEE 21st Asian Test Symposium, ATS 2012, pp. 19\u201324. IEEE Computer Society (2012)","DOI":"10.1109\/ATS.2012.55"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-40970-2_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MN Rabe","year":"2016","unstructured":"Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375\u2013392. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_23"},{"key":"19_CR12","first-page":"611","volume":"12225","author":"P Golia","year":"2020","unstructured":"Golia, P., Roy, S., Meel, K.S.: Manthan: a data-driven approach for Boolean function synthesis. Comput. Aided Verificat. 12225, 611\u2013633 (2020)","journal-title":"Comput. Aided Verificat."},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Akshay, S., Arora, J., Chakraborty, S., Krishna, S., Raghunathan, D., Shah, S.: Knowledge compilation for boolean functional synthesis. In: Proceedings of of Formal Methods in Computer Aided Design (FMCAD), 2019","DOI":"10.23919\/FMCAD.2019.8894266"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10703-020-00352-2","volume":"57","author":"S Akshay","year":"2021","unstructured":"Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: Boolean functional synthesis: hardness and practical algorithms. Formal Methods Syst. Des. 57(1), 53\u201386 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-662-54577-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Akshay","year":"2017","unstructured":"Akshay, S., Chakraborty, S., John, A.K., Shah, S.: Towards parallel boolean functional synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 337\u2013353. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_19"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"John, A., Shah, S., Chakraborty, S., Trivedi, A., Akshay, S.: Skolem functions for factored formulas. In: FMCAD, pp. 73\u201380 (2015)","DOI":"10.1109\/FMCAD.2015.7542255"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Golia, P., Slivovsky, F., Roy, S., Meel, K.S.: Engineering an efficient Boolean functional synthesis engine. In: IEEE\/ACM International Conference On Computer Aided Design, ICCAD 2021, Munich, Germany, 1\u20134 November 2021, pp. 1\u20139. IEEE (2021)","DOI":"10.1109\/ICCAD51958.2021.9643583"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-41540-6_22","volume-title":"Computer Aided Verification","author":"D Fried","year":"2016","unstructured":"Fried, D., Tabajara, L.M., Vardi, M.Y.: BDD-based boolean functional synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 402\u2013421. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_22"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Factored Boolean functional synthesis. In: 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 124\u2013131 (2017)","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Shah, P., Bansal, A., Akshay, S., Chakraborty, S.: A normal form characterization for efficient boolean skolem function synthesis. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, 29 June\u20132 July 2021, pp. 1\u201313. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470741"},{"issue":"1","key":"19_CR21","first-page":"229","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Int. Res. 17(1), 229\u2013264 (2002)","journal-title":"J. Artif. Int. Res."},{"issue":"4","key":"19_CR22","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A Darwiche","year":"2001","unstructured":"Darwiche, A.: Decomposable negation normal form. J. ACM 48(4), 608\u2013647 (2001)","journal-title":"J. ACM"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Darwiche, A.: Tractable Boolean and arithmetic circuits. In: Hitzler, P., Sarker, M.K. (eds.) Neuro-Symbolic Artificial Intelligence: The State of the Art, vol. 342 of Frontiers in Artificial Intelligence and Applications, pp. 146\u2013172. IOS Press (2021)","DOI":"10.3233\/FAIA210353"},{"issue":"1\u20132","key":"19_CR24","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/jancl.11.11-34","volume":"11","author":"A Darwiche","year":"2001","unstructured":"Darwiche, A.: On the tractable counting of theory models and its application to truth maintenance and belief revision. J. Appl. Non-Classical Logics 11(1\u20132), 11\u201334 (2001)","journal-title":"J. Appl. Non-Classical Logics"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Shi, W., Shih, A., Darwiche, A., Choi, A.: On tractable representations of binary neural networks. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, 12\u201318 September 2020, pp. 882\u2013892 (2020)","DOI":"10.24963\/kr.2020\/91"},{"key":"19_CR26","unstructured":"Somenzi, F.: Binary decision diagrams. In: Calculational System Design, vol. 173 of NATO Science Series F, pp. 303\u2013366. IOS Press (1999)"},{"key":"19_CR27","unstructured":"Abc: A system for sequential synthesis and verification"},{"issue":"4","key":"19_CR28","doi-asserted-by":"publisher","first-page":"34:1","DOI":"10.1145\/2068716.2068720","volume":"4","author":"A Mishchenko","year":"2011","unstructured":"Mishchenko, A., Brayton, R.K., Jiang, J.H.R., Jang, S.: Scalable don\u2019t-care-based logic optimization and resynthesis. ACM Trans. Reconfigurable Technol. Syst. 4(4), 34:1-34:23 (2011)","journal-title":"ACM Trans. Reconfigurable Technol. Syst."},{"key":"19_CR29","volume-title":"Synthesis and Optimization of Digital Circuits","author":"G De Micheli","year":"1994","unstructured":"De Micheli, G.: Synthesis and Optimization of Digital Circuits. McGraw-Hill Higher Education, Boston (1994)"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic simulation-techniques and applications. In: 27th ACM\/IEEE Design Automation Conference, pp. 517\u2013521 (1990)","DOI":"10.1145\/123186.128296"},{"key":"19_CR31","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: Walsh, T. (ed.) IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, 16\u201322 July 2011, pp. 819\u2013826. IJCAI\/AAAI (2011)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T06:57:01Z","timestamp":1729753021000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"26% - 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":"11","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)"}}]}}