{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:57:48Z","timestamp":1762102668554,"version":"3.28.0"},"reference-count":26,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6,29]]},"DOI":"10.1109\/lics52264.2021.9470741","type":"proceedings-article","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T16:14:07Z","timestamp":1625674447000},"page":"1-13","source":"Crossref","is-referenced-by-count":7,"title":["A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis"],"prefix":"10.1109","author":[{"given":"Preey","family":"Shah","sequence":"first","affiliation":[]},{"given":"Aman","family":"Bansal","sequence":"additional","affiliation":[]},{"given":"S.","family":"Akshay","sequence":"additional","affiliation":[]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542255"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806632"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-319-96145-3_14","article-title":"What&#x2019;s Hard About Boolean Functional Synthesis?","author":"akshay","year":"2018","journal-title":"Proc of 30th International Conference on Computer Aided Verification Part I"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_31"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2019.8894266"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.11.11-34"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/12.73590"},{"key":"ref18","first-page":"137","article-title":"A survey on knowledge compilation","volume":"10","author":"cadoli","year":"1997","journal-title":"AI Commun"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/502090.502091"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"ref6","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":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_23"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_19"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_22"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603000"},{"key":"ref1","first-page":"383","article-title":"Quantifier elimination via functional composition","volume":"5643","author":"jiang","year":"2009","journal-title":"CAV"},{"key":"ref20","article-title":"DSHARP: Fast d-DNNF Compilation with sharpSAT","author":"muise","year":"2016","journal-title":"Beyond NP AAAI Workshops"},{"key":"ref22","article-title":"A normal form characterization for efficient Boolean Skolem function synthesis","author":"shah","year":"2021","journal-title":"CoRR"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1613\/jair.989"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_17"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"ref26","first-page":"1008","article-title":"Knowledge compilation meets communication complexity","author":"bova","year":"2016","journal-title":"Proc of 25th International Joint Conference on Artificial Intelligence IJCAI"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00352-2"}],"event":{"name":"2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","start":{"date-parts":[[2021,6,29]]},"location":"Rome, Italy","end":{"date-parts":[[2021,7,2]]}},"container-title":["2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9470497\/9470501\/09470741.pdf?arnumber=9470741","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T02:31:16Z","timestamp":1672713076000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9470741\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,29]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/lics52264.2021.9470741","relation":{},"subject":[],"published":{"date-parts":[[2021,6,29]]}}}