{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:31:03Z","timestamp":1750307463629,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,7,25]],"date-time":"2010-07-25T00:00:00Z","timestamp":1280016000000},"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,7,25]]},"DOI":"10.1145\/1837934.1837954","type":"proceedings-article","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T14:10:11Z","timestamp":1280239811000},"page":"77-84","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Parametric quantified SAT solving"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Sturm","sequence":"first","affiliation":[{"name":"Universidad de Cantabria, Santander, Spain"}]},{"given":"Christoph","family":"Zengler","sequence":"additional","affiliation":[{"name":"Universit\u00e4t T\u00fcbingen, T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2010,7,25]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"133","article-title":"QBF-based formal verification: Experience and perspectives","volume":"5","author":"Benedetti M.","year":"2008","unstructured":"M. Benedetti and H. Mangassarian . QBF-based formal verification: Experience and perspectives . JSAT , 5 : 133 -- 191 , 2008 . M. Benedetti and H. Mangassarian. QBF-based formal verification: Experience and perspectives. JSAT, 5:133--191, 2008.","journal-title":"JSAT"},{"key":"e_1_3_2_1_2_1","first-page":"75","article-title":"Picosat essentials","volume":"4","author":"Biere A.","year":"2008","unstructured":"A. Biere . Picosat essentials . JSAT , 4 : 75 -- 97 , 2008 . A. Biere. Picosat essentials. JSAT, 4:75--97, 2008.","journal-title":"JSAT"},{"key":"e_1_3_2_1_3_1","series-title":"Advances in Computers","volume-title":"Highly Dependable Software","author":"Biere A.","year":"2003","unstructured":"A. Biere , A. Cimatti , E. Clarke , O. Strichman , and Y. Zhu . Bounded model checking . In M. Zelkowitz, editor, Highly Dependable Software , volume 58 of Advances in Computers . Academic Press , San Diego, CA , 2003 . A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. In M. Zelkowitz, editor, Highly Dependable Software, volume 58 of Advances in Computers. Academic Press, San Diego, CA, 2003."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/261320.261324"},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"502","volume-title":"SAT","author":"E\u00e9n N.","year":"2003","unstructured":"N. E\u00e9n and N. S\u00f6rensson . An extensible SAT-solver . In SAT , volume 2919 of LNCS , pages 502 -- 518 . Springer , 2003 . N. E\u00e9n and N. S\u00f6rensson. An extensible SAT-solver. In SAT, volume 2919 of LNCS, pages 502--518. Springer, 2003."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1676041"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/777092.777192"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/982792.982838"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01581082"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006370506164"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646892.709422"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/850949.853610"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_19_1","first-page":"92","volume-title":"Comptes Rendus du premier congres de Mathematiciens des Pays Slaves","author":"Presburger M.","year":"1929","unstructured":"M. Presburger . \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen , in welchem die Addition als einzige Operation hervortritt . In Comptes Rendus du premier congres de Mathematiciens des Pays Slaves , pages 92 -- 101 , Warsaw , Poland , 1929 . M. Presburger. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du premier congres de Mathematiciens des Pays Slaves, pages 92--101, Warsaw, Poland, 1929."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645730.668044"},{"key":"e_1_3_2_1_21_1","first-page":"329","volume-title":"Proceedings of the CASC 2003","author":"Seidl A. M.","year":"2003","unstructured":"A. M. Seidl and T. Sturm . Boolean quantification in a first-order context . In Proceedings of the CASC 2003 , pages 329 -- 345 . Technische Universit\u00e4t M\u00fcnchen, Munich, Germany , 2003 . A. M. Seidl and T. Sturm. Boolean quantification in a first-order context. In Proceedings of the CASC 2003, pages 329--345. Technische Universit\u00e4t M\u00fcnchen, Munich, Germany, 2003."},{"key":"e_1_3_2_1_22_1","first-page":"521","volume-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","author":"Selman B.","year":"1995","unstructured":"B. Selman , H. Kautz , and B. Cohen . Local search strategies for satisfiability testing . In DIMACS Series in Discrete Mathematics and Theoretical Computer Science , pages 521 -- 532 , 1995 . B. Selman, H. Kautz, and B. Cohen. Local search strategies for satisfiability testing. In DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 521--532, 1995."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0890060403171065"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1987.tb00208.x"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80003-8"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774637"}],"event":{"name":"ISSAC '10: International Symposium on Symbolic and Algebraic Computation","sponsor":["Gesellschaft fur Informtatik","SIGSAM ACM Special Interest Group on Symbolic and Algebraic Manipulation"],"location":"Munich Germany","acronym":"ISSAC '10"},"container-title":["Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1837934.1837954","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1837934.1837954","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:28Z","timestamp":1750248508000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1837934.1837954"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,25]]},"references-count":24,"alternative-id":["10.1145\/1837934.1837954","10.1145\/1837934"],"URL":"https:\/\/doi.org\/10.1145\/1837934.1837954","relation":{},"subject":[],"published":{"date-parts":[[2010,7,25]]},"assertion":[{"value":"2010-07-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}