[60] Steven David Prestwich. CNF encodings. In Armin Biere, **Marijn Heule, Hans van Maaren, and Toby**
Walsh, editors, Handbook of Satisfiability**, pages 75–97 [3], 2009.**
[61] Olivier Roussel and Christophe Lecoutre. XML representation of constraint networks: Format xcsp 2.1.

CoRR**, abs/0902.2362, 2009.**
[62] Joachim Schimpf. Logical loops. In **Logic Programming, 18th International Conference, ICLP 2002**,
LNCS 2401, pages 224–238. Springer, 2002.

[63] Barbara M. Smith, Kostas Stergiou, and Toby Walsh. Using auxiliary variables and implied constraints to model non-binary problems. In AAAI/IAAI**, pages 182–187. AAAI Press / The MIT Press, 2000.**
[64] Peter J. Stuckey, Maria J. Garc´ıa de la Banda, Michael J. Maher, Kim Marriott, John K. Slaney, Zoltan Somogyi, Mark Wallace, and Toby Walsh. The g12 project: Mapping solver independent models to efficient solutions. In Principles and Practice of Constraint Programming - CP 2005**, LNCS 3709,** pages 13–16. Springer, 2005.

[65] Tommi Syrj¨anen and Ilkka Niemel¨a. The smodels system. In **Logic Programming and Nonmonotonic**
Reasoning, 6th International Conference, LPNMR 2001**, LNCS 2173, pages 434–438. Springer, 2001.**
[66] Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear csp into sat. Constraints**, 14(2):254–272, 2009.**
[67] Christian Thiffault, Fahiem Bacchus, and Toby Walsh. Solving Non-clausal Formulas with DPLL Search.

In Principles and Practice of Constraint Programming - CP 2004**, LNCS 3258, pages 663–678. Springer,**
2004.

[68] Nikolai Tillmann and Jonathan de Halleux. Pex-white box test generation for .net. In **Tests and Proofs**
- TAP 2008**, LNCS 4966, pages 134–153. Springer, 2008.**
[69] Milan Todorovi´c. Applications of non-CNF solvers. Master's thesis, Faculty of Mathematics, University of Belgrade, 2011.

[70] G. S. Tseitin. On the complexity of derivations in propositional calculus. In **Studies in Constructive**
Mathematics and Mathematical Logic (Part II), pages 115–125. Consultants Bureau, 1968. (Also in The Automation of Reasoning**, Springer-Verlag, 1983.).**
[71] Milan Seˇsum. Logical cryptoanalysis of des. Master's thesis, Fa ˇ **culty of Mathematics, University of**
Belgrade, 2009.

[72] Toby Walsh. SAT v CSP. In Principles and Practice of Constraint Programming - CP 2000**, LNCS**
1894, pages 441–456. Springer, 2000.

[73] Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. SATzilla: portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research**, 32:565–606, 2008.**
[74] Hantao Zhang, Dapeng Li, and Haiou Shen. A SAT based scheduler for tournament schedules. In The Seventh International Conference on Theory and Applications of Satisfiability Testing - SAT 2004**, 2004.**
Online Proceedings.

[75] Lintao Zhang and Sharad Malik. The Quest for Efficient Boolean Satisfiability Solvers. In **Automated**
Deduction (CADE 2002)**, LNCS 2392, pages 295–313. Springer, 2002.**