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
Representative Encodings to Translate Finite CSPs into SAT
May 2014
BaHH14
Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, focussing on two specific encodings: the representative-sparse encoding, already proposed albeit not thoroughly tested, and a new representative-order encoding ...
In proceedings
Pedro Barahona, Steffen Hölldobler, Nguyen Van Hau
Helmut Simonis
Integration of AI and OR Techniques in Constraint Programming
Lecture Notes in Computer Science
Springer
-
8451
251-267
978-3-319-07045-2
-
DOI: 10.1007/978-3-319-07046-9_18
-
Publication files
- click here to download - pdf 299 KB
Export formats
Pedro Barahona and Steffen Hölldobler and Nguyen Van Hau, Representative Encodings to Translate Finite CSPs into SAT, in: Helmut Simonis (eds), Integration of AI and OR Techniques in Constraint Programming, Lecture Notes in Computer Science, Springer, Vol. 8451, ISBN 978-3-319-07045-2, Pag. 251-267, DOI: 10.1007/978-3-319-07046-9_18, May 2014.
<a href="/people/members/view.php?code=7e27bc13fad97e99cd21ea6914d55659" class="author">Pedro Barahona</a>, Steffen Hölldobler and Nguyen Van Hau, <b>Representative Encodings to Translate Finite CSPs into SAT</b>, in: Helmut Simonis (eds), <u>Integration of AI and OR Techniques in Constraint Programming</u>, Lecture Notes in Computer Science, <a href="http://www.springer.com" title="Link to external entity..." target="_blank" class="publisher">Springer</a>, Vol. 8451, ISBN 978-3-319-07045-2, Pag. 251-267, <i>DOI: 10.1007/978-3-319-07046-9_18</i>, May 2014.
@inproceedings {BaHH14, author = {Pedro Barahona and Steffen H\"olldobler and Nguyen Van Hau}, editor = {Helmut Simonis}, title = {Representative Encodings to Translate Finite CSPs into SAT}, booktitle = {Integration of AI and OR Techniques in Constraint Programming}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = {8451}, pages = {251-267}, isbn = {978-3-319-07045-2}, note = {DOI: 10.1007/978-3-319-07046-9_18}, abstract = {Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, focussing on two specific encodings: the representative-sparse encoding, already proposed albeit not thoroughly tested, and a new representative-order encoding ...}, month = {May}, year = {2014}, }
Publication's urls
/publications/view.php?code=61fb3e34e554495023c390add658c669
/publications/view.php?code=BaHH14
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