De Novo Peptide Sequencing via Tandem Mass Spectometry and Propositional Satisfiability

Peptide analysis is one of the most important and frequent issues in biological and medical research. This holds even more after the beginning of the Proteome Project, focused indeed on the study of proteins. In particular, a basic problem is the determination of the aminoacid sequence of an unknown peptide by processing the data obtained from the tandem mass spectrometry analysis. In practical cases, due to the very large number of possible peptides, such sequencing cannot rely on data bases, and the problem is known as "peptide de novo sequencing". The problem have been approached in many ways, but most of such approaches can only solve very rough simplifications of the real problem. In particular, due to its computationally demanding nature and its inherent combinatorial nature, discrete mathematical approaches to the problem should be used. We therefore present here a new construction for approaching the problem of determining all aminoacid sequences compatible with the given spectral data as a propositional satisfiability problem. Successful results on real-world peptide analysis problems are presented.