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.

Site officiel et téléchargement

Tags:
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.

Veuillez renseigner les champs ci dessous :

Votre nom ou pseudo

Paragraphe

Type de modification

Les modifications à apporter*
Majeure : une nouvelle version avec des nouveautés, des changements majeurs.

En cochant cette case, vous allez créer une page sur le wiki afin de mettre à jour la notice.

Mettre la notice de SAToulouse sur le wiki

<< Poster un message >>
:: question :: précision :: avis :: commentaire :: bug ::

Faire un don ? (défiscalisé)

Faire un DON

Aidez-nous à atteindre notre objectif de 600 donateurs récurrents pour assurer notre pérennité et notre développement ! (nous y sommes presque).

Je soutiens Framasoft pour 10€/mois

Autres logiciels

Framasoft needs you !

Vous trouverez ici une liste de logiciels qui ont fait acte de candidature et qui n’attendent que vous pour réussir avec brio l’examen d’entrée dans notre annuaire.