Une structure de données pour des ensembles d'arbres.

Les essais permettent un stockage efficace des listes d'éléments. Les préfixes sont partagés, ce qui optimise l'espace.

Je cherche un moyen similaire de stocker efficacement les arbres. Je voudrais pouvoir vérifier l'appartenance et ajouter des éléments, sachant si un arbre donné est un sous-arbre de certains arbres stockés ou s'il existe un arbre stocké étant un sous-arbre de l'arbre donné est également souhaitable.

Je stockais généralement environ 500 arbres binaires non équilibrés d'une hauteur inférieure à 50.

ÉDITER

Mon application est une sorte de vérificateur de modèle utilisant une sorte de mémorisation. Imaginez que j'ai un état et les formules suivantes: et avec étant une sous-formule complexe, et imaginez que je veux d'abord savoir si tient dans . Je vérifie si tient et après un long processus j'obtiens que c'est le cas. Maintenant, je veux savoir si est valable dans l' . Je voudrais me souvenir du fait que est vrai et remarquer que pour que je puisse dériver in presque instantanément.f = ϕ g = ( ϕ ∨ ψ ) ϕ f s ϕ g s f g ⇒ f g $s$$f = \phi$$g = (\phi \vee \psi)$$\phi$$f$$s$$\phi$$g$$s$$f$$g \Rightarrow f$$g$$s$
Inversement, si j'ai prouvé que ne tient pas en , alors je veux dire que ne tient pas en presque instantanément.t f $g$$t$$f$$t$

Nous pouvons construire un ordre partiel sur les formules, et avoir iff . Pour chaque état , nous stockons deux ensembles de formules; stocke les formules maximales qui tiennent et stocke les formules minimales qui ne tiennent pas. Maintenant donné un état et une formule , je peux voir si , ou si auquel cas je suis fait et je sais directement si est valable à l' .g ⇒ f s L ( s ) l ( s ) s g ∃ f ∈ L ( s ) , f ⇒ g ∃ f ∈ l ( s ) , g ⇒ f g $g \geq f$$g \Rightarrow f$$s$$L(s)$$l(s)$$s$$g$$\exists f \in L(s), f \Rightarrow g$$\exists f \in l(s), g \Rightarrow f$$g$$s$

Actuellement, et sont implémentés sous forme de listes et ce n'est clairement pas optimal car j'ai besoin d'itérer individuellement toutes les formules stockées. Si mes formules étaient des séquences, et si l'ordre partiel était "est un préfixe de" alors un trie pourrait s'avérer beaucoup plus rapide. Malheureusement, mes formules ont une structure arborescente basée sur ¬ , ∧ , un opérateur modal et des propositions atomiques.$L$$l$$\neg, \wedge$

Comme le souligne @Raphael et @Jack, je pourrais séquencer les arbres, mais je crains que cela ne résoudrait pas le problème car l'ordre partiel qui m'intéresse ne correspondrait pas à "est un préfixe de".

Vous voudrez peut-être consulter les g-try . Il s'agit essentiellement de la structure de données que vous recherchez, mais conçue pour être utilisée avec des graphiques généraux au lieu de simplement des arbres. En tant que tel, je ne suis pas sûr que les g-try aient de bonnes garanties théoriques - je pense qu'ils utilisent un algorithme de canonisation de graphe comme sous-programme - mais en pratique, ils semblent bien fonctionner.

(N'ayez pas peur que l'article lié porte sur les "motifs de réseau dans les réseaux biologiques": le g-trie est une structure de données abstraite parfaitement bonne pour les graphiques.)

La persistance en est une forme particulière : voir les articles Rendre les structures de données persistantes par Driscoll, Sarnak, Sleator et Tarjan et Planar Point Location Using Persistent Search Trees de Sarnak & Tarjan, qui stockent les familles d'arbres associés.

Cela ressemble un peu à une forêt (forêts disjointes ) ...

Il amortit le coût d'insertion grâce à une technique appelée union par rang et l'opération de recherche utilisant la compression de chemin . Je sais qu'il y a aussi une version persistante de cette structure développée par Sylvain Conchon et Jean-Christophe Filliâtre mais je ne sais pas si c'est la même que celle que Jack mentionne ...

Qu'en est-il des automates arborescents minimaux ?

Dans "Purely Functional Data Structures" (1998), Chris Okasaki propose des essais d'arbres binaires en utilisant l'agrégation de types (10.3.2).

Je ne sais pas si cela aide immédiatement; la solution qui y est donnée pourrait ne pas être directement implémentable.

Dans le jargon du programmeur: Si vous créez les arbres à partir de sous-expressions / arbres / DAG communs, vous auriez un joli modèle compact. Graphiques acycliques ainsi dirigés. Ensuite, un ensemble d'arbres suffirait.

public class Tree {String operation; Arbres [] sous-arbres;

public int compareTo(Tree rhs) {
    if (rhs == null) return false;
    int cmp = operation.compareTo(rhs.operation);
    if (cmp == 0) {
        cmp = Arrays.compareTo(subtrees, rhs.subtrees);
    }
    return cmp;
}

...}

Map commonSubExpressions = new HashMap ();

Tree get (String expressionSyntax) {Tree t = new Tree (); t.operation = ...; t.subtrees = ... appel récursif pour obtenir des sous-expressions; Arbre t2 = commonSubExpressions.get (t); if (t2 == null) {t2 = t; commonSubExpressions.put (t2, t2); } return t2; }}