The theory and practice of satis ability solvers has experienced dramatic advances [1] in the past couple of decades. This fact attracted the attention of researchers that work with hard combinatorial problems [2, 6, 9{11, 5] with the hope that if suitable and e cient SAT encodings of these problems can be constructed, then SAT solvers can be used to solve large instances of such problems e ectively. On the other hand, researchers working in the area of SAT and SMT solvers observed that by combining the combinatorial search capabilities of SAT solvers with mathematical reasoning abilities of computer algebra systems (CAS), one could attack combinatorial problems in a way that either of these approaches by themselves may not be able to [2]. Further, SAT researchers have been interested in hard combinatorial problems and produced signi cant breakthroughs [7, 8, 3, 4] using either customtailored highly-tuned SAT solvers implementations or by combining the SAT and CAS paradigms. In our own work, we are using SAT solvers to solve hard combinatorial problems, such as Williamson Hadamard matrices, D-optimal matrices, complex Golay pairs and so forth. These problems are de ned via the fundamental concept of autocorrelation [12]. It turns out that both these approaches (namely hand-tuned SAT solvers and SAT+CAS combinations) 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 rmly believe that the interaction between SAT researchers and combinatorialists will continue to be very fruitful. Acknowledgement This is joint work with Vijay Ganesh at the University of Waterloo.
? Supported by an NSERC grant