SAToulouse
Ce logiciel permet de s’initier à la programmation logique à l’aide de la logique propositionnelle. Il s’adresse surtout aux étudiants en informatique et logique niveau licence. Pour plus de précision sur la logique propositionnelle, n’hésitez pas à consulter Wikipedia.
Ce logiciel permet de résoudre des problèmes comme celui des carrés latins, le Sudoku, des problèmes de planification, etc.
L’utilisateur programme la résolution d’un problème en le décrivant à l’aide de la logique propositionnelle. Contrairement à la programmation impérative (Java, C, etc.), où on donne les instructions qui devront être exécutées pour résoudre un problème, la programmation logique est descriptive. Programmer revient à décrire les règles du problème que l’on souhaite résoudre.
Ainsi, les problèmes traités sont formalisés en logique propositionnelle et ramenés au problème de « satisfiabilité ».
Par exemple, pour le Sudoku, l’utilisateur décrit les règles du Sudoku, et les hypothèses de l’énoncé : « le 5 apparaît sur l’une des cases de la troisième ligne ». Pour cela, on introduit des propositions comme « il y a un 5 dans la case (3, 4) » puis à l’aide des connecteurs booléens comme « implique », « et », « ou », « non », on forme des formules logiques qui décrivent les règles du jeu. Par exemple la règle « le 5 apparaît sur l’une des cases de la troisième ligne » s’écrit (« il y a un 5 dans la case (3, 1) » ou « il y a un 5 dans la case (3, 2) » ou « il y a un 5 dans la case (3, 3) » etc.). Le logiciel introduit des macros permettant d’écrire de grosses formules comme (OU_pour i entre 1 et 9 « il y a un 5 dans la case (3, i) »).
Une fois un problème décrit par un ensemble de formules booléennes, le logiciel permet de vérifier si leur intégralité est recevable (satisfiable) ; en d’autres termes, de savoir si le problème a une solution. Dans le cas où le problème a une solution, le logiciel donne une « valuation » (aussi appelée « interprétation ») : la « valuation » correspond au résultat du problème. Dans le cas du Sudoku, une valuation indique comment est remplie une grille solution.
Programmer un solveur de Sudoku en C, Pascal, Java etc. est plus difficile. Le développement d’un tel programme est long et n’est pas garanti. En effet il est difficile de garantir l’exactitude d’un programme impératif dans toutes les situations, à moins de fournir une preuve de programme, ce qui rallonge les coûts de développements.
En comparaison, un étudiant au clair avec la logique des propositions, écrit ses règles du Sudoku en 10 minutes. Le solveur qu’il programme est garanti dans la mesure où les règles décrites en logique des propositions sont justes. Comme les règles sont courtes et peu nombreuses, il est facile de s’assurer de leurs exactitudes et donc du programme logique écrit par l’étudiant. En revanche, à l’exécution les performances sont moins bonnes : le solveur met une seconde à résoudre une grille classique sur un ordinateur récent. Ce logiciel permet donc aussi de lancer le débat : préfère-t-on un logiciel sûr ou un logiciel rapide ?
Le logiciel est fourni avec quelques exemples de problèmes concrets directement implémentés.
Par ailleurs, SAToulouse permet d’ouvrir/sauvegarder sa liste de formules. Il ouvre également le format standard de conjonction en forme normale DIMACS afin de bénéficier des « benchmarks » des conférences de logique théorique.
Contexte
Les solveurs SAT sont nombreux : SAT4J (celui utilisé par SAToulouse), march_dl, MiniSAT etc. Ils sont efficaces mais offrent des interfaces austères, en ligne de commande, ce qui n’est pas optimal pour les étudiants. SAToulouse a pour objectif de rendre ce champs de recherche et d’application mathématique plus accessible en proposant une interface facilement utilisable par un étudiant pour montrer que les solveurs SAT sont utiles et utilisables pour résoudre des problèmes.
Par ailleurs, la programmation logique est souvent introduite via Prolog. SAToulouse se distingue de Prolog par deux aspects :
- D’une part, la logique utilisée est plus simple : SAToulouse utilise la logique propositionnelle et non pas la logique des prédicats. L’avantage est pédagogique : le nombre de notions à maîtriser est plus petit. Par exemple, pas besoin d’introduire les notions de termes, prédicats, substitutions, unification, résolution etc.
- D’autre part, Prolog utilise la règle du “cut”, difficile à maîtriser pour un étudiant.
Avis personnel
Si les formules sont très longues, il est parfois difficile d’écrire/lire une formule sans s’emmêler dans les parenthèses. De plus, les parenthèses sont obligatoires ce qui rend l’utilisation un peu fastidieuse au début. Les améliorations vont se diriger vers une analyse syntaxique pour éviter les parenthèses lorsqu’elles ne sont pas utiles à l’œil pour l’utilisateur.
Pour finir, le logiciel est utilisé à l’université de Toulouse 3 en licence deuxième année d’informatique.
Merci à François Schwarzentruber pour la rédaction originale de cette notice dans notre wiki.
Ajouter des tags (séparés par des virgules ou des espaces) : Attention: tous les caractères spéciaux sont interdits (sauf le .). Les tags n'apparaîtront qu'au prochain rafraichissement du cache (dans plusieurs heures).
<< Mettre à jour >>
:: lien mort :: orthographe :: nouveauté :: mise à jour ::
Vous souhaitez mettre à jour la notice ? La première chose à faire est de déterminer s'il s'agit d'une mise à jour mineure ou d'une mise à jour majeure .
- Mineure : un lien mort, des fautes d'orthographe, un lien à ajouter ou encore une petite précision.
- Majeure : une nouvelle version avec des nouveautés, des changements majeurs.
Commentaires
<< Poster un message >>
:: question :: précision :: avis :: commentaire :: bug ::
Informations complémentaires
Faire un don ? (défiscalisé)
Aidez-nous à atteindre notre objectif de 1080 donateurs récurrents pour assurer notre pérennité et notre développement !
Autres logiciels
Dégooglisons Internet, l’an 2
Les services en ligne de géants tentaculaires comme Google, Apple, Facebook, Amazon ou Microsoft (GAFAM) mettent en danger nos vies numériques.
Pour cette 2e année, nous continuons le défi de vous proposer une alternative Libre, Éthique, Décentralisée et Solidaire à chacun de ces services.
Autres rubriques
Libre : agenda
- Nantes: Atelier de contribution à Wikipédia, On Wednesday 30 January 2019 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Monday 30 January 2017 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Wednesday 21 December 2016 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Monday 5 December 2016 from 18h30 to 21h30.
- Nantes: Atelier de contribution à Wikipédia, On Saturday 19 November 2016 from 18h30 to 21h30.
Informations générales
Sur le Framablog
Sur Framagora
- Disque externe hfs en lecture seule
- Problème de couleur
- Changer la langue d'un clavier sous xubuntu
- LibreOfficePortable : décimales
- au sujet de mon netbook gdium
- framabag certificat SSL revoqué
- rendre vierge ma clé
- Soumettre une notice pour un logiciel dont on est l'auteur
- Blender - Projet Gooseberry
- Bonjour
Juste une image
- Fly 1-PW
- Creative Commons BY-SA