Бул изилдөө туруктуу кеңдиктеги бит-вектор теориясына тиешелүү satisfiability modulo theory (SMT) маселелерин Grover алгоритми менен чечүү үчүн кванттык схемаларга негизделген ыкманы иштеп чыгат. Ыкма классикалык lazy-SMT ыкмасындагы Boolean чечимин түзүү жана теориялык шайкештикти текшерүү кадамдарын өз-өзүнчө кайталоонун ордуна, Boolean өзгөрмөлөрү менен бит-вектор өзгөрмөлөрүнүн бардык мүмкүн болгон маанилерин кванттык суперпозицияда көрсөтөт; SAT схемасы, теория схемасы, шайкештик чыгаруучусу жана чечим инверторунан турган oracle аркылуу жарактуу SMT чечимдерин фаза боюнча белгилеп, Grover diffuser бул чечимдердин өлчөнүү ыктымалдыгын жогорулатат. Qiskit чөйрөсүндө жүргүзүлгөн үлгүлүү баалоодо 32 qubitтик схема, беш Grover итерациясы жана 1024 measurement shot колдонулуп, алты туура чечим жалпысынан 1017 жолу өлчөнгөн жана чечимди өлчөө ыктымалдыгы %99,32 деп билдирилген. Изилдөөнүн негизги чектөөсү баалоо кичинекей 2-bit мисалда симуляция аркылуу жүргүзүлгөнү жана заманбап классикалык SMT чечкичтери менен чыныгы иштөө убактысы, gate чыгымы же масштабдуулук benchmark’ы берилбегендиги болуп саналат.

Макаланын жаңылыгы Grover алгоритмин SMT маселесине колдонуу менен гана чектелбейт. Авторлор Grover oracle’ы SMTнин эки өзүнчө логикалык катмарын бир эле схема ичинде текшере алышы үчүн системалуу түзүлүш сунушташат. Boolean абстракциясы үчүн SAT схемасы, чыныгы бит-вектор туюнтмаларын эсептеген arithmetic/comparator схемалары, эки катмар бирдей чындык маанисин чыгарабы же жокпу текшерген consistency extractor жана бардык шарттарды канааттандырган киргизүүлөргө −1 фаза берген solution inverter бирге иштейт.

“Бардык чечимдерди бир учурда текшерүү” деген сөз айкашын этият чечмелөө керек. Суперпозициянын аркасында oracle бардык эсептөө-базис киргизүүлөрүн когеренттүү түрдө баалап, жарактуу абалдарды бир эле кванттык операциянын ичинде белгилей алат; бирок бир гана акыркы өлчөө бардык чечимдерди тизмек түрүндө чыгарып бербейт. Булактын өз тажрыйбасында алты башка чечимди алуу үчүн 1024 measurement shot колдонулган.

SMT маселеси SAT маселесинен эмнеси менен айырмаланат?

Boolean satisfiability (SAT) маселесинде өзгөрмөлөр түздөн-түз туура/жалган маанилерин алат. SMT болсо Boolean логикасын белгилүү бир математикалык теория менен бириктирет. Атом, мисалы, эки бит-вектордун теңдиги же чоңдук мамилеси болушу мүмкүн.

Изилдөө өзгөчө quantifier-free fixed-width bit-vector theory, кыскача \(\mathcal{BV}\), багытына топтолот. Бит-вектор туюнтмасы өзгөрмө, туруктуу же эки туюнтманын арифметикалык операциясы болушу мүмкүн. Изилдөөдө мисал катары келтирилген операция класстарына modulo кошуу, modulo көбөйтүү, bitwise операциялар, жылдыруу жана word concatenation кирет.

Атомдор болсо эки туюнтманы

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

салыштыргычтарынын бири менен байланыштырат.

Классикалык lazy SMT ыкмасы кандай иштейт?

Булактын 1-сүрөтүндө классикалык lazy ыкмасы үч негизги кадамга бөлүнөт:

1. Баштапкы SMT формуласы Boolean формулага абстракцияланат.
2. SAT чечкичи бул Boolean формула үчүн дайындоо табат.
3. Theory solver Boolean дайындоонун чыныгы теория өзгөрмөлөрү менен шайкеш же шайкеш эместигин текшерет.

Эгер дайындоо теориялык жактан шайкеш эмес болсо, SAT чечкичине кайра кайтып, башка 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-сүрөттө SAT чечкичинин алгачкы үч Boolean дайындоосу theory solver тарабынан четке кагылып, шайкеш чечим төртүнчү итерацияда гана табылат. Авторлордун кванттык ыкмага өтүшүнүн негизги мотивациясы ушул Boolean–теория кайра кайтуу цикли болуп саналат.

Кванттык ыкмадагы негизги идея эмне?

Эки 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 \]

абалы менен көрсөтүлөт.

Бул жети киргизүү бити үчүн \(2^7=128\) мүмкүн болгон эсептөө-базис киргизүүсү бар. Биринчи мисалда oracle ушул мүмкүн болгон бардык киргизүүлөрдүн суперпозициясында иштейт.

Киргизүү чечим болушу үчүн адегенде Boolean формуланы канааттандырышы керек:

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

Мындан тышкары Boolean абстракт өзгөрмөлөрү бит-вектор теориясындагы чыныгы маанилери менен шайкеш болушу керек:

\[ (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 жана теория шарттарын канааттандырган киргизүүнүн фазасын тескери бурат:

\[ \Psi(|v\rangle) = \begin{cases} -|v\rangle, & \text{Boolean формула жана бардык теория-шайкештик шарттары аткарылса},\\ |v\rangle, & \text{болбосо}. \end{cases} \]

Бул −1 фаза белгиси Grover diffuser кайсы базис абалдарынын өлчөө амплитудасын көбөйтөрүн аныктайт.

Булактын 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 иш жүзүндө колдонулган эмес.

Бул “квадраттык тездетүү” канчалык күчтүү жыйынтык?

Булак жыйынтык бөлүмүндө ыкма салттуу ыкмага салыштырмалуу теориялык квадраттык тездетүү берет деп билдирет. Бул сөз Grover издөө татаалдыгы контекстинде айтылган.

Изилдөө заманбап өнөр жай SMT чечкичтерине каршы чыныгы дубал-саат benchmark’ын жүргүзбөйт. Мындан тышкары oracle ичиндеги SAT, arithmetic, comparator, consistency жана uncomputation схемаларынын gate/depth чыгымдары маселенин өлчөмү менен кантип масштабданары боюнча толук end-to-end татаалдык анализи берилген эмес.

Ошондуктан жыйынтык “чыныгы кванттык компьютерде бардык классикалык SMT чечкичтеринен квадраттык түрдө тез иштей турганы эксперименталдык түрдө көрсөтүлдү” деп чечмеленбеши керек.

Oracle’дын төрт негизги бөлүгү

SAT схемасы кантип түзүлөт?

Авторлор 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-сүрөт бир үч-literal clause үчүн колдонулган схеманы көрсөтөт. 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, \]

жана бардык киргизүү literal биттери схема аягында баштапкы маанилерине кайтып келет:

\[ v'_i=v_i. \]

Экинчи жана үчүнчү касиеттер кванттык схеманын кайтарымдуу болушу жана ancilla’лар кийинки операцияларда кайра колдонулушу үчүн маанилүү.

Theorem 2: Толук 3-SAT формуласынын тууралыгы

7-сүрөттө эки ички формуланын output qubitтери бир CCNOT gate’инде бириктирилип

\[ F=F_1\wedge F_2 \]

эсептелет.

Theorem 2 түзүмдүк индукция аркылуу бул курулуш каалаган 3-SAT CNF формуласы үчүн

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

касиетин сактай турганын көрсөтөт.

Theory Circuit эмнени эсептейт?

Bit-vector theory тарабында ар бир атом

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

түрүндө болот.

Адегенде керектүү арифметикалык операциялар эсептелет. Андан кийин comparator схемасы эки bit-string ортосундагы мамилени эки output бит менен коддойт:

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

Булак comparator дизайнында \((1,1)\) абалы пайда болбой турганын белгилейт.

Бул эки output биттин негизинде алты салыштыруу түрү үчүн өзүнчө атом схемалары түзүлөт:

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

Theorem 3: Атом схемасынын тууралыгы

Theorem 3’түн жыйынтыгы түздөн-түз мындай:

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

Авторлор далил primitive quantum gate truth table’дарын текшерүү аркылуу түз алынарын айтып, барак чектөөсүнөн улам кеңири далилди бербей коюшат.

Theory Circuit бардык бит-вектор операцияларын толук аткарабы?

Изилдөө жалпы BV синтаксисинде ар кандай arithmetic operation түрлөрү болушу мүмкүн экенин билдирет; бирок бардык арифметикалык схемалардын кеңири gate-деңгээлдеги дизайнын бул макалада түзбөйт.

Арифметикалык операция блогу 8(a)-сүрөттө жалпы модуль катары көрсөтүлөт. Авторлор керектүү операцияларды primitive gate’терден түзүүгө же мурунку иштердеги quantum arithmetic схемаларын колдонууга болорун билдиришет.

Демек макала бардык BV операторлору үчүн башынан аягына чейин оптималдаштырылган өндүрүш деңгээлиндеги quantum-SMT software stack сунуштабайт. Анын салымы көбүрөөк SAT жана theory модулдарын бир Grover oracle архитектурасында кантип байланыштырууну системалаштыруу болуп саналат.

Consistency Extractor эмне үчүн керек?

Boolean абстракциясы өзү эле жетишсиз. Мисалы Boolean өзгөрмө бир атомду “туура” деп тандашы мүмкүн, бирок бит-вектор схемасы чыныгы маанилер үчүн ошол атом жалган экенин аныкташы мүмкүн.

Ошондуктан ар бир 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 формуланы канааттандыруу гана жетишсиз; бардык Boolean атомдор theory-domain маанилери менен да шайкеш болушу керек.

Solution Inverter эмне кылат?

10(b)-сүрөттөгү Solution Inverter бардык consistency биттери жана SAT output бити 1 болгондо \(q_{\mathrm{SMT}}\) qubitин активдештирет.

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 итерациясында киргизүү менен чырмалышып калып, diffuser күткөн түзүлүштү бузушу мүмкүн.

Ошондуктан SAT, theory, consistency жана solution-inverter эсептөөлөрүнүн тиешелүү бөлүктөрү тескери иретте колдонулуп, аралык qubitтер баштапкы абалдарына кайтарылат.

Бул операция quantum computing’деги uncomputation принцибинин макаладагы эквиваленти.

Баалоодо кайсы SMT формуласы колдонулат?

Авторлор экинчи, схемага көбүрөөк багытталган мисалда Boolean формуланы

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

деп тандашат.

Атомдор:

\[ 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” деген сөздү колдонот. Бирок андан кийин дароо берилген атомдордун баарында \(a\) жана \(b\) гана бар.

11-сүрөттөгү негизги SMT киргизүүлөрү да болгону

\[ a,\;b \]

биттерин камтыйт жана 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 жана \(a,b\) SMT өзгөрмөлөрү Hadamard gate’тери менен суперпозицияга алынат.

SAT circuit жана theory circuit сүрөттө ырааттуу көрүнгөнү менен, авторлор алардын ортосунда маалымат көз карандылыгы жок болгондуктан реалдуу колдонууда параллелдүү иштей аларын айтышат.

Theory бөлүмүндө:

• modulo adder,
• bitwise XOR,
• \((a+b)\) менен \((a\oplus b)\) ни салыштырган comparator,
• \((a+b)\) менен 1 ди салыштырган экинчи comparator

жайгашат.

Андан кийин consistency extractor, reverse circuit жана Grover diffusion circuit келет.

Эмне үчүн quantum counting колдонулган жок?

Grover итерацияларынын оптималдуу саны максаттуу чечимдердин саны \(M\) ге көз каранды. Негизинен авторлор сунуштаган ыкма quantum counting аркылуу \(M\) ни болжолдуу аныктоо болуп саналат.

Бирок баалоо схемасы буга чейин эле 32 qubit колдонуп, булакта колдонулган Qiskit чөйрөсүнүн 32-qubit чегине жеткени айтылат. Ошондуктан quantum counting схемасын кошууга мүмкүн болгон эмес.

Изилдөөчүлөр анын ордуна бир 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’дын маанилүү артыкчылыгы бардык жарактуу базис абалдарын бир суперпозицияда фаза боюнча белгилей алышы.

Бирок кванттык өлчөөдө бир shot бир гана classical bit-string берет. Демек “oracle 16 же 6 чечимди бир учурда тааныйт” менен “колдонуучу бир өлчөөдө бардык чечимдердин тизмесин алат” бир эле нерсе эмес.

Булактын эксперименталдык ыкмасы да муну ырастайт: алты башка чечим 1024 кайталанган өлчөөдө үлгүлөнөт.

Сүрөттөрдүн илимий ролу

Изилдөө колдогон жыйынтыктар

• Fixed-width bit-vector SMT маселелери үчүн Grover негизиндеги quantum oracle архитектурасын курууга болот.
• Boolean SAT шарттары жана bit-vector theory шарттары бир oracle ичинде чогуу бааланышы мүмкүн.
• 3-SAT CNF формулалары үчүн clause жана formula схемаларын конструктивдүү түрдө түзүүгө болот.
• Clause жана formula схемаларынын тууралыгы Theorem 1 жана Theorem 2 менен көрсөтүлгөн.
• Comparator чыгыштарынан алты негизги bit-vector салыштыруусу үчүн atom схемаларын түзүүгө болот.
• Consistency Extractor Boolean atom менен theory-domain atom бирдей чындык маанисине ээби же жокпу туура аныктайт.
• Solution Inverter бардык Boolean жана theory шарттарын канааттандырган абалдарга −1 фаза берет.
• Reverse circuit аралык qubitтерди тазалап, oracle’ды Grover итерацияларында кайра колдонууга мүмкүндүк берет.
• Qiskit симуляциясындагы үлгүлүү 32 qubitтик схемада алты туура SMT чечимдин өлчөнүү ыктымалдыгы жогорулатылган.
• Беш Grover итерациясы жана 1024 shot соңунда алты чечим жалпы 1017 жолу өлчөнүп, булак %99,32 чечим өлчөө ыктымалдыгын билдирген.
• Grover издөөсү жагынан чечим издөөдө теориялык издөө татаалдыгы классикалык сызыктуу издөөгө салыштырмалуу квадрат-тамыр масштабына түшүрүлүшү мүмкүн.

Изилдөө колдобогон же текшербеген жыйынтыктар

• Изилдөө реалдуу кванттык процессордо SMT чечимин аткарган эмес; баалоо Qiskit симуляциясы.
• %99,32 жыйынтыгы жалпы SMT маселелери үчүн ийгилик көрсөткүчү эмес; ал макаладагы конкреттүү кичинекей мисалдын 1024-shot симуляциясына гана тиешелүү.
• Бир quantum measurement бардык SMT чечимдерин тизмек түрүндө кайтарбайт.
• Чыныгы иштөө убактысында заманбап classical SMT solver’лерге салыштырмалуу квадраттык тездетүү эксперименталдык түрдө көрсөтүлгөн эмес.
• Oracle ичиндеги SAT, arithmetic, comparator жана uncomputation чыгымдарынын чоңойгон реалдуу маселелердеги жалпы gate/depth масштабдуулугу кең benchmark менен изилденген эмес.
• Бардык bit-vector arithmetic операторлору үчүн оптималдаштырылган gate-деңгээлдеги схема дизайны макалада берилбейт.
• Quantum counting баалоо схемасына колдонулган эмес; керектүү Grover итерация саны кичинекей мисалда эксперименталдык скан жана классикалык enumeration менен аныкталган.
• 32 qubitтик кичинекей мисалдан чоң өнөр жай formal-verification маселелери практикалык деп жыйынтык чыгарууга болбойт.
• Ыкманы башка SMT теорияларына кеңейтүүгө болот деген ой келечектеги изилдөө сунушу; макала бул теориялар үчүн иштеген oracle’дарды көрсөтпөйт.

Түркия жагынан кантип окуу керек?

Булак Түркияга тиешелүү эксперименталдык же тармактык маалыматтарды камтыбайт. Түркия жагынан изилдөө көбүрөөк кванттык программалык камсыздоо, formal verification, hardware verification жана EDA изилдөөлөрү үчүн методологиялык мисал катары бааланышы мүмкүн.

Өзгөчө bit-vector SMT процессор жана санариптик схема текшерүү маселелеринде көп колдонулган математикалык түзүлүштөрдүн бири. Бирок бул изилдөөдөн Түркиядагы учурдагы кванттык жабдык SMT чечүүгө даяр же классикалык текшерүү куралдары жакын арада ордун бошотот деген жыйынтык чыгарууга болбойт.

Изилдөөнүн Ыкмасы жана Жыйынтыктары

Изилдөөнүн түрү

Изилдөө теориялык компьютер илими жана кванттык эсептөө тармагындагы иш. Ыкма кванттык схема синтезин, математикалык тууралык далилдерин жана state-vector/circuit simulation ыкмасын бириктирет.

Жаңы физикалык эксперимент, реалдуу quantum processing unit benchmark’ы же өнөр жай SMT benchmark suite колдонулган эмес.

Методологиялык чынжыр

Тууралык далилдери

Изилдөө oracle архитектурасын симуляция жыйынтыгы менен гана негиздебейт; беш өзүнчө тууралык жыйынтыгын берет.

Баалоо схемасы

Баалоодо эки 2-bit SMT өзгөрмөсү жана үч Boolean abstract variable колдонулат. Theory circuit үчүн modulo adder, bitwise XOR жана эки comparator керек.

Макаланын Table I эсеби боюнча жалпы qubit керектөөсү 32.

11(a)-сүрөт SAT жана theory circuit схема чиймесинде ырааттуу көрүнгөнүнө карабай, алардын ортосунда маалымат көз карандылыгы жок болгондуктан параллелдүү аткарылышы мүмкүн экенин белгилейт.

Grover итерацияларын аныктоо

Булак максат саны белгилүү болгондо Grover итерация санын

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

менен байланыштырат.

Баалоодо quantum counting үчүн жетиштүү кошумча qubit калбагандыктан авторлор итерация санын 1ден көбөйтүп, measurement бөлүштүрүүсү бузулган бурулуш чекитин аныктап, 5 итерацияны тандашкан.

Чечим мейкиндигинин manual enumeration’у кийин бул тандоого шайкеш деп табылган.

Өлчөө жыйынтыгы

1024 shot ичиндеги алты жарактуу чечимдин counts маанилери:

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

деп билдирилген.

Эң жогорку count:

\[ 183 \]

менен `0010001`, эң төмөн count болсо

\[ 156 \]

менен `1001101` чечими.

Бирок бул кичинекей count айырмалары ыкмалар же чечимдер ортосунда сапат айырмасы бар дегенди билдирбейт. Grover amplification идеалдуу шартта бардык максаттардын амплитудаларын жогорулатат жана чектелген-shot sampling табигый статистикалык бөлүштүрүү түзөт. Булак бул алты чечимдин ортосунда статистикалык артыкчылык бар деп билдирбейт.

Изилдөөнүн эң күчтүү жагы

Изилдөөнүн эң күчтүү жагы классикалык SMTнин SAT жана theory бөлүктөрүн Grover oracle’га өткөрүү үчүн ачык модулдук архитектураны аныкташы.

Өзгөчө consistency extractor SMTнин Boolean абстракциясын кванттык схемада жөн гана “SAT чечимин табуу” маселесине кыскартып салууга жол бербейт. Theory-domain чындык маанилери да ошол эле oracle’дын максаттуу шартына киргизилет.

Изилдөөнүн негизги чектөөлөрү

Биринчи чектөө — масштаб. Болгону эки 2-bit SMT өзгөрмөсү колдонулган үлгүлүү схема 32 qubit талап кылат. Бит кеңдиги чоңойгондо arithmetic жана comparator модулдары тез эле кошумча ресурс талап кылышы мүмкүн.

Экинчи чектөө — баалоо ыкмасы. Реалдуу quantum hardware колдонулбагандыктан gate noise, decoherence, connectivity, routing жана error-correction чыгымдары моделденген эмес.

Үчүнчү чектөө — theoretical quadratic speedup end-to-end solver benchmark’ына айландырылган эмес. Grover oracle чакырууларынын саны square-root артыкчылык бергени менен, oracle’дын өз gate чыгымын көз жаздымда калтырууга болбойт.

Төртүнчү чектөө — максаттуу чечимдердин санын билбөө маселеси. Булак quantum counting’ди чечим катары көрсөтөт, бирок 32-qubit чектен улам өз тажрыйбасында колдонбойт.

Бешинчи чектөө — макала quantifier-free fixed-width BV теориясына гана багытталып, SAT тарабында 3-SAT CNF схема түзүлүшүн кеңири өнүктүргөн. Башка SMT теориялары келечектеги иш катары калтырылган.

Булак жана Ыкма Жөнүндө Эскертүү

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.

Авторлордун ирети: Жүктөлгөн булакта берилген ирет ошол бойдон сакталган.

Тең салым: Булакта тең салым же тең биринчи авторлук жөнүндө билдирүү жок.

Жооптуу автор: Булакта расмий 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 версиясы: v1, 16 Mart 2023.

arXiv-issued DOI: 10.48550/arXiv.2303.09353.

Hakemlik/yayın durumu: Каралган файл arXiv repository/preprint версиясы жана файлдын өзүндө hakemli журнал же конференция жарыясы тууралуу жазуу жок. Ошондуктан жүктөлгөн v1 hakemli version of record катары бааланган эмес.

Ошол эле аталыштагы 2026 жазуу тууралуу библиографиялык эскертүү: 2026 International Conference on Quantum Communications, Networking, and Computing жазууларында ошол эле аталыштагы конференциялык макала бар; бирок авторлор тизмеси 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 жок. Расмий булактарда эки жазуунун версиялык байланышы так ырасталбагандыктан 2026 конференциялык иш бул Verianla макаласында жүктөлгөн v1дин hakemli версиясы катары колдонулган эмес.

Лицензия: arXiv жазуусу Creative Commons Attribution 4.0 International (CC BY 4.0) лицензиясына багыттайт.

Каржылоо: Жүктөлгөн булакта өзүнчө каржылоо же grant тууралуу билдирүү жок.

Маалымат жеткиликтүүлүгү: Өзүнчө data-availability билдирүүсү жок. Изилдөө эксперименталдык маалымат топтомуна эмес, теориялык схема дизайнына жана Qiskit симуляциясына негизделет.

Кызыкчылыктардын кагылышы: Жүктөлгөн булакта өзүнчө conflict-of-interest билдирүүсү жок; мындан кызыкчылыктардын кагылышы жок деген кошумча жыйынтык чыгарылган эмес.

Автордук салымдар: Булакта CRediT же кеңири author-contributions билдирүүсү жок.

Булак ичиндеги дал келбестик: Текст формула/баалоо мисалы \(a,b,c\) аттуу үч 2-bit өзгөрмөнү камтыйт деп айтат; бирок көрсөтүлгөн атомдор, схема киргизүүлөрү жана чечим таблицасы \(a\) жана \(b\) гана колдонот. \(c\)нин баалоодогу функциясы булакта көрсөтүлбөгөндүктөн Verianla тексти муну өз алдынча толуктаган эмес.

Изилдөө ыкмасы: Grover search; quantum oracle construction; 3-SAT circuit synthesis; reversible CCNOT/CNOT/X/Z/H gate түзүлүштөрү; quantum arithmetic; quantum comparator; Boolean–theory consistency extraction; phase inversion; uncomputation/reverse circuit жана Qiskit simulation.

Баалоо шарты: Макаладагы негизги Qiskit мисалы 32 qubit, беш Grover итерациясы жана 1024 measurement shot колдонот. Алты жарактуу чечимдин жалпы count мааниси 1017 болуп, булак %99,32 solution-measurement probability деп билдирет.

Методологиялык чек: Изилдөөнүн теориялык квадраттык тездетүү жөнүндө сөзү Grover search complexity контекстинде. Булак реалдуу quantum hardware’де заманбап classical SMT solver’лер менен end-to-end runtime салыштыруусун жүргүзбөйт.

Илимий мазмун чеги: Бул Verianla макаласындагы алгоритм архитектурасы, формулалар, теоремалар, схема компоненттери, qubit ресурс таблицасы жана симуляция жыйынтыктары жүктөлгөн жети беттик arXiv:2303.09353v1 файлына негизделген. Тышкы булактар arXiv идентификаторун, лицензияны жана ошол эле аталыштагы 2026 конференция жазуусунун библиографиялык абалын текшерүү үчүн гана колдонулган; жүктөлгөн булакта жок илимий аткаруу жыйынтыгы кошулган эмес.

Verianla Live эскертүүсү: Булактын Tablo II’синдеги алты чечимдин measurement counts маанилери түздөн-түз бир эле симуляция шартына таандык болгондуктан `vlive-bar` колдонулган. Булакта классикалык жана кванттык SMT чечкичтеринин ортосунда реалдуу runtime benchmark жок болгондуктан теориялык тездетүү дооматы үчүн жасалма көрсөткүч графиги түзүлгөн эмес.