yazan: Donald E. Knuth*
Özet. Clause'ların hiyerarşik bir yapıya sahip olduğu sağlanabilirlik probleminin özel bir durumunun, clause'ların uygun bir şekilde temsil edildiği varsayımı altında, doğrusal zamanda çözülebilir olduğu gösterilmiştir.
$X$, $<$ bağıntısı ile doğrusal olarak sıralanmış sonlu bir alfabe olsun; $X$'in elemanlarını mantıksal (boolean) değişkenler olarak düşüneceğiz. Her zamanki gibi, $X$ üzerindeki literalleri (harfleri), $x \in X$ olmak üzere, $x$ veya $\bar{x}$ formundaki elemanlar olarak tanımlıyoruz. $X$'e ait olan literallere pozitif, diğerlerine ise negatif literaller denir.
$X$ üzerindeki doğrusal sıralama, işaretler göz ardı edilerek doğal bir yolla tüm literallerin doğrusal bir yarı-sıralamasına (preordering) genişletilebilir. Örneğin, $X = \{a, b, c\}$ kümesi alışılagelmiş alfabetik sıraya sahipse, şunu elde ederiz:
$$\bar{a} \equiv a < \bar{b} \equiv b < \bar{c} \equiv c.$$
Eğer $\sigma$ ve $\tau$ iki literal ise, $\sigma < \tau$ veya $\sigma \equiv \tau$ olduğunda $\sigma \preceq \tau$ yazarız; bu durum ancak ve ancak $\sigma \succ \tau$ bağıntısı yanlış olduğunda geçerlidir.
$X$ üzerinde bir clause, farklı değişkenlerden oluşan bir literaller kümesidir. Dolayısıyla, bir clause'un literalleri artan sırada yazılabilir:
$$\sigma_1 < \sigma_2 < \cdots < \sigma_k.$$
$X$ üzerindeki bir clause'lar kümesi $C$, eğer $C$'deki her clause ile kesişimi boş olmayan, $X$ üzerinde bir clause mevcutsa sağlanabilirdir. Örneğin, $\{a, b, c\}$ üzerindeki
$$\{\bar{a}, \bar{b}, \bar{c}\},\; \{\bar{a}, c\},\; \{\bar{a}, b, \bar{c}\},\; \{a, \bar{c}\},\; \{a, b\}$$
clause'ları, benzersiz bir şekilde $\{\bar{a}, \bar{b}, \bar{c}\}$ clause'u tarafından sağlanabilir.
Eğer $C$ clause'unda $\sigma, \tau$ ve $C'$ clause'unda $\xi'$ literalleri
$$\sigma < \xi' < \tau$$
olacak biçimde mevcutsa, $C$ clause'unun $C'$ clause'unu ortaladığını (straddle ettiğini) söyleriz.
İki clause karşılıklı olarak birbirini ortalıyorsa çakışır (overlap). Örneğin, $\{\bar{a}, b, c\}$ ve $\{a, \bar{b}, \bar{c}\}$ clause'ları çakışır; ancak yukarıdaki örnekteki diğer dokuz clause çifti çakışmamaktadır. Her biri ikişer elemanlı olan $\{\bar{a}, c\}$ ve $\{\bar{b}, d\}$ gibi clause'lar da çakışabilir. Hiçbir iki clause'un çakışmadığı bir clause'lar kümesine iç içe geçmiş (nested) denir.
Verilen bir clause'lar kümesinin sağlanabilir olup olmadığına karar verme genel probleminin NP-tam (NP-complete) olduğu iyi bilinmektedir. Ancak iç içe geçmiş clause'lar için benzer sorunun verimli bir şekilde kararlaştırılabileceğini göreceğiz. İç içe geçmiş clause'lara duyulan ilginin temel nedeni, David Lichtenstein'ın düzlemsel sağlanabilirlik (planar satisfiability) teoremidir; bu teorem cebirsel terimlerle şu şekilde yeniden ifade edilebilir: İki iç içe geçmiş clause kümesi $C$ ve $C'$ için ortak sağlanabilirlik problemi NP-tamdır. Hatta Lichtenstein, $C$'nin tüm clause'ları yalnızca pozitif literaller içerse ve $C'$'nin tüm clause'ları yalnızca negatif literaller içerse dahi (her clause'da en fazla üç literal olmak üzere) bu problemin NP-tam olduğunu kanıtlamıştır [1, s. 339].
1. İç içe geçmiş clause'ların yapısı.
Sıralı bir alfabe üzerindeki bir clause'un bir en küçük literali $\sigma$ ve bir en büyük literali $\tau$ vardır. $\sigma$ ile $\tau$ arasında kesin olarak yer alan herhangi bir değişkene, o clause'un iç (interior) değişkeni denir. Bir değişken, iç içe geçmiş clause'lar kümesinde en fazla bir kez bir iç literal olarak yer alabilir; çünkü eğer iki farklı clause'da iç literal olarak bulunursa, bu clause'lar çakışır. Bu nedenle, $n$ değişken üzerindeki $m$ adet iç içe geçmiş clause'daki toplam eleman sayısı (tüm clause'ların boyutlarının toplamı) en fazla $2m + n$ olabilir.
Eğer $C$ clause'u $C'$ clause'unu ortalıyor ancak $C'$ clause'u $C$ clause'unu ortalamıyorsa, $C \succ C'$ yazarız. Bu bağıntı geçişlidir (transitive). Çünkü eğer $C \succ C'$ ve $C'$ clause'u $C''$ clause'unu ortalıyorsa, uygun clause'larda
$$\sigma < \xi' < \tau, \quad \sigma' < \xi'' < \tau'$$
literallerine sahibizdir; ve $\sigma \preceq \sigma'$ ile $\tau' \preceq \tau$ olmalıdır, aksi takdirde $C'$ clause'u $C$'yi ortalardı. Dolayısıyla $C$ clause'u $C''$ clause'unu ortalar. Benzer şekilde, eğer $C' \succ C''$ ve $C''$ clause'u $C$ clause'unu ortalıyorsa, o zaman $C'$ clause'u $C$ clause'unu ortalar. Dolayısıyla $C \succ C' \succ C''$ olması $C \succ C''$ olmasını gerektirir.
İç içe geçmiş bir clause'lar kümesinde, $C \succ C'$ olması ancak ve ancak $C$ clause'unun $C'$ clause'unu ortalaması durumunda geçerlidir. Bu bağıntının geçişli olması, herhangi bir iç içe geçmiş clause'lar kümesini, her clause'un ortaladığı her clause'dan sonra göründüğü doğrusal bir dizilim haline topolojik olarak sıralayabileceğimizi (topological sort) gösterir. Böyle bir dizilim verildiğinde ve her clause'un elemanları sıralı olarak sunulduğunda, sağlanabilirliğin bir RAM (Rastgele Erişimli Makine) üzerinde $O(m + n)$ adımda kararlaştırılabileceğini göstereceğiz; burada $m$ clause sayısı ve $n$ değişken sayısıdır.
(Yeri gelmişken belirtelim ki, algoritmada bu karakterizasyona ihtiyaç duymasak da, iç içe geçmiş bir clause'lar kümesinin ağaçsı (tree-like) bir yapıya sahip olduğu gösterilebilir. Eğer tüm $\sigma \in C$ ve $\tau' \in C'$ için $\sigma \preceq \tau'$ ise $C \preceq C'$ yazalım. Ne $C$ ne de $C'$ diğerini ortalamıyorsa, $C$ ve $C'$ clause'larının her ikisi de aynı iki literalden oluşan clause'lar olmadığı sürece, ya $C \preceq C'$ ya da $C' \preceq C$ olması gerektiğini görmek kolaydır. Bu tür 2 elemanlı clause'lara denk diyelim. O halde iç içe geçmiş bir clause'lar kümesi şu koşulu sağlayacaktır:
$$(C \succ C'' \text{ ve } C' \succ C'') \text{ ise } (C \succ C' \text{ veya } C \equiv C' \text{ veya } C' \succ C),$$
çünkü $C \preceq C'$ olduğunda hem $C \succ C''$ hem de $C' \succ C''$ durumuna sahip olamayız. Bu, $\succ$ bağıntısının bir hiyerarşideki ata (ancestor) ilişkisi olduğu anlamına gelir.)
2. Bir algoritma.
$X$ alfabesinin $\bar{x} = -x$ olmak üzere $\{1, 2, \dots, n\}$ pozitif tam sayıları ile temsil edildiğini varsayalım. Clause'lar, iki dizide belirtilecektir:
lit[1..N], start[1..m+1]
burada her clause'un literalleri indeks arttıkça artan sıradadır. Clause'ların, $i < i'$ olduğunda $i$ clause'unun $i'$ clause'unu ortalamayacağı şekilde düzenlendiği varsayılır. Tüm clause'ların en az iki literal içerdiğini güvenle varsayabiliriz.
Aşağıdaki algoritmanın temel fikri, bir clause'un iç değişkenlerinin sonraki clause'larda yer almamasıdır. Bu nedenle, henüz iç değişken olarak görünmemiş ve dinamik olarak değişen tüm değişkenlerin kümesi hakkında
$$1 = x_1 < x_2 < \cdots < x_k = n$$
bilgi tutmamız yeterlidir. Başlangıçta $k = n$'dir.
Algoritma clause'ları sırayla ele alırken, şu ana kadar görülen tüm clause'ların kümesi kavramsal olarak
$$[x_1 \dots x_2], [x_2 \dots x_3], \dots, [x_{k-1} \dots x_k],$$
aralıklarına bölünebilir; öyle ki önceden işlenmiş her bir clause'un tüm literalleri bu aralıklardan birine aittir.
Mevcut aralıklar
next[1..n]
dizisinde tutulur; burada $1 \leq j < k$ için $next[x_j] = x_{j+1}$'dir.
Aşağıdaki algoritmadaki tek biraz karmaşık veri yapısı,
sat[0..n, boolean, boolean]
dizisidir ve şu şekilde yorumlanır: Eğer $[x_j \dots x_{j+1}]$ mevcut bölüntünün (partition) bir aralığı ise, o zaman her $s, t \in \{ \text{false}, \text{true} \}$ çifti için $sat[x_j, s, t]$ değeri 0 ya da 1 olacaktır. Bu değer ancak ve ancak $[x_j \dots x_{j+1}]$ aralığına ait olan ve halihazırda işlenmiş clause'lar, en küçük ve en büyük literalleri sırasıyla $x_j|s$ ve $x_{j+1}|t$ olan clause'lar tarafından sağlanabiliyorsa 1'dir; burada
$$x|s = \begin{cases} -x, & s = \text{false}; \\ +x, & s = \text{true}. \end{cases}$$
Görünüşe göre $sat$ dizisi, işlemeye devam etmek için gerekli tüm bilgileri içermektedir; çünkü iç değişkenler olarak görünmiş literaller sonraki clause'larda yer almayacaktır.
Algoritmanın ana görevi, yeni bir $C_i = \{\sigma_1, \dots, \sigma_q\}$ clause'unu incelerken $sat$ dizisini güncellemektir. $|\sigma_1| < \cdots < |\sigma_q|$ değişkenleri, mevcut bölüntü değişkenleri olan $x_1, \dots, x_k$'nin bir alt kümesi olacaktır. $|\sigma_1|$ ile $|\sigma_q|$ arasındaki tüm mevcut bölüntü değişkenleri, yeni clause'da yer alıp almadıklarına bakılmaksızın, bu tümcenin iç değişkenleridir (buradaki "tümce" kelimesi clause anlamındadır) ve dolayısıyla bölüntüden kaldırılacaklardır.
Farz edelim ki $|\sigma_1| = x_p$ olsun. Algoritma, $x$ değişkeninin $x_p, x_{p+1}, \dots, |\sigma_q|$ değerleri üzerinden geçmesini sağlayarak, $C_i$'nin iç değişkenleri bölüntüden çıkarıldığında $sat[x_p, s, t]$ değerlerini güncellemek için gereken bilgileri tutar. $C_i(x)$, $C_i$ clause'unun $x$'ten kesin olarak küçük olan literalleri olsun ve $C(x)$, $C_i$'den önce gelen ve literalleri $[x_p \dots x]$ aralığıyla sınırlı olan clause'lar olsun. Güncelleme işlemi, şu şekilde tanımlanan yardımcı $newsat_x[s, t]$ değerlerinin hesaplanmasıyla gerçekleştirilir:
$$newsat_x[s, t] = \begin{cases} 0, & C(x) \text{ sağlanabilir değilse}(s, t); \\ 1, & C(x) \text{ sağlanabilir}(s, t) \text{ ancak } C(x) \cup \{C_i(x)\} \text{ değilse}; \\ 2, & C(x) \cup \{C_i(x)\} \text{ sağlanabilirse}(s, t). \end{cases}$$
Burada "sağlanabilir$(s, t)$", verilen clause'lar kümesinin her bir clause'u ile boş olmayan bir kesişime sahip olan ve $x_p|s$ ile $x|t$ literallerini içeren bir clause'un var olduğu anlamına gelir.
Örneğin, $C_i = \{-1, 2, 4\}$ ve $\{x_1, x_2, x_3, x_4\} = \{1, 2, 3, 4\}$ olduğunu ve $C_1, \dots, C_{i-1}$ clause'larının aşağıdaki değerlere yol açtığını varsayalım:
s t sat[1,s,t] sat[2,s,t] sat[3,s,t]
false false 0 0 0
false true 1 1 0
true false 1 1 0
true true 1 0 1
Bu durumda şunları elde ederiz:
s t newsat_1[s,t] newsat_2[s,t] newsat_3[s,t] newsat_4[s,t]
false false 1 0 2 0
false true 0 2 0 0
true false 0 1 2 0
true true 1 1 1 1
ve dizileri $next[1] \leftarrow 4$ ve
$$sat[1, s, t] \leftarrow newsat_4[s, t] \text{ div } 2.$$
şeklinde güncellemek isteyeceğiz.
Eğer $C_i$ clause'u $\{-1, 2, 4\}$ yerine $\{-1, 2, -4\}$ olsaydı, $newsat$ hesaplaması aynı kalacaktı ancak $sat[1, s, t]$ değerlerinin tümü 0 olacaktı; bu durumda clause'lar sağlanamaz (unsatisfiable) olacaktı, çünkü $newsat_4[\text{true}, \text{true}]$ değeri 2 değil, yalnızca 1 olmaktadır. (Okuyucunun bu örneği dikkatle incelemesi önerilir, çünkü algoritmanın temelini oluşturan ana ilkeleri ortaya koymaktadır.)
3. Programlama detayları.
$C_m$ clause'undan sonra $\{0, n+1\}$ kukla (dummy) değişkenlerine sahip yapay bir $(m+1)$. clause'un eklendiğini varsaymak kolaylık sağlar. Bu nedenle, daha önce belirtilenden biraz daha büyük diziler tanımlayacağız:
lit[0..N+2], start[0..m+2]
İki yardımcı dizi $newsat[\text{boolean},\text{boolean}]$ ve $tmp[\text{boolean},\text{boolean}]$ olsun. İç içe geçmiş sağlanabilirlik problemine artık şu şekilde karar verebiliriz:
for x ← 0 to n do next[x] ← x + 1;
for x ← 0 to n do
for s ← false to true do for t ← false to true do sat[x, s, t] ← 1;
for i ← 1 to m + 1 do
begin l ← abs(lit[start[i]]); r = abs(lit[start[i + 1] - 1]);
⟨newsat tablosunu hesapla⟩;
next[l] ← r;
for s ← false to true do for t = false to true do
sat[l, s, t] ← newsat[s, t] div 2;
end;
if sat[0, true, true] = 1 then print('Sağlanabilir') else print('Sağlanamaz').
⟨newsat tablosunu hesapla⟩ makrosu şöyledir:
⟨newsat tablosunu hesapla⟩ =
j ← start[i]; sig ← lit[j]; x ← abs(sig);
newsat[false, false] ← 1; newsat[true, true] ← 1;
newsat[false, true] ← 0; newsat[true, false] ← 0;
while true do
begin if x = abs(sig) then
begin ⟨Mümkünse bir newsat değerini 1'den 2'ye yükselt⟩;
j ← j + 1; sig ← lit[j];
if j = start[i + 1] then goto done;
end;
⟨Bir sonraki x değeri için newsat'ı güncelle⟩;
x ← next[x];
end;
done:
Alt makrolar:
⟨Mümkünse bir newsat değerini 1'den 2'ye yükselt⟩ =
t ← (x = sig);
for s ← false to true do
if newsat[s, t] = 1 then newsat[s, t] ← 2.
⟨Bir sonraki x değeri için newsat'ı güncelle⟩ =
for s ← false to true do for t ← false to true do
tmp[s, t] ← max(newsat[s, false] * sat[x, false, t],
newsat[s, true] * sat[x, true, t]);
for s ← false to true do for t ← false to true do
newsat[s, t] ← tmp[s, t].
Önceki bölümdeki örnek, $newsat$ tablosunun genel olarak nasıl hesaplanabileceğini açıklamaktadır. Süreci biraz daha uzun çalıştırırız, böylece başarılı bir $newsat$ değeri sonda (1 değil) 2 olacaktır. ($\sigma_q$ değerinin incelenmesi gerekir.)
Çalışma süresi $O(m + n)$'dir; çünkü her $x$ değeri ya mevcut clause'daki ilk veya son değerdir (bu durum $2(m+1)$ vakaya karşılık gelir) ya da bölüntüden kalıcı olarak çıkarılmaktadır (sondaki $\{0, n+1\}$ kukla clause'u nedeniyle tam olarak $n$ vakada).
Verilen bir sağlanabilirlik probleminin, değişkenlerinin belirli bir sıralaması altında gerçekten iç içe geçmiş olup olmadığını test etmek için gerekebilecek süreyi burada ele almadık.
Sonuç değerlendirmeleri. İç içe geçmiş sağlanabilirlik için geliştirilen bu algoritma, temelde her clause'u yalnızca iki literal içeren bir clause'la değiştirerek çalışır ve bu değişimi gerekçelendirmek için "dinamik 2-SAT"ın özel bir formunu kullanır. Ancak ortaya çıkan 2-SAT durumları tamamen genel değildir. Bu durum, sağlanabilirlik probleminin biraz daha geniş bir özel durumunun da benzer tekniklerle doğrusal zamanda çözülebilir olduğunu düşündürmektedir.
Teşekkür. Lichtenstein teoremi hakkındaki bir sohbetimiz sırasında iç içe geçmiş sağlanabilirlik problemini ortaya atan Andrew Goldberg'e ve faydalı görüşleri için hakemlere teşekkürlerimi sunarım.
Kaynaklar
[1] Lichtenstein, D.: Planar Formulæ and Their Uses. SIAM J. Comput. 11, 329–343 (1982)
- Bilgisayar Bilimleri Bölümü, Stanford Üniversitesi; araştırma kısmen Ulusal Bilim Vakfı (National Science Foundation) CCR–8610181 nolu hibesi tarafından desteklenmiştir.