Please use this identifier to cite or link to this item:
|Title:||The MiniZinc-SAT Compiler|
The MiniZinc-SAT Compiler
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.
|Appears in Collections:||學位論文|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.