Exploiting Model Checking in Constraint-based Approaches to the Protein Folding Problem ?

In this paper we show how model checking can be used to drive the solution search in the protein folding problem encoded as a constraint optimization problem. The application of the model checking technique allows us to distinguish between meaningful protein confor- mations and bad ones. This classification of conformations can then be exploited by constraint solvers to significatively prune the search space of the protein folding problem. Furthermore, our approach seems promising in the study of folding/energy landscapes of proteins. In this paper we show how model checking can be used to drive the solution search in the protein folding problem encoded as a constraint optimization problem. Given the molecular composition of a protein, i.e., a list of amino acids, known as its primary structure, the protein structure prediction (or pro- tein folding) problem consists in determining the 3D shape (tertiary structure or conformation) that the protein assumes in normal conditions in biological environments (5). To solve the protein folding problem it is crucial to determine the confor- mations of the amino acid sequences in the 3D space with minimum energy. It is indeed widely accepted that a state with minimum energy represents the protein's natural shape (a.k.a. the native conformation). The energy of a con- formation can be modeled by means of suitable energy functions, which express the energy level in terms of the interactions between pairs of amino acids (3). Since the protein folding problem is extremely complex, it is often simplified in several respects. A common simplification consists in using lattice space models to restrict the admissible positions of the amino acids in the space (11). The energy function can be simplified as well, e.g., by adopting the 20×20 poten-