Solving De Novo Peptide Sequencing via Propositional Logic

We present here a new construction for approaching the problem of determining all aminoacid sequences compatible with the mass spectrum of an unknown peptide as a propositional satisfiability problem. Data obtained from the mass spectrometry analysis of a generic compound, constituted, according to specific chemical rules, by a sequence of components, are used to build up a propositional logic formula, whose models represent coherent interpretations of the set of spectral data and can be used to generate all possible correct results of the sequencing itself. The proposed approach has several advantages on other known approaches, both from the accuracy and from the computational points of view. Successful results on real-world peptide analysis problems are presented.