Villkorsprogrammering

Villkorsprogrammering, på engelska constraint programming, är ett paradigm för att lösa kombinatoriska problem i vilket ett antal variabler med givna domäner skall tilldelas värden i enlighet med ett antal villkor. I villkorsprogrammering så deklarerar användaren villkor på de giltiga lösningarna vilka variablerna måste uppfylla. Området har av Association for Computing Machinery utpekats som strategiskt viktigt.

Vid villkorsprogrammering behöver inte någon sekvens specificeras, det är upp till den underliggande mjukvaran att testa kombinationer till dess en lösning hittats eller till dess det konstaterats att ingen lösning finns.

Exempel

Hur villkor deklareras beror på det underliggande språket. Följande modell skriven i MiniZinc är en modell för det klassiska SEND+MORE=MONEY-pusselproblemet.

include "globals.mzn";
% Skapa variabler
var 1..9: S;
var 0..9: E;
var 0..9: N;
var 0..9: D;
var 1..9: M;
var 0..9: O;
var 0..9: R;
var 0..9: Y;

constraint
  % Alla variabler ska ta unika värden
  all_different([S,E,N,D,M,O,R,Y]);

constraint
            1000*S + 100*E + 10*N + D  +  
            1000*M + 100*O + 10*R + E  = 
  10000*M + 1000*O + 100*N + 10*E + Y 
;

solve satisfy;

En variabel skapas för varje bokstav i pusslet. Varje bokstav tilldelas en domän 0..9 , eller 1..9 ifall det är en ledande siffra. Efter detta så deklareras först villkoret all_different som betyder att alla variabler i en giltig lösning måste ha unika värden. Detta villkor kommer inte ännu att reducera någon domän, utan kommer att sparas undan. Det andra, och sista, villkoret deklarerar att "SEND+MORE=MONEY" ska uppfyllas då varje bokstav byts ut mot ett motsvarande siffra. Från detta villkor kan den underliggande lösaren lista ut att variabeln M måste ta värdet 1, detta i sin tur kommer leda till att villkoret all_different tar bort värdet 1 från domänerna hos alla variabler förutom M.

Den sista raden solve satisfy instruerar den underliggande lösaren att den ska söka efter en giltig lösning och ge tillbaka den, givet att en giltig lösning finns.

Formalisering och versioner

Termerna villkorsprogram och villkorsprogrammering används omväxlande för att beskriva både en snävare familj av tekniker för att lösa kombinatoriska problem med diskreta variabler och en större uppsättning som också inkluderar närliggande tekniker och formaliseringar som även tillåter kontinuerliga variabeldomäner såsom satisfierbarhet modulo teorier (SMT).