Bu tədqiqat sabit enli bit-vektor nəzəriyyəsinə aid satisfiability modulo theory (SMT) problemlərini Grover alqoritmi ilə həll etmək üçün kvant dövrə əsaslı metod hazırlayır. Metod klassik lazy-SMT yanaşmasında Boolean həllinin yaradılması və nəzəriyyə uyğunluğunun yoxlanılması addımlarını ayrı-ayrılıqda təkrar etmək əvəzinə, Boolean dəyişənləri ilə bit-vektor dəyişənlərinin bütün mümkün qiymətlərini kvant superpozisiyasında təmsil edir; SAT dövrəsi, nəzəriyyə dövrəsi, uyğunluq çıxarıcısı və həll inversiyasından ibarət oracle ilə etibarlı SMT həllərini faza görə işarələyir və Grover diffuser-i bu həllərin ölçülmə ehtimalını artırır. Qiskit üzərində aparılan nümunə qiymətləndirmədə 32 qubitlik dövrə, beş Grover iterasiyası və 1024 measurement shot istifadə edilərək altı düzgün həll ümumilikdə 1017 dəfə ölçülmüş və həll ölçmə ehtimalı %99,32 kimi bildirilmişdir. Tədqiqatın əsas məhdudiyyəti qiymətləndirmənin kiçik 2-bit nümunə üzərində simulyasiya ilə aparılması və müasir klassik SMT həll ediciləri ilə real işləmə müddəti, gate xərci və ya miqyaslana bilmə benchmark-ının təqdim edilməməsidir.
Məqalənin yeniliyi yalnız Grover alqoritmini bir SMT probleminə tətbiq etmək deyil. Müəlliflər Grover oracle-ının SMT-nin iki ayrı məntiqi qatını eyni dövrədə yoxlaya bilməsi üçün sistematik bir quruluş təklif edirlər. Boolean abstraksiyası üçün SAT dövrəsi, real bit-vektor ifadələrini hesablayan arithmetic/comparator dövrələri, iki qatın eyni həqiqət qiymətini yaradıb-yaratmadığını yoxlayan consistency extractor və bütün şərtləri ödəyən girişlərə −1 faza verən solution inverter birlikdə işləyir.
“Bütün həlləri eyni anda yoxlamaq” ifadəsi diqqətlə şərh edilməlidir. Superpozisiya sayəsində oracle bütün hesablama-baza girişlərini koherent şəkildə qiymətləndirib etibarlı vəziyyətləri eyni kvant əməliyyatı daxilində işarələyə bilər; lakin tək bir son ölçmə bütün həlləri siyahı şəklində çıxarmır. Mənbənin öz təcrübəsində altı fərqli həlli əldə etmək üçün 1024 measurement shot istifadə edilmişdir.
SMT problemi SAT problemindən necə fərqlənir?
Boolean satisfiability (SAT) problemində dəyişənlər birbaşa doğru/yanlış qiymətləri alır. SMT isə Boolean məntiqini müəyyən bir riyazi nəzəriyyə ilə birləşdirir. Bir atom, məsələn iki bit-vektorun bərabərliyi və ya böyüklük münasibəti ola bilər.
Tədqiqat xüsusilə quantifier-free fixed-width bit-vector theory, qısaca \(\mathcal{BV}\), üzərində cəmlənir. Bit-vektor ifadəsi dəyişən, sabit və ya iki ifadənin arifmetik əməliyyatı ola bilər. Tədqiqatda nümunələnən əməliyyat sinifləri arasında modulo toplama, modulo vurma, bitwise əməliyyatlar, sürüşdürmə və word concatenation mövcuddur.
Atomlar isə iki ifadəni
\[ <,\;>,\;=,\;\geq,\;\leq,\;\neq \]
müqayisəçilərindən biri ilə bağlayır.
Klassik lazy SMT yanaşması necə işləyir?
Mənbənin Şəkil 1-ində klassik lazy yanaşması üç əsas addıma ayrılır:
- Orijinal SMT formulu Boolean formuluna abstraksiya edilir.
- SAT həll edicisi bu Boolean formul üçün bir təyinat tapır.
- Theory solver Boolean təyinatının real nəzəriyyə dəyişənləri ilə uyğun olub-olmadığını yoxlayır.
Təyinat nəzəri baxımdan uyğunsuzdursa SAT həll edicisinə geri qayıdılır və başqa Boolean həlli axtarılır.
Mənbə ilk nümunədə
\[ F= [(a>b)\vee(ab)\vee\neg(a
formulundan istifadə edir.
Boolean dəyişənləri
\[ x:(a>b),\qquad y:(a
kimi təyin edildikdə abstrakt formul
\[ F_B= (x\vee y\vee z) \wedge (\neg x\vee\neg y\vee\neg z) \]
olur.
Şəkil 1-də SAT həll edicisinin ilk üç Boolean təyinatı theory solver tərəfindən rədd edilir və yalnız dördüncü iterasiyada uyğun həll tapılır. Müəlliflərin kvant yanaşmasına yönəlməsinin əsas motivasiyası bu Boolean–nəzəriyyə geri dönüş dövrəsidir.
Kvant yanaşmasındakı əsas fikir nədir?
İki ədəd 2-bit dəyişən
\[ a=a_1a_2, \qquad b=b_1b_2 \]
və üç Boolean abstrakt dəyişəni \(x,y,z\) birlikdə
\[ |v\rangle = |x,y,z,a_1,a_2,b_1,b_2\rangle \]
vəziyyəti ilə təmsil olunur.
Bu yeddi giriş biti üçün \(2^7=128\) mümkün hesablama-baza girişi vardır. İlk nümunədə oracle bütün bu mümkün girişlərin superpozisiyası üzərində işləyir.
Bir girişin həll ola bilməsi üçün əvvəlcə Boolean formulunu ödəməsi lazımdır:
\[ F_B(x,y,z) = (x\vee y\vee z) \wedge (\neg x\vee\neg y\vee\neg z) = 1. \]
Bundan əlavə Boolean abstrakt dəyişənlərin bit-vektor nəzəriyyəsindəki real qarşılıqları ilə uyğun olması tələb olunur:
\[ (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 etibarlı həlləri necə işarələyir?
Təklif edilən oracle \(\Psi\), bütün Boolean və nəzəriyyə şərtlərini ödəyən girişin fazasını tərsinə çevirir:
\[ \Psi(|v\rangle) = \begin{cases} -|v\rangle, & \text{Boolean formul və bütün nəzəriyyə-uyğunluq şərtləri ödənirsə},\\ |v\rangle, & \text{əks halda}. \end{cases} \]
Bu −1 faza işarəsi Grover diffuser-in hansı baza vəziyyətlərinin ölçmə amplitudasını artıracağını müəyyən edir.
Mənbənin Şəkil 2-sindəki ilk nümunədə oracle, 128 mümkün giriş içindəki 16 etibarlı SMT həllini eyni oracle tətbiqində faza baxımından işarələyə bilir.
Grover alqoritmi həll ehtimalını necə artırır?
Grover alqoritmində iki əməliyyat təkrarlanır:
- Oracle hədəf vəziyyətlərin fazasını tərsinə çevirir.
- Diffuser amplitudaları orta qiymət ətrafında tərsinə çevirərək işarələnmiş vəziyyətlərin ölçmə ehtimalını artırır.
Bir hədəfin olduğu \(N\) elementli ideal axtarışda mənbə
\[ O(\sqrt{N}) \]
Grover əməliyyatını klassik
\[ O(N) \]
axtarışa qarşı kvadratik sürətlənmə kimi verir.
\(M\) hədəf olduqda optimal iterasiya sayı təxminən
\[ \frac{\pi}{4} \sqrt{\frac{N}{M}} \]
olur.
Mənbə həmçinin \(M\)-in əvvəlcədən məlum olmaya biləcəyinə diqqət çəkir və bu halda quantum counting istifadə edilə biləcəyini bildirir. Lakin tədqiqatın Qiskit qiymətləndirməsində zəruri əlavə qubitlər olmadığı üçün quantum counting faktiki tətbiq edilməmişdir.
Bu “kvadratik sürətlənmə” nə qədər güclü nəticədir?
Mənbə nəticə bölməsində metodun ənənəvi metoda nisbətən nəzəri kvadratik sürətlənmə təqdim etdiyini bildirir. Bu ifadə Grover-in axtarış mürəkkəbliyi kontekstindədir.
Tədqiqat müasir sənaye SMT həll edicilərinə qarşı real divar-saatı benchmark-ı aparmır. Bundan başqa oracle daxilində SAT, arithmetic, comparator, consistency və uncomputation dövrələrinin gate/depth xərclərinin problem ölçüsü ilə necə miqyaslandığına dair əhatəli uçdan-uca mürəkkəblik analizi verilmir.
Buna görə nəticə “real kvant kompüterində bütün klassik SMT həll edicilərindən kvadratik dərəcədə daha sürətli işləyəcəyi eksperimental olaraq göstərildi” kimi şərh edilməməlidir.
Oracle-ın dörd əsas komponenti
| Komponent | Vəzifəsi | Mənbədəki qarşılığı |
|---|---|---|
| SAT Circuit | Boolean abstrakt formulun doğru olub-olmadığını hesablayır. | \(F_B\) doğruluğu |
| Theory Circuit | Bit-vektor ifadələrini və atomların real həqiqət qiymətlərini hesablayır. | Arifmetik dövrələr + comparator dövrələri |
| Consistency Extractor | Boolean atom ilə nəzəriyyə dövrəsindəki real atom qiymətinin eyni olub-olmadığını yoxlayır. | \(v_{B_i}\equiv atom_i\) |
| Solution Inverter | Bütün şərtləri ödəyən vəziyyətlərə −1 faza verir. | Grover oracle-ın hədəfi işarələmə addımı |
SAT dövrəsi necə yaradılır?
Müəlliflər SAT tərəfini 3-SAT conjunctive normal form üçün konstruktiv şəkildə təyin edirlər:
\[ F ::= C\mid F_1\wedge F_2, \]
\[ C ::= l_1\vee l_2\vee l_3, \]
\[ l ::= v\mid\neg v\mid0. \]
Şəkil 6 tək üç-literal clause üçün istifadə olunan dövrəni göstərir. Literal müsbət olduqda və ya sabit 0 olduqda \(Q\) qapısı \(X\); literal mənfi olduqda \(Q\) qapısı identity \(I\) kimi seçilir.
Clause daxilində aralıq hesab üçün bir ancilla qubit, clause-un həqiqət qiyməti üçün ayrıca output qubit istifadə olunur.
Theorem 1: Clause dövrəsinin doğruluğu
Theorem 1 üç xüsusiyyəti sübut edir:
\[ q'_o(C)=1 \Longleftrightarrow C\text{ doğrudur}, \]
\[ q'_a(C)=0, \]
və bütün giriş literal bitləri dövrənin sonunda başlanğıc qiymətlərinə qayıdır:
\[ v'_i=v_i. \]
İkinci və üçüncü xüsusiyyətlər kvant dövrəsinin geri çevrilə bilən olması və ancilla-ların sonrakı əməliyyatlarda yenidən istifadə edilə bilməsi baxımından əhəmiyyətlidir.
Theorem 2: Tam 3-SAT formulunun doğruluğu
Şəkil 7-də iki alt formulun output qubitləri bir CCNOT qapısında birləşdirilərək
\[ F=F_1\wedge F_2 \]
hesablanır.
Theorem 2 struktur induksiya ilə bu konstruksiyanın ixtiyari 3-SAT CNF formulu üçün
\[ q'_o(F)=1 \Longleftrightarrow F\text{ doğrudur} \]
xüsusiyyətini qoruduğunu göstərir.
Theory Circuit nəyi hesablayır?
Bit-vector theory tərəfində hər atom
\[ E_1\mathrel{\rhd}E_2 \]
şəklindədir.
Əvvəlcə zəruri arifmetik əməliyyatlar hesablanır. Sonra comparator dövrəsi iki bit-string arasındakı münasibəti iki output biti ilə kodlayır:
\[ (O_1,O_2) = \begin{cases} (0,1), & E_1E_2,\\ (0,0), & E_1=E_2. \end{cases} \]
Mənbə comparator dizaynında \((1,1)\) vəziyyətinin yaranmadığını bildirir.
Bu iki output biti üzərindən altı müqayisə növü üçün ayrıca atom dövrələri qurulur:
\[ >,\;<,\;=,\;\geq,\;\leq,\;\neq. \]
Theorem 3: Atom dövrəsinin doğruluğu
Theorem 3-ün nəticəsi birbaşa belədir:
\[ atom=1 \Longleftrightarrow (E_1\mathrel{\rhd}E_2)=1. \]
Müəlliflər sübutun primitive quantum gate truth table-larının yoxlanması ilə birbaşa əldə edildiyini bildirərək səhifə məhdudiyyətinə görə ətraflı sübutu vermirlər.
Theory Circuit bütün bit-vektor əməliyyatlarını tam yerinə yetirirmi?
Tədqiqat ümumi BV sintaksisində müxtəlif arithmetic operation növlərinin ola biləcəyini bildirir; lakin bütün arifmetik dövrələrin ətraflı gate səviyyəli dizaynını bu məqalədə yaratmır.
Arifmetik əməliyyat bloku Şəkil 8(a)-da ümumi modul kimi göstərilir. Müəlliflər zəruri əməliyyatların primitive gate-lərdən qurula biləcəyini və ya əvvəlki tədqiqatlardakı quantum arithmetic dövrələrindən istifadə edilə biləcəyini bildirirlər.
Beləliklə məqalə bütün BV operatorları üçün başdan sona optimallaşdırılmış istehsal səviyyəli quantum-SMT software stack təqdim etmir. Töhfəsi daha çox SAT və theory modullarının tək Grover oracle arxitekturasında necə birləşdiriləcəyini sistematikləşdirməkdir.
Consistency Extractor niyə lazımdır?
Boolean abstraksiyası təkbaşına kifayət deyil. Məsələn Boolean dəyişəni bir atomu “doğru” kimi seçə bilər, halbuki bit-vektor dövrəsi real qiymətlər üçün eyni atomun yanlış olduğunu tapa bilər.
Buna görə hər Boolean abstract variable \(v_{B_i}\) ilə real atom nəticəsi \(atom_i\) müqayisə edilir.
Şəkil 10(a)-dakı dövrə bir CNOT və sonra \(X\) qapısından istifadə edir. Theorem 4:
\[ v'_{B_i}=1 \Longleftrightarrow v_{B_i}\equiv atom_i. \]
Beləliklə yalnız Boolean formulunu ödəmək kifayət etmir; bütün Boolean atomların theory-domain mənaları ilə də uyğun olması lazımdır.
Solution Inverter nə edir?
Şəkil 10(b)-dəki Solution Inverter, bütün consistency bitləri və SAT output biti 1 olduqda \(q_{\mathrm{SMT}}\) qubitini aktivləşdirir.
Theorem 5-in ilk şərti:
\[ q'_{\mathrm{SMT}}=1 \]
yalnız və yalnız
\[ q'_o(F_B)=1 \]
və bütün \(i\)-lər üçün
\[ v_{B_i}\equiv atom_i \]
olduqda ödənir.
Ardınca \(Z\) qapısı
\[ Z|1\rangle=-|1\rangle \]
xüsusiyyəti ilə tam həll vəziyyətlərinə −1 faza verir.
Reverse Circuit niyə var?
Oracle-ın aralıq hesablamaları çoxlu ancilla və output qubit üzərində müvəqqəti məlumat yaradır. Bunlar təmizlənməsə növbəti Grover iterasiyasında girişlə dolaşıq qala bilər və diffuser-in gözlədiyi quruluş pozula bilər.
Buna görə SAT, theory, consistency və solution-inverter hesablamalarının müvafiq hissələri əks ardıcıllıqla tətbiq edilərək aralıq qubitlər başlanğıc vəziyyətlərinə qaytarılır.
Bu əməliyyat quantum computing-dəki uncomputation prinsipinin məqalədəki qarşılığıdır.
Qiymətləndirmədə hansı SMT formulu istifadə olunur?
Müəlliflər ikinci, daha dövrə-yönümlü nümunədə Boolean formulunu
\[ F_B= (x\vee y\vee z) \wedge (x\vee\neg y\vee z) \]
kimi seçirlər.
Atomlar:
\[ y:(a+b>a\oplus b), \]
\[ z:(a+b=1) \]
şəklindədir.
Burada \(+\) fixed-width modulo-sum, \(\oplus\) isə bitwise exclusive-OR əməliyyatıdır.
Mənbə daxilindəki “c dəyişəni” uyğunsuzluğu
Qiymətləndirmə mətni “\(a,b,c\) dəyişənlərinin hamısı 2-bit” ifadəsini işlədir. Lakin dərhal sonra verilən atomların hamısında yalnız \(a\) və \(b\) mövcuddur.
Şəkil 11-dəki əsas SMT girişləri də yalnız
\[ a,\;b \]
bitlərini ehtiva edir və Tablo II yalnız bu iki dəyişən üçün qiymət verir.
Buna görə mənbədə adı çəkilən \(c\)-nin qiymətləndirmə dövrəsində real rolu olduğu təsdiqlənə bilmir. Verianla mətni bunu mənbə-daxili adlandırma/mətn uyğunsuzluğu kimi qoruyur.
32 qubit hara sərf olunur?
Mənbənin Tablo I-i qiymətləndirmə dövrəsindəki qubit istifadəsini ətraflı göstərir:
| Modul | Qubit növü | Say |
|---|---|---|
| SMT | Boolean abstract variables | 3 |
| SMT | SMT variables | 4 |
| SMT | Ancilla qubits | 5 |
| SMT | SMT output | 1 |
| SMT | Addition qubit | 1 |
| SAT | SAT output | 1 |
| SAT | Extra qubits | 2 |
| Adder | Adder output | 3 |
| Bitwise XOR | Bitwise-XOR output | 2 |
| İki comparator | Comparator output | 4 |
| İki comparator | Comparator internal output | 4 |
| İki comparator | Comparator ancilla | 2 |
Cəmi:
\[ 3+4+5+1+1+1+2+3+2+4+4+2 = 32\text{ qubit}. \]
Kiçik 2-bit SMT nümunəsinin belə 32 qubit istifadə etməsi tədqiqatın praktik miqyaslana bilmə baxımından mühüm məhdudiyyətlərindən biridir.
Şəkil 11 nəyi göstərir?
Şəkil 11(a), qiymətləndirilən bütün dövrəni tək blok diaqramında göstərir. Başlanğıcda Boolean abstract variables ilə \(a,b\) SMT dəyişənləri Hadamard qapıları ilə superpozisiyaya gətirilir.
SAT circuit və theory circuit şəkildə ardıcıl görünsə də müəlliflər aralarında məlumat asılılığı olmadığı üçün real tətbiqdə paralel işləyə biləcəklərini bildirirlər.
Theory bölməsində:
- modulo adder,
- bitwise XOR,
- \((a+b)\) ilə \((a\oplus b)\)-ni müqayisə edən comparator,
- \((a+b)\) ilə 1-i müqayisə edən ikinci comparator
yer alır.
Ardınca consistency extractor, reverse circuit və Grover diffusion circuit gəlir.
Quantum counting niyə istifadə edilmədi?
Grover iterasiyalarının optimal sayı hədəf həll sayı \(M\)-dən asılıdır. Normalda müəlliflərin təklif etdiyi metod quantum counting ilə \(M\)-ni təxmini müəyyən etməkdir.
Lakin qiymətləndirmə dövrəsi artıq 32 qubit istifadə edir və mənbədə istifadə olunan Qiskit mühitinin 32-qubit həddinə çatdığı bildirilir. Buna görə quantum counting dövrəsi əlavə edilə bilməmişdir.
Tədqiqatçılar bunun əvəzinə bir Grover iterasiyasından başlayıb iterasiya sayını artırmış və ölçmə paylanmasının pisləşməyə başladığı dönüş nöqtəsini axtarmışdır.
Bu təcrübə üçün optimal nöqtə 5 Grover iterasiyası kimi tapılmışdır. Müəlliflər daha sonra həll fəzasını klassik olaraq əl ilə enumerate edərək bu qiymətin Grover-in nəzəri iterasiya hesabı ilə uyğun olduğunu bildirirlər.
Bu metod nümayiş təcrübəsi üçün istifadə oluna bilsə də, həll sayının əvvəlcədən bilinmədiyi böyük real SMT problemlərində təkbaşına ümumi həll deyil.
Simulyasiyanın əsas nəticəsi
Beş Grover iterasiyasından sonra dövrə 1024 dəfə ölçülmüşdür. Mənbənin Tablo II-si altı həlli belə bildirir:
| Output bit-string | Ölçmə sayı | \((x,y,z)\) | \(a\) | \(b\) |
|---|---|---|---|---|
| 0010100 | 174 | (0,0,1) | 01 | 00 |
| 0011110 | 158 | (0,0,1) | 11 | 10 |
| 0010001 | 183 | (0,0,1) | 00 | 01 |
| 1001101 | 156 | (1,0,0) | 11 | 01 |
| 0011011 | 164 | (0,0,1) | 10 | 11 |
| 1000111 | 182 | (1,0,0) | 01 | 11 |
Bu altı həllin ümumi ölçmə sayı
\[ 174+158+183+156+164+182 = 1017 \]
olduğuna görə mənbə
\[ \frac{1017}{1024} \approx 0.9932 \]
nəticəsini verir və həll ölçmə ehtimalını %99,32 kimi bildirir.
“Bütün həlləri tapır” ifadəsi necə şərh edilməlidir?
Oracle-ın mühüm üstünlüyü bütün etibarlı baza vəziyyətlərini eyni superpozisiya üzərində faza baxımından işarələyə bilməsidir.
Lakin kvant ölçməsində tək shot yalnız bir classical bit-string verir. Buna görə “oracle 16 və ya 6 həlli eyni anda tanıyır” ilə “istifadəçi tək ölçmədə bütün həll siyahısını alır” eyni şey deyil.
Mənbənin eksperimental metodu da bunu təsdiqləyir: altı fərqli həll 1024 təkrar ölçmə daxilində nümunələnir.
Şəkillərin elmi rolu
| Şəkil | Əsas məzmun | Məqalədəki rolu |
|---|---|---|
| Şəkil 1 | Klassik lazy-SMT-nin SAT/theory geri dönüş dövrəsi | Kvant yanaşmasının həll etməyə çalışdığı darboğazı izah edir. |
| Şəkil 2 | Oracle-ın dörd modulu və ilk nümunədəki 16 həll | Təklif edilən arxitekturanın yüksək səviyyəli xülasəsidir. |
| Şəkil 3 | Grover oracle–diffuser–measurement axını | SMT oracle-ın Grover daxilində yerini göstərir. |
| Şəkil 5 | Tam BV-SMT dövrə blok diaqramı | SAT və theory hesablarının consistency qatına necə bağlandığını göstərir. |
| Şəkil 6–7 | Clause və formula SAT circuit strukturları | Theorem 1 və 2-də sübut edilən konstruktiv SAT dövrəsini göstərir. |
| Şəkil 8–9 | Arithmetic/comparator və altı comparison atom dövrəsi | Bit-vector theory tərəfinin kvant dövrəsinə necə çevrildiyini izah edir. |
| Şəkil 10 | Consistency Extractor və Solution Inverter | Boolean–theory uyğunluğunu və −1 faza işarələməsini göstərir. |
| Şəkil 11 | 32-qubit qiymətləndirmə dövrəsi və ölçmə histogramı | Tədqiqatın əsas simulyasiya doğrulamasını təqdim edir. |
Tədqiqatın dəstəklədiyi nəticələr
- Fixed-width bit-vector SMT problemləri üçün Grover əsaslı quantum oracle arxitekturası qurula bilər.
- Boolean SAT şərtləri və bit-vector theory şərtləri eyni oracle daxilində birlikdə qiymətləndirilə bilər.
- 3-SAT CNF formulları üçün clause və formula dövrələri konstruktiv şəkildə yaradıla bilər.
- Clause və formula dövrələrinin doğruluğu Theorem 1 və Theorem 2 ilə göstərilmişdir.
- Comparator çıxışlarından altı əsas bit-vector müqayisəsi üçün atom dövrələri yaradıla bilər.
- Consistency Extractor Boolean atom ilə theory-domain atomının eyni həqiqət qiymətinə malik olub-olmadığını düzgün müəyyən edir.
- Solution Inverter bütün Boolean və theory şərtlərini ödəyən vəziyyətlərə −1 faza verir.
- Reverse circuit aralıq qubitləri təmizləyərək oracle-ın Grover iterasiyalarında yenidən istifadəsinə imkan yaradır.
- Qiskit simulyasiyasındakı nümunə 32 qubitlik dövrədə altı düzgün SMT həlli yüksək ölçmə ehtimalına yüksəldilmişdir.
- Beş Grover iterasiyası və 1024 shot sonunda altı həll birlikdə 1017 dəfə ölçülmüş və mənbə %99,32 həll ölçmə ehtimalı bildirmişdir.
- Grover axtarışı baxımından həll axtarışının nəzəri axtarış mürəkkəbliyi klassik xətti axtarışa nisbətən kvadrat-kök miqyasına endirilə bilər.
Tədqiqatın dəstəkləmədiyi və ya sınaqdan keçirmədiyi nəticələr
- Tədqiqat real kvant prosessorunda SMT həlli həyata keçirməyib; qiymətləndirmə Qiskit simulyasiyasıdır.
- %99,32 nəticəsi ümumi SMT problemləri üçün uğur nisbəti deyil; yalnız məqalədəki konkret kiçik nümunənin 1024-shot simulyasiyasına aiddir.
- Tək quantum measurement bütün SMT həllərini siyahı şəklində qaytarmır.
- Real işləmə müddətində müasir classical SMT solver-lara qarşı kvadratik sürətlənmə eksperimental olaraq göstərilməyib.
- Oracle daxilində SAT, arithmetic, comparator və uncomputation xərclərinin böyüyən real problemlərdə ümumi gate/depth miqyaslana bilməsi əhatəli benchmark ilə araşdırılmayıb.
- Bütün bit-vector arithmetic operatorları üçün optimallaşdırılmış gate-səviyyəli dövrə dizaynı məqalədə verilmir.
- Quantum counting qiymətləndirmə dövrəsinə tətbiq edilməyib; zəruri Grover iterasiya sayı kiçik nümunədə eksperimental skan və klassik enumeration ilə müəyyən edilib.
- 32 qubitlik kiçik nümunədən böyük sənaye formal-verification problemlərinin praktik olduğu nəticəsi çıxarıla bilməz.
- Metodun başqa SMT nəzəriyyələrinə genişləndirilə biləcəyi gələcək tədqiqat təklifidir; məqalə bu nəzəriyyələr üçün işləyən oracle-ları göstərmir.
Türkiyə baxımından necə oxunmalıdır?
Mənbə Türkiyəyə xas eksperimental və ya sektoral məlumat ehtiva etmir. Türkiyə baxımından tədqiqat daha çox kvant proqram təminatı, formal verification, hardware verification və EDA tədqiqatları üçün metodoloji nümunə kimi qiymətləndirilə bilər.
Xüsusilə bit-vector SMT prosessor və rəqəmsal dövrə doğrulama problemlərində tez-tez istifadə olunan riyazi strukturlardan biridir. Lakin bu tədqiqatdan Türkiyədəki mövcud kvant avadanlığının SMT həll etməyə hazır olduğu və ya klassik doğrulama alətlərinin yaxın müddətdə əvəz ediləcəyi nəticəsi çıxarıla bilməz.
Tədqiqatın Metodu və Nəticələri
Tədqiqatın növü
Tədqiqat nəzəri kompüter elmi və kvant hesablama araşdırmasıdır. Metod kvant dövrə sintezini, riyazi doğruluq sübutlarını və state-vector/circuit simulation yanaşmasını birləşdirir.
Yeni fiziki təcrübə, real quantum processing unit benchmark-ı və ya sənaye SMT benchmark suite istifadə edilməmişdir.
Metodoloji zəncir
| Mərhələ | Metod | Çıxış |
|---|---|---|
| 1 | SMT formulunun Boolean abstraksiyası | \(F_B\) və Boolean abstract variables |
| 2 | 3-SAT clause/formula circuit construction | SAT-domain həqiqət output-u |
| 3 | Quantum arithmetic + comparator circuits | Bit-vector atom həqiqət qiymətləri |
| 4 | Consistency Extractor | Boolean və theory qatlarının uyğunluq bitləri |
| 5 | Solution Inverter | Etibarlı SMT həll vəziyyətlərində −1 faza |
| 6 | Reverse Circuit | Ancilla və müvəqqəti çıxışların uncompute edilməsi |
| 7 | Grover Diffusion | İşarələnmiş həllərin ölçmə amplitudalarının böyüdülməsi |
| 8 | Qiskit simulation | Altı həll üçün ölçmə histogramı |
Doğruluq sübutları
Tədqiqat oracle arxitekturasını yalnız simulyasiya nəticəsi ilə əsaslandırmır; beş ayrı doğruluq nəticəsi verir.
| Teorem | Sübut edilən xüsusiyyət |
|---|---|
| Theorem 1 — Clause Correctness | Clause output-u yalnız clause doğru olduqda 1 olur; ancilla təmizlənir və literal girişləri qorunur. |
| Theorem 2 — Formula Correctness | Struktur induksiya ilə ixtiyari 3-SAT CNF formulunun output-u düzgün hesablanır. |
| Theorem 3 — Atom Correctness | Comparator əsaslı atom output-u seçilən BV müqayisəsinin həqiqət qiyməti ilə eynidir. |
| Theorem 4 — Consistency Extractor | Consistency biti yalnız Boolean abstraction ilə theory atom eyni həqiqət qiymətinə malik olduqda 1 olur. |
| Theorem 5 — Solution Inverter | Yalnız tam SMT həlləri seçilir və bu vəziyyətlərə −1 faza tətbiq olunur. |
Qiymətləndirmə dövrəsi
Qiymətləndirmədə iki ədəd 2-bit SMT dəyişəni və üç Boolean abstract variable istifadə olunur. Theory circuit üçün modulo adder, bitwise XOR və iki comparator tələb olunur.
Məqalənin Table I hesabına görə ümumi qubit tələbi 32-dir.
Şəkil 11(a), SAT ilə theory circuit-in dövrə təsvirində ardıcıl görünməsinə baxmayaraq bir-birinə məlumat asılılığı olmadığı üçün paralel icra edilə biləcəyini bildirir.
Grover iterasiyalarının müəyyən edilməsi
Mənbə hədəf sayının məlum olduğu halda Grover iterasiya sayını
\[ r\approx \frac{\pi}{4} \sqrt{\frac{N}{M}} \]
ilə əlaqələndirir.
Qiymətləndirmədə quantum counting üçün kifayət qədər əlavə qubit qalmadığından müəlliflər iterasiya sayını 1-dən artıraraq measurement paylanmasının pozulduğu dönüş nöqtəsini müəyyən etmiş və 5 iterasiyada qərarlaşmışdır.
Həll fəzasının manual enumeration-u daha sonra bu seçimlə uyğun tapılmışdır.
Ölçmə nəticəsi
1024 shot daxilində altı etibarlı həllin counts qiymətləri:
\[ 174,\;158,\;183,\;156,\;164,\;182 \]
kimi bildirilmişdir.
Ən yüksək count:
\[ 183 \]
ilə `0010001`, ən aşağı count isə
\[ 156 \]
ilə `1001101` həllidir.
Lakin bu kiçik count fərqləri metodlar və ya həllər arasında keyfiyyət fərqi demək deyil. Grover amplification ideal olaraq bütün hədəflərin amplitudalarını artırır və sonlu-shot sampling təbii statistik paylanma yaradır. Mənbə bu altı həll arasında statistik üstünlük iddiası irəli sürmür.
Tədqiqatın ən güclü tərəfi
Tədqiqatın ən güclü cəhəti klassik SMT-nin SAT və theory hissələrini Grover oracle-a köçürə bilmək üçün açıq modul arxitektura təyin etməsidir.
Xüsusilə consistency extractor SMT-nin Boolean abstraksiyasının kvant dövrəsində sadəcə “SAT həlli tapmaq” probleminə endirilməsinin qarşısını alır. Theory-domain həqiqət qiymətləri də eyni oracle-ın hədəf şərtinə daxil edilir.
Tədqiqatın əsas məhdudiyyətləri
Birinci məhdudiyyət ölçəkdir. Yalnız iki 2-bit SMT dəyişəni istifadə olunan nümunə dövrə 32 qubit tələb edir. Daha böyük bit enlərində arithmetic və comparator modulları sürətlə əlavə resurs tələb edə bilər.
İkinci məhdudiyyət qiymətləndirmə metodudur. Real quantum hardware istifadə edilmədiyinə görə gate noise, decoherence, connectivity, routing və error-correction xərcləri modelləşdirilməmişdir.
Üçüncü məhdudiyyət theoretical quadratic speedup-ın uçdan-uca solver benchmark-ına çevrilməməsidir. Grover oracle çağırış sayı square-root üstünlüyü verərkən oracle-ın öz gate xərci nəzərə alınmadan buraxıla bilməz.
Dördüncü məhdudiyyət hədəf həll sayının bilinməməsi problemidir. Mənbə quantum counting-i həll kimi göstərir, lakin 32-qubit limit səbəbindən öz təcrübəsində tətbiq etmir.
Beşinci məhdudiyyət məqalənin yalnız quantifier-free fixed-width BV nəzəriyyəsinə fokuslanması və SAT tərəfində 3-SAT CNF dövrə quruluşunu ətraflı inkişaf etdirməsidir. Digər SMT nəzəriyyələri gələcək tədqiqat kimi saxlanılmışdır.
Mənbə və Metod Qeydi
Tam özgün çalışma adı: A Quantum SMT Solver for Bit-Vector Theory
Müəlliflər: Shang-Wei Lin; Si-Han Chen; Tzu-Fan Wang; Yean-Ru Chen.
Müəllif sırası: Yüklənmiş mənbədə verilən sıra olduğu kimi qorunmuşdur.
Bərabər töhfə: Mənbədə bərabər töhfə və ya bərabər birinci müəlliflik bəyanı yoxdur.
Məsul müəllif: Mənbədə rəsmi corresponding-author işarəsi yoxdur. Shang-Wei Lin və Yean-Ru Chen üçün əlaqə e-poçt ünvanları verilmişdir.
Qurumlar: Shang-Wei Lin — Nanyang Technological University, Singapore. Si-Han Chen, Tzu-Fan Wang və Yean-Ru Chen — National Cheng Kung University, Taiwan.
Elmi sahə: Logic in Computer Science, quantum computing, formal verification, satisfiability modulo theories və fixed-width bit-vector solving.
İncelənən mənbə: arXiv:2303.09353v1 [cs.LO].
İlk və incelenən arXiv sürümü: v1, 16 Mart 2023.
arXiv-issued DOI: 10.48550/arXiv.2303.09353.
Hakemlik/yayın durumu: İncelənən fayl arXiv repository/preprint sürümüdür və faylın özündə hakemli jurnal və ya konfrans yayım qeydi yoxdur. Buna görə yüklənmiş v1, hakemli version of record kimi qiymətləndirilməmişdir.
Eyni başlıqlı 2026 qeyd barədə bibliyografik qeyd: 2026 International Conference on Quantum Communications, Networking, and Computing qeydlərində eyni başlıqla konfrans məqaləsi vardır; lakin müəllif siyahısı Shang-Wei Lin, Si-Han Chen, Lei-Han Yao, Yu-Chung Chen və Yean-Ru Chen kimidir. Yüklənmiş v1-də isə Tzu-Fan Wang vardır və Lei-Han Yao ilə Yu-Chung Chen yoxdur. Rəsmi mənbələrdə iki qeyd arasındakı sürüm əlaqəsi açıq şəkildə doğrulanmadığı üçün 2026 konfrans işi bu Verianla məqaləsində yüklənmiş v1-in hakemli sürümü kimi istifadə edilməmişdir.
Lisenziya: arXiv qeydi Creative Commons Attribution 4.0 International (CC BY 4.0) lisenziyasına yönləndirir.
Maliyyələşdirmə: Yüklənmiş mənbədə ayrıca maliyyələşdirmə və ya grant bəyanı yoxdur.
Verilənlərin əlçatanlığı: Ayrı data-availability bəyanı yoxdur. Tədqiqat eksperimental məlumat dəstinə deyil, nəzəri dövrə dizaynı və Qiskit simulyasiyasına əsaslanır.
Maraq toqquşması: Yüklənmiş mənbədə ayrıca conflict-of-interest bəyanı yoxdur; bundan maraq toqquşması olmadığı nəticəsi çıxarılmamışdır.
Müəllif töhfələri: Mənbədə CRediT və ya ətraflı author-contributions bəyanı yoxdur.
Mənbə-daxili uyğunsuzluq: Mətn formulun/qiymətləndirmə nümunəsinin \(a,b,c\) adlı üç 2-bit dəyişən ehtiva etdiyini bildirir; lakin göstərilən atomlar, dövrə girişləri və həll cədvəli yalnız \(a\) və \(b\)-ni istifadə edir. \(c\)-nin qiymətləndirmədəki funksiyası mənbədə göstərilmədiyi üçün Verianla mətni bunu səssizcə tamamlamamışdır.
Tədqiqat metodu: Grover search; quantum oracle construction; 3-SAT circuit synthesis; reversible CCNOT/CNOT/X/Z/H gate strukturları; quantum arithmetic; quantum comparator; Boolean–theory consistency extraction; phase inversion; uncomputation/reverse circuit və Qiskit simulation.
Qiymətləndirmə şərti: Məqalədəki əsas Qiskit nümunəsi 32 qubit, beş Grover iterasiyası və 1024 measurement shot istifadə edir. Altı etibarlı həllin ümumi count qiyməti 1017 olub mənbə %99,32 solution-measurement probability bildirir.
Metodoloji sərhəd: Tədqiqatın nəzəri kvadratik sürətlənmə ifadəsi Grover search complexity kontekstindədir. Mənbə real quantum hardware üzərində müasir classical SMT solver-larla uçdan-uca runtime müqayisəsi aparmır.
Elmi məzmun sərhədi: Bu Verianla məqaləsindəki alqoritm arxitekturası, formullar, teoremlər, dövrə komponentləri, qubit resurs cədvəli və simulyasiya nəticələri yüklənmiş yeddi səhifəlik arXiv:2303.09353v1 faylına əsaslanır. Xarici mənbələr yalnız arXiv kimliyini, lisenziyanı və eyni başlıqlı 2026 konfrans qeydinin bibliyografik vəziyyətini yoxlamaq üçün istifadə edilmişdir; yüklənmiş mənbədə olmayan elmi performans nəticəsi əlavə edilməmişdir.
Verianla Live qeydi: Mənbənin Tablo II-sindəki altı həllin measurement counts qiymətləri birbaşa eyni simulyasiya şərtindən gəldiyi üçün `vlive-bar` istifadə edilmişdir. Mənbədə klassik və kvant SMT həll ediciləri arasında real runtime benchmark-ı olmadığı üçün nəzəri sürətlənmə iddiası üçün süni performans qrafiki yaradılmamışdır.
Şərh yazın
E-poçt ünvanınız yayımlanmayacaq. Məcburi sahələr * ilə işarələnib