{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T01:14:42Z","timestamp":1768439682106,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319282275","type":"print"},{"value":"9783319282282","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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-319-28228-2_4","type":"book-chapter","created":{"date-parts":[[2016,1,8]],"date-time":"2016-01-08T11:54:42Z","timestamp":1452254082000},"page":"48-62","source":"Crossref","is-referenced-by-count":18,"title":["The Picat-SAT Compiler"],"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":[[2016,1,9]]},"reference":[{"key":"4_CR1","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Bjork, M.: Successful SAT encoding techniques. JSAT Addendum (2009)","DOI":"10.3233\/SAT190085"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1093\/qjmam\/4.2.236","volume":"IV","author":"AD Booth","year":"1951","unstructured":"Booth, A.D.: A signed binary multiplication technique. Q. J. Mech. Appl. Math. IV, 236\u2013240 (1951)","journal-title":"Q. J. Mech. Appl. Math."},{"issue":"4","key":"4_CR4","doi-asserted-by":"publisher","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":"4_CR5","doi-asserted-by":"publisher","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, Boston (1984)"},{"issue":"12","key":"4_CR6","doi-asserted-by":"publisher","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"},{"key":"4_CR7","unstructured":"Chen, J.: A new SAT encoding of the at-most-one constraint. In: Proceeding of the 9th International Workshop of Constraint Modeling and Reformulation (2010)"},{"key":"4_CR8","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":"4_CR9","volume-title":"Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method","year":"2014","unstructured":"Boulanger, J.L. (ed.): Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, New York (2014)"},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10601-013-9148-0","volume":"19","author":"KG Francis","year":"2014","unstructured":"Francis, K.G., Stuckey, P.J.: Explaining circuit propagation. Constraints 19(1), 1\u201329 (2014)","journal-title":"Constraints"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Gavanelli, M.: The log-support encoding of CSP into SAT. In: CP, pp. 815\u2013822 (2007)","DOI":"10.1007\/978-3-540-74970-7_59"},{"key":"4_CR12","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: IJCAI, pp. 386\u2013392 (2007)"},{"key":"4_CR13","unstructured":"Ian Gent, P.: Arc consistency in SAT. In: ECAI, pp. 121\u2013125 (2002)"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1287\/ijoc.14.4.345.2826","volume":"14","author":"P Hentenryck Van","year":"2002","unstructured":"Van Hentenryck, P.: Constraint and integer programming in OPL. INFORMS J. Comput. 14, 345\u2013372 (2002)","journal-title":"INFORMS J. Comput."},{"key":"4_CR15","first-page":"144","volume-title":"Lecture Notes in Computer Science","author":"Jinbo Huang","year":"2008","unstructured":"Huang, J.: Universal Booleanization of constraint models. In: CP, pp. 144\u2013158 (2008)"},{"key":"4_CR16","first-page":"253","volume":"1","author":"K Iwama","year":"1994","unstructured":"Iwama, K., Miyazaki, S.: SAT-varible complexity of hard combinatorial problems. IFIP Congress 1, 253\u2013258 (1994)","journal-title":"IFIP Congress"},{"key":"4_CR17","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"issue":"4\u20135","key":"4_CR18","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1017\/S1471068414000337","volume":"14","author":"EK Jackson","year":"2014","unstructured":"Jackson, E.K.: A module system for domain-specific languages. Theory Pract. Logic Program. 14(4\u20135), 771\u2013785 (2014)","journal-title":"Theory Pract. Logic Program."},{"key":"4_CR19","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1613\/jair.3531","volume":"43","author":"P Jeavons","year":"2012","unstructured":"Jeavons, P., Petke, J.: Local consistency and SAT-solvers. JAIR 43, 329\u2013351 (2012)","journal-title":"JAIR"},{"key":"4_CR20","unstructured":"Karatsuba, A., Ofman, Y.: Multiplication of many-digital numbers by automatic computers. In: Proceeding the USSR Academy of Sciences, vol. 145 pp. 293\u2013294 (1962)"},{"key":"4_CR21","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359\u2013363 (1992)"},{"key":"4_CR22","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2004)"},{"issue":"8","key":"4_CR23","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76\u201382 (2009)","journal-title":"Commun. ACM"},{"key":"4_CR24","unstructured":"Marriott, K., Stuckey, P.J., De Koninck, L., Samulowitz, H.: A MiniZinc tutorial. http:\/\/www.minizinc.org\/downloads\/doc-latest\/minizinc-tute.pdf"},{"issue":"4\u20135","key":"4_CR25","doi-asserted-by":"publisher","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. Theory Pract. Logic Program. 12(4\u20135), 465\u2013483 (2012)","journal-title":"Theory Pract. Logic Program."},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.R.: MiniZinc: towards a standard CP modelling language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529\u2013543. Springer, Heidelberg (2007)"},{"key":"4_CR27","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.artint.2012.08.001","volume":"193","author":"J Rintanen","year":"2012","unstructured":"Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45\u201386 (2012)","journal-title":"Artif. Intell."},{"key":"4_CR28","volume-title":"High Quality Test Pattern Generation and Boolean Satisfiability","author":"R Drechsler","year":"2012","unstructured":"Drechsler, R., Eggersgl\u00fc\u00df, S.: High Quality Test Pattern Generation and Boolean Satisfiability. Springer, New York (2012)"},{"issue":"4","key":"4_CR29","doi-asserted-by":"publisher","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"},{"key":"4_CR30","unstructured":"Sugar. bach.istc.kobe-u.ac.jp\/sugar\/"},{"issue":"2","key":"4_CR31","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 14(2), 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-31612-8_37","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"T Tanjo","year":"2012","unstructured":"Tanjo, T., Tamura, N., Banbara, M.: Azucar: a SAT-based CSP solver using compact order encoding. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 456\u2013462. Springer, Heidelberg (2012)"},{"key":"4_CR33","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 - CP 2000","author":"T Walsh","year":"2000","unstructured":"Walsh, T.: SAT $$v$$ CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, p. 441. Springer, Heidelberg (2000)"},{"key":"4_CR34","unstructured":"Zhou, N.-F., Fruhman, J.: A User\u2019s Guide to Picat. http:\/\/picat-lang.org"},{"key":"4_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25883-6","volume-title":"Constraint Solving and Planning with Picat","author":"N-F Zhou","year":"2015","unstructured":"Zhou, N.-F., Kjellerstrand, H., Fruhman, J.: Constraint Solving and Planning with Picat. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-28228-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,13]],"date-time":"2020-09-13T19:03:08Z","timestamp":1600023788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-28228-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319282275","9783319282282"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-28228-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}