{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:30:13Z","timestamp":1750307413192,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,6,13]],"date-time":"2010-06-13T00:00:00Z","timestamp":1276387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,6,13]]},"DOI":"10.1145\/1837274.1837318","type":"proceedings-article","created":{"date-parts":[[2010,10,28]],"date-time":"2010-10-28T14:47:40Z","timestamp":1288277260000},"page":"170-175","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["An AIG-Based QBF-solver using SAT for preprocessing"],"prefix":"10.1145","author":[{"given":"Florian","family":"Pigorsch","sequence":"first","affiliation":[{"name":"Albert-Ludwigs-Universit\u00e4t Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[{"name":"Albert-Ludwigs-Universit\u00e4t Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,6,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/646484.691763"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646187.683247"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_27"},{"key":"e_1_3_2_1_4_1","volume-title":"Proc. of SAT","author":"Biere A.","year":"2004","unstructured":"A. Biere . Resolve and Expand . In Proc. of SAT 2004 , Selected Papers. A. Biere. Resolve and Expand. In Proc. of SAT 2004, Selected Papers."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_6_1","author":"Cadoli M.","year":"1998","unstructured":"M. Cadoli , M. Schaerf , A. Giovanardi , and M. Giovanardi . An algorithm to evaluate quantified Boolean formulae. In Journal of Automated Reasoning, pages 262--267 , 1998 . M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi. An algorithm to evaluate quantified Boolean formulae. In Journal of Automated Reasoning, pages 262--267, 1998.","journal-title":"An algorithm to evaluate quantified Boolean formulae. In Journal of Automated Reasoning, pages 262--267"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_32"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_5"},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. of SAT","author":"E\u00e9n N.","year":"2003","unstructured":"N. E\u00e9n and N. S\u00f6rensson . An Extensible SAT-solver . In Proc. of SAT 2003 . N. E\u00e9n and N. S\u00f6rensson. An Extensible SAT-solver. In Proc. of SAT 2003."},{"key":"e_1_3_2_1_12_1","volume-title":"Proc. of QiCP","author":"Giunchiglia E.","year":"2008","unstructured":"E. Giunchiglia , P. Marin , and M. Narizzano . sQueezBF: An Effective Preprocessor for QBF . In Proc. of QiCP 2008 . E. Giunchiglia, P. Marin, and M. Narizzano. sQueezBF: An Effective Preprocessor for QBF. In Proc. of QiCP 2008."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/648237.753955"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_30"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.022"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.310903"},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. of IJCAI","author":"Li C. M.","year":"1997","unstructured":"C. M. Li and A. Anbulagan . Heuristics based on unit propagation for satisfiability problems . In Proc. of IJCAI 1997 , San Francisco, CA, USA. C. M. Li and A. Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proc. of IJCAI 1997, San Francisco, CA, USA."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"e_1_3_2_1_20_1","first-page":"03","author":"Mishchenko A.","year":"2005","unstructured":"A. Mishchenko , S. Chatterjee , R. Jiang , and R. K. Brayton . FRAIGs: A unifying representation for logic synthesis and verification. Technical report, EECS Dept., UC Berkeley , 03 2005 . A. Mishchenko, S. Chatterjee, R. Jiang, and R. K. Brayton. FRAIGs: A unifying representation for logic synthesis and verification. Technical report, EECS Dept., UC Berkeley, 03 2005.","journal-title":"Technical report, EECS Dept., UC Berkeley"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30201-8_34"},{"key":"e_1_3_2_1_22_1","volume-title":"QBF Evaluation","author":"Peschiera C.","year":"2008","unstructured":"C. Peschiera , A. Tacchella , and A. Tacchella . QBF Evaluation 2008 . http:\/\/www.qbfeval.org\/2008. C. Peschiera, A. Tacchella, and A. Tacchella. QBF Evaluation 2008. http:\/\/www.qbfeval.org\/2008."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1874620.1875003"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.4"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622859.1622870"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_33"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11889205_37"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378471"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/646399.688905"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379019"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774637"},{"key":"e_1_3_2_1_32_1","volume-title":"Proc. of CP","author":"Zhang L.","year":"2002","unstructured":"L. Zhang and S. Malik . Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver . In Proc. of CP 2002 . L. Zhang and S. Malik. Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver. In Proc. of CP 2002."}],"event":{"name":"DAC '10: The 47th Annual Design Automation Conference 2010","sponsor":["EDAC Electronic Design Automation Consortium","SIGDA ACM Special Interest Group on Design Automation","IEEE-CEDA"],"location":"Anaheim California","acronym":"DAC '10"},"container-title":["Proceedings of the 47th Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1837274.1837318","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1837274.1837318","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:39:35Z","timestamp":1750246775000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1837274.1837318"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6,13]]},"references-count":32,"alternative-id":["10.1145\/1837274.1837318","10.1145\/1837274"],"URL":"https:\/\/doi.org\/10.1145\/1837274.1837318","relation":{},"subject":[],"published":{"date-parts":[[2010,6,13]]},"assertion":[{"value":"2010-06-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}