Certains problèmes mathématiques ne peuvent pas être résolus en temps raisonnable par force brute.
Par exemple :
\(\begin{cases} x \in [1,50], y \in [1,100], z \in [1,100]\\ z = \dfrac{x+y}{2}\\ (x \times y) \equiv 14 \pmod{21}\\ LSB((x+y) \lor z) = 126\\ \end{cases}\)
Les tests ne sont pas très coutêux en performance, ce ne sont que des opérations mathématiques et binaires simples, mais il y a déjà \(50 \times 100 \times 100 = 500\,000\) possibilités à tester. Le temps de calcul est proportionnel à la taille des variables d’entrée, donc il peut être gigantesque.
Temps pour un programme en C :
| Valeurs (x, y, z) | Temps (s) | Temps (humain) |
|---|---|---|
| (50, 100, 100) | instantané | instantané |
| (500, 1000, 1000) | 2 s | 2 s |
| (5 000, 10 000, 10 000) | 2000 s | 33 min |
| (50 000, 100 000, 100 000) | 2 000 000 s | 23 jours |
| (500 000, 1 000 000, 1 000 000) | 2 000 000 000 | 63 ans |
Dans ce genre de cas, la force brute n’est pas impossible mais doit être largement parallélisée, ou on doit utiliser des optimisations.
Un solveur SMT peut nous aider à trouver une des solutions de ce problème. On utilise par exemple le solveur Z3 de Microsoft.
Son module Python s’installe avec
pip install z3-solver
On peut ensuite résoudre le problème précédent de cette façon :
from z3 import *
# Variables que le solveur va chercher
x, y, z = BitVecs("x y z", 32)
# Solveur
s = Solver()
# Contraintes sur ces variables
s.add(x > 0, x <= 50)
s.add(y > 0, y <= 100)
s.add(z > 0, z <= 100)
s.add((x + y) / 2 == z)
s.add((x * z) % 21 == 14)
s.add(((x + y) | z) & 0xFF == 126)
if s.check():
print(s.model())
else:
print("Solution non trouvée")Ces solveurs ne sont pas faits pour trouver toutes les solutions d’un problème, à la manière de la programmation linéaire, mais pour en trouver une le plus rapidement possible. En effet, même en ajoutant plusieurs ordres de grandeur au problème, il ne faut que quelques secondes de calcul au solveur pour trouver un résultat.