王弘倫Wang, Hung-LungHendrik BierleeHendrik Bierlee2020-12-142020-09-162020-12-142020http://etds.lib.ntnu.edu.tw/cgi-bin/gs32/gsweb.cgi?o=dstdcdr&s=id=%22G060847070S%22.&http://rportal.lib.ntnu.edu.tw:80/handle/20.500.12235/111750noneCombinatorial (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.noneOptimizationConstraint ProgrammingSAT