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
Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT
November 2013
NgVB2013
Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that can not only be efficiently generated, but also efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, namely a previously proposed log-direct encoding, as well as a new combination, the log-order encoding. Experiments conducted on different domain problems with these hierarchical encodings demonstrate their significant promise in practice ... the log-direct encoding significantly outperforms the direct encoding (typically by one or two orders of magnitude) ... the log-order encoding is clearly competitive with the order encoding although more studies are required to clearly understand the tradeoff between the fewer variables and longer clauses in the former when expressing complex CSP constraints.
In proceedings
Hau Nguyen Van, Miroslav N. Velev, Pedro Barahona
Alexander Brodsky
Proc. 2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI2013)
-
IEEE Computer Society Press
Washington DC, USA
-
1028-1035
978-1-4799-2971-9
1082-3409
-
http://dx.doi.org/10.1109/ICTAI.2013.154
Export formats
Hau Nguyen Van and Miroslav N. Velev and Pedro Barahona, Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT, in: Alexander Brodsky (eds), Proc. 2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI2013), IEEE Computer Society Press, Washington DC, USA, ISBN 978-1-4799-2971-9, ISSN 1082-3409, Pag. 1028-1035, (http://dx.doi.org/10.1109/ICTAI.2013.154), November 2013.
Hau Nguyen Van, Miroslav N. Velev and <a href="/people/members/view.php?code=7e27bc13fad97e99cd21ea6914d55659" class="author">Pedro Barahona</a>, <b>Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT</b>, in: Alexander Brodsky (eds), <u>Proc. 2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI2013)</u>, IEEE Computer Society Press, Washington DC, USA, ISBN 978-1-4799-2971-9, ISSN 1082-3409, Pag. 1028-1035, (<a href="http://dx.doi.org/10.1109/ICTAI.2013.154" target="_blank">url</a>), November 2013.
@inproceedings {NgVB2013, author = {Hau Nguyen Van and Miroslav N. Velev and Pedro Barahona}, editor = {Alexander Brodsky}, title = {Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT}, booktitle = {Proc. 2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI2013)}, publisher = {IEEE Computer Society Press}, address = {Washington DC, USA}, pages = {1028-1035}, isbn = {978-1-4799-2971-9}, issn = {1082-3409}, url = {http://dx.doi.org/10.1109/ICTAI.2013.154}, abstract = {Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that can not only be efficiently generated, but also efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, namely a previously proposed log-direct encoding, as well as a new combination, the log-order encoding. Experiments conducted on different domain problems with these hierarchical encodings demonstrate their significant promise in practice ... the log-direct encoding significantly outperforms the direct encoding (typically by one or two orders of magnitude) ... the log-order encoding is clearly competitive with the order encoding although more studies are required to clearly understand the tradeoff between the fewer variables and longer clauses in the former when expressing complex CSP constraints.}, keywords = {SAT Encodings; Hierarchical Encodings}, month = {November}, year = {2013}, }
Publication's urls
/publications/view.php?code=f02b075e501e313a14273c2065b98e68
/publications/view.php?code=NgVB2013
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