specs

Structures de donnees utilisees: (ce que possede un thread)
__partagées (en ro)__
    [formula] : tableau contenant tous les atomes, les uns après les autres (clauses concaténées)
    [n] : nombre de clauses
    [clauses_index] : tableau d'indices : début de chaque clause dans la formule.
        indique la fin de la dernière clause)
__privée__
    [satisfied] : tableau de booleen indiquant les clauses satisfaites (taille n)
    [affectations] : tableau indiquant les valeurs de vérité des variables (si déjà affectées)
    
    
    
    

    1 variable = 1 mot de 16 bits (short int, 2 octets)
        bit 1: affectation (MSB)
        bit 2: signe
        bits 3-16: nom de variable
    => macros et masques pour tester les variables


    1 valuation (valeur de vérité) = 1 mot de 8 bits (char, 1 octet)
        bit 1: la variable est-elle immutable (MSB)
        bit 2: la variable est-elle affectée ?
        bit 8: valeur de vérité
    => pourquoi ? difficile de faire plus petit simplement (tableau de champ de bits ??)


Renseignements a prendre :
    taille de la memoire partagee ====> 2^14 Bytes ie 2^12 entiers ie 2^10 shorts 
        par coeur ie 1024 atomes par formule. 
        => on ne peut pas stocker les donnees des formules en shared, une par thread
    on peut partager le tableau de pointeur, la formule
    selon input : peut-etre avoir le tableau de bool en shared
    taille de la memoire GPU ===>  un peu moins de 2^30


Objectifs:
    2^14 noms de variables est raisonnable


TODO:
    implementer une version uni-threadee (pour avoir une base pour ecrire les kernel threads):
        [OK] parser le fichier
        [OK] initialiser la formule
        calculer une affectation
        recuperer la satisfiabilite
    
DONE:
    ecrire les structures, et macros dans un header
    


Algorithme : (DPLL)
    Il s'agit d'une recherche exhaustive guidée par des heuristiques. 
    À chaque étape, on cherche les clauses unitaires (un seul atome non encore affecté), on affecte les variables
    concernées (un seul choix possibles).
    Si toutes les clauses sont satisfaites, on retourne succès
    Si l'une des clauses est absurde, on retourne échec
    Sinon, on choisit de manière "éclairée" une variable, et on récurse sur les 2 affectations possibles de 
    cette variable.

Problèmes:
    comment se souvenir de chaque changement (quand on unit_propagate ou qu'on récurse, par exemple)
    comment implémenter la récursivité ?
    comment occuper les threads qui ont fini trop tot (branche clairement insatisfiable)
        -> file d'attente de tâches commune ? (pb: parcours en largeur et non en profondeur)