Combinatorial (optimization) problems occur in nature and society. Constraint programming allows users to model such problems by declaring the variables and their constraints in a model. A powerful way to solve the model is by encoding it purely as Boolean algebra, specifically a SAT formula, and then use a specialized SAT solver. This thesis reports on the encoding process for the newly developed MiniZinc-SAT compiler -- a SAT compiler that supports and mixes three different encoding methods -- and offers an experimental evaluation.

[AGMES16] Ignasi Ab´ıo, Graeme Gange, Valentin Mayer-Eichberger, and Peter J Stuckey. On cnf encodings of decision diagrams. In International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pages 1–17. Springer, 2016.
[ANO+12] Ignasi Ab´ıo, Robert Nieuwenhuis, Albert Oliveras, Enric Rodr´ıguez Carbonell, and Valentin Mayer-Eichberger. A new look at bdds for pseudo-boolean constraints. Journal of Artificial Intelligence Research, 45:443–480, 2012.
[ANOR13] Ignasi Ab´ıo, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodr´ıguez-Carbonell. A parametric approach for smaller and better encodings of cardinality constraints. In Christian Schulte, editor, Proceedings of Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013, volume 8124 of Lecture Notes in Computer Science, pages 80–96. Springer, 2013.
[APS20] Gilles Audemard, Lo¨ıc Paulev´e, and Laurent Simon. SAT heritage: A community-driven effort for archiving, building and running more than thousand SAT solvers. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings,volume 12178 of Lecture Notes in Computer Science, pages 107–113. Springer, 2020.
[AS14][AS14] Ignasi Ab´ıo and Peter J Stuckey. Encoding linear constraints into sat. In International Conference on Principles and Practice of Constraint Programming, pages 75–91. Springer, 2014.
[BHN14] Pedro Barahona, Steffen H¨olldobler, and Van-Hau Nguyen. Efficient sat-encoding of linear CSP constraints. In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2014, Fort Lauderdale, FL, USA, January 6-8, 2014, 2014.
[Bie13] Armin Biere. Lingeling, plingeling and treengeling entering the sat competition 2013. Proceedings of SAT competition, 2013:1, 2013.
[BSTW16] Gleb Belov, Peter J Stuckey, Guido Tack, and Mark Wallace. Improved linearization of constraint programming models. In International Conference on Principles and Practice of Constraint Programming, pages 49–65. Springer, 2016.
[Che10] Jingchao Chen. A new sat encoding of the at-most-one constraint. Proceedings of Constraint Modelling and Reformulation, 2010.
[Dav13] Jessica Davies. Solving MaxSAT by decoupling optimization and satisfaction. PhD thesis, University of Toronto, 2013.
[DLL62] Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394–397, 1962.
[ES06] Niklas E´en and Niklas S¨orensson. Translating pseudo-boolean constraints into sat. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, 2006.
[FSS11] Thibaut Feydy, Zoltan Somogyi, and Peter J. Stuckey. Half reification and flattening. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 286–301. Springer, 2011.
[Gav07] Marco Gavanelli. The log-support encoding of CSP into SAT. In Christian Bessiere, editor, Principles and Practice of Constraint Program- ming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, volume 4741 of Lecture Notes in Computer Science, pages 815–822. Springer, 2007.
[GO20] LLC Gurobi Optimization. Gurobi optimizer reference manual, 2020.
[Hua08] Jinbo Huang. Universal booleanization of constraint models. In International Conference on Principles and Practice of Constraint Pro- gramming, pages 144–158. Springer, 2008.
[IMM19] Alexey Ignatiev, Ant´onio Morgado, and Jo˜ao Marques-Silva. RC2: an efficient maxsat solver. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):53–64, 2019.
[JKRM19] Saurabh Joshi, Prateek Kumar, Sukrut Rao, and Ruben Martins. Open-wbo-inc: Approximation strategies for incomplete weighted maxsat. J. Satisf. Boolean Model. Comput., 11(1):73–97, 2019.
[MML14] Ruben Martins, Vasco M. Manquinho, and Inˆes Lynce. Open-wbo: A modular maxsat solver,. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume8561 of Lecture Notes in Computer Science, pages 438–445. Springer, 2014.
[NM15] Van-Hau Nguyen and Son T Mai. A new method to encode the at-most-one constraint into sat. In Proceedings of the Sixth International Symposium on Information and Communication Technology, pages 46–53, 2015.
[NSB+07] Nicholas Nethercote, Peter J Stuckey, Ralph Becket, Sebastian Brand, Gregory J Duck, and Guido Tack. Minizinc: Towards a standard cp modelling language. In International Conference on Principles and Practice of Constraint Programming, pages 529–543. Springer, 2007.
[OSC09] Olga Ohrimenko, Peter J. Stuckey, and Michael Codish. Propagation via lazy clause generation. Constraints: An International Journal, 14(3):357–391, 2009.
[PJ11] Justyna Petke and Peter Jeavons. The order encoding: From tractable csp to tractable sat. In International Conference on Theory and Applications of Satisfiability Testing, pages 371–372. Springer, 2011.
[PS15] Tobias Philipp and Peter Steinke. Pblib – a library for encoding pseudo- boolean constraints into cnf. In Marijn Heule and Sean Weaver, editors, Theory and Applications of Satisfiability Testing – SAT 2015, volume 9340 of Lecture Notes in Computer Science, pages 9–16. Springer In- ternational Publishing, 2015.
[RVBW06] Francesca Rossi, Peter Van Beek, and Toby Walsh. Handbook of Con- straint Programming. Elsevier, 2006.
[SdlBM+05] Peter J. Stuckey, Maria J. Garc´ıa de la Banda, Michael J. Maher, Kim Marriott, John K. Slaney, Zoltan Somogyi, Mark Wallace, and Toby Walsh. The G12 project: Mapping solver independent models to efficient solutions. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, volume 3709 of Lecture Notes in Computer Science, pages 13–16. Springer, 2005.
[Sil18] Anthony Silvestre. Solving NP-hard problems using quantum comput- ing. (Unpublished BSc. thesis at Monash University, Australia), 2018.
[ST13] Peter J. Stuckey and Guido Tack. Minizinc with functions. In Carla P. Gomes and Meinolf Sellmann, editors, Integration of AI and OR Tech- niques in Constraint Programming for Combinatorial Optimization Problems, 10th International Conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18-22, 2013. Proceedings, volume 7874 of Lecture Notes in Computer Science, pages 268–283. Springer, 2013.
[TB08] Naoyuki Tamura and Mutsunori Banbara. Sugar: A csp to sat trans- lator based on order encoding. Proceedings of the Second International CSP Solver Competition, pages 65–69, 2008.
[TBS13] Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh. Compiling pseudo-boolean constraints to SAT with order encoding. In 25th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2013, Herndon, VA, USA, November 4-6, 2013, pages 1020–1027. IEEE Computer Society, 2013.
[TTB11] Tomoya Tanjo, Naoyuki Tamura, and Mutsunori Banbara. A compact and efficient sat-encoding of finite domain CSP. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, AnnArbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 375–376. Springer, 2011.
[TTKB09] Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear csp into sat. Constraints, 14(2):254–272, 2009.
[ZK16] Neng-Fa Zhou and H˚akan Kjellerstrand. The picat-sat compiler. In International Symposium on Practical Aspects of Declarative Languages, pages 48–62. Springer, 2016.
[ZKF15] Neng-Fa Zhou, H˚akan Kjellerstrand, and Jonathan Fruhman. Constraint Solving and Planning with Picat. Springer Briefs in Intelligent