Récursivité (DPLL / SAT)

Je suis plutôt très amateur.

Je me suis inspiré de quelques notions simples pour écrire un code type DPLL, mais je ne sais pas mettre en oeuvre la récursivité.

dans le code ci-dessous, c'est la dernière partie qui me pose problème : comment remonter aux noeux successifs de l'arborescence.

Le code recherche le littéral qui a le maximum d'occurrences dans les clauses, et l'ajoute comme clause unitaire. Si ce littéral ne convient pas, c'est son opposé qui devient clause unitaire.

C'est bien me semble-t-il le principe de l'algorithme, mais sans l'implémentation de la récursivité.

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20

def traiter_dictionnairedesclauses(dct)   Conditions d'arrêt   #Propager clauses unitaires   #Traiter littéraux purs   counter = Counter() for clause in dct.values(): counter.update(clause) most, _ = counter.most_common(1)[0] maxi = max(dct.keys()) dct[maxi+1] = {most} if traiter_dictionnairedesclauses(dct): return True   dct[maxi+1] = {-most} print('appel récursif') return traiter_dictionnairedesclauses(dct)

---

Merci

Bonjour

Je ne comprends pas trop ce que tu veux faire (clause unitaire, opposé d'un truc qui a le maximum d'occurrences, etc).

Ce que je sais, c'est que le principe de recherche récursif d'un truc dans un arbre où chaque noeud aurait n fils est le suivant

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16

def cherche(noeud, truc): # On commence par regarder si le truc cherché se trouve dans le noeud courant if truc in noeud.info: return noeud   # On balaye maintenant les fils du noeud for f in noeud.fils: # On récupère le résultat de la recherche récursive de l'élément dans le fils en cours res=cherche(f, truc)   # Si ce résultat est probant, alors on a trouvé et on le remonte à l'appelant (qui, lui-même, le remontera à l'appelant et etc) if res is not None: return res # for   # La branche entière ne contient pas le résultat: on remonte l'info à l'appelant qui testera alors un autre frère return None # cherche()

---

Au final, on obtient le premier noeud de l'arbre qui contient l'info cherchée. C'est un peu l'algorithme de base qui s'adapte à toutes les situations à peu près standard.

Si maintenant ton support d'information c'est pas un arbre mais une simple liste, alors pas besoin de récursivité. La récursivité c'est vraiment le dernier recours quand on n'a pas pu faire autrement. C'est lourd, consommateur de ressources et en plus c'est limité (à 1000 par défaut).

>C'est lourd, consommateur de ressources et en plus c'est limité (à 1000 par défaut).
Mais cela n'est il pas plus rapide à l'exécution ?
j'ai fait un test de temps d'exécution pour comparer le tri d'une liste de manière récursive et dichotomique, et au niveau temps, le tri récursif était bien mieux dès que la liste devenait grande.

Salut,

Citation:

---

Envoyé par Arbraz

Je me suis inspiré de quelques notions simples pour écrire un code type DPLL, mais je ne sais pas mettre en oeuvre la récursivité.

---

Vous essayez de coder un algorithme connu et documenté qu'il y a juste à traduire en Python.
Relisez votre code, comparez avec l'algorithme qui est documenté et essayez de comprendre si les différences sont dues à son codage en Python ou à un oubli.

Citation:

---

Envoyé par racine carrée

j'ai fait un test de temps d'exécution pour comparer le tri d'une liste de manière récursive et dichotomique, et au niveau temps, le tri récursif était bien mieux dès que la liste devenait grande.

---

Un algorithme récursif sera plus simple à penser (et à coder). Après un travail peut être de le coder en itératif: vous aurez la même complexité puisque, c'est le même algo. Les différences seront côté appels de fonctions côté récursif et gestion de l'état (pour remplacer la pile) côté itératif. Au bout du compte il y aura des algos plus rapides codés en récursif et d'autres seront plus rapides codés en itératif... pour autant que ce soient les mêmes algo.

- W

Merci à tous d'avoir répondu

Citation:

---

Envoyé par wiztricks

Salut,

Vous essayez de coder un algorithme connu et documenté qu'il y a juste à traduire en Python.

---

Je connais le lien que tu me donnes, mais de ce pseudo-code très minimal, mais suffisant pour comprendre le principe, à sa traduction en Python (qu'il faut tout de même maîtriser) il y a un grand pas pour quelqu'un qui maitrise mal la récursivité. En ce qui me concerne, je fais de la compréhension de ce type de problèmes un loisir parmi d'autres, je n'ai donc pas de compétences très avancées dans ce domaine.

Ma difficulté est la suivante :

La formule dont on cherche la satisfaisabilité est une conjonction de disjonctions dont l'implémentation peut être une liste, un dictionnaire ... avant traitement.
L'algorithme cherche un (ou plusieurs) ensemble(s) de littéraux, s'ils existent, qui rendent la formule vraie, d'où la récursivité en cas d'échec de la recherche partielle.
Il faut donc dans ce cas revenir (remonter) à une version précédente de la formule, et ainsi de suite, et c'est là que je bloquais.
J'ai trouvé un algorithme qui m'a fourni la solution : http://www.cs.cmu.edu/~emc/15414-f11...ec02_grasp.pdf
Je l'ai transcrit, mais cela ne veut pas dire que je comprends bien ce que j'appelle la remontée à une version précédente de la formule.

Je joins l'algorithme (que je n'ai pas documenté), les initiés le liront facilement.

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71

# -*- coding: utf-8 -*- """ Created on Thu Oct 25 11:34:14 2018   @author: Administrateur """   from collections import defaultdict, Counter from copy import deepcopy, copy   def constituer_listedesclauses(nf,p): listedesclauses = [] f = open(nf,'r') for ligne in f : if ligne[0] == 'c': print(ligne) elif ligne[0] == 'p' : ligne = ligne.split() V = int(ligne[2]) C = int(ligne[3]) if p != 0 : print('\nVariables :',V,' - ','Clauses :',C,'\n') else : ligne = (ligne.split()[:-1]) clause = [] for litteral in ligne : clause.append(int(litteral)) listedesclauses.append(clause) if p != 0: print('Liste des clauses :\n',listedesclauses,'\n') f.close() return listedesclauses   def assignlit (clauselist, lit): clauselist = deepcopy(clauselist) for clause in copy(clauselist): if lit in clause: clauselist.remove(clause) if -lit in clause: clause.remove(-lit) return clauselist   def choixlit (clauselist): counter = Counter() for clause in clauselist : counter.update(clause) most, _ = counter.most_common(1)[0] return most   def constituer_listedesclausesunitaires (clauselist): listeclu = [] for clause in clauselist : if len(clause)==1 : listeclu.append(clause[0]) return listeclu   def traiter_clausesunitaires(clauselist): listeclu = constituer_listedesclausesunitaires(clauselist) for forcedlit in listeclu : clauselist = assignlit(clauselist,forcedlit) return clauselist   def satisfiable (clauselist): clauselist = traiter_clausesunitaires(clauselist) if(len(clauselist)) == 0 : return True if [] in clauselist : return False declit = choixlit (clauselist) return (satisfiable(assignlit(clauselist,declit)) \ or satisfiable(assignlit(clauselist,-declit)))   print('\n----------TRAITEMENT----------')   nomdefichier = "ex06.cnf"   lcl = constituer_listedesclauses(nomdefichier,0) print('\nListe des clauses:',lcl)   res = satisfiable(lcl) print (res)

---

Je subodore que c'est dans la fonction assignlit que tout se joue avec deepcopy.

Si l'un d'entre vous peut m'expliquer simplement, ce serait bien.

J'ai aussi plusieurs questions ; la première est :
Dans le cas d'une formule satisfiable, comment connaître au moins une solution pour l'imprimer.
Pour les autres questions, j'attendrai un peu.

Merci à l'avance

Bonjour,

Citation:

---

Envoyé par Arbraz

Je subodore que c'est dans la fonction assignlit que tout se joue avec deepcopy.
Si l'un d'entre vous peut m'expliquer simplement, ce serait bien.

---

Je n'ai pas regardé ton algorithme, mais je peux répondre pour deepcopy.

Voilà un petit code de test:

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13 14

from copy import deepcopy, copy   A = [1,2,[3,4,5],6,7] B = A C = copy(A) D = deepcopy(A)   A[1] = 8 A[2][1] = 9   print(A) print(B) print(C) print(D)

---

Ce qui affichera:

Code:

---

1 2 3 4

[1, 8, [3, 9, 5], 6, 7] [1, 8, [3, 9, 5], 6, 7] [1, 2, [3, 9, 5], 6, 7] [1, 2, [3, 4, 5], 6, 7]

---

On voit bien le problème:

- B = A ne fait que recopier l'adresse de la liste A dans B. Ainsi, toute modification de A se propagera sur B.

- C = copy(A) recopie les éléments de 1er niveau qui ne seront pas modifiés, mais les modifications des niveaux supérieurs de A (des listes à l'intérieur de la liste) se propageront sur C.

- D = deepcopy(A) fait une copie complète de A sur D qui devient différente à tous les niveaux: aucune modification de A se propagera sur D.

A noter que la simple copie C = copy(A) peut être remplacée couramment par C = A[:], ce qui évite l'importation.

[Edit] pour compléter, voilà une petite fonction récursive qui simule deepcopy et qui donne, bien sûr, les même résultats:

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12

def copieprofonde(L): """Retourne une copie complète de L, et convertit les éventuels tuples en listes     """ R = [] for elem in L: if isinstance(elem, list): R.append(copieprofonde(elem)) elif isinstance(elem, tuple): R.append(copieprofonde(list(elem))) else: R.append(elem) return R

---

Citation:

---

Envoyé par tyrtamos

Code:

---

1 2 3 4 5 6 7 8 9 10

def copieprofonde(L): R = [] for elem in L: if isinstance(elem, list): R.append(copieprofonde(elem)) elif isinstance(elem, tuple): R.append(copieprofonde(list(elem))) else: R.append(elem) return R

---

---

copieprofonde=lambda L: list(copieprofonde(list(elem)) if isinstance(elem, (list, tuple)) else elem for elem in L) ;) :chin: