[11] Marco Cadoli and Andrea Schaerf. Compiling problem specifications into SAT. **Artificial Intelligence**,
162(1-2):89–120, 2005.

[12] Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design**, 19(1):7–34, 2001.**
[13] Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In TACAS 2004**, pages 168–176. LNCS 2988, Springer, 2004.**
[14] Philippe Codognet and Daniel Diaz. Compiling Constraints in clp(FD). **Journal of Logic Programming**,
27(3):185–226, 1996.

[15] Stephen A. Cook. The complexity of theorem-proving procedures. In **STOC '71: Proceedings of the**
third annual ACM symposium on Theory of computing**, pages 151–158. ACM Press, 1971.**
[16] Manuel Costa, Jon Crowcroft, Miguel Castro, Antony I. T. Rowstron, Lidong Zhou, Lintao Zhang, and Paul Barham. Vigilante: End-to-end containment of internet worm epidemics. **ACM Transactions on**
Computer Systems**, 26(4), 2008.**
[17] Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM**, 5(7):394–397, 1962.**
[18] Martin Davis and Hilary Putnam. A Computing Procedure for Quantification Theory. Journal of Association for Computing Machinery**, 7(3):201–215, 1960.**
[19] Tristan Denmat, Arnaud Gotlieb, and Mireille Ducass´e. An abstract interpretation based combinator for modelling while loops in constraint programming. In **CP'07: Proceedings of the 13th international** conference on Principles and practice of constraint programming**, LNCS 4741. Springer, 2007.**
[20] Duˇsan Djuki,¸ Vladimir Jankovi´c, Ivan Mati´c, and Nikola Petrovi´c. **The IMO Compendium 1959-2004**.

Springer, 2005.

[21] Agostino Dovier, Andrea Formisano, and Enrico Pontelli. An empirical study of constraint logic programming and answer set programming solutions of combinatorial problems. **Jorunal of Experimental**
and Theoretical Artificial Intelligence**, 21(2):79–121, 2009.**
[22] Niklas E´en and Niklas S¨orensson. An Extensible SAT-solver. In **Theory and Applications of Satisfiability**
Testing (SAT 2003)**, LNCS 2919, pages 502–518. Springer, 2004.**
[23] Uwe Egly. On different structure-preserving translations to normal form. Journal of Symbolic Computation**, 22(2):121–142, 1996.**
[24] Antonio J. Fern´andez and Patricia M. Hill. A comparative study of eight constraint programming languages over the boolean and finite domains. Constraints**, 5(3):275–301, 2000.**
[25] Carsten Fuhs, J¨urgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, Ren´e Thiemann, and Harald Zankl. Sat solving for termination analysis with polynomial interpretations. In **Theory and Applications**
of Satisfiability Testing - SAT 2007**, LNCS 4501, pages 340–354. Springer, 2007.**
[26] M. R. Garey and D. S. Johnson. Computers and Intractability**. W. H. Freeman, New York, 1979.**
[27] Martin Gebser, Benjamin Kaufmann, Andr´e Neumann, and Torsten Schaub. clasp **: A conflict-driven**
answer set solver. In Logic Programming and Nonmonotonic Reasoning**, LNCS 4483, pages 260–265.**
Springer, 2007.

[28] Allen Van Gelder. Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics**, 156(2):230–243, 2008.**
[29] I.P. Gent, E. Macintyre., P. Prosser, and T. Walsh. The constraidness of search. In **Proceedings of**
AAAI-96**, pages 246–252, Menlo Park, AAAI Press/MIT Press., 1996.**
[30] Enrico Giunchiglia, Yuliya Lierler, and Marco Maratea. SAT-Based Answer Set Programming. In The Nineteenth National Conference on Artificial Intelligence (AAAI 2004)**, pages 61–66. AAAI Press / The**
MIT Press, 2004.

[31] Enrico Giunchiglia, Yuliya Lierler, and Marco Maratea. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning**, 36(4):345–377, 2006.**
[32] John Harrison. Meta theory and reflection in theorem proving: a survey and critique. Technical Report CRC-053, SRI International Cambridge Computer Science Research Center, 1995.

[33] Pascal Van Hentenryck. The OPL Optimization Programming Language**. The MIT Press, 1999.**
[34] Holger H. Hoos. SAT-encodings, search space structure, and local search performance. In **Proceedings**
of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI 99**, pages 296–303.**
Morgan Kaufmann, 1999.

[35] Jinbo Huang. Universal booleanization of constraint models. In **Principles and Practice of Constraint**
Programming - CP 2008, LNCS 5202, pages 144–158. Springer, 2008.