Qu’est-ce qu’un solveur comme Z3 ?
Un solveur est un programme qui cherche des valeurs respectant des règles, ou qui prouve qu’il n’en existe aucune. Z3 est l’un des plus utilisés. Il vérifie une affirmation sur tous les entiers sans en essayer un seul.
Une calculatrice prétend que le carré d’un entier n’est jamais négatif. Z3 peut le prouver. Il peut aussi trouver le cas qui contredit une affirmation fausse.
À la fin de cette leçon
Remarque
Je peux demander à Z3 si une affirmation est toujours vraie et lire sa réponse.
Mots-clés
| Mot | Ce que ça veut dire | Exemple |
|---|---|---|
| Solveur | un programme qui cherche des valeurs qui respectent des règles | |
| Satisfiable (sat) | au moins une valeur respecte toutes les règles | |
| Insatisfiable (unsat) | aucune valeur ne respecte toutes les règles | |
| Affirmation | une phrase qu’on veut prouver vraie pour tous les cas | n * n >= 0 |
| Négation | l’affirmation contraire | n * n < 0 |
| Modèle | les valeurs que le solveur donne quand il répond sat |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Un solveur répond sat ou unsat
On déclare des inconnues, on pose des règles, puis on demande si un jeu de valeurs les respecte toutes. Z3 répond sat et donne un exemple, ou unsat : aucune valeur ne convient.
Prenons des stylos à 3 euros et des cahiers à 2 euros, au moins un de chaque. Le premier Run cherche un panier de 12 euros. Le second cherche un panier de 4 euros.
Un panier de 12 euros existe-t-il ?
echo '(declare-const stylos Int) (declare-const cahiers Int) (assert (and (> stylos 0) (> cahiers 0) (= (+ (* 3 stylos) (* 2 cahiers)) 12))) (check-sat) (get-model)' | z3 -inAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Un panier de 4 euros existe-t-il ?
echo '(declare-const stylos Int) (declare-const cahiers Int) (assert (and (> stylos 0) (> cahiers 0) (= (+ (* 3 stylos) (* 2 cahiers)) 4))) (check-sat)' | z3 -inAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
On prouve en cherchant le contraire
Pour prouver une affirmation, on demande à Z3 un cas où elle est fausse : sa négation. Si Z3 répond unsat, aucun cas ne la contredit, donc elle est toujours vraie.
Si Z3 répond sat, il donne un contre-exemple. Le premier Run teste « le carré n’est jamais négatif ». Le second teste « le carré est toujours plus grand que le nombre ».
Chercher un carré négatif
echo '(declare-const n Int) (assert (< (* n n) 0)) (check-sat)' | z3 -inAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Chercher un carré pas plus grand
echo '(declare-const n Int) (assert (<= (* n n) n)) (check-sat) (get-model)' | z3 -inAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Exemple travaillé : deux affirmations
| Affirmation | Ce qu’on demande à Z3 | Réponse | Conclusion |
|---|---|---|---|
| n * n >= 0 | n * n < 0 | unsat | Toujours vraie |
| n * n > n | n * n <= n | sat, avec n égal à 1 | Fausse : 1 * 1 n’est pas plus grand que 1 |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Erreur fréquente
Attention
Beaucoup de gens pensent que sat veut dire que l’affirmation est vraie. Pour une preuve par le contraire, c’est l’inverse. Si Z3 répond unsat à la négation, l’affirmation est prouvée. S’il répond sat, il montre un contre-exemple.
Z3 retrouve la faille sans borne
Dans la leçon précédente, une règle de livraison offerte dès 50 euros était codée > 50 au lieu de >= 50. On a essayé 101 montants pour trouver la faille.
Z3 la cherche parmi tous les entiers, sans borne. Il demande un montant où le code et la règle donnent des réponses différentes.
Chercher un montant où ils diffèrent
echo '(declare-const total Int) (assert (not (= (> total 50) (>= total 50)))) (check-sat) (get-model)' | z3 -inAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Pour aller plus loin
Changez la ligne du carré. Demandez à Z3 s’il existe un entier n avec n * n = 2 : écrivez (= (* n n) 2) à la place de (< (* n n) 0).
Lancez la commande, puis expliquez ce que veut dire la réponse pour les entiers.