Programmation logique par
contraintes
Partie II
Plan du cours
• Programmation logique et Prolog (PL)
– SWI-Prolog, Sicstus
• Programmation logique par contraintes (PLC)
– Sicstus
• Problèmes de satisfaction de contraintes (CSP/PC)
– Choco
Qu’est-ce qu’une contrainte?
• Une contrainte est une formule logique, construite sur un
langage fixé dʼavance.
• Une contrainte dénote un ensemble de solutions (les solutions
de la formule) pour une interprétation logique fixée dʼavance.
• Exemple : La contrainte X + Y = 1 dénote les deux solutions {X
= 0, Y = 1} et {X = 1, Y = 0} si le domaine dʼinterprétation est N.
• Cʼest une généralisation des problèmes dʼunification :
– Problème dʼunification contrainte (formule)
– Unificateur Solution
• Utilité: Utiliser les techniques de la programmation logiques pour
des domaines autres que les termes symboliques.
Pourquoi faire?
• Problèmes combinatoires (jeux, . . .)
• Problèmes de planification (par exemple un emploi de
temps)
• Problèmes dʼordonnancement (par exemple trouver une
affectation de tâches à exécuter sur des machines)
• Problèmes de placement (par exemple placer des objets
dans un espace limité)
• Tous ces problèmes avec éventuellement une fonction
objective f à optimiser (utiliser un espace minimal, un
temps minimal, un nombre minimal de machines, . . .)
Comment ça marche ?
• Le programmeur utilise des contraintes (formules logiques) pour
modéliser son problème.
• Lʼinterprète Prolog peut faire appel à des solveurs de contraintes
pour savoir si une contrainte a une solution ou pas.
• Il y a des solveur de contraintes pour des domaines différents
(« Systèmes de contraintes ») : arithmétique, domaine finis, . . .
• Difficulté́ : en général ces solveurs ne sont pas complets !
Le rôle du programmeur?
• Choisir le bon système de contraintes
• Choisir la bonne modélisation du problème par contraintes
• Programmer lʼentrée/sortie
• Programmer la génération de contraintes
• Comprendre les conséquences de lʼincomplétude du solveurs de
contraintes, programmer une stratégie de recherche.
Exemple : Sudoko
Exemple : n reines
Exemple : peut-on construire la
maison en 14 jours
Exemple : Ordonnancement
• Exécuter des tâches sur plusieurs machines.
•
• Un ensemble de tâches est donné
– avec des précédences (des tâches doivent être terminées
avant dʼautres)
– et des ressources partagées (des tâches ont besoin de la
même machine)
• Déterminer pour toute tâche la machine et le temps
de démarrage,
– en satisfaisant les contraintes
– en minimisant le temps global
Plan de cette partie
• Généralités, Contraintes Arithmétiques sur R
• Contraintes : Syntaxe et sémantique
• Exemple : contraintes linéaires sur R
• Contraintes non-linéaires, solveurs
incomplets.
Contraintes : Syntaxe
• Donnée un langage de la logique du premier ordre :
• F: symboles de fonctions (et constantes);
• P: symboles de prédicat.
• Contrainte simple : Prédicat appliqué à des termes.
• Contrainte : conjonction de contraintes simples
– C = c1 ∧ c2 ∧ … ∧ ck
– Exemple X ≥ 42 ∧ X = Y + 2
• Contraintes spéciales :
– true : conjonction vide, toujours vraie
– false : toujours fausse
• Une contrainte est une formule de la logique du premier
ordre. (Normalement sans négation, disjonction,
quantificateurs)
Système de Contraintes
• Domaine de contraintes : D. Par exemple :
lʼensemble des entiers, lʼensemble des nombres
réels, . . .
• Un système de contraintes est donné par F,P,D et
une interprétation des symboles en F et P.
• Par exemple: Système des contraintes numériques
linéaires : F = {+,−,0,1,...},P = {=,≤,<,≥, >, ≠},D = N
• Interprétations : comme dʼhabitude.
• Autre systèmes de contraintes : nombres réels,
contraintes de Herbrand, contraintes de domaine fini,
contraintes dʼordre, . . .
Contraintes : Sémantiques
• Affectation : fonction partielle des variables vers le
domaine de contraintes.
• Une affectation θ viole une contrainte simple, si elle
la rend fausse, et viole une contrainte si elle viole au
moins une de ses contraintes simples.
• Une affectation θ est consistante pour une contrainte
si elle ne la viole pas.
• Solution : une affectation totale et consistante
– X ≥ 42 ∧ X = Y + 2 a une solution
– θ={X ←43,Y ←41}
• Cʼest exactement la sémantique de la logique du
premier ordre.
Contraintes : Satisfiabilité, équivalence
• Une contrainte est satisfaisable, si elle a une
solution.
• Lʼordre des contraintes simples peut être important,
certains algorithmes dépendent de lʼordre.
• Pour C=c1∧c2∧…∧ck on définit
– ensemble(C) = {c1,c2,...,ck}.
• Une contrainte c1 implique une contrainte c2 si toute
solution de c1 est aussi solution de c2.
– Anglais : c1 entails c2.
• Deux contraintes sont équivalentes si elles ont le
même ensemble de solutions (équivalence logique).
Problèmes de satisfaction de contraintes
Constraint Satisfaction Problems - CSP
Données :
– Les variables du probl`eme avec leur domaines
– Une contrainte C
Questions :
– C est satisfaisable ?
– Donnez une solution, si C en a une.
• Un solveur de contraintes répond à la
première question. Mais souvent aussi à la
deuxième.
Satisfaction de contraintes
• Comment résoudre le problème de
satisfaction de contrainte ?
• Approche naïve :
– essayer toutes les affectations ne marchera pas
pour les réelles, entiers, etc.
– pour les domaines finis, on va essayer dʼêtre plus
intelligent.
On risque de rencontrer des limites :
– Non-décidabilité
– Complexité (problèmes NP-complets, ou pire)
Exemple : équations linéaires sur R
• Langage :
– Constantes : R (on peut écrire toutes les constantes)
– Fonctions : + (binaire), − (unaire et binaire), ∗ (binaire)
– Prédicats : = (binaire)
• Pour lʼinstant, restriction à des termes
arithmétiques linéaires : pas de produits entre
variables.
• Domaine : R
• Interprétation : comme dʼhabitude.
Exemple : équations linéaires sur R
Exemples de contraintes arithmétiques linéaires :
• X = Y+Z ∧ Y = 1+Z
• 2∗Y = 17∗(X +42)−3∗X
Ne sont pas de contraintes arithmétiques linéaires :
• X = 5∗Y∗Z
• Y = X ∗ (42 + Z )
• 2∗X+Y∗Y = 3∗Z+Y∗Y
Exemple : Résolution de contraintes
arithmétiques linéaires
• Forme résolue : x1 =t1 ∧...∧ xn =tn où
– xi ≠ xj si i ≠ j
– xi ∉ V(tj) pour tous i, j.
• Toute forme résolue est satisfaisable en R.
• x1, . . . , xn : variables déterminées
• On a même le droit de choisir les valeurs des
variables non déterminées.
• En général : définition des formes résolues
fait partie du solveurs de contraintes.
Formes résolues
• Exemple dʼune forme résolue :
x1 = 2∗y+5∗z
x2 = 3−y−z
x3 = 42∗y−17∗z
• Une solution est:
y →1, z →1, x1 →7, x2 →1, x3 →25
• On peut même, pour nʼimporte quel choix de
valeurs pour y et z, trouver des valeurs de x1,
x2, x3 satisfaisant les équations.
Formes résolues
• Nʼest pas une forme résolue :
x1 = 2∗y+5∗z
17 = 42
• Nʼest pas une forme résolue :
x1 = 2∗x2+5∗z
x2 = 3−y−x3
x3 = 42∗y−17∗x1
Résoudre des contraintes arithmétiques
linéaires
• Lʼalgorithme est donné par des règles de
transformation.
• On applique les règles tant que possible, dans
nʼimporte quel ordre.
• Si on ne peut plus appliquer une règle on sʼarrête, et
on renvoie la contrainte obtenue.
• Equation normalisée :Soit une équation entre deux
constantes, soit une équation de la forme x = t où x ∉
V(t).
• Exemple dʼune équation normalisée : x = 17 + 3 ∗ y +
5 ∗ z.
• On peut transformer toute équation linéaire en une
équation normalisée qui lui est équivalente.
Résoudre des contraintes
arithmétiques linéaires
• Règle 1 : Choisir une équation non normalisée, et la
normaliser.
• Règle2: Sʼil y a une équation c1 =c2, où c1 et c2 sont
des constantes différentes, alors remplacer toute la
contrainte par ⊥.
• Règle 3: Sʼil y une équation c = c, où c constante, la
supprimer.
• Règle 4: Sʼil y a une équation normalisée x = t (avec
x ∉ V(t)) et x apparaît dans dʼautres équations alors
remplacer dans toutes les autres équations x par t.
exemple
x+1 = y+2
y+3 = z+4−2x
z+2 = 2x+u
• On résout la première équation pour x, et remplace x
par y + 1 :
x=y+1
3y+3 = z+2
z+2 = 2y+2+u
• On résout la deuxième équation pour z, on remplace
z par 3y + 1, on résout la dernière équation pour u, et
on obtient une forme résolue :
x=y+1
z = 3y+1
u = −3y−1
Correction du solveur
• Toute règle est une transformation
d’équivalence (les deux contraintes sont
équivalentes)
• Lʼapplication des règles termine toujours :
trouver un ordre de terminaison.
• Si aucune règle nʼest applicable alors on a
soit ⊥, soit une forme résolue.
Contraintes réelles en Sicstus
• Avec la bibliothèque clpr :
F = {+, −, ∗, /, sin, cos, tan,...}
P= {=,<,>,=<,>=, =/=,...}
D=R (les nombres réels)
• Ne pas oublier : use_module(library(clpr))
• Ecrire des contraintes entre accolades { et }
• Ecrire une virgule pour la conjonction logique.
Lʼexemple en Sicstus Prolog
?- use_module(library(clpr)).
?- {X+1=Y+2, Y+3=Z+4-2*X, Z+2=2*X+U}.
{Y= -1.0+X},
{Z= -2.0+3.0*X},
{U=X} ? ;
no
Ne sont pas des contraintes numériques
en Prolog:
– e1=:=e2 car il faut que e1 et e2 soient close.
– e1=e2 car Prolog traite les deux expressions de
façon syntaxique (unification).
– X is e car il faut que e soit close, et X une
variable.
Les contraintes expriment des relations.
Intégration des contraintes dans la
programmation logique
• Atome : Prédicat, ou contrainte
• Configuration : liste dʼatomes, plus une contrainte résolue
Notée : B | c
• Tant que la liste B nʼest pas vide : configuration a, Bʼ | c
– si le premier atome est un prédicat : le remplacer par le corps
dʼune clause de sa définition (comme Prolog)
– si le premier atome est une contrainte : appliquer le solveur de
contraintes à la contrainte a ∧ c.
• Si résultat ⊥ : échec.
• Si résultat est une forme résolue cʼ : passer à la configuration Bʼ | c′ .
• Donne lieu à un arbre de recherche comme Prolog.
Exemple : contraindre la somme dʼune liste
:- use_module(library(clpr)).
listsum([],X) :- {X=0}.
listsum([H|R],X) :-
{X = H + XR},
listsum(R,XR).
Exemple : contraindre la somme dʼune liste
?- listsum([2,3,4],X).
X = 9.0 ? ;
no
?- listsum([2,X,4],9).
X = 3.0 ? ;
no
?- listsum([2,X,Y],9).
{Y=7.0-X} ? ;
no
?- listsum(L,9).
L = [9.0] ? ;
L = [_A,_B],
{_B=9.0-_A} ? ;
L = [_A,_B,_C],
{_C=9.0-_A-_B} ? ;
…
Exécution du programme listsum
listsum([],X) :- {X=0}.
listsum([H|R],X) :-
{X = H + XR},
listsum(R,XR).
listsum([2, Y ], 5) |T
{5 = 2+XR},listsum([Y],XR) |T
listsum([Y],XR) | XR=3
{XR=Y+XR′ },listsum([],XR′ ) | XR=3
listsum([],XR′ ) | Y=3 -XRʼ
{XR′ =0} | Y=3 -XRʼ
|Y=3
Contraintes non-linéaires
• Maintenant on permet des équations
arithmétiques quelconques, pas nécessairement
linéaires.
• Par exemple X +(Y ∗Z)=3∗Z ∗Z ∗Z +2∗Y ∗Y
• Il est toujours théoriquement possible dʼécrire un
solveur de contraintes (résultat de Tarski, 1951).
Mais cet algorithme a une complexité
catastrophique.
• Cʼest possible car il sʼagit des nombres réels.
Solveurs incomplets
• En général, un solveur peut être incomplet.
• Un solveur peut donner trois réponses
possibles :
– « non » (ou ⊥)
– « oui » (ou une forme résolue)
– « je ne sais pas » (ou une formule seulement
partiellement résolue)
• Dans le cas dʼun solveur sur R : les équations
qui contiennent des produits entre variables
ne peuvent pas être traitées (sauf si
lʼéquation devient linaire à cause de
lʼinstantiation de variables).
Intégration de solveurs incomplets en
Prolog
• Quand une contrainte ne peut pas être traitée par le
solveur elle reste en suspens, et Prolog continue sur
lʼatome suivant.
• Quand la contrainte résolue est modifiée, les
contraintes en suspens sont examinées de nouveau.
• Implémentation plus efficace : maintenir une liste de
contraintes en suspens par variable, réexaminer
seulement les contraintes en suspens qui
contiennent une variable pour laquelle la contrainte
résolue a des nouvelles informations.
Exemple : somme des carrés
listsqsum([],X) :- {X=0}.
listsqsum([H|R],X) :-
{X = H*H + XR},
listsqsum(R,XR).
?- listsqsum([2,3,4],X).
X = 29.0 ?;
no
?- listsqsum([2,X,4],29).
{9.0-X^2.0=0.0};
no
Intérêts Composés
Le programme CLP(R) suivant exprime la formule des
intérêts composés avec le prédicat int(P,T,I,B,M) où :
P : capital
T : durée en mois
I : intérêt mensuel
B : balance
M : le montant mensuel
:- use_module(library(clpr)).
int(P,T,I,B,M):- {T > 0, T =< 1, B + M = P * (1 + I)}.
int(P,T,I,B,M):-
{T > 1, P1 = P * (1 + I) - M, T1 = T - 1},
int(P1, T1, I, B, M).
Intérêts Composés
?- int(120000, 120, 0.01, 0, M).
M = 1721.6513808310488 ? ;
No
?- int(P, 120, 0.01, 0, 1721.6513808310488).
P = 119999.99999999994 ? ;
no
?- int(P,120,0.01,0,M).
{M=0.014347094840258747*P} ? ;
No
Calcul de la température d’une surface discrétisée
On veut modéliser la température d’une feuille de métal. Pour cela, on
découpe la feuille en une matrice de dimension m x n de points. Si la
feuille est dans un état stable, chaque point de la matrice a la même
température que la moyenne de ses quatre voisins.
Etant données les températures des points limites, les valeurs des autres
points sont déterminées.
:-use_module(library(clpr)).
laplace([H1,H2,H3|T]):-
laplace_vec(H1,H2,H3),
laplace([H2,H3|T]).
laplace([_,_]).
laplace_vec([TL,T,TR|T1],[ML,M,MR|T2],[BL,B,BR|T3]):-
{B + T + ML + MR - 4 * M = 0},
laplace_vec([T,TR|T1],[M,MR|T2],[B,BR|T3]).
laplace_vec([_,_],[_,_],[_,_]).
Calcul de la température d’une surface discrétisée
test(X):- X = [
[0,0,0,0,0,0,0,0,0,0,0],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,_,_,_,_,_,_,_,_,_,100],
[100,100,100,100,100,100,100,100,100,100,100]
],
laplace(X).
test2(L):-L=[
[B11, B12, B13, B14],
[B21, M22, M23, B24],
[B31, M32, M33, B34],
[B41, B42, B43, B44]
],
laplace(L).
Calcul de la température d’une surface discrétisée
?- test(X).
? - test2(X).