ABSTRACT. The theory and practice of satisfiability solvers has experienced dramatic advances in the past couple of decades. This fact attracted the attention of researchers that work with hard combinatorial problems with the hope that if suitable and efficient SAT encodings of these problems can be established, then SAT solvers can be used to solve large instances of such problems effectively. On the other hand SAT researchers have been interested in hard combinatorial problems and produced significant breakthroughs using custom-tailored highly-tuned SAT solvers implementations. It turns out that both these approaches have had a number of successes already and it is safe to assume that a lot more successes are to be expected in the near future. Combinatorics is a vast source of very hard and challenging problems, often containing thousands of discrete variables, and i firmly believe that the interaction between SAT researchers and combinatorialists will continue to be very fruitful.