{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T14:16:44Z","timestamp":1790518604738,"version":"4.1.0"},"reference-count":48,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/fmcad.2018.8603004","type":"proceedings-article","created":{"date-parts":[[2019,1,9]],"date-time":"2019-01-09T01:33:52Z","timestamp":1546997632000},"page":"1-10","source":"Crossref","is-referenced-by-count":9,"title":["Expansion-Based QBF Solving Without Recursion"],"prefix":"10.23919","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Braud-Santoni","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vedad","family":"Hadzic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Uwe","family":"Egly","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_19"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"key":"ref32","first-page":"735","article-title":"Theory of Quantified Boolean Formulas","volume":"185","author":"kleine b\u00fcning","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref31","first-page":"230","article-title":"Abstraction-Based Algorithm for 2QBF","volume":"6695","author":"janota","year":"2011","journal-title":"SAT LNCS"},{"key":"ref30","first-page":"325","article-title":"Solving QBF by Clause Selection","author":"janota","year":"2015","journal-title":"IJCAI"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98334-9_19"},{"key":"ref36","first-page":"371","article-title":"DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL","volume":"10395","author":"lonsing","year":"2017","journal-title":"CADE LNCS"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45616-3_12"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_12"},{"key":"ref10","article-title":"Solving QBF Instances with Nested SAT Solvers","volume":"ws 16 5","author":"bogaerts","year":"2016","journal-title":"Beyond NP AAAI Workshops"},{"key":"ref40","article-title":"A Comparative Study of 2QBF Algorithms","author":"ranjan","year":"2004","journal-title":"SAT"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_24"},{"key":"ref12","first-page":"27","article-title":"Dynamic Programming-based QBF Solving","volume":"1719","author":"charwat","year":"0"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_6"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_23"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_32"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-016-9501-2"},{"key":"ref18","first-page":"354","article-title":"Encodings of Bounded Synthesis","volume":"10205","author":"faymonville","year":"2017","journal-title":"TACAS LNCS"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:12)2015"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_7"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.08.007"},{"key":"ref27","first-page":"114","article-title":"Solving QBF with Counterexample Guided Refinement","volume":"7317","author":"janota","year":"2012","journal-title":"SAT LNCS"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_28"},{"key":"ref6","first-page":"101","article-title":"Blocked Clause Elimination for QBF","volume":"6803","author":"biere","year":"2011","journal-title":"CADE LNCS"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44465-8_8"},{"key":"ref8","first-page":"1","article-title":"SAT-Based Synthesis Methods for Safety Specs","volume":"8318","author":"bloem","year":"2014","journal-title":"VMCAI LNCS"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603004"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_12"},{"key":"ref9","first-page":"63","article-title":"SAT-to-SAT in QBFEval 2016","volume":"1719","author":"bogaerts","year":"2016"},{"key":"ref1","first-page":"399","article-title":"Predicting learnt clauses quality in modern SAT solvers","author":"audemard","year":"0"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_21"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1007\/978-3-319-06200-6_23","article-title":"A Synthesized Algorithm for Interactive Consistency","volume":"8430","author":"gasc\u00f3n","year":"2014","journal-title":"NASA Formal Methods Ser LNCS"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"ref48","first-page":"224","article-title":"QBF Encoding of Temporal Properties and QBF-Based Verification","volume":"8562","author":"zhang","year":"2014","journal-title":"IJCAR of LNCS"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_9"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46135-3_14"},{"key":"ref21","first-page":"761","article-title":"Reasoning with Quantified Boolean Formulas","volume":"185","author":"giunchiglia","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_24"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_18"},{"key":"ref41","first-page":"1045","article-title":"Asymptotically Optimal Encodings of Conformant Planning in QBF","author":"rintanen","year":"2007","journal-title":"AAAI"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1613\/jair.4694"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_25"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.004"},{"key":"ref43","first-page":"475","article-title":"On Expansion and Resolution in CEGAR Based QBF Solving","volume":"10427","author":"tentrup","year":"2017","journal-title":"CAV LNCS"},{"key":"ref25","doi-asserted-by":"crossref","DOI":"10.1609\/aaai.v32i1.12208","article-title":"Towards Generalization in QBF Solving via Machine Learning","author":"janota","year":"2018","journal-title":"AAAI"}],"event":{"name":"2018 Formal Methods in Computer Aided Design (FMCAD)","location":"Austin, TX","start":{"date-parts":[[2018,10,30]]},"end":{"date-parts":[[2018,11,2]]}},"container-title":["2018 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8585253\/8602989\/08603004.pdf?arnumber=8603004","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,12]],"date-time":"2023-09-12T19:36:56Z","timestamp":1694547416000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8603004\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":48,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2018.8603004","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}