[Rule] KSatisfiability to MultivariateQuadratic

[QingyunQian]

Source: KSatisfiability (k = 3)
Target: MultivariateQuadratic (over F₂)
Motivation: 3-SAT can be reduced to MQ over F₂ in polynomial time via the standard CNF-to-ANF conversion. This connects the well-studied KSatisfiability family to algebraic formulations, enabling solving via Gröbner basis or XL-style algorithms. Together with the reverse reduction (issue #132), it establishes polynomial-time equivalence between 3-SAT and MQ over F₂. Depends on model issue #129.
Reference:

• Fraenkel, A. S., & Yesha, Y. (1979). "Complexity of problems in games, graphs and algebraic equations." Discrete Applied Mathematics, 1(1–2), 15–30. Original NP-completeness proof for solving polynomial systems over F₂ via reduction from 3-SAT.
• Horacek, J., & Kreuzer, M. (2020). "On conversions from CNF to ANF." Journal of Symbolic Computation, 100, 164–186. Describes the standard CNF-to-ANF conversion method used here and analyzes its properties.

Reduction Algorithm

Notation:

• Source: KSatisfiability instance with num_vars Boolean variables x₁, ..., x_n and num_clauses clauses, each with exactly 3 literals
• Target: MultivariateQuadratic instance over F₂

Variable mapping:

1. Original variables: For each x_i ∈ {0, 1}, create an MQ variable x_i ∈ F₂.
2. Auxiliary variables: For each clause C_j, introduce one auxiliary variable t_j ∈ F₂ to reduce the cubic polynomial to two quadratic equations.

Constraint transformation:

For each 3-SAT clause C_j = (ℓ₁ ∨ ℓ₂ ∨ ℓ₃):

1. Negate literals: Define

   • α = 1 + ℓ₁ (in F₂, so 1 + x_i for a positive literal, x_i for a negated literal)
   • β = 1 + ℓ₂
   • γ = 1 + ℓ₃

   Clause satisfaction is equivalent to α·β·γ = 0 in F₂.

2. Quadratize: Introduce auxiliary variable t_j and replace the single cubic equation with two quadratic equations:

   • t_j + α·β = 0 (mod 2)
   • t_j·γ = 0 (mod 2)

   These two equations jointly enforce α·β·γ = 0:

   • If α·β·γ = 0, set t_j = α·β; then t_j + α·β = 0 and t_j·γ = α·β·γ = 0.
   • If α·β·γ = 1, then α = β = γ = 1, so t_j + 1 = 0 ⟹ t_j = 1, but t_j·γ = 1·1 = 1 ≠ 0 — no solution.

Both equations are quadratic (degree ≤ 2), so they fit MultivariateQuadratic.

Solution extraction:

Read the original variables x₁, ..., x_n from any satisfying MQ assignment; auxiliary variables t_j are discarded.

Size Overhead

Target metric (code name)	Formula
num_variables	num_vars + num_clauses
num_equations	2 * num_clauses

Where:

• num_vars — number of source Boolean variables
• num_clauses — number of source 3-SAT clauses
• Original variables: num_vars
• Auxiliary variables: num_clauses (one per clause)
• Total MQ variables: num_vars + num_clauses
• Total MQ equations: 2 * num_clauses (two quadratic equations per clause)

Validation Method

• Build a closed-loop test on small KSatisfiability (k=3) instances.
• Reduce the source instance to a MultivariateQuadratic instance over F₂.
• Solve the MQ instance with brute-force search.
• Extract the x_i assignment from the MQ solution and verify that every source clause is satisfied.
• Cross-check against exhaustive search on the source problem to confirm the MQ instance is satisfiable iff the 3-SAT instance is satisfiable.

Example

Source KSatisfiability instance (k = 3):

Variables: x₁, x₂, x₃
Clauses:
  C₁: (x₁ ∨ ¬x₂ ∨ x₃)
  C₂: (¬x₁ ∨ x₂ ∨ x₃)

Target MultivariateQuadratic instance (F₂):

Field: F₂ = {0, 1}
Variables: x₁, x₂, x₃, t₁, t₂
Equations:
  # Clause C₁: (x₁ ∨ ¬x₂ ∨ x₃)
  # α = 1+x₁, β = x₂, γ = 1+x₃
  f₁: t₁ + (1 + x₁)·x₂ = 0    i.e.  t₁ + x₂ + x₁·x₂ = 0
  f₂: t₁·(1 + x₃) = 0          i.e.  t₁ + t₁·x₃ = 0

  # Clause C₂: (¬x₁ ∨ x₂ ∨ x₃)
  # α = x₁, β = 1+x₂, γ = 1+x₃
  f₃: t₂ + x₁·(1 + x₂) = 0    i.e.  t₂ + x₁ + x₁·x₂ = 0
  f₄: t₂·(1 + x₃) = 0          i.e.  t₂ + t₂·x₃ = 0

Solution:

• 3-SAT solution: x₁=1, x₂=1, x₃=1 (satisfies both clauses)
• MQ extension: t₁ = (1+1)·1 = 0, t₂ = 1·(1+1) = 0
• Verification:
  • f₁: 0 + (1+1)·1 = 0 ✓
  • f₂: 0·(1+1) = 0 ✓
  • f₃: 0 + 1·(1+1) = 0 ✓
  • f₄: 0·(1+1) = 0 ✓

Overhead verification:

• num_vars = 3, num_clauses = 2
• num_variables = 3 + 2 = 5 ✓
• num_equations = 2 × 2 = 4 ✓

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No path from Satisfiability to MultivariateQuadratic
Non-trivial	✅ Pass	CNF clauses → quadratic polynomials via auxiliary variables
Correctness	⚠️ Warn	References don't directly describe this specific reduction
Well-written	⚠️ Warn	SAT→3SAT dependency unclear; n'/m' undefined

Overall: 2 passed, 0 failed, 2 warnings

---

Usefulness

MultivariateQuadratic does not exist in the codebase. Once added, this would demonstrate polynomial-time equivalence between SAT and MQ over F₂. Requires [Model] issue first.

Non-trivial

Decomposes degree-3 clause terms (α·β·γ = 0) into two quadratic equations using auxiliary variable t_j. Genuine quadratization construction — not a simple relabeling.

Correctness — WARN

Reference	Status	Notes
Courtois & Meier (2003), EUROCRYPT	⚠️ Misattributed	Paper is about algebraic attacks on stream ciphers, not SAT-to-MQ reduction
Bard (2009), Algebraic Cryptanalysis	✅ Relevant	Covers ANF/CNF conversions, but no specific chapter/theorem cited

The reduction algorithm is mathematically correct — independently verified:

• For clause (l₁ ∨ l₂ ∨ l₃): α·β·γ = 0 correctly encodes satisfiability
• Quadratization {t_j + α·β = 0, t_j·γ = 0} ≡ α·β·γ = 0 — verified in both directions
• Example checks out

Recommendation: Replace Courtois & Meier with Horacek & Kreuzer (2020), "On Conversions from CNF to ANF," J. Symbolic Computation or cite Bard Ch. 13 specifically.

Well-written — WARN

All sections present. Algorithm is detailed. Example (3 vars, 2 clauses) is correct.

Issues:

• SAT→3SAT preprocessing is hand-waved. Says "first convert SAT to 3-SAT (standard polynomial-time step)" but doesn't specify how n'/m' relate to original n/m. Three options:
  1. Change source to KSatisfiability (3-SAT) — cleanest
  2. Specify the composition explicitly with overhead accounting
  3. Handle arbitrary clause widths directly (k-literal → k−2 auxiliary vars)
• Overhead uses n'/m' without defining them relative to source
• Target metrics field_size, num_variables, num_equations cannot be verified (MQ model doesn't exist)

Recommendations

1. Change source to KSatisfiability or specify SAT→3SAT overhead
2. Define n'/m' explicitly
3. Fix reference attribution
4. File [Model] issue for MultivariateQuadratic first

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	⚠️ Warn	Target problem MultivariateQuadratic does not exist in codebase; usefulness cannot be fully evaluated
Non-trivial	✅ Pass	Genuine structural transformation: cubic clause expressions quadratized via auxiliary variables
Correctness	❌ Fail	Cited references do not support the specific reduction claimed; overhead expressions reference 3-SAT sizes, not source problem getters
Well-written	❌ Fail	Multiple issues: overhead uses undefined intermediate symbols; preprocessing step conflates source problem identity

Overall: 1 passed, 2 failed, 1 warning

---

Usefulness

The target problem MultivariateQuadratic does not currently exist in the codebase (pred show MultivariateQuadratic fails). This means a [Model] issue and implementation for MultivariateQuadratic must be completed before this rule can be implemented. Since no path from Satisfiability to MultivariateQuadratic exists (the target doesn't exist), the reduction would be novel if the model is added. However, usefulness depends on whether MultivariateQuadratic connects to other problems in the reduction graph — the issue's motivation section only says it "complements the reverse direction" without explaining what practical value the MQ formulation provides (e.g., which downstream problems it connects to, or what solvers benefit from this formulation).

Non-trivial

Pass. The reduction involves genuine structural transformation:

• Converting CNF clause disjunctions into polynomial equations over F₂
• Introducing auxiliary variables to quadratize the cubic term α·β·γ into two quadratic equations (t + α·β = 0 and t·γ = 0)
• This is a non-trivial gadget construction, not a simple variable relabeling or type coercion

The quadratization technique is a well-known approach for reducing the degree of polynomial systems.

Correctness

Fail. Two issues:

1. References do not support the claimed reduction:

   • Courtois & Meier (2003) — "Algebraic Attacks on Stream Ciphers with Linear Feedback" (EUROCRYPT 2003). This paper is about algebraic attacks on LFSR-based stream ciphers. It does not describe a SAT-to-MQ reduction. The paper analyzes how to find low-degree annihilators of Boolean functions to break stream ciphers — a completely different topic.
   • Bard (2009) — Algebraic Cryptanalysis (Springer). This textbook covers connections between SAT solvers and polynomial systems, including ANF↔CNF conversions. While it discusses the MQ problem and SAT in the same context, the specific quadratization construction (using one auxiliary variable per clause to reduce degree-3 to degree-2) is not attributed to either of these references. The book's focus is on using SAT solvers to solve MQ, which is the reverse direction.

   The SAT-to-MQ reduction over F₂ is a well-known folklore result, but the issue should cite a reference that actually presents this construction. For example, the reduction from Boolean satisfiability to systems of polynomial equations over F₂ is more directly discussed in works on the MQ problem's NP-completeness (e.g., Garey & Johnson for general polynomial systems, or the direct construction in Kipnis & Shamir 1999 for the MQ problem definition).

2. Quadratization correctness is verified: The mathematical construction is correct — the two equations t_j + α·β = 0 and t_j·γ = 0 together enforce α·β·γ = 0 over F₂, which correctly encodes the clause. The example verifies correctly.

Well-written

Fail. Several issues:

1. Overhead uses intermediate 3-SAT symbols, not source getters: The overhead table uses n' and m' (the 3-SAT instance sizes after preprocessing), but the source problem is Satisfiability, whose getter methods are num_vars, num_clauses, and num_literals. The overhead expressions must be written in terms of the source problem's actual size fields. If the reduction internally converts to 3-SAT first, the overhead must express the final target sizes as a function of the original SAT instance's dimensions (e.g., num_variables = num_vars + num_clauses would be wrong since the 3-SAT conversion may increase both n and m).

2. Preprocessing step is under-specified: The algorithm says "first convert SAT to 3-SAT (standard polynomial-time step)" but does not specify:

   • The exact transformation used (Tseitin? clause splitting with auxiliary variables?)
   • How n' and m' relate to the original n and m
   • Whether this intermediate conversion is part of the reduction or a prerequisite

3. The field_size metric in the overhead table — is field_size an actual getter method on MultivariateQuadratic? Since the model doesn't exist yet, this cannot be verified, but it should be confirmed against the eventual model's size_fields.

4. Symbol consistency issue: The Notation section defines n and m for the SAT instance but then immediately switches to n' and m' for the 3-SAT instance. The overhead table only uses n' and m', making it impossible to determine the actual overhead from the original SAT input.

5. Missing code metric name mapping: The overhead table column says "Target metric (code name)" with values like field_size, num_variables, num_equations — these need to match actual getter methods on the (future) MultivariateQuadratic type.

6. Example quality is adequate: The example is small (3 variables, 2 clauses), fully worked, and verifiable by hand. It is acceptable.

Recommendations

• Replace the Courtois & Meier and Bard references with citations that directly describe the SAT-to-MQ reduction. Consider citing the original NP-completeness proof for MQ over finite fields, or a survey that explicitly constructs this reduction.
• Express the overhead in terms of the Satisfiability source problem's getters (num_vars, num_clauses, num_literals), accounting for the SAT-to-3-SAT blowup explicitly. For standard clause-splitting, a clause of length k produces O(k) 3-clauses and O(k) auxiliary variables, so worst-case n' = num_vars + num_literals, m' = num_clauses * (max_clause_length - 2) or similar.
• Alternatively, consider making this a KSatisfiability (k=3) to MultivariateQuadratic reduction, which avoids the 3-SAT preprocessing entirely and makes the overhead expressions clean.
• A [Model] issue for MultivariateQuadratic must be filed and implemented before this rule can proceed.