{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:58:06Z","timestamp":1782878286965,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1453386"],"award-info":[{"award-number":["1453386"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["8750-14-2-0270"],"award-info":[{"award-number":["8750-14-2-0270"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192382","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"420-435","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":71,"title":["Program synthesis using conflict-driven learning"],"prefix":"10.1145","author":[{"given":"Yu","family":"Feng","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Osbert","family":"Bastani","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_2_3_1","volume-title":"Proc. International Conference on Learning Representations . OpenReview.","author":"Balog Matej","year":"2017","unstructured":"Matej Balog , Alexander L Gaunt , Marc Brockschmidt , Sebastian Nowozin , and Daniel Tarlow . 2017 . Deepcoder: Learning to write programs . In Proc. International Conference on Learning Representations . OpenReview. Matej Balog, Alexander L Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. 2017. Deepcoder: Learning to write programs. In Proc. International Conference on Learning Representations . OpenReview."},{"key":"e_1_3_2_2_4_1","volume-title":"The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation","author":"Berre Daniel Le","year":"2010","unstructured":"Daniel Le Berre and Anne Parrain . 2010. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation ( 2010 ), 59\u20136. Daniel Le Berre and Anne Parrain. 2010. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation (2010), 59\u20136."},{"key":"e_1_3_2_2_5_1","volume-title":"Frontiers in Artificial Intelligence and Applications","author":"Biere Armin","year":"2009","unstructured":"Armin Biere , Marijn Heule , Hans van Maaren , and Toby Walsh . 2009. Conflict-driven clause learning SAT solvers. Handbook of Satisfiability , Frontiers in Artificial Intelligence and Applications ( 2009 ), 131\u2013153. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. 2009. Conflict-driven clause learning SAT solvers. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications (2009), 131\u2013153."},{"key":"e_1_3_2_2_6_1","volume-title":"Proc. Tools and Algorithms for Construction and Analysis of Systems","author":"Moura Leonardo De","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An efficient SMT solver . In Proc. Tools and Algorithms for Construction and Analysis of Systems . Springer , 337\u2013340. Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proc. Tools and Algorithms for Construction and Analysis of Systems . Springer, 337\u2013340."},{"key":"e_1_3_2_2_7_1","unstructured":"Yu Feng Ruben Martins Osbert Bastani and Isil Dillig. 2018. Neo. http:\/\/utopia-group.github.io\/neo\/ .  Yu Feng Ruben Martins Osbert Bastani and Isil Dillig. 2018. Neo. http:\/\/utopia-group.github.io\/neo\/ ."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_5"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462192"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_2_19_1","volume-title":"Proc. International Conference on Machine Learning. Proceedings of Machine Learning Research, 187\u2013195","author":"Menon Aditya","year":"2013","unstructured":"Aditya Menon , Omer Tamuz , Sumit Gulwani , Butler Lampson , and Adam Kalai . 2013 . A machine learning framework for programming by example . In Proc. International Conference on Machine Learning. Proceedings of Machine Learning Research, 187\u2013195 . Aditya Menon, Omer Tamuz, Sumit Gulwani, Butler Lampson, and Adam Kalai. 2013. A machine learning framework for programming by example. In Proc. International Conference on Machine Learning. Proceedings of Machine Learning Research, 187\u2013195."},{"key":"e_1_3_2_2_20_1","volume-title":"Proc. International Conference on Learning Representations . OpenReview.","author":"Neelakantan Arvind","year":"2017","unstructured":"Arvind Neelakantan , Quoc V Le , Martin Abadi , Andrew McCallum , and Dario Amodei . 2017 . Learning a natural language interface with neural programmer . In Proc. International Conference on Learning Representations . OpenReview. Arvind Neelakantan, Quoc V Le, Martin Abadi, Andrew McCallum, and Dario Amodei. 2017. Learning a natural language interface with neural programmer. In Proc. International Conference on Learning Representations . OpenReview."},{"key":"e_1_3_2_2_21_1","volume-title":"Proc. International Conference on Learning Representations . OpenReview.","author":"Neelakantan Arvind","year":"2016","unstructured":"Arvind Neelakantan , Quoc V Le , and Ilya Sutskever . 2016 . Neural programmer: Inducing latent programs with gradient descent . In Proc. International Conference on Learning Representations . OpenReview. Arvind Neelakantan, Quoc V Le, and Ilya Sutskever. 2016. Neural programmer: Inducing latent programs with gradient descent. In Proc. International Conference on Learning Representations . OpenReview."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837671"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594321"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.14778\/2977797.2977807"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837668"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908102"},{"key":"e_1_3_2_2_29_1","volume-title":"Program synthesis by sketching","author":"Solar-Lezama Armando","unstructured":"Armando Solar-Lezama . 2008. Program synthesis by sketching . University of California , Berkeley. Armando Solar-Lezama. 2008. Program synthesis by sketching. University of California, Berkeley."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_2_33_1","unstructured":"Ilya Sutskever Oriol Vinyals and Quoc V Le. 2014. Sequence to sequence learning with neural networks. In Advances in Neural Information Processing Systems . 3104\u20133112.   Ilya Sutskever Oriol Vinyals and Quoc V Le. 2014. Sequence to sequence learning with neural networks. In Advances in Neural Information Processing Systems . 3104\u20133112."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_33"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462174"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062365"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133886"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158151"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908088"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133887"},{"key":"e_1_3_2_2_41_1","volume-title":"Proc. of International Conference on Computer-Aided Design. IEEE Computer Society, 279\u2013285","author":"Zhang Lintao","year":"2001","unstructured":"Lintao Zhang , Conor F. Madigan , Matthew W. Moskewicz , and Sharad Malik . 2001 . Efficient Conflict Driven Learning in Boolean Satisfiability Solver . In Proc. of International Conference on Computer-Aided Design. IEEE Computer Society, 279\u2013285 . Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. 2001. Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In Proc. of International Conference on Computer-Aided Design. IEEE Computer Society, 279\u2013285."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693082"}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192382","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192382","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192382","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192382"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":42,"alternative-id":["10.1145\/3192366.3192382","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192382","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192382","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}