Nicolas Fiorini

Vincent Lefort

François Chevenet

Vincent Berry

Anne-Muriel Arigon Chifolleau

CompPhy: a web-based collaborative platform for comparing phylogenies

Keywords: Evolutionary trees, Tree comparison, Online resource, Real-time collaboration

Background

Collaborative systems are emerging as a kind of tool to help people located in different places conduct joint work. Basically, they allow several persons to edit and analyze common documents in a coordinated way. Evolutionary biologists and systematicians need to communicate, share data and interact despite being separated by long distances. This applies regardless of the extent and type of joint effort involved in, for instance, studying a few genes in a metabolic pathway, or determining the phylogeny of a specific taxonomic group based on previously published *Correspondence: anne-muriel.arigon@lirmm.fr 1 Institut de Biologie Computationnelle, LIRMM, Université de Montpellier II -CNRS, Montpellier, France Full list of author information is available at the end of the article studies. Over the past few years, several collaborative tools have been proposed, such as Teamlab focused on project management, Mendeley on research papers, GitHub on software source code, ShareLaTeX on LaTeX documents and Google Drive on office documents. Unfortunately, none of these tools applies when phylogenies are the documents to be shared and jointly edited. Recently, a collaborative tool devoted to tree-building, Phylografter [START_REF] Beaulieu | Synthesizing phylogenetic knowledge for ecological research[END_REF], was developed. It aims to facilitate the process of collaborative tree-assembly while providing links to published phylogenetic hypotheses and represents a web-based content management system for phylogenetic information that provides node-by-node provenance of grafted trees. However, in this software, the collaborative aspect corresponds to the sharing of data (trees and annotations) and tree manipulation (edition, visualization, ...) is made in an asynchronous way. The bioinformatic resource proposed here, named CompPhy, is a good step forward. In a few words, CompPhy is a web platform devoted to collaborative work on phylogenies, providing facilities to jointly visualize, manipulate and mainly compare trees. Note that it allows a user to actually see on the screen changes performed by distant collaborators. This is very useful to support a phone or video conversation about a collection of trees tp overcome the need for repeated exchanges of tree files on a shared folder together with round trips with the users' separate -hence unsynchronized -tree visualization software.

Visualizing trees is a recurrent activity in evolutionary biology and systematics due to the central role of trees in these fields. This has led to the development of more than a dozen standalone software programs to visualize trees, such as TreeView [START_REF] Page | Visualizing phylogenetic trees using TreeView[END_REF], TreeDyn [START_REF] Chevenet | TreeDyn: towards dynamic graphics and annotations for analyses of trees[END_REF], Dendroscope [START_REF] Huson | Dendroscope: An interactive viewer for large phylogenetic trees[END_REF], Archaeopteryx [START_REF] Han | phyloXML: XML for evolutionary biology and comparative genomics[END_REF], FigTree [6] and most recently some web tools, such as ScripTree [START_REF] Chevenet | ScripTree: scripting phylogenetic graphics[END_REF], iTOL [START_REF] Letunic | Interactive Tree Of Life v2: online annotation and display of phylogenetic trees made easy[END_REF], jsPhyloSVG [START_REF] Smits | jsPhyloSVG: a javascript library for visualizing interactive and vector-based phylogenetic trees on the web[END_REF] and EvolView [START_REF] Zhang | EvolView, an online tool for visualizing, annotating and managing phylogenetic trees[END_REF]. Some of these tools also allow for tree annotation. This process consists of highlighting parts of trees (tips, nodes, branches, subtrees) or whole trees with various kinds of information (e.g., geographical and molecular data, references). Depending on the tool, complex annotations, such as histograms or pie charts can also be associated with subtrees to indicate the proportion of their taxa having specific properties. These are powerful tools to visualize trees individually but most of them lack features to compare trees.

Tree visualization in systematic and evolutionary biology is often done with tree comparison in mind, e.g., how does the inferred tree change when tuning this or that parameter in the inference? What is the difference between trees obtained by this or that method, or from this or that dataset? How much does a gene tree differ from the species tree? Starting from this observation, CompPhy is built with an approach symmetrical to that of the above-mentioned software: yes, it offers tree visualization features, but with tree comparison as a main focus; its name stems from "Comparing Phylogenies". Table 1 details the functionalities provided in different software and web systems with respect to the focus of the present paper. CompPhy is currently the only available service to compute and visualize consensus and supertrees in a browser (i.e., not requiring a software installation). It is also the only web-based resource enabling the collaborative edition of a tree collection during a joint work session.

Basically, there are two kinds of tree comparison situations: comparing two trees, or comparing a non-trivial number of trees. We detail both of these cases below.

Several situations require side by side display of two trees to visually highlight their differences or common parts. For instance, comparing a gene tree to a species tree allows recovery of evolutionary events that shaped a gene family history [START_REF] Goodman | Fitting the gene lineage into its species lineage, a parsimony strategy illustrated by cladograms constructed from globin sequences[END_REF]. Similarly, a parasite tree is often compared to a host tree to study co-evolutionary patterns [START_REF] Charleston | Preferential host switching by primate lentiviruses can account for phylogenetic similarity with the primate phylogeny[END_REF][START_REF] Page | Trees within trees: phylogeny and historical associations[END_REF]. Such a pairwise comparison situation is at the core of the CompPhy's interface, whose central zone allows the user to display two trees side by side or face to face depending on where they prefer the taxa names to appear. Probably the simplest way to measure the topological difference between two trees is by computing a global distance measure that separates the trees [START_REF] Robinson | Comparison of phylogenetic trees[END_REF]. This helps for clustering or ranking trees in a set. However, this does not pinpoint conflicting zones in the topologies of the two trees. Consensus methods are a useful work-around, displaying a summary of the topological signal common to the compared trees. Among tree visualization tools, Dendroscope and Mega [START_REF] Tamura | MEGA5: molecular evolutionary genetics analysis using maximum likelihood, evolutionary distance, and maximum parsimony methods[END_REF] can compute consensus trees. But, Mega only allows users to compute a consensus tree in the context of a bootstrap analysis. Dendroscope can compute several kinds of consensus but it does not highlight agreeing or disagreeing parts of the initial trees, which is however often required to identify interesting parts in the source trees. In contrast, TreeJuxtaposer [START_REF] Munzner | Treejuxtaposer: scalable tree comparison using focus+context with guaranteed visibility[END_REF] enables simultaneous comparison of several trees, notably by highlighting structural differences and similarities between trees displayed side by side. Unfortunately this software does not run on current computers. We also refer readers to DensiTree [START_REF] Bouckaert | DensiTree: making sense of sets of phylogenetic trees[END_REF], which provides a graphical summary of large collections of trees. It is however not suited to a detailed comparison of trees. Finally, for those familiar with the command line, the PAUP* [23] and PHYLIP [24] packages can be used to compute consensus trees.

In situations where a large number of trees need to be compared, consensus trees and supertrees are the most appropriate tool. Formally, consensus methods apply when all trees have exactly the same set of taxa, while supertree methods extend consensus methods to situations with unequal taxon sets [START_REF] Orp | Phylogenetic supertrees: combining information to reveal the tree of life[END_REF]. Nowadays, trees are obtained more easily by automated pipelines from genomic resources, so studies tend to encompass more trees, that rarely have the same taxon set. Supertree methods are thus a tool of choice. What is really needed there is an integrated tool that allows both tree collection management and supertree computation. Indeed, in practice, an initial set of source trees is usually obtained from a pipeline or from a tree inference software program, after which they are usually cut and pasted into a file, then several scripts and programs (e.g., [23,[START_REF] Bininda-Emonds | Getting to the roots of matrix representation[END_REF]27]) are used for the supertree inference, and the newick form of the obtained supertree is subsequently cut and pasted into another tool to display it. The analysis is usually repeated several times to generate other supertrees by changing parameters in the supertree computation or by selecting a slightly different subset of source trees. Overall, it is quite easy to get mislead in this juggling act involving different files and tools. Unfortunately, there is a real lack of tools for managing a collection of trees and building consensus and supertrees from selected trees: RadCon software [START_REF] Thorley | RadCon: Phylogenetic tree comparison and consensus[END_REF] could once be used to perform some of the above mentioned tasks, but it does not run on modern computers. Morover, there is a shortage of web tools that offer to compute supertrees, and those available do not allow tree collection management and visualization [29].

When two or more trees containing a few dozen taxa are compared, several graphical operations are needed, such as a consistent rooting of trees, a common ordering of their tips (if the potential topological disagreement allows it), differential coloration of taxa depending on the molecular, taxonomic or geographical information. Maximum comfort is achieved when these tasks can be performed in an automated way, but this can only be achieved in a tool that manages trees collectively. This excludes a good deal of the software cited above where trees have to be opened independently from one another (usually in different windows), except when scripting facilities are provided, such as in Dendroscope and ScripTree.

This outline of tree comparison functions spread out in different tree display tools, or simply missing, and the absence of tools for collaborative exploration and management of trees prompted us to develop the CompPhy web-based platform. Recent advances in web technologies now allow users to have web applications as powerful as stand-alone software. Such applications can be accessed from any operating system while avoiding cumbersome installation and parameterizing steps. Moreover, centralizing data on a server overcomes the need for renewed copies and updates of data among the various devices researchers generally use.

The next sections describe CompPhy's architecture and functionalities. Then, an example of a typical use of the platform shows how this tool can help distant scientists to collectively analyze trees.

Implementation

CompPhy is based on a classic web architecture, see Figure 1. The main part is composed of PHP modules coupled to a MySQL database. The database stores information on projects and data related to trees, such as their Newick format, annotations and commands to draw them.

The ScripTree interpreter for phylogenetic graphics is in charge of generating tree pictures [START_REF] Chevenet | ScripTree: scripting phylogenetic graphics[END_REF]. It manages tree edition and annotation. ScripTree takes text files as input to produce a tree picture: the tree in Newick format, a script for the graphical rendering and annotations in CSV format. However, users need no knowledge of ScripTree to operate CompPhy: they upload trees in Newick format and CompPhy maintains the script and annotation files Figure 1 The architecture of the CompPhy platform. Projects and their trees are stored in a relational database; ScripTree [START_REF] Chevenet | ScripTree: scripting phylogenetic graphics[END_REF] is used as the picture generating module. Perl is used for tree modifications requiring computation, e.g., restricting trees to common taxa, and as a wrapper for external tree computations modules, e.g., computing a consensus with PAUP* [23]. Users interact with CompPhy from their browser, whose content is connected to the CompPhy core essentially through the jQuery javascript framework.

according to the users' requests on its interface. Nonetheless, a dedicated zone for the MANUAL TUNING OF THE PICTURES allows users with knowledge of ScripTree to tweak these files for a more specific or elaborated tree rendering. Tree pictures are generated by ScripTree in SVG format, which allows users to interact with pictures, e.g., by pointing at taxa to be swapped, and it is now accepted by all recent browsers.

A set of Perl scripts also participates in the core of CompPhy: they modify the Newick format encoding trees when needed, e.g., to restrict them to a subset of taxa. These scripts also interface external programs such as PAUP*, PHYLIP, PhySIC_IST and Spruce, in which case format transformation is often needed. Moreover, as CompPhy is developed according to established programming frameworks, it is relatively easy to add new computational modules in the future.

The communication between the server-side of CompPhy and client browsers heavily relies on the AJAX framework, which basically makes CompPhy behave similarly to a stand-alone application in many respects, often avoiding the need to reload the whole web page in response to users' interactions. By adding different plugins to jQuery, CompPhy also handles the display, manipulation and refresh of SVG pictures on the client side, and this generally makes CompPhy more user friendly by displaying tooltips, modal boxes, etc.

CompPhy is hosted by the ATGC platform, which is managed by the French Bioinformatics Institute and coordinates the bioinformatics services for the South of France. Its servers run ≈190,000 hours each year for ≈11,000 different users from many countries.

Results

Trees are the central object handled by CompPhy. They are contained in tree collections, investigated in projects, each of which can be accessed by a declared list of users (possibly by anyone knowing the URL if the project is declared to be public). When working on a project, CompPhy's interface can be divided in four main parts, see Figure 2.

Zone 1 contains the site menu, enabling users to navigate between their projects, to edit their account details or to access the onsite manual. Zone 2 first displays the project menu and the collaborative box (on the righthand side) enabling users to coordinate their actions when jointly visualizing a project. For instance, this box allows them to indicate which person is in charge of a current edit. Below, it displays short captions of the project trees, organized in two collections (e.g., to separate gene from species trees, or host from parasite trees). Trees can be reordered within each collection and dragged to Zone 3 to be displayed in full size. Zone 3 consists of two workbenches allowing users to display two trees side-by-side when focusing on their comparison. Operations can be performed on each tree individually or on both trees jointly: (i) tools on a workbench allow to investigate the tree it contains by zooming, resizing, flipping or translating its image, or by swapping chosen subtrees (other tools are available in Zone 4, see the paragraph below on tree edition); (ii) Zone 3 also provides pairwise comparison tools that consider the two trees displayed together on the workbenches: coordinated swap of their tips, computation of their topological distance or highlighting of their topological agreement and disagreement. At the bottom of the interface, Zone 4 contains tools that may apply to more than two trees, and tools to manage other data associated with the project (see specific paragraphs below).

Our system limits impose that you upload no more than 10,000 trees covering at most 5,000 different taxa inside a same project. Please note that we also limit the number of trees during an import to 1,000 per collection. However, CompPhy's main focus is on collections of several dozen to a few hundred trees. Above this limit, you might not find it too convenient to use. CompPhy can easily handle trees containing more than 1,000 taxa. Above this limit you can still use it, but be aware that pictures will take longer times to load and to be rendered by your browser (they are in SVG format, which requires some computation time from the browser).

Collaborative work

CompPhy allows a group of users to jointly work on a project. This work can usually be done in a number of working sessions to which a variable number of persons will participate. CompPhy thus proposes synchronization tools for multi-user sessions but also asynchronous tools for communication between users present and absent for some sessions. For instance, a FORUM is associated with each project, where project members can exchange questions, agree on an analysis protocol or simply leave a summary of the member's recent work for other members who were absent at the last working session.

To coordinate users during a joint working session, CompPhy ensures that at any moment only one of them performs project changes. All members connected to the project are offered a synchronized (shared) view of the trees and tools. The view refreshes itself regularly, reflecting the edits done by the person in control. Insisting that only one person is in control at any moment avoids concurrent edits and ensures that a project stays in a coherent state. A COLLABORATIVE BOX (right-hand part of Zone 2 in Figure 2) indicates which project members are currently online, who is currently in control of the interface, and allows other members to REQUEST THE CONTROL in turn. Each request can be accepted or declined by either the control holder or the administrator. The latter can also TAKE THE CONTROL over the project at any moment. An option also enables a user to detach their browser from the activity performed by the others (SYNCHRONIZE tool). In this case, they can change the trees displayed on the workbenches but they can not make any concrete changes in the project, as this would interfere with the actions of the user in control.

Data management

Data in CompPhy is organized around the project concept, that basically pools a set of analyzed trees and associated documents. Each project has an administrator who can invite other people to become members of the project. By default, projects are created with a private status, so only the project members can access the data after being identified by CompPhy. This policy guarantees data privacy while still allowing data sharing. In contrast, a public project can be accessed by any guest to which the URL is sent. Without opening an account on CompPhy, a guest can see the project trees and examine them on the workbenches. However, no guest can make changes to the trees or data of the project.

A TODO LIST reminds project members of the next tasks to be performed in the dataset analysis. Once performed, each task can be registered as an historical point in the project TIMELINE, thus keeping track of the main analysis steps. BACKUPS of the data can be built at these intermediate moments and later restored if needed.

Additional trees can be added to a project with an UPLOAD facility. Trees of the project along with their images can be downloaded one by one from the workbenches, or by collection. Extra files related to the project can also be shared between members (DOCUMENTS section), e.g., documents explaining how the trees were obtained or papers related to study. It usually helps to have all information relative to a project available in one place. Tree pictures with sufficient resolution for publication can be downloaded, as well as trees and other data stored in the project in case a user wants to work offline.

Tree edition tools

Various tree edition facilities ease the tree comparison process. As in most tree visualization programs, it is possible to color taxa or whole subtrees (COLORIZE TREES) but, importantly, this can be done here in a coordinated way for several trees together. It is possible to alter the interleaf scale and font size (DISPLAY OPTIONS) with which trees are displayed. Once again, this can be applied to a set of selected trees. Taxa names at the tips of the trees can be changed in one or several trees, and individual trees can be renamed at any time. Zoom in and out are available for trees on the workbenches to facilitate side by side comparison of trees containing different numbers of taxa.

The tree structure itself can be changed in an automated way via several operations. First, trees can be rerooted by defining a new outgroup (REROOT tool [START_REF] Dutheil | Non-homogeneous models of sequence evolution in the Bio++ suite of libraries and programs[END_REF]). This operation can be done jointly for several trees, with several outgroup taxa being indicated in case the precise outgroup taxa differs between trees. Several outgroup levels can be indicated: when the most exterior group has no representative in some trees, a taxon from the next level is sought, and so on. The second way to alter a tree structure is by swapping branches of trees on the workbenches. This can be done on one tree (MANUAL SWAP) by selecting representative taxa of the two branches to swap, or in an automated way on the two trees in the workbenches (AUTO SWAP [START_REF] Fernau | Comparing trees via crossing minimization[END_REF]) so that taxa appear as much as possible in the same order in both trees. Another tool enables users to RESTRICT TREES to their common taxa. This can help focus on their topological disagreement, which by definition can only derive from shared taxa arranged in different ways. In particular, gene trees obtained by phyloinformatic pipelines often have different sets of taxa, simply because genes can be lost in some species over the course of evolution.

Distance, consensus and supertree computation

A commonly used distance to measure the disagreement between two trees is that proposed by [START_REF] Robinson | Comparison of phylogenetic trees[END_REF]. It counts the number of clades (or bipartitions) present in one tree but not in the other. CompPhy proposes to indicate this value for two trees on the workbenches by interfacing PHYLIP treedist program [24]. This distance originally applies to two trees with identical taxon sets, so when provided with trees on different taxon sets, CompPhy first restricts the compared trees to their common taxa, as often done in the field.

When comparing two trees with conflicting topologies, it is often useful to highlight in evidence the largest common structure they share. Users can thus drag two trees on the workbenches and ask CompPhy to compute their MAXIMUM AGREEMENT SUBTREE CONSENSUS. This consensus is defined as the subtree linking the largest set of taxa whose relative placement in the two trees is exactly the same (in rare cases where several of such sets exist, one is chosen at random). CompPhy thus first restricts the two trees to their common taxa, then it uses PAUP* [23] to compute the consensus of the two trees, and finally displays the two trees with taxa not belonging to the consensus being shaded in light grey, while taxa in the consensus are represented with their original color. Subtrees containing taxa present in just one tree are also in grey, so that the structure of the consensus tree is clearly apparent. This has a main advantage to highlight -inside each of the two compared trees -the topological part on which they agree.

The consensus feature is thus focused on the comparison of two trees. When dealing with more than two trees, supertrees offer advantages over consensus trees. For instance, supertree methods consider taxa not present in all compared trees, whereas consensus methods overlook these taxa. CompPhy gives access to two SUPERTREE COMPUTATION methods: PhySIC_IST [START_REF] Scornavacca | PhySIC_IST: cleaning source trees to infer more informative supertrees[END_REF] and Matrix Representation with Parsimony (MRP, [START_REF] Baum | Combining trees as a way of combining data sets for phylogenetic inference, and the desirability of combining gene trees[END_REF][START_REF] Ragan | CompPhy: a web-based collaborative platform for comparing phylogenies[END_REF]). When computing the supertree by the PhySIC_IST method with default parameters, the degree of agreement of the input trees is translated in the resolution level of the obtained supertree: basically, a supertree containing only a few taxa and/or being poorly resolved indicates low agreement among the input trees. Changing the parameters of PhySIC_IST or resorting to the MRP method gives users an idea of the majority signal in case of substantial disagreement among the input trees (though the MRP supertree can sometimes contain artifacts representing topological signal absent from the source trees [START_REF] Orp | Phylogenetic supertrees: combining information to reveal the tree of life[END_REF]). The MRP method is implemented via the Spruce library [27] to create the matrix representation of a set of source trees and via PAUP* to analyze the matrix with parsimony.

Discussion

Progress in computing technologies has considerably boosted the potential of web browsers, which are now a real alternative to stand-alone software for different tasks. Together with cloud sourcing facilities (data being stored online on trusted servers), they overcome the need to install specific software while still offering the possibility to access and edit data from different devices (desktop or laptop computer, smartphone, tablet), the underlying operating system as well as the place they are in (work, home, airport, visited lab). The tool presented in this paper was created under this cloud philosophy for all the reasons listed above. It is hosted on a bioinformatics platform that has been receiving for ten years requests from several hundreds to several thousands users a month.

Most of all, CompPhy relies on web technologies to be a collaborative tool. Over the course of their activity, systematic and evolutionary biologists are involved in a number of phylogenetic projects with other local or distant people, such as academics, co-workers in the industry, and students. For all of these projects, there are always cumbersome and repeated steps for exchanging the data, converting them into the format required by the tool used by each person. Moreover, for distant co-workers, there is a difficult task of explaining and discussing the changes that were done and those to be done, or simply discussing what a collection of trees highlights in one's data, which is best done by jointly visualizing the collection.

Consider the following illustration where CompPhy could be highly useful. Mr S., a PhD student, works on horizontal gene transfers (HGT) among bacteria, in collaboration with Mr B. (lab. of infectious diseases) and Mrs C. (lab. of computer science). Mr S. invites his collaborators to access the project (PROJECT SETTINGS) containing his gene trees, a comprehensive tree computed by a supermatrix approach and other documents (alignments, articles, etc). After logging onto the site, Mr B. and Mrs C. can visualize, compare and edit the tree collections of the project. They first do this asynchronously: Mr B. (from a mobile device remote from his lab) colors some taxa (COLOR TREES) in order to clarify the data; then Mrs C. edits gene trees and reroots some of them (REROOT TREES) to ease the comparison. Then they each leave a message (FORUM) to briefly explain their edits. The three of them plan a common working session during which they both connect to CompPhy and to a video conference system. Once logged onto the project, each participant can easily know who is currently in control of the interface (COLLABORATIVE BOX). During the meeting, all participants have a synchronized view (SYNCHRONIZE TOOL) and can see the tree collection changing in real time when the one in control performs the edits. Mr S. presents his first conclusions on the presence of HGTs by highlighting on the shared visualization page the species suspected to be involved in HGTs (COLOR TREES). Mr B. requests to be in control of the interface (COLLABORATIVE BOX). After several branch swaps in the species tree (MANUAL SWAP), Mr B. advocates that part of Mr S. 's conclusions are wrong due to a species group being misplaced in the supermatrix tree with respect to current taxonomic knowledge. He identifies a gene tree responsible for this topological problem (AUTOMATIC SWAP, and MAXIMUM AGREEMENT SUBTREE CONSENSUS), corrects it, then asks Mr S. to redo the supermatrix analysis. The latter then uploads the new comprehensive tree (UPLOAD TREES and TREE NAMES). Eventually, they end up with a consistent coloring of the gene trees and of the species trees showing evidence of HGT events in a particular gene tree. To use the tree pictures in an article, they standardize the taxon names in their different trees (RENAME TAXA), they add annotations corresponding to the tips of their trees to indicate taxonomic groups (MANUAL TUNING) and make a backup of the project (BACKUP tool).

Though CompPhy is designed for researchers, it can also be used for educational purposes. Practical sessions with undergraduates are ready to set up as this tool requires no specific installation: students only need a web browser for the session. Before the session, the lecturer can prepare data to be visualized by the students by creating a public project, which grants access to students as soon as they are communicated the project URL. When a lecturer wants students to perform tree analyses, he can ask them to create accounts and projects, inviting him to their project so that he can later access online or collect their grouped or individual homework.

The fact that CompPhy offers numerous features for collaborative work does not impede users from creating personal projects, i.e., hosting of the data (i.e., granting them access to an updated data whatever the computer or device used) and the various tree comparison tools.

Several extensions of CompPhy are currently being investigated, including a versioning system of individual trees. This would enable users to keep track of the various versions of their trees and hence bring the "undo" facility. Other pairwise comparison and consensus methods should be available soon. We are also planning to accept more tree formats as input (e.g., Nexus and PhyloXML) and to implement more real-time features such as onsite audio/video calls and chat.

Conclusion

CompPhy is the first online platform allowing several users to synchronously or asynchronously handle phylogenetic trees in a collaborative way. It allows them to see the actions performed by the others in real time on compared trees, which greatly facilitates joint work from distant places. Moreover, CompPhy is a unique tool pooling tree comparison operations such as restriction to common taxa, automatic branch swap, consensus and supertree computation, whose results can be readily visualized in its interface. Finally, it offers an interface for usual tree edition facilities, such as leaf and subtree coloring, subtree swapping and tree rerooting.

Figure 2

 2 Figure 2 CompPhy's main interface. Zone 1 contains the website navigation bar. Zone 2 displays the project menu, a toolbox allowing participants to coordinate when editing trees together, and the tree collections, each tree being identified by a name and a sketched picture. Zone 3 displays two workbenches on which trees can be laid down for individual observation or comparison. Zone 4 presents several tools to edit trees and manage the project.

Table 1 Tree comparison facilities of phylogeny visualizing tools

 1

	Tool	Year	Type	Annotations	Joint edit.	Cons./SuperT.	Collab.	Reference
	TreeView	2001	S.a.	No	No	No	No	[2]
	TreeMap3	2002	S.a.	Int.	Yes	No	No	[11]
	TreeDyn	2007	S.a.	Int. & scr.	Yes	No	No	[3]

Acknowledgements

This work was funded by the Programme 6ème Extinction (ANR-09-PEXT-000 PhyloSpace).

http://www.atgc-montpellier

Availability and requirements

Project name: CompPhy Project home page: http://www.atgc-montpellier.fr/ compphy/ Operating system(s): Platform independent Other requirements: A recent internet browser License: The tool is available online free of charge, and code is available under GitHub (https://github.com/Johy/ CompPhy) Any restrictions to use by non-academics: None

Competing interests

The authors declare that they have no competing interests.

Authors' contributions

AMAC and VB initiated the project. AMAC, NF and VB designed the interface and the functionalities. NF implemented the current version of CompPhy. FC updated ScriptTree to provide functionalities in CompPhy. AMAC, NF, VB and VL tested the CompPhy platform. VL maintains the ATGC platform hosting CompPhy. AMAC, NF and VB wrote the paper. FC, NF and VB produced the figures of the paper. All authors read and approved the final manuscript.


Thierry Martinez
email: thierry.martinez@inria.fr

François Fages
email: francois.fages@inria.fr

Sylvain Soliman
email: sylvain.soliman@inria.fr

Search by Constraint Propagation

Keywords: modeling languages, search, constraint programming, Horn clauses

Constraint programming is traditionally viewed as the combination of two components: a constraint model and a search procedure. In this paper we show that tree search procedures can be fully internalized in the constraint model with a fixed enumeration strategy. This approach has several advantages: 1) it makes search strategies declarative, and modeled as constraint satisfaction problems; 2) it makes it possible to express search strategies in existing front-end modeling languages supporting reified constraints without any extension; 3) it opens up constraint propagation algorithms to search constraints and to the implementation of novel search procedures based on constraint propagation. We illustrate this approach with a Horn clause extension of the MiniZinc modeling language and the modeling in this language of a variety of search procedures, including dynamic symmetry breaking procedures and limited discrepancy search, as constraint satisfaction problems. We show that this generality does not come with a significant overhead, and can in fact exhibit exponential speedups over procedural implementations, thanks to the propagation of the search constraints..

Introduction

Constraint programming is traditionally presented as the combination of two components: a constraint model and a search procedure [START_REF] Van Hentenryck | The OPL Optimization programming Language[END_REF]. Front-end modeling languages are designed for solving problems using constraint programming solvers, thus either rely on a fixed strategy (e.g. Essence [START_REF] Frisch | Essence: A constraint language for specifying combinatorial problems[END_REF]), or contain special features for specifying the search strategy for the constraint solvers (e.g. Zinc [START_REF] Nethercote | MiniZinc: Towards a standard CP modelling language[END_REF]). The modeling language Zinc, and its implementation MiniZinc 1 , succeeded in becoming a common input format across many solvers in the Constraint Programming community. In Zinc, the search procedure is specified through special annotations that are dedicated to the constraint solver [START_REF] Rafeh | Adding search to zinc[END_REF] and ignored by the other solvers.

In this paper, we show that a completely different approach for specifying search is possible, by internalizing the search procedure in the constraint model with a fixed enumeration strategy. In prin-1. it makes search strategies declarative, and modeled as constraint satisfaction problems;

2. it makes it possible to express search strategies in existing frontend modeling languages without any extension;

3. it opens up constraint propagation algorithms to search constraints and to the implementation of novel search procedures based on constraint propagation.

The idea of this transformation is to associate to each choice point a reified constraint with an auxiliary model variable for representing that choice (e.g. value enumeration, domain splitting or any constraint). The search heuristic can then be specified simply by the enumeration strategy for the choice variables. This approach is not limited to static search procedures in which all choice points are precisely known statically, but can accommodate dynamic search strategies, such as dichotomic or interval splitting search [START_REF] Simonis | Search strategies for rectangle packing[END_REF] for example. In constraint programming, dynamic search procedures rely on the values of indexicals (domain size, minimum value, etc.). They are expressed in the framework presented here by extending the enumeration strategy with annotations that assign the values of indexicals to auxiliary model variables. Static search procedures do not rely on the values of indexicals and their encodings do not need any specific support on the solver-side. The encoding of dynamic search procedures can be run through simple additions in the solvers for providing the capability to query the values of indexicals.

In this paper, to make concrete the presentation of the transformation, we consider the Zinc modeling language and introduce ClpZinc2 , a language extending Zinc with the ability to describe new relations by Horn clauses. The choice of Horn clauses as a specification language for search procedures is guided by Horn clauses being the smallest language with the addition of constraint to the store as primitive and closed by conjunction and disjunction (for expressing choices), and with a general form of recursion. Given a constraint system X (e.g. finite domains) and the Herbrand constraint system H, we describe a partial evaluation procedure to transform any terminating Horn(X + H) goal to an and/or tree with constraints over X .

Plan

In Section 2, we introduce the encoding of search strategies into constraints on the Korf's Square Packing example, showing that a couple of arithmetic constraints encode Helmut Simonis and Barry O'Sullivan's search strategy for this example, that is one of the best known search strategies. In Section 3, we generalize this approach by encoding any search strategy described as an and/or tree into reified constraints. In Section 4, we introduce the ClpZinc language for describing search strategies and describe the transformation of search procedures from Horn(X + H) to and/or trees over X . In the subsequent sections, we evaluate this approach on benchmarks of models with specific search strategies, namely: Korf's Square Packing problem in Section 5, limited discrepancy search in Section 6.1 and symmetry breaking during search in Section 6.2. In Section 7, we show how it is possible to go beyond tree search procedures by using a simple mechanism of annotations for global store, and specify optimization procedures such as Branch-and-Bound. In Section 8, we compare our approach with Search Combinators, which are another proposal for describing search strategies in Zinc. In Section 9, we conclude on some new perspectives.

Korf's Square Packing Strategy Revisited

In this section, we consider Korf's Optimal Rectangle Square Packing problem [START_REF] Korf | Optimal rectangle packing: Initial results[END_REF], i.e., given an integer n ≥ 1, find an enclosing rectangle of smallest area containing n squares from sizes 1 × 1, 2 × 2, up to n × n, without overlap. Helmut Simonis and Barry O'Sullivan proposed a complex dynamic search strategy for that problem in [START_REF] Simonis | Search strategies for rectangle packing[END_REF], that they have implemented for a specific Constraint Logic Programming solver (SICStus prolog).

Their model involves three global constraints: a geometric non-overlapping constraint over the squares, and two redundant constraints that express in each dimension that the sum of lengths of squares placed at every abscissa (resp. ordinate) should not exceed the height (resp. the width) of the enclosing rectangle. This is expressed by two "cumulative" constraints that are usually used in resource allocation and scheduling [START_REF] Caseau | Cumulative scheduling with task intervals[END_REF].

     non-overlap({(xi, yi, i × i) | 1 ≤ i ≤ n}) cumulative(∀1 ≤ x ≤ w, {i | xi ≤ x ≤ xi + i} ≤ h) cumulative(∀1 ≤ y ≤ h, {i | yi ≤ y ≤ yi + i} ≤ w)
This model that relates abscissas xi with the height h and ordinates yi with the width w gives surprisingly good results experimentally with a strategy that first fully enumerates in one dimension, e.g. xi, and then fully enumerates in the other one, yi. The enumeration strategy that Simonis and O'Sullivan proposed first makes a coarse-grained placement that splits each dimension into intervals up to one third of the square widths, from the biggest square to the smallest one and, then, the placement is refined by dichotomy, still from the biggest square to the smallest one. We show that these two enumeration strategies, interval splitting and dichotomy, can be expressed as arithmetic constraints.

Let x be a finite-domain variable and let s be the size of intervals which the domain should be split into. Interval splitting on x can be reduced to an Euclidean division with denominator s.

x = s × q + r r is a finite-domain variable left unbound between 0 and s -1, and the quotient q is a finite-domain variable that selects one of the intervals of size s where x should lay in. Therefore, interval splitting equivalents to the value enumeration of q. Now, let x be a finite-domain variable, 0 ≤ x < 2 d , to be enumerated by dichotomy. Dichotomy is equivalent to the enumeration of the values of the bits in the writing of x in base 2, from the most significant bit to the less significant one.

x = 0≤k<d x (k) 2 k
x (k) are variables of domain {0, 1}: dichotomy equivalents to the value enumeration of the d variables x (d-1) , then x (d-2) , etc. up to x (0) . It is worth noticing that the number of introduced variables is only logarithmic in the size of the domain.

We will see in the next section that this transformation of search strategies into arithmetic constraints plus simple value enumeration can be formalized generally for every tree search strategy. We will see in section 5 that this does not come with significant overhead.

Compiling And/Or Trees into Reified Constraints

In this section, we consider and/or trees with leaves with constraints over a domain X. and/or trees are widely used in constraint programming systems for representing search strategies: they can be described by constraint logic programming [START_REF] Jaffar | Constraint logic programming[END_REF], list monads in functional settings [START_REF] Bekkers | Monadic constructs for logic programming[END_REF], search combinators [START_REF] Schrijvers | Search combinators[END_REF], etc.

Definition 1. An and/or tree over a constraint domain X is either

• a constraint c over X ,

• a conjunction t ∧ t where t and t are two and/or trees,

• a disjunction t ∨ t where t and t are two and/or trees.

Sometimes, by abuse of notation, search strategies are defined directly on a search tree, whereas they are actually traversals of an and/or tree that result in a given search tree. In other words, a search tree is the result of applying a search strategy to a given instance. Definition 2. A search tree over a constraint domain X is either

• a constraint c over X , • a node (c, t ∨ t )
where c is a constraint over X , and t and t are two search trees.

Let c be a constraint and t be a search tree. We denote c ∧ t the search tree defined either by c ∧ c if t = c , or by

(c ∧ c , t0 ∨ t1) if t = (c , t0 ∨ t1).
Now, we define the usual transformation from and/or-trees to search trees, as done for instance by the CSLD resolution. For practical reasons we define this transformation inductively and therefore describe it from sequences of and/or-trees to search trees. Definition 3. The interpretation function s from sequences of and/or-trees to search trees is described as follows, by induction over the sum of the heights of the trees in the sequence.

• s( ) = , • s(c • κ) = c ∧ s(κ) • s((t ∧ t ) • κ) = s(t • t • κ) • s((t ∨ t ) • κ) = ( , s(t • κ) ∨ s(t • κ))
Definition 4. Given a CSP(X ) model M, two search trees t and t over X are equivalent w.r.t. M if:

• t and t have the same structure;

• for all path π from the root to a node in t, let c be the conjunction of the constraints labelling the nodes along π projected over the variables of M and c be the corresponding constraint for the same path π in t . We have M c ⇔ c

We shall denote this property by: t ≡M t .

Given a CSP(X ) model M and a tree search strategy represented by an and/or tree t, the generation of Zinc code proceeds by assigning an additional model variable to every or-node in the tree t, and by emitting search annotations that fix the enumeration strategy for these additional variables in a way compatible with the traversal ordering.

In Figure 2, the variable X1 is assigned to the root node, with the domain 0..5 corresponding to the arity of the node. As shown in the Zinc model generated for Example 1, each constraint labeling the leaves under this or-node appears in the model guarded by an implication checking for a particular value of X1. Therefore, when the search annotation int_search enumerates the possible values of X1, these guarded constraints are successively enabled for exploring the different branches of the tree.

More generally, the transformation presented in this paper can be seen as a constructive proof for the following theorem. We call fixed enumeration strategies the search strategies that are reduced to a sequence of variables selected in a fixed order and enumerated with the increasing value selection (indomain_min).

Theorem 1. For every pair (M, t) where M is a CSP model and t a tree search strategy described as an and/or tree, there exists a model Mt and a fixed enumeration strategy t such that s(t) ≡M+M t s(t ).

Proof. First, let us remark that in M + Mt, the variables and the constraints of M are left unchanged; only additional model variables accompanied with additional constraints are introduced in Mt.

Let us assume that we have a function that maps each or-node n of t to a model variable (n) ∈ V (Mt), such that for every pair n1, n2 of nodes of t, if (n1) = (n2), either n1 = n2 or the lowest common ancestor of n1 and n2 is an or-node.

Each constraint c that appears as a leaf of t is translated as a constraint in Mt. Let n1, . . . , n k denote the or-nodes that are traversed by the path π from the root of t to the leaf c and, for every 1 ≤ i ≤ k, let pi be the rank of the branch taken by π at node ni. We adopt the convention that branches are numbered from left to right and that the left-most branch has rank 0. Then the following constraint is posted in the MiniZinc model, for translating the leaf c:

constraint (n1)=p1 /\ . . . /\ (n k )=p k -> c;
Let X ∈ V (Mt) be one of the variables that label or-nodes. The domain of X will be 0..max{w(n) -1 | (n) = X} where w(n) denotes the width of the or-node n (i.e., the number of branches issued from n). For every or-node n k such that (n k ) = X that does not reach this maximum, the following additional constraint is posted, where (ni, pi)i denotes the or-path to n k as above:

constraint (n1)=p1 /\ . . . /\ (n k-1 )=p k-1 -> (n k ) < w(k);
To prevent enumerating on a variable X in branches where X does not occur, the following constraint imposes a fixed value to X on these branches. constraint (

(n i ,p i ) i (n k )=X (n1)!=p1 \/ . . . \/ (n k )!=p k ) -> X=0;
We should now establish the connection between the enumeration of the variables that label the or-nodes and the exploration of the and/or tree.

Search annotations have to be emitted to fix the enumeration strategy for the variables V (Mt). MiniZinc search annotations have a depth-first semantics. To reproduce the semantics of (M, t), it is thus sufficient in t to emit the annotations that select the variables in the order where their corresponding nodes are encountered following the traversal of t. The value selection strategy fixes the order in which the sub-branches are explored. For t , it can thus be reduced to the value selection indomain_min that selects the leftmost branch, by switching the values if necessary. We thus have that, by construction, (M + Mt, t ) explores the same search tree as (M, t).

Note that in order for the resulting Zinc program to have the intended semantics, we assume that the input and/or tree meets the following conditions:

1. all the variables that appear in constraints are finite-domain variables;

2. all lists are well-formed, in particular the tail of every non-empty list is a list and cannot be a variable since such a variable would be a finite-domain variable according to the previous condition (this ensures that lists can be expanded into Zinc array literals);

The following optimization is not mandatory but has been measured to give significant performance improvements, by reducing the number of generated constraints.

Proposition 1. In the particular case where a constraint c occurs under an or-node n k (possibly separated with some and-nodes) and when ¬c occurs in all other branches of n k , the constraints corresponding to the leaves c and ¬c are logically equivalent to the following constraint.

constraint (n1)=p1 /\ . . . /\ (n k-1 )=p k-1 -> ( (n k )=p k <-> c);
That is to say, the implication on the leaf c may be replaced by an equivalence and the constraints corresponding to the leaves ¬c are not posted.

This simplification can be seen in the Zinc code generated for Examples 2 and 3.

Extending Zinc with Horn Clauses 4.1 The Language ClpZinc

We propose to use Horn clauses to specify search strategies in Zinc. More precisely, given a constraint system X (e.g. finite domain constraints) and a CSP model with constraints in X , we consider search procedures that are expressible as the traversal of an and/or tree with constraints over X , i.e. an and/or tree where every leaf is either labeled by a constraint in X or, for dynamic search procedures, labeled by a query to indexicals. In addition, we consider the Prolog primitive constraint system, H, i.e. Herbrand terms with unification. The choice of Herbrand terms for representing Zinc data structures makes the language look familiar to Prolog users and other constraint logic programming (CLP) systems. Similarly, we fix the strategy as depth-first and left-to-right.

The language ClpZinc is an extension of Zinc where the item solve satisfy; in models is replaced by a goal of the form ":-goal.", and where user-defined predicates are defined by Horn clauses of the form "p(t1,. . .,tn) :-goal.".

Example 1 (Labeling). The following ClpZinc model implements the search strategy that enumerates all possible values for a given variable in ascending order. As shown in the following section, this ClpZinc model for the given goal of labeling x between 0 and 5, can be expanded to the following MiniZinc model: • a call to a user-defined predicate,

• the conjunction (A,B) or the disjunction (A;B) of two goals.

A ClpZinc clause is an item of the form p(t1,. . .,tn) :-goal. where t1 and tn are terms and goal is a ClpZinc goal. The goal part can be omitted: "p(t1,. . .,tn)." is a shorthand for "p(t1,. . .,tn) :-true.".

The search annotations of MiniZinc are accessible in goals in order to allow the composition of user-defined strategies with builtin ones. Terms are either logical variables (X, Y, Max, . . . ), numbers, or compound terms of the form p(t1,. . .,tn) where t1, . . . , and tn are terms. Model variables are a special case of compound terms, either atomic (a, b, . . . ) or array accessors (x[I,J]). Zinc arrays have been unified with Prolog-like lists to ease their enumeration in search strategies.

In Horn(X + H), arithmetic differs from Prolog. Indeed, in accordance with the theory of CLP and unlike most Prolog systems, arithmetic is supposed to be contained in X and is distinguished from H terms, e.g., "1 + 1" is undistinguishable from "2" and is not a H term. In ClpZinc, the different forms of unification, equality, and evaluation predicates that are encountered in Prolog systems (=, #=, is, . . . ) are thus all unified in a unique notion of equality, which is accessible either explicitly with the predicate =, or implicitly when predicate arguments in either X of H are unified.

Arithmetic expressions are also extended for accessing the indexicals of the model variables. For instance, the goal M = min(X) assumes that X is a model variable and unifies M with the currently known lower-bound of X. We consider the indexicals min, max, card and dom_nth (for retrieving the nth value in a variable domain). Concretely, an intermediary variable is introduced to receive the value of the indexical and search annotations are emitted for getting them with: annotation indexical_min(var int: target, var int: x); annotation indexical_max(var int: target, var int: x); annotation indexical_card(var int: target, var int: x); annotation indexical_dom_nth(var int: target, var int: x, var int: n);

These annotations require to extend the solvers to communicate the indexicals. That is the only change made to the interface of the solvers.

Example 2 (Dichotomic search). The Zinc indomain_split value selection strategy can be implemented in ClpZinc using indexicals. The predicate dichotomy/3 below expresses the bisection of a variable X that has the initial domain Min . . . Max. The bisection defined in the auxiliary predicate dichotomy/2 is iterated Depth = log 2 |X| times to ensure that the domain is reduced to a value on every leaf. dichotomy(X, Min, Max) :dichotomy(X, ceil(log(2, Max -Min + 1))).

dichotomy(X, Depth) :-Depth > 0, Middle = (min(X) + max(X)) div 2, (X <= Middle ; X > Middle), dichotomy(X, Depth -1).

dichotomy(X, 0). var 0..5: x; :-dichotomy(x, 0, 5).

The MiniZinc model generated for the given goal is var 0..5: x; var 0..5: X3; var 0..5: X5; var 0..1: X7; var 0..5: X4; var 0..5: X6; var 0..5: X2; var 0..1: X8; var 0..5: X1; var 0..1: X9; constraint X7 = 0 <-> x <= (X1 + X2) div 2; constraint X8 = 0 <-> x <= (X3 + X4) div 2; constraint X9 = 0 <-> x <= (X5 + X6) div The next example shows a partial search strategy that is not available using the usual MiniZinc search annotations. This is the interval slitting strategy introduced in [START_REF] Simonis | Search strategies for rectangle packing[END_REF] for solving Korf's packing problem [START_REF] Korf | Optimal rectangle packing: Initial results[END_REF] by making a preliminary coarse-grained filtering of the variable domains. The corresponding MiniZinc model for the given goal is var 0..5: x; var 0..1: X3; var 0..1: X4; var 0..5: X2; var 0..5: X1; constraint X3 = 0 <-> x < X1 + 2; constraint X3 = 1 -> (X4 = 0 <-> x < X2 + 2); constraint X3 = 0 -> X4 = 0; solve :: seq_search([ indexical_min(X1, x), int_search([X3], input_order, indomain_min, complete), indexical_min(X2, x), int_search([X4], input_order, indomain_min, complete) ]) satisfy;

Partial Evaluation of ClpZinc into And/Or Trees

From now on, let us assume that the initial ClpZinc goals provided in the items ":-goal." of the ClpZinc models that we consider, always terminate. That hypothesis should hold even if X only resolves fully instantiated constraints, as is the case of the static partial evaluator. Verifying termination of logic programs is a classical topic for which many results have been obtained using type systems or abstract interpretation techniques [START_REF] Bruynooghe | Termination analysis of logic programs through combination of typebased norms[END_REF]. The description of these techniques is however beyond the scope of this paper. Given a constraint system X , the partial evaluation of a Horn(X + H) goal will lead to an and/or tree with constraints over X . The partial evaluator resolves predicate calls, Herbrand constraints and fully instantiated arithmetic constraints, i.e., arithmetic tests. Since, without loss of generality, we settled for a left-to-right evaluation of Horn clauses, the and/or trees will be traversed in a similar left-toright fashion in our examples, but any other traversal order can be treated similarly (see for example Figure 1 where the branches of the and-nodes should be executed from left to right). Note that the transformation itself does not follow a strict DFS and does not either rely on the classical CSLD resolution, which would lead to a pure or-tree. It is rather defined as a continuation-based generation of the and/or tree. The precise definition is given below, where s is the initially empty partial evaluation store built along the transformation and denotes a hole around which the context is built and labelled by such a store. The unfolding of predicate calls and resolution of arithmetic tests is left out for readability reasons.

Definition 6. The transformation [[•]

]s : goal → search-tree, in the partial evaluation store s ∈ H, is defined inductively over the structure of the goal.

[[true]]s -→ s [[false]]s -→ ⊥ [[X = v]]s -→ s∧(X = v) [[c]]s -→ ∧ c s
where c is a constraint or a search annotation

[[A,B]]s -→ [[A]]s s 1 [[B]]s 1 sn [[B]]s n all s i of [[A]]s are filled with [[B]]s i i.e., [[A]]s[∀i, [[B]]s i / s i ] • if A or B changes the store, i.e., ∃s = s, s ∈ [[A]]s or [[B]]s: [[A;B]]s -→ ∨ [[A]]s [[B]]s
• if neither A nor B changes the store:

[[A;B]]s -→ ∧ s ∨ [[A]]s s [[B]]s s the leftmost leaf is [[A]]s[ / s] and its sibling [[B]]s[ / s]
The associativity of the nodes is enforced during the transformation, allowing n-ary nodes. As shown in Figure 2 for Example 1, or-nodes are flattened so that nested choices become a single large disjunction. And-nodes are similarly flattened into conjunctions. In the general case, the partial evaluation of the continuation may duplicate constraints with different partial instanciations. For instance, Figure 3 However, when the partial evaluation store is left unchanged by a choice (typically, when only constraints in X are involved), the continuation will remain undeveloped, as shown in Figure 4 for Example 2. The and/or tree is in logarithmic size with respect to the size of the domain whereas the fully expanded search tree would be in linear size.

Examples of Transformation

∨ x = 5 x = 4 x = 3 x = 2 x = 1 x = 0
∧ ∨ x > (X5 + X6) div 2 x <= (X5 + X6) div 2 indexical_max(X6, x) indexical_min(X5, x) ∨ x > (X3 + X4) div 2 x <= (X3 + X4) div 2 indexical_max(X4, x) indexical_min(X3, x) ∨ x > (X1 + X2) div 2 x <= (X1 + X2) div 2 indexical_max(X2, x) indexical_min(X1, x)

Computation Results on Korf's Square Packing Benchmark

In this section, we consider Korf's Optimal Rectangle Square Packing problem [START_REF] Korf | Optimal rectangle packing: Initial results[END_REF], i.e., given an integer n ≥ 1, find an enclosing rectangle of smallest area containing n squares from sizes 1 × 1, 2 × 2, up to n × n, without overlap. Helmut Simonis and Barry O'Sullivan proposed a complex dynamic search strategy for that problem in [START_REF] Simonis | Search strategies for rectangle packing[END_REF], which is interesting to specify and evaluate in ClpZinc.

First, the model they consider for packing the nconsecutive squares in a rectangle of size w × h can be written in MiniZinc as follows. Since the 1 × 1 square can always be placed afterward if the area w × h is big enough, the model only considers the remaining n -1 other squares. Two redundant cumulative constraints are introduced. The two last constraints break some symmetries by forcing the largest square to be in the bottom-left quadrant.

int: n; constraint diffn( x,y,[i+1|i in 1..n-1],[i+1|i in 1..n-1] ); constraint cumulative( x,[i+1|i in 1..n-1],[i+1|i in 1..n-1],h ); constraint cumulative( y,[i+1|i in 1..n-1],[i+1|i in 1..n-1],w ); constraint forall(i in 1..n-1) (x[i] <= w -i /\ y[i] <= h -i); constraint x[n-1] <= (w -n + 2) div 2; constraint y[n-1] <= (h + 1) div 2;
Second, the optimization procedure used in [START_REF] Simonis | Search strategies for rectangle packing[END_REF] enumerates all the possible sizes w × h for the enclosing rectangle by increasing area. This strategy can be internalized in the model by successively considering all the rectangles up to max_size × max_size, from the minimal area covered by the squares themselves ( 1≤i≤n i 2 ) and with bounds on w and h that are described in [START_REF] Simonis | Search strategies for rectangle packing[END_REF]: Now, the search strategy of [START_REF] Simonis | Search strategies for rectangle packing[END_REF] firsts enumerates in x and then in y, considering in each dimension a preliminary interval splitting on the origins of the squares from sizes n × n to 7 × 7, and then a dichotomic search on the origins, still by considering the biggest square first. This search strategy is implemented in ClpZinc by enumerating first on area and w to find the rectangle of smallest area first. It is worth noticing that we can combine the user-defined interval splitting strategy defined in Example 3 with the built-in dichotomic search (indomain_split). where reverse is implemented as usual with Horn clauses.

This strategy can be compared to the use of the dichotomic search only, on each dimension, from the biggest to the smallest square, relying on the native indomain_split of MiniZinc. This is indeed a good candidate for the best strategy that can be easily written in MiniZinc without the help of ClpZinc.

:: seq_search([ int_search( [area, w], input_order, indomain_min, complete ), int_search( [x[n-i] | i in 1..n-1] ++ [y[n-i] | i in 1..n-1], input_order, indomain_split, complete ) ]) satisfy;
To measure the overhead of ClpZinc, we also include the version of dichotomic search relying on the user-defined predicate of Example 2.

:-int_search(

[area, w], input_order, indomain_min, complete ), reverse(x, Rx), dichotomy_list(Rx, 0, max_size), reverse(y, Ry), dichotomy_list(Ry, 0, max_size).

Table 1 shows the results of the native dichotomic search procedure in MiniZinc, of the user-defined dichotomic and intervalsplitting search procedure in ClpZinc, solved using either Choco or SICStus solvers, and of the original SICStus-Prolog program of [START_REF] Simonis | Search strategies for rectangle packing[END_REF], all of them running on Intel R Xeon R CPU E5-1620 0 @ 3.60GHz machines. As shown in Table by the reification of the search procedure is quite reasonable, averaging a two-fold slowdown of the program. On the other hand, the reified search enables the encoding of the interval splitting strategy that induces a crucial increase in performance comparable to the results obtained in [START_REF] Simonis | Search strategies for rectangle packing[END_REF]. Note that, though the number of generated constraints is much larger than in the original model, it mostly depends on max_size and appears to have little impact on the observed two-fold overhead, which remains quite constant. That table also shows that the specification in ClpZinc of the dichotomic and interval-splitting search strategy makes it readily available in a variety of solvers for which its implementation was not trivial. The implementation in Choco is the most efficient, followed by SICStus-Prolog, probably due to differences in the implementation of reified constraints.

LDS and SBDS as Strategy Transformers in ClpZinc

Since and/or trees are first-class terms in ClpZinc, they can be arguments of ClpZinc predicates to define search strategy transformers.

In this section, we illustrate this possibility with the modeling of Limited Discrepancy Search (LDS) [START_REF] Harvey | Limited discrepancy search[END_REF] and Symmetry Breaking During Search (SBDS) [START_REF] Gent | Symmetry breaking during search in constraint programming[END_REF] as strategy transformers for labeling or dichotomic search for instance. This technique is closely related to the monadic approach of strategy transformers presented in [START_REF] Schrijvers | Monadic constraint programming[END_REF]. The main difference, outside of purely syntactic choices, is that the monadic transformations described in [START_REF] Schrijvers | Monadic constraint programming[END_REF] heavily rely on laziness to not expand the trees, whereas in ClpZinc, in order to finally compile towards a CSP, we fully meta-interpret, and therefore expand, the search trees, with some possible benefits thanks to the propagation of search constraints.

Limited Discrepancy Search

LDS can be modeled very simply in ClpZinc using meta-interpretation.

Basically the and/or tree is developed but the right turns are counted at the same time, by increment when going in the right branch of an or and by addition of the two branches when going through an and: Interestingly, since right turns are counted at the constraint level, the propagation of search constraints may actively reduce the search space, whereas a classical procedural implementation of LDS limits the number of right turns by generate-and-test. The following example demonstrates an exponential speed-up thanks to this propagation with respect to a procedural implementation of LDS. Whereas a procedural implementation would explore the 2 n possible assignments for a before detecting that the model is unsatisfiable within the reduced search space, the inconsistency is immediately detected in the MiniZinc model generated by ClpZinc.

Symmetry Breaking During Search

Symmetry Breaking During Search [START_REF] Backofen | Excluding symmetries in constraint-based search[END_REF][START_REF] Gent | Symmetry breaking during search in constraint programming[END_REF] is a general method that transforms a search tree so as to remove symmetric branches from enumeration. Each time the search backtracks from enumerating solutions with a given search constraint c, the other search branch considers ¬c and also all the symmetric constraints σ(¬c) for symmetries σ compatible with search constraints already posted. This schema is implemented in the predicate below, supposing a predicate cut_symmetry that adds the symmetric negations for a given constraint. The predicate search_tree constructs the search tree associated with the and/or tree of a goal by meta-interpretation.

Beyond Tree Search Strategies

Some search strategies require to iterate a search tree several times with a memory passed from one branch to another. That is typically the case for optimization methods like branch-and-bound where the best score reached up to now is remembered from one iteration to another of the underlying search strategy, or for shaving, where one step of propagation is performed and undone in order to select the best one. In languages like Prolog, such methods are implemented with the help of a global state, most commonly stored within the fact database (with assert and retract). We propose two additional annotations for search in MiniZinc to handle global state. The semantics of store(cond, id, source) is to remember, if cond is true, the current values of the sequence of variables source into the global state identified as id. The store annotation does nothing if cond is false, such that the assignation to id is skipped outside the computation branch that involves this assignation. The parameter cond does not appear in ClpZinc: it is implicitly fixed to the guard associated to the path leading to the node where the annotation appears in the and/or tree. The semantics of retrieve(id, target) is to assign the values previously remembered into the global state identified as id into the sequence of variables target.

As shown below, these two simple annotations allow the specification of branch-and-bound optimization in ClpZinc. Once again, for such strategy one might also use the native maximize annotation of MiniZinc, but as far as we know, more complex iterative procedures like shaving or enumerating solutions, using previously found ones in the search (whether to guide it or to limit it), cannot be natively written in MiniZinc. Note that in order to make this branch-and-bound procedure possible, the gap between failures at the search and at the constraint level has to be bridged. Using the incompleteness of arc-consistency, the reified constraint imposing that A, B and C are all different allows us to fail at will in the success branches (Fail = 0) by labelling A and B. There is also an optimization in the above code where the upper bound on the score is used in the Fail = 1 branch as some kind of cut: all attempts after the first failure will be immediately discarded, except the last one where appropriate values for variables will be rebuilt by running the goal G again.

Encoding Search Combinators

Search combinators [START_REF] Schrijvers | Search combinators[END_REF] introduce a domain-specific language for modeling search. We recall the primitive constructions of this domain-specific language in table 8. Search combinators are known to go beyond the conjunctions and disjunctions of CLP goals, as it is mentioned in the related work section of [START_REF] Schrijvers | Search combinators[END_REF]. However, we show that these combinators are straightforward to express using Horn clauses through meta-interpretation, thus can be expressed through the above transformation as labelling in pure CSPs. The only restriction is on restart: since the unfolding of Horn clauses into search trees should terminate, the number of iteration should be bounded statically. We only illustrate some encodings. The prune combinator is encoded as a failure at constraint level, as in section 7. The global state prune allows portfolio to implement the exhaustiveness check: by definition, the search tree is exhaustive if no call to prune are performed during its exploration.

portfolio([]) :prune. portfolio([H | T]) :

retrieve(prune, Former_prune), store(prune, 0), H, retrieve(prune, New_prune), store(prune, Former_prune), ( New_prune = 0 ; New_prune = 1, portfolio(T) ).

let and assign rely on a global state. new_atom is a primitive that generates a fresh Herbrand function symbol. let(X, V, S) :-new_atom(X), store(X, V), S.

assign(X, V) :store(X, V).

ifthenelse and post interleaves the exploration of the search tree with the test of the condition by meta-interpretation. We illustrate this meta-interpretation on post. Finally, note that even if the first_fail variable selection strategy (or a similar one) is not available as a built-in in the underlying solver, it is once again quite straightforward to implement in ClpZinc. Remark that, due to the lack of access to indexicals, such an encoding is not possibles using search combinators which are limited to what base_search makes available. The first_fail variable selection strategy selects the variable with the smallest domain among the variables that are not already instantiated (i.e., whose domain is not reduced to a singleton). If all variables are instantiated, the predicate returns by convention the first variable, so that there is no failure when iterating this predicate once per model variable, which ensures complete instantiation.

Conclusion

We have shown that tree search procedures, such as for instance heuristic labeling, dichotomy, interval-splitting, limited discrepancy search, and dynamic symmetry breaking during search, can be internalized in a constraint model through reified constraints. On the complex dynamic strategy used for solving Korf's benchmark for square packing, we have shown that the implementation overhead is limited to a factor 2, and can be measured on different CSP solvers without particular support for search. We have also shown with an example that the propagation of search constraints can in fact exhibit an exponential speed up, compared to a classical procedural implementation of the search strategy. This has been demonstrated by realizing an extension of MiniZinc with Horn clauses. Annotations for indexicals have also been added to MiniZinc for defining dynamic search strategies. Furthermore, by adding annotations for storing intermediate values during search, we have shown that this approach can be generalized to non tree search procedures, such as branch-and-bound optimization.

It is worth noting that the conversion of search into constraints opens up a whole field of challenges for CSP solvers with limited built-in search strategies. For instance, Korf's packing problem with the complex strategy of [START_REF] Simonis | Search strategies for rectangle packing[END_REF] can now be proposed for the MiniZinc contest, since any constraint solver implementing the indexical min can in principle solve it. Therefore, the two sentences of [START_REF] Simonis | Search strategies for rectangle packing[END_REF] stating that this packing problem "nicely tests the generality of a search method" and is a "more attractive benchmark for placement problems than the perfect square" can now apply to compare a broad range of CSP solvers. Furthermore, work on complex problems with dedicated heuristics can now become more independent of a particular solver through the modeling of the search strategy in our approach. We have added the needed indexicals to the FlatZinc parser of some solvers (Choco [START_REF][END_REF], JaCoP [START_REF] Kuchcinski | Jacop 4.0.0[END_REF], SICStus [START_REF] Ab | Sicstus 4.2.3[END_REF], Gecode [START_REF] Community | Gecode 4.2.1[END_REF], or-tools [START_REF]or-tools[END_REF]) and encourage all solver developers to so in order to tackle these new challenging problems for the MiniZinc community.

Finally, as a perspective for future work, the reification of choice point constraints in our scheme is in principle compatible with lazy clause generation techniques [START_REF] Ohrimenko | Propagation via lazy clause generation[END_REF] and the learning of nogood by using a SAT solver. Such a combination of modeling search by constraints and learning constraints during search is however quite intriguing and will be the matter of future work.

  var 0..5: x; constraint x * x = x + x; labeling(X, Min, Max) :-Min <= Max, (X = Min ; labeling(X, Min + 1, Max)).:-labeling(x, 0, 5). output [show(x)];

  var 0..5: x; constraint x * x = x + x; var 0..5: X1; constraint X1 = 0 -> x = 0; constraint X1 = 1 -> x = 1; constraint X1 = 2 -> x = 2; constraint X1 = 3 -> x = 3; constraint X1 = 4 -> x = 4; constraint X1 = 5 -> x = 5; solve :: seq_search([ int_search([X1], input_order, indomain_min, complete) ]) satisfy; output [show(x)]; Definition 5. A ClpZinc goal is either • a constraint, • a MiniZinc search annotation,

Example 3 (

 3 Interval splitting). The interval_splitting/4 predicate, defined below, expresses the splitting of the domain of X into intervals of width Step. X is supposed to have the initial domain Min . . . Max. interval_splitting(X, Step, Min, Max) :-Min + Step <= Max, NextX = min(X) + Step, ( X < NextX ; X >= NextX, interval_splitting(X, Step, Min + Step, Max) ). interval_splitting(X, Step, Min, Max) :-Min + Step > Max. var 0..5: x; :-interval_splitting(x, 2, 0, 5).

Figure 1 .

 1 Figure 1. And/Or tree for Example 3 (Interval splitting)

Figure 2 .

 2 Figure 2. And/Or tree derived from Example 1 (Labeling)

Figure 3 .

 3 Figure 3. And/Or tree for the ClpZinc goal var 0..5: x; :-(Min=3, Max=5; Min=0, Max=2), Min <= x, x <= Max.

Figure 4 .

 4 Figure 4. And/Or tree for Example 2 (Dichotomic search)

  int: max_size; array[1..n-1] of var 1..max_size: x; array[1..n-1] of var 1..max_size: y; var 0..max_size: w; var 0..max_size: h; var 0..max_size * max_size: area; constraint w * h = area /\ w <= h; constraint sum([i*i | i in 1..n]) <= area; constraint w >= 2 * n -1 \/ h >= (n * n + n -((w + 1) div 2 -1) * ((w + 1) div 2 -1) -((w + 1) div 2 -1)) div 2;

  solve

  lds(true, L). lds((A ; B), L) :domain(L0, 0, 1024), domain(D, 0, 1), ( D = 0, lds(A, L0) ; D = 1, lds(B, L0)), L = D + L0. lds((A, B), L) :domain(L0, 0, 1024), domain(L1, 0, 1024), lds(A, L0), lds(B, L1), L = L0 + L1. lds(B, L) :-builtin(B), B, L = 0. lds(H, L) :-clause(H, B), lds(B, L).

  var 0..1: x; var 0..1: y; array[0..n] of var 0..1: a;:-int_search(a, input_order, indomain_min, complete), lds(((x = 0; x = 1), (y = 0; y = 1)), 0), x != y.

  var 0..1: x; var 0..1: y; array[0..n] of var 0..1: a; constraint x = 0; constraint y = 0; constraint x != y; solve :: seq_search([ int_search(a, input_order, indomain_min, complete) ]) satisfy; n = 1000;

  sbds(top, _). sbds(or(A, B), Path) :-( A = constraint(C, A0), ( C, sbds(A, [C | Path]) ; cut_symmetry(C, Path), sbds(B, Path)) ; A \= constraint(_, _), (sbds(A, Path) ; sbds(B, Path))). sbds(constraint(C, T), Path) :-C, sbds(T, [C | Path]). :-search_tree(labeling_list(queens, 1, n), T), sbds(T, []).

  maximize(G, S, Min, Max) :domain(I, Min, Max + 1), domain(Best, Min, Max), domain(Fail, 0, 1), domain(A, 0, 1), domain(B, 0, 1), domain(C, 0, 1), (Fail = 0 -> A != B /\ B != C /\ A != C), store("bb_best", [Min, 0]), labeling(I, Min, Max + 1), retrieve("bb_best", [Best, Fail]), ( Fail = 0, store("bb_best", [Best, 1]), S > Best, G, store("bb_best", [S, 0]), labeling(A, 0, 1), labeling(B, 0, 1) ; Fail = 1, I = Max + 1, S = Best, G). minimize(G, S, Min, Max) :domain(Dual, Min, Max), Dual = Max -S + Min, maximize(G, Dual, Min, Max).

  prune :store(prune, 1), domain([A, B, C], 0, 1), A != B, B != C, A != C.

Table 1 .

 1 Solving times in ms for Korf's problem for strategies implemented in ClpZinc with Choco 3 and SICStus as solvers, compared to the original SICStus program. For 16 ≤ n ≤ 19, max_size=80; For 20 ≤ n ≤ 24, max_size=100; For 25 ≤ n ≤ 26, max_size=150.

	1, the overhead introduced

Table 2 .

 2 s ::= prune prunes the current search branch (i.e., fails) | base_search(vars,var-select,domain-split) search annotation | let(x,initial-value,s) introduces a new variable (i.e., global state) x in s | assign(x,new-value) changes the value of the global state x | post(c,s) posts the constraint c at every choice-point during s | ifthenelse(cond,s1,s2) substitutes in s1 every subtree where c is false by s2 | and([s1,s2,. . . ,sn]) performs s1, s2, up to sn while they succeed, and fails otherwise | or([s1,s2,. . . ,sn]) if s1 succeeds then succeeds, otherwise if s2 succeeds, then succeeds, otherwise. . . | portfolio([s1,s2,. . . ,sn]) performs s1, s2, up to sn until one of them is exhaustive (i.e., does not perform prune) | restart([cond,s]) restarts s as long as cond holds Primitive search combinators.

The Clp2Zinc compiler that transforms ClpZinc models into MiniZinc is available for download, together with patches for Choco, JaCoP, SICStus, Gecode and or-tools: http://lifeware.inria.fr/~tmartine/clp2zinc/

Acknowledgments

We are grateful to the French ANR for its support of the Net-WMS-2 project, and to the partners of this project and particularly to Philippe Morignot for stimulating discussions on these topics.