{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:00:13Z","timestamp":1740132013123,"version":"3.37.3"},"reference-count":31,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"9","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/501100004663","name":"Ministry of Science and Technology of Taiwan","doi-asserted-by":"publisher","award":["101-2923-E-002-015-MY2","103-2221-E-002-273","104-2628-E-002-013-MY3"],"award-info":[{"award-number":["101-2923-E-002-015-MY2","103-2221-E-002-273","104-2628-E-002-013-MY3"]}],"id":[{"id":"10.13039\/501100004663","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Taiwan Scholarship"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2016,9]]},"DOI":"10.1109\/tcad.2015.2512906","type":"journal-article","created":{"date-parts":[[2015,12,29]],"date-time":"2015-12-29T18:19:31Z","timestamp":1451413171000},"page":"1557-1568","source":"Crossref","is-referenced-by-count":0,"title":["Flexibility and Optimization of QBF Skolem\u2013Herbrand Certificates"],"prefix":"10.1109","volume":"35","author":[{"given":"Valeriy","family":"Balabanov","sequence":"first","affiliation":[]},{"given":"Shuo-Ren","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1120725.1120821"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/11499107_32","article-title":"Bounded model checking with QBF","author":"dershowitz","year":"2005","journal-title":"Proc Int Conf Theory and Appl Satisfiability Testing"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_21"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_38"},{"key":"ref13","first-page":"546","article-title":"A uniform approach for generating proofs and strategies for both true and false QBF formulas","author":"goultiaeva","year":"2011","journal-title":"Proc Int Joint Conf Artif Intell (IJCAI)"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","article-title":"Clause-term resolution and learning in quantified Boolean logic satisfiability","volume":"26","author":"giunchiglia","year":"2006","journal-title":"Artif Intell Res"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_21"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1687399.1687544"},{"key":"ref17","first-page":"114","article-title":"Solving QBF with counterexample guided refinement","author":"janota","year":"2012","journal-title":"Proc Int Conf Theory and Appl Satisfiability Testing"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"key":"ref19","first-page":"836","article-title":"Minimal module extraction from DL-lite ontologies using QBF solvers","author":"kontchakov","year":"2009","journal-title":"Proc Int Joint Conf Artif Intell (IJCAI)"},{"journal-title":"Quantified Boolean Formulas Satisfiability Library (QBFLIB)","year":"2014","key":"ref28"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_12"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_34"},{"key":"ref3","first-page":"47","article-title":"Extracting certificates from quantified Boolean formulas","author":"benedetti","year":"2005","journal-title":"Proc Int Joint Conf Artif Intell (IJCAI)"},{"key":"ref6","first-page":"3694","article-title":"Efficient extraction of QBF (counter)models from long-distance resolution proofs","author":"balabanov","year":"2015","journal-title":"Proc AAAI Conf Artif Intell"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_25"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0152-6"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_12"},{"journal-title":"ABC A System for Sequential Synthesis and Verification","year":"2015","key":"ref7"},{"key":"ref2","first-page":"285","article-title":"Evaluating QBFs via symbolic Skolemization","author":"benedetti","year":"2004","journal-title":"Proc Int Conf Logic Program Artif Intell Reasoning (LPAR)"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015019416843"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190077","article-title":"DepQBF: A dependency-aware QBF solver","volume":"7","author":"lonsing","year":"2010","journal-title":"J Satisfiability Boolean Model Comput"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837398"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/AIC-2009-0468","article-title":"Evaluating and certifying QBFs: A comparison of state-of-the-art tools","volume":"22","author":"narizzano","year":"2009","journal-title":"AI Commun"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"ref26","first-page":"1045","article-title":"Asymptotically optimal encodings of conformant planning in QBF","author":"rintanen","year":"2007","journal-title":"Proc Nat Conf Artif Intell (AAAI)"},{"journal-title":"Computational Complexity","year":"1994","author":"papadimitriou","key":"ref25"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/7547335\/07368172.pdf?arnumber=7368172","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:48:48Z","timestamp":1641988128000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7368172\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":31,"journal-issue":{"issue":"9"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2015.2512906","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"type":"print","value":"0278-0070"},{"type":"electronic","value":"1937-4151"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}