pith. sign in

arxiv: 2605.25756 · v1 · pith:ARFSQNWGnew · submitted 2026-05-25 · 🪐 quant-ph

QGCL: Quantum-Guided Clause Learning for Cryptanalytic SAT

Walid El Maouaki , Alberto Marchisio , Muhammad Shafique This is my paper

Pith reviewed 2026-06-29 21:30 UTC · model grok-4.3

classification 🪐 quant-ph
keywords quantum-guided SATGrover searchCDCLcryptanalytic SATAESpower side-channelhybrid quantum-classicalconflict-driven clause learning
0
0 comments X

The pith

A hybrid solver applies Grover search to small subformulas around CDCL conflict cores to bias branching and cut conflicts by up to 86 percent in large AES cryptanalytic SAT instances.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces QGCL, a method that keeps the main SAT solving process classical but calls Grover search only on small, dynamically chosen subformulas extracted near conflict points. These quantum calls return candidate assignments that steer the classical branching heuristic toward more promising directions. The approach is evaluated on structured SAT formulas encoding AES power side-channel attacks, with up to about 39,000 variables. A sympathetic reader would care because full Grover search on the entire formula is currently impossible, so the work tests whether limited quantum resources can still deliver measurable help on real cryptographic search problems.

Core claim

QGCL invokes Grover search only on small subformulas extracted dynamically around CDCL conflict cores. The quantum subsolver returns candidate assignments and violation scores that bias branching heuristics, while final SAT/UNSAT decisions and key verification remain classical. Experiments on AES-oriented power-SCA instances show consistent reductions in solver-internal statistics on harder instances, with up to an 86 percent reduction in conflicts compared with the classical baseline. Parameter sweeps identify regimes where modest quantum resources capture most of the observed improvement.

What carries the argument

The QGCL framework, in which Grover search on dynamically extracted small subformulas around CDCL conflict cores supplies candidate assignments and violation scores to bias classical branching heuristics.

If this is right

  • Solver statistics such as conflicts, restarts, decisions, and propagations decrease on harder instances.
  • Most of the measured improvement occurs with a modest number of Grover oracle calls and small subproblem sizes.
  • Final key verification stays entirely classical, avoiding any requirement for quantum search over the full formula.
  • The method targets highly structured, large CNFs that arise from cryptographic specifications rather than random formulas.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the subformula extraction remains effective, the same selective quantum guidance pattern could be tested on other structured SAT domains such as hardware verification or planning.
  • Improvements in quantum hardware that allow modestly larger subformulas might widen the gap between QGCL and classical CDCL.
  • The approach illustrates a middle path in which quantum resources assist rather than replace classical solvers on near-term devices.

Load-bearing premise

Grover search on small dynamically extracted subformulas around CDCL conflict cores supplies useful guidance to branching heuristics and the added quantum overhead does not erase the net benefit.

What would settle it

A direct comparison on the same AES-derived SAT instances in which disabling the quantum guidance or replacing it with random suggestions produces no reduction in conflicts or total decisions.

Figures

Figures reproduced from arXiv: 2605.25756 by Alberto Marchisio, Muhammad Shafique, Walid El Maouaki.

Figure 1
Figure 1. Figure 1: Asymptotic scaling motivation for applying Grover search to sufficiently [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: SAT-assisted AES-128 power side-channel key-recovery workflow. Power traces from the target are translated into hard leakage predicates and, when [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: Circuit sketch for SAT-oracle building blocks. (a) Clause-violation [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figure 3
Figure 3. Figure 3: High-level control flow of the proposed QGCL solver. A standard [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Schematic illustration of BFS-based subformula extraction and simplification from an input CNF formula. Each clause [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Grover-subsolver output distributions for small CNF formulas used to [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Comparison of the CDCL baseline (blue) and the QGCL hybrid [PITH_FULL_IMAGE:figures/full_fig_p008_7.png] view at source ↗
Figure 9
Figure 9. Figure 9: QGCL performance when varying the Grover budget, defined as the [PITH_FULL_IMAGE:figures/full_fig_p009_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Extraction strategies in QGCL on the T = 2 Power SCA CNF instance. Structured localization, especially activity-BFS and variable-frontier (VF), reduces search effort and wall time more effectively than random extraction. small, dynamically selected subformulas and keeps final correctness classical. It is not yet NISQ-efficient in wall time. Addressing this limitation will require noise-aware oracle synthe… view at source ↗
read the original abstract

Power side-channel attacks on AES exploit data-dependent physical leakage to recover secret keys, but turning noisy leakage observations into a verified AES-128 key remains a hard combinational search problem. SAT-assisted power side-channel cryptanalysis addresses this challenge by encoding AES semantics, key constraints, plaintext/ciphertext consistency, and leakage predicates as CNF, so that candidate keys must satisfy the exact cryptographic specification. These cryptanalytic SAT formulas are large and highly structured; our largest controlled AES-oriented power-SCA instances contain up to 39,389 variables and 137,712 clauses, making a full-formula Grover search well beyond the scale studied here and beyond currently practical near-term implementations. We propose QGCL, a Quantum-Guided Conflict-Driven Clause Learning (CDCL) framework in which Grover search is invoked only on small subformulas extracted dynamically around CDCL conflict cores. The quantum subsolver returns candidate assignments and violation scores that bias branching heuristics, while final SAT/UNSAT decisions and key verification remain classical. We evaluate QGCL on AES-oriented cryptanalytic SAT instances derived from power side-channel CNFs with leakage-derived hint configurations, measuring conflicts, restarts, decisions, and propagations. The experiments show consistent reductions in these solver-internal statistics on harder instances, with up to an 86% reduction in conflicts compared with the classical conflict-learning baseline. Parameter sweeps over the number of Grover oracle calls and the subproblem size identify a regime in which a modest quantum resource allocation captures most of the observed improvement.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces QGCL, a hybrid Quantum-Guided Conflict-Driven Clause Learning framework for cryptanalytic SAT instances arising from AES power side-channel attacks. Grover search is invoked exclusively on small, dynamically extracted subformulas centered on CDCL conflict cores; the quantum routine supplies candidate assignments and violation scores that bias the classical solver's branching heuristics, while all final SAT/UNSAT decisions and key verification remain classical. Experiments on AES-derived CNFs (up to 39 389 variables) report consistent reductions in solver-internal statistics, reaching an 86 % drop in conflicts versus a plain CDCL baseline, together with parameter sweeps over Grover oracle calls and subproblem size.

Significance. If the reported reductions can be attributed to the quantum guidance rather than the subformula extraction heuristic, the work would establish a concrete, near-term-compatible route for injecting limited quantum oracles into classical CDCL solvers on highly structured cryptanalytic problems. The design choice to restrict quantum calls to small cores and to keep all logical decisions classical is a pragmatic strength that aligns with current hardware constraints. The parameter-sweep results that identify a modest-resource regime capturing most of the gain are also useful. However, the absence of any control that isolates the quantum component from the extraction procedure substantially weakens the evidential basis for these claims.

major comments (2)
  1. [Experimental evaluation] Experimental evaluation (abstract and § on results): the central claim of up to an 86 % reduction in conflicts (and corresponding drops in restarts, decisions, and propagations) is presented without any description of the number of instances, instance selection criteria, statistical analysis, or variance across runs. This information is load-bearing for assessing whether the observed improvements are robust.
  2. [Experimental evaluation] Experimental evaluation: no ablation is reported that applies identical dynamic subformula extraction around conflict cores but replaces the Grover oracle with a classical subsolver (e.g., exhaustive enumeration or a lightweight CDCL run on the same small core) to generate the biasing assignments and violation scores. Without this control, the reductions are consistent with either the quantum component or the extraction heuristic being responsible; the manuscript therefore does not distinguish the two.
minor comments (2)
  1. The abstract states that the largest instances contain 39 389 variables and 137 712 clauses; it would be helpful to list the exact instance sizes and leakage-hint configurations used in the reported runs.
  2. Notation for the violation scores returned by the quantum subsolver should be defined explicitly when first introduced.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on our manuscript. We address each major comment below and will revise the paper accordingly to improve the experimental evaluation section.

read point-by-point responses

  1. Referee: Experimental evaluation (abstract and § on results): the central claim of up to an 86 % reduction in conflicts (and corresponding drops in restarts, decisions, and propagations) is presented without any description of the number of instances, instance selection criteria, statistical analysis, or variance across runs. This information is load-bearing for assessing whether the observed improvements are robust.

    Authors: We agree that the manuscript should provide these details for proper assessment of robustness. In the revised version we will add a dedicated experimental setup subsection that specifies the full set of AES-derived instances used, the selection criteria based on leakage hint configurations and instance difficulty, and reports mean values together with standard deviations across multiple independent runs with different random seeds for the classical components. revision: yes

  2. Referee: Experimental evaluation: no ablation is reported that applies identical dynamic subformula extraction around conflict cores but replaces the Grover oracle with a classical subsolver (e.g., exhaustive enumeration or a lightweight CDCL run on the same small core) to generate the biasing assignments and violation scores. Without this control, the reductions are consistent with either the quantum component or the extraction heuristic being responsible; the manuscript therefore does not distinguish the two.

    Authors: We acknowledge that the current results do not isolate the quantum oracle from the subformula extraction heuristic. We will add an ablation study in the revision that applies the identical extraction procedure but substitutes a classical random sampler for the Grover-generated assignments and violation scores. While exhaustive enumeration or a full lightweight CDCL on every core is not practical at the scale of our larger instances, the random baseline will provide a direct control for the contribution of the quantum component. revision: yes

Circularity Check

0 steps flagged

No significant circularity; empirical comparison stands on direct measurement

full rationale

The paper's central claim rests on an empirical head-to-head comparison of QGCL (Grover-guided CDCL on extracted subformulas) versus plain classical CDCL, reporting measured reductions in conflicts, restarts, decisions and propagations on AES-derived SAT instances. No equations, parameters or predictions are defined in terms of the target statistics; the subformula extraction and Grover calls are external procedures whose outputs are fed into an otherwise standard CDCL loop whose termination and verification remain classical. No self-citations are invoked to justify uniqueness or to close a derivation loop. The absence of an ablation control (classical subsolver on identical subformulas) is a methodological limitation that affects causal attribution but does not render any reported statistic equivalent to its input by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The abstract does not detail any free parameters, axioms, or new entities introduced.

pith-pipeline@v0.9.1-grok · 5808 in / 1079 out tokens · 34470 ms · 2026-06-29T21:30:46.226772+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

40 extracted references · 3 canonical work pages · 2 internal anchors

  1. [1]

    Improved algebraic side-channel attack on aes,

    M. S. E. Mohamed, S. Bulygin, M. Zohner, A. Heuser, M. Walter, and J. Buchmann, “Improved algebraic side-channel attack on aes,”Journal of Cryptographic Engineering, vol. 3, no. 3, pp. 139–156, 2013

    2013

  2. [2]

    Solving aes-sat using side-channel hints: A practical assessment,

    E. Dubrova, “Solving aes-sat using side-channel hints: A practical assessment,” in2025 IEEE 55th International Symposium on Multiple- Valued Logic (ISMVL). IEEE Computer Society, 2025, pp. 147–152

    2025

  3. [3]

    Algebraic side-channel attacks,

    M. Renauld and F.-X. Standaert, “Algebraic side-channel attacks,” inInternational Conference on Information Security and Cryptology. Springer, 2009, pp. 393–410

    2009

  4. [4]

    Simplest normal truth functions,

    R. J. Nelson, “Simplest normal truth functions,”The journal of symbolic logic, vol. 20, no. 2, pp. 105–108, 1955

    1955

  5. [5]

    Solving difficult sat instances in the presence of symmetry,

    F. A. Aloul, A. Ramani, I. L. Markov, and K. A. Sakallah, “Solving difficult sat instances in the presence of symmetry,” inProceedings of the 39th annual Design Automation Conference, 2002, pp. 731–736

    2002

  6. [6]

    Proof complexity and sat solving,

    A. Biere, M. Heule, H. van Maaren, and T. Walsh, “Proof complexity and sat solving,”Handbook of Satisfiability, p. 233, 2021

    2021

  7. [7]

    Applying grover’s algorithm to aes: quantum resource estimates,

    M. Grassl, B. Langenberg, M. Roetteler, and R. Steinwandt, “Applying grover’s algorithm to aes: quantum resource estimates,” inInternational Workshop on Post-Quantum Cryptography. Springer, 2016, pp. 29–43

    2016

  8. [8]

    Implementing grover oracles for quantum key search on aes and lowmc,

    S. Jaques, M. Naehrig, M. Roetteler, and F. Virdia, “Implementing grover oracles for quantum key search on aes and lowmc,” in Annual International Conference on the Theory and Applications of Cryptographic Techniques. Springer, 2020, pp. 280–310

    2020

  9. [9]

    On the practical cost of grover for aes key recovery,

    D. Sarah and C. Peter, “On the practical cost of grover for aes key recovery,” in5th NIST PQC standardization conference, 2024

    2024

  10. [10]

    Hybrid quantum-classical neural networks,

    D. Arthur and P. Date, “Hybrid quantum-classical neural networks,” in2022 IEEE international conference on quantum computing and engineering (QCE). IEEE, 2022, pp. 49–55

    2022

  11. [11]

    Robqunns: A methodology for robust quanvolutional neural networks against adversarial attacks,

    W. El Maouaki, A. Marchisio, T. Said, M. Shafique, and M. Bennai, “Robqunns: A methodology for robust quanvolutional neural networks against adversarial attacks,” in2024 IEEE International Conference on Image Processing Challenges and Workshops (ICIPCW). IEEE, 2024, pp. 4090–4095

    2024

  12. [12]

    Advqunn: A methodology for analyzing the adversarial robustness of quanvolutional neural networks,

    W. El Maouaki, A. Marchisio, T. Said, M. Bennai, and M. Shafique, “Advqunn: A methodology for analyzing the adversarial robustness of quanvolutional neural networks,” in2024 IEEE International Conference on Quantum Software (QSW). IEEE, 2024, pp. 175–181

    2024

  13. [13]

    Designing robust quantum neural networks via optimized circuit metrics,

    W. El Maouaki, A. Marchisio, T. Said, M. Shafique, and M. Bennai, “Designing robust quantum neural networks via optimized circuit metrics,” Advanced Quantum Technologies, vol. 8, no. 6, p. 2400601, 2025

    2025

  14. [14]

    Cryptominisat switches-optimization for solving cryptographic instances,

    A.-M. Leventi-Peetz, O. Zendel, W. Lennartz, and K. Weber, “Cryptominisat switches-optimization for solving cryptographic instances,” arXiv preprint arXiv:2112.11484, 2021

    work page arXiv 2021

  15. [15]

    Solving aes-sat using side-channel hints: A practical assessment,

    E. Dubrova, “Solving aes-sat using side-channel hints: A practical assessment,”Cryptology ePrint Archive, 2024

    2024

  16. [16]

    Formal verification of software countermeasures against side-channel attacks,

    H. Eldib, C. Wang, and P. Schaumont, “Formal verification of software countermeasures against side-channel attacks,”ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 24, no. 2, pp. 1–24, 2014

    2014

  17. [17]

    Minisat-a sat solver with conflict-clause minimization,

    N. Een, “Minisat-a sat solver with conflict-clause minimization,”Proc. Theory and Applications of Satisfiability Testing (SAT 05), 2005

    2005

  18. [18]

    Smt-based verification of software countermeasures against side-channel attacks,

    H. Eldib, C. Wang, and P. Schaumont, “Smt-based verification of software countermeasures against side-channel attacks,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2014, pp. 62–77

    2014

  19. [19]

    Conflict-driven clause learning sat solvers,

    J. Marques-Silva, I. Lynce, and S. Malik, “Conflict-driven clause learning sat solvers,”Handbook of satisfiability, pp. 131–153, 2009

    2009

  20. [20]

    Chaff: Engineering an efficient sat solver,

    M. W. Moskewicz, C. F. Madigan, Y . Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an efficient sat solver,” inProceedings of the 38th annual Design Automation Conference, 2001, pp. 530–535

    2001

  21. [21]

    A lightweight component caching scheme for satisfiability solvers,

    K. Pipatsrisawat and A. Darwiche, “A lightweight component caching scheme for satisfiability solvers,” inInternational conference on theory and applications of satisfiability testing. Springer, 2007, pp. 294–299

    2007

  22. [22]

    The effect of restarts on the efficiency of clause learning

    J. Huanget al., “The effect of restarts on the efficiency of clause learning.” inIJCAI, vol. 7, 2007, pp. 2318–2323

    2007

  23. [23]

    An extensible sat-solver,

    N. E ´en and N. S ¨orensson, “An extensible sat-solver,” inInternational conference on theory and applications of satisfiability testing. Springer, 2003, pp. 502–518

    2003

  24. [24]

    Predicting learnt clauses quality in modern sat solvers

    G. Audemard and L. Simon, “Predicting learnt clauses quality in modern sat solvers.” inIJCAI, vol. 9, 2009, pp. 399–404

    2009

  25. [25]

    Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020,

    A. Biere, K. Fazekas, M. Fleury, and M. Heisinger, “Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020,” inProc. of SAT Competition 2020 - Solver and Benchmark Descriptions, ser. Department of Computer Science Report Series B, {Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J ¨arvisalo, Martin Suda }, Ed...

    2020

  26. [26]

    The complexity of theorem-proving procedures,

    S. A. Cook, “The complexity of theorem-proving procedures,” inLogic, automata, and computational complexity: The works of Stephen A. Cook, 2023, pp. 143–152

    2023

  27. [27]

    A fast quantum mechanical algorithm for database search,

    L. K. Grover, “A fast quantum mechanical algorithm for database search,” inProceedings of the twenty-eighth annual ACM symposium on Theory of computing, 1996, pp. 212–219

    1996

  28. [28]

    Using grover’s search quantum algorithm to solve boolean satisfiability problems: Part i,

    D. Fernandes and I. Dutra, “Using grover’s search quantum algorithm to solve boolean satisfiability problems: Part i,”XRDS: Crossroads, The ACM Magazine for Students, vol. 26, no. 1, pp. 64–66, 2019

    2019

  29. [29]

    Quantum algorithm for maximum satisfiability,

    A. Alasow and M. Perkowski, “Quantum algorithm for maximum satisfiability,” in2022 IEEE 52nd International Symposium on Multiple- Valued Logic (ISMVL). IEEE, 2022, pp. 27–34

    2022

  30. [30]

    Quantum annealing-based software components: An experimental case study with sat solving,

    T. Kr ¨uger and W. Mauerer, “Quantum annealing-based software components: An experimental case study with sat solving,” inProceedings of the IEEE/ACM 42nd International Conference on Software Engineering Workshops, 2020, pp. 445–450

    2020

  31. [31]

    Optimization by quantum annealing: Lessons from hard satisfiability problems,

    D. A. Battaglia, G. E. Santoro, and E. Tosatti, “Optimization by quantum annealing: Lessons from hard satisfiability problems,”Physical Review E—Statistical, Nonlinear, and Soft Matter Physics, vol. 71, no. 6, p. 066707, 2005

    2005

  32. [32]

    Solving boolean satisfiability problems with the quantum approximate optimization algorithm,

    S. Boulebnane and A. Montanaro, “Solving boolean satisfiability problems with the quantum approximate optimization algorithm,”PRX Quantum, vol. 5, no. 3, p. 030348, 2024

    2024

  33. [33]

    A parallel and distributed quantum sat solver based on entanglement and teleportation,

    S.-W. Lin, T.-F. Wang, Y .-R. Chen, Z. Hou, D. San´an, and Y . S. Teo, “A parallel and distributed quantum sat solver based on entanglement and teleportation,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2024, pp. 363–382

    2024

  34. [34]

    Quantum walk speedup of backtracking algorithms

    A. Montanaro, “Quantum walk speedup of backtracking algorithms,” arXiv preprint arXiv:1509.02374, 2015

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  35. [35]

    Solving k–sat problems with generalized quantum measurement,

    Y . Zhang, P. Lewalle, and K. B. Whaley, “Solving k–sat problems with generalized quantum measurement,”npj Quantum Information, vol. 11, no. 1, p. 170, 2025

    2025

  36. [36]

    Hyqsat: A hybrid approach for 3-sat problems by integrating quantum annealer with cdcl,

    S. Tan, M. Yu, A. Python, Y . Shang, T. Li, L. Lu, and J. Yin, “Hyqsat: A hybrid approach for 3-sat problems by integrating quantum annealer with cdcl,” in2023 IEEE International Symposium on High-Performance Computer Architecture (HPCA). IEEE, 2023, pp. 731–744

    2023

  37. [37]

    Tight bounds on quantum searching,

    M. Boyer, G. Brassard, P. Høyer, and A. Tapp, “Tight bounds on quantum searching,”Fortschritte der Physik: Progress of Physics, vol. 46, no. 4-5, pp. 493–505, 1998

    1998

  38. [38]

    The shortest path through a maze,

    E. F. Moore, “The shortest path through a maze,” inProc. of the International Symposium on the Theory of Switching. Harvard University Press, 1959, pp. 285–292

    1959

  39. [39]

    An algorithm for path connections and its applications,

    C. Y . Lee, “An algorithm for path connections and its applications,”IRE transactions on electronic computers, no. 3, pp. 346–365, 1961

    1961

  40. [40]

    PennyLane: Automatic differentiation of hybrid quantum-classical computations

    V . Bergholm, J. Izaac, M. Schuld, C. Gogolin, S. Ahmed, V . Ajith, M. S. Alam, G. Alonso-Linaje, B. AkashNarayanan, A. Asadiet al., “Pennylane: Automatic differentiation of hybrid quantum-classical computations,” arXiv preprint arXiv:1811.04968, 2018

    work page internal anchor Pith review Pith/arXiv arXiv 2018