The MiniZinc-SAT Compiler

dc.contributor	王弘倫	zh_TW
dc.contributor	Wang, Hung-Lung	en_US
dc.contributor.author	Hendrik Bierlee	zh_TW
dc.contributor.author	Hendrik Bierlee	en_US
dc.date.accessioned	2020-12-14T09:07:55Z
dc.date.available	2020-09-16
dc.date.available	2020-12-14T09:07:55Z
dc.date.issued	2020
dc.description.abstract	none	zh_TW
dc.description.abstract	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.	en_US
dc.description.sponsorship	資訊工程學系	zh_TW
dc.identifier	G060847070S
dc.identifier.uri	http://etds.lib.ntnu.edu.tw/cgi-bin/gs32/gsweb.cgi?o=dstdcdr&s=id=%22G060847070S%22.&
dc.identifier.uri	http://rportal.lib.ntnu.edu.tw:80/handle/20.500.12235/111750
dc.language	英文
dc.subject	none	zh_TW
dc.subject	Optimization	en_US
dc.subject	Constraint Programming	en_US
dc.subject	SAT	en_US
dc.title	The MiniZinc-SAT Compiler	zh_TW
dc.title	The MiniZinc-SAT Compiler	en_US

Files

Now showing 1 - 1 of 1