Hashtbl

[yhamoudi]

Je suis en train de faire qqs tests de perf avec des hashtbl pour les clauseset, mais j'ai l'impression que ce n'est pas formidable. C'est correct si je met des des couples (clause,int) dans la table (pour l'entier je prends le numéro de clause, mais en fait il n'y a que la clé (clause) qui m'intéresse) ?

[ilsordo]

Il faut peut être faire (int,clause) non?

[yhamoudi]

(int,clause) ? donc je prend une clause en argument et je récupère l'id pour savoir si elle est dans la table ?

[ilsordo]

si tu déclares une (int,clause) Hashtbl.t les clés sont des int et les éléments des clauses, donc tu peux faire Hashtbl.add clauseset 7 clause par exemple

[yhamoudi]

oui, je suis en train de faire la modif. Je vais vooir si c'est mieux

[ilsordo]

Pour mem tu peux chercher la clause selon son id pour du 0(1)

[yhamoudi]

oui, tout marche très bien. La seule fonction où je dois ruser c'est "choose" : je fais un iter avec un raise s'il y a une clause

[yhamoudi]

Total des résultats sur (200,3,900) avec 20 passages (il faut diviser par r.count) et timeout à 300s. Il faut bien regarder toutes les stats (par exemple, un temps peut être élevé parce qu'il y a eu bcp de conflits, et non parce que les structures de données sont moins bonnes).

Set

  {{:algo=>"dpll",
    :heuristic=>"jewa",
    :cl=>false,
    :type=>:cnf,
    :n=>200,
    :l=>3,
    :k=>900}=>
    #<Report:0x000000027fa8d0
     @data=
      {"count"=>17,
       "sat"=>0.0,
       "Conflits"=>1231751,
       "Paris"=>1231734,
       "Total execution (s)"=>2752.844,
       "Decisions (s)"=>1230.3640000000003,
       "Propagation (s)"=>766.3919999999999,
       "Backtrack (s)"=>674.0720000000001}>},

Hashtbl(clause,int)

  {{:algo=>"dpll",
    :heuristic=>"jewa",
    :cl=>false,
    :type=>:cnf,
    :n=>200,
    :l=>3,
    :k=>900}=>
    #<Report:0x000000026503e0
     @data=
      {"count"=>12,
       "sat"=>0.0,
       "Conflits"=>805867,
       "Paris"=>805855,
       "Total execution (s)"=>2367.136,
       "Decisions (s)"=>901.9680000000001,
       "Propagation (s)"=>768.1999999999999,
       "Backtrack (s)"=>631.852}>},

Hashtbl(int,clause)

{{:algo=>"dpll",
    :heuristic=>"jewa",
    :cl=>false,
    :type=>:cnf,
    :n=>200,
    :l=>3,
    :k=>900}=>
    #<Report:0x000000027ff790
     @data=
      {"count"=>13,
       "sat"=>1.0,
       "Conflits"=>828070,
       "Paris"=>828088,
       "Total execution (s)"=>2313.7799999999997,
       "Decisions (s)"=>873.5999999999999,
       "Propagation (s)"=>761.828,
       "Backtrack (s)"=>617.832}>},

---

Pour les hashtbl, j'initialisais avec une taille 10000 et ça donnait des résultats extrêmement élevés. En passant à 1000 (900 clauses au départ et pas de clause learning), ça a bien amélioré.

Les hashtbl (int,clause) font mieux que (clause,int).

Il y a un net avantage aux set ! On voit que la propagation, dans le cas des hashtbl, est très longue (c'est normal : c'est le moment où on modifie les ensembles de clauses). Je n'ai pas localisé plus précisément la source de ralentissement, mais il semble quand même y avoir un problème conceptuel lié aux hashtbl.

Je ne sais pas si j'ai fait une grosse erreur d'implémentation (voir la branche perf). Sinon, j'ai vu que la librairie core (de jane street) proposait des Hashset, ça peut être intéressant à essayer.