SAT Strikes Back: Parameter and Path Relations in Quantum Toolchains

TL;DR

The paper investigates how to optimally transform high-level problem formulations into hardware-executable forms for quantum toolchains, using exact-$k$ SAT as a case study to map to QUBO/PUBO representations. It compares four transformation pathways (textbook $k$-SAT → $3$-SAT → QUBO, generalized Choi*, Dobry, and DeMorgan direct mappings) and analyzes how input structure, intermediate representations, and quadratisation affect metrics like variable count, monomial degree, and graph density. Key contributions include empirical scaling insights, the role of the quadratisation parameter $p$, and qualitative extrapolations tying problem structure to hardware-aware encoding decisions, all aimed at enabling automated, structure-aware toolchains. The findings support predictable performance planning and highlight how transformation choices interact with hardware connectivity and error-correction considerations, informing practical quantum software design. Overall, the work lays a foundation for optimizing transformation paths in automated quantum pipelines to improve solution quality and runtime on near-term devices.

Abstract

In the foreseeable future, toolchains for quantum computing should offer automatic means of transforming a high level problem formulation down to a hardware executable form. Thereby, it is crucial to find (multiple) transformation paths that are optimised for (hardware specific) metrics. We zoom into this pictured tree of transformations by focussing on k-SAT instances as input and their transformation to QUBO, while considering structure and characteristic metrics of input, intermediate and output representations. Our results can be used to rate valid paths of transformation in advance -- also in automated (quantum) toolchains. We support the automation aspect by considering stability and therefore predictability of free parameters and transformation paths. Moreover, our findings can be used in the manifesting era of error correction (since considering structure in a high abstraction layer can benefit error correcting codes in layers below). We also show that current research is closely linked to quadratisation techniques and their mathematical foundation.

Figures (9)

• Figure 1: Possible paths from $k$- to via known transformations with special focus on properties induced into resulting . Choi* marks a generalised version of the $3$- to transformation. Perceived abstraction layer of NP-complete problems coloured in blue and Optimisation problems coloured in grey.
• Figure 2: Example of a $I = \{v_2, v_5\}$ coloured in blue. Note that $\{v_1, v_2, v_3\}$ and $\{v_4, v_5, v_6\}$ form a $3$-clique (i.e., a fully connected subgraph).
• Figure 3: Abstracted / relation. (Dashed) lines: (Multiple intermediate) transformation(s).
• Figure 4: Number of variables in $k$- (x-axis) vs number of variables in resulting (y-axis), coloured by the number of clauses. Horizontal facet: Transformation path. Vertical facet: $k$ in $k$-. For DeMorg. and Dobry., $p=1$.
• Figure 5: Number of variables in $k$- (x-axis) vs number of monomials in resulting (y-axis), coloured by the number of clauses. Horizontal facet: Transformation path. Vertical facet: $k$ in $k$-. For DeMorg. and Dobry., $p=1$.