[Rule] Satisfiability to MultivariateQuadratic

[QingyunQian]

Source: Satisfiability
Target: MultivariateQuadratic (over F₂)
Motivation: SAT can be reduced to MQ over F₂ in polynomial time. This reduction enables solving SAT instances using algebraic formulations and complements the reverse direction (MQ over F₂ to SAT).
Reference:

• Courtois, N., & Meier, W. (2003). "Algebraic attacks on stream ciphers with linear feedback." In Advances in Cryptology — EUROCRYPT 2003.
• Bard, G. V. (2009). Algebraic Cryptanalysis. Springer.

Reduction Algorithm

Notation:

• Source: SAT instance with n boolean variables x₁, ..., xₙ and m clauses
• Preprocessing: first convert SAT to 3-SAT (standard polynomial-time step), obtaining n' variables and m' clauses
• Target: MQ instance over F₂ with n' + m' variables and 2m' quadratic equations (one auxiliary variable per clause)

Variable mapping:

• Each 3-SAT variable xᵢ ∈ {0, 1} maps directly to MQ variable xᵢ ∈ F₂
• For each 3-SAT clause Cⱼ = (ℓ₁ ∨ ℓ₂ ∨ ℓ₃), introduce one auxiliary variable tⱼ ∈ F₂

Constraint transformation:
For each 3-SAT clause Cⱼ = (ℓ₁ ∨ ℓ₂ ∨ ℓ₃):

1. Define

   • α = 1 + ℓ₁
   • β = 1 + ℓ₂
   • γ = 1 + ℓ₃
     so clause satisfaction is equivalent to α·β·γ = 0 in F₂.

2. Quadratize with one auxiliary variable tⱼ:

   • tⱼ + α·β = 0
   • tⱼ·γ = 0

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

Solution extraction:
Read the original variables x₁, ..., xₙ from any satisfying MQ assignment; auxiliary variables tⱼ are internal and can be ignored.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
field_size	2 (constant, F₂)
num_variables	n' + m'
num_equations	2m'

Validation Method

• Cross-check with SAT solvers on standard benchmarks (SATLIB, SAT Competition instances)
• Verify on small hand-crafted instances (3-4 variables, 5-6 clauses)
• Compare with existing SAT-to-polynomial converters (PolyBoRi, ANF tools)
• Test on unsatisfiable instances to ensure NO is correctly detected

Example

Source SAT instance (already 3-SAT):

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

Target MQ instance (F₂):

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

  # Clause C₂: (¬x₁ ∨ x₂ ∨ x₃)
  f₃: t₂ + x₁·(1 + x₂) = 0
  f₄: t₂·(1 + x₃) = 0

Solution:

• SAT solution: x₁=1, x₂=1, x₃=1 (satisfies all clauses)
• MQ extension: choose t₁=0, t₂=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:

• Source (3-SAT): n'=3 variables, m'=2 clauses
• Target: num_variables = n' + m' = 3 + 2 = 5, num_equations = 2m' = 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.