Structure pour une sortie en fichier CNF

[edgarogh]

c.f. spec format DIMACS CNF (conjunctive normal form): https://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html

Type Literal

Implémenter un type (struct ou enum, les deux sont faisables) Literal qui contient les coordonnées d'une cellule et si l'atome est en négation ou pas (si la cellule est vraie ou fausse / 1 ou 0). Ça peut se faire de plein de façons.
Il faut pouvoir représenter par exemple: non (1, 2); (3, 4); (1, 0); non (1, 1)

Implémenter une méthode sur ce type qui à partir d'une taille de grille (je pense qu'on peut partir du principe qu'elle est carrée) renvoie le litéral sous la forme d'un nombre relatif non nul (rappel, le format de fichier CNF utilise le negatif pour représenter la négation d'un litéral, et les litéraux sont tous des nombres). Par exemple, sur une grille de taille 4, le litéral (2, 1) peut correspondre à 6 (1 * 4 + 2), mais il faut rajouter 1 pour pas que ce nombre puisse être nul, ce qui donne 7. L'idée est d'avoir une bijection Literal ⟷ [i64≠0].

Type CNFFile

La structure engloberait un BufWriter<File> (fonctionne comme un BufReader 📖 mais pour l'écriture) et fournirait des méthodes pour écrire dans le fichier CNF. Le constructeur prend la taille de la grille et écrit un en-tête*. Une méthode prend une liste de Literal (une clause au fond) et l'écrit sur une ligne au format spécifié par la spec.

La magie de Rust fait qu'on a pas besoin de fermer le fichier, ce sera fait automatiquement quand la structure sera Dropée (ne sera plus accessible).

*Reste à voir comment on implémente le nombre de clauses dans l'entête. Le plus simple est sûrement de réserver de la place avec des espaces puis d'y revenir écrire le nombre de clauses à la fin