[Enhancement] Reduce 3SAT-to-QUBO auxiliary variables through shared literal pairs

[isPANN]

Source

KSatisfiability<K3> (including clauses of width 0–3).

Target

QUBO<i64>.

Motivation

Reduce the number of target variables in the existing rule in src/rules/ksatisfiability_qubo.rs. The current default-branch implementation allocates n + m variables: one auxiliary per input clause, including unused auxiliaries for short clauses. Full clauses use independent Rosenberg gadgets with penalty 2.

Allocate auxiliaries only for cubic clause penalties and share an auxiliary between penalties with the same selected pair of signed false-literals. This can reduce output size while retaining the existing endpoints and extraction semantics. This is an application of known quadratization, not a claim of a new mathematical reduction or guaranteed solver speedup.

Reduction Algorithm

1. Preserve source variables and their indices. Simplify each clause locally: repeated literals collapse and tautological clauses contribute zero. Preserve duplicate-clause multiplicity; an empty clause contributes constant 1.

2. Encode penalties of degree at most two directly, without auxiliaries.

3. Sort the remaining three literals by variable index and select the first two as a deterministic pair. Group clauses by this signed pair; opposite literal polarities must not be conflated. No globally optimal pair-selection algorithm is required.

4. For a group of t clauses, let p,q be the shared false-literal values and r_j the third false-literal in clause j. Introduce one auxiliary a and use

   P(p,q,a) = pq - 2pa - 2qa + 3a
   H = a * sum_j r_j + (t+1) * P(p,q,a)
   

   Expand signed literals into input bits, aggregate coefficients, and retain the omitted constant C for the aggregate SAT threshold. Use checked arithmetic for group sizes, penalty multiplication, coefficient accumulation, offsets, and threshold negation.

Correctness and extraction

For fixed input bits, P=0 at a=pq and P>=1 otherwise. Changing a can improve the first term by at most t, so penalty t+1 makes every minimizing auxiliary equal pq. Consequently,

min_aux (Q(x,aux) + C) = number of violated input clauses under x.

Groups may share source variables: after fixing x, their auxiliary minimizations remain independent. Every global target optimum projects to a minimum-violation source assignment, including tied optima. SAT is YES exactly when the target minimum equals -C. On a NO instance, the QUBO remains feasible; projection must not be reported as a satisfying witness.

Do not reuse penalty 2 for a shared group. For t=3 with p=q=r_1=r_2=r_3=1, this gives energy 2 at a=0, below the true clause penalty 3. This is a counterexample to that proposed shortcut, not a defect in the existing per-clause gadget.

Size Overhead

Let m_3 be the number of cubic clauses after local simplification and g the number of selected signed-pair groups.

Metric	Bound / behavior
Target variables	n + g, where g <= m_3 <= m
Improvement	m - g fewer variables than the current allocation; strict savings are input-dependent
Group penalty	t + 1; aggregate coefficients have magnitude O(m) and mathematical bit length O(log(m+2))
Generated nonzero terms	O(m) before/after aggregation
Current dense storage	(n+g)^2 entries instead of (n+m)^2; retain the storage representation in effect when implementing
Construction	Deterministic grouping in O(m log(m+2)) fixed-width operations, plus target-storage initialization and coefficient insertion
Extraction	O(n)

Larger coefficients are a real precision tradeoff. Preserve explicit i64 overflow errors; do not silently saturate or wrap. Document bounds for the actual storage representation and arithmetic domain. Update the reduction metadata: n+m becomes an upper bound, not the exact output variable count. Do not add a second primitive edge for the same endpoints.

Example

Take five variables and the three clauses

(not x1 or not x2 or not x3)
(not x1 or not x2 or not x4)
(not x1 or not x2 or not x5)

The shared false-literal pair is (x1,x2). With one auxiliary and penalty 4:

Q = a(x3+x4+x5) + 4*x1*x2 - 8*x1*a - 8*x2*a + 12*a
C = 0

This uses 6 variables instead of 8. With dense storage, that is 36 matrix entries instead of 64. The omitted lower-triangular entries are zero under the existing upper-triangular convention.

Validation Method / Acceptance Criteria

• Independently enumerate source assignments and target auxiliaries for small mixed formulas, asserting the pointwise energy identity, not only equality of final optimal values.
• Cover mixed signs, overlapping groups, repeated and opposite literals, duplicate clauses, short and empty clauses, no-sharing inputs, unused source variables, and satisfiable/unsatisfiable formulas.
• Check all tied global target optima and the aggregate threshold, including nonzero constant offsets.
• Assert actual variable counts and metadata bounds; include the worked example and short-clause savings.
• Test the fixed-penalty counterexample and arithmetic overflow paths.
• Update the existing rule's proof, documentation, and affected tests. Verify the Rust coefficient builder and closed-loop extraction with an independent oracle.

Preliminary feasibility evidence: a standalone Python check enumerated all 2,040 source assignments for single shared groups of sizes 1–8, checked both auxiliary values and every minimizing auxiliary, and reproduced the penalty counterexample. The argument above applies to arbitrary group sizes. These finite checks do not validate an implementation of the proposed Rust change.

Reference

Schmidbauer, Lobe, Schaefer, and Mauerer, It's Quick to be Square: Fast Quadratisation for Quantum Toolchains, Section 2.2, equations (4)–(6), Algorithm 1 and its following paragraph. These describe shared-pair substitution across monomials and penalty scaling. The signed-clause specialization and deterministic pair policy above follow directly from that construction.

Journal version, ACM Transactions on Quantum Computing, 2026. Sources and default-branch implementation checked on 2026-09-14.