Back to first pageBack to first page Centre for Artificial Intelligence of UNL
Browse our site
You are here:

Publication details

Go back
Publication details
Main information
SAT Encodings of Finite CSPs
February 2015
HauBH15
This thesis studies SAT encodings of CSPs and aims at: 1) conducting a comprehensively profound study of SAT encodings of CSPs by separately investigating encodings of CSP domains and constraints; 2) proposing new SAT encodings of CSP domains; 3) proposing new SAT encoding of the at-most-one constraint, which is essential for encoding CSP variables; 4) introducing the redundant encoding and the hybrid encoding that aim to benefit from both two efficient and common SAT encodings (i.e., the sparse and order encodings) by using the channeling constraint (a term used in Constraint Programming) for SAT; and 5) revealing interesting guidelines on how to choose an appropriate SAT encoding in the way that one can exploit the availability of many efficient SAT solvers to solve CSPs efficiently and effectively. Experiments show that the proposed encodings and guidelines improve the state-of-the-art SAT encodings of CSPs.
Ph. D. dissertation
Hau Nguyen Van
Steffen Hölldobler, Pedro Barahona
TU Dresden
-
-
Export formats
Hau Nguyen Van, SAT Encodings of Finite CSPs, Steffen Hölldobler and Pedro Barahona (superv.), TU Dresden, February 2015.
<b>Hau Nguyen Van</b>, <u>SAT Encodings of Finite CSPs</u>, Steffen Hölldobler and <a href="/people/members/view.php?code=7e27bc13fad97e99cd21ea6914d55659" class="supervisor">Pedro Barahona</a> (superv.), TU Dresden, February 2015.
@phdthesis {HauBH15, author = {Hau Nguyen Van}, title = {SAT Encodings of Finite CSPs}, school = {TU Dresden}, note = {Steffen H\"olldobler and Pedro Barahona (superv.); }, abstract = {This thesis studies SAT encodings of CSPs and aims at: 1) conducting a comprehensively profound study of SAT encodings of CSPs by separately investigating encodings of CSP domains and constraints; 2) proposing new SAT encodings of CSP domains; 3) proposing new SAT encoding of the at-most-one constraint, which is essential for encoding CSP variables; 4) introducing the redundant encoding and the hybrid encoding that aim to benefit from both two efficient and common SAT encodings (i.e., the sparse and order encodings) by using the channeling constraint (a term used in Constraint Programming) for SAT; and 5) revealing interesting guidelines on how to choose an appropriate SAT encoding in the way that one can exploit the availability of many efficient SAT solvers to solve CSPs efficiently and effectively. Experiments show that the proposed encodings and guidelines improve the state-of-the-art SAT encodings of CSPs.}, keywords = {SAT Encodings; SAT Solvers; CP solvers}, month = {February}, year = {2015}, }
Publication's urls
/publications/view.php?code=48b5768b90e83fea232c64cfed33092f
/publications/view.php?code=HauBH15
Go back
Centre for Artificial Intelligence of UNL
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541

Fundacao_FCT