Complete and Exact Peptide Sequence Analysis Based on Propositional Logic

  • Renato Bruni


Peptides are the short polymeric molecules constituting all the proteins. They are formed by the linking of amino acids, and the determination of the amino acid sequence of a peptide is a fundamental issue in many areas of chemistry, medicine and biology. Nowadays, the prevalent approach to this problem consists in using a mass spectrometry analysis. This gives information about the molecular weight of the full peptidic molecule and of its fragments. Such information should be used in order to find the sequence, but this constitutes, in the general case, a difficult mathematical problem. After a brief overview of the approaches proposed in literature, and of their features and limits, the chapter describes in detail a promising one based on propositional logic. Differently from the others, this approach can be proved to be complete and exact.


Integer Linear Program Propositional Logic Conjunctive Normal Form Truth Assignment Component Amino Acid 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



The author is grateful to Prof. G. Gianfranceschi and to Prof. G. Koch for stimulating discussions and for providing details on the biological aspects of the problems. Partially reprinted from [5] with permission from Elsevier. Italian Patent number: MI2002A000396. International Patent Application number: PCT/IB03/00714.


  1. 1.
    B. Aspvall, M.F. Plass, and R.E. Tarjan. A linear time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters8, 121–123 (1979)CrossRefGoogle Scholar
  2. 2.
    V. Bafna and N. Edwards. On de novo interpretation of tandem mass spectra for peptide identification. In Annual Conference on Research in Computational Molecular BiologyRECOMB03, 9–18 (2003)Google Scholar
  3. 3.
    E. Boros, Y. Crama, and P.L. Hammer. Polynomial time inference of all valid implications for Horn and related formulae. Annals of Mathematics and Artificial Intelligence1, 21–32 (1990)CrossRefGoogle Scholar
  4. 4.
    C. Branden and J. Tooze. Introduction to Protein Structure.Garland Publishing, New York (1999)Google Scholar
  5. 5.
    R. Bruni. Solving peptide sequencing as satisfiability. Computer and Mathematics with Applications55(5), 912–923 (2008)CrossRefGoogle Scholar
  6. 6.
    R. Bruni and A. Santori. Adding a new conflict-based branching heuristic in two evolved DPLL SAT solvers. In Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability TestingSAT2004 (2004)Google Scholar
  7. 7.
    R. Bruni, G. Gianfranceschi, and G. Koch. On peptide de novo sequencing: a new approach. Journal of Peptide Science11, 225–234 (2005)PubMedCrossRefGoogle Scholar
  8. 8.
    G. Casella and C.P. Robert. Monte Carlo Statistical Methods. Springer, New York (2006)Google Scholar
  9. 9.
    V. Chandru and J.N. Hooker. Extend Horn clauses in propositional logic. Journal of the ACM38, 203–221 (1991)CrossRefGoogle Scholar
  10. 10.
    V. Chandru and J.N. Hooker. Optimization Methods for Logical Inference. Wiley, New York (1999)CrossRefGoogle Scholar
  11. 11.
    T. Chen, M.Y. Kao, M. Tepel, J. Rush, and G.M. Church. A dynamic programming approach to de novo peptide sequencing via tandem mass spectrometry. Journal of Computational Biology8(6), 571–583 (2001)PubMedCrossRefGoogle Scholar
  12. 12.
    W.F. Clocksin. Logic programming and digital circuit analysis. Journal of Logic Programming4(1), 59–82 (1987)CrossRefGoogle Scholar
  13. 13.
    M. Conforti and G. Cornuéjols. A class of logical inference problems soluble by linear programming. Journal of the ACM42(5), 1107–1113 (1995)CrossRefGoogle Scholar
  14. 14.
    V. Dancik, T.A. Addona, K.R. Clauser, J.E. Vath, and P.A. Pevzner. De novo peptide sequencing via tandem mass spectrometry. Journal of Computational Biology6, 327–342 (1999)PubMedCrossRefGoogle Scholar
  15. 15.
    M.R. Garey and D.S. Johnson. Computers and Intractability. Freeman, New York (1979)Google Scholar
  16. 16.
    J. Gu, P.W. Purdom, J. Franco, and B.W. Wah. Algorithms for the Satisfiability (SAT) Problem: A Survey. DIMACS Series in Discrete Mathematics35, 19–151, American Mathematical Society (1997)Google Scholar
  17. 17.
    R.S. Johnson and J.A. Taylor. Searching sequence databases via de novo peptide sequencing by tandem mass spectrometry. Methods in Molecular Biology146, 41–61 (2000)PubMedGoogle Scholar
  18. 18.
    H. Kleine Büning and T. Lettman. Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)Google Scholar
  19. 19.
    T.D. Lee. Fast atom bombardment and secondary ion mass spectrometry of peptides and proteins. In Methods of Protein Microcharacterization, J.E. Shively (editor) 403–441, Humana Press, NJ (1986)Google Scholar
  20. 20.
    G. Montaudo and R.P. Lattimer (editors). Mass Spectrometry of Polymers. CRC Press, Boca Raton (2001)Google Scholar
  21. 21.
    G.L. Nemhauser and L.A. Wolsey. Integer and Combinatorial Optimization.Wiley, New York (1988)Google Scholar
  22. 22.
    J.S. Schlipf, F.S. Annexstein, J.V. Franco, and R.P. Swaminathan. On finding solutions for extended horn formulas. Information Processing Letters54(3), 133–137 (1995)CrossRefGoogle Scholar
  23. 23.
    G. Siuzdak. Mass Spectrometry for Biotechnology. Academic Press, New York (1996)Google Scholar
  24. 24.
    Software system DeNovoX. ThermoFinnigan Corp. (
  25. 25.
    Software system Mass Seq. Micromass Ltd. (
  26. 26.
    Software system PEAKS. Bioinformatics Solutions Inc. (http://www.bioinformaticssolutions. com)
  27. 27.
    Software system Spectrum Mill. Agilent Technologies Inc. (
  28. 28.
    J.T. Stults. Peptide sequencing by mass spectrometry. Methods of Biochemical Analysis34, 145–201 (1990)PubMedCrossRefGoogle Scholar
  29. 29.
    J.A. Taylor and R.S. Johnson. Implementation and uses of automated de novo peptide sequencing by tandem mass spectrometry. Analytical Chemistry73, 2594–2604 (2001)PubMedCrossRefGoogle Scholar
  30. 30.
    K. Truemper. Effective Logic Computation. Wiley, New York (1998)Google Scholar
  31. 31.
    P. Van Hentenryck. Constraint satisfaction in logic programming.MIT, MA (1989)Google Scholar
  32. 32.
    D. Voet. Biochemistry. Wiley, New York (2004)Google Scholar

Copyright information

© Springer New York 2011

Authors and Affiliations

  1. 1.Department of Computer and System SciencesUniversity of Roma “Sapienza”RomeItaly

Personalised recommendations