{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T16:17:24Z","timestamp":1769876244414,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642333460","type":"print"},{"value":"9783642333477","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33347-7_10","type":"book-chapter","created":{"date-parts":[[2012,9,8]],"date-time":"2012-09-08T02:26:21Z","timestamp":1347071181000},"page":"107-118","source":"Crossref","is-referenced-by-count":16,"title":["A Compact Encoding of Pseudo-Boolean Constraints into SAT"],"prefix":"10.1007","author":[{"given":"Steffen","family":"H\u00f6lldobler","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Steinke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Potsdam answer set solving collection, \n                    \n                      http:\/\/potassco.sourceforge.net\/"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-21581-0_7","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"I. Ab\u00edo","year":"2011","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: BDDs for Pseudo-Boolean Constraints \u2013 Revisited. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 61\u201375. Springer, Heidelberg (2011)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Apt, K.: Principles of Constraint Programming. Cambridge University Press (2003)","DOI":"10.1017\/CBO9780511615320"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R. As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality Networks and Their Applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 167\u2013180. Springer, Heidelberg (2009)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-642-02777-2_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"O. Bailleux","year":"2009","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: New Encodings of Pseudo-Boolean Constraints into CNF. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 181\u2013194. Springer, Heidelberg (2009)"},{"key":"10_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. DAC, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"issue":"7","key":"10_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Comm. ACM"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"issue":"1-4","key":"10_CR9","first-page":"1","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. JSAT\u00a02(1-4), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-79719-7_7","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"T. Eibach","year":"2008","unstructured":"Eibach, T., Pilz, E., V\u00f6lkel, G.: Attacking Bivium Using SAT Solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 63\u201376. Springer, Heidelberg (2008)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-31087-4_18","volume-title":"Advanced Research in Applied Artificial Intelligence","author":"P. Gro\u00dfmann","year":"2012","unstructured":"Gro\u00dfmann, P., H\u00f6lldobler, S., Manthey, N., Nachtigall, K., Opitz, J., Steinke, P.: Solving Periodic Event Scheduling Problems with SAT. In: Jiang, H., Ding, W., Ali, M., Wu, X. (eds.) IEA\/AIE 2012. LNCS, vol.\u00a07345, pp. 166\u2013175. Springer, Heidelberg (2012)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Kaiss, D., Skaba, M., Hanna, Z., Khasidashvili, Z.: Industrial strength SAT-based alignability algorithm for hardware equivalence verification. In: Proc. FMCAD, pp. 20\u201326 (2007)","DOI":"10.1109\/FAMCAD.2007.37"},{"issue":"1-4","key":"10_CR13","first-page":"209","volume":"2","author":"V.M. Manquinho","year":"2006","unstructured":"Manquinho, V.M., Marques-Silva, J.P.: On using cutting planes in pseudo-Boolean optimization. JSAT\u00a02(1-4), 209\u2013219 (2006)","journal-title":"JSAT"},{"issue":"5","key":"10_CR14","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Trans. Comput.\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. DAC, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"10_CR16","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.\u00a02(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"10_CR17","unstructured":"Roussel, O., Manquinho, V.: Pseudo-Boolean and Cardinality Constraints, Frontiers in Artificial Intelligence and Applications, vol. 185, ch. 22, pp. 695\u2013733. IOS Press (2009)"},{"key":"10_CR18","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)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N. S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing Learned Clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 237\u2013243. Springer, Heidelberg (2009)"},{"issue":"115-125","key":"10_CR20","first-page":"10","volume":"2","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a02(115-125), 10\u201313 (1968)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"issue":"1","key":"10_CR21","first-page":"565","volume":"32","author":"L. Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: portfolio-based algorithm selection for SAT. J. Artif. Int. Res.\u00a032(1), 565\u2013606 (2008)","journal-title":"J. Artif. Int. Res."}],"container-title":["Lecture Notes in Computer Science","KI 2012: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33347-7_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T08:04:52Z","timestamp":1620115492000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33347-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642333460","9783642333477"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33347-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}