{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:21Z","timestamp":1740122721762,"version":"3.37.3"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1319459","IIS-1527668"],"award-info":[{"award-number":["CCF-1319459","IIS-1527668"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004541","name":"Ministry of Human Resource Development","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004541","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002425","name":"Governo Brasil","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002425","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,4]]},"DOI":"10.1007\/s10703-023-00410-5","type":"journal-article","created":{"date-parts":[[2023,3,26]],"date-time":"2023-03-26T21:12:19Z","timestamp":1679865139000},"page":"228-258","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Functional synthesis via input\u2013output separation"],"prefix":"10.1007","volume":"60","author":[{"given":"Supratik","family":"Chakraborty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dror","family":"Fried","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9608-1404","authenticated-orcid":false,"given":"Lucas M.","family":"Tabajara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,3,9]]},"reference":[{"key":"410_CR1","doi-asserted-by":"crossref","unstructured":"Akshay S, Arora J, Chakraborty S, Krishna S, Raghunathan D, Shah S (2019) Knowledge compilation for Boolean functional synthesis. In: Formal methods in computer-aided design, FMCAD 2019, pp 161\u2013169","DOI":"10.23919\/FMCAD.2019.8894266"},{"key":"410_CR2","doi-asserted-by":"publisher","unstructured":"Akshay S, Chakraborty S, Goel S, Kulal S, Shah S (2018) What\u2019s hard about Boolean functional synthesis? In: Computer aided verification\u201330th international conference, CAV 2018, pp 251\u2013269. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_14","DOI":"10.1007\/978-3-319-96145-3_14"},{"key":"410_CR3","doi-asserted-by":"publisher","unstructured":"Akshay S, Chakraborty S, John AK, Shah S (2017) Towards parallel Boolean functional synthesis. In: Tools and algorithms for the construction and analysis of systems\u201323rd international conference, TACAS 2017, pp 337\u2013353. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_19","DOI":"10.1007\/978-3-662-54577-5_19"},{"issue":"2","key":"410_CR4","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 (2005) Symbolic computational techniques for solving games. STTT 7(2):118\u2013128","journal-title":"STTT"},{"key":"410_CR5","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui C, Bonet ML, Levy J (2009) Solving (Weighted) partial MaxSAT through satisfiability testing. In: Theory and applications of satisfiability testing\u2013SAT 2009\u201312th international conference, pp 427\u2013440. https:\/\/doi.org\/10.1007\/978-3-642-02777-2_39","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"410_CR6","unstructured":"Audemard G, Simon L (2009) Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st international joint conference on artificial intelligence, IJCAI 2009, pp 399\u2013404. http:\/\/ijcai.org\/Proceedings\/09\/Papers\/074.pdf"},{"key":"410_CR7","unstructured":"Bacchus F, J\u00e4rvisalo M, Malik S (2021) Maxium satisfiability. In: Handbook of satisfiability, pp 929\u2013991"},{"issue":"1","key":"410_CR8","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 JHR (2012) Unified QBF certification and its applications. Form Methods Syst Des 41(1):45\u201365. https:\/\/doi.org\/10.1007\/s10703-012-0152-6","journal-title":"Form Methods Syst Des"},{"key":"410_CR9","doi-asserted-by":"publisher","unstructured":"Balabanov V, Jiang JR (2011) Resolution proofs and Skolem functions in QBF evaluation and applications. In: Computer aided verification\u201323rd international conference, CAV 2011, pp 149\u2013164. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_12","DOI":"10.1007\/978-3-642-22110-1_12"},{"key":"410_CR10","doi-asserted-by":"publisher","unstructured":"Balabanov V, Widl M, Jiang JR (2014) QBF Resolution systems and their proof complexities. In: Theory and applications of satisfiability testing\u2013SAT 2014\u201317th international conference, pp 154\u2013169. https:\/\/doi.org\/10.1007\/978-3-319-09284-3_12","DOI":"10.1007\/978-3-319-09284-3_12"},{"key":"410_CR11","volume-title":"The mathematical analysis of logic","author":"G Boole","year":"1847","unstructured":"Boole G (1847) The mathematical analysis of logic. Philosophical Library, New York"},{"issue":"8","key":"410_CR12","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Tran Comput 35(8):677\u2013691. https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE Tran Comput"},{"key":"410_CR13","volume-title":"Formal methods in computer aided design FMCAD 2018","author":"S Chakraborty","year":"2018","unstructured":"Chakraborty S, Fried D, Tabajara LM, Vardi MY (2018) Functional synthesis via input-output separation. In: Bj\u00f8rner N, Gurfinkel A (eds) Formal methods in computer aided design FMCAD 2018. IEEE, New York"},{"key":"410_CR14","doi-asserted-by":"publisher","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible SAT-solver. In: Theory and applications of satisfiability testing\u2013SAT 2003\u20136th International Conference, pp 502\u2013518. https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"410_CR15","doi-asserted-by":"publisher","unstructured":"Fried D, Legay A, Ouaknine J, Vardi MY (2018) Sequential relational decomposition. In: Proceedings of the 33rd annual ACM\/IEEE symposium on logic in computer science, LICS 2018, pp. 432\u2013441. https:\/\/doi.org\/10.1145\/3209108.3209203. http:\/\/doi.acm.org\/10.1145\/3209108.3209203","DOI":"10.1145\/3209108.3209203"},{"key":"410_CR16","doi-asserted-by":"publisher","unstructured":"Fried D, Tabajara LM, Vardi MY (2016) BDD-Based Boolean functional synthesis. In: Computer aided verification\u201328th international conference, CAV 2016, pp 402\u2013421. https:\/\/doi.org\/10.1007\/978-3-319-41540-6_22. http:\/\/dx.doi.org\/10.1007\/978-3-319-41540-6_22","DOI":"10.1007\/978-3-319-41540-6_22"},{"key":"410_CR17","doi-asserted-by":"publisher","unstructured":"Ganian R, Szeider S (2017) New width parameters for model counting. In: Theory and applications of satisfiability testing\u2013sat 2017\u201320th international conference, pp 38\u201352. https:\/\/doi.org\/10.1007\/978-3-319-66263-3_3","DOI":"10.1007\/978-3-319-66263-3_3"},{"key":"410_CR18","doi-asserted-by":"crossref","unstructured":"Golia P, Roy S, Meel KS (2020) Manthan: a data driven approach for Boolean function synthesis. https:\/\/arxiv.org\/abs\/2005.06922","DOI":"10.1007\/978-3-030-53291-8_31"},{"key":"410_CR19","doi-asserted-by":"publisher","unstructured":"Heule M, Seidl M, Biere A (2014) Efficient extraction of skolem functions from QRAT proofs. In: Formal methods in computer-aided design, FMCAD 2014, pp 107\u2013114. https:\/\/doi.org\/10.1109\/FMCAD.2014.6987602","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"410_CR20","doi-asserted-by":"publisher","unstructured":"Ignatiev A, Morgado A, Planes J, Marques-Silva J (2013) Maximal falsifiability\u2013definitions, algorithms, and applications. In: Logic for programming, artificial intelligence, and reasoning\u201319th international conference, LPAR-19, pp 439\u2013456. https:\/\/doi.org\/10.1007\/978-3-642-45221-5_30","DOI":"10.1007\/978-3-642-45221-5_30"},{"key":"410_CR21","doi-asserted-by":"crossref","unstructured":"Jacobs S, Bloem R, Brenguier R, K\u00f6nighofer R, P\u00e9rez GA, Raskin J, Ryzhyk L, Sankur O, Seidl M, Tentrup L, Walker A (2015) The second reactive synthesis competition (SYNTCOMP 2015). In: Proceedings fourth workshop on synthesis, SYNT 2015, pp 27\u201357","DOI":"10.4204\/EPTCS.202.4"},{"key":"410_CR22","doi-asserted-by":"publisher","unstructured":"Jiang JR (2009) Quantifier elimination via functional composition. In: Computer aided verification, 21st international conference, CAV 2009, pp 383\u2013397. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_30","DOI":"10.1007\/978-3-642-02658-4_30"},{"key":"410_CR23","doi-asserted-by":"crossref","unstructured":"Jo S, Matsumoto T, Fujita M (2012) SAT-based automatic rectification and debugging of combinational circuits with LUT insertions. In: Proceedings of the 2012 IEEE 21st Asian test symposium, ATS \u201912, pp 19\u201324. IEEE Computer Society","DOI":"10.1109\/ATS.2012.55"},{"key":"410_CR24","doi-asserted-by":"crossref","unstructured":"John AK, Shah S, Chakraborty S, Trivedi A, Akshay S (2015) Skolem functions for factored formulas. In: Formal methods in computer-aided design, FMCAD 2015, pp 73\u201380","DOI":"10.1109\/FMCAD.2015.7542255"},{"issue":"12","key":"410_CR25","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann A, Paruthi V, Krohm F, Ganai M (2002) Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans Comput Aided Des Integr Circuits Syst 21(12):1377\u20131394. https:\/\/doi.org\/10.1109\/TCAD.2002.804386","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"410_CR26","doi-asserted-by":"publisher","unstructured":"Kukula JH, Shiple TR (2000) Building circuits from relations. In: Computer aided verification, 12th international conference, CAV 2000, pp 113\u2013123. https:\/\/doi.org\/10.1007\/10722167_12","DOI":"10.1007\/10722167_12"},{"key":"410_CR27","doi-asserted-by":"crossref","unstructured":"Lakkaraju H, Bach SH, Jure L (2016) Interpretable decision sets: a joint framework for description and prediction. In: International conference on knowledge discovery and data mining (KDD), pp 1675V\u20131684","DOI":"10.1145\/2939672.2939874"},{"key":"410_CR28","doi-asserted-by":"publisher","unstructured":"Li CM, Many\u00e0 F (2009) MaxSAT, hard and soft constraints. In: Handbook of satisfiability, pp 613\u2013631. https:\/\/doi.org\/10.3233\/978-1-58603-929-5-613","DOI":"10.3233\/978-1-58603-929-5-613"},{"key":"410_CR29","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/BF01474159","volume":"68","author":"L Lowenheim","year":"1910","unstructured":"Lowenheim L (1910) \u00dcber die Aufl\u00f6sung von Gleichungen in Logischen Gebietkalkul. Math Ann 68:169\u2013207","journal-title":"Math Ann"},{"key":"410_CR30","unstructured":"Macii E, Odasso G, Poncino M (2006) Comparing different Boolean unification algorithms. In: Proceedings of 32nd Asilomar conference on signals, systems and computers, pp 17\u201329"},{"key":"410_CR31","doi-asserted-by":"publisher","unstructured":"Martins R, Manquinho VM, Lynce I (2014) Open-WBO: a modular MaxSAT solver. In: Theory and applications of satisfiability testing\u2013SAT 2014\u201317th international conference, pp 438\u2013445. https:\/\/doi.org\/10.1007\/978-3-319-09284-3_33","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"410_CR32","doi-asserted-by":"crossref","unstructured":"Narizzano M, Pulina L, Tacchella A (2006) The QBFEVAL web portal. In: Logics in artificial intelligence, pp 494\u2013497. Springer, Berlin","DOI":"10.1007\/11853886_45"},{"key":"410_CR33","doi-asserted-by":"crossref","unstructured":"Niemetz A, Preiner M, Lonsing F, Seidl M, Bierre A (2012) Resolution-based certificate extraction for QBF - (tool presentation). In: Theory and applications of satisfiability testing\u2013SAT 2012\u201315th international conference, pp 430\u2013435","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"410_CR34","doi-asserted-by":"publisher","unstructured":"Rabe MN, Seshia SA (2016) Incremental determinization. In: Theory and applications of satisfiability testing\u2013SAT 2016\u201319th International Conference, pp 375\u2013392. https:\/\/doi.org\/10.1007\/978-3-319-40970-2_23","DOI":"10.1007\/978-3-319-40970-2_23"},{"key":"410_CR35","doi-asserted-by":"crossref","unstructured":"Rabe MN, Tentrup L (2015) CAQE: A certifying QBF solver. In: Formal methods in computer-aided design, FMCAD 2015, pp 136\u2013143","DOI":"10.1109\/FMCAD.2015.7542263"},{"issue":"3","key":"410_CR36","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/BF00058680","volume":"2","author":"RL Rivest","year":"1987","unstructured":"Rivest RL (1987) Learning decision lists. Mach Learn 2(3):229\u2013246. https:\/\/doi.org\/10.1007\/BF00058680","journal-title":"Mach Learn"},{"key":"410_CR37","doi-asserted-by":"publisher","unstructured":"Silva JPM, Lynce I, Malik S (2009) Conflict-driven clause learning SAT solvers. In: Handbook of satisfiability, pp 131\u2013153. https:\/\/doi.org\/10.3233\/978-1-58603-929-5-131","DOI":"10.3233\/978-1-58603-929-5-131"},{"issue":"5\u20136","key":"410_CR38","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 (2013) Program sketching. STTT 15(5\u20136):475\u2013495","journal-title":"STTT"},{"key":"410_CR39","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Rabbah RM, Bod\u00edk R, Ebcioglu K (2005) Programming by sketching for bit-streaming programs. In: Proceedings of the ACM SIGPLAN 2005 conference on programming language design and implementation, pp 281\u2013294","DOI":"10.1145\/1065010.1065045"},{"issue":"5\u20136","key":"410_CR40","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 JS (2013) Template-based program verification and program synthesis. STTT 15(5\u20136):497\u2013518","journal-title":"STTT"},{"issue":"1","key":"410_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"LJ Stockmeyer","year":"1976","unstructured":"Stockmeyer LJ (1976) The polynomial-time hierarchy. Theort Comput Sci 3(1):1\u201322","journal-title":"Theort Comput Sci"},{"key":"410_CR42","unstructured":"Tabajara LM (2018) BDD-based Boolean synthesis. Master\u2019s thesis, Rice University"},{"key":"410_CR43","doi-asserted-by":"publisher","unstructured":"Tabajara LM, Vardi MY (2017) Factored Boolean functional synthesis. In: Formal methods in computer aided design, FMCAD 2017, pp 124\u2013131. https:\/\/doi.org\/10.23919\/FMCAD.2017.8102250","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"410_CR44","doi-asserted-by":"publisher","unstructured":"Zhu, S., Tabajara LM, Li J, Pu G, Vardi, MY (2017) Symbolic LTLf synthesis. In: Proceedings of the 26th international joint conference on artificial intelligence, IJCAI 2017, pp 1362\u20131369 . https:\/\/doi.org\/10.24963\/ijcai.2017\/189","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00410-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00410-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00410-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,13]],"date-time":"2023-04-13T17:12:58Z","timestamp":1681405978000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00410-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["410"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00410-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2022,4]]},"assertion":[{"value":"25 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 January 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 March 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}