Ин таҳқиқот барои ҳалли масъалаҳои satisfiability modulo theory (SMT), ки ба назарияи bit-vector-и паҳноии собит тааллуқ доранд, усули ба схемаҳои квантӣ асосёфтаро бо истифода аз алгоритми Grover таҳия мекунад. Ба ҷойи он ки қадамҳои тавлиди ҳалли Boolean ва санҷиши мутобиқати назария дар равиши классикии lazy-SMT ҷудогона такрор шаванд, усул ҳамаи қиматҳои имконпазири тағйирёбандаҳои Boolean ва bit-vector-ро дар суперпозицияи квантӣ ифода мекунад; бо oracle, ки аз SAT circuit, theory circuit, consistency extractor ва solution inverter иборат аст, ҳалли дурусти SMT-ро аз рӯйи фаза аломатгузорӣ мекунад ва Grover diffuser эҳтимоли ченшавии ин ҳаллҳоро афзоиш медиҳад. Дар арзёбии намунавӣ дар Qiskit бо истифода аз схемае дорои 32 qubit, панҷ итератсияи Grover ва 1024 measurement shot, шаш ҳалли дуруст дар маҷмӯъ 1017 маротиба чен карда шуданд ва эҳтимоли чен кардани ҳалли дуруст %99,32 гузориш шуд. Маҳдудияти асосии таҳқиқот он аст, ки арзёбӣ бо симулятсия дар як мисоли хурди 2-bit анҷом дода шудааст ва бо SMT solver-ҳои муосири классикӣ benchmark-и воқеии вақти иҷро, gate cost ё миқёспазирӣ пешниҳод намешавад.

Навоварии мақола танҳо дар татбиқи алгоритми Grover ба масъалаи SMT нест. Муаллифон сохтори низоммандеро пешниҳод мекунанд, то Grover oracle тавонад ду қабати ҷудогонаи мантиқии SMT-ро дар як схема санҷад. SAT circuit барои абстраксияи Boolean, arithmetic/comparator circuits барои ҳисоб кардани ифодаҳои воқеии bit-vector, consistency extractor барои санҷидани он ки ду қабат як қимати ҳақиқат медиҳанд ё не, ва solution inverter, ки ба ҳамаи воридҳое, ки ҳамаи шартҳоро қонеъ мекунанд, фазаи −1 медиҳад, якҷоя кор мекунанд.

Ибораи “санҷидани ҳамаи ҳаллҳо дар як вақт” бояд бо эҳтиёт тафсир шавад. Ба шарофати суперпозиция oracle метавонад ҳамаи воридҳои computational-basis-ро ба таври когерент арзёбӣ карда, ҳолатҳои дурустро дар дохили як амали квантӣ аломатгузорӣ намояд; аммо як ченкунии ниҳоӣ ҳамаи ҳаллҳоро ба шакли рӯйхат берун намекунад. Дар таҷрибаи худи манбаъ барои ба даст овардани шаш ҳалли гуногун 1024 measurement shot истифода шудааст.

Масъалаи SMT аз масъалаи SAT чӣ фарқ дорад?

Дар масъалаи Boolean satisfiability (SAT) тағйирёбандаҳо мустақиман қиматҳои дуруст/нодуруст мегиранд. SMT бошад мантиқи Boolean-ро бо як назарияи муайяни математикӣ муттаҳид мекунад. Масалан, атом метавонад баробарии ду bit-vector ё муносибати бузургӣ байни онҳо бошад.

Таҳқиқот махсусан ба quantifier-free fixed-width bit-vector theory, ба таври кӯтоҳ \(\mathcal{BV}\), равона шудааст. Ифодаи bit-vector метавонад тағйирёбанда, собит ё амали арифметикӣ байни ду ифода бошад. Аз ҷумлаи синфҳои амалҳое, ки дар таҳқиқот мисол оварда шудаанд, modulo addition, modulo multiplication, bitwise operations, shifting ва word concatenation ҳастанд.

Атомҳо бошанд ду ифодаро бо яке аз муқоисакунандаҳои

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

пайваст мекунанд.

Равиши классикии lazy SMT чӣ гуна кор мекунад?

Дар Шакли 1-и манбаъ равиши классикии lazy ба се қадами асосӣ ҷудо мешавад:

1. Формулаи аслии SMT ба формулаи Boolean абстраксия мешавад.
2. SAT solver барои ин формулаи Boolean як таъйинот пайдо мекунад.
3. Theory solver месанҷад, ки таъйиноти Boolean бо тағйирёбандаҳои воқеии назария мутобиқ аст ё не.

Агар таъйинот аз ҷиҳати назариявӣ номувофиқ бошад, ба SAT solver баргашта, ҳалли дигари Boolean ҷустуҷӯ мешавад.

Манбаъ дар мисоли аввал

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

формуларо истифода мебарад.

Вақте тағйирёбандаҳои Boolean ҳамчун

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

таъриф мешаванд, формулаи абстрактӣ

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

мешавад.

Дар Шакли 1 се таъйиноти аввалини Boolean-и SAT solver аз ҷониби theory solver рад мешаванд ва танҳо дар итератсияи чорум ҳалли мутобиқ пайдо мешавад. Ангезаи асосии гузариши муаллифон ба равиши квантӣ ҳамин ҳалқаи бозгашти Boolean–theory мебошад.

Ғояи асосӣ дар равиши квантӣ чист?

Ду тағйирёбандаи 2-bit

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

ва се тағйирёбандаи абстрактии Boolean \(x,y,z\) якҷоя бо ҳолати

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

ифода мешаванд.

Барои ин ҳафт bit-и ворид \(2^7=128\) вориди имконпазири computational-basis мавҷуд аст. Дар мисоли аввал oracle дар суперпозицияи ҳамаи ин воридҳои имконпазир кор мекунад.

Барои он ки як ворид ҳалли масъала бошад, аввал бояд формулаи Boolean-ро қонеъ кунад:

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

Илова бар ин, тағйирёбандаҳои абстрактии Boolean бояд бо ҳамтоёни воқеии худ дар назарияи bit-vector мутобиқ бошанд:

\[ (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 ҳалли дурустро чӣ гуна аломатгузорӣ мекунад?

Oracle-и пешниҳодшуда \(\Psi\) фазаи воридеро, ки ҳамаи шартҳои Boolean ва theory-ро қонеъ мекунад, баръакс мегардонад:

\[ \Psi(|v\rangle) = \begin{cases} -|v\rangle, & \text{агар формулаи Boolean ва ҳамаи шартҳои theory-consistency иҷро шаванд},\\ |v\rangle, & \text{дар акси ҳол}. \end{cases} \]

Ин аломати фазаи −1 муайян мекунад, ки Grover diffuser амплитудаи ченшавии кадом ҳолатҳои basis-ро зиёд мекунад.

Дар мисоли аввалини Шакли 2-и манбаъ oracle метавонад аз миёни 128 вориди имконпазир 16 ҳалли дурусти SMT-ро дар як татбиқи oracle аз рӯйи фаза аломатгузорӣ кунад.

Алгоритми Grover эҳтимоли ҳалли дурустро чӣ гуна зиёд мекунад?

Дар алгоритми Grover ду амал такрор мешаванд:

• Oracle фазаи ҳолатҳои ҳадафро баръакс мегардонад.
• Diffuser амплитудаҳоро нисбат ба миёна инверсия карда, эҳтимоли ченшавии ҳолатҳои аломатгузоришударо зиёд мекунад.

Дар ҷустуҷӯи идеалии дорои \(N\) унсур ва як ҳадаф манбаъ

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

амали Grover-ро нисбат ба ҷустуҷӯи классикии

\[ O(N) \]

ҳамчун тезониши квадратӣ тавсиф мекунад.

Вақте \(M\) ҳадаф вуҷуд дорад, шумораи оптималии итератсияҳо тақрибан

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

мешавад.

Манбаъ инчунин қайд мекунад, ки \(M\) метавонад пешакӣ маълум набошад ва дар ин ҳолат quantum counting истифода шавад. Аммо дар арзёбии Qiskit-и таҳқиқот, бинобар набудани qubit-ҳои иловагии кофӣ, quantum counting амалан татбиқ нашудааст.

Ин “тезониши квадратӣ” то чӣ андоза натиҷаи қавӣ аст?

Манбаъ дар бахши натиҷаҳо мегӯяд, ки усул нисбат ба усули анъанавӣ тезониши назариявии квадратӣ медиҳад. Ин изҳорот дар заминаи search complexity-и Grover аст.

Таҳқиқот бо SMT solver-ҳои муосири саноатӣ benchmark-и воқеии wall-clock иҷро намекунад. Ғайр аз ин, таҳлили пурраи end-to-end барои он ки gate/depth cost-и SAT, arithmetic, comparator, consistency ва uncomputation circuits дар дохили oracle бо андозаи масъала чӣ гуна миқёс меёбад, пешниҳод нашудааст.

Аз ин рӯ, натиҷаро набояд чунин тафсир кард, ки “дар компютери воқеии квантӣ аз ҳамаи SMT solver-ҳои классикӣ ба таври квадратӣ тезтар кор карданаш эксперименталӣ нишон дода шуд”.

Чор ҷузъи асосии Oracle

SAT circuit чӣ гуна сохта мешавад?

Муаллифон тарафи SAT-ро барои 3-SAT conjunctive normal form ба таври созанда таъриф мекунанд:

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

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

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

Шакли 6 схемаи истифодашавандаро барои як clause-и се-literal нишон медиҳад. Вақте literal мусбат ё собити 0 аст, \(Q\) gate ҳамчун \(X\); вақте literal манфӣ аст, \(Q\) gate ҳамчун identity \(I\) интихоб мешавад.

Барои ҳисобкунии мобайнии clause як ancilla qubit ва барои қимати ҳақиқати clause як output qubit-и ҷудогона истифода мешавад.

Theorem 1: Дурустии схемаи Clause

Theorem 1 се хусусиятро исбот мекунад:

\[ q'_o(C)=1 \Longleftrightarrow C\text{ дуруст аст}, \]

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

ва ҳамаи bit-ҳои literal-и ворид дар охири схема ба қиматҳои ибтидоии худ бармегарданд:

\[ v'_i=v_i. \]

Хусусиятҳои дуюм ва сеюм барои reversible будани схемаи квантӣ ва аз нав истифода бурдани ancilla-ҳо дар амалҳои минбаъда муҳим мебошанд.

Theorem 2: Дурустии формулаи пурраи 3-SAT

Дар Шакли 7 output qubit-ҳои ду зерформула дар як CCNOT gate муттаҳид карда шуда,

\[ F=F_1\wedge F_2 \]

ҳисоб карда мешавад.

Theorem 2 бо structural induction нишон медиҳад, ки ин сохт барои формулаи дилхоҳи 3-SAT CNF хусусияти

\[ q'_o(F)=1 \Longleftrightarrow F\text{ дуруст аст} \]

ро нигоҳ медорад.

Theory Circuit чиро ҳисоб мекунад?

Дар тарафи bit-vector theory ҳар atom шакли

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

дорад.

Аввал амалҳои арифметикии лозим ҳисоб карда мешаванд. Сипас comparator circuit муносибати байни ду bit-string-ро бо ду output bit рамзгузорӣ мекунад:

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

Манбаъ қайд мекунад, ки дар тарҳи comparator ҳолати \((1,1)\) ба вуҷуд намеояд.

Аз рӯйи ин ду output bit барои шаш навъи муқоиса atom circuit-ҳои ҷудогона сохта мешаванд:

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

Theorem 3: Дурустии схемаи Atom

Натиҷаи Theorem 3 мустақиман чунин аст:

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

Муаллифон мегӯянд, ки исбот аз баррасии primitive quantum gate truth table-ҳо мустақим ҳосил мешавад ва бинобар маҳдудияти саҳифа тафсилоти исботро намеоранд.

Оё Theory Circuit ҳамаи амалҳои bit-vector-ро пурра иҷро мекунад?

Таҳқиқот қайд мекунад, ки дар синтаксиси умумии BV намудҳои гуногуни arithmetic operation мавҷуд буда метавонанд; аммо тарҳи муфассали gate-level барои ҳамаи arithmetic circuits дар ин мақола сохта нашудааст.

Блоки амали арифметикӣ дар Шакли 8(a) ҳамчун модули умумӣ нишон дода мешавад. Муаллифон мегӯянд, ки амалҳои лозимро аз primitive gate-ҳо сохтан ё quantum arithmetic circuit-ҳои корҳои қаблиро истифода бурдан мумкин аст.

Аз ин рӯ мақола барои ҳамаи операторҳои BV як production-level quantum-SMT software stack-и пурра ва оптимизатсияшуда пешниҳод намекунад. Саҳми асосӣ бештар дар систематизатсияи он аст, ки SAT ва theory modules дар як Grover oracle architecture чӣ гуна пайваст карда мешаванд.

Consistency Extractor барои чӣ лозим аст?

Boolean abstraction худ ба худ кофӣ нест. Масалан, тағйирёбандаи Boolean метавонад як atom-ро “дуруст” интихоб кунад, дар ҳоле ки bit-vector circuit барои қиматҳои воқеӣ ҳамон atom-ро нодуруст ёбад.

Аз ин сабаб ҳар Boolean abstract variable \(v_{B_i}\) бо натиҷаи воқеии atom \(atom_i\) муқоиса мешавад.

Схемаи Шакли 10(a) як CNOT ва баъдан \(X\) gate истифода мекунад. Theorem 4:

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

Ҳамин тавр танҳо қонеъ кардани формулаи Boolean кофӣ нест; ҳамаи atom-ҳои Boolean низ бояд бо маънои theory-domain-и худ мутобиқ бошанд.

Solution Inverter чӣ кор мекунад?

Solution Inverter-и Шакли 10(b) вақте ҳамаи consistency bit-ҳо ва SAT output bit ба 1 баробаранд, qubit-и \(q_{\mathrm{SMT}}\)-ро фаъол мекунад.

Шарти аввалини Theorem 5:

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

танҳо ва танҳо вақте иҷро мешавад, ки

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

ва барои ҳамаи \(i\)

\[ v_{B_i}\equiv atom_i \]

бошад.

Баъдан \(Z\) gate бо хусусияти

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

ба ҳолатҳои пурраи ҳалли дуруст фазаи −1 медиҳад.

Reverse Circuit барои чӣ вуҷуд дорад?

Ҳисобкуниҳои мобайнии oracle дар бисёр ancilla ва output qubit-ҳо маълумоти муваққатӣ тавлид мекунанд. Агар онҳо тоза нашаванд, дар итератсияи навбатии Grover бо ворид entangled шуда, сохтореро, ки diffuser интизор аст, вайрон карда метавонанд.

Аз ин рӯ қисмҳои дахлдори ҳисобҳои SAT, theory, consistency ва solution-inverter бо тартиби баръакс татбиқ мешаванд ва qubit-ҳои мобайнӣ ба ҳолатҳои ибтидоӣ баргардонида мешаванд.

Ин амал дар мақола муодили принсипи uncomputation дар quantum computing мебошад.

Дар арзёбӣ кадом формулаи SMT истифода мешавад?

Муаллифон дар мисоли дуюм, ки бештар ба схема нигаронида шудааст, формулаи Boolean-ро

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

чунин интихоб мекунанд.

Atom-ҳо:

\[ x:(a+b

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

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

мебошанд.

Дар ин ҷо \(+\) fixed-width modulo-sum ва \(\oplus\) bitwise exclusive-OR мебошад.

Номувофиқии “тағйирёбандаи c” дар дохили манбаъ

Матни арзёбӣ ибораи “ҳамаи тағйирёбандаҳои \(a,b,c\) 2-bit мебошанд”-ро истифода мебарад. Аммо дар ҳамаи atom-ҳои баъдӣ танҳо \(a\) ва \(b\) мавҷуданд.

Воридҳои асосии SMT дар Шакли 11 низ танҳо

\[ a,\;b \]

bit-ҳоро дар бар мегиранд ва Tablo II танҳо барои ҳамин ду тағйирёбанда қимат медиҳад.

Аз ин рӯ, дар схемаи арзёбӣ нақши воқеии \(c\), ки дар манбаъ номбар шудааст, тасдиқ намешавад. Матни Verianla инро ҳамчун номувофиқии номгузорӣ/матн дар дохили манбаъ нигоҳ медорад.

32 qubit дар куҷо истифода мешавад?

Tablo I-и манбаъ истифодаи qubit-ҳоро дар схемаи арзёбӣ муфассал нишон медиҳад:

Ҳамагӣ:

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

Ҳатто як мисоли хурди 2-bit SMT истифодаи 32 qubit-ро талаб мекунад, ки яке аз маҳдудиятҳои муҳими таҳқиқот аз ҷиҳати миқёспазирии амалӣ мебошад.

Шакли 11 чиро нишон медиҳад?

Шакли 11(a) тамоми схемаи арзёбишавандаро дар як блок-диаграмма нишон медиҳад. Дар оғоз Boolean abstract variables ва тағйирёбандаҳои SMT-и \(a,b\) бо Hadamard gate-ҳо ба суперпозиция гузошта мешаванд.

Гарчанде SAT circuit ва theory circuit дар расм пайдарпай намоёнанд, муаллифон мегӯянд, ки байни онҳо вобастагии додаҳо нест ва дар татбиқи воқеӣ метавонанд параллелӣ кор кунанд.

Дар қисми Theory:

• modulo adder,
• bitwise XOR,
• comparator барои муқоисаи \((a+b)\) бо \((a\oplus b)\),
• comparator-и дуюм барои муқоисаи \((a+b)\) бо 1

мавҷуданд.

Баъдан consistency extractor, reverse circuit ва Grover diffusion circuit меоянд.

Чаро quantum counting истифода нашуд?

Шумораи оптималии итератсияҳои Grover аз шумораи ҳалли ҳадаф \(M\) вобаста аст. Усули пешниҳодкардаи муаллифон дар ҳолати умумӣ муайян кардани тахминии \(M\) бо quantum counting мебошад.

Аммо схемаи арзёбӣ аллакай 32 qubit истифода мекунад ва манбаъ мегӯяд, ки муҳити Qiskit-и истифодашуда ба маҳдудияти 32-qubit расидааст. Аз ин рӯ илова кардани quantum counting circuit имконнопазир буд.

Ба ҷойи ин, муҳаққиқон аз як итератсияи Grover оғоз карда, шумораи итератсияҳоро зиёд карданд ва нуқтаи гардишеро ҷустуҷӯ намуданд, ки дар он тақсимоти ченкунӣ бад шудан мегирад.

Барои ин таҷриба нуқтаи оптималӣ 5 итератсияи Grover муайян шуд. Муаллифон баъдан фазои ҳаллро ба таври классикӣ дастӣ enumerate карда, мувофиқати ин қиматро бо ҳисоби назариявии итератсияҳои Grover қайд мекунанд.

Ин усул барои таҷрибаи намоишӣ қобили истифода аст, аммо барои масъалаҳои калони воқеии SMT, ки шумораи ҳаллҳо пешакӣ маълум нест, худ ба худ ҳалли умумӣ намебошад.

Натиҷаи асосии симулятсия

Пас аз панҷ итератсияи Grover схема 1024 маротиба чен карда шуд. Tablo II-и манбаъ шаш ҳалли зеринро гузориш мекунад:

Азбаски шумораи умумии ченкуниҳои ин шаш ҳалли дуруст

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

аст, манбаъ

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

натиҷаро медиҳад ва эҳтимоли чен кардани ҳалли дурустро %99,32 гузориш мекунад.

Ибораи “ҳамаи ҳаллҳоро пайдо мекунад” чӣ гуна тафсир шавад?

Бартарии муҳими oracle дар он аст, ки метавонад ҳамаи ҳолатҳои дурусти basis-ро дар як суперпозиция аз рӯйи фаза аломатгузорӣ кунад.

Аммо дар ченкунии квантӣ як shot танҳо як classical bit-string медиҳад. Аз ин рӯ “oracle 16 ё 6 ҳалли дурустро дар як вақт мешиносад” ва “корбар бо як ченкунӣ рӯйхати ҳамаи ҳаллҳоро мегирад” як чиз нестанд.

Усули эксперименталии манбаъ низ инро тасдиқ мекунад: шаш ҳалли гуногун дар 1024 ченкунии такрорӣ намуна гирифта мешаванд.

Нақши илмии шаклҳо

Натиҷаҳое, ки таҳқиқот дастгирӣ мекунад

• Барои масъалаҳои fixed-width bit-vector SMT сохтани architecture-и quantum oracle бар асоси Grover имконпазир аст.
• Шартҳои Boolean SAT ва bit-vector theory метавонанд дар як oracle якҷоя арзёбӣ шаванд.
• Барои формулаҳои 3-SAT CNF clause ва formula circuit-ҳоро ба таври конструктивӣ сохтан мумкин аст.
• Дурустии clause ва formula circuit-ҳо бо Theorem 1 ва Theorem 2 нишон дода шудааст.
• Аз output-и comparator барои шаш муқоисаи асосии bit-vector atom circuit сохтан мумкин аст.
• Consistency Extractor дуруст муайян мекунад, ки Boolean atom ва theory-domain atom як қимати ҳақиқат доранд ё не.
• Solution Inverter ба ҳолатҳое, ки ҳамаи шартҳои Boolean ва theory-ро қонеъ мекунанд, фазаи −1 медиҳад.
• Reverse circuit qubit-ҳои мобайниро тоза карда, истифодаи такрории oracle-ро дар итератсияҳои Grover имконпазир мекунад.
• Дар схемаи намунавии 32-qubit-и Qiskit simulation шаш ҳалли дурусти SMT ба эҳтимоли баланди ченшавӣ тақвият дода шуданд.
• Пас аз панҷ итератсияи Grover ва 1024 shot, шаш ҳалли дуруст дар маҷмӯъ 1017 маротиба чен карда шуданд ва манбаъ эҳтимоли ченкунии ҳалли %99,32-ро гузориш кард.
• Аз нуқтаи назари Grover search, theoretical search complexity-и ҷустуҷӯи ҳалли дуруст метавонад аз linear classical search ба square-root scale коҳиш дода шавад.

Натиҷаҳое, ки таҳқиқот дастгирӣ ё санҷиш намекунад

• Таҳқиқот ҳалли SMT-ро дар quantum processor-и воқеӣ иҷро накардааст; арзёбӣ Qiskit simulation мебошад.
• Натиҷаи %99,32 success rate барои масъалаҳои умумии SMT нест; он танҳо ба 1024-shot simulation-и мисоли хурди мушаххаси мақола дахл дорад.
• Як quantum measurement ҳамаи ҳаллҳои SMT-ро ба шакли рӯйхат барнамегардонад.
• Quadratic speedup нисбат ба modern classical SMT solver-ҳо дар вақти воқеии иҷро эксперименталӣ нишон дода нашудааст.
• Миқёспазирии умумии gate/depth cost-и SAT, arithmetic, comparator ва uncomputation дар дохили oracle барои масъалаҳои воқеии калон бо benchmark-и фарогир санҷида нашудааст.
• Барои ҳамаи bit-vector arithmetic operators тарҳи optimized gate-level circuit дар мақола дода нашудааст.
• Quantum counting ба evaluation circuit татбиқ нашудааст; шумораи зарурии итератсияҳои Grover дар мисоли хурд бо experimental scan ва classical enumeration муайян шудааст.
• Аз мисоли хурди 32-qubit наметавон хулоса кард, ки масъалаҳои калони industrial formal-verification амалӣ мебошанд.
• Густариши усул ба дигар SMT theories пешниҳоди future work мебошад; мақола oracle-ҳои коркунандаро барои ин theories нишон намедиҳад.

Аз нуқтаи назари Туркия чӣ гуна бояд хонда шавад?

Манбаъ додаҳои эксперименталӣ ё соҳавии махсуси Туркияро дар бар намегирад. Аз нуқтаи назари Туркия, таҳқиқотро бештар ҳамчун намунаи методологӣ барои quantum software, formal verification, hardware verification ва EDA research метавон арзёбӣ кард.

Махсусан bit-vector SMT яке аз сохторҳои математикӣ мебошад, ки дар verification-и processor ва digital circuits зиёд истифода мешавад. Аммо аз ин таҳқиқот набояд чунин хулоса гирифт, ки quantum hardware-и мавҷуда дар Туркия барои ҳалли SMT омода аст ё classical verification tools дар ояндаи наздик ҷойи худро аз даст медиҳанд.

Усул ва Натиҷаҳои Таҳқиқот

Навъи таҳқиқот

Ин кор таҳқиқоти theoretical computer science ва quantum computing мебошад. Усул quantum circuit synthesis, mathematical correctness proofs ва state-vector/circuit simulation approach-ро муттаҳид мекунад.

Ягон physical experiment-и нав, benchmark-и воқеии quantum processing unit ё industrial SMT benchmark suite истифода нашудааст.

Занҷираи методологӣ

Исботҳои дурустӣ

Таҳқиқот architecture-и oracle-ро танҳо бо simulation result асоснок намекунад; панҷ натиҷаи ҷудогонаи correctness пешниҳод мекунад.

Схемаи арзёбӣ

Дар арзёбӣ ду тағйирёбандаи 2-bit SMT ва се Boolean abstract variable истифода мешаванд. Барои Theory circuit modulo adder, bitwise XOR ва ду comparator лозим аст.

Мувофиқи ҳисоби Table I-и мақола, талаботи умумии qubit 32 мебошад.

Шакли 11(a) қайд мекунад, ки гарчанде SAT ва theory circuit дар расми схема пайдарпай намоёнанд, бинобар набудани data dependency байни онҳо, метавонанд параллелӣ иҷро шаванд.

Муайян кардани итератсияҳои Grover

Манбаъ вақте шумораи ҳадафҳо маълум аст, шумораи итератсияҳои Grover-ро бо

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

алоқаманд мекунад.

Азбаски дар арзёбӣ барои quantum counting qubit-и кофии иловагӣ намонд, муаллифон шумораи итератсияҳоро аз 1 зиёд карда, нуқтаи гардиши вайроншавии measurement distribution-ро муайян намуданд ва ба 5 итератсия қарор карданд.

Manual enumeration-и solution space баъдан бо ин интихоб мувофиқ дониста шуд.

Натиҷаи ченкунӣ

Counts values-и шаш ҳалли дуруст дар 1024 shot:

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

гузориш шудаанд.

Баландтарин count:

\[ 183 \]

барои `0010001`, ва пасттарин count:

\[ 156 \]

барои `1001101` мебошад.

Аммо ин фарқҳои хурди count маънои фарқи сифат байни methods ё solutions-ро надоранд. Grover amplification дар ҳолати идеалӣ amplitudes-и ҳамаи targets-ро зиёд мекунад ва finite-shot sampling тақсимоти табиии оморӣ ҳосил мекунад. Манбаъ байни ин шаш ҳалли дуруст ягон даъвои statistical superiority намекунад.

Қавитарин ҷиҳати таҳқиқот

Қавитарин ҷиҳати таҳқиқот дар он аст, ки architecture-и modular-и равшанеро барои интиқоли қисмҳои SAT ва theory-и SMT-и классикӣ ба Grover oracle таъриф мекунад.

Хусусан consistency extractor намегузорад, ки Boolean abstraction-и SMT дар quantum circuit танҳо ба масъалаи “ёфтани SAT solution” коҳиш дода шавад. Theory-domain truth values низ ба target condition-и ҳамон oracle дохил карда мешаванд.

Маҳдудиятҳои асосии таҳқиқот

Маҳдудияти аввал scale аст. Example circuit, ки танҳо ду тағйирёбандаи 2-bit SMT истифода мекунад, 32 qubit талаб мекунад. Дар bit-width-ҳои калонтар arithmetic ва comparator modules метавонанд зуд resource-и иловагӣ талаб кунанд.

Маҳдудияти дуюм evaluation method мебошад. Азбаски quantum hardware-и воқеӣ истифода нашудааст, gate noise, decoherence, connectivity, routing ва error-correction costs моделсозӣ нашудаанд.

Маҳдудияти сеюм он аст, ки theoretical quadratic speedup ба end-to-end solver benchmark табдил дода нашудааст. Гарчанде шумораи Grover oracle calls square-root advantage медиҳад, gate cost-и худи oracle-ро нодида гирифтан мумкин нест.

Маҳдудияти чорум масъалаи номаълум будани шумораи target solutions мебошад. Манбаъ quantum counting-ро ҳамчун роҳи ҳал нишон медиҳад, аммо бинобар 32-qubit limit онро дар таҷрибаи худ истифода намекунад.

Маҳдудияти панҷум он аст, ки мақола танҳо ба quantifier-free fixed-width BV theory диққат медиҳад ва дар тарафи SAT сохтори 3-SAT CNF circuit-ро муфассал таҳия мекунад. Дигар SMT theories ба future work гузошта шудаанд.

Ёддошт оид ба Манбаъ ва Усул

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

Муаллифон: Shang-Wei Lin; Si-Han Chen; Tzu-Fan Wang; Yean-Ru Chen.

Тартиби муаллифон: Тартиби дар манбаи боршуда овардашуда айнан нигоҳ дошта шудааст.

Саҳми баробар: Дар манбаъ изҳорот дар бораи саҳми баробар ё first co-authorship мавҷуд нест.

Муаллифи масъул: Дар манбаъ аломати расмии corresponding-author мавҷуд нест. Барои Shang-Wei Lin ва Yean-Ru Chen суроғаҳои e-mail-и тамос оварда шудаанд.

Муассисаҳо: Shang-Wei Lin — Nanyang Technological University, Singapore. Si-Han Chen, Tzu-Fan Wang ва Yean-Ru Chen — National Cheng Kung University, Taiwan.

Соҳаи илмӣ: Logic in Computer Science, quantum computing, formal verification, satisfiability modulo theories ва fixed-width bit-vector solving.

Манбаи баррасишуда: arXiv:2303.09353v1 [cs.LO].

Аввалин ва баррасишудаи arXiv version: v1, 16 Mart 2023.

arXiv-issued DOI: 10.48550/arXiv.2303.09353.

Hakemlik/yayın durumu: Файли баррасишуда arXiv repository/preprint version мебошад ва худи файл record-и peer-reviewed journal ё conference publication надорад. Аз ин рӯ v1-и боршуда ҳамчун peer-reviewed version of record арзёбӣ нашудааст.

Ёддошти библиографӣ дар бораи record-и ҳамноми 2026: Дар records-и 2026 International Conference on Quantum Communications, Networking, and Computing мақолаи conference бо ҳамин title мавҷуд аст; аммо author list чунин аст: Shang-Wei Lin, Si-Han Chen, Lei-Han Yao, Yu-Chung Chen ва Yean-Ru Chen. Дар v1-и боршуда бошад Tzu-Fan Wang ҳаст ва Lei-Han Yao ва Yu-Chung Chen нестанд. Азбаски relation-и version байни ду record дар sources-и расмӣ ба таври возеҳ тасдиқ нашудааст, conference work-и 2026 дар ин Verianla article ҳамчун peer-reviewed version-и v1-и боршуда истифода нашудааст.

Литсензия: Record-и arXiv ба Creative Commons Attribution 4.0 International (CC BY 4.0) ишора мекунад.

Маблағгузорӣ: Дар манбаи боршуда ягон funding ё grant statement-и ҷудогона мавҷуд нест.

Дастрасии додаҳо: Data-availability statement-и ҷудогона мавҷуд нест. Таҳқиқот ба experimental dataset не, балки ба theoretical circuit design ва Qiskit simulation асос ёфтааст.

Ихтилофи манфиатҳо: Дар манбаи боршуда conflict-of-interest statement-и ҷудогона нест; аз ин ҳолат хулосаи иловагӣ дар бораи набудани conflict of interest бароварда нашудааст.

Саҳми муаллифон: Дар манбаъ CRediT ё detailed author-contributions statement вуҷуд надорад.

Номувофиқии дохили манбаъ: Матн мегӯяд, ки formula/evaluation example се тағйирёбандаи 2-bit бо номҳои \(a,b,c\) дорад; аммо atom-ҳои нишон додашуда, circuit inputs ва solution table танҳо \(a\) ва \(b\)-ро истифода мекунанд. Азбаски function-и \(c\) дар evaluation дар манбаъ нишон дода нашудааст, матни Verianla онро худсарона пур накардааст.

Усули таҳқиқот: Grover search; quantum oracle construction; 3-SAT circuit synthesis; reversible CCNOT/CNOT/X/Z/H gate structures; quantum arithmetic; quantum comparator; Boolean–theory consistency extraction; phase inversion; uncomputation/reverse circuit ва Qiskit simulation.

Шарти арзёбӣ: Example-и асосии Qiskit дар мақола 32 qubit, панҷ Grover iteration ва 1024 measurement shot истифода мекунад. Total count-и шаш valid solution ба 1017 баробар буда, манбаъ %99,32 solution-measurement probability гузориш медиҳад.

Марзи методологӣ: Ифодаи theoretical quadratic speedup дар таҳқиқот дар контексти Grover search complexity аст. Манбаъ дар real quantum hardware бо modern classical SMT solver-ҳо end-to-end runtime comparison анҷом намедиҳад.

Марзи мазмуни илмӣ: Algorithm architecture, formulas, theorems, circuit components, qubit resource table ва simulation results дар ин Verianla article ба файли ҳафтсаҳифагии arXiv:2303.09353v1 асос ёфтаанд. External sources танҳо барои санҷидани arXiv identity, license ва bibliographic status-и conference record-и ҳамноми 2026 истифода шуданд; ягон scientific performance result, ки дар манбаи боршуда набуд, илова нашудааст.

Verianla Live note: Азбаски measurement counts values-и шаш solution дар Tablo II-и манбаъ бевосита аз ҳамон як simulation condition омадаанд, `vlive-bar` истифода шудааст. Азбаски манбаъ real runtime benchmark байни classical ва quantum SMT solvers надорад, барои claim-и theoretical speedup ягон artificial performance chart сохта нашудааст.