{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:48:55Z","timestamp":1726037335075},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030255428"},{"type":"electronic","value":"9783030255435"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25543-5_6","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T08:03:09Z","timestamp":1562918589000},"page":"84-94","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Incremental Determinization for Quantifier Elimination and Functional Synthesis"],"prefix":"10.1007","author":[{"given":"Markus N.","family":"Rabe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-14295-6_33","volume-title":"Computer Aided Verification","author":"R Ehlers","year":"2010","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 365\u2013379. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-14295-6_33"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Brenguier, R., P\u00e9rez, G.A., Raskin, J., Sankur, O.: AbsSynthe: abstract synthesis from succinct safety specifications. In: Proceedings of SYNT, pp. 100\u2013116 (2014)","DOI":"10.4204\/EPTCS.157.11"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Jacobs, S., et al.: The 4th reactive synthesis competition (syntcomp 2017): benchmarks, participants & results. arXiv preprint \n                      arXiv:1711.11439\n                      \n                     (2017)","DOI":"10.4204\/EPTCS.260.10"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTLf synthesis. In: Proceedings of IJCAI, IJCAI 2017, pp. 1362\u20131369. AAAI Press (2017)","DOI":"10.24963\/ijcai.2017\/189"},{"issue":"3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/s10703-014-0214-z","volume":"45","author":"E Goldberg","year":"2014","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination by dependency sequents. Formal Methods Syst. Des. 45(2), 111\u2013143 (2014). \n                      https:\/\/doi.org\/10.1007\/s10703-014-0214-z","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination via clause redundancy. In: Formal Methods in Computer-Aided Design, pp. 85\u201392, October 2013","DOI":"10.1109\/FMCAD.2013.6679395"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fried, D., Tabajara, L.M., Vardi, M.Y.: Functional synthesis via input-output separation. In: Proceedings of FMCAD, pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603000"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-662-54577-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Akshay","year":"2017","unstructured":"Akshay, S., Chakraborty, S., John, A.K., Shah, S.: Towards parallel Boolean functional synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 337\u2013353. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54577-5_19"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-96145-3_14","volume-title":"Computer Aided Verification","author":"S Akshay","year":"2018","unstructured":"Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What\u2019s hard about boolean functional synthesis? In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 251\u2013269. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-96145-3_14"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114\u2013128. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31612-8_10"},{"key":"6_CR12","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proceedings of IJCAI, pp. 325\u2013331. AAAI Press (2015)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Proceedings of FMCAD, pp. 136\u2013143 (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"6_CR14","unstructured":"QBFEVAL: QBF solver evaluation portal. \n                      http:\/\/www.qbflib.org\/index_eval.php\n                      \n                    . Accessed Jan 2018"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"Automated Deduction \u2013 CADE-23","author":"A Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22438-6_10"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-662-54577-5_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Wimmer","year":"2017","unstructured":"Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre \u2013 an effective preprocessor for QBF and DQBF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 373\u2013390. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54577-5_21"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-14186-7_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"W Klieber","year":"2010","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128\u2013142. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-14186-7_12"},{"key":"6_CR18","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. In: AAAI Workshop: Beyond NP (2016)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-319-40970-2_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"V Balabanov","year":"2016","unstructured":"Balabanov, V., Jiang, J.-H.R., Scholl, C., Mishchenko, A., Brayton, R.K.: 2QBF: challenges and solutions. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 453\u2013469. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40970-2_28"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-40970-2_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"L Tentrup","year":"2016","unstructured":"Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393\u2013401. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40970-2_24"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-94144-8_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"M Janota","year":"2018","unstructured":"Janota, M.: Circuit-based search space pruning in QBF. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 187\u2013198. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-94144-8_12"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-40970-2_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MN Rabe","year":"2016","unstructured":"Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375\u2013392. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40970-2_23"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-319-96142-2_17","volume-title":"Computer Aided Verification","author":"MN Rabe","year":"2018","unstructured":"Rabe, M.N., Tentrup, L., Rasmussen, C., Seshia, S.A.: Understanding and extending incremental determinization for 2QBF. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 256\u2013274. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-96142-2_17"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-02658-4_30","volume-title":"Computer Aided Verification","author":"J-HR Jiang","year":"2009","unstructured":"Jiang, J.-H.R.: Quantifier elimination via functional composition. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 383\u2013397. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02658-4_30"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-70389-3_10","volume-title":"Hardware and Software: Verification and Testing","author":"S Zhu","year":"2017","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety ltl synthesis. In: Strichman, O., Tzoref-Brill, R. (eds.) Hardware and Software: Verification and Testing. LNCS, vol. 10629, pp. 147\u2013162. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Factored Boolean functional synthesis. In: Proceedings of FMCAD, pp. 124\u2013131. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-41540-6_22","volume-title":"Computer Aided Verification","author":"D Fried","year":"2016","unstructured":"Fried, D., Tabajara, L.M., Vardi, M.Y.: BDD-based Boolean functional synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 402\u2013421. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41540-6_22"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10722167_15"},{"issue":"2\u20133","key":"6_CR29","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. JSAT 7(2\u20133), 71\u201376 (2010)","journal-title":"JSAT"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-319-08587-6_7","volume-title":"Automated Reasoning","author":"MJH Heule","year":"2014","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 91\u2013106. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-08587-6_7"},{"issue":"115\u2013125","key":"6_CR31","first-page":"10","volume":"2","author":"GS Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Constructive Math. Math. Log. 2(115\u2013125), 10\u201313 (1968)","journal-title":"Stud. Constructive Math. Math. Log."},{"issue":"1","key":"6_CR32","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H Buning","year":"1995","unstructured":"Buning, H., Karpinski, M., Flogel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of PLDI, pp. 281\u2013294 (2005)","DOI":"10.1145\/1064978.1065045"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-12002-2_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2010","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 236\u2013250. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-12002-2_19"},{"issue":"1","key":"6_CR35","first-page":"3","volume":"42","author":"CM Wintersteiger","year":"2013","unstructured":"Wintersteiger, C.M., Hamadi, Y., De Moura, L.: Efficiently solving quantified bit-vector formulas. Proc. FMSD 42(1), 3\u201323 (2013)","journal-title":"Proc. FMSD"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-642-39071-5_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"C Jordan","year":"2013","unstructured":"Jordan, C., Kaiser, \u0141.: Experiments with reduction finding. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 192\u2013207. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39071-5_15"},{"key":"6_CR37","unstructured":"Vazquez-Chanlatte, M.: mvcisback\/py-aiger, August 2018. \n                      https:\/\/doi.org\/10.5281\/zenodo.1326224"},{"key":"6_CR38","unstructured":"Lederman, G., Rabe, M.N., Lee, E.A., Seshia, S.A.: Learning heuristics for automated reasoning through deep reinforcement learning. arXiv preprint \n                      arXiv:1807.08058\n                      \n                     (2018)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25543-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T08:04:44Z","timestamp":1562918684000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25543-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255428","9783030255435"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25543-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}