{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:54:12Z","timestamp":1762102452264,"version":"3.28.0"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894266","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T09:25:06Z","timestamp":1573637106000},"page":"161-169","source":"Crossref","is-referenced-by-count":13,"title":["Knowledge Compilation for Boolean Functional Synthesis"],"prefix":"10.23919","author":[{"given":"S.","family":"Akshay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jatin","family":"Arora","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Krishna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Divya","family":"Raghunathan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shetal","family":"Shah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"ref11","first-page":"383","article-title":"Quantifier elimination via functional composition","author":"jiang","year":"2009","journal-title":"Proc of CAV"},{"key":"ref12","first-page":"149","article-title":"Resolution proofs and Skolem functions in QBF evaluation and applications","author":"jiang","year":"2011","journal-title":"Proc of CAV"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542255"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806632"},{"key":"ref15","article-title":"Propositional independence - formula-variable independence and forgetting","author":"lang","year":"2011","journal-title":"CoRR abs\/1106 4578"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF01474159"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref18","article-title":"DSHARP: Fast d-DNNF Compilation with sharpSAT","author":"muise","year":"2016","journal-title":"Beyond NP AAAI Workshops"},{"journal-title":"QBFLib QBFEval","year":"2018","key":"ref19"},{"journal-title":"The Mathematical Analysis of Logic","year":"1847","author":"boole","key":"ref4"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_19"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603000"},{"key":"ref5","first-page":"137","article-title":"A survey on knowledge compilation","volume":"10","author":"cadoli","year":"1997","journal-title":"AI Commun"},{"key":"ref8","article-title":"A knowledge compilation map","author":"darwiche","year":"2011","journal-title":"CoRR abs\/1106 1819"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/502090.502091"},{"key":"ref2","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 Held as Part of the Federated Logic Conference FloC 2018"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_22"},{"key":"ref1","article-title":"Knowledge compilation for boolean functional synthesis","author":"akshay","year":"2019","journal-title":"CoRR submit\/2808510"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_23"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_17"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"ref24","first-page":"115","article-title":"On the complexity of derivation in propositional calculus","author":"tseitin","year":"1968","journal-title":"Structures in Constructive Mathematics and Mathematical Logic Part II Seminars in Mathematics"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/800135.804419"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","start":{"date-parts":[[2019,10,22]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894266.pdf?arnumber=8894266","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T22:45:34Z","timestamp":1598222734000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894266\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":25,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894266","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}