Bu çalışma, sabit genişlikli bit-vektör teorisine ait satisfiability modulo theory (SMT) problemlerini Grover algoritmasıyla çözmek için kuantum devre tabanlı bir yöntem geliştiriyor. Yöntem, klasik lazy-SMT yaklaşımındaki Boolean çözüm üretme ve teori tutarlılığı denetleme adımlarını ayrı ayrı tekrar etmek yerine, Boolean değişkenleri ile bit-vektör değişkenlerinin bütün olası değerlerini kuantum süperpozisyonunda temsil ediyor; SAT devresi, teori devresi, tutarlılık çıkarıcısı ve çözüm tersleyicisinden oluşan bir oracle ile geçerli SMT çözümlerini faz açısından işaretliyor ve Grover diffuser'ı bu çözümlerin ölçüm olasılığını yükseltiyor. Qiskit üzerinde gerçekleştirilen örnek değerlendirmede 32 qubitlik devre, beş Grover iterasyonu ve 1024 measurement shot kullanılarak altı doğru çözüm toplam 1017 kez ölçülmüş ve çözüm ölçme olasılığı %99,32 olarak raporlanmıştır. Çalışmanın temel sınırlılığı, değerlendirmenin küçük bir 2-bit örnek üzerinde simülasyonla yapılması ve modern klasik SMT çözücüleriyle gerçek çalışma süresi, gate maliyeti veya ölçeklenebilirlik benchmark'ı sunulmamasıdır.

Makalenin yeniliği yalnız Grover algoritmasını bir SMT problemine uygulamak değildir. Yazarlar, Grover oracle'ının SMT'nin iki ayrı mantıksal katmanını aynı devre içinde denetleyebilmesi için sistematik bir yapı önerir. Boolean soyutlama için bir SAT devresi, gerçek bit-vektör ifadelerini hesaplayan arithmetic/comparator devreleri, iki katmanın aynı doğruluk değerini üretip üretmediğini kontrol eden consistency extractor ve bütün koşulları sağlayan girdilere −1 fazı veren solution inverter birlikte çalışır.

“Bütün çözümleri aynı anda kontrol etmek” ifadesi dikkatli yorumlanmalıdır. Süperpozisyon sayesinde oracle bütün hesaplama-bazı girdilerini koherent biçimde değerlendirip geçerli durumları aynı kuantum işlemi içinde işaretleyebilir; ancak tek bir son ölçüm bütün çözümleri liste halinde çıktılamaz. Kaynağın kendi deneyinde altı farklı çözümü elde etmek için 1024 measurement shot kullanılmıştır.

SMT problemi SAT probleminden nasıl ayrılıyor?

Boolean satisfiability (SAT) probleminde değişkenler doğrudan doğru/yanlış değerleri alır. SMT ise Boolean mantığını belirli bir matematiksel teoriyle birleştirir. Bir atom, örneğin iki bit-vektörün eşitliği veya büyüklük ilişkisi olabilir.

Çalışma özellikle quantifier-free fixed-width bit-vector theory, kısaca \(\mathcal{BV}\), üzerinde yoğunlaşır. Bir bit-vektör ifadesi değişken, sabit veya iki ifadenin aritmetik işlemi olabilir. Çalışmada örneklenen işlem sınıfları arasında modulo toplama, modulo çarpma, bitwise işlemler, kaydırma ve word concatenation bulunur.

Atomlar ise iki ifadeyi

\[ <,\;>,\;=,\;\geq,\;\leq,\;\neq \]

karşılaştırıcılarından biriyle bağlar.

Klasik lazy SMT yaklaşımı nasıl çalışıyor?

Kaynağın Şekil 1'inde klasik lazy yaklaşım üç temel adıma ayrılır:

1. Özgün SMT formülü Boolean bir formüle soyutlanır.
2. SAT çözücüsü bu Boolean formül için bir atama bulur.
3. Theory solver, Boolean atamanın gerçek teori değişkenleriyle tutarlı olup olmadığını kontrol eder.

Atama teorik olarak tutarsızsa SAT çözücüsüne geri dönülür ve başka bir Boolean çözüm aranır.

Kaynak ilk örnekte

\[ F= [(a>b)\vee(ab)\vee\neg(a

formülünü kullanır.

Boolean değişkenleri

\[ x:(a>b),\qquad y:(a

olarak tanımlandığında soyut formül

\[ F_B= (x\vee y\vee z) \wedge (\neg x\vee\neg y\vee\neg z) \]

olur.

Şekil 1'de SAT çözücüsünün ilk üç Boolean ataması theory solver tarafından reddedilir ve ancak dördüncü iterasyonda tutarlı çözüm bulunur. Yazarların kuantum yaklaşımına yönelmesinin temel motivasyonu bu Boolean–teori geri dönüş döngüsüdür.

Kuantum yaklaşımındaki temel fikir nedir?

İki adet 2-bit değişken

\[ a=a_1a_2, \qquad b=b_1b_2 \]

ve üç Boolean soyut değişken \(x,y,z\) birlikte

\[ |v\rangle = |x,y,z,a_1,a_2,b_1,b_2\rangle \]

durumuyla temsil edilir.

Bu yedi giriş biti için \(2^7=128\) olası hesaplama-bazı girdisi vardır. İlk örnekte oracle bütün bu olası girdilerin süperpozisyonu üzerinde çalışır.

Bir girişin çözüm olabilmesi için önce Boolean formülü sağlaması gerekir:

\[ F_B(x,y,z) = (x\vee y\vee z) \wedge (\neg x\vee\neg y\vee\neg z) = 1. \]

Buna ek olarak Boolean soyut değişkenlerinin bit-vektör teorisindeki gerçek karşılıklarıyla tutarlı olması gerekir:

\[ (x=1\Longleftrightarrow a_1a_2>b_1b_2) \vee (x=0\Longleftrightarrow a_1a_2\not>b_1b_2), \]

\[ (y=1\Longleftrightarrow a_1a_2

\[ (z=1\Longleftrightarrow a_1a_2=b_1b_2) \vee (z=0\Longleftrightarrow a_1a_2\neq b_1b_2). \]

Oracle geçerli çözümleri nasıl işaretliyor?

Önerilen oracle \(\Psi\), bütün Boolean ve teori koşullarını sağlayan bir girişin fazını ters çevirir:

\[ \Psi(|v\rangle) = \begin{cases} -|v\rangle, & \text{Boolean formül ve bütün teori-tutarlılık koşulları sağlanıyorsa},\\ |v\rangle, & \text{aksi durumda}. \end{cases} \]

Bu −1 faz işareti, Grover diffuser'ının hangi baz durumlarının ölçüm genliğini yükselteceğini belirler.

Kaynağın Şekil 2'sindeki ilk örnekte oracle, 128 olası girdinin içindeki 16 geçerli SMT çözümünü aynı oracle uygulamasında faz açısından işaretleyebilmektedir.

Grover algoritması çözüm olasılığını nasıl büyütüyor?

Grover algoritmasında iki işlem tekrarlanır:

• Oracle hedef durumların fazını ters çevirir.
• Diffuser genlikleri ortalama etrafında tersleyerek işaretlenmiş durumların ölçüm olasılığını büyütür.

Tek hedef bulunan \(N\) elemanlı ideal bir aramada kaynak

\[ O(\sqrt{N}) \]

Grover işlemini klasik

\[ O(N) \]

aramaya karşı kuadratik hızlanma olarak verir.

\(M\) hedef bulunduğunda optimum iterasyon sayısı yaklaşık

\[ \frac{\pi}{4} \sqrt{\frac{N}{M}} \]

olur.

Kaynak ayrıca \(M\)'nin önceden bilinmeyebileceğine dikkat çeker ve bu durumda quantum counting kullanılabileceğini belirtir. Ancak çalışmanın Qiskit değerlendirmesinde gerekli ek qubitler bulunmadığı için quantum counting fiilen uygulanmamıştır.

Bu “kuadratik hızlanma” ne kadar güçlü bir sonuç?

Kaynak sonuç bölümünde yöntemin geleneksel yönteme göre teorik kuadratik hızlanma sunduğunu belirtmektedir. Bu ifade Grover'ın arama karmaşıklığı bağlamındadır.

Çalışma, modern endüstriyel SMT çözücülerine karşı gerçek duvar-saati benchmark'ı gerçekleştirmemektedir. Ayrıca oracle'ın içindeki SAT, arithmetic, comparator, consistency ve uncomputation devrelerinin gate/depth maliyetlerinin problem büyüklüğüyle nasıl ölçeklendiğine ilişkin kapsamlı bir uçtan uca karmaşıklık analizi verilmemektedir.

Bu nedenle sonuç “gerçek bir kuantum bilgisayarda bütün klasik SMT çözücülerinden kuadratik olarak daha hızlı çalışacağı deneysel olarak gösterildi” biçiminde yorumlanmamalıdır.

Oracle'ın dört temel bileşeni

SAT devresi nasıl oluşturuluyor?

Yazarlar SAT tarafını 3-SAT conjunctive normal form için yapıcı biçimde tanımlar:

\[ F ::= C\mid F_1\wedge F_2, \]

\[ C ::= l_1\vee l_2\vee l_3, \]

\[ l ::= v\mid\neg v\mid0. \]

Şekil 6, tek bir üç-literal clause için kullanılan devreyi gösterir. Literal pozitif olduğunda veya sabit 0 olduğunda \(Q\) kapısı \(X\); literal negatif olduğunda \(Q\) kapısı identity \(I\) olarak seçilir.

Clause içindeki ara hesaplama için bir ancilla qubit, clause'un doğruluk değeri için ayrı bir output qubit kullanılır.

Theorem 1: Clause devresinin doğruluğu

Theorem 1 üç özelliği kanıtlar:

\[ q'_o(C)=1 \Longleftrightarrow C\text{ doğrudur}, \]

\[ q'_a(C)=0, \]

ve bütün giriş literal bitleri devre sonunda başlangıç değerlerine geri döner:

\[ v'_i=v_i. \]

İkinci ve üçüncü özellikler kuantum devresinin geri döndürülebilir olması ve ancilla'ların sonraki işlemlerde yeniden kullanılabilmesi açısından önemlidir.

Theorem 2: Tam 3-SAT formülünün doğruluğu

Şekil 7'de iki alt formülün output qubitleri bir CCNOT kapısında birleştirilerek

\[ F=F_1\wedge F_2 \]

hesaplanır.

Theorem 2, yapısal tümevarımla bu inşanın keyfi 3-SAT CNF formülü için

\[ q'_o(F)=1 \Longleftrightarrow F\text{ doğrudur} \]

özelliğini koruduğunu gösterir.

Theory Circuit neyi hesaplıyor?

Bit-vector theory tarafında her atom

\[ E_1\mathrel{\rhd}E_2 \]

biçimindedir.

Önce gerekli aritmetik işlemler hesaplanır. Ardından comparator devresi iki bit-string arasındaki ilişkiyi iki output bitiyle kodlar:

\[ (O_1,O_2) = \begin{cases} (0,1), & E_1E_2,\\ (0,0), & E_1=E_2. \end{cases} \]

Kaynak comparator tasarımında \((1,1)\) durumunun oluşmadığını belirtir.

Bu iki output biti üzerinden altı karşılaştırma türü için ayrı atom devreleri kurulur:

\[ >,\;<,\;=,\;\geq,\;\leq,\;\neq. \]

Theorem 3: Atom devresinin doğruluğu

Theorem 3'ün sonucu doğrudan şöyledir:

\[ atom=1 \Longleftrightarrow (E_1\mathrel{\rhd}E_2)=1. \]

Yazarlar ispatın primitive quantum gate truth table'larının incelenmesiyle doğrudan elde edildiğini belirterek sayfa sınırı nedeniyle ayrıntılı ispatı vermemektedir.

Theory Circuit bütün bit-vektör işlemlerini eksiksiz gerçekleştiriyor mu?

Çalışma genel BV sözdiziminde farklı arithmetic operation türlerinin bulunabileceğini belirtir; ancak bütün aritmetik devrelerinin ayrıntılı gate düzeyi tasarımını bu makalede üretmez.

Aritmetik işlem bloğu Şekil 8(a)'da genel bir modül olarak gösterilir. Yazarlar gerekli işlemlerin primitive gate'lerden oluşturulabileceğini veya önceki çalışmalardaki quantum arithmetic devrelerinin kullanılabileceğini belirtmektedir.

Dolayısıyla makale, bütün BV operatörleri için baştan sona optimize edilmiş üretim seviyesi bir quantum-SMT software stack sunmaz. Katkısı daha çok SAT ve theory modüllerini tek Grover oracle mimarisinde nasıl bağlayacağını sistematik hale getirmektir.

Consistency Extractor neden gerekli?

Boolean soyutlama kendi başına yeterli değildir. Örneğin Boolean değişkeni bir atomu “doğru” olarak seçebilirken bit-vektör devresi gerçek değerler için aynı atomun yanlış olduğunu bulabilir.

Bu nedenle her Boolean abstract variable \(v_{B_i}\) ile gerçek atom sonucu \(atom_i\) karşılaştırılır.

Şekil 10(a)'daki devre bir CNOT ve ardından \(X\) kapısı kullanır. Theorem 4:

\[ v'_{B_i}=1 \Longleftrightarrow v_{B_i}\equiv atom_i. \]

Böylece yalnız Boolean formülü sağlamak yetmez; bütün Boolean atomların theory-domain anlamlarıyla da tutarlı olması gerekir.

Solution Inverter ne yapıyor?

Şekil 10(b)'deki Solution Inverter, bütün consistency bitleri ve SAT output biti 1 olduğunda \(q_{\mathrm{SMT}}\) qubitini aktif hale getirir.

Theorem 5'in ilk koşulu:

\[ q'_{\mathrm{SMT}}=1 \]

ancak ve ancak

\[ q'_o(F_B)=1 \]

ve bütün \(i\)'ler için

\[ v_{B_i}\equiv atom_i \]

olduğunda sağlanır.

Ardından \(Z\) kapısı

\[ Z|1\rangle=-|1\rangle \]

özelliğiyle tam çözüm durumlarına −1 fazı verir.

Reverse Circuit neden var?

Oracle'ın ara hesaplamaları çok sayıda ancilla ve output qubit üzerinde geçici bilgi üretir. Bunlar temizlenmezse sonraki Grover iterasyonunda girişle dolaşık kalabilir ve diffuser'ın beklediği yapı bozulabilir.

Bu nedenle SAT, theory, consistency ve solution-inverter hesaplarının ilgili bölümleri ters sırada uygulanarak ara qubitler başlangıç durumlarına geri döndürülür.

Bu işlem quantum computing'deki uncomputation prensibinin makaledeki karşılığıdır.

Değerlendirmede hangi SMT formülü kullanılıyor?

Yazarlar ikinci, daha devre-odaklı örnekte Boolean formülünü

\[ F_B= (x\vee y\vee z) \wedge (x\vee\neg y\vee z) \]

olarak seçer.

Atomlar:

\[ x:(a+b

\[ y:(a+b>a\oplus b), \]

\[ z:(a+b=1) \]

şeklindedir.

Burada \(+\) fixed-width modulo-sum, \(\oplus\) ise bitwise exclusive-OR işlemidir.

Kaynak içindeki “c değişkeni” tutarsızlığı

Değerlendirme metni “\(a,b,c\) değişkenlerinin tümü 2-bit” ifadesini kullanmaktadır. Ancak hemen ardından verilen atomların tamamında yalnız \(a\) ve \(b\) bulunur.

Şekil 11'deki ana SMT girişleri de yalnız

\[ a,\;b \]

bitlerini içerir ve Tablo II yalnız bu iki değişken için değer verir.

Bu nedenle kaynakta adı geçen \(c\)'nin değerlendirme devresinde gerçek bir rolü olduğu doğrulanamamaktadır. Verianla metni bunu kaynak-içi bir isimlendirme/metin tutarsızlığı olarak korur.

32 qubit nereye harcanıyor?

Kaynağın Tablo I'i değerlendirme devresindeki qubit kullanımını ayrıntılı biçimde verir:

Toplam:

\[ 3+4+5+1+1+1+2+3+2+4+4+2 = 32\text{ qubit}. \]

Küçük bir 2-bit SMT örneğinin bile 32 qubit kullanması, çalışmanın pratik ölçeklenebilirlik açısından önemli sınırlılıklarından biridir.

Şekil 11 neyi gösteriyor?

Şekil 11(a), değerlendirilen bütün devreyi tek blok diyagramda gösterir. Başlangıçta Boolean abstract variables ile \(a,b\) SMT değişkenleri Hadamard kapılarıyla süperpozisyona alınır.

SAT circuit ve theory circuit şekil üzerinde ardışık görünse de yazarlar aralarında veri bağımlılığı olmadığı için gerçek uygulamada paralel çalışabileceklerini belirtir.

Theory bölümünde:

• modulo adder,
• bitwise XOR,
• \((a+b)\) ile \((a\oplus b)\)'yi karşılaştıran comparator,
• \((a+b)\) ile 1'i karşılaştıran ikinci comparator

yer alır.

Ardından consistency extractor, reverse circuit ve Grover diffusion circuit gelir.

Neden quantum counting kullanılmadı?

Grover iterasyonlarının optimum sayısı hedef çözüm sayısı \(M\)'ye bağlıdır. Normalde yazarların önerdiği yöntem quantum counting ile \(M\)'yi yaklaşık olarak belirlemektir.

Ancak değerlendirme devresi zaten 32 qubit kullanmaktadır ve kaynakta kullanılan Qiskit ortamının 32-qubit sınırına ulaştığı belirtilir. Bu nedenle quantum counting devresi eklenememiştir.

Araştırmacılar bunun yerine bir Grover iterasyonundan başlayıp iterasyon sayısını artırmış ve ölçüm dağılımının kötüleşmeye başladığı dönüş noktasını aramıştır.

Bu deney için optimum nokta 5 Grover iterasyonu olarak bulunmuştur. Yazarlar daha sonra çözüm uzayını klasik olarak elle enumerate ederek bu değerin Grover'ın teorik iterasyon hesabıyla uyumlu olduğunu belirtir.

Bu yöntem gösterim deneyi için kullanılabilir olmakla birlikte, çözüm sayısının önceden bilinmediği büyük gerçek SMT problemlerinde kendi başına genel bir çözüm değildir.

Simülasyonun ana sonucu

Beş Grover iterasyonundan sonra devre 1024 kez ölçülmüştür. Kaynağın Tablo II'si altı çözümü şu şekilde raporlar:

Bu altı çözümün toplam ölçüm sayısı

\[ 174+158+183+156+164+182 = 1017 \]

olduğundan kaynak

\[ \frac{1017}{1024} \approx 0.9932 \]

sonucunu verir ve çözüm ölçme olasılığını %99,32 olarak raporlar.

“Bütün çözümleri buluyor” ifadesi nasıl yorumlanmalı?

Oracle'ın önemli avantajı bütün geçerli baz durumlarını aynı süperpozisyon üzerinde faz bakımından işaretleyebilmesidir.

Fakat kuantum ölçümünde tek shot yalnız tek classical bit-string verir. Dolayısıyla “oracle 16 veya 6 çözümü aynı anda tanıyor” ile “kullanıcı tek ölçümde bütün çözüm listesini alıyor” aynı şey değildir.

Kaynağın deneysel yöntemi de bunu doğrular: altı farklı çözüm, 1024 tekrar ölçümü içinde örneklenmektedir.

Şekillerin bilimsel rolü

Çalışmanın desteklediği sonuçlar

• Fixed-width bit-vector SMT problemleri için Grover tabanlı bir quantum oracle mimarisi kurulabilir.
• Boolean SAT koşulları ve bit-vector theory koşulları aynı oracle içinde birlikte değerlendirilebilir.
• 3-SAT CNF formülleri için clause ve formula devreleri yapıcı biçimde oluşturulabilir.
• Clause ve formula devrelerinin doğruluğu Theorem 1 ve Theorem 2 ile gösterilmiştir.
• Comparator çıktılarından altı temel bit-vector karşılaştırması için atom devreleri oluşturulabilir.
• Consistency Extractor, Boolean atom ile theory-domain atomının aynı doğruluk değerine sahip olup olmadığını doğru biçimde belirler.
• Solution Inverter, bütün Boolean ve theory koşullarını sağlayan durumlara −1 fazı verir.
• Reverse circuit ara qubitleri temizleyerek oracle'ın Grover iterasyonlarında yeniden kullanılmasını sağlar.
• Qiskit simülasyonundaki örnek 32 qubitlik devrede altı doğru SMT çözümü yüksek ölçüm olasılığına yükseltilmiştir.
• Beş Grover iterasyonu ve 1024 shot sonunda altı çözüm toplam 1017 kez ölçülmüş ve kaynak %99,32 çözüm ölçme olasılığı raporlamıştır.
• Grover araması açısından çözüm aramasının teorik arama karmaşıklığı klasik doğrusal taramaya göre karekök ölçeğine indirilebilir.

Çalışmanın desteklemediği veya test etmediği sonuçlar

• Çalışma gerçek bir kuantum işlemci üzerinde SMT çözümü gerçekleştirmemiştir; değerlendirme Qiskit simülasyonudur.
• %99,32 sonucu genel SMT problemleri için başarı oranı değildir; yalnız makaledeki belirli küçük örneğin 1024-shot simülasyonuna aittir.
• Tek bir quantum measurement bütün SMT çözümlerini liste olarak döndürmez.
• Gerçek çalışma süresinde modern classical SMT solver'lara karşı kuadratik hızlanma deneysel olarak gösterilmemiştir.
• Oracle içindeki SAT, arithmetic, comparator ve uncomputation maliyetlerinin büyüyen gerçek problemler üzerindeki toplam gate/depth ölçeklenebilirliği kapsamlı benchmark ile incelenmemiştir.
• Bütün bit-vector arithmetic operatörleri için optimize edilmiş gate-düzeyi devre tasarımı makalede verilmemektedir.
• Quantum counting değerlendirme devresine uygulanmamış; gerekli Grover iterasyon sayısı küçük örnekte deneysel tarama ve klasik enumeration ile belirlenmiştir.
• 32 qubitlik küçük örnekten büyük endüstriyel formal-verification problemlerinin uygulanabilir olduğu sonucu çıkarılamaz.
• Yöntemin başka SMT teorilerine genişletilebileceği gelecek çalışma önerisidir; makale bu teoriler için çalışan oracle'ları göstermemektedir.

Türkiye açısından nasıl okunmalı?

Kaynak Türkiye'ye özgü deneysel veya sektörel veri içermemektedir. Türkiye açısından çalışma daha çok kuantum yazılımı, formal verification, donanım doğrulama ve EDA araştırmaları için metodolojik bir örnek olarak değerlendirilebilir.

Özellikle bit-vector SMT, işlemci ve dijital devre doğrulama problemlerinde sık kullanılan matematiksel yapılardan biridir. Ancak bu çalışmadan Türkiye'deki mevcut kuantum donanımının SMT çözmek için hazır olduğu veya klasik doğrulama araçlarının yakın vadede yerini alacağı sonucu çıkarılamaz.

Çalışmanın Yöntemi ve Bulguları

Araştırmanın türü

Çalışma teorik bilgisayar bilimi ve kuantum hesaplama araştırmasıdır. Yöntem, kuantum devre sentezi, matematiksel doğruluk ispatları ve state-vector/circuit simulation yaklaşımını birleştirir.

Yeni fiziksel deney, gerçek quantum processing unit benchmark'ı veya endüstriyel SMT benchmark suite kullanılmamıştır.

Yöntemsel zincir

Doğruluk ispatları

Çalışma oracle mimarisini yalnız simülasyon sonucuyla savunmaz; beş ayrı doğruluk sonucu verir.

Değerlendirme devresi

Değerlendirmede iki adet 2-bit SMT değişkeni ve üç Boolean abstract variable kullanılır. Theory circuit için modulo adder, bitwise XOR ve iki comparator gerekir.

Makalenin Table I hesabına göre toplam qubit gereksinimi 32'dir.

Şekil 11(a), SAT ile theory circuit'in devre çiziminde ardışık görünmelerine rağmen birbirlerine veri bağımlılığı olmadığı için paralel yürütülebileceğini belirtir.

Grover iterasyonlarının belirlenmesi

Kaynak, hedef sayısının bilinmesi halinde Grover iterasyon sayısını

\[ r\approx \frac{\pi}{4} \sqrt{\frac{N}{M}} \]

ile ilişkilendirir.

Değerlendirmede quantum counting için yeterli ek qubit kalmadığından, yazarlar iterasyon sayısını 1'den artırarak measurement dağılımının bozulduğu dönüş noktasını tespit etmiş ve 5 iterasyonda karar kılmıştır.

Çözüm uzayının manuel enumeration'ı daha sonra bu seçimle uyumlu bulunmuştur.

Ölçüm sonucu

1024 shot içindeki altı geçerli çözümün counts değerleri:

\[ 174,\;158,\;183,\;156,\;164,\;182 \]

olarak raporlanmıştır.

En yüksek count:

\[ 183 \]

ile `0010001`, en düşük count ise

\[ 156 \]

ile `1001101` çözümüdür.

Ancak bu küçük count farkları yöntemler veya çözümler arasında kalite farkı anlamına gelmez. Grover amplification ideal olarak bütün hedeflerin genliklerini yükseltir ve sonlu-shot sampling doğal istatistiksel dağılım üretir. Kaynak bu altı çözüm arasında istatistiksel üstünlük iddiasında bulunmamaktadır.

Çalışmanın en güçlü tarafı

Çalışmanın en güçlü yönü, klasik SMT'nin SAT ve theory bölümlerini Grover oracle'a aktarabilmek için açık bir modüler mimari tanımlamasıdır.

Özellikle consistency extractor, SMT'nin Boolean soyutlamasının kuantum devrede yalnız “SAT çözümü bulma” problemine indirgenmesini önler. Theory-domain doğruluk değerleri de aynı oracle'ın hedef koşuluna dahil edilir.

Çalışmanın başlıca sınırlılıkları

Birinci sınırlılık ölçektir. Yalnız iki 2-bit SMT değişkeni kullanılan örnek devre 32 qubit gerektirmektedir. Daha büyük bit genişliklerinde arithmetic ve comparator modülleri hızla ek kaynak gerektirebilir.

İkinci sınırlılık değerlendirme yöntemidir. Gerçek quantum hardware kullanılmadığından gate noise, decoherence, connectivity, routing ve error-correction maliyetleri modellenmemiştir.

Üçüncü sınırlılık, theoretical quadratic speedup'ın uçtan uca solver benchmark'ına dönüştürülmemiş olmasıdır. Grover oracle çağrı sayısı square-root avantajı sunarken oracle'ın kendi gate maliyeti ihmal edilemez.

Dördüncü sınırlılık, hedef çözüm sayısının bilinmemesi problemidir. Kaynak quantum counting'i çözüm olarak işaret eder fakat 32-qubit limit nedeniyle kendi deneyinde uygulamaz.

Beşinci sınırlılık, makalenin yalnız quantifier-free fixed-width BV teorisine odaklanması ve SAT tarafında 3-SAT CNF devre yapısını ayrıntılı olarak geliştirmesidir. Diğer SMT teorileri gelecekteki çalışma olarak bırakılmıştır.

Kaynak ve Yöntem Notu

Tam özgün çalışma adı: A Quantum SMT Solver for Bit-Vector Theory

Yazarlar: Shang-Wei Lin; Si-Han Chen; Tzu-Fan Wang; Yean-Ru Chen.

Yazar sırası: Yüklenen kaynakta verilen sıra aynen korunmuştur.

Eş katkı: Kaynakta eş katkı veya eş birinci yazarlık beyanı bulunmamaktadır.

Sorumlu yazar: Kaynakta resmî corresponding-author işareti bulunmamaktadır. Shang-Wei Lin ve Yean-Ru Chen için iletişim e-posta adresleri verilmiştir.

Kurumlar: Shang-Wei Lin — Nanyang Technological University, Singapore. Si-Han Chen, Tzu-Fan Wang ve Yean-Ru Chen — National Cheng Kung University, Taiwan.

Bilimsel alan: Logic in Computer Science, quantum computing, formal verification, satisfiability modulo theories ve fixed-width bit-vector solving.

İncelenen kaynak: arXiv:2303.09353v1 [cs.LO].

İlk ve incelenen arXiv sürümü: v1, 16 Mart 2023.

arXiv-issued DOI: 10.48550/arXiv.2303.09353.

Hakemlik/yayın durumu: İncelenen dosya arXiv repository/preprint sürümüdür ve dosyanın kendi üzerinde hakemli dergi veya konferans yayın kaydı bulunmamaktadır. Bu nedenle yüklenen v1, hakemli version of record olarak değerlendirilmemiştir.

Aynı başlıklı 2026 kayıt hakkında bibliyografik not: 2026 International Conference on Quantum Communications, Networking, and Computing kayıtlarında aynı başlıkla bir konferans makalesi bulunmaktadır; ancak yazar listesi Shang-Wei Lin, Si-Han Chen, Lei-Han Yao, Yu-Chung Chen ve Yean-Ru Chen şeklindedir. Yüklenen v1'de ise Tzu-Fan Wang bulunmaktadır ve Lei-Han Yao ile Yu-Chung Chen bulunmamaktadır. Resmî kaynaklarda iki kayıt arasındaki sürüm ilişkisi açıkça doğrulanmadığından 2026 konferans çalışması bu Verianla makalesinde yüklenen v1'in hakemli sürümü olarak kullanılmamıştır.

Lisans: arXiv kaydı Creative Commons Attribution 4.0 International (CC BY 4.0) lisansına yönlendirmektedir.

Finansman: Yüklenen kaynakta ayrı bir finansman veya grant beyanı bulunmamaktadır.

Veri erişilebilirliği: Ayrı bir data-availability beyanı bulunmamaktadır. Araştırma deneysel veri setine değil, kuramsal devre tasarımı ve Qiskit simülasyonuna dayanmaktadır.

Çıkar çatışması: Yüklenen kaynakta ayrı bir conflict-of-interest beyanı bulunmamaktadır; bundan çıkar çatışması olmadığı şeklinde ek sonuç çıkarılmamıştır.

Yazar katkıları: Kaynakta CRediT veya ayrıntılı author-contributions beyanı bulunmamaktadır.

Kaynak-içi tutarsızlık: Metin formülün/değerlendirme örneğinin \(a,b,c\) adlı üç 2-bit değişken içerdiğini belirtmektedir; ancak gösterilen atomlar, devre girişleri ve çözüm tablosu yalnız \(a\) ve \(b\)'yi kullanmaktadır. \(c\)'nin değerlendirmedeki işlevi kaynakta gösterilmediğinden Verianla metni bunu sessizce tamamlamamıştır.

Araştırma yöntemi: Grover search; quantum oracle construction; 3-SAT circuit synthesis; reversible CCNOT/CNOT/X/Z/H gate yapıları; quantum arithmetic; quantum comparator; Boolean–theory consistency extraction; phase inversion; uncomputation/reverse circuit ve Qiskit simulation.

Değerlendirme koşulu: Makaledeki ana Qiskit örneği 32 qubit, beş Grover iterasyonu ve 1024 measurement shot kullanmaktadır. Altı geçerli çözümün toplam count değeri 1017 olup kaynak %99,32 solution-measurement probability raporlamaktadır.

Yöntemsel sınır: Çalışmanın teorik kuadratik hızlanma ifadesi Grover search complexity bağlamındadır. Kaynak, gerçek quantum hardware üzerinde modern classical SMT solver'larla uçtan uca runtime karşılaştırması yapmamaktadır.

Bilimsel içerik sınırı: Bu Verianla makalesindeki algoritma mimarisi, formüller, teoremler, devre bileşenleri, qubit kaynak tablosu ve simülasyon sonuçları yüklenen yedi sayfalık arXiv:2303.09353v1 dosyasına dayanmıştır. Haricî kaynaklar yalnız arXiv kimliği, lisans ve aynı başlıklı 2026 konferans kaydının bibliyografik durumunu kontrol etmek amacıyla kullanılmıştır; yüklenen kaynakta bulunmayan bilimsel performans sonucu eklenmemiştir.

Verianla Live notu: Kaynağın Tablo II'sindeki altı çözümün measurement counts değerleri doğrudan aynı simülasyon koşulundan geldiği için `vlive-bar` kullanılmıştır. Kaynakta klasik ve kuantum SMT çözücüleri arasında gerçek runtime benchmark'ı bulunmadığından teorik hızlanma iddiası için yapay performans grafiği oluşturulmamıştır.