Kısıt mantığı programlama - Constraint logic programming

Kısıtlama mantık programlama şeklidir kısıt programlama hangi, mantık programlama kavramları içerecek şekilde genişletilmiştir kısıt memnuniyeti . Kısıtlama mantık programı, tümcelerin gövdesinde kısıtlamalar içeren bir mantık programıdır. Kısıtlama içeren bir cümle örneği . Bu maddede, bir kısıtlamadır; , , ve normal mantık programlamasında olduğu gibi değişmez değerlerdir . Bu fıkra deyimi altında bir durumu belirtiyor : tutar sıfırdan büyük ve her ikisi de ve doğrudur. A(X,Y) :- X+Y>0, B(X), C(Y)X+Y>0A(X,Y)B(X)C(Y)A(X,Y)X+YB(X)C(Y)

Normal mantıksal programlamada olduğu gibi, programlar değişmezlere ek olarak kısıtlamalar içerebilen bir hedefin kanıtlanabilirliği hakkında sorgulanır. Bir amacın ispatı, gövdeleri tatmin edici kısıtlamalar olan maddelerden ve sırayla diğer maddeler kullanılarak ispatlanabilen değişmezlerden oluşur. Yürütme, hedeften başlayan ve hedefi kanıtlamaya çalışan tümceleri yinelemeli olarak tarayan bir tercüman tarafından gerçekleştirilir . Bu tarama sırasında karşılaşılan kısıtlamalar, kısıtlama deposu adı verilen bir kümeye yerleştirilir . Bu kümenin tatmin edici olmadığı tespit edilirse, tercüman hedefi kanıtlamak için diğer tümceleri kullanmaya çalışarak geri adım atar . Uygulamada, kısıtlama deposunun tatmin ediciliği, her zaman tutarsızlığı tespit etmeyen eksik bir algoritma kullanılarak kontrol edilebilir.

genel bakış

Resmi olarak, kısıtlama mantığı programları normal mantık programları gibidir, ancak tümcelerin gövdesi, normal mantık programlama değişmezlerine ek olarak kısıtlamalar içerebilir. Örnek olarak, X>0bir kısıtlamadır ve aşağıdaki kısıtlama mantık programının son maddesine dahil edilmiştir.

B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).

Normal mantık programlamasında olduğu gibi, gibi bir hedefi A(X,1)değerlendirmek, son tümcenin gövdesini ile değerlendirmeyi gerektirir Y=1. Normal mantıksal programlamada olduğu gibi, bu da amacı kanıtlamayı gerektirir B(X,1). Normal mantıksal programlamanın aksine, bu aynı zamanda bir kısıtlamanın da yerine getirilmesini gerektirir: X>0, son tümcenin gövdesindeki kısıtlama (düzenli mantık programlamada, X tam bir temel terime bağlı olmadıkça ve yürütmenin yürütülmesi dışında X>0 kanıtlanamaz . durum böyle değilse program başarısız olur).

Bir kısıtlamanın karşılanıp karşılanmadığı, kısıtlamayla karşılaşıldığında her zaman belirlenemez. Bu durumda, örneğin, Xson fıkra değerlendirilirken değeri belirlenmez. Sonuç olarak, X>0bu noktada kısıtlama sağlanmaz veya ihlal edilmez. Aksine değerlendirilmesinde geçmeden daha B(X,1)sonra elde edilen değer olup olmadığını kontrol Xsonradan pozitiftir, tercüman depolar kısıt X>0sonra ve değerlendirilmesinde ilerler B(X,1); bu sayede yorumcu X>0, değerlendirme sırasında kısıtlamanın ihlal edildiğini tespit edebilir B(X,1)ve bu durumda değerlendirmenin B(X,1)sonuçlanmasını beklemek yerine hemen geri dönebilir .

Genel olarak, bir kısıtlama mantık programının değerlendirilmesi, normal bir mantık programının yaptığı gibi ilerler. Ancak, değerlendirme sırasında karşılaşılan kısıtlamalar, kısıtlama deposu adı verilen bir kümeye yerleştirilir. Örnek olarak, amacın A(X,1)değerlendirilmesi, birinci fıkranın gövdesini Y=1; bu değerlendirme X>0, kısıtlama deposuna eklenir ve hedefin B(X,1)kanıtlanmasını gerektirir . Bu amacı kanıtlamaya çalışırken, birinci fıkra uygulanır, ancak değerlendirmesi X<0kısıtlama deposuna eklenir . Bu ekleme, kısıtlama deposunu tatmin edilemez hale getirir. Yorumlayıcı daha sonra geri döner ve son eklemeyi kısıtlama deposundan kaldırır. İkinci fıkranın değerlendirilmesi , kısıtlama deposuna X=1ve ekler Y>0. Kısıt deposu tatmin edici olduğundan ve kanıtlanacak başka bir hazır bilgi kalmadığından, yorumlayıcı çözümle durur X=1, Y=1.

anlambilim

Kısıtlama mantığı programlarının semantiği, yürütme sırasında bir çifti koruyan sanal bir yorumlayıcı olarak tanımlanabilir . Bu çiftin ilk elemanına mevcut hedef denir; ikinci öğeye kısıtlama deposu denir. Geçerli hedefi tercüman kanıtlamaya çalışıyor ve aynı zamanda tatmin çalışıyor bazı kısıtlamalar içerebilir değişmezleri içerir; kısıt mağaza tercüman şimdiye kadar karşılanabilir üstlenmiş olduğu tüm sınırlamalar içeriyor. ${\displaystyle \langle G,S\rangle }$

Başlangıçta, geçerli hedef hedeftir ve kısıtlama deposu boştur. Yorumlayıcı, mevcut hedeften ilk öğeyi çıkararak ve onu analiz ederek ilerler. Bu analizin detayları aşağıda açıklanmıştır, ancak sonuçta bu analiz başarılı bir sonlandırma veya başarısızlıkla sonuçlanabilir. Bu analiz, özyinelemeli çağrıları ve mevcut hedefe yeni değişmezlerin eklenmesini ve kısıtlama deposuna yeni kısıtlamayı içerebilir . Bir hata oluşursa yorumlayıcı geri döner. Geçerli hedef boş olduğunda ve kısıtlama deposu tatmin edici olduğunda başarılı bir sonlandırma oluşturulur.

Hedeften çıkarılan bir kelimenin analizinin detayları aşağıdaki gibidir. Bu literal hedefin önünden çıkarıldıktan sonra bir kısıtlama mı yoksa literal mi olduğu kontrol edilir. Bir kısıtlama ise, kısıtlama deposuna eklenir. Bir değişmez ise, başı değişmez ile aynı yüklemi olan bir yan tümce seçilir; yan tümce, değişkenlerini yeni değişkenlerle (hedefte oluşmayan değişkenler) değiştirerek yeniden yazılır: sonuç, yan tümcenin yeni bir varyantı olarak adlandırılır ; cümlenin yeni varyantının gövdesi daha sonra hedefin önüne yerleştirilir; literalin her bir argümanının, yeni değişken kafanın karşılık gelen biriyle eşitliği de hedefin önüne yerleştirilir.

Bu işlemler sırasında bazı kontroller yapılır. Özellikle, kısıtlama deposu, ona her yeni kısıtlama eklendiğinde tutarlılık açısından kontrol edilir. Prensip olarak, kısıtlama deposu tatmin edici olmadığında, algoritma geri dönebilir. Ancak, her adımda tatminsizliğin kontrol edilmesi verimsiz olacaktır. Bu nedenle, bunun yerine eksik bir tatmin edicilik denetleyicisi kullanılabilir. Pratikte, tatmin edicilik, kısıtlama deposunu basitleştiren, yani onu eşdeğer ancak çözmesi daha basit bir forma yeniden yazan yöntemler kullanılarak kontrol edilir. Bu yöntemler bazen, ancak her zaman değil, tatmin edilemez bir kısıtlama deposunun tatmin edilemezliğini kanıtlayabilir.

Yorumlayıcı, mevcut hedef boş olduğunda ve kısıtlama deposunun tatmin edici olmadığı tespit edildiğinde hedefi kanıtlamıştır. Yürütmenin sonucu, geçerli (basitleştirilmiş) kısıtlamalar kümesidir. Bu küme, değişkenleri belirli bir değere zorlayan kısıtlamalar içerebilir , ancak belirli bir değer vermeden yalnızca değişkenleri sınırlayan kısıtlamalar da içerebilir . ${\görüntüleme stili X=2}$${\displaystyle X>2}$

Resmi olarak, kısıtlama mantığı programlamasının semantiği, türevler cinsinden tanımlanır . Bir geçiş, not edilen bir çift hedef/depolamadır . Böyle bir çifti durumundan gitme ihtimalini bildiren durumuna . Böyle bir geçiş üç olası durumda mümkündür: ${\displaystyle \langle G,S\rangle \rightarrow \langle G',S'\rangle }$${\displaystyle \langle G,S\rangle }$${\displaystyle \langle G',S'\rangle }$

• unsuru G bir kısıtlama Cı , ve ; başka bir deyişle, bir kısıtlama hedeften kısıtlama deposuna taşınabilir.${\displaystyle G'=G\ters eğik çizgi \{C\}}$${\displaystyle S'=S\cup \{C\}}$
• unsuru G hazır bilgi olup, yeni değişkenleri kullanılarak yeniden, bir madde vardır, , olup G ile değiştirilir , ve ; başka bir deyişle, bir hazır bilgi, başında aynı yüklemi olan bir tümcenin yeni bir varyantının gövdesiyle değiştirilebilir, yeni varyantın gövdesi ve yukarıdaki terim eşitlikleri hedefe eklenebilir.${\displaystyle L(t_{1},\ldots ,t_{n})}$${\displaystyle L(t_{1}',\ldots ,t_{n}'):-B}$${\görüntüleme stili G'}$${\displaystyle L(t_{1},\ldots ,t_{n})}$${\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B}$${\görüntüleme stili S'=S}$
• S ve belirli kısıtlama semantiğine göre eşdeğerdir${\ Displaystyle S'}$

Bir geçiş dizisi bir türetmedir. Bir hedef G, bir türetme mevcutsa ispat edilebilir için bir karşılanabilir kısıtlama deposu için S . Bu semantik, işlenecek hedefin değişmezini ve değişmezlerin yerini alacak yan tümceyi keyfi olarak seçen bir yorumlayıcının olası evrimlerini resmileştirir. Başka bir deyişle, boş bir hedefe ve tatmin edici bir depoya yol açan, muhtemelen birçokları arasında bir dizi hazır bilgi ve yan tümce seçeneği varsa, bu semantik altında bir hedef kanıtlanır. ${\displaystyle \langle G,\emptyset \rangle }$${\displaystyle \langle \emptyset ,S\rangle }$

Gerçek tercümanlar, hedef öğeleri bir LIFO düzeninde işler: öğeler önden eklenir ve önden işlenir. Ayrıca ikinci kuralın yan tümcesini yazıldıkları sıraya göre seçerler ve değiştirildiğinde kısıtlama deposunu yeniden yazarlar.

Üçüncü olası geçiş türü, kısıtlama deposunun eşdeğeri ile değiştirilmesidir. Bu değiştirme, kısıtlama yayılımı gibi belirli yöntemlerle yapılanlarla sınırlıdır . Kısıtlama mantığı programlamasının semantiği, yalnızca kullanılan kısıtlamaların türü için değil, aynı zamanda kısıtlama deposunu yeniden yazma yöntemi için de parametriktir. Uygulamada kullanılan özel yöntemler, kısıtlama deposunu çözmesi daha basit olanla değiştirir. Kısıt deposu tatmin edici değilse, bu sadeleştirme bu tatminsizliği bazen tespit edebilir, ancak her zaman değil.

Bir hedefin bir kısıt mantık programına karşı değerlendirilmesinin sonucu, hedef kanıtlanırsa tanımlanır. Bu durumda, ilk çiftten hedefin boş olduğu bir çifte bir türetme vardır. Bu ikinci çiftin kısıt deposu, değerlendirmenin sonucu olarak kabul edilir. Bunun nedeni, kısıtlama deposunun, hedefi kanıtlamak için tatmin edici olduğu varsayılan tüm kısıtlamaları içermesidir. Başka bir deyişle, bu kısıtlamaları karşılayan tüm değişken değerlendirmeleri için amaç kanıtlanmıştır.

İki değişmezin terimlerinin ikili eşitliği genellikle şu şekilde ifade edilir : bu, kısıtlamalar için bir kestirme yoldur . Kısıtlama mantığı programlaması için semantiğin yaygın bir çeşidi, hedeften ziyade doğrudan kısıtlama deposuna eklenir . ${\displaystyle L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')}$${\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'}$${\displaystyle L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')}$

Şartlar ve koşullar

Farklı türde kısıtlama mantığı programlaması üreten farklı terim tanımları kullanılır: ağaçlar, gerçekler veya sonlu alanlar üzerinde. Her zaman mevcut olan bir tür kısıtlama, terimlerin eşitliğidir. Bu tür kısıtlamalar gereklidir, çünkü yorumlayıcı t1=t2, bir hazır bilgi P(...t1...), head olan bir yeni varyantın gövdesiyle değiştirildiğinde hedefe ekler P(...t2...).

Ağaç terimleri

Ağaç terimleriyle kısıtlama mantığı programlaması, ikameleri kısıtlama deposunda kısıtlamalar olarak depolayarak normal mantık programlamaya öykünür. Terimler, diğer terimlere uygulanan değişkenler, sabitler ve fonksiyon sembolleridir. Dikkate alınan tek kısıtlama, terimler arasındaki eşitlikler ve eşitsizliklerdir. Gibi kısıtlamalar t1=t2genellikle yorumlayıcı tarafından oluşturulduğundan eşitlik özellikle önemlidir . Terimlerdeki eşitlik kısıtlamaları basitleştirilebilir, yani birleştirme yoluyla çözülebilir :

Her t1=t2iki terim de diğer terimlere uygulanan işlev sembolleriyse, bir kısıtlama basitleştirilebilir. İki fonksiyon sembolü aynıysa ve alt terim sayısı da aynıysa, bu kısıtlama alt terimlerin ikili eşitliği ile değiştirilebilir. Terimler farklı işlev sembollerinden veya aynı işlevden oluşuyor ancak farklı sayıda terimden oluşuyorsa, kısıtlama tatmin edici değildir.

İki terimden biri bir değişkense, değişkenin alabileceği tek izin verilen değer diğer terimdir. Sonuç olarak, diğer terim, mevcut hedef ve kısıtlama deposundaki değişkenin yerini alabilir, böylece değişkeni pratik olarak dikkate alınmaz. Bir değişkenin kendisiyle eşitliğinin özel durumunda, kısıtlama her zaman sağlandığı gibi kaldırılabilir.

Bu kısıtlama tatmini biçiminde, değişken değerler terimlerdir.

gerçekler

Gerçek sayılarla kısıtlama mantığı programlaması , gerçek ifadeleri terim olarak kullanır. Hiçbir fonksiyon sembolü kullanılmadığında, terimler, muhtemelen değişkenler de dahil olmak üzere, gerçekler üzerindeki ifadelerdir. Bu durumda, her değişken değer olarak yalnızca gerçek bir sayı alabilir.

Kesin olmak gerekirse, terimler değişkenler ve gerçek sabitler üzerindeki ifadelerdir. Terimler arasındaki eşitlik, yorumlayıcı, yürütme sırasında terimlerin eşitliğini oluşturduğundan, her zaman mevcut olan bir tür kısıtlamadır. Örnek olarak, mevcut hedefin ilk değişmezi ise A(X+1)ve yorumlayıcı A(Y-1):-Y=1değişkenler yeniden yazıldıktan sonra bir tümce seçtiyse, mevcut hedefe eklenen kısıtlamalar X+1=Y-1ve . İşlev sembolleri için kullanılan sadeleştirme kuralları açıkça kullanılmamaktadır: ilk ifade kullanılarak oluşturulduğu ve ikinci ifade kullanılarak oluşturulduğu için tatmin edici değildir . ${\görüntüleme stili Y=1}$X+1=Y-1+-

Gerçekler ve fonksiyon sembolleri birleştirilebilir, bu da gerçekler üzerinde ifadeler olan terimlere ve diğer terimlere uygulanan fonksiyon sembollerine yol açar. Biçimsel olarak, değişkenler ve gerçek sabitler, diğer ifadeler üzerindeki herhangi bir aritmetik operatör gibi ifadelerdir. Değişkenler, sabitler (sıfır işlevli simgeler) ve ifadeler, terimlere uygulanan herhangi bir işlev simgesi gibi terimlerdir. Başka bir deyişle, terimler ifadeler üzerine, ifadeler ise sayılar ve değişkenler üzerine kurulur. Bu durumda, değişkenler gerçek sayılar ve terimler arasında değişir . Başka bir deyişle, bir değişken değer olarak gerçek bir sayı alabilirken, bir diğeri bir terim alabilir.

İki terimden hiçbiri gerçek bir ifade değilse, iki terimin eşitliği ağaç terimleri için kurallar kullanılarak basitleştirilebilir. Örneğin, iki terim aynı işlev sembolüne ve alt terim sayısına sahipse, eşitlik kısıtlaması alt terimlerin eşitliği ile değiştirilebilir.

sonlu alanlar

Kısıtlama mantığı programlamasında kullanılan üçüncü kısıtlama sınıfı, sonlu etki alanlarıdır. Değişkenlerin değerleri bu durumda sonlu bir bölgeden alınır, genellikle tamsayı sayılarıdır . Her bir değişken için, farklı bir etki alanı belirtilebilir: X::[1..5]değeri, bu, örneğin bir araç Xarasındadır 1ve 5. Bir değişkenin alanı, bir değişkenin alabileceği tüm değerleri numaralandırarak da verilebilir; bu nedenle, yukarıdaki alan beyanı da yazılabilir X::[1,2,3,4,5]. Bir etki alanı belirtmenin bu ikinci yolu, gibi tamsayılardan oluşmayan etki alanlarına izin verir X::[george,mary,john]. Bir değişkenin etki alanı belirtilmemişse, dilde temsil edilebilen tamsayılar kümesi olduğu varsayılır. Gibi bir bildirim kullanılarak bir değişken grubuna aynı etki alanı verilebilir [X,Y,Z]::[1..5].

Bir değişkenin etki alanı, yürütme sırasında azaltılabilir. Aslında yorumlayıcı kısıtlama deposuna kısıtlamalar eklediğinden, bir tür yerel tutarlılığı zorlamak için kısıtlama yayılımı gerçekleştirir ve bu işlemler değişkenlerin alanını azaltabilir. Bir değişkenin etki alanı boşalırsa, kısıtlama deposu tutarsız olur ve algoritma geri döner. Bir değişkenin etki alanı bir singleton olursa, değişkene etki alanındaki benzersiz değer atanabilir. Tipik olarak uygulanan tutarlılık biçimleri, yay tutarlılığı , hiper-yay tutarlılığı ve sınır tutarlılığıdır . Bir değişkenin geçerli etki alanı, belirli değişmezler kullanılarak incelenebilir; örneğin, bir değişkenin geçerli etki alanını bulur . dom(X,D)DX

Gerçeklerin etki alanlarına gelince, işlevler tamsayıların etki alanları ile kullanılabilir. Bu durumda, bir terim tamsayılar üzerinde bir ifade, bir sabit veya diğer terimler üzerinde bir functor uygulaması olabilir. Bir değişken, etki alanı bir tamsayı veya sabitler kümesi olarak belirtilmemişse, rastgele bir terimi değer olarak alabilir.

kısıtlama deposu

Kısıt deposu, şu anda karşılanabilir olduğu varsayılan kısıtlamaları içerir. Normal mantık programlaması için mevcut ikamenin ne olduğu düşünülebilir. Yalnızca ağaç terimlerine izin verildiğinde, kısıtlama deposu şu şekilde kısıtlamalar içerir t1=t2; bu kısıtlamalar birleştirme ile basitleştirilir, bu da formun kısıtlamaları ile sonuçlanır variable=term; bu tür kısıtlamalar bir ikameye eşdeğerdir.

Ancak, kısıtlama deposu, terimler arasındaki t1!=t2farka !=izin veriliyorsa , formdaki kısıtlamaları da içerebilir . Gerçekler veya sonlu alanlar üzerindeki kısıtlamalara izin verildiğinde, kısıtlama deposu X+2=Y/2, vb. gibi alana özgü kısıtlamalar da içerebilir .

Kısıt deposu, mevcut ikame kavramını iki şekilde genişletir. Birincisi, yalnızca bir değişmezi bir tümcenin yeni bir varyantının başıyla eşitlemekten türetilen kısıtlamaları değil, aynı zamanda tümce gövdesinin kısıtlamalarını da içerir. İkincisi, yalnızca formun variable=valuekısıtlamalarını değil, aynı zamanda dikkate alınan kısıtlama dili üzerindeki kısıtlamaları da içerir. Normal bir mantık programının başarılı bir değerlendirmesinin sonucu nihai ikame iken, bir kısıtlama mantık programının sonucu, değişken=değer biçimindeki kısıtlamayı içerebilen ancak genel olarak keyfi kısıtlamalar içerebilen son kısıtlama deposudur.

Etki alanına özgü kısıtlamalar, hem bir tümcenin gövdesinden hem de bir değişmez değeri bir yan tümce başlığıyla eşitlemekten kısıtlama deposuna gelebilir: örneğin, yorumlayıcı değişmezi A(X+2), yeni değişken başlığı olan bir yan tümceyle yeniden yazarsa A(Y/2), kısıtlama buna X+2=Y/2eklenir. kısıtlama deposu. Bir değişken gerçek veya sonlu alan ifadesinde görünüyorsa, yalnızca gerçellerde veya sonlu alanda bir değer alabilir. Böyle bir değişken, diğer terimlere uygulanan bir işlevden oluşan bir terimi değer olarak alamaz. Bir değişken hem belirli etki alanının bir değerini hem de terimlere uygulanan bir işlevciyi almaya bağlıysa, kısıtlama deposu tatmin edici değildir.

Kısıt deposuna bir kısıt eklendikten sonra, kısıt deposunda bazı işlemler gerçekleştirilir. Hangi işlemlerin gerçekleştirileceği, dikkate alınan etki alanına ve kısıtlamalara bağlıdır. Örneğin, sonlu ağaç eşitlikleri için birleştirme , gerçekler üzerindeki polinom denklemleri için değişken eleme , sonlu alanlar için bir yerel tutarlılık biçimini zorlamak için kısıtlama yayılımı kullanılır . Bu işlemler, kısıt deposunun tatmin edilebilirlik açısından kontrol edilmesini ve çözülmesini kolaylaştırmayı amaçlamaktadır.

Bu işlemler sonucunda yeni kısıtların eklenmesi eskileri değiştirebilir. Tercümanın geri döndüğünde bu değişiklikleri geri alabilmesi önemlidir. En basit durum yöntemi, yorumlayıcının her seçim yaptığında deponun tam durumunu kaydetmesidir (bir hedefi yeniden yazmak için bir madde seçer). Kısıt deposunun önceki bir duruma dönmesine izin vermek için daha verimli yöntemler mevcuttur. Özellikle, eski kısıtlamalarda yapılan değişiklikler de dahil olmak üzere, iki seçim noktası arasında yapılan kısıtlama deposundaki değişiklikler kaydedilebilir. Bu, değiştirilen kısıtlamaların eski değerini kaydederek yapılabilir; bu yönteme izleme denir . Daha gelişmiş bir yöntem, değiştirilen kısıtlamalarda yapılan değişiklikleri kaydetmektir. Örneğin, bir doğrusal kısıtlama, katsayısı değiştirilerek değiştirilir: eski ve yeni katsayı arasındaki farkı kaydetmek, bir değişikliğin geri alınmasına izin verir. Bu ikinci yönteme anlamsal geri izleme adı verilir , çünkü değişikliğin anlamı yalnızca kısıtlamaların eski sürümü yerine kaydedilir.

etiketleme

Etiketleme değişmezleri, kısıtlama deposunun tatmin edilebilirliğini veya kısmi tatmin edilebilirliğini kontrol etmek ve tatmin edici bir atama bulmak için sonlu alanlar üzerindeki değişkenler üzerinde kullanılır. Bir etiketleme değişmezi, labeling([variables])argümanın sonlu etki alanları üzerindeki değişkenlerin bir listesi olduğu biçimdedir . Yorumlayıcı böyle bir değişmez değeri değerlendirdiğinde, ilgili tüm kısıtlamaları karşılayan bir atama bulmak için listenin değişkenlerinin etki alanları üzerinde bir arama yapar. Tipik olarak, bu bir tür geri izleme ile yapılır : değişkenler sırayla değerlendirilir, her biri için olası tüm değerler denenir ve tutarsızlık tespit edildiğinde geri izleme yapılır.

Etiketleme değişmezinin ilk kullanımı, kısıtlama deposunun gerçek tatmin edilebilirliğini veya kısmi tatmin edilebilirliğini kontrol etmektir. Yorumlayıcı, kısıtlama deposuna bir kısıtlama eklediğinde, bunun üzerinde yalnızca bir tür yerel tutarlılık uygular. Bu işlem, kısıtlama deposu tatmin edici olmasa bile tutarsızlığı algılamayabilir. Bir değişkenler kümesi üzerinde bir etiketleme değişmezi, bu değişkenler üzerindeki kısıtlamaların bir tatmin edilebilirlik kontrolünü zorlar. Sonuç olarak, kısıt deposunda belirtilen tüm değişkenlerin kullanılması, mağazanın tatmin ediciliğinin kontrol edilmesini sağlar.

Etiketleme değişmezinin ikinci kullanımı, kısıtlama deposunu karşılayan değişkenlerin bir değerlendirmesini fiilen belirlemektir. Etiketleme değişmezi olmadan, yalnızca kısıtlama deposu formun bir kısıtlamasını içerdiğinde X=valueve yerel tutarlılık bir değişkenin alanını tek bir değere indirdiğinde değişkenlere değerler atanır . Bazı değişkenler üzerinde bir etiketleme değişmezi, bu değişkenleri değerlendirilmeye zorlar. Diğer bir deyişle, etiketleme değişmezi dikkate alındıktan sonra tüm değişkenlere bir değer atanır.

Tipik olarak, kısıtlama mantığı programları, etiketleme değişmezleri ancak kısıtlama deposunda mümkün olduğu kadar çok kısıtlama biriktikten sonra değerlendirilir. Bunun nedeni, sabit değerleri etiketlemenin aramayı zorlaması ve yerine getirilmesi gereken daha fazla kısıtlama varsa aramanın daha verimli olmasıdır. Bir kısıtlama tatmin sorunu tipik olarak aşağıdaki yapıya sahip bir kısıtlama mantık programı tarafından çözülür:

solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)

Yorumlayıcı hedefi değerlendirdiğinde, solve(args)birinci fıkranın yeni bir varyantının gövdesini mevcut hedefe yerleştirir. İlk hedef olduğundan constraints(X'), ikinci fıkra değerlendirilir ve bu işlem mevcut hedefteki ve sonunda kısıtlama deposundaki tüm kısıtlamaları hareket ettirir. Daha labeling(X')sonra değişmez değer değerlendirilir ve kısıtlama deposunun bir çözümünü aramaya zorlanır. Kısıt deposu, orijinal kısıt tatmin probleminin kısıtlamalarını tam olarak içerdiğinden, bu işlem orijinal problemin bir çözümünü arar.

Program reformülasyonları

Belirli bir kısıtlama mantığı programı, verimliliğini artırmak için yeniden formüle edilebilir. Birinci kural, etiketlenmiş değişmezler üzerindeki kısıtlama deposunda biriken kadar çok kısıtlamanın ardından etiketleme değişmezlerinin yerleştirilmesi gerektiğidir. Teoride eşdeğer olmakla birlikte , yorumlayıcı etiketleme değişmeziyle karşılaştığında gerçekleştirilen arama, kısıtlamayı içermeyen bir kısıtlama deposundadır . Sonuç olarak , daha sonra bu kısıtlamayı karşılamadığı anlaşılan gibi çözümler üretebilir . Öte yandan, ikinci formülasyonda arama, yalnızca kısıtlama zaten kısıtlama deposundayken gerçekleştirilir. Sonuç olarak, arama, ek kısıtlamaların arama alanını azalttığı gerçeğinden yararlanarak, yalnızca kendisiyle tutarlı olan çözümleri döndürür. A(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1

Verimliliği artırabilecek ikinci bir yeniden formüle etme, kısıtlamaları tümcelerin gövdesinde değişmez değerlerden önce yerleştirmektir. Yine ve prensipte eşdeğerdir. Ancak, ilki daha fazla hesaplama gerektirebilir. Örneğin, kısıtlama deposu kısıtlamayı içeriyorsa , yorumlayıcı ilk durumda yinelemeli olarak değerlendirir ; başarılı olursa, kısıtlama deposunun eklerken tutarsız olduğunu anlar . İkinci durumda, bu maddeyi değerlendirirken, yorumlayıcı önce kısıtlama deposuna ekler ve sonra muhtemelen değerlendirir . Kısıt deposunun eklenmesinden sonra tutarsız olduğu ortaya çıktığından, özyinelemeli değerlendirmesi hiç yapılmaz. A(X):-B(X),X>0A(X):-X>0,B(X)X<-2B(X)X>0X>0B(X)X>0B(X)

Verimliliği artırabilecek üçüncü bir yeniden formül, gereksiz kısıtlamaların eklenmesidir. Programcı (her ne şekilde olursa olsun) bir problemin çözümünün belirli bir kısıtlamayı karşıladığını biliyorsa, kısıtlama deposunun tutarsızlığını mümkün olan en kısa sürede sağlamak için bu kısıtlamayı dahil edebilir. Örneğin, değerlendirmesinin B(X)pozitif bir değerle sonuçlanacağı önceden biliniyorsa X, programcı X>0herhangi bir oluşmadan önce ekleme yapabilir B(X). Örnek olarak, A(X,Y):-B(X),C(X)hedefte başarısız olur A(-2,Z), ancak bu yalnızca alt hedefin değerlendirilmesi sırasında bulunur B(X). Öte yandan, yukarıdaki fıkra ile değiştirilirse , yorumlayıcı , eşit değerlendirmesi başlamadan önce olan kısıtlama deposuna kısıtlama eklenir eklenmez geri döner . A(X,Y):-X>0,A(X),B(X)X>0B(X)

Kısıt işleme kuralları

Kısıt işleme kuralları , başlangıçta kısıtlama çözücüleri belirtmek için tek başına bir formalizm olarak tanımlandı ve daha sonra mantık programlamaya gömüldü. İki tür kısıtlama işleme kuralı vardır. Birinci tür kurallar, belirli bir koşul altında bir dizi kısıtlamanın diğerine eşdeğer olduğunu belirtir. İkinci tür kurallar, belirli bir koşul altında bir dizi kısıtlamanın bir başkasını ima ettiğini belirtir. Kısıtlama işleme kurallarını destekleyen bir kısıtlama mantığı programlama dilinde, bir programcı kısıtlama deposunun olası yeniden yazımlarını ve buna olası kısıtlama eklemelerini belirtmek için bu kuralları kullanabilir. Aşağıdakiler örnek kurallardır:

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

İlk kural B(X), mağaza tarafından A(X)zorunlu kılınırsa , kısıtlamanın olarak yeniden yazılabileceğini söyler C(X). Örnek N*X>0olarak X>0, mağaza bunu ima ediyormuş gibi yeniden yazılabilir N>0. Sembol <=>, mantıktaki eşdeğerliğe benzer ve ilk kısıtlamanın ikincisine eşdeğer olduğunu söyler. Pratikte bu, ilk kısıtlamanın ikincisiyle değiştirilebileceği anlamına gelir .

Bunun yerine ikinci kural, eğer ortadaki kısıtlama kısıtlama deposu tarafından gerektiriyorsa, ikinci kısıtlamanın birincinin bir sonucu olduğunu belirtir. Sonuç olarak, A(X)kısıtlama deposundaysa ve kısıtlama deposu B(X)tarafından gerekliyse , mağazaya C(X)eklenebilir. Denklik durumundan farklı olarak, bu bir eklemedir, değiştirme değil: yeni kısıtlama eklenir, ancak eskisi kalır.

Denklik, bazı kısıtlamaları daha basit olanlarla değiştirerek kısıtlama deposunu basitleştirmeye izin verir; özellikle, bir denklik kuralındaki üçüncü kısıtlama ise trueve ikinci kısıtlama zorunluysa, birinci kısıtlama kısıtlama deposundan kaldırılır. Çıkarım, kısıtlama deposunun tutarsızlığının kanıtlanmasına yol açabilecek ve genellikle tatmin edilebilirliğini belirlemek için gereken arama miktarını azaltabilecek yeni kısıtlamaların eklenmesine izin verir.

Kısıt işleme kurallarıyla birlikte mantıksal programlama maddeleri, kısıtlama deposunun tatmin edilebilirliğini belirlemek için bir yöntem belirtmek için kullanılabilir. Yöntemin farklı seçimlerini uygulamak için farklı maddeler kullanılır; kısıtlama işleme kuralları, yürütme sırasında kısıtlama deposunu yeniden yazmak için kullanılır. Örnek olarak, bu şekilde birim yayılımı ile geri izleme uygulanabilir . Let holds(L), listedeki değişmezlerin değerlendirildikleri sırada olduğu bir önerme cümlesini temsil eder L. Algoritma, bir değişmez değeri doğru veya yanlış olarak atama seçimi için yan tümceler ve yayılımı belirtmek için kısıtlama işleme kuralları kullanılarak uygulanabilir. Bu kurallar belirtmek holds([l|L])durumunda kaldırılabilir l=truemağazadan takip ve gibi tekrar yazılabilir holds(L)eğer l=falsemağazadan izler. Benzer şekilde, holds([l])ile değiştirilebilir l=true. Bu örnekte, bir değişken için değer seçimi, mantıksal programlamanın yan tümceleri kullanılarak gerçekleştirilir; ancak, ayrık kısıtlama işleme kuralları veya CHR ^∨ adı verilen bir uzantı kullanılarak kısıtlama işleme kurallarında kodlanabilir .

Aşağıdan yukarıya değerlendirme

Mantık programlarının standart değerlendirme stratejisi yukarıdan aşağıya ve derinlikten öncedir : hedeften, hedefi kanıtlayabilecek bir dizi madde tanımlanır ve bedenlerinin değişmezleri üzerinde özyineleme gerçekleştirilir. Alternatif bir strateji, gerçeklerden başlamak ve yeni gerçekleri türetmek için tümcecikleri kullanmaktır; bu stratejiye aşağıdan yukarıya denir . Amaç, tek bir amacı kanıtlamak yerine belirli bir programın tüm sonuçlarını üretmek olduğunda, yukarıdan aşağıya olandan daha iyi kabul edilir. Özellikle, bir programın tüm sonuçlarını standart yukarıdan aşağıya ve derinlik öncelikli şekilde bulmak, aşağıdan yukarıya değerlendirme stratejisi sona ererken sona ermeyebilir.

Aşağıdan yukarıya değerlendirme stratejisi, değerlendirme sırasında şimdiye kadar kanıtlanmış gerçekleri korur. Bu küme başlangıçta boştur. Her adımda, mevcut olgulara bir program maddesi uygulanarak yeni olgular türetilir ve kümeye eklenir. Örneğin, aşağıdaki programın aşağıdan yukarıya değerlendirilmesi iki adım gerektirir:

A(q).
B(X):-A(X).

Sonuçlar kümesi başlangıçta boştur. İlk adımda, A(q)gövdesi kanıtlanabilen (çünkü boş olduğu için) tek tümcedir ve A(q)bu nedenle mevcut sonuçlara eklenir. İkinci adımda, A(q)ispat edildiğinden, ikinci fıkra kullanılabilir ve B(q)sonuçlara eklenir. 'den başka bir sonuç kanıtlanamadığı için {A(q),B(q)}yürütme sona erer.

Aşağıdan yukarıya değerlendirmenin yukarıdan aşağıya değerlendirmeye göre avantajı, türetme döngülerinin sonsuz bir döngü üretmemesidir . Bunun nedeni, halihazırda onu içeren sonuç kümesine bir sonuç eklemenin hiçbir etkisi olmamasıdır. Örnek olarak, yukarıdaki programa üçüncü bir madde eklemek, yukarıdan aşağıya değerlendirmede bir türetme döngüsü oluşturur:

A(q).
B(X):-A(X).
A(X):-B(X).

Örneğin, hedefe verilen tüm yanıtları değerlendirirken A(X)yukarıdan aşağıya strateji aşağıdaki türevleri üretecektir:

A(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q), A(q)

Başka bir deyişle, önce tek sonuç A(q)üretilir, ancak daha sonra algoritma başka bir cevap üretmeyen türevler üzerinde döngü yapar. Daha genel olarak, yukarıdan aşağıya değerlendirme stratejisi, muhtemelen başka türevler mevcut olduğunda, olası türevler arasında geçiş yapabilir.

Aşağıdan yukarıya strateji aynı dezavantaja sahip değildir, çünkü halihazırda elde edilmiş sonuçların hiçbir etkisi yoktur. Yukarıdaki programda, aşağıdan yukarıya strateji A(q), bir dizi sonuç eklemeye başlar ; ikinci adımda, B(X):-A(X)türetmek için kullanılır B(q); Üçüncü aşamada, mevcut sonuçlar elde edilebilir, yalnızca olgulardır A(q)ve B(q)sonuçların dizi içinde, ancak daha önce olan,. Sonuç olarak, algoritma durur.

Yukarıdaki örnekte, tek kullanılan gerçekler temel bilgilerdi. Genel olarak, yalnızca gövdede kısıtlamalar içeren her madde bir gerçek olarak kabul edilir. Örneğin, bir madde A(X):-X>0,X<10de bir gerçek olarak kabul edilir. Gerçeklerin bu genişletilmiş tanımı için, bazı gerçekler sözdizimsel olarak eşit olmasa da eşdeğer olabilir. Örneğin A(q), eşittir A(X):-X=qve her ikisi de eşittir A(X):-X=Y, Y=q. Bu sorunu çözmek için, gerçekler, kafanın tamamen farklı değişkenlerden oluşan bir demet içerdiği normal bir forma çevrilir; o zaman iki olgu, gövdeleri baş değişkenleri üzerinde eşdeğer ise, yani bu değişkenlerle sınırlandırıldığında çözüm kümeleri aynıysa eşdeğerdir.

Açıklandığı gibi, aşağıdan yukarıya yaklaşımın avantajı, halihazırda elde edilmiş sonuçları dikkate almamadır. Ancak yine de, bunlardan herhangi birine eşit olmamakla birlikte, daha önce türetilenlerin gerektirdiği sonuçlar doğurabilir. Örnek olarak, aşağıdaki programın aşağıdan yukarıya değerlendirmesi sonsuzdur:

A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).

Aşağıdan yukarıya değerlendirme algoritması önce ve A(X)için doğru olanı türetir . İkinci adımda, üçüncü fıkra ile birinci olgu türetilmesine izin verir . Üçüncü adımda, türetilir, vb. Ancak, bu gerçekler, herhangi bir negatif olmayan için doğru olan olgu tarafından zaten gerekli kılınmıştır . Bu dezavantajı kontrol ederek aşılabilir Vasiyetiniz sonuçlarının geçerli kümesine eklenecek olan gerçekler. Yeni sonuç küme tarafından zaten gerekliyse, ona eklenmez. Olgular, muhtemelen "yerel değişkenler" ile yan tümceler olarak depolandığından, onların kafalarının değişkenleri ile sınırlandırılmıştır. X=0X>0A(1)A(2)A(X)X

Eşzamanlı kısıtlama mantığı programlama

Kısıt mantığı programlamanın eşzamanlı sürümleri, kısıtlama tatmin problemlerini çözmek yerine eşzamanlı süreçleri programlamayı amaçlar . Kısıtlı mantık programlamasındaki hedefler eş zamanlı olarak değerlendirilir; bu nedenle eşzamanlı bir süreç, yorumlayıcı tarafından bir hedefin değerlendirilmesi olarak programlanır .

Sözdizimsel olarak, eşzamanlı kısıtlamalar mantık programları, eşzamanlı olmayan programlara benzer, tek istisna, yan tümcelerin, bazı koşullar altında yan tümcenin uygulanabilirliğini engelleyebilecek kısıtlamalar olan korumaları içermesidir . Anlamsal olarak, eşzamanlı kısıtlama mantığı programlaması, eşzamanlı olmayan sürümlerinden farklıdır, çünkü bir hedef değerlendirmesi, bir soruna çözüm bulmaktan ziyade eşzamanlı bir süreci gerçekleştirmeyi amaçlar. En önemlisi, bu fark, birden fazla yan tümce uygulanabilir olduğunda yorumlayıcının nasıl davrandığını etkiler: eşzamanlı olmayan kısıtlama mantık programlaması , tüm yan tümceleri yinelemeli olarak dener; eşzamanlı kısıtlama mantığı programlama yalnızca birini seçer. Bu amaçlanan en belirgin etkisidir yönlülük asla daha önce aldığı bir seçim revize tercüman ait. Bunun diğer etkileri, tüm değerlendirme başarısız olmazken kanıtlanamayan bir hedefe sahip olma semantik olasılığı ve bir hedefi ve bir cümle başını eşitlemenin özel bir yoludur.

Uygulamalar

Kısıtlama mantığı programlama, otomatik zamanlama , tip çıkarımı , inşaat mühendisliği , makine mühendisliği , dijital devre doğrulama, hava trafik kontrolü , finans ve diğerleri gibi bir dizi alana uygulanmıştır .

Tarih

Kısıtlama mantığı programlaması 1987'de Jaffar ve Lassez tarafından tanıtıldı. Prolog II'deki denklemler ve eşitsizlikler teriminin belirli bir kısıtlama biçimi olduğu gözlemini genelleştirdiler ve bu fikri keyfi kısıtlama dillerine genelleştirdiler. Bu konseptin ilk uygulamaları Prolog III , CLP(R) ve CHIP idi .

Ayrıca bakınız

• BProlog
• BNR Prolog (diğer adıyla CLP(BNR))
• ciao
• CLP(R)
• Dağıtılmış Oz Mozart
• ECLiPSe
• GNU Girişi
• SWI-Prolog

Referanslar

• Dechter, Rina (2003). Kısıt işleme . Morgan Kaufmann. ISBN'si 1-55860-890-7. ISBN  1-55860-890-7
• Apt, Krzysztof (2003). Kısıt programlamanın ilkeleri . Cambridge Üniversitesi Yayınları. ISBN'si 0-521-82583-0. ISBN  0-521-82583-0
• Marriott, Kim; Peter J. Stuckey (1998). Kısıtlı programlama: Bir giriş . MİT Basın. ISBN  0-262-13341-5
• Frühwirth, Thom; İnce Abdennadher (2003). Kısıtlı programlamanın temelleri . Springer. ISBN'si 3-540-67623-6. ISBN  3-540-67623-6
• Cafer, Joxan; Michael J. Maher (1994). "Kısıtlama mantığı programlama: bir anket" . Mantık Programlama Dergisi . 19/20: 503-581. doi : 10.1016/0743-1066(94)90033-7 .
• Colmerauer, Alain (1987). "Prolog III Evrenini Açmak". bayt . Ağustos.

Referanslar