{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T08:02:41Z","timestamp":1791964961090,"version":"4.3.4"},"reference-count":36,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/fmcad.2018.8603000","type":"proceedings-article","created":{"date-parts":[[2019,1,9]],"date-time":"2019-01-09T01:33:52Z","timestamp":1546997632000},"page":"1-9","source":"Crossref","is-referenced-by-count":12,"title":["Functional Synthesis via Input-Output Separation"],"prefix":"10.23919","author":[{"given":"Supratik","family":"Chakraborty","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dror","family":"Fried","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lucas M.","family":"Tabajara","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","article-title":"Template-Based Program Verification and Program Synthesis","volume":"15","author":"srivastava","year":"2013","journal-title":"STTT"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","article-title":"Program Sketching","volume":"15","author":"solar-lezama","year":"2013","journal-title":"STTT"},{"key":"ref30","first-page":"131","article-title":"Conflict-Driven Clause Learning SAT Solvers","author":"silva","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/189"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"ref34","article-title":"BDD-Based Boolean Synthesis","author":"tabajara","year":"2018","journal-title":"Master’s thesis"},{"key":"ref10","first-page":"502","article-title":"An Extensible SAT-solver","author":"e\u00e9n","year":"2003","journal-title":"Theory and Applications of Satisfiability Testing 6th Int Conf SAT 2003"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209203"},{"key":"ref12","first-page":"402","article-title":"BDD-Based Boolean Functional Synthesis","author":"fried","year":"2016","journal-title":"Computer Aided Verification - 28th International Conference CAV 2016"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_3"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_30"},{"key":"ref16","first-page":"27","article-title":"The Second Reactive Synthesis Competition (SYNTCOMP 2015)","author":"jacobs","year":"2015","journal-title":"Proceedings Fourth Workshop on Synthesis SYNT 2015"},{"key":"ref17","first-page":"383","article-title":"Quantifier Elimination via Functional Composition","author":"jiang","year":"2009","journal-title":"Computer Aided Verification 21st International Conference CAV 2009"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ATS.2012.55"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542255"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/978-3-642-02777-2_39","article-title":"Solving (Weighted) Partial MaxSAT through Satisfiability Testing","author":"ans\u00f3tegui","year":"2009","journal-title":"Theory and Applications of Satisfiability Testing - SAT 2009"},{"key":"ref27","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/978-3-319-40970-2_23","article-title":"Incremental Determinization","author":"rabe","year":"2016","journal-title":"Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0179-0"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0152-6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BF00058680"},{"key":"ref5","first-page":"399","article-title":"Predicting Learnt Clauses Quality in Modern SAT Solvers","author":"audemard","year":"2009","journal-title":"Proceedings of the 21st International Joint Conference on Artificial Intelligence IJCAI 2009"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_12"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_12"},{"key":"ref2","first-page":"337","article-title":"Towards Parallel Boolean Functional Synthesis","author":"akshay","year":"2017","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference TACAS 2017"},{"key":"ref9","author":"boole","year":"1847","journal-title":"The Mathematical Analysis of Logic"},{"key":"ref1","first-page":"251","article-title":"What’s Hard About Boolean Functional Synthesisƒ","author":"akshay","year":"2018","journal-title":"Computer Aided Verification -30th International Conference CAV 2018"},{"key":"ref20","first-page":"113","article-title":"Building Circuits from Relations","author":"kukula","year":"2000","journal-title":"Computer Aided Verification 12th International Conference CAV 2000"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01474159"},{"key":"ref21","first-page":"613","article-title":"MaxSAT, Hard and Soft Constraints","author":"li","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/978-3-319-09284-3_33","article-title":"Open-WBO: A Modular MaxSAT Solver","author":"martins","year":"2014","journal-title":"Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference"},{"key":"ref23","first-page":"17","article-title":"Comparing Different Boolean Unification Algorithms","author":"macii","year":"2006","journal-title":"Proceedings of 32nd Asilomar Conference on Signals Systems and Computers"},{"key":"ref26","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","article-title":"Resolution-Based Certificate Extraction for QBF - (Tool Presentation)","author":"niemetz","year":"2012","journal-title":"Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11853886_45"}],"event":{"name":"2018 Formal Methods in Computer Aided Design (FMCAD)","location":"Austin, TX","start":{"date-parts":[[2018,10,30]]},"end":{"date-parts":[[2018,11,2]]}},"container-title":["2018 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8585253\/8602989\/08603000.pdf?arnumber=8603000","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T00:42:31Z","timestamp":1643157751000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8603000\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":36,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2018.8603000","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}