Utafiti huu unatengeneza mbinu inayotegemea saketi za quantum kwa ajili ya kutatua matatizo ya satisfiability modulo theory (SMT) ya nadharia ya bit-vector yenye upana usiobadilika kwa kutumia algoriti ya Grover. Badala ya kurudia kando hatua za kutengeneza suluhisho la Boolean na kukagua ulinganifu wa nadharia kama katika mbinu ya classical lazy-SMT, mbinu hii inawakilisha thamani zote zinazowezekana za vigezo vya Boolean na bit-vector katika quantum superposition; hutumia oracle yenye SAT circuit, theory circuit, consistency extractor na solution inverter kuweka alama ya awamu kwa suluhisho halali za SMT, kisha Grover diffuser huongeza uwezekano wa kupima suluhisho hizo. Katika tathmini ya mfano iliyofanywa kwenye Qiskit, saketi ya 32 qubit, marudio matano ya Grover na 1024 measurement shot zilitumika; suluhisho sita sahihi zilipimwa jumla ya mara 1017 na uwezekano wa kupima suluhisho uliripotiwa kuwa %99,32. Kizuizi kikuu cha utafiti ni kwamba tathmini ilifanywa kwa simulation kwenye mfano mdogo wa 2-bit na hakuna benchmark ya muda halisi wa utekelezaji, gharama ya gate au scalability dhidi ya SMT solver za kisasa za classical iliyowasilishwa.

Ubunifu wa makala hauishii tu kwenye kutumia algoriti ya Grover kwa tatizo la SMT. Waandishi wanapendekeza muundo wa kimfumo ili Grover oracle iweze kukagua tabaka mbili tofauti za kimantiki za SMT ndani ya saketi moja. SAT circuit kwa Boolean abstraction, arithmetic/comparator circuits zinazokokotoa misemo halisi ya bit-vector, consistency extractor inayokagua kama tabaka hizi mbili zinatoa thamani ileile ya ukweli, na solution inverter inayotoa awamu ya −1 kwa ingizo zinazokidhi masharti yote, hufanya kazi pamoja.

Kauli ya “kukagua suluhisho zote kwa wakati mmoja” inapaswa kufasiriwa kwa uangalifu. Kwa sababu ya superposition, oracle inaweza kutathmini kwa hali ya koherensi ingizo zote za computational basis na kuweka alama kwa hali halali ndani ya operesheni ileile ya quantum; hata hivyo kipimo kimoja cha mwisho hakiwezi kutoa suluhisho zote kama orodha. Katika jaribio la chanzo lenyewe, 1024 measurement shot zilitumika kupata suluhisho sita tofauti.

Tatizo la SMT linatofautianaje na tatizo la SAT?

Katika tatizo la Boolean satisfiability (SAT), vigezo huchukua moja kwa moja thamani za kweli/uongo. SMT huunganisha mantiki ya Boolean na nadharia fulani ya kihisabati. Atom inaweza kuwa, kwa mfano, usawa kati ya bit-vector mbili au uhusiano wa ukubwa kati yao.

Utafiti unalenga hasa quantifier-free fixed-width bit-vector theory, kwa kifupi \(\mathcal{BV}\). Usemi wa bit-vector unaweza kuwa kigezo, thamani thabiti au operesheni ya kihesabu kati ya misemo miwili. Miongoni mwa aina za operesheni zilizotolewa kama mifano katika utafiti ni modulo addition, modulo multiplication, bitwise operations, shifting na word concatenation.

Atom huunganisha misemo miwili kwa mojawapo ya vilinganishi

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

.

Mbinu ya classical lazy SMT hufanyaje kazi?

Kielelezo 1 cha chanzo kinagawanya mbinu ya classical lazy katika hatua kuu tatu:

1. Fomula ya awali ya SMT huwekwa katika Boolean abstraction.
2. SAT solver hutafuta assignment kwa fomula hii ya Boolean.
3. Theory solver hukagua kama assignment ya Boolean inaendana na vigezo halisi vya nadharia.

Ikiwa assignment haipatani kinadharia, mchakato hurudi kwa SAT solver na suluhisho jingine la Boolean hutafutwa.

Katika mfano wa kwanza, chanzo kinatumia

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

fomula.

Vigezo vya Boolean vinapofafanuliwa kama

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

fomula iliyofanyiwa abstraction huwa

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

.

Katika Kielelezo 1, assignment tatu za kwanza za Boolean zinazotolewa na SAT solver zinakataliwa na theory solver, na assignment inayolingana inapatikana tu katika iteration ya nne. Motisha kuu ya waandishi kuelekea mbinu ya quantum ni mzunguko huu wa kurudi kati ya Boolean na nadharia.

Wazo kuu katika mbinu ya quantum ni nini?

Vigezo viwili vya 2-bit

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

na vigezo vitatu vya Boolean abstraction \(x,y,z\) vinawakilishwa pamoja kwa hali

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

.

Kwa bit hizi saba za ingizo kuna \(2^7=128\) ingizo zinazowezekana za computational basis. Katika mfano wa kwanza, oracle hufanya kazi juu ya superposition ya ingizo hizi zote zinazowezekana.

Ili ingizo liwe suluhisho, lazima kwanza likidhi fomula ya Boolean:

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

Zaidi ya hayo, vigezo vya Boolean abstraction lazima viendane na maana zao halisi katika nadharia ya 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 huwekaje alama kwa suluhisho halali?

Oracle inayopendekezwa \(\Psi\) hugeuza awamu ya ingizo linalokidhi masharti yote ya Boolean na theory:

\[ \Psi(|v\rangle) = \begin{cases} -|v\rangle, & \text{ikiwa fomula ya Boolean na masharti yote ya theory-consistency yametimizwa},\\ |v\rangle, & \text{vinginevyo}. \end{cases} \]

Alama hii ya awamu −1 huamua ni hali zipi za basis ambazo Grover diffuser itaongeza amplitude ya kipimo chake.

Katika mfano wa kwanza wa Kielelezo 2 cha chanzo, oracle inaweza kuweka alama kwa awamu kwa suluhisho 16 halali za SMT miongoni mwa ingizo 128 zinazowezekana katika matumizi moja ya oracle.

Algoriti ya Grover huongezaje uwezekano wa suluhisho?

Katika algoriti ya Grover, operesheni mbili hurudiwa:

• Oracle hugeuza awamu ya hali zinazolengwa.
• Diffuser hugeuza amplitude kuzunguka wastani, na hivyo kuongeza uwezekano wa kupima hali zilizowekwa alama.

Katika utafutaji bora wenye elementi \(N\) na lengo moja, chanzo hutoa

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

operesheni za Grover dhidi ya utafutaji wa classical wa

\[ O(N) \]

kama quadratic speedup.

Kunapokuwa na malengo \(M\), idadi bora ya iterations ni takriban

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

.

Chanzo pia kinaeleza kuwa \(M\) huenda isijulikane mapema na kwamba quantum counting inaweza kutumika katika hali hiyo. Hata hivyo, katika tathmini ya Qiskit ya utafiti, quantum counting haikutekelezwa kwa sababu qubit za ziada zinazohitajika hazikupatikana.

“Quadratic speedup” hii ni hitimisho lenye nguvu kiasi gani?

Katika sehemu ya hitimisho, chanzo kinasema mbinu hiyo hutoa theoretical quadratic speedup dhidi ya mbinu ya jadi. Kauli hii iko katika muktadha wa search complexity ya Grover.

Utafiti haufanyi benchmark ya kweli ya wall-clock dhidi ya SMT solver za kisasa za viwandani. Pia hauwasilishi uchambuzi mpana wa end-to-end complexity unaoonyesha jinsi gate/depth costs za SAT, arithmetic, comparator, consistency na uncomputation circuits ndani ya oracle zinavyokua pamoja na ukubwa wa tatizo.

Kwa hiyo, matokeo hayapaswi kutafsiriwa kama “imeonyeshwa kwa majaribio kwamba kwenye kompyuta halisi ya quantum itafanya kazi kwa kasi ya quadratic kuliko SMT solver zote za classical”.

Vipengele vinne vya msingi vya Oracle

SAT circuit hutengenezwa vipi?

Waandishi wanafafanua upande wa SAT kwa njia ya kujenga kwa 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. \]

Kielelezo 6 kinaonyesha saketi inayotumika kwa clause moja ya literal tatu. Literal ikiwa chanya au constant 0, gate \(Q\) huchaguliwa kuwa \(X\); literal ikiwa hasi, gate \(Q\) huchaguliwa kuwa identity \(I\).

Ancilla qubit moja hutumika kwa hesabu ya kati ndani ya clause na output qubit tofauti hutumika kwa thamani ya ukweli ya clause.

Theorem 1: Usahihi wa saketi ya Clause

Theorem 1 inathibitisha sifa tatu:

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

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

na bit zote za literal za ingizo hurudi kwenye thamani zao za awali mwishoni mwa saketi:

\[ v'_i=v_i. \]

Sifa ya pili na ya tatu ni muhimu kwa sababu saketi ya quantum lazima iwe reversible na ancilla ziweze kutumiwa tena katika operesheni zinazofuata.

Theorem 2: Usahihi wa fomula kamili ya 3-SAT

Katika Kielelezo 7, output qubit za fomula mbili ndogo huunganishwa kwenye CCNOT gate moja ili kukokotoa

\[ F=F_1\wedge F_2 \]

.

Theorem 2 inaonyesha kwa structural induction kwamba ujenzi huu huhifadhi sifa

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

kwa fomula yoyote ya 3-SAT CNF.

Theory Circuit hukokotoa nini?

Kwenye upande wa bit-vector theory, kila atom ina umbo

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

.

Kwanza operesheni za kihesabu zinazohitajika hukokotolewa. Kisha comparator circuit huweka msimbo wa uhusiano kati ya bit-string mbili kwa output bit mbili:

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

Chanzo kinasema hali \((1,1)\) haitokei katika muundo wa comparator.

Kutokana na output bit hizi mbili, atom circuits tofauti huundwa kwa aina sita za comparison:

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

Theorem 3: Usahihi wa saketi ya Atom

Hitimisho la Theorem 3 ni moja kwa moja:

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

Waandishi wanasema uthibitisho hupatikana moja kwa moja kwa kuchunguza primitive quantum gate truth tables na hawaonyeshi uthibitisho wa kina kwa sababu ya kikomo cha kurasa.

Je, Theory Circuit hutekeleza operesheni zote za bit-vector kikamilifu?

Utafiti unaeleza kwamba sintaksia ya jumla ya BV inaweza kuwa na aina mbalimbali za arithmetic operation; hata hivyo, haujengi miundo ya kina ya gate-level kwa arithmetic circuits zote katika makala hii.

Arithmetic operation block inaonyeshwa kama moduli ya jumla katika Kielelezo 8(a). Waandishi wanaeleza kuwa operesheni zinazohitajika zinaweza kujengwa kutoka primitive gate au quantum arithmetic circuits za tafiti za awali zinaweza kutumiwa.

Kwa hiyo makala haitoi production-level quantum-SMT software stack iliyoboreshwa mwanzo hadi mwisho kwa operators zote za BV. Mchango wake ni zaidi katika kuweka mfumo wa jinsi SAT na theory modules zinavyounganishwa katika architecture moja ya Grover oracle.

Kwa nini Consistency Extractor inahitajika?

Boolean abstraction pekee haitoshi. Kwa mfano, kigezo cha Boolean kinaweza kuchagua atom kuwa “kweli”, lakini bit-vector circuit ikagundua kuwa atom hiyo ni uongo kwa thamani halisi.

Kwa hiyo kila Boolean abstract variable \(v_{B_i}\) hulinganishwa na matokeo halisi ya atom \(atom_i\).

Saketi ya Kielelezo 10(a) hutumia CNOT moja na kisha gate \(X\). Theorem 4:

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

Hivyo, haitoshi tu kukidhi fomula ya Boolean; atom zote za Boolean lazima pia ziwe na maana zinazolingana katika theory-domain.

Solution Inverter hufanya nini?

Solution Inverter ya Kielelezo 10(b) huamilisha qubit \(q_{\mathrm{SMT}}\) wakati consistency bit zote na SAT output bit ni 1.

Sharti la kwanza la Theorem 5:

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

hutimia ikiwa na ikiwa tu

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

na kwa kila \(i\)

\[ v_{B_i}\equiv atom_i \]

.

Kisha gate \(Z\) kwa kutumia sifa

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

hutoa awamu ya −1 kwa hali za suluhisho kamili.

Kwa nini Reverse Circuit ipo?

Hesabu za kati za oracle hutengeneza taarifa za muda kwenye ancilla na output qubit nyingi. Zisipofutwa, zinaweza kubaki entangled na ingizo katika iteration inayofuata ya Grover na kuharibu muundo unaotarajiwa na diffuser.

Kwa hiyo sehemu husika za hesabu za SAT, theory, consistency na solution-inverter hutekelezwa kwa mpangilio wa kinyume ili kurudisha qubit za kati kwenye hali zao za awali.

Operesheni hii ni matumizi ya kanuni ya uncomputation ya quantum computing katika makala.

Ni fomula gani ya SMT inayotumika katika tathmini?

Katika mfano wa pili, unaolenga zaidi saketi, waandishi huchagua fomula ya Boolean

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

.

Atom ni:

\[ x:(a+b

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

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

.

Hapa \(+\) ni fixed-width modulo-sum na \(\oplus\) ni bitwise exclusive-OR.

Kutolingana kwa “kigezo c” ndani ya chanzo

Maandishi ya tathmini yanatumia kauli “vigezo \(a,b,c\) vyote ni 2-bit”. Hata hivyo atom zote zinazoonyeshwa mara moja baada ya hapo zinatumia tu \(a\) na \(b\).

Ingizo kuu za SMT katika Kielelezo 11 pia zina bit za

\[ a,\;b \]

pekee, na Tablo II hutoa thamani kwa vigezo hivi viwili tu.

Kwa hiyo haiwezi kuthibitishwa kwamba \(c\) iliyotajwa katika chanzo ina jukumu halisi katika evaluation circuit. Maandishi ya Verianla yanahifadhi hili kama kutolingana kwa majina/maandishi ndani ya chanzo.

32 qubit zinatumika wapi?

Tablo I ya chanzo inaonyesha kwa kina matumizi ya qubit katika saketi ya tathmini:

Jumla:

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

Ukweli kwamba hata mfano mdogo wa 2-bit SMT unatumia 32 qubit ni mojawapo ya vikwazo muhimu vya utafiti kwa upande wa scalability ya vitendo.

Kielelezo 11 kinaonyesha nini?

Kielelezo 11(a) kinaonyesha saketi yote inayotathminiwa katika block diagram moja. Mwanzoni, Boolean abstract variables pamoja na vigezo vya SMT \(a,b\) huwekwa katika superposition kwa kutumia Hadamard gates.

Ingawa SAT circuit na theory circuit zinaonekana mfululizo katika mchoro, waandishi wanasema zinaweza kukimbia kwa sambamba katika utekelezaji halisi kwa sababu hakuna data dependency kati yake.

Katika sehemu ya Theory kuna:

• modulo adder,
• bitwise XOR,
• comparator inayolinganisha \((a+b)\) na \((a\oplus b)\),
• comparator ya pili inayolinganisha \((a+b)\) na 1

.

Kisha hufuata consistency extractor, reverse circuit na Grover diffusion circuit.

Kwa nini quantum counting haikutumika?

Idadi bora ya Grover iterations hutegemea idadi ya suluhisho lengwa \(M\). Kwa kawaida njia inayopendekezwa na waandishi ni kukadiria \(M\) kwa kutumia quantum counting.

Hata hivyo evaluation circuit tayari hutumia 32 qubit, na chanzo kinaeleza kuwa mazingira ya Qiskit yaliyotumika yalifikia kikomo cha 32-qubit. Kwa hiyo quantum counting circuit haikuweza kuongezwa.

Badala yake, watafiti walianza na iteration moja ya Grover, wakaongeza idadi ya iterations na kutafuta turning point ambapo measurement distribution ilianza kuwa mbaya.

Kwa jaribio hili, sehemu bora ilipatikana kuwa 5 Grover iterations. Waandishi baadaye wali-enumerate solution space kwa classical manual enumeration na kusema kuwa thamani hii inaendana na hesabu ya nadharia ya iterations za Grover.

Mbinu hii inaweza kutumika kwa jaribio la maonyesho, lakini si suluhisho la jumla kwa matatizo makubwa halisi ya SMT ambapo idadi ya suluhisho haijulikani mapema.

Matokeo kuu ya simulation

Baada ya iterations tano za Grover, saketi ilipimwa mara 1024. Tablo II ya chanzo inaripoti suluhisho sita kama ifuatavyo:

Kwa kuwa jumla ya idadi ya vipimo vya suluhisho hizi sita ni

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

chanzo kinatoa

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

na kuripoti uwezekano wa kupima suluhisho kuwa %99,32.

Kauli ya “inapata suluhisho zote” inapaswa kutafsiriwaje?

Faida muhimu ya oracle ni uwezo wa kuweka alama kwa awamu kwa hali zote halali za basis ndani ya superposition moja.

Lakini katika quantum measurement, shot moja hutoa classical bit-string moja tu. Kwa hiyo “oracle inatambua suluhisho 16 au 6 kwa wakati mmoja” si sawa na “mtumiaji anapata orodha ya suluhisho zote kwa kipimo kimoja”.

Mbinu ya majaribio ya chanzo pia inathibitisha hili: suluhisho sita tofauti zinachukuliwa sampuli ndani ya vipimo 1024 vya kurudia.

Jukumu la kisayansi la vielelezo

Matokeo yanayoungwa mkono na utafiti

• Architecture ya quantum oracle inayotegemea Grover inaweza kujengwa kwa matatizo ya fixed-width bit-vector SMT.
• Masharti ya Boolean SAT na bit-vector theory yanaweza kutathminiwa pamoja ndani ya oracle moja.
• Clause na formula circuits zinaweza kujengwa kwa njia ya konstruktivu kwa fomula za 3-SAT CNF.
• Usahihi wa clause na formula circuits umeonyeshwa kwa Theorem 1 na Theorem 2.
• Atom circuits zinaweza kujengwa kwa comparisons sita za msingi za bit-vector kutoka kwa comparator outputs.
• Consistency Extractor huamua kwa usahihi kama Boolean atom na theory-domain atom zina thamani ileile ya ukweli.
• Solution Inverter hutoa awamu ya −1 kwa hali zinazokidhi masharti yote ya Boolean na theory.
• Reverse circuit husafisha qubit za kati na kuruhusu oracle kutumiwa tena katika Grover iterations.
• Katika mfano wa Qiskit simulation wa saketi ya 32 qubit, suluhisho sita sahihi za SMT ziliimarishwa hadi uwezekano mkubwa wa kipimo.
• Baada ya iterations tano za Grover na 1024 shot, suluhisho sita zilipimwa jumla ya mara 1017 na chanzo kiliripoti uwezekano wa kupima suluhisho wa %99,32.
• Kwa mtazamo wa Grover search, theoretical search complexity ya kutafuta suluhisho inaweza kupunguzwa kutoka linear classical search hadi square-root scale.

Matokeo ambayo utafiti hauungi mkono au haujajaribu

• Utafiti haukutatua SMT kwenye quantum processor halisi; tathmini ni Qiskit simulation.
• Matokeo ya %99,32 si success rate ya matatizo yote ya SMT; yanahusu tu 1024-shot simulation ya mfano maalum mdogo wa makala.
• Quantum measurement moja hairudishi suluhisho zote za SMT kama orodha.
• Quadratic speedup dhidi ya modern classical SMT solver haijaonyeshwa kwa majaribio katika muda halisi wa utekelezaji.
• Scalability ya jumla ya gate/depth cost za SAT, arithmetic, comparator na uncomputation ndani ya oracle kwa matatizo makubwa halisi haijachunguzwa kwa benchmark pana.
• Miundo ya optimized gate-level circuit kwa bit-vector arithmetic operators zote haijatolewa katika makala.
• Quantum counting haikutumika kwenye evaluation circuit; idadi ya Grover iterations inayohitajika iliamuliwa kwenye mfano mdogo kwa experimental scan na classical enumeration.
• Haiwezi kuhitimishwa kutoka mfano mdogo wa 32 qubit kwamba matatizo makubwa ya industrial formal-verification yanaweza kutekelezwa kwa vitendo.
• Kupanua mbinu kwenda SMT theories nyingine ni pendekezo la kazi ya baadaye; makala haionyeshi oracle zinazofanya kazi kwa theories hizo.

Inapaswa kusomwaje kwa mtazamo wa Türkiye?

Chanzo hakina data ya majaribio au ya kisekta inayohusu Türkiye moja kwa moja. Kwa mtazamo wa Türkiye, utafiti unaweza kuonekana zaidi kama mfano wa kimetodolojia kwa quantum software, formal verification, hardware verification na utafiti wa EDA.

Hasa bit-vector SMT ni mojawapo ya miundo ya kihisabati inayotumika mara kwa mara katika verification ya processor na digital circuits. Hata hivyo, utafiti huu hauonyeshi kwamba quantum hardware iliyopo Türkiye iko tayari kutatua SMT au kwamba zana za classical verification zitabadilishwa katika muda mfupi.

Mbinu na Matokeo ya Utafiti

Aina ya utafiti

Utafiti ni wa theoretical computer science na quantum computing. Mbinu inaunganisha quantum circuit synthesis, mathematical correctness proofs na state-vector/circuit simulation approach.

Hakuna physical experiment mpya, real quantum processing unit benchmark au industrial SMT benchmark suite iliyotumika.

Mlolongo wa kimetodolojia

Uthibitisho wa usahihi

Utafiti hautetei architecture ya oracle kwa matokeo ya simulation pekee; unatoa matokeo matano tofauti ya correctness.

Saketi ya tathmini

Tathmini hutumia vigezo viwili vya 2-bit SMT na Boolean abstract variables tatu. Theory circuit inahitaji modulo adder, bitwise XOR na comparator mbili.

Kulingana na hesabu ya Table I ya makala, mahitaji ya jumla ni 32 qubit.

Kielelezo 11(a) kinaeleza kwamba ingawa SAT na theory circuit zinaonekana mfululizo katika mchoro wa saketi, zinaweza kutekelezwa kwa sambamba kwa sababu hakuna data dependency kati yao.

Kuamua Grover iterations

Chanzo huunganisha idadi ya Grover iterations, wakati idadi ya malengo inajulikana, na

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

.

Kwa sababu hakukuwa na qubit za ziada za kutosha kwa quantum counting katika tathmini, waandishi waliongeza idadi ya iterations kuanzia 1, wakatambua turning point ambapo measurement distribution ilianza kuharibika na wakaamua kutumia iterations 5.

Manual enumeration ya solution space ilionekana baadaye kuwa inalingana na chaguo hili.

Matokeo ya kipimo

Counts values za suluhisho sita halali ndani ya 1024 shot ziliripotiwa kuwa:

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

.

Count ya juu zaidi:

\[ 183 \]

kwa `0010001`, na count ya chini zaidi:

\[ 156 \]

kwa `1001101`.

Hata hivyo tofauti hizi ndogo za count hazimaanishi tofauti ya ubora kati ya mbinu au suluhisho. Grover amplification katika hali bora huongeza amplitudes za malengo yote, na finite-shot sampling huzalisha usambazaji wa kawaida wa takwimu. Chanzo hakidai statistical superiority kati ya suluhisho hizi sita.

Nguvu kuu ya utafiti

Nguvu kuu ya utafiti ni kwamba unafafanua architecture ya moduli iliyo wazi kwa ajili ya kuhamisha sehemu za SAT na theory za classical SMT kwenda kwenye Grover oracle.

Hasa consistency extractor huzuia Boolean abstraction ya SMT kupunguzwa kuwa tatizo la “kupata SAT solution” pekee ndani ya quantum circuit. Theory-domain truth values pia hujumuishwa katika target condition ya oracle ileile.

Vikwazo vikuu vya utafiti

Kizuizi cha kwanza ni scale. Saketi ya mfano inayotumia vigezo viwili tu vya 2-bit SMT inahitaji 32 qubit. Kwa bit-width kubwa, arithmetic na comparator modules zinaweza kuhitaji rasilimali za ziada kwa kasi.

Kizuizi cha pili ni mbinu ya tathmini. Kwa kuwa real quantum hardware haikutumika, gate noise, decoherence, connectivity, routing na error-correction costs hazikuwekwa kwenye modeli.

Kizuizi cha tatu ni kwamba theoretical quadratic speedup haijageuzwa kuwa end-to-end solver benchmark. Ingawa idadi ya Grover oracle calls hutoa square-root advantage, gate cost ya oracle yenyewe haiwezi kupuuzwa.

Kizuizi cha nne ni tatizo la kutokujua idadi ya target solutions. Chanzo kinataja quantum counting kama suluhisho, lakini hakitumii katika jaribio lake kwa sababu ya 32-qubit limit.

Kizuizi cha tano ni kwamba makala inalenga quantifier-free fixed-width BV theory pekee na inaendeleza kwa kina muundo wa 3-SAT CNF circuit upande wa SAT. SMT theories nyingine zimeachwa kwa kazi ya baadaye.

Maelezo ya Chanzo na Mbinu

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

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

Mpangilio wa waandishi: Mpangilio uliotolewa katika chanzo kilichopakiwa umehifadhiwa bila kubadilishwa.

Mchango sawa: Chanzo hakina tamko la equal contribution au co-first authorship.

Mwandishi wa mawasiliano: Chanzo hakina alama rasmi ya corresponding-author. Anwani za e-mail za mawasiliano zimetolewa kwa Shang-Wei Lin na Yean-Ru Chen.

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

Eneo la kisayansi: Logic in Computer Science, quantum computing, formal verification, satisfiability modulo theories na fixed-width bit-vector solving.

Chanzo kilichokaguliwa: arXiv:2303.09353v1 [cs.LO].

Toleo la kwanza na lililokaguliwa la arXiv: v1, 16 Mart 2023.

arXiv-issued DOI: 10.48550/arXiv.2303.09353.

Hakemlik/yayın durumu: Faili iliyokaguliwa ni arXiv repository/preprint version na faili yenyewe haina record ya peer-reviewed journal au conference publication. Kwa hiyo v1 iliyopakiwa haijatathminiwa kama peer-reviewed version of record.

Dokezo la bibliografia kuhusu record ya 2026 yenye jina lilelile: Katika records za 2026 International Conference on Quantum Communications, Networking, and Computing kuna conference paper yenye title ileile; hata hivyo author list ni Shang-Wei Lin, Si-Han Chen, Lei-Han Yao, Yu-Chung Chen na Yean-Ru Chen. Katika v1 iliyopakiwa, Tzu-Fan Wang yupo, huku Lei-Han Yao na Yu-Chung Chen hawapo. Kwa kuwa uhusiano wa version kati ya records hizi mbili haujathibitishwa wazi katika sources rasmi, conference work ya 2026 haikutumika katika makala hii ya Verianla kama peer-reviewed version ya v1 iliyopakiwa.

Leseni: Record ya arXiv inaelekeza kwenye Creative Commons Attribution 4.0 International (CC BY 4.0).

Ufadhili: Hakuna funding au grant statement tofauti katika chanzo kilichopakiwa.

Upatikanaji wa data: Hakuna data-availability statement tofauti. Utafiti hautegemei experimental dataset bali theoretical circuit design na Qiskit simulation.

Mgongano wa maslahi: Hakuna conflict-of-interest statement tofauti katika chanzo kilichopakiwa; kutokana na hilo, hitimisho la ziada kwamba hakuna conflict of interest halijatolewa.

Michango ya waandishi: Chanzo hakina CRediT au detailed author-contributions statement.

Kutolingana ndani ya chanzo: Maandishi yanasema formula/evaluation example ina vigezo vitatu vya 2-bit vinavyoitwa \(a,b,c\); hata hivyo atom zilizoonyeshwa, circuit inputs na solution table hutumia tu \(a\) na \(b\). Kwa kuwa kazi ya \(c\) katika evaluation haijaonyeshwa katika chanzo, maandishi ya Verianla hayajaijaza kimya kimya.

Mbinu ya utafiti: 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 na Qiskit simulation.

Sharti la tathmini: Mfano mkuu wa Qiskit katika makala hutumia 32 qubit, iterations tano za Grover na 1024 measurement shot. Total count ya suluhisho sita halali ni 1017 na chanzo kinaripoti %99,32 solution-measurement probability.

Kikomo cha kimetodolojia: Kauli ya theoretical quadratic speedup katika utafiti iko katika muktadha wa Grover search complexity. Chanzo hakifanyi end-to-end runtime comparison kwenye real quantum hardware dhidi ya modern classical SMT solver.

Kikomo cha maudhui ya kisayansi: Algorithm architecture, formulas, theorems, circuit components, qubit resource table na simulation results katika makala hii ya Verianla zinategemea faili ya kurasa saba ya arXiv:2303.09353v1 iliyopakiwa. External sources zilitumika tu kukagua arXiv identity, license na bibliographic status ya conference record ya 2026 yenye title ileile; hakuna scientific performance result isiyokuwepo katika chanzo kilichopakiwa iliyoongezwa.

Verianla Live note: Kwa sababu measurement counts values za suluhisho sita katika Tablo II ya chanzo zilitoka moja kwa moja kwenye simulation condition ileile, `vlive-bar` imetumika. Kwa kuwa chanzo hakina real runtime benchmark kati ya classical na quantum SMT solvers, hakuna artificial performance chart iliyoundwa kwa ajili ya theoretical speedup claim.