[Rule] KSatisfiability to KLocalHamiltonian

[QingyunQian]

Source: KSatisfiability (k-SAT)
Target: KLocalHamiltonian
Motivation: Embeds classical satisfiability into the quantum Hamiltonian framework via a standard clause-to-projector mapping ( frustration-free local Hamiltonians). Enables a unified reduction chain from classical NP-complete problems into quantum complexity.
Reference:

• Kitaev, A. Yu., Shen, A. H. & Vyalyi, M. N. (2002). Classical and Quantum Computation. AMS, Section 14.4.
• Kempe, J., Kitaev, A. & Regev, O. (2006). "The Complexity of the Local Hamiltonian Problem." SIAM J. Comput., 35(5), 1070–1097.

Reduction Algorithm

Notation:

• Source (KSatisfiability): $n$ Boolean variables $x_0, \dots, x_{n-1}$; $m$ clauses $C_1, \dots, C_m$, each containing exactly $k$ literals on distinct variables (standard for k-SAT; if duplicates exist, preprocess by removing repeated literals and shrinking the clause). Literal $l$ is either $x_i$ (positive) or $\neg x_i$ (negative). DIMACS convention: positive integer $i+1$ for $x_i$, negative integer $-(i+1)$ for $\neg x_i$.
• Target (KLocalHamiltonian): $n$ qubits, $m$ Hamiltonian terms $H_1, \dots, H_m$, thresholds $a, b$.

Convention: qubit computational basis $|0\rangle$ = FALSE, $|1\rangle$ = TRUE.

Variable mapping:

Each Boolean variable $x_i$ maps one-to-one to qubit $i$. A classical assignment $(x_0, \dots, x_{n-1}) \in {0,1}^n$ corresponds to the computational basis state $|x_0 x_1 \cdots x_{n-1}\rangle$.

Constraint/objective transformation:

For each clause $C_j$ acting on variable indices $S_j = {q_1, \dots, q_k}$:

1. Identify the unique violating assignment: the $k$-bit string $|v_j\rangle = |b_1 b_2 \cdots b_k\rangle$ where

   • $b_i = 0$ if the literal on variable $q_i$ is positive ($x_{q_i}$), because the clause is violated when $x_{q_i} = 0$
   • $b_i = 1$ if the literal on variable $q_i$ is negative ($\neg x_{q_i}$), because the clause is violated when $x_{q_i} = 1$

2. Construct the $k$-local projector:

$$H_j = \Big(|v_j\rangle\langle v_j|\Big)_{S_j} \otimes I_{\overline{S_j}}$$

where $\overline{S_j}$ denotes the remaining $n - k$ qubits. The local part $|v_j\rangle\langle v_j|$ is the tensor product (taken in the fixed ordering of qubits in $S_j$):

$$|v_j\rangle\langle v_j| = \bigotimes_{i=1}^{k} P_{q_i}$$

where $P_{q_i} = |0\rangle\langle 0|$ if the literal is positive, $P_{q_i} = |1\rangle\langle 1|$ if negative. In matrix form:

$$|0\rangle\langle 0| = \begin{pmatrix} 1 & 0 \ 0 & 0 \end{pmatrix}, \quad |1\rangle\langle 1| = \begin{pmatrix} 0 & 0 \ 0 & 1 \end{pmatrix}$$

3. Set thresholds:
   • $a = 0$ (SAT: there exists a basis state with energy 0)
   • $b = 1$ (UNSAT: every basis state violates $\geq 1$ clause)

Total Hamiltonian: $H = \sum_{j=1}^{m} H_j$

Correctness

• $H$ is diagonal in the computational basis. For a classical assignment $z \in {0,1}^n$:

$$\langle z | H | z \rangle = \text{number of clauses violated by } z$$

• SAT $\implies$ $\exists z$ with $\langle z|H|z\rangle = 0 \leq a$. Since $H$ is positive semidefinite, the ground-state energy is exactly 0.
• UNSAT $\implies$ $\forall z$, $\langle z|H|z\rangle \geq 1 \geq b$. Since $H$ is diagonal, the quantum ground-state energy equals the minimum over computational basis states, so ground energy $\geq 1$.
• Promise gap: $b - a = 1 \geq 1/\text{poly}(n)$, always satisfied.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_qubits	$n$ (= num_vars)
num_terms	$m$ (= num_clauses)
matrix_dim per term	$2^k \times 2^k$ (constant for fixed $k$)
threshold_a	$0$
threshold_b	$1$

The reduction is linear: dense encoding of each local matrix requires $4^k$ entries, giving total storage $O(m \cdot 4^k)$, which is $O(m)$ for fixed $k$. Sparse/structured representations can reduce this further since each $H_j$ is rank-1.

Validation Method

• Exact diagonalization of $H$ on small instances ($n \leq 20$) and comparison with brute-force SAT solving: ground energy = 0 iff SAT, $\geq 1$ iff UNSAT
• Verify each $H_j$ is a rank-1 projector: $H_j^2 = H_j$, $\text{Tr}(H_j) = 1$, $||H_j|| = 1$
• Cross-check: for every satisfying assignment $z$, confirm $\langle z|H_j|z\rangle = 0$ for all $j$; for every unsatisfying assignment, confirm $\langle z|H|z\rangle \geq 1$
• Test on known UNSAT instances (e.g., pigeonhole-principle formulas) to confirm ground energy $\geq 1$

Example

Source: 3-SAT instance

n = 3 variables: x_0, x_1, x_2
m = 2 clauses (k = 3):
  C_1 = (x_0 ∨ x_1 ∨ x_2)          DIMACS: 1 2 3
  C_2 = (¬x_0 ∨ ¬x_1 ∨ x_2)       DIMACS: -1 -2 3

Clause-to-projector construction

Clause $C_1 = (x_0 \vee x_1 \vee x_2)$:

• Violated when $x_0=0, x_1=0, x_2=0$
• Violating state: $|000\rangle$
• $H_1 = |0\rangle\langle 0| \otimes |0\rangle\langle 0| \otimes |0\rangle\langle 0|$ on qubits ${0, 1, 2}$

$$H_1 = \text{diag}(1, 0, 0, 0, 0, 0, 0, 0)$$

Clause $C_2 = (\neg x_0 \vee \neg x_1 \vee x_2)$:

• Violated when $x_0=1, x_1=1, x_2=0$
• Violating state: $|110\rangle$
• $H_2 = |1\rangle\langle 1| \otimes |1\rangle\langle 1| \otimes |0\rangle\langle 0|$ on qubits ${0, 1, 2}$

$$H_2 = \text{diag}(0, 0, 0, 0, 0, 0, 1, 0)$$

Target: KLocalHamiltonian instance

num_qubits = 3, num_terms = 2, k = 3
H = H_1 + H_2 = diag(1, 0, 0, 0, 0, 0, 1, 0)
threshold_a = 0, threshold_b = 1

Verification (all 8 assignments):

$x_0 x_1 x_2$	$C_1$	$C_2$	$\langle z \mid H \mid z \rangle$
000	violated	sat	1
001	sat	sat	0
010	sat	sat	0
011	sat	sat	0
100	sat	sat	0
101	sat	sat	0
110	sat	violated	1
111	sat	sat	0

Ground-state energy = 0 (achieved by 6 out of 8 assignments). Since $0 \leq a = 0$, the answer is YES (SAT).

Note: the resulting Hamiltonian is diagonal in the computational basis. This means the reduction embeds a classical problem into the quantum framework without introducing quantum entanglement in the ground state. The non-trivial quantum aspect arises when this reduction is composed with further transformations (e.g., perturbation gadgets for locality reduction from $k$-local to 2-local).

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Target problem KLocalHamiltonian does not yet exist in the reduction graph; no existing path
Non-trivial	✅ Pass	Genuine structural transformation: Boolean clauses mapped to tensor-product projectors on a Hilbert space
Correctness	✅ Pass	Both references verified; reduction is the standard clause-to-projector mapping from quantum complexity theory
Well-written	⚠️ Warn	Minor issues with overhead table (see details below)

Overall: 3 passed, 0 failed, 1 warning

---

Usefulness

The target problem KLocalHamiltonian does not currently exist in the codebase (pred show KLocalHamiltonian returns nothing), so this reduction is entirely novel. No path from KSatisfiability to KLocalHamiltonian exists. The motivation clearly explains the value: embedding classical NP-complete satisfiability into the quantum Hamiltonian framework, enabling a unified reduction chain from classical to quantum complexity. This is a foundational reduction in quantum complexity theory.

Non-trivial

The reduction performs a genuine structural transformation:

• Boolean variables are mapped to qubits in a Hilbert space.
• Each clause is mapped to a rank-1 projector (tensor product of single-qubit projectors) acting on the relevant qubits.
• The satisfiability question becomes a ground-state energy question for a positive semidefinite Hamiltonian.

This is not a variable substitution or subtype coercion. The construction involves projector operators, tensor products, and a threshold (promise gap) mechanism. The resulting Hamiltonian is diagonal in the computational basis, which is the correct and standard construction for classical-to-quantum embeddings.

Correctness

Reference 1: Kitaev, Shen & Vyalyi (2002), Classical and Quantum Computation, AMS GSM/47

• Verified: This is a well-known graduate textbook published by AMS as Volume 47 in the Graduate Studies in Mathematics series. ISBN 0-8218-3229-8. The clause-to-projector mapping for classical SAT is covered in the relevant chapters on quantum NP-completeness.

Reference 2: Kempe, Kitaev & Regev (2006), "The Complexity of the Local Hamiltonian Problem," SIAM J. Comput. 35(5), 1070-1097

• Verified: Published in SIAM Journal on Computing with DOI 10.1137/S0097539704445226. Also available as arXiv:quant-ph/0406180. This paper proves that k-Local Hamiltonian is QMA-complete for k >= 2, settling a major open question.

The reduction algorithm described in the issue (clause-to-projector mapping where each violated assignment becomes a rank-1 projector) is the standard construction from quantum complexity theory. The correctness argument (diagonal Hamiltonian, energy = number of violated clauses, promise gap b - a = 1) is sound.

Well-written

Completeness: All required sections are present and substantive: Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, and Example.

Algorithm quality: The reduction algorithm is detailed, step-by-step, and implementable. All intermediate values are defined. The notation section clearly establishes all symbols before use. The DIMACS convention is mentioned for concreteness.

Example quality: Excellent. The example uses a 3-SAT instance with 3 variables and 2 clauses, constructs both projectors explicitly with matrix representations, and verifies all 8 assignments in a table. This is brute-force verifiable and fully worked.

Minor issues (warnings, not failures):

1. Overhead table entries: The fields matrix_dim, threshold_a, and threshold_b are constants (2^k x 2^k, 0, and 1 respectively), not expressions over source problem metrics. In the #[reduction(overhead = {...})] macro, overhead expressions must reference getter methods on the source type and produce target size metrics. The actual overhead entries for implementation would likely be just:

   • num_qubits = "num_vars"
   • num_terms = "num_clauses"

   The constant thresholds and per-term matrix dimensions are properties of the construction, not overhead expressions. Consider reformulating the table to match the expected overhead attribute format.

2. Target model dependency: KLocalHamiltonian does not yet exist as a problem model in the codebase. This rule requires a corresponding [Model] issue for KLocalHamiltonian to be implemented first. The overhead field names (num_qubits, num_terms) will need to match the getter methods on the eventual KLocalHamiltonian type.

Recommendations

• File a [Model] issue for KLocalHamiltonian before or alongside this rule, so the target type and its getter methods are defined.
• Simplify the overhead table to only include the two non-constant fields (num_qubits, num_terms) that will map to actual #[reduction(overhead = {...})] expressions.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	KLocalHamiltonian does not exist in the reduction graph; novel reduction bridging classical and quantum complexity
Non-trivial	✅ Pass	Constructs k-local projectors from clause structure with tensor product gadgets
Correctness	✅ Pass	Both references verified; clause-to-projector mapping is a standard construction
Well-written	⚠️ Warn	Minor issues: target problem not yet implemented; overhead table metrics unverifiable

Overall: 3 passed, 0 failed, 1 warning

---

Usefulness

KLocalHamiltonian is not currently implemented in the codebase (pred show KLocalHamiltonian returns "Unknown problem"). No existing path from KSatisfiability to any quantum Hamiltonian problem exists. This reduction bridges classical NP-completeness (k-SAT) into the quantum Hamiltonian framework, enabling a unified reduction chain from classical problems into quantum complexity (QMA). This is a genuinely novel addition to the reduction graph.

The motivation is concrete: embedding classical satisfiability into the quantum Hamiltonian framework via frustration-free local Hamiltonians, enabling further quantum reductions (e.g., perturbation gadgets for locality reduction).

Non-trivial

The reduction is non-trivial. It involves:

• Constructing k-local projector operators from clause structure (tensor products of single-qubit projectors)
• Mapping Boolean satisfiability constraints to quantum energy penalties
• Setting promise gap thresholds (a=0, b=1) that encode the SAT/UNSAT distinction as a ground-state energy question

This is not a variable substitution, subtype coercion, or identity mapping — it is a genuine structural transformation from Boolean formulas to Hermitian operators on a Hilbert space.

Correctness

Reference 1: Kitaev, Shen & Vyalyi (2002). Classical and Quantum Computation. AMS, Graduate Studies in Mathematics, Vol. 47. Verified — the book exists and is a standard reference for quantum complexity theory. Section 14.4 covers the local Hamiltonian problem. AMS Bookstore

Reference 2: Kempe, Kitaev & Regev (2006). "The Complexity of the Local Hamiltonian Problem." SIAM J. Comput., 35(5), 1070–1097. Verified — the paper exists at the cited DOI and on arXiv (quant-ph/0406180). It proves that 2-local Hamiltonian is QMA-complete and establishes the k-local Hamiltonian problem as the natural complete problem for QMA.

The clause-to-projector mapping described in the issue (each clause maps to a rank-1 projector onto the unique violating assignment) is the standard construction from Kitaev's original work. The correctness argument is sound:

• H is diagonal in the computational basis, so the quantum ground-state energy equals the classical minimum number of violated clauses
• SAT implies ground energy = 0, UNSAT implies ground energy >= 1
• The promise gap b - a = 1 is always inverse-polynomial

Well-written

Strengths:

• All template sections are present and substantive
• The reduction algorithm is detailed step-by-step with explicit notation
• The example is fully worked with all 8 assignments verified in a table
• Symbol usage is consistent across sections (n, m, k, S_j, v_j, H_j all defined and used consistently)
• The correctness proof is clear and self-contained

Minor issues (warnings, not failures):

• The target problem KLocalHamiltonian does not yet exist in the codebase. This reduction requires a companion [Model] issue to define KLocalHamiltonian first. The overhead table lists target metrics (num_qubits, num_terms, matrix_dim, threshold_a, threshold_b) that cannot be verified against actual getter methods until the model is implemented.
• The matrix_dim row in the overhead table says "2^k x 2^k (constant for fixed k)" — this is per-term storage, not a standard code metric. It may need to be reformulated once the KLocalHamiltonian model schema is defined.
• The issue does not explicitly mention that a [Model] issue for KLocalHamiltonian is a prerequisite.

Recommendations

• File a companion [Model] issue for KLocalHamiltonian before implementing this rule, so the target type and its getter methods are defined first.
• Once the model is defined, revisit the overhead table to use the actual code metric names from KLocalHamiltonian::size_fields().

[GiggleLiu]

Closing as part of batch cleanup.