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 : Sélectionner tout - Visualiser dans une fenêtre à part
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