{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T09:43:25Z","timestamp":1725615805651},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642243714"},{"type":"electronic","value":"9783642243721"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24372-1_14","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T09:41:14Z","timestamp":1317289274000},"page":"183-197","source":"Crossref","is-referenced-by-count":3,"title":["Antichain-Based QBF Solving"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Brihaye","sequence":"first","affiliation":[]},{"given":"V\u00e9ronique","family":"Bruy\u00e8re","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Doyen","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Ducobu","sequence":"additional","affiliation":[]},{"given":"Jean-Francois","family":"Raskin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1006\/jagm.2001.1202","volume":"42","author":"T. Asano","year":"2002","unstructured":"Asano, T., Williamson, D.P.: Improved approximation algorithms for max sat. J. Algorithms\u00a042(1), 173\u2013202 (2002)","journal-title":"J. Algorithms"},{"key":"14_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-540-32275-7_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Evaluating QBFs via Symbolic Skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 285\u2013300. Springer, Heidelberg (2005)"},{"unstructured":"Benedetti, M.: Extracting Certificates from Quantified Boolean Formulas. In: Kaelbling, L.P., Saffiotti, A. (eds.) IJCAI, pp. 47\u201353. Professional Book Center (2005)","key":"14_CR3"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/11499107_28","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Quantifier Trees for QBFs. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 378\u2013385. Springer, Heidelberg (2005)"},{"key":"14_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: A Suite to Evaluate and Certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"issue":"1-4","key":"14_CR6","first-page":"133","volume":"5","author":"M. Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: Qbf-based formal verification: Experience and perspectives. JSAT\u00a05(1-4), 133\u2013191 (2008)","journal-title":"JSAT"},{"issue":"2-4","key":"14_CR7","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT Essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"14_CR8","first-page":"262","volume-title":"Proc. of AAAI 1998\/IAAI 1998","author":"M. Cadoli","year":"1998","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified Boolean formulae. In: Proc. of AAAI 1998\/IAAI 1998, pp. 262\u2013267. MIT Press, Cambridge (1998)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F. Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 66\u201380. Springer, Heidelberg (2005)"},{"issue":"1-3","key":"14_CR10","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2007.07.050","volume":"388","author":"B. Cook","year":"2007","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Verification of boolean programs with unbounded thread creation. Theor. Comput. Sci.\u00a0388(1-3), 227\u2013242 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M. Wulf De","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A New Algorithm for Checking Universality of Finite Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 17\u201330. Springer, Heidelberg (2006)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-12002-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Doyen","year":"2010","unstructured":"Doyen, L., Raskin, J.-F.: Antichain Algorithms for Finite Automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 2\u201322. Springer, Heidelberg (2010)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"14_CR14","first-page":"417","volume-title":"Proc. of IAAI","author":"U. Egly","year":"2000","unstructured":"Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. In: Proc. of IAAI, pp. 417\u2013422. AAAI Press, Menlo Park (2000)"},{"unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), www.qbflib.org","key":"14_CR15"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-30494-4_15","volume-title":"Formal Methods in Computer-Aided Design","author":"E. Giunchiglia","year":"2004","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: An Efficient QBF Solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 201\u2013213. Springer, Heidelberg (2004)"},{"key":"14_CR17","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E. Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas. J. Artif. Intell. Res.\u00a026, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"14_CR18","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T. Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing BMC Encodings with QBF. Electron. Notes Theor. Comput. Sci.\u00a0174, 45\u201356 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"14_CR19","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1137\/S0895480191220836","volume":"7","author":"R. Kohli","year":"1994","unstructured":"Kohli, R., Krishnamurti, R., Mirchandani, P.: The Minimum Satisfiability Problem. SIAM J. Discrete Math.\u00a07(2), 275\u2013283 (1994)","journal-title":"SIAM J. Discrete Math."},{"unstructured":"K\u00fcgel, A.: Improved Exact Solver for the Weighted Max-SAT problem. Accepted at the workshop Pragmatics of SAT. To appear in easychair electronic proceedings (2011)","key":"14_CR20"},{"key":"14_CR21","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"613","volume-title":"Handbook of Satisfiability","author":"C.M. Li","year":"2009","unstructured":"Li, C.M., Many\u00e0, F.: MaxSAT, Hard and Soft Constraints. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 613\u2013631. IOS Press, Amsterdam (2009)"},{"key":"14_CR22","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190077","volume":"7","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver (System Description). Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 71\u201376 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-14186-7_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: Integrating Dependency Schemes in Search-Based QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 158\u2013171. Springer, Heidelberg (2010)"},{"key":"14_CR24","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/AIC-2009-0468","volume":"22","author":"M. Narizzano","year":"2009","unstructured":"Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and certifying QBFs: A comparison of state-of-the-art tools. AI Commun.\u00a022, 191\u2013210 (2009)","journal-title":"AI Commun."},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-30201-8_34","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G. Pan","year":"2004","unstructured":"Pan, G., Vardi, M.Y.: Symbolic Decision Procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 453\u2013467. Springer, Heidelberg (2004)"},{"key":"14_CR26","volume-title":"Computational complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational complexity. Addison-Wesley Publishing Company, Reading (1994)"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-14186-7_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"C. Peschiera","year":"2010","unstructured":"Peschiera, C., Pulina, L., Tacchella, A., Bubeck, U., Kullmann, O., Lynce, I.: The Seventh QBF Solvers Evaluation (QBFEVAL 2010). In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 237\u2013250. Springer, Heidelberg (2010)"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/11889205_37","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"H. Samulowitz","year":"2006","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol.\u00a04204, pp. 514\u2013529. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24372-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,25]],"date-time":"2020-06-25T06:08:54Z","timestamp":1593065334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24372-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243714","9783642243721"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24372-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}