Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem

• Autorzy: Morgado A. , Marques-Silva J.
• Języki publikacji: EN

Abstrakty

EN

Phylogenetic analysis is a widely used technique, for example in biology and biomedical sciences. The construction of phylogenies can be computationally hard. A commonly used solution for construction of phylogenies is to start from a set of biological species and relations among those species. This work addresses the case where the relations among species are specified as quartet topologies. Moreover, the problem to be solved consists of computing a phylogeny that satisfies the maximum number of quartet topologies. This is referred to as the Maximum Quartet Consistency (MQC) problem, and represents an NP-hard optimization problem. MQC has been solved both heuristically and exactly. Exact solutions forMQC include those based on Constraint Programming, Answer Set Programming, Pseudo-Boolean Optimization (PBO), and SatisfiabilityModulo Theories (SMT). This paper provides a comprehensive overview of the use of PBO and SMT for solving MQC, and builds on recent work in this area. Moreover, the paper provides new insights on how to use SMT for solving optimization problems, by focusing on the concrete case of MQC. The solutions based on PBO and SMT were experimentally compared with other exact solutions. The results show that for instances with small percentage of quartet errors, the models based on SMT can be competitive, whereas for instances with higher number of quartet errors the PBO models are more efficient.

Słowa kluczowe

EN

maximum quartet consistency; optimization algorithms; pseudo-boolean optimization; satisfiability modulo theories

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 3/4
• Strony: 363--389
• Opis fizyczny: Bibliogr. 64 poz., tab.

Twórcy

autor

Morgado A.

autor

Marques-Silva J.

• Complex & Adaptive Systems Laboratory, School of Computer Science and Informatics, University College of Dublin, Ireland,

Bibliografia

• [1] Aloul, F., Ramani, A., Markov, I., Sakallah, K. A.: Generic ILP versus Specialized 0-1 ILP: An Update, International Conference on Computer-Aided Design, November 2002.
• [2] Armando, A., Castellini, C., Giunchiglia, E.: SAT-Based Procedures for Temporal Reasoning, European Conference on Planning, 1999.
• [3] Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers, International Journal on Software Tools for Technology Transfer, 11(1), 2009, 69-83.
• [4] Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over Boolean and linear mathematical propositions, International Conference on Automated Deduction, 2002.
• [5] Bailleux, O., Boufkhad, Y.: Full CNF Encoding: The Counting Constraints Case, International Conference on Theory and Applications of Satisfiability Testing, 2004.
• [6] Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB), http://www.SMT-LIB.org, 2008.
• [7] Ben-Dor, A., Chor, B., Graur, D., Ophir, R., Pelleg, D.: From four-taxon trees to phylogenies (preliminary report): the case of mammalian evolution, International Conference on Computational Molecular Biology, 1998.
• [8] Berry, V., Jiang, T., Kearney, P., Li, M., Wareham, T.: Quartet Cleaning: Improved Algorithms and Simulations, European Symposium on Algorithms, 1999.
• [9] Biere, A.: PicoSAT Essentials, Journal on Satisfiability, Boolean Modeling and Computation, 4(2-4), 2008, 75-97, Available at http://fmv.jku.at/picosat.
• [10] Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs, Tools and Algorithms for the Construction and Analysis of Systems, March 1999.
• [11] Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability, IOS Press, Amsterdam, The Netherlands, 2009, ISBN 1586039296, 9781586039295.
• [12] Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver, Design Automation Conference, June 2003.
• [13] Chen, P., Keutzer, K.: Towards True Crosstalk Noise Analysis, International Conference on Computer-Aided Design, November 1999.
• [14] Cimatti, A.: Beyond Boolean SAT: Satisfiability Modulo Theories, International Workshop on Discrete Event Systems, 2008.
• [15] Claessen, K., Eén, N., Sheeran, M., Sörensson, N.: SAT-solving in practice, International Workshop on Discrete Event Systems, 2008.
• [16] Cook, S.: The Complexity of Theorem Proving Procedures, Annual Symposium on Theory of Computing, 1971.
• [17] Coudert, O.: Two-Level Logic Minimization, An Overview, Integration, The VLSI Journal, 17(2), October 1993, 677-691.
• [18] Déharbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code, International Conference on Software Engineering and Formal Methods, 2003.
• [19] Dunham, E., Dugan, V., Kaser, E., Perkins, S., Brown, I., Holmes, E., Taubenberger, J.: Different evolutionary trajectories of European avian-like and classical swine H1N1 influenza A viruses, Journal of Virology, 83(11),March 2009.
• [20] Dutertre, B., de Moura, L.: The YICES SMT Solver, Technical report, SRI International, Available at http://yices.csl.sri.com.
• [21] Een, N., Sörensson, N.: An Extensible SAT Solver, International Conference on Theory and Applications of Satisfiability Testing, May 2003.
• [22] Een, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT, Journal on Satisfiability, Boolean Modeling and Computation, 2, March 2006, 1-26, Available at http://minisat.se/MiniSat+.html.
• [23] Erdös, P., Steel, M., Székely, L., Warnow, T.: Constructing Big Trees from Short Sequences, International Colloquium on Automata, Languages, and Programming, 1997.
• [24] Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT Solving for Termination Analysis with Polynomial Interpretations, International Conference on Theory and Applications of Satisfiability Testing, 2007.
• [25] Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures, Computer-Aided Verification, 2004.
• [26] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp : A Conflict-Driven Answer Set Solver, International Conference on Logic Programming and Nonmonotonic Reasoning, 2007, Available at http://www.cs.uni-postdam.de/clasp.
• [27] Giunchiglia, E., Lierler, Y., Maratea, M.: Answer Set Programming Based on Propositional Satisfiability, Journal of Automated Reasoning, 36(4), 2006, 345-377, Available at htpp://www.cs.utexas.edu/users/tag/cmodels.html.
• [28] Graca, A., Marques-Silva, J., Lynce, I., Oliveira, A.: Efficient Haplotype Inference with Pseudo-Boolean Optimization, Algebraic Biology, 2007.
• [29] Gramm, J., Niedermeier, R.: A fixed-parameter algorithm for minimum quartet inconsistency, Computer and System Sciences, 67(4), December 2003, 723-741.
• [30] Gusfield, D.: Algorithms on Strings, Trees, and Sequences: Computer Science and Computational Biology, Cambridge University Press, January 1997, ISBN 0521585198.
• [31] Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSat: a New Weighted Max-SAT Solver, International Conference on Theory and Applications of Satisfiability Testing, May 2007.
• [32] Jiang, T., Kearney, P., Li, M.: Orchestrating quartets: approximation and data correction, Foundations of Computer Science, 1998.
• [33] Letz, R.: Lemma andModel Caching in Decision Procedures for Quantified Boolean Formulas, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, July 2002.
• [34] Li, C., Many`a, F., Planes, J.: New Inference Rules for Max-SAT, Journal of Artificial Intelligence Research, 30, 2007, 321-359.
• [35] Liu, L., Truszczynski, M.: Pbmodels - Software to Compute Stable Models by Pseudoboolean Solvers, International Conference on Logic Programming and Nonmonotonic Reasoning, 2005, Available at http://www.cs.uky.edu/ai/pbmodels.
• [36] Lynce, I., Marques-Silva, J.: Efficient Haplotype Inference with Boolean Satisfiability, National Conference on Artificial Intelligence, July 2006.
• [37] Manquinho, V., Marques-Silva, J.: Search Pruning Conditions for Boolean Optimization, European Conference on Artificial Intelligence, August 2000.
• [38] Manquinho, V., Marques-Silva, J.: Search Pruning Techniques in SAT-Based Branch-and-BoundAlgorithms for the Binate Covering Problem, IEEE Transactions on Computer-AidedDesign, 21(5),May 2002, 505-516.
• [39] Manquinho, V., Marques-Silva, J.: Satisfiability-Based Algorithms for Boolean Optimization, Annals of Mathematics and Artificial Intelligence, 40(3-4), March 2004, 353-372, Available at http://sat.inescid. pt/bsolo.
• [40] Manquinho, V., Marques-Silva, J.: Effective Lower Bounding Techniques for Pseudo-Boolean Optimization, Design, Automation and Testing in Europe Conference, March 2005.
• [41] Manquinho, V., Roussel, O.: The First Evaluation of Pseudo-Boolean Solvers (PB'05), Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4), 2006, 103-143.
• [42] Marques-Silva, J.: Practical applications of Boolean Satisfiability, InternationalWorkshop on Discrete Event Systems, 2008.
• [43] Marques-Silva, J., Sakallah, K.: GRASP: A New Search Algorithm for Satisfiability, International Conference on Computer-Aided Design, November 1996.
• [44] McMillan, K.: Interpolation and SAT-based Model Checking, Computer-Aided Verification, 2003.
• [45] Morgado,A.,Marques-Silva, J.: Combinatorial optimization solutions for theMaximumQuartet Consistency Problem, Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, December 2008.
• [46] Morgado, A., Marques-Silva, J.: A Pseudo-Boolean Solution to theMaximum Quartet Consistency Problem, Workshop on Constraint Based Methods for Bioinformatics, May 2008.
• [47] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Engineering an Efficient SAT Solver, Design Automation Conference, June 2001.
• [48] de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, 2008, Available at http://research.microsoft.com/en-us/um/redmond/projects/z3.
• [49] Niemel¨a, I., Simons, P.: Smodels - An Implementation of the Stable Model andWell-Founded Semantics for Normal LP, International Conference on Logic Programming and Nonmonotonic Reasoning, 1997, Available at http://www.tcs.hut.fi/Software/smodels.
• [50] Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems, International Conference on Theory and Applications of Satisfiability Testing, 2006.
• [51] Pizzuti, C.: Computing Prime Implicants by Integer Programming, International Conference on Tools with Artificial Intelligence, November 1996.
• [52] Rintanen, J., Heljanko, K., Niemel¨a, I.: Planning as Satisfiability: parallel plans and algorithms for plan search, Artificial Intelligence, 170(12-13), 2006, 1031-1080.
• [53] Sebastiani, R.: Lazy Satisability Modulo Theories, Journal on Satisfiability, Boolean Modeling and Computation, 3(3-4), 2007, 141-224.
• [54] Selman, B., Kautz, H.: Planning as Satisfiability, European Conference on Artificial Intelligence, 1992.
• [55] Sheeran,M., Singh, S., St°almarck, G.: Checking Safety PropertiesUsing Induction and a SAT Solver, Formal Methods in Computer-Aided Design, 2000.
• [56] Sheini, H., Sakallah, K.: Pueblo: A Hybrid Pseudo-Boolean SAT Solver, Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4), 2006, 165-189.
• [57] Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints, International Conference on Principles and Practice of Constraint Programming, 2005.
• [58] Smith, A., Veneris, A., Ali, M., Viglas, A.: Fault diagnosis and logic debugging using Boolean satisfiability, IEEE Transactions on Computer-Aided Design, 24(10), 2005, 1606-1621.
• [59] Villa, T., Kam, T., Brayton, R. K., Sangiovanni-Vincentelli, A. L.: Explicit and Implicit Algorithms for Binate Covering Problems, IEEE Transactions on Computer-Aided Design, 16(7), July 1997, 677-691.
• [60] Wu, G., Kao, M., Lin, G., You, J.: Reconstructing phylogenies from noisy quartets in polynomial time with a high success probability, Algorithms for Molecular Biology, 3(1), 2008.
• [61] Wu, G., Lin, G., You, J.: Quartet Based Phylogeny Reconstruction with Answer Set Programming, International Conference on Tools with Artificial Intelligence, 2004.
• [62] Wu, G., You, J., Lin, G.: A Lookahead Branch-and-Bound Algorithm for the Maximum QuartetConsistency Problem, Workshop on Algorithms in Bioinformatics, October 2005.
• [63] Wu, G., You, J., Lin, G.: Quartet-Based Phylogeny Reconstruction with Answer Set Programming, IEEE/ACM Transactions on Computational Biology and Bioinformatics, 4(1), 2007, 139-152.
• [64] Zohari, S., Gyarmati, P., Ejdersund, A., Berglof, U., Thoren, P., Ehrenberg,M., Czifra, G., Belak, S.,Waldenstrom, J., Olsen, B., Berg., M.: Phylogenetic analysis of the non-structural (NS) gene of influenza A viruses isolated from mallards in Northern Europe in 2005, Journal of Virology, 5(147), 2008.