{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:00:27Z","timestamp":1725796827193},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319092836"},{"type":"electronic","value":"9783319092843"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_26","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"351-366","source":"Crossref","is-referenced-by-count":3,"title":["Simplifying Pseudo-Boolean Constraints in Residual Number Systems"],"prefix":"10.1007","author":[{"given":"Yoav","family":"Fekete","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Codish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Aavani, A., Mitchell, D.G., Ternovska, E.: New encoding for translating pseudo-Boolean constraints into SAT. In: Frisch, A.M., Gregory, P. (eds.) SARA. AAAI (2013)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Mayer-Eichberger, V.: A new look at BDDs for pseudo-Boolean constraints. J. Artif. Intell. Res. (JAIR)\u00a045, 443\u2013480 (2012)","DOI":"10.1613\/jair.3653"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11527695_1","volume-title":"Theory and Applications of Satisfiability Testing","author":"C. Ans\u00f3tegui","year":"2005","unstructured":"Ans\u00f3tegui, C., Many\u00e0, F.: Mapping problems with finite-domain variables into problems with Boolean variables. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 1\u201315. Springer, Heidelberg (2005)"},{"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.\u00a02833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"key":"26_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-1315-1","volume-title":"Logic-based 0-1 constraint programming","author":"P. Barth","year":"1996","unstructured":"Barth, P.: Logic-based 0-1 constraint programming. Kluwer Academic Publishers, Norwell (1996)"},{"issue":"2-3","key":"26_CR6","first-page":"6","volume":"7","author":"D.L. Berre","year":"2010","unstructured":"Berre, D.L., Parrain, A.: The Sat4j library, rel. 2.2. JSAT\u00a07(2-3), 6\u201359 (2010)","journal-title":"JSAT"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Bixby, R.E., Boyd, E.A., Indovina, R.R.: MIPLIB: A test set of mixed integer programming problems. SIAM News 25, 16 (1992)","DOI":"10.21236\/ADA455431"},{"issue":"3-4","key":"26_CR8","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1002\/rsa.10004","volume":"19","author":"C. Borgs","year":"2001","unstructured":"Borgs, C., Chayes, J.T., Pittel, B.: Phase transition and finite-size scaling for the integer partitioning problem. Random Struct. Algorithms\u00a019(3-4), 247\u2013288 (2001)","journal-title":"Random Struct. Algorithms"},{"key":"26_CR9","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Deciding CLU logic formulas via Boolean and pseudo-Boolean encodings. In: Proc. Intl. Workshop on Constraints in Formal Verification, CFV 2002 (2002)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-19835-9_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Codish","year":"2011","unstructured":"Codish, M., Fekete, Y., Fuhs, C., Schneider-Kamp, P.: Optimal base encodings for pseudo-Boolean constraints. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 189\u2013204. Springer, Heidelberg (2011)"},{"key":"26_CR12","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press (2009)"},{"key":"26_CR13","first-page":"1092","volume-title":"AAAI","author":"J.M. Crawford","year":"1994","unstructured":"Crawford, J.M., Baker, A.B.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: Hayes-Roth, B., Korf, R.E. (eds.) AAAI, vol.\u00a02, pp. 1092\u20131097. AAAI Press \/ The MIT Press, Seattle (1994)"},{"issue":"1-4","key":"26_CR14","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":"26_CR15","unstructured":"Manquinho, V., Roussel, O.: Pseudo-Boolean competition (2012), http:\/\/www.cril.univ-artois.fr\/PB12\/"},{"issue":"1-4","key":"26_CR16","doi-asserted-by":"crossref","first-page":"103","DOI":"10.3233\/SAT190018","volume":"2","author":"V.M. Manquinho","year":"2006","unstructured":"Manquinho, V.M., Roussel, O.: The first evaluation of Pseudo-Boolean solvers (PB 2005). Journal on Satisfiability, Boolean Modeling and Computation (JSAT)\u00a02(1-4), 103\u2013143 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation (JSAT)"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Metodi, A., Codish, M., Stuckey, P.J.: Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems. J. Artif. Intell. Res. (JAIR)\u00a046, 303\u2013341 (2013)","DOI":"10.1613\/jair.3809"},{"issue":"2","key":"26_CR18","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/s10601-008-9061-0","volume":"14","author":"N. Tamura","year":"2009","unstructured":"Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints\u00a014(2), 254\u2013272 (2009)","journal-title":"Constraints"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,21]],"date-time":"2020-08-21T22:01:33Z","timestamp":1598047293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}