SAT Teknolojisi Kullanarak Minimal Perfect Hash Fonksiyonlarının Oluşturulması

Sean A. Weaver
Laboratory for Advanced Cybersecurity Research
U.S. National Security Agency
saweave@evoforge.org

Marijn J.H. Heule
Computer Science Department
Carnegie Mellon University
marijn@cmu.edu
Amazon Scholar

Minimal perfect hash fonksiyonları (MPHF), büyük sözlüklerin (anahtar-değer çiftlerinden oluşan kümelerin) değerlerine verimli erişim sağlamak için kullanılır. MPHF oluşturmak için yeni algoritmalar geliştirmek, özellikle depolama verimliliği açısından, aktif bir araştırma alanıdır. MPHF'ler için bilgi-kuramsal sınır şudur:

1 / ln 2 ≈ 1.44 bit anahtar başına.

Günümüzdeki en iyi pratik algoritmalar anahtar başına 2 ile 4 bit arasında değişmektedir. Bu makalede, MPHF oluşturmak için SAT tabanlı iki yöntem öneriyoruz. İlk yöntemimiz bilgi-kuramsal sınıra yakın MPHF'ler üretir. Bu yaklaşım için, mevcut en gelişmiş SAT çözücüleri sözlüklerin 40 öğeye kadar eleman içerdiği örnekleri işleyebilmektedir; böylece mevcut (brute-force) yöntemlerden daha iyi performans göstermektedir. İkinci yöntemimiz ise yaklaşık olarak anahtar başına 1.83 bitlik uzun dönemli depolama sağlayan pratik bir yaklaşımı gerçekleştirmek için XOR-SAT filtrelerini kullanır.

Introduction

Bir küme Y içinde n farklı eleman bulunduğunda, bu küme için minimal perfect hash fonksiyonu (MPHF), Y kümesindeki elemanları [n] = {1, ..., n} kümesine çakışmasız biçimde eşleyen bir fonksiyondur. MPHF'ler, anahtar-değer çiftlerinden oluşan bir kümede her anahtar için benzersiz bir indeks sağlayarak büyük veritabanlarında saklanan verilere verimli erişim sağlar. Bu sayede her anahtar-değer çiftinin değeri, n girişli bir tabloda kendisine karşılık gelen indeks konumunda saklanabilir. Endüstriyel veritabanları genellikle oldukça büyük olduğundan, bir MPHF kullanılacaksa mümkün olduğunca az ek alan kullanması tercih edilir.

MPHF'ler için bilgi-kuramsal sınır şu şekildedir:

1 / ln 2 ≈ 1.44 bit anahtar başına (Mehlhorn 1982; Fredman and Komlós 1984),

ancak bu sınıra ulaşan pratik yöntemler (brute force yöntemlerine dayanmayanlar) henüz bulunmamıştır. Günümüzdeki en iyi algoritmalar anahtar başına 2 ile 4 bit arasında değişmektedir (Belazzougui, Botelho, and Dietzfelbinger 2009; Botelho, Pagh, and Ziviani 2013; Genuzio, Ottaviano, and Vigna 2016; Limasset et al. 2017). Uygulamalar oluşturma süresi ve sorgu süresi gibi maliyetleri de dikkate alabileceğinden, MPHF oluşturma ve sorgulama maliyetleri kompakt bir gösterimin sağladığı faydayı aşacak kadar yüksek olmamalıdır.

Statik MPHF'ler için iki yeni yöntem sunuyoruz: yani Y kümesinin değişmez olduğu ve önceden bilindiği MPHF'ler. Her iki yöntem de tatmin edilebilirlik (SAT) tekniklerine dayanır ve evrensel bir hash fonksiyonları ailesi kullanır.

Information-Theoretic Limit

Tablo 1. Farklı anahtar sayıları (n) için anahtar başına bit cinsinden bilgi-kuramsal sınır (αₙ).

İlk yöntemimiz MPHF oluşturma problemini bir Boolean formül olarak kodlar ve bunu çözmek için bir SAT çözücüsü kullanır. Amaç, bilgi-kuramsal sınıra yakın MPHF'ler elde etmektir (büyük kümeler için yaklaşık olarak anahtar başına 1.44 bit; örneğin birkaç bin anahtardan fazla içeren kümeler). Bu fonksiyonlar log₂ n adımda sorgulanabilir. Daha küçük n değerleri için bilgi-kuramsal sınır αₙ, Tablo 1'de gösterilmiştir.

Kompakt bir O(n² log² n) SAT kodlaması ve daha etkili bir O(n³) kodlama sunuyoruz. Bu kodlamalar üzerinde, güncel SAT çözücüleri (hem tam hem de eksik yaklaşımlar) sözlükteki eleman sayısına göre üstel çalışma süresi göstermektedir; çalışma süreleri yaklaşık 40 eleman civarında aşırı büyüyerek büyük kümeler için yöntemimizi şu anda pratik olmaktan çıkarmaktadır. Bununla birlikte, bildiğimiz kadarıyla mevcut başka hiçbir yöntem (brute force dahil) 20'den fazla eleman içeren kümeler için bilgi-kuramsal sınıra yakın MPHF'leri makul sürede oluşturamamaktadır.

Yalnızca tatmin edilebilir formüllerle (MPHF'nin varlığı) ilgilendiğimiz için, yerel arama teknolojisine dayanan SAT yaklaşımları doğal bir seçenek gibi görünmektedir. Şu anda tam çözüm yöntemleri kodlamalarımız üzerinde daha iyi performans göstermektedir. Bununla birlikte, yöntemimiz güçlü bir rastgelelik özelliğine sahip formüller meydana getirir ve uniform rastgele k-SAT örnekleri için yerel arama tekniklerinde büyük ilerlemeler kaydedilmiştir (Kautz and Selman 1996; Balint and Schöning 2012; Gableske 2014).

İkinci yöntemimiz anahtar başına yaklaşık 1.83 bit kullanır ve O(n³) adımda MPHF oluşturabilir (oluşturma işlemi kolayca paralelleştirilebilir). Bu MPHF'ler en kötü durumda max(3, ln n + ln(ln n)) adımda sorgulanabilir. Biçimsel olarak, bu yöntem ağırlıklı iki parçalı bir grafın minimum ağırlıklı perfect matching sonucunu, XORSAT filter adı verilen alan verimli bir erişim yapısında saklamayı içerir (Weaver, Roberts, and Smith 2018). Uygulanan prototipimiz, yaklaşımın büyük veri kümeleri (2³⁰ anahtar) için MPHF üretebildiğini ve düşük maliyetle yüksek sorgu hızları (saniyede yaklaşık bir milyon sorgu) sağlayabildiğini göstermektedir.

arXiv:1911.10099v1 [cs.LO] 22 Nov 2019

Abstract

Preliminaries

Aşağıda bu makalenin katkılarıyla ilgili en önemli arka plan kavramlarını sunuyoruz.

Minimal Perfect Hash Functions

n farklı eleman içeren bir Y kümesi için minimal perfect hash fonksiyonu (MPHF), Y kümesindeki elemanları ([n] = {1, ..., n}) kümesine eşleyen bire bir ve örten bir eşlemedir. MPHF oluşturulurken üç önemli denge unsuru rol oynar: depolama alanı, sorgu hızı ve oluşturma maliyeti. Araştırmaların çoğu, kabul edilebilir sorgu hızı ve oluşturma maliyeti korunurken depolama alanını azaltmaya odaklanır.

Aralığı ([n]) olan evrensel bir H fonksiyonunun Y için minimal perfect hash fonksiyonu olma olasılığı (n! / n^n)'dir. i ∈ [n] için her bir y_i elemanı açısından, ((j < i)) olmak üzere (H(y_i)) ve (H(y_j))'nin çakışmama olasılığı ((n + 1 − i) / n)'dir.

Bilgi-kuramsal sınır (α_n), eleman başına (\log_2(n^n / n!) / n) bittir. Bu sınır büyük n için yaklaşık eleman başına 1.44 bit değerindedir, ancak küçük n için daha küçüktür. Tablo 1, n değerinin çeşitli durumları için bu sınırı göstermektedir.

Bu sınıra ulaşabilen mevcut tek MPHF yöntemleri brute-force tabanlıdır: birçok hash fonksiyonunu Y üzerinde değerlendirir ve minimal perfect hash fonksiyonu bulunduğu anda sonlandırır. Böyle bir hash fonksiyonunun gösterimi ortalama olarak eleman başına (α_n) bit gerektirdiğinden, örneğin 20 elemanlı bir küme üzerinde brute-force yöntemi ortalama olarak 43 milyonun (2^25.36) üzerinde hash fonksiyonunun değerlendirilmesini gerektirir.

Propositional Logic and Satisfiability

Önerme formüllerini konjonktif normal formda ele alıyoruz ve bunlar aşağıdaki şekilde tanımlanır.

Bir literal, ya bir değişken x (pozitif literal) ya da bir x değişkeninin değillemesi (¬x) (negatif literal) şeklindedir. Bir l literali için, l'nin değişkenini var(l) ile gösteririz.

Bir l literalinin tamamlayıcı literali (\bar{l}) şu şekilde tanımlanır:

• (\bar{l} = ¬x) eğer (l = x)
• (\bar{l} = x) eğer (l = ¬x)

Bir clause, şu biçimde sonlu bir ayrışım (disjunction) ifadesidir:

(l₁ ∨ ... ∨ lₖ)

burada l₁, ..., lₖ literallerdir.

Bir formula, şu biçimde sonlu bir bağlaç (conjunction) ifadesidir:

C₁ ∧ ... ∧ Cₘ

burada C₁, ..., Cₘ clause'lardır.

Bir XOR kısıtı, şu biçimde bir ifadedir:

l₁ ⊕ ... ⊕ lₖ ≡ b

burada l₁, ..., lₖ literallerdir ve b ∈ {0,1}.

Bir assignment, bir değişken kümesinden doğruluk değerlerine 1 (doğru) ve 0 (yanlış) eşleme yapan bir fonksiyondur.

Bir l literali, bir α ataması tarafından şu durumlarda sağlanır:

• l pozitif ise ve (α(var(l)) = 1), veya
• l negatif ise ve (α(var(l)) = 0).

Bir literal, tamamlayıcısı atama tarafından sağlanıyorsa atama tarafından yanlışlanmış kabul edilir.

Bir l literali için bazen şu gösterimleri kullanırız:

• α, l literalini sağlıyorsa (α(l) = 1)
• α, l literalini yanlışlıyorsa (α(l) = 0)

Bir clause, içinde α tarafından sağlanan bir literal bulunduğunda α ataması tarafından sağlanmış olur. Bir formula, tüm clause'ları α tarafından sağlandığında sağlanmış kabul edilir. Bir formula, onu sağlayan bir atama varsa satisfiable, aksi halde unsatisfiable olarak adlandırılır.

Bir XOR kısıtı

l₁ ⊕ ... ⊕ lₖ ≡ b

şu durumda bir α ataması tarafından sağlanır:

α(l₁) + ... + α(lₖ) ≡ b (mod 2)

XORSAT Filters

Bir XORSAT filter, bir elemanın bir kümede bulunup bulunmadığını test etmek için kullanılan alan verimli olasılıksal bir veri yapısıdır. Bu makalenin bağlamında, XORSAT filtreleri tek bitlik öğeler içeren sözlükler olarak ele alınır.

Bir XORSAT filter, n bit ve aralığı ([n]) olan k adet hash fonksiyonundan oluşur.

Bir elemana karşılık gelen saklı biti elde etmek için k hash fonksiyonu bu eleman üzerinde değerlendirilir. Bunun sonucu olarak dizide k giriş elde edilir. Eğer değeri 1 olan girişlerin sayısı çift ise saklanan bit 0, aksi halde saklanan bit 1 olur.

XORSAT filtreleri şu şekilde oluşturulur:

Öncelikle kümedeki n elemanın her biri için uzunluğu k olan bir XOR kısıtı üretilir ve her kısıtın sağ tarafı saklanacak karşılık gelen bite eşit yapılır. Bunun ardından, bu XOR kısıtlarının bağlacının bir çözümü hesaplanarak XORSAT filter oluşturulur.

A Space-Optimal MPHF Construction

Öncelikle SAT çözme tekniklerinin alan açısından optimal (anahtar başına αₙ bit) MPHF'ler oluşturma yeteneğini inceliyoruz.

Aşağıdaki kümenin verildiğini varsayıyoruz:

Y = {y₁, ..., yₙ}

(hashlenecek elemanlar) ve bir m tamsayısı (MPHF'yi saklamak için kullanılan bit sayısı).

Açıktır ki Y kümesinin elemanları şu uzunlukta bit-vektörlerle temsil edilebilir:

k = ⌈log₂(n)⌉.

Yöntemlerimiz için, tanım kümesi Y ve değer aralığı

{−m, ..., m} \ {0}

olan k adet evrensel hash fonksiyonundan oluşan bir aile kullanıyoruz:

H₁, ..., Hₖ

Bir yⱼ elemanı için, Lᵢ(yⱼ) ile şu literal ifade edilir:

• (x_{H_i(y_j)}) eğer (H_i(y_j) > 0)
• (x_{−H_i(y_j)}) aksi halde.

MPHF bulma problemini önerme mantığına kodlamak için önce m adet farklı Boolean değişkeni tanıtıyoruz:

x₁, ..., xₘ.

Daha sonra, formülün bir α tatmin edici atamasından her yᵢ elemanının indeksinin (hash değerinin) türetilebilmesini sağlayacak bir önerme formülü tanımlarız. Özellikle, x₁, ..., xₘ değişkenlerine atanan doğruluk değerlerinden yararlanılır.

yᵢ için indeks şu bit-vektördür:

α(L₁(yⱼ)) ... α(Lₖ(yⱼ)).

Örnek:

m = 3, j = 1 olsun ve

• H₁(y₁) = 3
• H₂(y₁) = −1
• H₃(y₁) = 2

olduğunu varsayalım.

Bu durumda y₁'in indeksi şu değişkenlere atanan doğruluk değerleriyle belirlenir:

• L₁(y₁) = x₃
• L₂(y₁) = ¬x₁
• L₃(y₁) = x₂

Dolayısıyla eğer

• α(x₁) = 1
• α(x₂) = 0
• α(x₃) = 1

ise y₁ şu indekse eşlenir:

α(x₃) α(¬x₁) α(x₂) = ⟨100⟩ = 5

(⟨100⟩ ifadesinin 4 yerine 5 sayısını temsil ettiğine dikkat edin; çünkü indeksler 0 yerine 1'den başlar).

Her elemanın eşlemesinin k farklı değişkene bağlı olmasını sağlamak için, her hash fonksiyonunun farklı bir değişken döndürmesi zorunlu tutulur; çakışma durumunda hash fonksiyonu tekrar uygulanır.

Bir MPHF elde etmek için, önerme formülünün bir α ataması tarafından sağlanması ancak ve ancak farklı iki eleman yᵢ ve yⱼ için şu koşulun geçerli olması durumunda mümkün olmalıdır:

α(L₁(yᵢ)) ... α(Lₖ(yᵢ)) ≠ α(L₁(yⱼ)) ... α(Lₖ(yⱼ)).

Başka bir deyişle, yᵢ ve yⱼ farklı indekslere eşlenmelidir.

Böyle bir atama elde edildiğinde, tüm literallerin doğruluk değerleri birleştirilerek bir bit-vektöre (depolama) dönüştürülür. Bu bit-vektör kullanılarak, H₁, ..., Hₖ hash fonksiyonları aracılığıyla basit erişimler yapılarak bir elemanın indeksi bit bit hesaplanabilir.

Example 1

Şu küme olsun:

Y = {y₁, y₂, y₃, y₄}

Buna göre:

• n = 4
• k = ⌈log₂(n)⌉ = 2

Bu örnek için m = 6 adet Boolean değişken seçiyoruz.

H₁ ve H₂ hash fonksiyonlarının değerlendirilmesi sonucunda aşağıdaki literaller elde edildiğini varsayalım:

Elde edilen bit-vektörler şunlardan oluşur:

• y₁ için x₁x₅
• y₂ için x₂x₆
• y₃ için x₃x₁
• y₄ için x₅x₄

Örneğin şu atama:

• x₂ = 0
• x₄ = 0
• diğer tüm değişkenler = 1

tüm indeksleri farklı yapar:

• y₁ → 2 (⟨01⟩)
• y₂ → 3 (⟨10⟩)
• y₃ → 4 (⟨11⟩)
• y₄ → 1 (⟨00⟩)

MPHF'nin depolama gösterimi:

⟨101011⟩

Bu, 4 eleman için 6 bit, yani eleman başına 1.5 bit kullanır.

Bir sorgu işlemi, saklanan bit-vektör üzerinde k adet erişim gerektirir.

Encodings

Bir problemin SAT biçimine kodlanması, SAT çözücülerinin performansı üzerinde önemli etki yapabilir. Aynı durum MPHF için de gözlemlenmiştir.

Etkili bir kodlama için yaygın kullanılan bir sezgisel yaklaşım, şu iki değerin toplamını en aza indirmektir:

• değişken sayısı
• clause sayısı

Bu sezgisel yaklaşım SAT ön işleme tekniği bounded variable elimination (Eén and Biere 2005) içinde kullanılır. Bu nedenle ilk çalışmalarımız kompakt bir kodlama tasarlamaya odaklanmıştır.

Eğer n (anahtar sayısı) 2'nin bir kuvveti ise, kodlama yalnızca aşağıdaki all-different constraint gerektirir:

∧_{1 ≤ i < j ≤ n} L₁(yᵢ)...Lₖ(yᵢ) ≠ L₁(yⱼ)...Lₖ(yⱼ)

Ayrıca anahtar sayısı 2'nin bir kuvveti değilse, hiçbir elemanın n'den büyük değerlere eşlenmemesini belirten bir kısıt da gereklidir.

Compact Encoding

İlk kodlama şu yardımcı değişkenleri tanıtır:

e_{a,b}

burada

a,b ∈ {x₁, ¬x₁, ..., xₘ, ¬xₘ}

olup a ve b literallerinin eşit olduğunu temsil eder.

Özellikler:

• e_{a,a} = 1
• e_{a,¬a} = 0
• e_{a,b} = e_{b,a}

Bu değişkenler şu clause'ları oluşturmak için kullanılır:

∧{1 ≤ i < j ≤ n} (e{L₁(yᵢ),L₁(yⱼ)} ∨ ... ∨ e_{Lₖ(yᵢ),Lₖ(yⱼ)})

Bu clause'lar farklı elemanların anahtarlarının en az bir bitte farklı olmasını garanti eder.

Eşitlik değişkenlerinin anlamı bir XOR kısıtı kullanılarak kodlanabilir. Üçlü XOR kısıtları normalde dört clause gerektirse de, diğerleri blocked (Kullmann 1999) ve dolayısıyla gereksiz olduğundan yalnızca pozitif literal içeren iki clause kullanılmıştır.

Ortaya çıkan kodlama şunları içerir:

• O(n² log² n) adet üçlü clause
• uzunluğu k olan O(n²) clause

Cubic Encoding

Daha etkili bir kodlama hiç yardımcı değişken kullanmaz.

Eğer anahtar sayısı 2'nin bir kuvveti ise, kısıt şu hale gelir:

L₁(yᵢ)...Lₖ(yᵢ) = l → L₁(yⱼ)...Lₖ(yⱼ) ≠ l

şu tüm durumlar için:

1 ≤ i,j,l ≤ n ve i ≠ j.

Burada L₁(yᵢ)...Lₖ(yᵢ) bit-vektörünün yorumu, [n] aralığındaki l konumuna karşılık gelir.

Örnek:

⟨000⟩ = 1
⟨001⟩ = 2

Eğer anahtar sayısı 2'nin bir kuvveti değilse, geçerli aralığın dışındaki l değerleri için en anlamlı bit literalleri (L₁(yᵢ) ve L₁(yⱼ)) kaldırılır.

CNF biçiminde temsil edildiğinde:

• clause sayısı O(n³)
• clause uzunluğu 2k

olur.

Bu, kompakt kodlamadan çok daha büyüktür. Bu nedenle bir milyonun üzerinde clause içeren formüllerin mevcut SAT çözücüleri için zaten zorlayıcı olması nedeniyle yüzlerce anahtara ölçeklenmesi olası görünmemektedir.

Bu kodlama ayrıca çok sayıda tautological clause ve duplicate literal üretir; bunlar üreteç tarafından kaldırılır.

Büyüklüğüne rağmen cubic kodlama daha etkili olduğunu göstermiştir.

Örnek performans karşılaştırması:

• 32 anahtar, 46 değişken
  • cubic kodlama: ~4 saniye
  • compact kodlama: ~8.5 saniye

Muhtemel sebep, cubic kodlamanın daha fazla unit propagation yapılmasına olanak sağlamasıdır.

Example 1 kullanılarak verilen örnek:

y₁ ve y₃'ün farklı olması gerektiği kısıtı şu anlama gelir:

x₁x₅ ≠ x₃x₁

Atama altında:

• x₃ = doğru
• x₅ = yanlış

x₁'in doğru olması gerektiğini çıkarabiliriz. Kübik kodlamadaki birim yayılım bu sonucu otomatik olarak türetir.

Buna karşılık, kompakt kodlama aşağıdaki gibi ikili klozlar üretir:

(ex₁,x₃ ∨ ex₁,x₅)

(ex₁,x₃ ∨ x₁)

(ex₁,x₅ ∨ x₁)

bunlar çıkarımı aynı derecede etkili biçimde yaymaz.

Tüm-farklı bit-vektör kısıtları için başka kodlamalar da incelenmiştir (Biere and Brummayer 2008; Surynek 2012), ancak bu çalışmalar bit-vektör sayısının aralıklarına göre çok daha küçük olduğu durumları ele almıştır. Bizim durumumuzda ise bu iki değer yaklaşık olarak eşittir.

Deneysel Gözlemler

m ≥ ⌈n / ln 2⌉

olan MPHF problemlerinin SAT kodlamalarının sağlanabilir olma olasılığı yüksektir (değerlendirmede n 40'a kadar).

MPHF oluşturmanın bilgi kuramsal sınırına yakın bir yerde bir faz geçişi ortaya çıkar.

Tüm m değişkenlerini kullanan örneklerin sağlanabilir olma olasılığı daha yüksektir. Değişkenler eksik olduğunda sağlanamazlık daha olası hale gelir.

n = 40 için gözlemlenen faz geçişi, yalnızca tüm değişkenleri kullanan örnekler dikkate alındığında α₄₀ değerine çok daha yakındır.

Deneyler, SAT tabanlı yöntemlerin değerlendirilen küçük anahtar kümeleri için neredeyse alan-optimal MPHFs oluşturabildiğini göstermektedir. Anahtar sayısı arttıkça eğrinin daha da keskinleşmesi beklenmektedir.

Bildiğimiz kadarıyla bu, 40 anahtar için makul sürede neredeyse alan-optimal MPHF oluşturabilen ilk yaklaşımdır.

Bununla birlikte, hazır SAT çözücüleriyle yapılan deneyler, çalışma süresinin anahtar sayısına göre üstel biçimde büyüdüğünü göstermektedir.

Örneğin:

• Faz geçişi yakınındaki 40 anahtarlı örneklerin çözümü ortalama ~800 saniye sürmektedir.
• Bazı örnekler birkaç saat sürebilir.
• En zor 30 anahtarlı örnek saniyeler içinde çözülür.

40 anahtar için anahtar başına 1.8 bit civarındaki çalışma süresi artışı, çözüm sırasında çok az sayıda alt problemin üretilmesinden kaynaklanır. Alt problem üretimini artırmak toplam çalışma süresini azaltabilir.

Deneyler, probsat (Balint and Schöning 2012) dahil olmak üzere tam ve eksik en gelişmiş SAT çözücüleri kullanılarak gerçekleştirilmiştir.

Daha büyük örneklere ölçeklenebilen daha iyi bir SAT kodlamasının bulunup bulunamayacağı gelecekteki çalışmalar için açık bir problemdir.

Deneysel Değerlendirme

Bilgi kuramsal sınıra yakın MPHFs oluşturmak için SAT tabanlı yaklaşımımızın etkinliğini değerlendirdik. Kodlama ve kod çözme araçları https://github.com/weaversa/MPHF adresinde mevcuttur. Ortaya çıkan formülleri çözmek için cube-and-conquer (Heule et al. 2012) yaklaşımını kullandık; çünkü bu yaklaşım en zor MPHF örneklerinde güçlü performans göstermiştir.

Cube-and-conquer verilen bir problemi birden fazla alt probleme böler ve bu alt problemler bir “conquer” çözücüsü tarafından çözülür. Conquer çözücüsü olarak glucose 3.0 (Audemard and Simon 2009) kullandık. Belirtilen tüm çalışma süreleri, problemin bölünmesi ile conquer çözücüsünün tek bir Xeon CPU E5-2650 çekirdeğinde gerçekleştirdiği çözme süresinin toplamıdır.

Şekil 1 (sol) 10, 20, 30 ve 40 rastgele anahtar için, anahtar başına bit sayısı 1 ile 2 arasında olacak şekilde elde edilen sonuçları göstermektedir. Her nokta, her anahtar sayısı (n) ve değişken sayısı (m) için 2400 örnek üzerinden ortalaması alınmış sağlanabilir formüllerin oranını göstermektedir. Kalın dikey çizgi bilgi kuramsal sınırı göstermektedir.

UNSAT'tan SAT'a gözlemlenen faz geçişi, anahtar sayısı arttıkça daha keskin hale gelmektedir. Ayrıca 40 anahtara dayalı eğri, büyük n değerlerinde bilgi kuramsal sınırdaki %50 noktasında neredeyse simetrik görünmektedir (180 derece döndürme). Bilgi kuramsal sınırın (\alpha_{40} = 1.343) olduğunu hatırlayalım. Bu nedenle faz geçişi sınırdan biraz sonra gerçekleşmektedir. Sonuçları analiz ettik ve yakınsamayan çeşitli örnekler fark ettik.

1.83n MPHF Oluşturma

Anahtar başına yaklaşık 1.83n bit ile MPHF oluşturulmasına izin veren ikinci MPHF oluşturma yöntemi de k evrensel karma fonksiyon ailesi kullanır ve m bitlik bir bit-vektör döndürür. Ancak bir anahtar için indeksin elde edilmesi oldukça farklıdır. İndeksi bit bit hesaplamak yerine, ikinci MPHF yaklaşımı indeksi elde etmek için hangi karma fonksiyonunun kullanılacağını hesaplar.

n elemanlı Y kümesi için bir MPHF oluşturmak üzere, aralığı ([n]) olan H₁, ..., Hₖ evrensel karma fonksiyonları verildiğinde, önce ağırlıklı iki parçalı bir grafik G = (Y, [n], E) oluştururuz. Burada tüm (y \in Y) ve tüm (i \in [k]) için ((y, H_i(y)) \in E) olur ve:

weight(y, H_i(y)) = i

Ağırlıklı iki parçalı grafik, sol taraftaki düğümlerin Y elemanlarını ve sağ taraftaki düğümlerin ([n]) elemanlarını temsil edeceği şekilde oluşturulur. Karma fonksiyonları, her sol taraf düğümünün k adet sağ taraf düğümüne nasıl bağlanacağını belirler. Her (y \in Y) için şu değerleri hesaplayın:

H₁(y), ..., Hₖ(y)

ve y düğümünden karma fonksiyonlarının ürettiği düğümlere kenarlar ekleyin. Her kenarın ağırlığı kullanılan karma fonksiyonunun indeksi olarak atanır.

k parametresi, G grafiğinin mükemmel eşleşmeye sahip olmasını garanti edecek şekilde seçilmelidir. Frieze and Melsted (2012) tarafından verilen bir sonuç, sol taraf düğümlerinin derecesi en az üç ve sağ taraf düğümlerinin derecesi en az iki olduğunda G'nin yüksek olasılıkla mükemmel eşleşmeye sahip olacağını göstermektedir.

Newman and Shepp (1960) sağ taraftaki düğümlerin, kenar sayısı şu değere ulaştığında yüksek olasılıkla derece ikiye sahip olacağını göstermiştir:

n(ln n + ln(ln n))

Her Hᵢ fonksiyonu n anahtarı karmaladığından, k parametresi için optimal değer şudur:

max(3, ln n + ln(ln n))

M, G grafiğinin minimum ağırlıklı mükemmel eşleşmesi olsun. M, Hungarian Algorithm (Kuhn 1955) kullanılarak (O(n^3)) adımda bulunabilir. M, aynı zamanda oluşturulan MPHF'nin birebir eşlemesidir. G, Parviainen'in önerdiği Case II durumuna uyduğundan (Parviainen 2004), M'nin ağırlığı asimptotik olarak yaklaşık 1.83n olur; bu değer deneysel olarak belirlenmiştir.

Eşleme M, her y için Hᵢ(y) ∈ M ise aşağıdakini saklayacak şekilde alan açısından verimli bir geri getirme yapısında saklanır:

• ((i, y), 1) — kesin varlık

ve her j < i için şu değer saklanır:

• ((j, y), 0) — kesin yokluk

Böyle bir geri getirme yapısı (O((1.83n)^3)) adımda oluşturulabilir, saklanan her eleman başına bir bit alan kullanır ve az sayıda sabit adımda erişilebilir (Dietzfelbinger and Walzer 2019a).

Hem Hungarian Algorithm hem de geri getirme yapısının oluşturma süreci, girdinin küçük kümelere bölünmesinden (sharding) fayda sağlayabilir; bu kümelerin tümü paralel olarak işlenebilir. Bu, MPHF'nin iki adet (O(n^3)) adımından daha verimli şekilde oluşturulabileceği anlamına gelir; ancak küçük bir alan verimliliği kaybı olabilir. Bu MPHF yapısının uzun vadeli depolama boyutu yaklaşık 1.83n bit olup geri getirme yapısının boyutuna karşılık gelir.

y elemanının karşılık gelen indeksini bulmak için geri getirme yapısı (i, y) ile sorgulanır; başlangıçta i = 1 alınır ve 1 döndürülene kadar artırılır. Bu durumda y için indeks Hᵢ(y) olur.

Örnek 2

İki parçalı bir grafiğin minimum ağırlıklı mükemmel eşleşmesini bir k-XORSAT örneğinin çözümünde saklayarak MPHF oluşturmanın ayrıntılı bir örneğini veriyoruz.

Şu küme olsun:

Y = {y₁, y₂, y₃, y₄, y₅}

Dolayısıyla n = 5 ve:

k = max(3, ln 5 + ln(ln 5)) = 3

Önce k karma fonksiyonu, Y kümesinin tüm elemanları üzerinde değerlendirilir ve aşağıdaki tablo elde edilir.

Sonraki adımda, tabloda her Y elemanı için elemandan karma fonksiyonlarının sonuçlarına kenarlar eklenerek iki parçalı bir grafik oluşturulur. Örneğin y₁, 1, 5 ve 2 düğümlerine bağlanır.

Her kenarın ağırlığı kullanılan karma fonksiyonunun indeksine eşittir. Örneğin:

• (y₁, 1) kenarının ağırlığı 1'dir
• (y₂, 5) kenarının ağırlığı 3'tür

Daha sonra iki parçalı grafiğin minimum ağırlıklı mükemmel eşleşmesini bulmak için Hungarian Algorithm kullanılır. Böyle bir eşleşmenin ağırlığı 8 olabilir.

Bu durum aşağıdaki saklanan tuple'lara karşılık gelir:

• ((y₁, 1), 1)
• ((y₂, 1), 1)
• ((y₃, 1), 0)
• ((y₃, 2), 0)
• ((y₃, 3), 1)
• ((y₄, 1), 0)
• ((y₄, 2), 1)
• ((y₅, 1), 1)

XORSAT Filtre Oluşturma

Son adım, eşleşmeyi bir XORSAT filtresinde saklamaktır. Bu örnekte aşağıdaki 8 elemanı saklıyoruz.

Elemanlar, Weaver, Roberts, and Smith (2018) tarafından önerildiği şekilde filtrede saklanır; burada tuple'ın ilk kısmı filtrelenen elemanı, ikinci kısmı ise bir bitlik metaveriyi temsil eder.

t, tuple sayısını göstersin (burada t = 8). XORSAT filtresi, aralığı ([t]) olan iki karma fonksiyonu kullanılarak oluşturulur. Okunabilirlik amacıyla burada yalnızca iki karma fonksiyonu kullanılmıştır; pratikte daha yüksek verimlilik için beş karma fonksiyonu kullanılır.

XOR kısıtlarının birleşimi sağlanabilirdir. Örneğin şu atamayı yapalım:

• x₂ = 1
• x₃ = 1
• x₅ = 1

ve diğer tüm değişkenleri 0.

Böylece şu bit vektörünü saklarız:

⟨01101000⟩

Bu, 5 eleman için 8 bit kullanır.

Bir y elemanının indeksini belirlemek için filtre, 1 döndürene kadar tekrar tekrar sorgulanır.

Örnek: y₃'ün indeksinin belirlenmesi.

1. (y₃, 1) sorgulanır → 4 ve 8'e karmalanır → filtre 0 döndürür.
2. (y₃, 2) sorgulanır → filtre 0 döndürür.
3. (y₃, 3) sorgulanır → filtre 1 döndürür.

Dolayısıyla MPHF indeksi:

H₃(y₃) = 4

Pratik Uygulama

Birçok pratik algoritma, statik sözlükler üzerinde doğrusal zamanlı oluşturma ve sabit zamanlı arama işlemlerini destekler (Seiden and Hirschberg 1994; Dietzfelbinger and Pagh 2008; Aumüller, Dietzfelbinger, and Rink 2009; Porat 2009; Botelho, Pagh, and Ziviani 2013; Genuzio, Ottaviano, and Vigna 2016; Dietzfelbinger and Walzer 2019a). Genelliği bozmadan burada XORSAT filtresi (Weaver, Roberts, and Smith 2018) kullanılmıştır.

Deneyler, şu bileşenlerin gerçekleştirimlerinden oluşan bir araç kullanılarak yürütülmüştür:

• minimum ağırlıklı iki parçalı mükemmel eşleşme bulucu
• bir XORSAT filtresi

Tüm çalıştırmalar şu özelliklere sahip bir Amazon EC2 örneğinde (m5.4xlarge) gerçekleştirilmiştir:

• 16 CPU çekirdeği
• 64 GiB RAM
• saat başına 0.768 USD maliyet

Tablo 2 — Minimum Ağırlıklı Mükemmel Eşleşme İçin Çalışma Süresi

n anahtar üzerinde minimum ağırlıklı iki parçalı mükemmel eşleşmeyi hesaplamak için gereken çalışma süresi (saniye).

Tablo 3 — Bloklu MPHF Performansı

n anahtar üzerinde bir bloklu MPHF hesaplamak için elde edilen anahtar başına bit (BPK) ve gereken süre. Boyut, elde edilen MPHF'nin kilobayt cinsinden boyutunu ifade eder. Sorgu hızı sorgu başına nanosaniye cinsinden ölçülmüştür.

Sonuçlar, girdi bloklama (sharding) yapılmadan büyük bir MPHF oluşturmanın pratik olmadığını göstermektedir. Bloklama, büyük kümelerin verimli biçimde işlenmesine olanak tanır; ancak ek blok metaverisi nedeniyle alan verimliliğini biraz azaltır.

2¹³ ile 2¹⁴ arasındaki bir blok boyutu, blokların yaklaşık bir saniyede oluşturulmasına olanak tanır ve hız ile alan verimliliği arasında pratik bir denge sağlar.

Kavram Kanıtı

1.83n MPHF oluşturma yönteminin kurulumu ve test edilmesine ilişkin bazı deneysel sonuçlar sunuyoruz. Bu amaçla, (Weaver, Roberts, and Smith 2018) yaklaşımını takip eden ve blok boyutu 4608 olan bir uygulama yazdık. Ayrıca Dietzfelbinger and Walzer tarafından önerilen seyrek vektör üretim yöntemini de kullandık (Dietzfelbinger and Walzer 2019a). Beklendiği gibi her çalıştırma, minimum ağırlığı 1.831n olan ağırlıklı bir iki parçalı grafik üretti; dolayısıyla alan verimliliğindeki herhangi bir kayıp, MPHF bloklama şeması hakkında saklanan ek bilgilerden ve ortaya çıkan XOR-SAT filtrelerindeki verimsizliklerden kaynaklanmaktadır.

Dietzfelbinger and Walzer tarafından önerilenler gibi alan açısından verimli geri getirme yapılarının oluşturulmasına yönelik son pratik iyileştirmeler (Dietzfelbinger and Walzer 2019b), burada verilen sonuçları muhtemelen geliştirecektir (daha kısa oluşturma süresi) ve bunları gelecekteki çalışmalarda değerlendirmeyi planlıyoruz.

Yaklaşımımız ile mevcut en gelişmiş yöntemler arasında bir karşılaştırma yaptık. Özellikle, 2³⁰ eleman için MPHF üretmek amacıyla benchmphf aracını kullandık. benchmphf aracı EMPHF (Belazzougui et al. 2014), HEM (Botelho, Pagh, and Ziviani 2013), CHD (Belazzougui, Botelho, and Dietzfelbinger 2009) ve Sux4j uygulamalarını desteklemektedir. Sonuçlarımız, Limasset et al. (Limasset et al. 2017) tarafından bildirilenlerle benzerdi; oluşturma süresi 400 ile 2000 saniye arasında, anahtar başına bit 2.90 ile 4.22 arasında ve sorgu süresi sorgu başına 250 ile 1000 nanosaniye arasındaydı. 2³⁰ eleman için uygulamamız anahtar başına 1.85 bit elde etti, oluşturma işlemi (sıralı olarak) 120000 saniye sürdü ve sorgu süresi yaklaşık sorgu başına 550 nanosaniyedir.

Mükemmel Karma Fonksiyonları

Çalışmamız MPHF'lere odaklanmaktadır, ancak aynı teknikler (minimal olmayan) mükemmel karma fonksiyonları (PHF) oluşturmak için de kullanılabilir. SAT tabanlı yaklaşımda zaten gözlemlediğimiz gibi, değişken sayısını artırmak (yani bilgi kuramsal sınıra olan mesafeyi büyütmek) bir MPHF oluşturma maliyetlerini azaltır. Alternatif olarak maliyetler, anahtarların eşlendiği aralığı büyüterek ve böylece boşluklara izin vererek de azaltılabilir.

PHF'ler için yeniden düzenlenmiş 1.83n MPHF oluşturma yöntemi ele alındığında, iki parçalı grafikte sağ taraf düğümlerinin sol taraf düğümlerine oranı 1'den büyük olacaktır. Bu durum grafiğin minimum ağırlığını nasıl etkiler? Eğer ağırlık oran büyüdükçe yavaş artıyorsa, burada önerilen yöntem alan açısından verimli PHF'ler oluşturmak için de kullanılabilir.

Sonuçlar ve Gelecek Çalışmalar

İki MPHF oluşturma yöntemi sunduk. İlk yöntemimiz bilgi kuramsal sınıra yakın depolama verimliliği sağlar; ancak dezavantajı, SAT çözme tekniklerinin şu anda yalnızca 40 anahtara kadar olan örneklerle başa çıkabilmesidir; bu yine de önceki (brute-force) yaklaşımların iki katıdır. İkinci yöntemimiz pratiktir; büyük veri kümeleri için düşük maliyetle ve yüksek sorgu hızlarıyla MPHF oluşturulmasına olanak tanır. Aslında bu, şu anda bilinen tüm pratik MPHF oluşturma yöntemleri arasında depolama açısından en verimli olanıdır.

Gelecekteki çalışmalar için heyecan verici zorluklardan biri, önemli sayıda eleman için bilgi-kuramsal sınıra yakın MPHFs oluşturabilen bir SAT çözme aracının geliştirilip geliştirilemeyeceğini belirlemektir. Böyle bir yaklaşım büyük olasılıkla yerel arama tekniklerine dayanacaktır; çünkü bu teknikler, uniform rastgele k-SAT formülleri gibi rastgele problemlerde daha iyi ölçeklenme eğilimindedir.

Deneylerimiz, yardımcı değişkenler içermeyen çok büyük bir kodlamanın, daha kompakt kodlamalardan daha iyi sonuçlar elde ettiğine dair şaşırtıcı bir gözlem ortaya koydu. Daha önce belirtildiği gibi, bunun nedeni kübik kodlamanın artmış yayılım gücü olabilir. Kübik kodlamayla aynı yayılım gücüne sahip, yalnızca O(n² log² n) kloz içeren bir kodlamanın geliştirilmesi sonuçları daha da iyileştirebilir.

Teşekkürler

İkinci yazar, CCF-1813993 numaralı hibe kapsamında National Science Foundation (NSF) tarafından desteklenmektedir. Yazarlar, makalenin kalitesini iyileştirmeye yönelik değerli katkılarından dolayı Benjamin Kiesl’e ve anonim hakemlere teşekkür eder. Yazarlar ayrıca, bu makalede raporlanan araştırma sonuçlarına katkıda bulunan HPC kaynaklarını sağladığı için The University of Texas at Austin bünyesindeki Texas Advanced Computing Center (TACC)’a teşekkür eder.

Kaynaklar

[Audemard and Simon 2009] Audemard, G., ve Simon, L. 2009. Modern SAT çözücülerinde öğrenilen klozların kalitesini tahmin etmek. IJCAI’09 içinde, 399–404. Morgan Kaufmann Publishers Inc.

[Aumüller, Dietzfelbinger, and Rink 2009] Aumüller, M.; Dietzfelbinger, M.; ve Rink, M. 2009. Kuramsal olarak iyi bir retrieval veri yapısının deneysel varyasyonları. European Symposium on Algorithms içinde, 742–751. Springer.

[Balint and Schöning 2012] Balint, A., ve Schöning, U. 2012. Stokastik yerel arama için olasılık dağılımlarının seçimi ve make ile break arasındaki rol. Cimatti, A., ve Sebastiani, R., eds., Theory and Applications of Satisfiability Testing – SAT 2012, Lecture Notes in Computer Science serisi, cilt 7317, 16–29. Springer.

[Belazzougui et al. 2014] Belazzougui, D.; Boldi, P.; Ottaviano, G.; Venturini, R.; ve Vigna, S. 2014. Rastgele hipergraphların cache-oblivious soyulması. Bilgin, A.; Marcellin, M. W.; Serra-Sagristà, J.; ve Storer, J. A., eds., Data Compression Conference, DCC 2014, Snowbird, UT, ABD, 26–28 Mart 2014, 352–361. IEEE.

[Belazzougui, Botelho, and Dietzfelbinger 2009] Belazzougui, D.; Botelho, F. C.; ve Dietzfelbinger, M. 2009. Hash, displace ve compress. European Symposium on Algorithms içinde, 682–693. Springer.

[Biere and Brummayer 2008] Biere, A., ve Brummayer, R. 2008. Bir SAT çözücü içinde bit-vektörler üzerindeki all-different kısıtlarının tutarlılık denetimi. Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, FMCAD ’08 içinde, 28:1–28:4. Piscataway, NJ, ABD: IEEE Press.

[Botelho, Pagh, and Ziviani 2013] Botelho, F. C.; Pagh, R.; ve Ziviani, N. 2013. Neredeyse optimal alanda pratik perfect hashing. Information Systems 38(1):108–131.

[Dietzfelbinger and Pagh 2008] Dietzfelbinger, M., ve Pagh, R. 2008. Retrieval ve yaklaşık üyelik için özlü veri yapıları. International Colloquium on Automata, Languages, and Programming içinde, 385–396. Springer.

[Dietzfelbinger and Walzer 2019a] Dietzfelbinger, M., ve Walzer, S. 2019a. o(log m) ek bit ile sabit zamanlı retrieval. STACS 2019 içinde. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.

[Dietzfelbinger and Walzer 2019b] Dietzfelbinger, M., ve Walzer, S. 2019b. Yoğun soyulabilir rastgele uniform hipergraphlar. ESA 2019 içinde, LIPIcs serisi, cilt 144, 38:1–38:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[Eén and Biere 2005] Eén, N., ve Biere, A. 2005. Değişken ve kloz eliminasyonu yoluyla SAT içinde etkili ön işleme. Bacchus, F., ve Walsh, T., eds., SAT, Lecture Notes in Computer Science serisi, cilt 3569, 61–75. Springer.

[Fredman and Komlós 1984] Fredman, M. L., ve Komlós, J. 1984. Ayırıcı sistemlerin ve perfect hash fonksiyon ailelerinin boyutu üzerine. SIAM Journal on Algebraic Discrete Methods 5(1):61–68.

[Frieze and Melsted 2012] Frieze, A., ve Melsted, P. 2012. Rastgele iki parçalı grafiklerde maksimum eşleşmeler ve cuckoo hash tablolarının alan kullanımı. Random Structures & Algorithms 41(3):334–364.

[Gableske 2014] Gableske, O. 2014. SAT için ürün tabanlı MP çerçevesinin Ising modeli esinli bir genişletmesi. Sinz, C., ve Egly, U., eds., Theory and Applications of Satisfiability Testing – SAT 2014, Lecture Notes in Computer Science serisi, cilt 8561, 367–383. Springer.

[Genuzio, Ottaviano, and Vigna 2016] Genuzio, M.; Ottaviano, G.; ve Vigna, S. 2016. (Minimal perfect hash) fonksiyonlarının hızlı ve ölçeklenebilir oluşturulması. International Symposium on Experimental Algorithms içinde, 339–352. Springer.

[Heule et al. 2012] Heule, M. J. H.; Kullmann, O.; Wieringa, S.; ve Biere, A. 2012. Cube and conquer: Lookahead kullanarak CDCL SAT çözücülerini yönlendirmek. Hardware and Software: Verification and Testing içinde, 50–65. Springer.

[Kautz and Selman 1996] Kautz, H. A., ve Selman, B. 1996. Sınırları zorlamak: Planlama, önermesel mantık ve stokastik arama. Clancey, W. J., ve Weld, D. S., eds., AAAI 96 içinde, 1194–1201. AAAI Press / The MIT Press.

[Kuhn 1955] Kuhn, H. W. 1955. Atama problemi için Hungarian yöntemi. Naval Research Logistics Quarterly 2(1–2):83–97.

[Kullmann 1999] Kullmann, O. 1999. Genişletilmiş çözümlemenin bir genellemesi üzerine. Discrete Applied Mathematics 96–97:149–176.

[Limasset et al. 2017] Limasset, A.; Rizk, G.; Chikhi, R.; ve Peterlongo, P. 2017. Çok büyük anahtar kümeleri için hızlı ve ölçeklenebilir minimal perfect hashing. 16th International Symposium on Experimental Algorithms içinde, cilt 11, 1–16.

[Mehlhorn 1982] Mehlhorn, K. 1982. Perfect ve evrensel hash fonksiyonlarının program boyutu üzerine. 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982) içinde, 170–175. IEEE.

[Newman and Shepp 1960] Newman, D. J., ve Shepp, L. 1960. Double dixie cup problemi. The American Mathematical Monthly 67(1):58–61.

[Parviainen 2004] Parviainen, R. 2004. Tamsayı maliyetlerle rastgele atama. Combinatorics, Probability and Computing 13(1):103–113.

[Porat 2009] Porat, E. 2009. Matris çözmeye dayalı optimal bir Bloom filter alternatifi. Frid, A. E.; Morozov, A.; Rybalchenko, A.; ve Wagner, K. W., eds., CSR 2009, Lecture Notes in Computer Science serisi, cilt 5675, 263–273. Springer.

[Seiden and Hirschberg 1994] Seiden, S. S., ve Hirschberg, D. S. 1994. Özlü sıralı minimal perfect hash fonksiyonlarının bulunması. Information Processing Letters 51(6):283–288.

[Surynek 2012] Surynek, P. 2012. Bit-vektörler üzerindeki all-different kısıtı için alternatif bir eager kodlama. Proceedings of the 20th European Conference on Artificial Intelligence, ECAI’12 içinde, 927–928. Amsterdam, Hollanda: IOS Press.

[Weaver, Roberts, and Smith 2018] Weaver, S. A.; Roberts, H. J.; ve Smith, M. J. 2018. XOR-doyurulabilirlik küme üyelik filtreleri. International Conference on Theory and Applications of Satisfiability Testing içinde, 401–418. Springer.