Multiple sequence alignment is a central and challenging problem in Bioinformatics. Several approaches to it have been tried, some very specialised (heuristic search based on progressive alignment) and some using generic techniques (genetic algorithms, dynamic programming, branch-and-cut). I describe a prototype SAT-based approach that sometimes finds better alignments than standard alignment packages. It is much slower but will be improved in future work.