SAT

Lancer le solveur

Des options sont passées au solveur en ligne de commande :

python solveur_sat.py --chemin_fichier=./tests/satlib_cnf/sat_cnf/UF20-91/uf20-01.cnf

options disponibles :

Option long	Option court	Description	Exemple
--choix_variable	-cv	Methode de choix de variable	python solveur_sat.py --choix_variable=lexicographique
--chemin_fichier	-cf	Chemin du fichier contenant la formule a evaluer	python solveur_sat.py --chemin_fichier=./tests/satlib_cnf/sat_cnf/UF20-91/uf20-01.cnf

Packages

Des packages sont utilisés pour les tests (pytest) et le linter (flake8) qui permet de vérifier de manière formelle la qualité du code.

Pour installer ces packages, créer un environnement virtuel :

python -m venv venv

Activer ensuite cet environnement (la procédure dépend de l'OS).

Et installer les packages nécessaires:

pip install -r requirements.txt

Tests

Des fichiers au format DIMACS sont utilisés pour les tests. Ces fichiers proviennent du site https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html.

Et également de https://people.sc.fsu.edu/~jburkardt/data/cnf/

D'autres fichiers ont été générés par nos soins.

./tests/
├── sat_cnf
│   └── UF20-91
    ...
└── unsat_cnf
    └── UUF50.218.1000
    ...

Exécuter

python -m pytest -v tests

Générateur

Les classes dans le fichier generateurs.py permettent de créer des fichiers pour les problèmes des dames et pigeons.

python3 generateurs.py -cp=dames -nb=1

Benchmarks

Après avoir installé les packages (voir plus haut).

Exécuter :

streamlit run ./tests/solveur_benchmark.py

Linter

Il est également possible d'avoir quelques informations sur la qualité du code en exécutant un linter.

flake8 solveur_sat.py

Auteurs

Par ordre alphabétique:

- BEN ABDALLAH Khaled
- BOULJIHAD Mohamed
- KERROUT Madian
- TRKULJA Sinisa