Kısıt Programlama ve Kombinatoryal Optimizasyon

Kısıt programlama, uygun çözümleri değişken etki alanları ve mantıksal ilişkilerle tanımlayan bildirime dayalı hesaplama yaklaşımıdır. Kombinatoryal optimizasyon, aynı ayrık çözüm uzayında bir amaç fonksiyonunu en iyi yapan çözümü arar. Yayılım, sistematik arama, global kısıt, SAT, SMT ve CP-SAT mekanizmaları uygulama alanları ve doğruluk sınırlarıyla incelenir.

Ünite 1: Kısıt Sağlama Problemlerinin Matematiksel Temelleri

1.1. Değişkenler, Etki Alanları ve İlişkiler

Kısıt sağlama problemi değişken kümesi, her değişkene ait etki alanı ve izin verilen değer birleşimlerini tanımlayan kısıtlardan oluşur. Çözüm bütün değişkenlere yapılan ve bütün kısıtları sağlayan tam atamadır. Uygunluk problemi ile bir maliyet fonksiyonunu eniyileme problemi aynı türde soru değildir.

1.2. Kısıt Grafları ve Çözüm Uzayı

Kısıt grafında düğümler değişkenleri, kenarlar ortak kısıtları temsil edebilir. Hiperkenarlar ise ikiden fazla değişkene bağlı ilişkilerin doğal gösterimidir. Sonlu etki alanlı modellerde kaba arama uzayı büyüklüğü etki alanı büyüklüklerinin çarpımıdır.

P = (X,D,C);   Sol(P) = {a ∈ ∏[i] Dᵢ : ∀c∈C, c(a)=true}

1.3. Tam Atamaların Doğrulanması

Modelin doğruluğu küçük örneklerde tüm kombinasyonların sayılmasıyla sınanır. Kısıt adı yerine ilişkinin mantıksal anlamı ve değişken alanları açık yazılmalıdır.

1.4. Sayısal ve Algoritmik Örnek

Üç değişkenin her birinde {1,2,3} alanı ve AllDifferent koşulu varsa toplam 27 ham atamadan yalnız 6 sı uygulanabilirdir. Çözüm sayısı 3! tir. Alanların küçülmesi, aynı problemlerin daha az düğümde aranmasını sağlayabilir.

1.5. Kısıt Ağının Matematiksel Gösterimi

Kısıt sağlama problemi değişken kümesi, her değişkenin sonlu veya uygun biçimde tanımlanmış etki alanı ve birlikte sağlanması gereken bağıntılarla tanımlanır. Kısıt grafiğinde değişken düğümleri, bir kısıtta birlikte bulunan değişkenler arasında bağlantı oluşturur; hipergraph gösterimi çok değişkenli kısıtları daha doğrudan korur. Kısıt sağlama, amaç fonksiyonu olmadan uygun atama bulur. Optimizasyon problemi ise ayrıca bir amaç karşılaştırması gerektirir.

CSP = (X,D,C);   Sol(CSP) = {x ∈ D : ∀c∈C, c(x)}

1.6. Kısıt Sağlamada Yerel ve Küresel Bilgi

Tek bir ikili kısıtın sağlanması bütün kısıt ağının uygulanabilir olduğu anlamına gelmez. Örneğin X≠Y, Y≠Z ve X=Z bağıntıları yerel olarak tutarlı olabilir; etki alanları daraltıldığında çelişki ortaya çıkabilir. Kısıt yayılımı değişken etki alanlarından imkânsız değerleri çıkarır ancak genel CSP'lerde uygulanabilirliği tek başına her zaman kararlaştıramaz. Bu nedenle yayılım ve dallanma farklı algoritmik görevlerdir.

1.7. Model Doğrulamada Küçük Örnekler

Küçük etki alanlarında bütün değişken atamalarını tarayan bir referans çözümleyici oluşturulabilir. Bu çözümleyici her kısıtı bağımsız değerlendirerek uzman çözücünün döndürdüğü uygun atamaları karşılaştırır. Kısıt tanımında sıra ve eşitlik yönü yanlış yazıldığında yayılım algoritması hatasız çalışsa bile model yanlış sonucu verebilir. Bu nedenle veri üretimi, model kurulumu ve çözüm değerlendirmesi ayrı test edilmelidir.

1.8. Hesaplamalı Örnek ve Çözüm

X,Y∈{1,2} ve X≠Y kısıtı için yalnız (1,2) ve (2,1) atamaları uygundur. Modeldeki tüm olası dört atama taranarak sonuç kümesi doğrudan doğrulanabilir.

|Sol(P)|=2;   (X,Y)∈{(1,2),(2,1)}

1.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Bağımsız tarama, yanlış yönlü bir kısıt veya değişken indeksleme hatasını ortaya çıkarabilir.

Ünite 2: Değişkenler, Etki Alanları ve Kısıt Modelleme

2.1. Karar Değişkenleri ve Yardımcı Değişkenler

Modelleme aşamasında karar değişkenleri ile türetilmiş değişkenler ayrılmalıdır. Çalışma zamanı açısından gereksiz değişkenler arama uzayını büyütebilir; buna karşılık güçlü kısıtlar için yardımcı değişken eklemek yayılımı kolaylaştırabilir. Kısıt modeli, yalnız denklemler değil alanların ve anlamlarının bütünüdür.

2.2. Global Kısıtlarla Modelleme

Zaman çizelgelemede her işin başlangıç zamanı, süresi ve gereken makine kapasitesi tanımlanır. AllDifferent, NoOverlap ve Cumulative gibi global kısıtlar problemin doğal yapısını ikili kısıtların uzun birleşiminden daha açık ifade eder. Ancak çözücü desteği önceden doğrulanmalıdır.

AllDifferent(x₁,…,xₙ) ⇒ xᵢ ≠ xⱼ   (i ≠ j)

2.3. Model Eşdeğerliği ve Alan Denetimi

Modellerin eşdeğerliği, aynı problem örnekleri üzerinde çözüm kümelerinin karşılaştırılmasıyla test edilir. Daha kısa model yazımının otomatik olarak daha hızlı çözüm anlamına gelmediği göz önünde tutulur.

2.4. Sayısal ve Algoritmik Örnek

Üç işlem tek makineyi paylaşsın ve süreleri 2, 3 ve 1 olsun. Başlama zamanları tamsayıysa NoOverlap kısıtı aralıkların kesişmemesini sağlar. İlk işlemin bitişinden önce ikinci işlem başlayamaz biçimindeki sıralama yalnız ayrıca ilan edilmişse uygulanır.

2.5. Seyrek ve Yoğun Kısıt Gösterimleri

İkili bir kısıt için izinli değer çiftleri tablo olarak, mantıksal bağıntı olarak veya aritmetik eşitsizliklerle gösterilebilir. Yoğun tablo temsili çok büyük etki alanlarında bellek tüketimini artırır; seyrek izinli veya yasaklı değer listeleri uygun problemler için daha ucuz olabilir. Alternatif gösterimlerin hepsi aynı çözüm kümesini üretmelidir. Kodlanmış model ile özgün problem arasındaki eşdeğerlik küçük örneklerde karşılaştırılmalıdır.

Allowed(X,Y) = {(a,b) ∈ D(X)×D(Y) : C(a,b)}

2.6. Reifikasyon ve Koşullu Kısıtlar

Reifikasyonda bir mantıksal değişken bir kısıtın doğruluk değeriyle ilişkilendirilir. Tek yönlü çıkarım ile çift yönlü eşdeğerlik aynı şey değildir: b=1 olduğunda C koşulu zorunlu olabilir fakat C doğruyken b değerinin 1 olması ayrıca istenmeyebilir. Yanlış yönlendirme, seçim ve çizelgeleme modellerinde beklenmeyen uygun çözümler oluşturabilir. Koşullu kısıtların iki doğruluk durumunda da test edilmesi gerekir.

2.7. Etki Alanı Daraltmasının Geri Alınması

Arama sırasında değişken etki alanlarından kaldırılan değerler, geri izleme ile önceki dallanma noktasına döndürülebilmelidir. Tam durum kopyalama basit ama pahalıdır; trail tabanlı tersine çevrilebilir güncelleme veya kalıcı veri yapıları daha ölçeklenebilir olabilir. İptal edilen bir dalın yayılım sonuçları diğer dala sızarsa çözücü geçerli çözümü kaybedebilir. Bu nedenle her dallanma için geri alma değişmezleri test edilmelidir.

2.8. Hesaplamalı Örnek ve Çözüm

b Boole değişkeni ve X tamsayısı için b=1 ⇒ X≤3 koşulu tanımlansın. X=2 ve b=0 bir yönlü çıkarımı ihlal etmez; buna karşılık b⇔(X≤3) eşdeğerliği bu atamayı reddeder.

b ⇒ (X≤3)  ≠  b ⇔ (X≤3)

2.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Model API çağrısının implication mı reification mı kurduğu küçük örneklerle sınanmalıdır.

Ünite 3: Kısıt Yayılımı ve Tutarlılık Algoritmaları

3.1. Yay Tutarlılığı ve Destek Kavramı

Kısıt yayılımı, hiçbir geçerli çözümü atmadan etki alanlarından desteklenmeyen değerleri çıkarır. İkili kısıt için yay tutarlılığı, her değer için karşı tarafta en az bir destek değeri bulunmasını gerektirir. Yay tutarlılığı tüm CSP için çözümün varlığını garanti etmez.

3.2. AC-3 Sabit Nokta Algoritması

AC-3, değişen alanların etkilediği yayları kuyruğa geri koyarak sabit noktaya ilerler. Her alan azaltımından sonra yalnız ilgili komşular tekrar ele alınır. Kuyruk düzeni ve destek arama maliyeti toplam süreyi etkiler.

∀a∈D(X), ∃b∈D(Y) : C[X,Y](a,b)

3.3. Seslilik ve Tamlık Sınırları

Bir değerin silinmesi için ilgili kısıtta destek bulunmadığı test edilmelidir. Kısıt yayılımı sonunda boş alan ortaya çıkması başarısızlığı kanıtlar; boş alan oluşmaması çözüm kanıtı değildir.

3.4. Sayısal ve Algoritmik Örnek

X ve Y alanları {1,2}, ilişki X<Y ise X için 2, Y için 1 değeri desteksizdir. Yay tutarlılığı sonrasında yalnız X=1, Y=2 kalır. Bu örnekte yayılım çözümü bulsa bile genel CSP için arama gerekliliği ortadan kalkmaz.

3.4.1. Açıklayıcı Sözde Kod

queue = all_directed_constraint_arcs()
while queue:
    (x,y) = queue.pop()
    if revise_domain(x, y):
        if empty(domain[x]): return INFEASIBLE
        enqueue_incoming_arcs_except(y, x)
return REDUCED_DOMAINS

3.5. Yay Tutarlılığı ve Destek Kavramı

X→Y yayı için X alanındaki her a değerinin Y alanında kısıtı sağlayan en az bir b desteği bulunmalıdır. Desteği olmayan a kaldırılır; bu değişiklik X ile komşu diğer kısıtların yeniden ele alınmasını gerektirebilir. AC-3 gibi algoritmalar güncelleme kuyruğuna dayanır. Destek saklayan gelişmiş algoritmalar tekrarlı kontrol maliyetini azaltabilir ancak ek veri yapısı ve bellek gerektirir.

∀a∈D(X), ∃b∈D(Y) : C(X=a,Y=b)

3.6. Güçlü Tutarlılık Düzeylerinin Maliyeti

Düğüm, yay ve yol tutarlılığı farklı yerel garanti düzeyleri sağlar. Daha güçlü tutarlılık arama ağacını küçültebilir fakat her düğümdeki yayılım maliyeti artabilir. Genel CSP için tüm tutarlılık seviyelerinin polinom maliyetli olduğu varsayılamaz. Belirli kısıt yapılarında global propagatör, yalnız ikili ayrıştırmadan daha güçlü çıkarım yapabilir. Ölçümde yayılan değer sayısı ve toplam arama düğümü birlikte gösterilmelidir.

3.7. Sabit Nokta ve Yayılım Sonlandırma

Sonlu etki alanlarında yalnız değer çıkaran monoton bir propagatör dizisi, herhangi bir alan boşalmadan veya yeni silme kalmadan sonlanır. Kuyruk yönetimi aynı kısıtı gereksiz tekrar işleyerek maliyeti artırabilir ancak doğru sabit nokta değişmez. Tüm alanlar boş değilken sabit noktaya ulaşılması, tam çözüm bulunduğu anlamına gelmez. Genel durumda dallanma ve yeniden yayılım gereklidir.

3.8. Hesaplamalı Örnek ve Çözüm

X∈{1,2}, Y∈{2} ve X<Y olduğunda X=2 değeri destek bulamaz, dolayısıyla kaldırılır. Kalan alanlar X={1}, Y={2} olur ve model çözülür.

D(X)={1};  D(Y)={2}

3.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Yay tutarlılığının sağlanması her büyük CSP için çözüm garantisi vermediğinden arama testleri ayrıca gereklidir.

Ünite 4: Geri İzleme ve Sistematik Arama Yöntemleri

4.1. Geri İzleme Ağacı ve Değişken Seçimi

Geri izleme araması değişkene bir değer atar, yayılım uygular ve başarısız dallardan geri döner. Minimum remaining values sezgiseli etki alanı küçük değişkenleri önce ele alır; degree sezgiseli kalan değişkenlerle güçlü etkileşimi tercih eder. Bu yöntemler çözüm arama sırasını değiştirir, çözüm kümesini değiştirmez.

4.2. Çatışma Analizi ve Nogood Kaydı

Conflict-directed backjumping ve nogood recording tekrar eden başarısız kombinasyonların önüne geçmeyi hedefler. Kaydedilmiş bir nogood yalnız gerçekten çözümsüz kısmi atamaları dışlamalıdır. Restart stratejileri arama geçmişi korunmazsa aynı alt ağaçların tekrar gezilmesine yol açabilir.

search(P) = propagate(P) → [branch(X=a) ∨ branch(X≠a)]

4.3. Arama Ölçümleri ve Yeniden Üretilebilirlik

Arama ölçütlerinde düğüm sayısı, propagator çağrıları ve çözüm süresi ayrı ölçülür. Heuristiklerin etkisi sabit örnek kümesi, seed ve donanım koşullarında karşılaştırılır.

4.4. Sayısal ve Algoritmik Örnek

Bir değişkenin alanı iki, diğerinin alanı yirmi değer içeriyorsa MRV ilk değişkeni seçebilir. Çatışma oluştuğunda arama geri döner ve geçersiz kombinasyon yeniden denenmez. Rastgele seçimin tek deneyde yavaş kalması genel yöntem üstünlüğü için yeterli kanıt değildir.

4.4.1. Açıklayıcı Sözde Kod

propagate_current_domains()
if contradiction(): return FAILURE
if complete_assignment(): return SOLUTION
x = choose_variable_mrv()
for value in ordered(domain[x]):
    snapshot = save_reversible_state()
    branch(x == value)
    restore(snapshot)

4.5. Arama Ağacı ve Değişken Seçimi

Backtracking, atama değerlerini karar ağacına dönüştürür; her düğümde yeni bilgi yayılarak imkânsız dallar elenir. En küçük kalan etki alanı (MRV) sezgiseli önce en kısıtlı değişkeni seçer. Derece sezgiseli çok sayıda komşu kısıta bağlı değişkenlere öncelik verebilir. Bu sezgisellerin performansı problem ailesine bağlıdır; her örnekte minimum düğüm sayısı garantisi sunmazlar.

T(n) ≈ |D₁|·|D₂|·…·|Dₙ|   (naive enumeration bound)

4.6. İleri Kontrol ve Çatışma Analizi

Forward checking yalnız atanmış değişkenin komşu alanlarını hemen daraltır; tam yay tutarlılığı daha geniş etki yaratabilir. Çatışma ortaya çıktığında hangi kararların bunu zorunlu kıldığı kaydedilebilir. Çatışma yönlendirmeli geri sıçrama, alakasız dallanma seviyelerini atlayabilir; bunun doğruluğu gerekçe ilişkilerinin korunmasına bağlıdır. Yanlış gerekçe çıkarımı, henüz denenmemiş geçerli çözümleri budayabilir.

4.7. Yeniden Başlatma ve Arama Belleği

Yeniden başlatma, arama ağacının başına dönerek farklı karar sırası denemeyi sağlar; bütün öğrenilmiş bilgilerin silinmesi gerekli değildir. Öğrenilen çatışma bilgisi uygun biçimde korunursa önceki başarısız alt uzaylara tekrar girilmez. Her yeniden başlatmanın maliyeti ve çakışma sayısı izlenmelidir. Rastgeleleştirilmiş aramada aynı tohum ve aynı bağlama kuralı sabit sonuçların yeniden üretilmesi için kaydedilir.

4.8. Hesaplamalı Örnek ve Çözüm

A değişkeninin iki, B değişkeninin dört kalmış değeri olsun. MRV kuralı A’yı önce dallandırır. Seçilen A değeri yayıldıktan sonra B alanının yeniden hesaplanması gerekir.

|D(A)|=2<4=|D(B)|

4.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Geri izleme sonrasında her iki etki alanının önceki karar seviyesindeki durumuna tam dönmesi kontrol edilmelidir.

Ünite 5: Global Kısıtlar ve Yayılım Algoritmaları

5.1. Eşleştirme Tabanlı AllDifferent

Global kısıt birçok değişken arasındaki özel yapıyı tek ilişkiyle temsil eder. AllDifferent için ikili eşitsizlik yazımı ile eşleştirme tabanlı global yayılım aynı kuvvette değildir. Cumulative zaman boyunca aynı kaynak üzerindeki toplam tüketimi sınırlayabilir.

5.2. Kümülatif Kaynak Kısıtları

Global propagator, mevcut alanların çözümsüz değerlerini ayıklarken her geçerli tam çözümü korumalıdır. Eşleştirme tabanlı yöntemler Hall türü alt küme koşullarını kullanabilir. Kapasite kısıtlarında zaman aralıklarının çakışması ve enerji muhakemesi farklı filtreleme derecelerine sahiptir.

∑[j : t∈[sⱼ,sⱼ+dⱼ)] rⱼ ≤ C   ∀t

5.3. Filtreleme Kuvveti ve Algoritma Maliyeti

Yayılım kuvveti ile işlem maliyeti dengelenir. Güçlü propagator her örnekte daha hızlı çözüm sağlamayabilir; propagator çalışma süresi ve arama ağacındaki azalma birlikte ölçülür.

5.4. Sayısal ve Algoritmik Örnek

Dört değişken üzerinde AllDifferent, altı ayrı ikili eşitsizlikle de ifade edilebilir. Ancak üç değişkenin yalnız iki değere sıkışması global eşleştirme propagatoründe çelişkiyi daha erken gösterebilir. Aynı sonuç kümesine sahip modeller farklı yayılım gücü gösterebilir.

5.5. AllDifferent ve İki Parçalı Eşleştirme

AllDifferent kısıtı, değişkenlerin birbirinden farklı değer almasını sağlar. İkili eşitsizliklere ayrıştırma doğru çözüm kümesini korusa da global propagatör kadar güçlü alan daraltması üretmeyebilir. Değişken-değer iki parçalı grafında tam eşleştirme bulunamıyorsa kısıt tutarsızdır. Régin türü filtreleme, eşleştirme yapısından yararlanarak hiçbir tam eşleşmede yer alamayan değerleri kaldırabilir.

AllDifferent(x₁,…,xₙ)  ⇒  |{x₁,…,xₙ}| = n

5.6. Cumulative ve Kaynak Zaman Çizelgeleri

Cumulative kısıtı, görev başlangıç zamanları ve sürelerinden doğan eşzamanlı kaynak tüketiminin kapasiteyi aşmamasını ister. Zaman tablosu yayılımı, zorunlu kullanım aralıklarını inceleyerek uygunsuz başlangıç değerlerini çıkarabilir. Enerji gerekçelendirmesi, belirli zaman penceresinde toplam iş yükünün kapasite çarpı pencere uzunluğunu aşamayacağı ilkesini kullanır. Süre sıfır, parçalanabilir işler ve alternatif kaynaklar farklı modelleme semantiği gerektirir.

5.7. Global Kısıtların Yeniden Kullanılabilir Gerçeklemesi

Global propagatör yalnız sonuç üretmez; hangi etki alanının değiştiğini ve hangi kararın geri alınacağını da yönetir. Yeniden çalıştırma koşulları, incremental cache, trail ve gerekçe üretimi genel çözücü mimarisinin parçasıdır. Bir global kısıtın uygulamaya özel kodlanması kısa vadede kolay görünse de kararlılık ve doğrulama maliyetini artırabilir. Bağımsız propagatör testlerinde hem eksik budama hem hatalı budama aranmalıdır.

5.8. Hesaplamalı Örnek ve Çözüm

Üç değişkenin etki alanları {1}, {1,2} ve {2,3} olsun. AllDifferent kısıtı altında tek tam eşleştirme sırasıyla 1,2,3 değerlerini seçer. Global yayılım, ikinci değişkenden 1’i ve üçüncü değişkenden 2’yi kaldırabilir.

(x₁,x₂,x₃)=(1,2,3)

5.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

İki değişkenin aynı değere zorlandığı örnekler uygunsuzluk algılamasını sınar.

Ünite 6: Simetri Kırma ve Hesaplama Karmaşıklığı

6.1. Değer ve Değişken Simetrileri

Bir CSP içindeki simetri, değişken veya değerlerin yer değiştirilmesine rağmen geçerliliğin korunmasıdır. Aynı özdeki birçok çözümün ayrı aranması maliyeti artırır. Simetri kırma kısıtları her eşdeğerlik sınıfından en az bir çözümü korumalıdır.

6.2. Leksikografik Simetri Kırma

Özdeş sunucuların atama modelinde sunucu sütunları permüte edilebilir. İlk kullanılan sunucu kimliğini küçük tutmak gibi leksikografik kurallar simetrik dalları budayabilir. Ancak sunucu maliyetleri farklıysa permütasyon artık geçerli simetri değildir.

σ∈Aut(P) ⇒ [a∈Sol(P) ⇔ σ(a)∈Sol(P)]

6.3. Eşdeğerlik Sınıfları ve Çözüm Korunumu

Simetri kümesinin doğruluğu küçük örneklerde doğrudan kontrol edilir. Bir kısıtın yanlış simetri varsayımıyla eklenmesi, en iyi çözümü kaybettirebilir.

6.4. Sayısal ve Algoritmik Örnek

İki özdeş sunucu varsa bütün işleri A sunucusuna atayan bir çözüm ile bütün işleri B ye atayan çözüm simetrik olabilir. Sunucu A nın maliyeti farklılaştırılırsa bu simetri kaybolur. Sıralama kısıtı eklenmeden önce özdeşlik kontrol edilmelidir.

6.5. Çözüm Simetrileri ve Grup Eylemleri

Bir değişken veya değer permütasyonu, bütün kısıtları ve amaç değerini koruyorsa çözüm uzayında simetri oluşturur. Eşdeğer çözümlerin tek tek aranması büyük tekrara neden olabilir. Simetri kırma, her simetri yörüngesinden en az bir temsilciyi bırakacak biçimde tasarlanmalıdır. Yanlış bir leksikografik sıralama kısıtı, bütün optimum çözüm sınıfını eleyebilir. Simetri olup olmadığı çözümün yalnız görünüşüne göre değil model dönüşümüne göre kanıtlanmalıdır.

σ ∈ Aut(P)  ⇒  [x∈Sol(P) ⇔ σ(x)∈Sol(P)]

6.6. Statik ve Dinamik Simetri Kırma

Statik simetri kırma kısıtları model başında ekler; dinamik yaklaşım arama sırasında simetrik dalları tanıyabilir. Statik kısıtlar fazla kuvvetli veya çok sayıda olduğunda yayılım yükünü artırabilir. Dinamik yöntemlerse izlenen karar sırası ve simetri grubunun temsilini gerektirir. Her iki yaklaşımda küçük örneklerde çözümlerin simetri yörüngelerine ayrıldığı ve her yörüngeden en az bir çözüm kaldığı doğrulanmalıdır.

6.7. Problem Yapısına Göre Karmaşıklık

Genel CSP'nin zor olması, her yapılandırılmış kısıt grafının zor olduğu anlamına gelmez. Ağaç yapılı kısıt ağlarında uygun değişken eleme veya dinamik programlama polinom maliyetli olabilir. Ağaç genişliği yükseldiğinde ara tablolar üstel büyüyebilir. Bu yüzden değişken sayısı kadar etki alanı büyüklüğü, kısıt sıkılığı ve grafiksel yapı da başarım değerlendirmesine dahil edilmelidir.

6.8. Hesaplamalı Örnek ve Çözüm

Özdeş iki kaynak için A ve B görevlerinin hangi kaynakta çalıştığı fiziksel sonucu değiştirmesin. Kaynak etiketlerinin yer değiştirmesi simetrik çözümler üretir; uygun bir sıra kısıtı bu tekrarı azaltabilir.

resource₁ ≤lex resource₂

6.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Kaynakların hızları farklıysa aynı simetri kırma işlemi geçersiz olur; izin verilen dönüşümler doğrulanmalıdır.

Ünite 7: Yumuşak Kısıtlar ve Kısıtlı Optimizasyon

7.1. Sert ve Yumuşak Kısıtların Ayrımı

Sert kısıtlar zorunlu uygulanabilirliği, yumuşak kısıtlar ise tercihleri veya ceza değerlerini ifade eder. Tüm kısıtların sağlanamadığı durumda hangi ihlallerin mümkün olduğu önceden tanımlanmalıdır. Ağırlıklı ceza toplamı farklı öncelikleri tek skora indirger fakat büyük ağırlıklar istenmeyen sayısal etkilere neden olabilir.

7.2. Ağırlıklı ve Leksikografik Amaçlar

Leksikografik optimizasyon önce en yüksek önceliği optimize eder, sonra aynı optimumu koruyarak alt önceliğe geçer. Pareto yaklaşımı tek optimum puan yerine baskın olmayan çözümleri inceler. Bunlar farklı karar kurallarıdır.

min[x∈ℱ] ∑[k=1..m] wₖ·violationₖ(x)

7.3. Ceza Ölçeklemesi ve Pareto Çözümleri

Ağırlıkların duyarlılık analizi yapılır ve sert kısıt ihlali hiçbir ceza fonksiyonu tarafından sessizce kabul edilmez. Farklı amaç normalizasyonları ayrı raporlanır.

7.4. Sayısal ve Algoritmik Örnek

Bir görev için tercih edilen bitiş zamanı ihlal edildiğinde her gecikme birimi 2 puan cezalandırılıyor olsun. Bu yumuşak kısıt, kaynak kapasitesini aşmama sert kısıtıyla karıştırılmamalıdır. Öncelik daha önemliyse amaçlar leksikografik uygulanır.

7.5. Yumuşak Kısıtlar ve İhlal Maliyetleri

Sert kısıtlar çözümün geçerliliğini tanımlar; yumuşak kısıtlar ise ihlal edildiğinde belirli maliyet üretir. İhlal miktarı Boole gösterge, mutlak fark veya kademeli ceza biçiminde modellenebilir. Ağırlıklar gerçek tercihleri ve birimleri temsil etmelidir; keyfî büyüklükte ağırlıklar farklı hedefleri farkında olmadan baskılayabilir. Önemli bir sert kısıtın yalnız yüksek ceza ile değiştirilmesi, ihlal edilemezlik garantisi sağlamaz.

min ∑ₖ wₖ · violationₖ(x)

7.6. Ağırlıklı MaxSAT ve Öncelikli Amaçlar

MaxSAT, Boole formüllerinin sağlanan tümcelerini ençoklamayı amaçlar; ağırlıklı sürümde her yumuşak tümcenin farklı ihlal bedeli olabilir. Birincil ve ikincil amaçlar kesin önceliğe sahipse büyük ağırlık seçmek yerine leksikografik optimizasyon daha güvenilir olabilir. Birinci amacın optimum değeri sabitlenerek ikinci amaç optimize edilir. Bu işlem için amaç değerleri ve toleranslar ayrı kaydedilmelidir.

7.7. Yumuşak Kısıtların Sonuç Açıklaması

Çözücü yalnız toplam ceza değerini vermemeli, hangi yumuşak kısıtların ihlal edildiğini ve her ihlalin maliyet katkısını da gösterebilmelidir. Bir çizelgede gecikmenin kaç birim olduğu, hangi görevde oluştuğu ve bunun hangi sert kapasite kısıtına bağlı olduğu bağımsız doğrulanmalıdır. Bu açıklama, teknik çözümün karar destek sistemiyle bütünleşmesini sağlar fakat optimizasyon algoritmasının doğruluk kanıtının yerine geçmez.

7.8. Hesaplamalı Örnek ve Çözüm

İki yumuşak kısıtın ihlal maliyetleri 3 ve 5 olsun. Sert kısıtlar gereği yalnız biri ihlal edilebiliyorsa toplam cezayı minimize eden çözüm maliyeti 3 olanı ihlal eder.

min penalty ∈ {3,5} = 3

7.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Bu örnekte hangi sert kısıtın çelişkiyi doğurduğu ve başka uygun atamanın bulunup bulunmadığı ayrı doğrulanır.

Ünite 8: Kombinatoryal Optimizasyon Algoritmaları

8.1. Kesin ve Yaklaşık Çözüm Kavramları

Kombinatoryal optimizasyon sonlu fakat çok büyük ayrık çözüm uzaylarında amaç değeri en iyi olan çözümü arar. Bir problem NP-zor olduğunda tüm örneklerin kesin çözümünün polinom zamanda bulunacağı garanti edilemez. Kesin çözüm, yaklaşım garantisi ve deneysel sezgisel başarı birbirinden ayrılmalıdır.

8.2. Yerel Arama ve Komşuluk İşleçleri

Yerel arama bir komşuluk içinde iyileşen çözümler arar; tabu belleği veya yeniden başlatma aramayı farklı bölgelere taşıyabilir. Yaklaşım algoritması ise belirli problem sınıfları için en kötü durum oranı ispatına dayanır. İkisini yalnız ortalama deney sonuçlarına göre eşdeğer saymak yanlıştır.

f(x[alg]) / f(x*) ≥ 1/α;   α ≥ 1;   f(x*) > 0

8.3. Kalite Garantileri ve Deneysel Boşluklar

Küçük örneklerin optimal değeri kesin çözücüyle bulunup sezgisel çözümler için göreli boşluk hesaplanır. Büyük örneklerde yalnız hesaplanmış alt sınırlar veya bilinen referans değerler kullanılır.

8.4. Sayısal ve Algoritmik Örnek

Gezgin satıcı örneğinde yerel arama iki kenarı değiştiren 2-opt komşuluğuyla turu iyileştirebilir, fakat ulaşılan yerel minimumun küresel optimum olduğu kanıtlanmaz. Küçük örneklerde tam enumeration veya kesin çözücü kıyas için kullanılabilir.

8.5. Kesin Algoritmalar ve Yaklaşım Garantileri

Kombinatoryal optimizasyonda kesin yöntem en iyi çözümü kanıtlayabilir veya kanıtlanmış alt/üst sınırlar sağlar. Yaklaşım algoritması ise açık varsayımlar altında bir oran garantisi sunar. Ençoklama ve enazlama problemlerinde oran eşitsizliklerinin yönü farklıdır; sıfır veya negatif amaç değerlerinde oran yorumuna özel dikkat gerekir. Sezgisel yöntemlerin deneysel olarak iyi sonuç vermesi, matematiksel yaklaşım oranı bulunduğu anlamına gelmez.

min problem: cost(alg) ≤ α·cost(opt),  α≥1

8.6. Gevşetme ve Yuvarlama

Tamsayılı değişkenlerin sürekli gevşetmesi daha kolay çözülebilen bir alt problem sağlayabilir. Gevşetme çözümünü bağımsız yuvarlamak kapasite veya tek atama koşullarını bozabilir; bu nedenle yuvarlama algoritmasının uygunluğu ayrıca ispatlanmalıdır. Rassallaştırılmış yuvarlamada beklenen maliyet yanında kısıt ihlali olasılığı hesaplanmalıdır. Derandomizasyon veya onarım yaklaşımı ek maliyet üretebilir ve garantiye dahil edilmelidir.

8.7. Özel Problem Ailelerinin Yapısı

Minimum kapsayan ağaç, en kısa yol, eşleştirme ve maksimum akış gibi belirli problemler polinom zamanda çözülürken genel gezgin satıcı veya küme örtme problemi NP-zordur. Problemlerin benzer çizge gösterimi kullanması hesaplama karmaşıklıklarının aynı olduğunu göstermez. Çözücü seçiminde amaç, kısıtlar, ağırlık işaretleri ve grafik türü dikkate alınmalıdır. Özelleştirilmiş algoritma kullanımı için modelin o problem ailesine tam uyduğu kanıtlanmalıdır.

8.8. Hesaplamalı Örnek ve Çözüm

Kapsanacak evren {a,b,c}, iki küme {a,b} ve {b,c} olsun. Bütün evreni kapsamak için iki kümenin de seçilmesi gerekir; optimum küme sayısı 2’dir.

minimum set cover size = 2

8.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Aynı örnek karma tamsayılı model, tam tarama ve greedy yaklaşımla karşılaştırılarak çözüm kalitesinin anlamı açıklanır.

Ünite 9: Boole Sağlanabilirlik ve SAT Çözücüleri

9.1. CNF ve Literaller

SAT problemi bir Boole formülünü doğru yapan atama olup olmadığını sorar. CNF biçiminde formül, maddelerin ve değişken/olumsuz değişkenlerden oluşan literal birleşimlerinin konjonksiyonudur. Genel SAT NP-tamdır; Horn-SAT ve 2-SAT gibi sınıflar özel algoritmalarla polinom zamanda çözülebilir.

9.2. CDCL ve Birim Yayılımı

CDCL çözücüleri birim yayılımı, karar atamaları, çatışma çözümlemesi ve öğrenilmiş madde eklemesiyle çalışır. İki izlemeli literal tekniği yayılım maliyetini azaltır. Öğrenilmiş madde ancak orijinal formülden mantıksal olarak çıkarılabiliyorsa güvenlidir.

F = ⋀[j=1..m] (⋁[ℓ∈Cⱼ] ℓ)

9.3. SAT/UNSAT Çıktılarının Doğrulanması

SAT ve UNSAT sonuçları farklı doğrulama gerektirir: SAT ataması formüle uygulanabilir, UNSAT iddiası uygun ispat günlüğüyle doğrulanabilir. Zaman sınırı dolması UNSAT değildir.

9.4. Sayısal ve Algoritmik Örnek

(a∨b)∧(¬a∨c) CNF formülünde a=0, b=1, c=0 ataması iki maddeyi de sağlar. Bir SAT çözücünün “SAT” yanıtı bu tür doğrudan değerlendirmeyle kontrol edilir. “UNSAT” için tek bir başarısız arama dalı yeterli değildir.

9.5. CNF ve Tseitin Dönüşümü

SAT çözücüleri önermesel mantık ifadelerini genellikle konjonktif normal biçimde işler. Doğrudan dağıtma kuralları formülü üstel büyütebilir; Tseitin dönüşümü yardımcı Boole değişkenleri ekleyerek uygunluk bakımından eşdeğer ve doğrusal boyutlu bir CNF üretir. Yeni değişkenlerin anlamı saklanmalıdır, çünkü çözücü atamasının özgün problem değişkenlerine geri çevrilmesi gerekir. Eşdeğerlik ile yalnız eş-uygunluk arasındaki ayrım doğrulamada önemlidir.

F = C₁ ∧ C₂ ∧ … ∧ Cₘ;   Cⱼ = ℓ₁ ∨ … ∨ ℓₖ

9.6. CDCL, Öğrenilmiş Tümceler ve Geri Sıçrama

Conflict-driven clause learning, Boole kısıt yayılımı ve karar seviyeleri üzerinden çelişkiyi analiz eder. Bir çatışmadan öğrenilen tümce önceki kararların birlikte tekrarlanmasını engelleyebilir. İlk benzersiz sonuç noktası (first UIP), yaygın bir öğrenme şemasıdır; öğrenilen tümcenin özgün formülle mantıksal olarak gerektirildiği korunmalıdır. Öğrenilen tümcelerin sınırsız birikmesi bellek maliyetini artırdığı için silme politikaları kullanılır.

9.7. İki İzlemeli Literal ve Birim Yayılım

İki izlemeli literal, bir tümcedeki her değişken atamasında tüm literal listesini taramadan birim yayılım yapmayı amaçlar. İzlenen literal yanlış olduğunda başka uygun literal aranır; bulunamazsa birim koşul veya çatışma belirlenir. İşaret ve karar seviyesi yanlış takip edilirse çözücü yanlış UNSAT sonucuna ulaşabilir. Küçük rastgele formüllerde brute-force çözücüyle sonuç karşılaştırması yapılmalıdır.

9.8. Hesaplamalı Örnek ve Çözüm

(a∨b)∧(¬a∨c) formülü için a=1, b=0, c=1 ataması iki tümceyi de sağlar. a=1, c=0 durumunda ikinci tümce yanlış olur.

F=(a∨b)∧(¬a∨c);   F(1,0,1)=true

9.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

CNF kodlamasından sonra özgün değişkenlerin ataması değerlendirilerek doğrulama yapılır.

Ünite 10: SMT ve CP-SAT Çözücü Mimarileri

10.1. Boole Mantığı ve Teori Çözücüleri

SMT, Boole yapısına ek olarak doğrusal aritmetik, bit-vektör veya dizi gibi teorilere ilişkin kısıtları ele alır. SMT çözücüsü, mantıksal kararlarla teori tutarlılığını birlikte yönetir. CP-SAT ise tamsayılı ve Boole kısıtların güçlü yayılım ve arama mekanizmalarıyla çözülmesine yönelik farklı bir mimaridir.

10.2. Modelleme Dilleri ve Tamsayılı Ölçekleme

SMT-LIB mantıksal formüller için bir değişim dili sağlar; MiniZinc modelleri ise uygun arka uç çözücülere derlenebilir. OR-Tools CP-SAT modelinde değişken aralıkları ve aritmetik katsayılar tamsayı mantığına uygun ölçeklenmelidir. Bu araçların kabul ettiği model sınıfları aynı değildir.

SMT: SAT + kuram tutarlılığı denetimleri;   CP-SAT ≠ SMT

10.3. Çözücü Sınıfları ve Karşılaştırma Ölçütleri

Çözücüler aynı test problemini destekliyorsa bulunan atamalar özgün modele göre bağımsız doğrulanır. Bir aracın bilinmeyen/timeout sonucu başka aracın yanlış olduğu anlamına gelmez.

10.4. Sayısal ve Algoritmik Örnek

(x−y=3)∧(x≥0)∧(y≥0) tamsayı aritmetiğinde SMT tarafından ele alınabilir. CP-SAT için sınırlı aralıklarla tamsayı değişkenler kullanılabilir. Gerçek sayı ile rasyonel/tamsayı semantiğini karıştıran bir çeviri model eşdeğerliğini bozabilir.

10.5. DPLL(T) ve Kuram Çözücülerinin İş Bölümü

SMT, Boole yapısı ile doğrusal aritmetik, bit-vektör veya dizi gibi seçilmiş kuramların tutarlılık denetimini birleştirir. DPLL(T) mimarisinde SAT katmanı aday Boole ataması üretirken kuram çözücüsü bu atamanın anlam bakımından tutarlı olup olmadığını kontrol eder. Kuram tutarsızlığı açıklayıcı tümceyle SAT katmanına geri bildirilebilir. Her kuramın karar verilebilirlik ve karmaşıklık özellikleri farklıdır; keyfî program davranışının tamamı çözülebilir varsayılamaz.

SMT = Boolean search + theory consistency;   SAT ≠ SMT

10.6. CP-SAT ve Tamsayılı Kısıtların Kodlanması

CP-SAT, SAT tabanlı öğrenme ve arama tekniklerini tamsayılı değişkenler, çizelgeleme kısıtları ve optimizasyon ile birleştirir. Genel SMT çözücüyle eş anlamlı değildir; desteklediği veri türleri ve aritmetik işlemler çözücüye özgüdür. Örneğin gerçek sayılı değişkenin tam hassasiyetle doğrudan desteklendiği varsayılamaz; rasyonel katsayılar gerekirse güvenli ölçeklenir. Ölçekleme, taşma sınırları ve tam sayılı aritmetik kontrolü model doğruluğunun parçasıdır.

10.7. Çözücü API Sınırlarında Doğrulama

Bir kısıt çözücü kütüphanesine veri aktarılırken indeksler, işaretli tamsayı aralığı ve model nesnelerinin yaşam döngüsü korunmalıdır. Çözücü “UNKNOWN” veya zaman sınırı döndürdüğünde kesin UNSAT sonucu ilan edilmez. Çözüm bulunduğunda tüm özgün kısıtlar bağımsız değerlendirilir. Farklı çözücülerde aynı model ailesini test etmek dönüşüm hatalarını yakalayabilir; aynı sonucu vermemeleri tek başına hangisinin hatalı olduğunu belirlemez.

10.8. Hesaplamalı Örnek ve Çözüm

x−y=3, x≥0 ve y≥0 kuram kısıtları için x=3, y=0 geçerli bir atamadır. Yalnız Boole iskeletinin SAT olması bu aritmetik kısıtların birlikte uygun olduğunu garanti etmez.

(x,y)=(3,0)  ⇒  x−y=3

10.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Kuram çözücüsü çelişki bildirdiğinde oluşturduğu açıklayıcı tümce, mevcut aritmetik varsayımlardan türetilmiş olmalıdır.

Ünite 11: Çizelgeleme, Atama ve Rota Optimizasyonu

11.1. Öncelik İlişkileri ve Zaman Değişkenleri

Çizelgeleme problemlerinde öncelik ilişkileri, başlangıç süreleri ve kaynak kapasitesi birlikte modellenir. İş süresi ile bekleme süresi farklı niceliklerdir. NoOverlap tek kaynakta çakışmayı, Cumulative kapasite kullanan eşzamanlı işleri sınırlamayı ifade eder.

11.2. Kaynak Kısıtları ve Rota Modelleri

Atama problemlerinde ikili değişkenler kaynak-iş bağlantısını belirtir. Rota problemlerinde kapasite ve ziyaret kısıtları yanında alt turların önlenmesi gerekir. Bir çözümün her düğümü ziyaret etmesi tek bir bağlı tur oluşturduğunu otomatik olarak göstermez.

sⱼ ≥ sᵢ + dᵢ   (i ≺ j);   ∑[i] rᵢ(t) ≤ C

11.3. Bağlantısallık ve Çizelge Denetimi

İş programları için öncelik kısıtı, rota çözümleri için bağlantısallık ve kapasite, atamalar için tekillik kontrol edilir. Süre ölçümleri aynı problemi çözen algoritmaları karşılaştıracak biçimde yapılır.

11.4. Sayısal ve Algoritmik Örnek

Üç işin süreleri 2, 3 ve 4 olsun. A≺C önceliği, C başlangıcının A tamamlanmasından önce olmamasını gerektirir. Çözümde kaynak çakışmaması sağlansa bile bu öncelik ihlal edilebileceğinden her kısıt sınıfı ayrı doğrulanır.

11.5. Öncelik Çizgeleri ve Kritik Yol

Bir çizelgeleme probleminde görevler düğüm, zorunlu bitiş-başlangıç ilişkileri yönlü kenardır. Öncelik grafı döngüsüz olmalıdır; pozitif süreli çevrim uygulanamazlık doğurur. Kritik yol yöntemi kaynak kapasitesi sonsuz sayıldığında önceliklerden gelen alt sınırı verir. Kaynak kısıtları eklendiğinde bu alt sınır tek başına optimum tamamlanma zamanını belirlemez; kaynak çatışmaları ayrıca modellenir.

startⱼ ≥ startᵢ + durationᵢ  (i ≺ j)

11.6. Alternatif Kaynaklar ve Kesintisiz Görevler

Bir görevin birden fazla makinede çalışabilmesi, seçilen makineye bağlı süre ve maliyet doğurabilir. Tek seferde tamamlanması gereken görevlerde preemption yasaktır; parçalanabilir görevler için farklı model gerekir. Başlangıç zamanlarını ayrıklaştırmak model boyutunu büyütür, zaman aralığı değişkenleri ve özel propagatörler daha etkili olabilir. Kaynak takvimi, tatil ve bakım pencereleri uygunluk denetimine dâhil edilmelidir.

11.7. Rota Kısıtları ve Alt Tur Engelleme

Araç rotalama ve gezgin satıcı problemlerinde her noktaya giriş-çıkış derecesi kısıtları yalnız ayrık çevrimler üretebilir. Tek rota elde etmek için alt tur engelleme, akış tabanlı bağlantılılık veya uygun kesmeler gerekir. Kapasite ve zaman pencereleri rota sırasına bağımlıdır. Testlerde yalnız toplam mesafe değil tüm noktaların tam ziyaret edilmesi, rota bağlantılılığı, zaman aralığı ve yük kapasitesi doğrulanmalıdır.

11.8. Hesaplamalı Örnek ve Çözüm

A görevi 2 birim, B görevi 3 birim sürsün ve B, A bittikten sonra başlayabilsin. Başka kaynak kısıtı yoksa en erken bitiş zamanı 5’tir.

startᴮ ≥ startᴬ+2;  finishᴮ ≥ 5

11.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Yeni kaynak takvimi veya bakım aralığı eklendiğinde bu alt sınırın hâlâ geçerli fakat optimumun değişebilir olduğu gözlenmelidir.

Ünite 12: Çözücü Gerçeklemesi, Doğruluk ve Başarım Analizi

12.1. Çözücü Yaşam Döngüsü ve Geri Alma

Çözücü uygulaması ayrıştırma, model normalleştirme, yayılım, arama ve sonuç doğrulama aşamalarını birbirinden ayırmalıdır. Geri dönüşlü veri yapıları, her dalda etki alanı değişimlerini doğru geri almalıdır. Bellek sızıntısı veya bozuk undo işlemi doğrudan yanlış çözüm üretir.

12.2. Metamorfik Testler ve Bağımsız Doğrulama

Doğruluk testleri kapsamlı küçük örnekler, rastgele üretilmiş örnekler, metamorfik dönüşümler ve bağımsız çözücü karşılaştırmalarını içerir. Simetrik yeniden adlandırma gibi dönüşümlerde çözüm varlığı korunmalıdır. UNSAT iddialarında uygun ispat veya ikinci bağımsız denetçi gerekir.

valid(x) = ⋀[c∈C] c(x);   gap = |z[inc]−z[bound]| / max(1, |z[inc]|)

12.3. Başarım ve Optimalite Ölçümleri

Başarım ölçümünde düğüm sayısı, propagator süresi, bellek tepe değeri, en iyi sınır ve süre sınırı birlikte raporlanır. Farklı seed ve örnek dağılımları olmadan tek bir süre değeri genelleştirilmez.

12.4. Sayısal ve Algoritmik Örnek

İki simetrik değişkenin isimlerini değiştiren modelin SAT/UNSAT sonucu aynı kalmalıdır. Böyle bir metamorfik test farklı sonuç verirse modelleme, parser veya geri alma mekanizmasında hata olabilir. Her testte ham model ve çözücü günlüğü korunur.

12.4.1. Açıklayıcı Sözde Kod

parse_and_normalize(model)
candidate = search_with_propagation(model)
if candidate: assert check_all_constraints(model, candidate)
if solver_claims_unsat: verify_proof_or_independent_solver()
record_nodes_time_memory_limits()

12.5. UNSAT ve OPTIMAL Kanıtlarının Ayrılması

Uygun çözüm için bütün kısıtların doğrudan değerlendirilmesi yeterli olabilir; uygulanamazlığın kanıtı ise çözümün bulunamamasından daha güçlü delil gerektirir. SAT dünyasında çözümün doğru atama olması kolay kontrol edilirken UNSAT için çözümleyicinin ürettiği kanıt izi ve bağımsız doğrulayıcı kullanılabilir. Optimizasyonda da yalnız iyi bir aday değil, adaydan daha iyi çözüm bulunamayacağına dair sınır gerekir. Farklı sonuç durumları açık sınıflandırılmalıdır.

verified OPTIMAL ⇒ feasible candidate ∧ valid bound ∧ closed gap

12.6. Özellik Tabanlı ve Diferansiyel Testler

Kısıt çözümleyicilerinin testleri rastgele geçerli modellerin yanında kasıtlı çelişki, boş alan, tek değer ve sınır durumlarını içermelidir. Bir değişkene yeni kısıt eklenmesi çözüm kümesini büyütemez; bu monotonluk uygunluk testinde kullanılabilir. Aynı modelin iki ayrı kodlaması eş-uygun değilse dönüştürme hatası olabilir. Hatalı bir UNSAT sonucu, gerekli bir çözümün kalıcı biçimde kaybedilmesine neden olduğu için özellikle kritik kabul edilir.

12.7. Kapsamlı Deney Tasarımı ve Sınırlar

Arama düğümü, çatışma, propagasyon, bellek, wall-clock süre ve zaman aşımı oranı birlikte ölçülmelidir. Problem örneklerinin yalnız kolay veya çözücünün tanıdığı kalıplardan seçilmesi karşılaştırmayı çarpıtır. Donanım, iş parçacığı sayısı, rastgele tohum ve varsayılan parametre sürümleri sabitlenmelidir. Bir problemi “UNKNOWN” sonucuyla bırakmak bilimsel olarak geçerli raporlamadır; bu sonucun ne SAT ne de UNSAT olduğu açıkça belirtilmelidir.

12.8. Hesaplamalı Örnek ve Çözüm

Etki alanı boş olan zorunlu bir değişken içeren CSP doğrudan uygunsuzdur. Ancak çözücünün bilinmeyen durum döndürmesi veya aramanın zaman aşımına uğraması bu matematiksel kanıtla aynı değildir.

D(X)=∅  ⇒  Sol(P)=∅

12.9. Bağımsız Doğrulama ve Gerçekleme Sınırları

Kanıt raporunda uygulanamazlığın açık gerekçesi ile gözlemsel arama başarısızlığı kesin biçimde ayrılmalıdır.

Kaynakça

• Google OR-Tools. CP-SAT Solver Documentation. https://developers.google.com/optimization/cp/cp_solver
• Korte, Bernhard; Vygen, Jens. Combinatorial Optimization: Theory and Algorithms. 6th ed. Springer, 2018.
• Microsoft Research. The Z3 Guide. https://microsoft.github.io/z3guide/
• MiniZinc. MiniZinc Handbook. https://docs.minizinc.org/en/stable/
• Rossi, Francesca; van Beek, Peter; Walsh, Toby (eds.). Handbook of Constraint Programming. Elsevier, 2006. ISBN 9780444527264.