{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:02:02Z","timestamp":1743073322682,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656323"},{"type":"electronic","value":"9783031656330"}],"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,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"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><jats:p>Inspired by recent progress in dynamic programming approaches for weighted model counting, we investigate a dynamic-programming approach in the context of boolean realizability and synthesis, which takes a conjunctive-normal-form boolean formula over input and output variables, and aims at synthesizing witness functions for the output variables in terms of the inputs. We show how graded project-join trees, obtained via tree decomposition, can be used to compute a BDD representing the realizability set for the input formulas in a bottom-up order. We then show how the intermediate BDDs generated during realizability checking phase can be applied to synthesizing the witness functions in a top-down manner. An experimental evaluation of a solver \u2013 DPSynth \u2013 based on these ideas demonstrates that our approach for Boolean realizabilty and synthesis has superior time and space performance over a heuristics-based approach using same symbolic representations. We discuss the advantage on scalability of the new approach, and also investigate our findings on the performance of the DP framework.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_6","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"112-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Dynamic Programming for\u00a0Symbolic Boolean Realizability and\u00a0Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8443-2246","authenticated-orcid":false,"given":"Yi","family":"Lin","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9608-1404","authenticated-orcid":false,"given":"Lucas","family":"Martinelli Tabajara","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0661-5773","authenticated-orcid":false,"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Akshay, S., Arora, J., Chakraborty, S., Krishna, S., Raghunathan, D., Shah, S.: Knowledge compilation for Boolean functional synthesis. In: 2019 Formal Methods in Computer Aided Design (FMCAD), pp. 161\u2013169. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894266"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-96145-3_14","volume-title":"Computer Aided Verification","author":"S Akshay","year":"2018","unstructured":"Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What\u2019s hard about Boolean functional synthesis? In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part I. LNCS, vol. 10981, pp. 251\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_14"},{"issue":"1","key":"6_CR3","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."},{"issue":"2","key":"6_CR4","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"RI Bahar","year":"1997","unstructured":"Bahar, R.I., et al.: Algebric decision diagrams and their applications. Formal Meth. Syst. Des. 10(2), 171\u2013206 (1997)","journal-title":"Formal Meth. Syst. Des."},{"issue":"3731","key":"6_CR5","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1126\/science.153.3731.34","volume":"153","author":"R Bellman","year":"1966","unstructured":"Bellman, R.: Dynamic programming. Science 153(3731), 34\u201337 (1966)","journal-title":"Science"},{"key":"6_CR6","unstructured":"Bodlaender, H.L., et al.: Treewidth is np-complete on cubic graphs (and related results). arXiv preprint arXiv:2301.10031 (2023)"},{"issue":"8","key":"6_CR7","first-page":"677","volume":"100","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE TC 100(8), 677\u2013691 (1986)","journal-title":"IEEE TC"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Heule, M.J.: Dual proof generation for quantified Boolean formulas with a BDD-based solver. In: CADE, pp. 433\u2013449 (2021)","DOI":"10.1007\/978-3-030-79876-5_25"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-030-72016-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2021","unstructured":"Bryant, R.E., Heule, M.J.H.: Generating extended resolution proofs with a BDD-based SAT solver. In: TACAS 2021. LNCS, vol. 12651, pp. 76\u201393. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_5"},{"key":"6_CR10","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transistion relations. In: Proceeding of the IFIP 10.5 International Conference on Very Large Scale Integration. IFIP Transactions, vol.\u00a0A-1, pp. 49\u201358. North-Holland (1991)"},{"issue":"2","key":"6_CR11","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-030-58475-7_13","volume-title":"Principles and Practice of Constraint Programming","author":"JM Dudek","year":"2020","unstructured":"Dudek, J.M., Phan, V.H.N., Vardi, M.Y.: DPMC: weighted model counting by dynamic programming on project-join trees. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 211\u2013230. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_13"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-030-80223-3_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"JM Dudek","year":"2021","unstructured":"Dudek, J.M., Phan, V.H.N., Vardi, M.Y.: ProCount: weighted projected model counting with graded project-join trees. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 152\u2013170. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_11"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Dudek, J.M., Phan, V.H., Vardi, M.Y.: ADDMC: weighted model counting with algebraic decision diagrams. In: AAAI, vol.\u00a034, pp. 1468\u20131476 (2020)","DOI":"10.1609\/aaai.v34i02.5505"},{"key":"6_CR15","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":"6_CR16","unstructured":"Gogate, V., Dechter, R.: A complete anytime algorithm for treewidth. arXiv preprint arXiv:1207.4109 (2012)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/978-3-030-53291-8_31","volume-title":"Computer Aided Verification","author":"P Golia","year":"2020","unstructured":"Golia, P., Roy, S., Meel, K.S.: Manthan: a data-driven approach for Boolean function synthesis. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 611\u2013633. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_31"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Golia, P., Slivovsky, F., Roy, S., Meel, K.S.: Engineering an efficient Boolean functional synthesis engine. In: 2021 IEEE\/ACM International Conference On Computer Aided Design (ICCAD), pp.\u00a01\u20139. IEEE (2021)","DOI":"10.1109\/ICCAD51958.2021.9643583"},{"key":"6_CR19","unstructured":"Hachtel, G.D., Somenzi, F.: Logic Synthesis and Verification Algorithms. Springer, Cham (2007)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Hamann, M., Strasser, B.: Graph bisection with pareto-optimization. In: Goodrich, M.T., Mitzenmacher, M. (eds.) Proceedings of the Eighteenth Workshop on Algorithm Engineering and Experiments, ALENEX 2016, Arlington, Virginia, USA, January 10, 2016, pp. 90\u2013102. SIAM (2016)","DOI":"10.1137\/1.9781611974317.8"},{"key":"6_CR21","unstructured":"Lin, Y., Tabajara, L.M., Vardi, M.Y.: Dynamic programming for symbolic Boolean realizability and synthesis (2024). arXiv:2405.07975"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proceedings of the 38th Annual Design Automation Conference. pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/11853886_45","volume-title":"Logics in Artificial Intelligence","author":"M Narizzano","year":"2006","unstructured":"Narizzano, M., Pulina, L., Tacchella, A.: The QBFEVAL web portal. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 494\u2013497. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11853886_45"},{"key":"6_CR24","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"},{"issue":"2","key":"6_CR25","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/0095-8956(91)90061-N","volume":"52","author":"N Robertson","year":"1991","unstructured":"Robertson, N., Seymour, P.D.: Graph minors. x. obstructions to tree-decomposition. J. Comb. Theory Ser. B 52(2), 153\u2013190 (1991)","journal-title":"J. Comb. Theory Ser. B"},{"key":"6_CR26","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD), pp. 42\u201347. IEEE (1993)"},{"key":"6_CR27","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 3.0.0. University of Colorado at Boulder (2015)"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Factored Boolean functional synthesis. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October, 2017, pp. 124\u2013131. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"6_CR29","unstructured":"Tabajara, L.M., Vardi, M.Y.: Partitioning techniques in LTLF synthesis. In: International Joint Conference on Artificial Intelligence (2019)"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-70389-3_10","volume-title":"Hardware and Software: Verification and Testing","author":"S Zhu","year":"2017","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety ltl synthesis. In: HVC 2017. LNCS, vol. 10629, pp. 147\u2013162. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTLF synthesis. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence, pp. 1362\u20131369. ijcai.org (2017)","DOI":"10.24963\/ijcai.2017\/189"}],"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-65633-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:04:17Z","timestamp":1721891057000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_6","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":"26 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}