edgarogh/inf402

SAT-solver-based takuzu solver

Hi! I'm Edgar, I am currently studying computer science at Polytech Grenoble¹ and ÉTS Montréal (in a double diploma) and aiming for an engineering degree.

I love programming in my free time since I'm 10. I particularily love 🦀Rust🦀, compiler and programming language development, back-end web development, CLI tool development, optimization and low-level stuff. I also have a bit of interest in theoretical computer science.

I care deeply about current social, societal and environmental issues and strive to prioritize addressing them over pursuing financial gain.

Contact

• [email protected]
• https://www.linkedin.com/in/edgarogh/

Devices

On vacation in France while I'm abroad...

---

Footnotes

1. Information on the curriculum: 🇬🇧 https://www.polytech-grenoble.fr/medias/fichier/info-anglais_1626773054059-pdf 🇫🇷 https://www.polytech-grenoble.fr/medias/fichier/info-francais_1626773087298-pdf ↩

inf402's Issues

Règle 2 « Pas plus de 2 chiffres identiques côte à côte »

https://md.edgar.bzh/s/73RWTRsNZ#r%C3%A8gle-2--pas-plus-de-2-chiffres-identiques-c%C3%B4te-%C3%A0-c%C3%B4te

Lecture de fichier "grille de Takuzu"

Création d'un module 📖 pour lire un fichier 📖 représentant une grille de Takuzu.

On peut essayer de définir le format du fichier sous cette issue.

Fonction pour afficher une grille

Contexte: Une fois le fichier de résultats du SAT-Solveur importé, on devra faire un petit traitement pour re-convertir les litéraux du modèle en coordonnées+[0/1] (c.f. #3) et on obtiendra une grille remplie (on fera ça plus tard).

Cette grille doit pouvoir être affichée.

La tâche est donc de créer une méthode sur la structure Grid qui l'affiche, ou, pour faire encore plus idiomatique, implémenter le trait Display de la bibliothèque standard, qui indique qu'un type est affichable et comment l'afficher.
Si vous partez sur la solution 1 (une simple méthode fait maison) et utilisez des println! (ou print!), c'est très facile d'"upgrade" vers la solution 2 qui est un peu plus idiomatique, et je pourrais vous guider. L'avantage de la seconde solution est qu'on est pas obligé de "print" la grille dans la console, on pourrait l'écrire dans une String ou dans un fichier par exemple. Ici ça sert à rien, certes...

N'oubliez pas qu'une cellule peut contenir des 0, des 1 et des cases vides. Même si la grille est censée être pleine à la fin, le type Grid considère qu'une cellule peut être vide, donc il faudra en tenir compte, ou alors faire planter le programme, mais est-ce bien nécéssaire ? C'est cool si on peut afficher une grille, même partiellement vide, pour déboguer.

Règle 1 « Autant de 1 et de 0 sur chaque ligne et sur chaque colonne. »

https://md.edgar.bzh/s/73RWTRsNZ#regle-1--autant-de-1-et-de-0-sur-chaque-ligne-et-sur-chaque-colonne

Structure pour une sortie en fichier CNF

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

Règle 3 « Pas deux colonnes ou deux lignes identiques »

https://md.edgar.bzh/s/73RWTRsNZ#r%C3%A8gle-3--pas-deux-colonnes-ou-deux-lignes-identiques

Lire le premier argument (rapide)

• Dans la fonction main(), lire le premier argument du programme (le nom du fichier à ouvir).
  On utilise la fonctions std::env::args() qui renvoie un std::env::Args, une structure qui implémente Iterator<Item=String> 📖, qu'on peut transformer en Vec<String>
• Créer un if dans le main qui selon l'extension du fichier (ou contenu, à décider), exécute une fonction main_generate (qui a terme génèrera le fichier CNF) ou une fonction main_result (qui a terme affichera la grille remplie à partir du fichier de résultats du SAT-Solveur

À décider: extension des fichiers (ou on commence à les lire et on devine selon le contenu comme j'avais suggéré)