Ushbu tadqiqot qat’iy kenglikdagi bit-vektor nazariyasiga oid satisfiability modulo theory (SMT) muammolarini Grover algoritmi yordamida yechish uchun kvant sxemaga asoslangan usulni ishlab chiqadi. Usul klassik lazy-SMT yondashuvidagi Boolean yechim hosil qilish va nazariya izchilligini tekshirish bosqichlarini alohida-alohida takrorlash o‘rniga, Boolean o‘zgaruvchilar va bit-vektor o‘zgaruvchilarining barcha mumkin bo‘lgan qiymatlarini kvant superpozitsiyasida ifodalaydi; SAT sxemasi, nazariya sxemasi, izchillik ajratuvchisi va yechim inverteridan tashkil topgan oracle yordamida haqiqiy SMT yechimlarini faza bo‘yicha belgilaydi hamda Grover diffuser ushbu yechimlarni o‘lchash ehtimolini oshiradi. Qiskit muhitida o‘tkazilgan namunaviy baholashda 32 qubitli sxema, beshta Grover iteratsiyasi va 1024 measurement shot yordamida oltita to‘g‘ri yechim jami 1017 marta o‘lchangan va yechimni o‘lchash ehtimoli %99,32 deb xabar qilingan. Tadqiqotning asosiy cheklovi baholash kichik 2-bitli misolda simulyatsiya orqali bajarilgani hamda zamonaviy klassik SMT yechuvchilar bilan haqiqiy ishlash vaqti, gate xarajati yoki masshtablanuvchanlik benchmark’i taqdim etilmaganidir.

Maqolaning yangiligi faqat Grover algoritmini SMT muammosiga qo‘llashdan iborat emas. Mualliflar Grover oracle SMTning ikkita alohida mantiqiy qatlamini bir xil sxema ichida tekshira olishi uchun tizimli tuzilma taklif qiladilar. Boolean abstraksiyasi uchun SAT sxemasi, haqiqiy bit-vektor ifodalarini hisoblaydigan arithmetic/comparator sxemalari, ikki qatlam bir xil rostlik qiymatini hosil qiladimi-yo‘qmi tekshiradigan consistency extractor va barcha shartlarni qanoatlantiruvchi kirishlarga −1 faza beradigan solution inverter birgalikda ishlaydi.

“Barcha yechimlarni bir vaqtda tekshirish” iborasi ehtiyotkorlik bilan talqin qilinishi kerak. Superpozitsiya tufayli oracle barcha hisoblash-bazis kirishlarini koherent ravishda baholab, haqiqiy holatlarni bir xil kvant amali ichida belgilashi mumkin; biroq bitta yakuniy o‘lchash barcha yechimlarni ro‘yxat ko‘rinishida chiqarmaydi. Manbaning o‘z tajribasida oltita turli yechimni olish uchun 1024 measurement shot ishlatilgan.

SMT muammosi SAT muammosidan qanday farq qiladi?

Boolean satisfiability (SAT) muammosida o‘zgaruvchilar bevosita rost/yolg‘on qiymatlarini oladi. SMT esa Boolean mantiqini muayyan matematik nazariya bilan birlashtiradi. Atom, masalan, ikki bit-vektorning tengligi yoki kattalik munosabati bo‘lishi mumkin.

Tadqiqot ayniqsa quantifier-free fixed-width bit-vector theory, qisqacha \(\mathcal{BV}\), ga qaratilgan. Bit-vektor ifodasi o‘zgaruvchi, doimiy yoki ikki ifoda ustidagi arifmetik amal bo‘lishi mumkin. Tadqiqotda misol tariqasida ko‘rsatilgan amallar sinflari qatoriga modulo qo‘shish, modulo ko‘paytirish, bitwise amallar, siljitish va word concatenation kiradi.

Atomlar esa ikki ifodani

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

taqqoslagichlaridan biri bilan bog‘laydi.

Klassik lazy SMT yondashuvi qanday ishlaydi?

Manbaning 1-rasmida klassik lazy yondashuv uchta asosiy bosqichga ajratiladi:

1. Asl SMT formulasi Boolean formulaga abstraksiyalanadi.
2. SAT yechuvchi ushbu Boolean formula uchun tayinlash topadi.
3. Theory solver Boolean tayinlashning haqiqiy nazariya o‘zgaruvchilari bilan izchil yoki izchil emasligini tekshiradi.

Agar tayinlash nazariy jihatdan izchil bo‘lmasa, SAT yechuvchiga qaytiladi va boshqa Boolean yechim qidiriladi.

Manba birinchi misolda

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

formulasidan foydalanadi.

Boolean o‘zgaruvchilari

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

deb ta’riflanganda abstrakt formula

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

bo‘ladi.

1-rasmda SAT yechuvchining dastlabki uchta Boolean tayinlashi theory solver tomonidan rad etiladi va faqat to‘rtinchi iteratsiyada izchil yechim topiladi. Mualliflarning kvant yondashuviga o‘tishidagi asosiy motivatsiya aynan shu Boolean–nazariya qaytish siklidir.

Kvant yondashuvining asosiy g‘oyasi nima?

Ikkita 2-bitli o‘zgaruvchi

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

va uchta Boolean abstrakt o‘zgaruvchi \(x,y,z\) birgalikda

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

holati bilan ifodalanadi.

Ushbu yetti kirish biti uchun \(2^7=128\) ta mumkin bo‘lgan hisoblash-bazis kirishi mavjud. Birinchi misolda oracle ana shu barcha mumkin bo‘lgan kirishlar superpozitsiyasi ustida ishlaydi.

Kirish yechim bo‘lishi uchun avvalo Boolean formulani qanoatlantirishi kerak:

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

Bundan tashqari Boolean abstrakt o‘zgaruvchilari bit-vektor nazariyasidagi haqiqiy muqobillari bilan izchil bo‘lishi kerak:

\[ (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 haqiqiy yechimlarni qanday belgilaydi?

Taklif etilgan oracle \(\Psi\) barcha Boolean va nazariya shartlarini qanoatlantiradigan kirishning fazasini teskari aylantiradi:

\[ \Psi(|v\rangle) = \begin{cases} -|v\rangle, & \text{Boolean formula va barcha nazariya-izchillik shartlari bajarilsa},\\ |v\rangle, & \text{aks holda}. \end{cases} \]

Ushbu −1 faza belgisi Grover diffuser qaysi bazis holatlarining o‘lchash amplitudasini oshirishini belgilaydi.

Manbaning 2-rasmidagi birinchi misolda oracle 128 ta mumkin bo‘lgan kirish ichidagi 16 ta haqiqiy SMT yechimni bitta oracle qo‘llanishida faza jihatdan belgilay oladi.

Grover algoritmi yechim ehtimolini qanday oshiradi?

Grover algoritmida ikkita amal takrorlanadi:

• Oracle maqsad holatlarning fazasini teskari aylantiradi.
• Diffuser amplitudalarni o‘rtacha qiymat atrofida teskari aylantirib, belgilangan holatlarning o‘lchash ehtimolini oshiradi.

Bitta maqsad mavjud bo‘lgan \(N\) elementli ideal qidiruvda manba

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

Grover amalini klassik

\[ O(N) \]

qidiruvga nisbatan kvadratik tezlashuv sifatida beradi.

\(M\) ta maqsad mavjud bo‘lganda optimal iteratsiyalar soni taxminan

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

bo‘ladi.

Manba, shuningdek, \(M\) oldindan ma’lum bo‘lmasligi mumkinligiga e’tibor qaratadi va bunday holatda quantum counting qo‘llanishi mumkinligini aytadi. Biroq tadqiqotning Qiskit baholashida zarur qo‘shimcha qubitlar yetishmagani uchun quantum counting amalda qo‘llanmagan.

Bu “kvadratik tezlashuv” qanchalik kuchli natija?

Manba xulosa bo‘limida usul an’anaviy usulga nisbatan nazariy kvadratik tezlashuv taqdim etishini bildiradi. Bu ifoda Grover qidiruv murakkabligi kontekstidadir.

Tadqiqot zamonaviy sanoat SMT yechuvchilariga qarshi haqiqiy devor-soati benchmark’ini o‘tkazmaydi. Bundan tashqari oracle ichidagi SAT, arithmetic, comparator, consistency va uncomputation sxemalarining gate/depth xarajatlari muammo hajmi bilan qanday masshtablanishiga oid keng qamrovli uchidan-uchigacha murakkablik tahlili berilmagan.

Shu sababli natija “haqiqiy kvant kompyuterida barcha klassik SMT yechuvchilardan kvadratik darajada tezroq ishlashi eksperimental ravishda ko‘rsatildi” deb talqin qilinmasligi kerak.

Oracle’ning to‘rtta asosiy komponenti

SAT sxemasi qanday yaratiladi?

Mualliflar SAT tomonini 3-SAT conjunctive normal form uchun konstruktiv tarzda belgilaydilar:

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

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

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

6-rasm bitta uch-literal clause uchun ishlatiladigan sxemani ko‘rsatadi. Literal musbat bo‘lganda yoki doimiy 0 bo‘lganda \(Q\) gate \(X\); literal manfiy bo‘lganda \(Q\) gate identity \(I\) sifatida tanlanadi.

Clause ichidagi oraliq hisoblash uchun bitta ancilla qubit, clause’ning rostlik qiymati uchun alohida output qubit ishlatiladi.

Theorem 1: Clause sxemasining to‘g‘riligi

Theorem 1 uchta xususiyatni isbotlaydi:

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

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

va barcha kirish literal bitlari sxema oxirida boshlang‘ich qiymatlariga qaytadi:

\[ v'_i=v_i. \]

Ikkinchi va uchinchi xususiyatlar kvant sxemaning qaytariluvchan bo‘lishi hamda ancilla’larning keyingi amallarda qayta ishlatilishi nuqtayi nazaridan muhimdir.

Theorem 2: To‘liq 3-SAT formulasining to‘g‘riligi

7-rasmda ikki quyi formula output qubitlari bitta CCNOT gate’da birlashtirilib

\[ F=F_1\wedge F_2 \]

hisoblanadi.

Theorem 2 tuzilmaviy induksiya orqali ushbu qurilish ixtiyoriy 3-SAT CNF formulasi uchun

\[ q'_o(F)=1 \Longleftrightarrow F\text{ rost} \]

xususiyatini saqlashini ko‘rsatadi.

Theory Circuit nimani hisoblaydi?

Bit-vector theory tomonida har bir atom

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

ko‘rinishidadir.

Avval zarur arifmetik amallar hisoblanadi. So‘ng comparator sxemasi ikki bit-string orasidagi munosabatni ikkita output biti orqali kodlaydi:

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

Manba comparator dizaynida \((1,1)\) holati yuzaga kelmasligini ta’kidlaydi.

Ushbu ikki output biti asosida oltita taqqoslash turi uchun alohida atom sxemalari quriladi:

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

Theorem 3: Atom sxemasining to‘g‘riligi

Theorem 3 natijasi bevosita quyidagicha:

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

Mualliflar isbot primitive quantum gate truth table’larini tekshirish orqali bevosita olinishi mumkinligini aytib, sahifa cheklovi sababli batafsil isbotni bermaydilar.

Theory Circuit barcha bit-vektor amallarini to‘liq bajaradimi?

Tadqiqot umumiy BV sintaksisida turli arithmetic operation turlari bo‘lishi mumkinligini bildiradi; biroq barcha arifmetik sxemalarning batafsil gate-darajadagi dizaynini ushbu maqolada ishlab chiqmaydi.

Arifmetik amal bloki 8(a)-rasmda umumiy modul sifatida ko‘rsatiladi. Mualliflar zarur amallar primitive gate’lardan tuzilishi yoki avvalgi ishlardagi quantum arithmetic sxemalaridan foydalanilishi mumkinligini ta’kidlaydilar.

Shunday qilib, maqola barcha BV operatorlari uchun boshidan oxirigacha optimallashtirilgan ishlab chiqarish darajasidagi quantum-SMT software stack taqdim etmaydi. Uning hissasi ko‘proq SAT va theory modullarini bitta Grover oracle arxitekturasida qanday bog‘lashni tizimlashtirishdan iborat.

Consistency Extractor nima uchun kerak?

Boolean abstraksiya o‘z-o‘zicha yetarli emas. Masalan, Boolean o‘zgaruvchi bir atomni “rost” deb tanlashi mumkin, holbuki bit-vektor sxemasi haqiqiy qiymatlar uchun o‘sha atom yolg‘onligini topishi mumkin.

Shu sababli har bir Boolean abstract variable \(v_{B_i}\) bilan haqiqiy atom natijasi \(atom_i\) taqqoslanadi.

10(a)-rasmdagi sxema bitta CNOT va undan keyin \(X\) gate’dan foydalanadi. Theorem 4:

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

Shunday qilib faqat Boolean formulani qanoatlantirish yetarli emas; barcha Boolean atomlar theory-domain ma’nolari bilan ham izchil bo‘lishi kerak.

Solution Inverter nima qiladi?

10(b)-rasmdagi Solution Inverter barcha consistency bitlari va SAT output biti 1 bo‘lganda \(q_{\mathrm{SMT}}\) qubitini faollashtiradi.

Theorem 5’ning birinchi sharti:

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

faqat va faqat

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

hamda barcha \(i\) lar uchun

\[ v_{B_i}\equiv atom_i \]

bo‘lganda bajariladi.

So‘ng \(Z\) gate

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

xususiyati bilan to‘liq yechim holatlariga −1 faza beradi.

Reverse Circuit nima uchun mavjud?

Oracle’ning oraliq hisoblari ko‘plab ancilla va output qubitlarda vaqtinchalik ma’lumot hosil qiladi. Ular tozalanmasa, keyingi Grover iteratsiyasida kirish bilan chirmashib qolishi va diffuser kutadigan tuzilmani buzishi mumkin.

Shu sababli SAT, theory, consistency va solution-inverter hisoblarining tegishli qismlari teskari tartibda qo‘llanib, oraliq qubitlar boshlang‘ich holatlariga qaytariladi.

Bu amal quantum computing’dagi uncomputation prinsipining maqoladagi muqobilidir.

Baholashda qaysi SMT formula ishlatiladi?

Mualliflar ikkinchi, sxemaga ko‘proq yo‘naltirilgan misolda Boolean formulani

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

deb tanlaydilar.

Atomlar:

\[ x:(a+b

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

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

ko‘rinishidadir.

Bu yerda \(+\) fixed-width modulo-sum, \(\oplus\) esa bitwise exclusive-OR amalidir.

Manbadagi “c o‘zgaruvchisi” nomuvofiqligi

Baholash matnida “\(a,b,c\) o‘zgaruvchilarining barchasi 2-bit” degan ibora ishlatiladi. Biroq darhol undan keyin berilgan atomlarning barchasida faqat \(a\) va \(b\) bor.

11-rasmdagi asosiy SMT kirishlari ham faqat

\[ a,\;b \]

bitlarini o‘z ichiga oladi va Tablo II faqat shu ikki o‘zgaruvchi uchun qiymatlar beradi.

Shu sababli manbada tilga olingan \(c\) baholash sxemasida haqiqiy rolga ega ekani tasdiqlanmaydi. Verianla matni buni manba ichidagi nomlash/matn nomuvofiqligi sifatida saqlaydi.

32 qubit qayerga sarflanadi?

Manbaning Tablo I baholash sxemasidagi qubit ishlatilishini batafsil ko‘rsatadi:

Jami:

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

Kichik 2-bitli SMT misolining o‘zi ham 32 qubit ishlatishi tadqiqotning amaliy masshtablanuvchanlik nuqtayi nazaridan muhim cheklovlaridan biridir.

11-rasm nimani ko‘rsatadi?

11(a)-rasm baholanayotgan butun sxemani bitta blok diagrammada ko‘rsatadi. Dastlab Boolean abstract variables hamda \(a,b\) SMT o‘zgaruvchilari Hadamard gate’lari bilan superpozitsiyaga keltiriladi.

SAT circuit va theory circuit rasmda ketma-ket ko‘rinsa-da, mualliflar ular orasida ma’lumot bog‘liqligi bo‘lmagani uchun haqiqiy qo‘llashda parallel ishlashi mumkinligini aytadilar.

Theory bo‘limida:

• modulo adder,
• bitwise XOR,
• \((a+b)\) bilan \((a\oplus b)\) ni taqqoslaydigan comparator,
• \((a+b)\) bilan 1 ni taqqoslaydigan ikkinchi comparator

mavjud.

So‘ng consistency extractor, reverse circuit va Grover diffusion circuit keladi.

Nima uchun quantum counting ishlatilmadi?

Grover iteratsiyalarining optimal soni maqsad yechimlar soni \(M\) ga bog‘liq. Odatda mualliflar taklif qilgan usul quantum counting yordamida \(M\) ni taxminan aniqlashdir.

Biroq baholash sxemasi allaqachon 32 qubit ishlatadi va manbada ishlatilgan Qiskit muhiti 32-qubit chegarasiga yetgani aytiladi. Shuning uchun quantum counting sxemasi qo‘shilmagan.

Tadqiqotchilar buning o‘rniga bitta Grover iteratsiyasidan boshlab iteratsiyalar sonini oshirgan va o‘lchash taqsimoti yomonlasha boshlaydigan burilish nuqtasini qidirgan.

Ushbu tajriba uchun optimal nuqta 5 Grover iteratsiyasi deb topilgan. Mualliflar keyinroq yechim fazosini klassik tarzda qo‘lda enumerate qilib, bu qiymat Grover’ning nazariy iteratsiya hisobiga mos kelishini ta’kidlaydilar.

Bu usul namoyish tajribasi uchun qo‘llanishi mumkin, biroq yechimlar soni oldindan noma’lum bo‘lgan katta haqiqiy SMT muammolarida o‘z-o‘zicha umumiy yechim emas.

Simulyatsiyaning asosiy natijasi

Beshta Grover iteratsiyasidan keyin sxema 1024 marta o‘lchangan. Manbaning Tablo II oltita yechimni quyidagicha xabar qiladi:

Ushbu oltita yechimning jami o‘lchash soni

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

bo‘lgani uchun manba

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

natijasini beradi va yechimni o‘lchash ehtimolini %99,32 deb xabar qiladi.

“Barcha yechimlarni topadi” iborasi qanday talqin qilinishi kerak?

Oracle’ning muhim afzalligi barcha haqiqiy bazis holatlarini bir xil superpozitsiya ustida faza jihatdan belgilay olishidir.

Biroq kvant o‘lchashda bitta shot faqat bitta classical bit-string beradi. Shuning uchun “oracle 16 yoki 6 yechimni bir vaqtda taniydi” bilan “foydalanuvchi bitta o‘lchashda barcha yechimlar ro‘yxatini oladi” bir xil narsa emas.

Manbaning tajriba usuli ham buni tasdiqlaydi: oltita turli yechim 1024 takroriy o‘lchash davomida namunalangan.

Rasmlarning ilmiy roli

Tadqiqot qo‘llab-quvvatlaydigan natijalar

• Fixed-width bit-vector SMT muammolari uchun Grover asosidagi quantum oracle arxitekturasi qurilishi mumkin.
• Boolean SAT shartlari va bit-vector theory shartlari bir oracle ichida birgalikda baholanishi mumkin.
• 3-SAT CNF formulalari uchun clause va formula sxemalari konstruktiv tarzda yaratilishi mumkin.
• Clause va formula sxemalarining to‘g‘riligi Theorem 1 va Theorem 2 bilan ko‘rsatilgan.
• Comparator chiqishlaridan oltita asosiy bit-vector taqqoslash uchun atom sxemalari yaratilishi mumkin.
• Consistency Extractor Boolean atom bilan theory-domain atom bir xil rostlik qiymatiga egaligini to‘g‘ri aniqlaydi.
• Solution Inverter barcha Boolean va theory shartlarini qanoatlantiruvchi holatlarga −1 faza beradi.
• Reverse circuit oraliq qubitlarni tozalab, oracle’ni Grover iteratsiyalarida qayta ishlatishga imkon beradi.
• Qiskit simulyatsiyasidagi namunaviy 32 qubitli sxemada oltita to‘g‘ri SMT yechim yuqori o‘lchash ehtimoliga kuchaytirilgan.
• Beshta Grover iteratsiyasi va 1024 shot oxirida oltita yechim jami 1017 marta o‘lchangan va manba %99,32 yechim o‘lchash ehtimolini xabar qilgan.
• Grover qidiruvi nuqtayi nazaridan yechim qidirishning nazariy qidiruv murakkabligi klassik chiziqli qidiruvga nisbatan kvadrat ildiz miqyosiga tushirilishi mumkin.

Tadqiqot qo‘llab-quvvatlamaydigan yoki sinamagan natijalar

• Tadqiqot haqiqiy kvant protsessorida SMT yechimini bajarmagan; baholash Qiskit simulyatsiyasidir.
• %99,32 natijasi umumiy SMT muammolari uchun muvaffaqiyat darajasi emas; faqat maqoladagi aniq kichik misolning 1024-shot simulyatsiyasiga tegishli.
• Bitta quantum measurement barcha SMT yechimlarini ro‘yxat ko‘rinishida qaytarmaydi.
• Haqiqiy ishlash vaqtida zamonaviy classical SMT solver’larga qarshi kvadratik tezlashuv eksperimental ravishda ko‘rsatilmagan.
• Oracle ichidagi SAT, arithmetic, comparator va uncomputation xarajatlarining o‘sib boruvchi haqiqiy muammolardagi jami gate/depth masshtablanuvchanligi keng benchmark bilan tekshirilmagan.
• Barcha bit-vector arithmetic operatorlari uchun optimallashtirilgan gate-darajadagi sxema dizayni maqolada berilmagan.
• Quantum counting baholash sxemasiga qo‘llanmagan; zarur Grover iteratsiyalar soni kichik misolda tajribaviy skan va klassik enumeration orqali aniqlangan.
• 32 qubitli kichik misoldan katta sanoat formal-verification muammolari amaliy degan xulosa chiqarib bo‘lmaydi.
• Usulni boshqa SMT nazariyalariga kengaytirish mumkinligi kelajakdagi ish taklifidir; maqola bu nazariyalar uchun ishlaydigan oracle’larni ko‘rsatmaydi.

Turkiya nuqtayi nazaridan qanday o‘qish kerak?

Manba Turkiyaga xos tajribaviy yoki sektoral ma’lumotlarni o‘z ichiga olmaydi. Turkiya nuqtayi nazaridan tadqiqotni ko‘proq kvant dasturiy ta’minoti, formal verification, hardware verification va EDA tadqiqotlari uchun metodologik misol sifatida baholash mumkin.

Xususan bit-vector SMT protsessor va raqamli sxemalarni tekshirish muammolarida tez-tez ishlatiladigan matematik tuzilmalardan biridir. Biroq ushbu tadqiqotdan Turkiyadagi mavjud kvant apparatlari SMT yechishga tayyor yoki klassik tekshirish vositalari yaqin muddatda o‘rnini bo‘shatadi degan xulosa chiqarib bo‘lmaydi.

Tadqiqot Usuli va Natijalari

Tadqiqot turi

Tadqiqot nazariy kompyuter fanlari va kvant hisoblash ishidir. Usul kvant sxema sintezi, matematik to‘g‘rilik isbotlari va state-vector/circuit simulation yondashuvini birlashtiradi.

Yangi fizik tajriba, haqiqiy quantum processing unit benchmark’i yoki sanoat SMT benchmark suite ishlatilmagan.

Metodologik zanjir

To‘g‘rilik isbotlari

Tadqiqot oracle arxitekturasini faqat simulyatsiya natijasi bilan asoslamaydi; beshta alohida to‘g‘rilik natijasini beradi.

Baholash sxemasi

Baholashda ikkita 2-bitli SMT o‘zgaruvchi va uchta Boolean abstract variable ishlatiladi. Theory circuit uchun modulo adder, bitwise XOR va ikkita comparator kerak.

Maqolaning Table I hisobiga ko‘ra jami qubit talabi 32.

11(a)-rasm SAT va theory circuit sxema chizmasida ketma-ket ko‘rinsa-da, ular orasida ma’lumot bog‘liqligi bo‘lmagani uchun parallel bajarilishi mumkinligini ta’kidlaydi.

Grover iteratsiyalarini aniqlash

Manba maqsadlar soni ma’lum bo‘lsa Grover iteratsiyalar sonini

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

bilan bog‘laydi.

Baholashda quantum counting uchun yetarli qo‘shimcha qubit qolmagani sababli mualliflar iteratsiyalar sonini 1 dan oshirib, measurement taqsimoti buziladigan burilish nuqtasini aniqlagan va 5 iteratsiyada to‘xtagan.

Yechim fazosining manual enumeration’i keyinchalik ushbu tanlovga mos deb topilgan.

O‘lchash natijasi

1024 shot ichidagi oltita haqiqiy yechimning counts qiymatlari:

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

deb xabar qilingan.

Eng yuqori count:

\[ 183 \]

bilan `0010001`, eng past count esa

\[ 156 \]

bilan `1001101` yechimidir.

Biroq bu kichik count farqlari usullar yoki yechimlar o‘rtasidagi sifat farqini anglatmaydi. Grover amplification ideal holda barcha maqsadlarning amplitudalarini oshiradi va cheklangan-shot sampling tabiiy statistik taqsimot hosil qiladi. Manba ushbu oltita yechim orasida statistik ustunlik da’vosini bildirmaydi.

Tadqiqotning eng kuchli tomoni

Tadqiqotning eng kuchli jihati klassik SMTning SAT va theory qismlarini Grover oracle’ga ko‘chirish uchun aniq modulli arxitekturani ta’riflashidir.

Ayniqsa consistency extractor SMTning Boolean abstraksiyasini kvant sxemada faqat “SAT yechimini topish” muammosiga qisqartirishga yo‘l qo‘ymaydi. Theory-domain rostlik qiymatlari ham xuddi shu oracle’ning maqsad shartiga kiritiladi.

Tadqiqotning asosiy cheklovlari

Birinchi cheklov masshtabdir. Faqat ikkita 2-bitli SMT o‘zgaruvchi ishlatiladigan namunaviy sxema 32 qubit talab qiladi. Kattaroq bit kengliklarida arithmetic va comparator modullari tezda qo‘shimcha resurs talab qilishi mumkin.

Ikkinchi cheklov baholash usulidir. Haqiqiy quantum hardware ishlatilmagani sababli gate noise, decoherence, connectivity, routing va error-correction xarajatlari modellashtirilmagan.

Uchinchi cheklov theoretical quadratic speedup uchidan-uchigacha solver benchmark’iga aylantirilmaganidir. Grover oracle chaqiriqlari soni square-root afzallik bersa-da, oracle’ning o‘z gate xarajatlarini e’tiborsiz qoldirib bo‘lmaydi.

To‘rtinchi cheklov maqsad yechimlar sonini bilmaslik muammosidir. Manba quantum counting’ni yechim sifatida ko‘rsatadi, biroq 32-qubit limit sababli o‘z tajribasida qo‘llamaydi.

Beshinchi cheklov maqolaning faqat quantifier-free fixed-width BV nazariyasiga qaratilgani va SAT tomonida 3-SAT CNF sxema tuzilishini batafsil ishlab chiqqanidir. Boshqa SMT nazariyalari kelajakdagi ish sifatida qoldirilgan.

Manba va Usul Haqida Izoh

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

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

Mualliflar tartibi: Yuklangan manbada berilgan tartib aynan saqlangan.

Teng hissa: Manbada teng hissa yoki teng birinchi mualliflik bayonoti mavjud emas.

Mas’ul muallif: Manbada rasmiy corresponding-author belgisi yo‘q. Shang-Wei Lin va Yean-Ru Chen uchun aloqa e-mail manzillari berilgan.

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

Ilmiy soha: Logic in Computer Science, quantum computing, formal verification, satisfiability modulo theories va fixed-width bit-vector solving.

Ko‘rib chiqilgan manba: arXiv:2303.09353v1 [cs.LO].

Birinchi va ko‘rib chiqilgan arXiv versiyasi: v1, 16 Mart 2023.

arXiv-issued DOI: 10.48550/arXiv.2303.09353.

Hakemlik/yayın durumu: Ko‘rib chiqilgan fayl arXiv repository/preprint versiyasidir va faylning o‘zida hakemli jurnal yoki konferensiya nashri qaydi yo‘q. Shu sababli yuklangan v1 hakemli version of record sifatida baholanmagan.

Xuddi shu nomdagi 2026 qaydi haqida bibliografik izoh: 2026 International Conference on Quantum Communications, Networking, and Computing yozuvlarida xuddi shu nomdagi konferensiya maqolasi mavjud; biroq mualliflar ro‘yxati Shang-Wei Lin, Si-Han Chen, Lei-Han Yao, Yu-Chung Chen va Yean-Ru Chen ko‘rinishidadir. Yuklangan v1 da esa Tzu-Fan Wang bor, Lei-Han Yao va Yu-Chung Chen yo‘q. Rasmiy manbalarda ikki qayd orasidagi versiya munosabati aniq tasdiqlanmagani uchun 2026 konferensiya ishi ushbu Verianla maqolasida yuklangan v1 ning hakemli versiyasi sifatida ishlatilmagan.

Litsenziya: arXiv qaydi Creative Commons Attribution 4.0 International (CC BY 4.0) litsenziyasiga yo‘naltiradi.

Moliyalashtirish: Yuklangan manbada alohida moliyalashtirish yoki grant bayonoti mavjud emas.

Ma’lumotlar mavjudligi: Alohida data-availability bayonoti mavjud emas. Tadqiqot tajribaviy ma’lumotlar to‘plamiga emas, nazariy sxema dizayni va Qiskit simulyatsiyasiga asoslangan.

Manfaatlar to‘qnashuvi: Yuklangan manbada alohida conflict-of-interest bayonoti yo‘q; bundan manfaatlar to‘qnashuvi yo‘q degan qo‘shimcha xulosa chiqarilmagan.

Mualliflar hissasi: Manbada CRediT yoki batafsil author-contributions bayonoti mavjud emas.

Manba ichidagi nomuvofiqlik: Matn formula/baholash misoli \(a,b,c\) nomli uchta 2-bitli o‘zgaruvchini o‘z ichiga olishini aytadi; biroq ko‘rsatilgan atomlar, sxema kirishlari va yechim jadvali faqat \(a\) va \(b\) dan foydalanadi. \(c\) ning baholashdagi vazifasi manbada ko‘rsatilmagani sababli Verianla matni buni jimlik bilan to‘ldirmagan.

Tadqiqot usuli: Grover search; quantum oracle construction; 3-SAT circuit synthesis; reversible CCNOT/CNOT/X/Z/H gate tuzilmalari; quantum arithmetic; quantum comparator; Boolean–theory consistency extraction; phase inversion; uncomputation/reverse circuit va Qiskit simulation.

Baholash sharti: Maqoladagi asosiy Qiskit misoli 32 qubit, beshta Grover iteratsiyasi va 1024 measurement shot ishlatadi. Oltita haqiqiy yechimning jami count qiymati 1017 bo‘lib, manba %99,32 solution-measurement probability xabar qiladi.

Metodologik chegara: Tadqiqotdagi nazariy kvadratik tezlashuv ifodasi Grover search complexity kontekstidadir. Manba haqiqiy quantum hardware’da zamonaviy classical SMT solver’lar bilan uchidan-uchigacha runtime taqqoslashini o‘tkazmaydi.

Ilmiy mazmun chegarasi: Ushbu Verianla maqolasidagi algoritm arxitekturasi, formulalar, teoremalar, sxema komponentlari, qubit resurs jadvali va simulyatsiya natijalari yuklangan yetti sahifalik arXiv:2303.09353v1 fayliga asoslangan. Tashqi manbalar faqat arXiv identifikatori, litsenziya va xuddi shu nomdagi 2026 konferensiya qaydining bibliografik holatini tekshirish uchun ishlatilgan; yuklangan manbada mavjud bo‘lmagan ilmiy ishlash natijasi qo‘shilmagan.

Verianla Live izohi: Manbaning Tablo II dagi oltita yechimning measurement counts qiymatlari to‘g‘ridan-to‘g‘ri bir xil simulyatsiya shartidan kelgani uchun `vlive-bar` ishlatilgan. Manbada klassik va kvant SMT yechuvchilari o‘rtasida haqiqiy runtime benchmark’i bo‘lmagani sababli nazariy tezlashuv da’vosi uchun sun’iy ishlash grafigi yaratilmagan.