{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T01:24:10Z","timestamp":1725845050670},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491218"},{"type":"electronic","value":"9783662491225"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_26","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T00:01:36Z","timestamp":1450915296000},"page":"536-556","source":"Crossref","is-referenced-by-count":7,"title":["Automatic Generation of Propagation Complete SAT Encodings"],"prefix":"10.1007","author":[{"given":"Martin","family":"Brain","sequence":"first","affiliation":[]},{"given":"Liana","family":"Hadarean","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"issue":"2","key":"26_CR1","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011)","journal-title":"Constraints"},{"key":"26_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.artint.2013.07.006","volume":"203","author":"M Babka","year":"2013","unstructured":"Babka, M., Balyo, T., \u010cepek, O., Gursk\u1ef3, \u0160., Ku\u010dera, P., Vl\u010dek, V.: Complexity issues related to propagation completeness. Artif. Intell. 203, 19\u201334 (2013)","journal-title":"Artif. Intell."},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-74970-7_12","volume-title":"principles and practice of constraint programming \u2013 cp 2007","author":"F Bacchus","year":"2007","unstructured":"Bacchus, F.: GAC via unit propagation. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 133\u2013147. Springer, Heidelberg (2007)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"26_CR6","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Workshop on Satisfiability Modulo Theories (2010)"},{"key":"26_CR7","unstructured":"Berkeley Logic Synthesis and Verification Group: ABC: A System for Sequential Synthesis and Verification, Release 70930, \n                      http:\/\/www.eecs.berkeley.edu\/alanmi\/abc"},{"key":"26_CR8","unstructured":"Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: International Joint Conference on Artificial Intelligence, pp. 412\u2013418. AAAI Press (2009)"},{"volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","year":"2009","key":"26_CR9","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"26_CR10","unstructured":"Bordeaux, L., Janota, M., Marques-Silva, J., Marquis, P.: On unit-refutation complete formulae with existentially quantified variables. In: Principles of Knowledge Representation and Reasoning. AAAI Press (2012)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1007\/978-3-642-27660-6_50","volume-title":"SOFSEM 2012: Theory and Practice of Computer Science","author":"L Bordeaux","year":"2012","unstructured":"Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 612\u2013624. Springer, Heidelberg (2012)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-35873-9_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Brain","year":"2013","unstructured":"Brain, M., D\u2019Silva, V., Haller, L., Griggio, A., Kroening, D.: An abstract interpretation of DPLL(T). In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 455\u2013475. Springer, Heidelberg (2013)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Del Val, A.: Tractable databases: how to make propositional unit resolution complete through compilation. In: Principles of Knowledge Representation and Reasoning, pp. 551\u2013561. Morgan Kaufmann (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50146-9"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33125-1_22","volume-title":"Static Analysis","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Satisfiability solvers are static analysers. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 317\u2013333. Springer, Heidelberg (2012)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Symposium on Principles of Programming Languages, pp. 143\u2013154. ACM (2013)","DOI":"10.1145\/2480359.2429087"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract satisfaction. In: Symposium on Principles of Programming Languages, pp. 139\u2013150. ACM (2014)","DOI":"10.1145\/2535838.2535868"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48\u201363. Springer, Heidelberg (2012)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-35873-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V D\u2019Silva","year":"2013","unstructured":"D\u2019Silva, V., Kroening, D.: Abstraction of syntax. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 396\u2013413. Springer, Heidelberg (2013)"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014)"},{"issue":"1\u20134","key":"26_CR23","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2(1\u20134), 1\u201326 (2006)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"26_CR24","unstructured":"Gent, I.P.: Arc consistency in SAT. In: European Conference on Artificial Intelligence, pp. 121\u2013125. IOS Press (2002)"},{"issue":"1","key":"26_CR25","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10817-013-9275-8","volume":"52","author":"M Gwynne","year":"2014","unstructured":"Gwynne, M., Kullmann, O.: Generalising unit-refutation completeness and slur via nested input resolution. J. Autom. Reasoning 52(1), 31\u201365 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-319-04921-2_33","volume-title":"Language and Automata Theory and Applications","author":"M Gwynne","year":"2014","unstructured":"Gwynne, M., Kullmann, O.: On SAT representations of XOR constraints. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 409\u2013420. Springer, Heidelberg (2014)"},{"key":"26_CR27","unstructured":"Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Formal Methods in Computer-Aided Design, pp. 131\u2013140. IEEE (2012)"},{"key":"26_CR28","unstructured":"Hansen, T.: A Constraint Solver and its Application to Machine Code Test Generation. Ph.D. thesis, University of Melbourne (2012)"},{"key":"26_CR29","unstructured":"Heule, M., van Maaren, H.: Look-ahead based SAT solvers. In: Handbook of Satisfiability, pp. 155\u2013184. IOS Press (2009)"},{"key":"26_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-02658-4_53","volume-title":"Computer Aided Verification","author":"S Jha","year":"2009","unstructured":"Jha, S., Limaye, R., Seshia, S.A.: Beaver: engineering an efficient SMT solver for bit-vector arithmetic. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 668\u2013674. Springer, Heidelberg (2009)"},{"key":"26_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-11319-2_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A King","year":"2010","unstructured":"King, A., S\u00f8ndergaard, H.: Automatic abstraction for congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 197\u2013213. Springer, Heidelberg (2010)"},{"key":"26_CR32","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Handbook of Satisfiability, pp. 339\u2013401. IOS Press (2009)"},{"issue":"3\u20134","key":"26_CR33","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:AMAI.0000012871.08577.0b","volume":"40","author":"O Kullmann","year":"2004","unstructured":"Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Ann. Math. Artif. Intelli. 40(3\u20134), 303\u2013352 (2004)","journal-title":"Ann. Math. Artif. Intelli."},{"key":"26_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-39611-3_14","volume-title":"Hardware and Software: Verification and Testing","author":"N Manthey","year":"2013","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 102\u2013117. Springer, Heidelberg (2013)"},{"key":"26_CR35","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Exploiting cardinality encodings in parallel maximum satisfiability. In: International Conference on Tools with Artificial Intelligence, pp. 313\u2013320. IEEE Computer Society (2011)","DOI":"10.1109\/ICTAI.2011.54"},{"key":"26_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"26_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"key":"26_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367\u2013373. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:25:21Z","timestamp":1559348721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}