{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T01:41:27Z","timestamp":1768441287338,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661575","type":"print"},{"value":"9783319661582","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66158-2_43","type":"book-chapter","created":{"date-parts":[[2017,8,22]],"date-time":"2017-08-22T03:24:38Z","timestamp":1503372278000},"page":"671-686","source":"Crossref","is-referenced-by-count":13,"title":["Optimizing SAT Encodings for Arithmetic Constraints"],"prefix":"10.1007","author":[{"given":"Neng-Fa","family":"Zhou","sequence":"first","affiliation":[]},{"given":"H\u00e5kan","family":"Kjellerstrand","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,23]]},"reference":[{"key":"43_CR1","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I Ab\u00edo","year":"2012","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) 45, 443\u2013480 (2012)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"43_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-10428-7_9","volume-title":"Principles and Practice of Constraint Programming","author":"I Ab\u00edo","year":"2014","unstructured":"Ab\u00edo, I., Stuckey, P.J.: Encoding linear constraints into SAT. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 75\u201391. Springer, Cham (2014). doi: 10.1007\/978-3-319-10428-7_9"},{"key":"43_CR3","volume-title":"Compilers: Principles","author":"AV Aho","year":"2007","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles. Techniques. Addison-Wesley, Tools Boston (2007)"},{"key":"43_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-540-85958-1_23","volume-title":"Principles and Practice of Constraint Programming","author":"I Araya","year":"2008","unstructured":"Araya, I., Neveu, B., Trombettoni, G.: Exploiting common subexpressions in numerical CSPs. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 342\u2013357. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-85958-1_23"},{"key":"43_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. 5584, pp. 181\u2013194. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_19"},{"key":"43_CR6","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825\u2013885 (2009)"},{"issue":"1","key":"43_CR7","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/s10009-004-0171-8","volume":"8","author":"C Bartzis","year":"2006","unstructured":"Bartzis, C., Bultan, T.: Efficient BDDs for bounded arithmetic constraints. Int. J. Softw. Tools Technol. Transf. (STTT) 8(1), 26\u201336 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"issue":"4","key":"43_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1177352.1177354","volume":"38","author":"L Bordeaux","year":"2006","unstructured":"Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: a comparative survey. ACM Comput. Surv. 38(4), 1\u201354 (2006)","journal-title":"ACM Comput. Surv."},{"key":"43_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-2821-6","volume-title":"Logic Minimization Algorithms for VLSI Synthesis","author":"RK Brayton","year":"1984","unstructured":"Brayton, R.K., Hachtel, G.D., McMullen, C.T., Sangiovanni-Vincentelli, A.L.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, Dordrecht (1984)"},{"issue":"12","key":"43_CR10","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., Truszczy\u0144ski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92\u2013103 (2011)","journal-title":"Commun. ACM"},{"issue":"1\u20132","key":"43_CR11","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.artint.2004.01.006","volume":"162","author":"M Cadoli","year":"2005","unstructured":"Cadoli, M., Schaerf, A.: Compiling problem specifications into SAT. Artif. Intell. 162(1\u20132), 89\u2013120 (2005)","journal-title":"Artif. Intell."},{"key":"43_CR12","unstructured":"Chen, J.: A new SAT encoding of the at-most-one constraint. In: Proceedings of the 9th International Workshop of Constraint Modeling and Reformulation (2010)"},{"key":"43_CR13","unstructured":"Crawford, J.M., Baker, A.B.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: AAAI, pp. 1092\u20131097 (1994)"},{"key":"43_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). doi: 10.1007\/11817963_11"},{"key":"43_CR15","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. 3569, pp. 61\u201375. Springer, Heidelberg (2005). doi: 10.1007\/11499107_5"},{"issue":"1\u20134","key":"43_CR16","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 2(1\u20134), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"43_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-04244-7_29","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"T Feydy","year":"2009","unstructured":"Feydy, T., Stuckey, P.J.: Lazy clause generation reengineered. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 352\u2013366. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04244-7_29"},{"key":"43_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1007\/978-3-540-74970-7_59","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"M Gavanelli","year":"2007","unstructured":"Gavanelli, M.: The log-support encoding of CSP into SAT. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 815\u2013822. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74970-7_59"},{"key":"43_CR19","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: IJCAI, p. 386 (2007)"},{"key":"43_CR20","unstructured":"Gent, I.P.: Arc consistency in SAT. In: ECAI, pp. 121\u2013125 (2002)"},{"key":"43_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-85958-1_10","volume-title":"Principles and Practice of Constraint Programming","author":"J Huang","year":"2008","unstructured":"Huang, J.: Universal booleanization of constraint models. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 144\u2013158. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-85958-1_10"},{"key":"43_CR22","unstructured":"Iwama, K., Miyazaki, S.: SAT-varible complexity of hard combinatorial problems. In: IFIP Congress, vol. 1, pp. 253\u2013258 (1994)"},{"key":"43_CR23","unstructured":"Jackson, D., Abstractions, S.: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"43_CR24","unstructured":"Li, C.M.: Integrating equivalency reasoning into davis-putnam procedure. In: AAAI, pp. 291\u2013296 (2000)"},{"issue":"4\u20135","key":"43_CR25","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1017\/S1471068412000130","volume":"12","author":"A Metodi","year":"2012","unstructured":"Metodi, A., Codish, M.: Compiling finite domain constraints to SAT with BEE. Theor. Pract. Log. Program. 12(4\u20135), 465\u2013483 (2012)","journal-title":"Theor. Pract. Log. Program."},{"key":"43_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-319-10428-7_42","volume-title":"Principles and Practice of Constraint Programming","author":"R Nieuwenhuis","year":"2014","unstructured":"Nieuwenhuis, R.: The intsat method for integer linear programming. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 574\u2013589. Springer, Cham (2014). doi: 10.1007\/978-3-319-10428-7_42"},{"issue":"6","key":"43_CR27","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract davis-putnam-logemann-loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"43_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-23219-5_23","volume-title":"Principles and Practice of Constraint Programming","author":"P Nightingale","year":"2015","unstructured":"Nightingale, P., Spracklen, P., Miguel, I.: Automatically improving SAT encoding of constraint problems through common subexpression elimination in savile row. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 330\u2013340. Springer, Cham (2015). doi: 10.1007\/978-3-319-23219-5_23"},{"issue":"3","key":"43_CR29","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357\u2013391 (2009)","journal-title":"Constraints"},{"key":"43_CR30","series-title":"Artificial Intelligence: Foundations, Theory, and Algorithms","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-21810-6","volume-title":"Bridging Constraint Satisfaction and Boolean Satisfiability","author":"J Petke","year":"2015","unstructured":"Petke, J.: Bridging Constraint Satisfaction and Boolean Satisfiability. Artificial Intelligence: Foundations, Theory, and Algorithms. Springer, Heidelberg (2015)"},{"key":"43_CR31","volume-title":"Handbook of Constraint Programming","author":"F Rossi","year":"2006","unstructured":"Rossi, F., van Beek, P., Walsh, T.: Handbook of Constraint Programming. Elsevier, Amsterdam (2006)"},{"issue":"1","key":"43_CR32","first-page":"1","volume":"26","author":"T Soh","year":"2017","unstructured":"Soh, T., Banbara, M., Tamura, N.: Proposal and evaluation of hybrid encoding of CSP to SAT integratin order and log encodings. Int. J. Artif. Intell. Tools 26(1), 1\u201329 (2017)","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"4","key":"43_CR33","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/s10601-014-9165-7","volume":"19","author":"M Stojadinovic","year":"2014","unstructured":"Stojadinovic, M., Maric, F.: meSAT: multiple encodings of CSP to SAT. Constraints 19(4), 380\u2013403 (2014)","journal-title":"Constraints"},{"issue":"2","key":"43_CR34","doi-asserted-by":"crossref","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 14(2), 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"43_CR35","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/j.artint.2016.06.002","volume":"238","author":"M Veksler","year":"2016","unstructured":"Veksler, M., Strichman, O.: Learning general constraints in CSP. Artif. Intell. 238, 135\u2013153 (2016)","journal-title":"Artif. Intell."},{"key":"43_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-45349-0_32","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2000","author":"T Walsh","year":"2000","unstructured":"Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441\u2013456. Springer, Heidelberg (2000). doi: 10.1007\/3-540-45349-0_32"},{"issue":"2","key":"43_CR37","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Inf. Process. Lett. 68(2), 63\u201369 (1998)","journal-title":"Inf. Process. Lett."},{"key":"43_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-319-28228-2_4","volume-title":"Practical Aspects of Declarative Languages","author":"N-F Zhou","year":"2016","unstructured":"Zhou, N.-F., Kjellerstrand, H.: The picat-SAT compiler. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016. LNCS, vol. 9585, pp. 48\u201362. Springer, Cham (2016). doi: 10.1007\/978-3-319-28228-2_4"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66158-2_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T13:14:24Z","timestamp":1570022064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66158-2_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661575","9783319661582"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66158-2_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}