{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T11:02:18Z","timestamp":1775818938108,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642027765","type":"print"},{"value":"9783642027772","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_19","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"181-194","source":"Crossref","is-referenced-by-count":45,"title":["New Encodings of Pseudo-Boolean Constraints into CNF"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Bailleux","sequence":"first","affiliation":[]},{"given":"Yacine","family":"Boufkhad","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Roussel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., Bjesse, P., E\u00e9n, N.: Symbolic reachability analysis based on SAT-solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 411\u2013425. Springer, Heidelberg (2000)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Generic ILP versus Specialized 0-1 ILP: An Update. In: Proc. of Int. Conf. on Computer Aided Design (ICCAD 2002), pp. 450\u2013457 (2002)","DOI":"10.1145\/774572.774638"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","first-page":"133","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"F. Bacchus","year":"2003","unstructured":"Bacchus, F.: Gac via unit propagation. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 133\u2013147. Springer, Heidelberg (2003)"},{"key":"19_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.\u00a02833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"key":"19_CR5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/SAT190021","volume":"2","author":"O. Bailleux","year":"2006","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: A Translation of Pseudo Boolean Constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a02, 191\u2013200 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic Model Checking using SAT procedures instead of BDDs. In: Proc. of Design Automation Conference (DAC 1999), pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-77442-6_6","volume-title":"Practical Aspects of Declarative Languages","author":"S. Brand","year":"2008","unstructured":"Brand, S., Duck, G.J., Puchinger, J., Stuckey, P.J.: Flexible, Rule-based Constraint Model Linearisation. In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol.\u00a04902, pp. 68\u201383. Springer, Heidelberg (2008)"},{"key":"19_CR8","unstructured":"Ernst, M., Millstein, T., Weld, D.S.: Automatic SAT-Compilation of Planning Problems. In: IJCAI 1997, pp. 1169\u20131176 (1997)"},{"key":"19_CR9","unstructured":"Gent, I.P.: Arc Consistency in SAT. In: Proc. of the Fifteenth European Conference on Artificial Intelligence (ECAI 2002), pp. 121\u2013125 (2002)"},{"key":"19_CR10","unstructured":"Grastien, A., Anbulagan, A., Rintanen, J., Kelareva, E.: Diagnosis of Discrete-Event Systems Using Satisfiability Algorithms. In: AAAI-2007, pp. 305\u2013310 (2007)"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-540-72788-0_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A. Hertel","year":"2007","unstructured":"Hertel, A., Hertel, P., Urquhart, A.: Formalizing Dangerous SAT Encodings. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 159\u2013172. Springer, Heidelberg (2007)"},{"key":"19_CR12","unstructured":"Baker, A.B., Crawford, J.M.: Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems. In: Proc. of the Twelfth National Conference on Artificial Intelligence, pp. 1092\u20131097 (1994)"},{"key":"19_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a02, 1\u201326 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"19_CR14","unstructured":"Sheini, H.M., Sakallah, K.A.: Pueblo: a modern pseudo-Boolean SAT solver. In: Design, Automation and Test in Europe, 2005. Proc., pp. 684\u2013685 (2005)"},{"key":"19_CR15","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.\u00a03709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"J.P. Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters\u00a068(2), 63\u201369 (1998)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T01:25:48Z","timestamp":1589937948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}