{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T16:57:19Z","timestamp":1773248239400,"version":"3.50.1"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T00:00:00Z","timestamp":1603238400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T00:00:00Z","timestamp":1603238400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004541","name":"Ministry of Human Resource Development","doi-asserted-by":"publisher","award":["MHRD IMPRINT-1 5496"],"award-info":[{"award-number":["MHRD IMPRINT-1 5496"]}],"id":[{"id":"10.13039\/501100004541","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001843","name":"Science and Engineering Research Board","doi-asserted-by":"publisher","award":["MTR\/2018\/000744"],"award-info":[{"award-number":["MTR\/2018\/000744"]}],"id":[{"id":"10.13039\/501100001843","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,7]]},"DOI":"10.1007\/s10703-020-00352-2","type":"journal-article","created":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T15:02:40Z","timestamp":1603292560000},"page":"53-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Boolean functional synthesis: hardness and practical algorithms"],"prefix":"10.1007","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2471-5997","authenticated-orcid":false,"given":"S.","family":"Akshay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7527-7675","authenticated-orcid":false,"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shubham","family":"Goel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sumith","family":"Kulal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shetal","family":"Shah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,21]]},"reference":[{"key":"352_CR1","doi-asserted-by":"crossref","unstructured":"Akshay S, Chakraborty S, John AK, Shah S (2017) Towards parallel Boolean functional synthesis. In: Proceedings of international conference on tools and algorithms for construction and analysis of systems (TACAS), part I, pp 337\u2013353","DOI":"10.1007\/978-3-662-54577-5_19"},{"key":"352_CR2","doi-asserted-by":"crossref","unstructured":"Akshay S, Arora J, Chakraborty S, Krishna S, Raghunathan D, Shah S (2019) Knowledge compilation for Boolean functional synthesis. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 161\u2013169","DOI":"10.23919\/FMCAD.2019.8894266"},{"key":"352_CR3","unstructured":"Akshay S, Chakraborty S, Goel S, Kulal S, Shah S (2020) Code and benchmark details for BFSS experiments. https:\/\/github.com\/BooleanFunctionalSynthesis\/bfss. Accessed Sept 2020"},{"issue":"2","key":"352_CR4","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/s10009-004-0179-0","volume":"7","author":"R Alur","year":"2005","unstructured":"Alur R, Madhusudan P, Nam W (2005) Symbolic computational techniques for solving games. Int J Softw Tools Technol Transf 7(2):118\u2013128","journal-title":"Int J Softw Tools Technol Transf"},{"key":"352_CR5","doi-asserted-by":"crossref","unstructured":"Andersson G, Bjesse P, Cook B, Hanna Z (2002) A proof engine approach to solving combinational design automation problems. In: Proceedings of design automation conference (DAC), pp 725\u2013730","DOI":"10.1145\/513918.514101"},{"key":"352_CR6","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0020-0190(98)00106-9","volume":"67","author":"F Baader","year":"1998","unstructured":"Baader F (1998) On the complexity of Boolean unification. Inf Process Lett 67:215\u2013220","journal-title":"Inf Process Lett"},{"issue":"1","key":"352_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov V, Jiang JHR (2012) Unified QBF certification and its applications. Form Methods Syst Des 41(1):45\u201365","journal-title":"Form Methods Syst Des"},{"key":"352_CR8","unstructured":"Boole G (1847) The mathematical analysis of logic. Philosophical Library"},{"issue":"5","key":"352_CR9","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1016\/S0747-7171(89)80054-9","volume":"8","author":"A Boudet","year":"1989","unstructured":"Boudet A, Jouannaud JP, Schmidt-Schauss M (1989) Unification in Boolean rings and Abelian groups. J Symb Comput 8(5):449\u2013477","journal-title":"J Symb Comput"},{"key":"352_CR10","doi-asserted-by":"crossref","unstructured":"Brayton R, Mishchenko A (2010) ABC: an academic industrial-strength verification tool. In: Proceedings of international conference on computer-aided verification (CAV), pp 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"352_CR11","doi-asserted-by":"crossref","unstructured":"Brenguier R, P\u00e9rez GA, Raskin JF, Sankur O (2014) AbsSynthe: abstract synthesis from succinct safety specifications. In: Proceedings of workshop on synthesis (SYNT), open publishing association, electronic proceedings in theoretical computer science, vol 157, pp 100\u2013116","DOI":"10.4204\/EPTCS.157.11"},{"issue":"8","key":"352_CR12","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"352_CR13","doi-asserted-by":"crossref","unstructured":"Chakraborty S, Fremont DJ, Meel KS, Seshia SA, Vardi MY (2015) On parallel scalable uniform SAT witness generation. In: Proceedings of international conference on tools and algorithms for the construction and analysis of systems (TACAS), pp 304\u2013319","DOI":"10.1007\/978-3-662-46681-0_25"},{"key":"352_CR14","doi-asserted-by":"crossref","unstructured":"Chakraborty S, Fried D, Tabajara LM, Vardi MY (2018) Functional synthesis via input\u2013output separation. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 1\u20139","DOI":"10.23919\/FMCAD.2018.8603000"},{"key":"352_CR15","unstructured":"Chandrasekaran V, Srebro N, Harsha P (2008) Complexity of inference in graphical models. In: Proceedings of international conference on uncertainty in artificial intelligence (UAI), pp 70\u201378"},{"key":"352_CR16","doi-asserted-by":"crossref","unstructured":"Chen Y, Eickmeyer K, Flum J (2012) The exponential time hypothesis and the parameterized clique problem. In: Proceedings of international conference on parameterized and exact computation (IPEC), pp 13\u201324","DOI":"10.1007\/978-3-642-33293-7_4"},{"issue":"4","key":"352_CR17","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A Darwiche","year":"2001","unstructured":"Darwiche A (2001) Decomposable negation normal form. J ACM 48(4):608\u2013647","journal-title":"J ACM"},{"issue":"4","key":"352_CR18","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0012-365X(72)90090-8","volume":"3","author":"JP Deschamps","year":"1972","unstructured":"Deschamps JP (1972) Parametric solutions of Boolean equations. Discrete Math 3(4):333\u2013342","journal-title":"Discrete Math"},{"key":"352_CR19","doi-asserted-by":"crossref","unstructured":"Fried D, Tabajara LM, Vardi MY (2016) BDD-based Boolean functional synthesis. In: Proceedings (part II) of international conference on computer-aided verification (CAV), pp 402\u2013421","DOI":"10.1007\/978-3-319-41540-6_22"},{"issue":"1","key":"352_CR20","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.jcss.2013.07.005","volume":"80","author":"R Ganian","year":"2014","unstructured":"Ganian R, Hlinen\u00fd P, Langer A, Obdrz\u00e1lek J, Rossmanith P, Sikdar S (2014) Lower bounds on the complexity of MSO$${}_{\\text{1 }}$$ model-checking. J Comput Syst Sci 80(1):180\u2013194","journal-title":"J Comput Syst Sci"},{"key":"352_CR21","doi-asserted-by":"crossref","unstructured":"Golia P, Roy S, Meel KS (2020) Manthan: a data-driven approach for Boolean function synthesis. In: Proceedings of international conference on computer-aided verification (CAV), pp 611\u2013633","DOI":"10.1007\/978-3-030-53291-8_31"},{"issue":"3","key":"352_CR22","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/PGEC.1963.263531","volume":"12","author":"L Hellerman","year":"1963","unstructured":"Hellerman L (1963) A catalog of three-variable Or-Invert and And-Invert logical circuits. IEEE Trans Electron Comput 12(3):198\u2013223","journal-title":"IEEE Trans Electron Comput"},{"key":"352_CR23","doi-asserted-by":"crossref","unstructured":"Heule M, Seidl M, Biere A (2014) Efficient extraction of Skolem functions from QRAT proofs. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 107\u2013114","DOI":"10.1109\/FMCAD.2014.6987602"},{"issue":"2","key":"352_CR24","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1006\/jcss.2000.1727","volume":"62","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo R, Paturi R (2001) On the complexity of k-SAT. J Comput Syst Sci 62(2):367\u2013375","journal-title":"J Comput Syst Sci"},{"key":"352_CR25","doi-asserted-by":"crossref","unstructured":"Jiang JHR (2009) Quantifier elimination via functional composition. In: Proceedings of international conference on computer-aided verification (CAV). Springer, pp 383\u2013397","DOI":"10.1007\/978-3-642-02658-4_30"},{"key":"352_CR26","doi-asserted-by":"crossref","unstructured":"Jiang JHR, Lin HP, Hung WL (2009) Interpolating functions from large Boolean relations. In: Proceedings of international conference on computer-aided design (ICCAD), pp 779\u2013784","DOI":"10.1145\/1687399.1687544"},{"key":"352_CR27","doi-asserted-by":"crossref","unstructured":"Jo S, Matsumoto T, Fujita M (2012) SAT-based automatic rectification and debugging of combinational circuits with LUT insertions. In: Proceedings of Asian test symposium (ATS), pp 19\u201324","DOI":"10.1109\/ATS.2012.55"},{"key":"352_CR28","doi-asserted-by":"crossref","unstructured":"John A, Shah S, Chakraborty S, Trivedi A, Akshay S (2015) Skolem functions for factored formulas. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 73\u201380","DOI":"10.1109\/FMCAD.2015.7542255"},{"issue":"2","key":"352_CR29","first-page":"191","volume":"28","author":"R Karp","year":"1982","unstructured":"Karp R, Lipton R (1982) Turing machines that take advice. L\u2019Enseignment Math\u00e9matique 28(2):191\u2013209","journal-title":"L\u2019Enseignment Math\u00e9matique"},{"key":"352_CR30","doi-asserted-by":"crossref","unstructured":"Kuehlmann A, Krohm F (1997) Equivalence checking using cuts and heaps. In: Proceedings of design automation conference (DAC), pp 263\u2013268","DOI":"10.1145\/266021.266090"},{"issue":"6","key":"352_CR31","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/1809028.1806632","volume":"45","author":"V Kuncak","year":"2010","unstructured":"Kuncak V, Mayer M, Piskac R, Suter P (2010) Complete functional synthesis. ACM SIGPLAN Not 45(6):316\u2013329","journal-title":"ACM SIGPLAN Not"},{"key":"352_CR32","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/BF01474159","volume":"68","author":"L L\u00f6wenheim","year":"1910","unstructured":"L\u00f6wenheim L (1910) \u00dcber die Aufl\u00f6sung von Gleichungen in Logischen Gebietkalkul. Math Ann 68:169\u2013207","journal-title":"Math Ann"},{"key":"352_CR33","doi-asserted-by":"crossref","unstructured":"Macii E, Odasso G, Poncino M (1998) Comparing different Boolean unification algorithms. In: Conference record of asilomar conference on signals, systems and computers (Cat. No. 98CH36284), vol\u00a02, pp 1052\u20131056","DOI":"10.1109\/ACSSC.1998.751423"},{"issue":"3\u20134","key":"352_CR34","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0747-7171(89)80013-6","volume":"7","author":"U Martin","year":"1989","unstructured":"Martin U, Nipkow T (1989) Boolean unification: the story so far. J Symb Comput 7(3\u20134):275\u2013293","journal-title":"J Symb Comput"},{"key":"352_CR35","doi-asserted-by":"crossref","unstructured":"Niemetz A, Preiner M, Lonsing F, Seidl M, Biere A (2012) Resolution-based certificate extraction for QBF\u2014(tool presentation). In: Proceedings of international conference on theory and applications of satisfiability testing (SAT), pp 430\u2013435","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"352_CR36","unstructured":"QBFLib (2018) QBFEval 2018. http:\/\/www.qbflib.org\/qbfeval18.php. Accessed July 2018"},{"key":"352_CR37","doi-asserted-by":"crossref","unstructured":"Rabe MN (2019) Incremental determinization for quantifier elimination and functional synthesis. In: Proceedings of international conference on computer-aided verification (CAV), part II, pp 84\u201394","DOI":"10.1007\/978-3-030-25543-5_6"},{"key":"352_CR38","doi-asserted-by":"crossref","unstructured":"Rabe MN, Seshia SA (2016) Incremental determinization. In: Proceedings of international conference on theory and applications of satisfiability testing (SAT), pp 375\u2013392","DOI":"10.1007\/978-3-319-40970-2_23"},{"key":"352_CR39","doi-asserted-by":"crossref","unstructured":"Rabe MN, Tentrup L (2015) CAQE: a certifying QBF solver. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 136\u2013143","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"352_CR40","doi-asserted-by":"crossref","unstructured":"Rabe MN, Tentrup L, Rasmussen C, Seshia SA (2018) Understanding and extending incremental determinization for 2QBF. In: Proceedings of international conference on computer-aided verification (CAV), part II, pp 256\u2013274","DOI":"10.1007\/978-3-319-96142-2_17"},{"key":"352_CR41","first-page":"127","volume-title":"Handbook of satisfiability, chap 14","author":"JM Silva","year":"2008","unstructured":"Silva JM, Lynce I, Malik S (2008) Conflict-driven clause learning SAT solvers. In: Biere A, Heule M, van Maaren H, Walsch T (eds) Handbook of satisfiability, chap 14. IOS Press, Amsterdam, pp 127\u2013149"},{"issue":"5\u20136","key":"352_CR42","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama A (2013) Program sketching. Int J Softw Tools Technol Transf 15(5\u20136):475\u2013495","journal-title":"Int J Softw Tools Technol Transf"},{"key":"352_CR43","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Rabbah RM, Bod\u00edk R, Ebcioglu K (2005) Programming by sketching for bit-streaming programs. In: Proceedings of international conference on programming language design and implementation (PLDI), pp 281\u2013294","DOI":"10.1145\/1064978.1065045"},{"issue":"5\u20136","key":"352_CR44","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava S, Gulwani S, Foster JS (2013) Template-based program verification and program synthesis. Int J Softw Tools Technol Transf 15(5\u20136):497\u2013518","journal-title":"Int J Softw Tools Technol Transf"},{"key":"352_CR45","doi-asserted-by":"crossref","unstructured":"Tabajara LM, Vardi MY (2017) Factored Boolean functional synthesis. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 124\u2013131","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"352_CR46","unstructured":"Trivedi A (2003) Techniques in symbolic model checking. Master\u2019s thesis, Indian Institute of Technology Bombay, Mumbai, India"},{"key":"352_CR47","doi-asserted-by":"crossref","unstructured":"Zhu S, Tabajara LM, Li J, Pu G, Vardi MY (2017) Symbolic LTLf synthesis. In: Proceedings of international joint conference on artificial intelligence (IJCAI), pp 1362\u20131369","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00352-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00352-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00352-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T00:18:26Z","timestamp":1634775506000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00352-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,21]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,7]]}},"alternative-id":["352"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00352-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,10,21]]},"assertion":[{"value":"22 September 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 October 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}