[Rule] MultivariateQuadratic to Satisfiability

[QingyunQian]

Source: MultivariateQuadratic (over F₂)
Target: Satisfiability (SAT)
Motivation: Enables solving MQ instances over F₂ using highly optimized SAT solvers (MiniSat, CryptoMiniSat, etc.). This is the reverse of SAT→MQ and demonstrates the polynomial-time equivalence between boolean MQ and 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.
• Tseitin, G. S. (1983). "On the complexity of derivation in propositional calculus."

Reduction Algorithm

Notation:

• Source: MQ instance over F₂ with n variables x₁, ..., xₙ and m polynomial equations
• Let P be the number of distinct quadratic product terms xᵢxⱼ used by the system (P ≤ n(n-1)/2)
• Let T be the total number of terms across all transformed equations after replacing products by auxiliary variables
• Target: SAT instance with polynomial size (variables O(n + P + T), clauses O(P + T))

Variable mapping:

1. Original variables: Each MQ variable xᵢ ∈ F₂ maps directly to SAT variable xᵢ
2. Product variables (Tseitin transformation): For each product term xᵢxⱼ appearing in the polynomials, introduce auxiliary SAT variable yᵢⱼ representing xᵢ ∧ xⱼ

Constraint transformation:

For each MQ equation fₖ(x) = Σᵢⱼ aᵢⱼ xᵢxⱼ + Σᵢ bᵢ xᵢ + c = 0 (mod 2):

Step 1: Convert to XOR-SAT form

• The equation is already in XOR form over F₂
• Example: x₁x₂ + x₁ + x₃ = 0 means (x₁ ∧ x₂) ⊕ x₁ ⊕ x₃ = 0

Step 2: Introduce auxiliary variables for products

• For each product xᵢxⱼ, introduce yᵢⱼ with Tseitin clauses:

  yᵢⱼ ↔ (xᵢ ∧ xⱼ)
  

  Encoded as CNF clauses:

  (¬yᵢⱼ ∨ xᵢ) ∧ (¬yᵢⱼ ∨ xⱼ) ∧ (yᵢⱼ ∨ ¬xᵢ ∨ ¬xⱼ)
  

Step 3: Convert XOR to CNF (polynomial-size encoding)

• Base case (k=2): u ⊕ v = 0 can be encoded directly as 2 clauses without any auxiliary variables:

  (u ∨ ¬v) ∧ (¬u ∨ v)
  

• General case (k≥3): For ℓ₁ ⊕ ℓ₂ ⊕ ... ⊕ ℓₖ = 0, introduce chaining variables s₂, ..., s_{k-1}:
  • s₂ ↔ (ℓ₁ ⊕ ℓ₂)
  • s₃ ↔ (s₂ ⊕ ℓ₃)
  • ...
  • s_{k-1} ↔ (s_{k-2} ⊕ ℓ_{k-1})
  • enforce s_{k-1} = ℓₖ
• Each equivalence u ↔ (v ⊕ w) is encoded by 4 CNF clauses:

  (¬u ∨ ¬v ∨ ¬w)
  (¬u ∨ v ∨ w)
  (u ∨ ¬v ∨ w)
  (u ∨ v ∨ ¬w)
  

• Constant term c=1: If the equation includes a constant term c=1 (i.e., ℓ₁ ⊕ ... ⊕ ℓₖ = 1), change the final enforcement from s_{k-1} = ℓₖ to s_{k-1} = ¬ℓₖ. For the k=2 base case, u ⊕ v = 1 becomes (u ∨ v) ∧ (¬u ∨ ¬v).
• Therefore a k-literal XOR uses O(k) auxiliary variables and O(k) clauses.

Alternative (more efficient): Use XOR-SAT solver

• Many modern SAT solvers support XOR clauses natively (CryptoMiniSat)
• Can keep XOR constraints without CNF conversion

Solution extraction:

• Extract values of original variables x₁, ..., xₙ from SAT solution
• Auxiliary variables yᵢⱼ are automatically consistent due to Tseitin clauses

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_variables	n + P + O(T) (original + products + XOR chain variables)
num_clauses	3P + O(T) (Tseitin for products + linear-size XOR encoding)

Detailed breakdown:

• Original variables: n
• Product auxiliary variables: P ≤ n(n-1)/2
• Tseitin clauses: 3 per product variable = 3P
• XOR-chain auxiliary variables/clauses: linear in total XOR length T
• Total variables: n + P + O(T)
• Total clauses: 3P + O(T)

Note: This encoding is polynomial even for long equations; in practice, native XOR support (e.g., CryptoMiniSat) is often faster.

Validation Method

• Cross-check with MQ solvers (PolyBoRi) on same instances
• Verify on small hand-crafted instances (2-3 variables)
• Test on cryptographic benchmarks (stream cipher algebraic attacks)
• Compare with direct SAT encoding of the same problem

Example

Source MQ instance (F₂):

Field: F₂ = {0, 1}
Variables: x₁, x₂, x₃
Equations:
  f₁: x₁·x₂ + x₃ = 0
  f₂: x₂·x₃ + x₁ = 0

Target SAT instance:

Variables:

• Original: x₁, x₂, x₃
• Auxiliary: y₁₂ (for x₁x₂), y₂₃ (for x₂x₃)

Clauses:

1. Tseitin clauses for y₁₂ ↔ (x₁ ∧ x₂):

 (¬y₁₂ ∨ x₁)
 (¬y₁₂ ∨ x₂)
 (y₁₂ ∨ ¬x₁ ∨ ¬x₂)

2. Tseitin clauses for y₂₃ ↔ (x₂ ∧ x₃):

 (¬y₂₃ ∨ x₂)
 (¬y₂₃ ∨ x₃)
 (y₂₃ ∨ ¬x₂ ∨ ¬x₃)

3. XOR clause for f₁: y₁₂ ⊕ x₃ = 0 (2 literals → 2 clauses):

 (y₁₂ ∨ ¬x₃)
 (¬y₁₂ ∨ x₃)

4. XOR clause for f₂: y₂₃ ⊕ x₁ = 0 (2 literals → 2 clauses):

 (y₂₃ ∨ ¬x₁)
 (¬y₂₃ ∨ x₁)

Total: 5 variables, 10 clauses

Solution:

• MQ solution: x₁=0, x₂=0, x₃=0 (satisfies both equations)
• SAT solution: x₁=0, x₂=0, x₃=0, y₁₂=0, y₂₃=0 (satisfies all clauses)

Overhead verification:

• Source: n=3 variables, m=2 equations, P=2 products
• Target:
  • Variables: n + P = 3 + 2 = 5 ✓
  • Clauses: 3P + 2·m = 6 + 4 = 10 ✓

Notes

Efficiency considerations:

• For sparse systems (few terms per equation): CNF conversion is efficient
• For dense systems (many terms per equation): Use XOR-SAT solvers (CryptoMiniSat)
• Chain-based XOR encoding keeps CNF size linear in k

Alternative: Direct XOR-SAT

• Modern SAT solvers support XOR clauses: x₁ ⊕ x₂ ⊕ x₃ = 0
• No CNF conversion needed, much more efficient
• Recommended for cryptographic applications

Complexity:

• Both MQ(F₂) and SAT are NP-complete
• This reduction is polynomial-time using Tseitin + chain XOR encoding

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No path from MultivariateQuadratic to Satisfiability
Non-trivial	✅ Pass	Tseitin encoding + XOR-to-CNF chain decomposition
Correctness	✅ Pass	All three references verified
Well-written	❌ Fail	Wrong metric name; O-notation in overhead not parseable

Overall: 3 passed, 1 failed, 0 warnings

---

Usefulness

MultivariateQuadratic does not exist in the codebase. Once added, this would enable MQ solving via SAT solvers — a standard technique in algebraic cryptanalysis. Requires [Model] issue first.

Non-trivial

Three-phase construction: (1) Tseitin encoding of AND gates (product terms → auxiliary variables + 3 CNF clauses each), (2) XOR-to-CNF chain decomposition (4 clauses per chain step), (3) constant term handling. Genuine structural transformation.

Correctness — PASS

Reference	Status	Notes
Courtois & Meier (2003), EUROCRYPT	✅ Verified	Provides MQ problem context in cryptanalysis
Bard (2009), Algebraic Cryptanalysis	✅ Verified	Chapter 13 specifically titled "Converting MQ to CNF-SAT" — directly describes this reduction
Tseitin (1983/1968), "On the Complexity of Derivation in Propositional Calculus"	✅ Verified	Core technique for AND gate → CNF encoding

Algorithm independently verified: Tseitin clauses and XOR chain decomposition are correct. Example (3 vars, 2 equations → 5 SAT vars, 10 clauses) checks out.

Well-written — FAIL

Wrong metric name. Overhead table uses num_variables but Satisfiability's actual getter is num_vars (confirmed: size_fields: ["num_clauses", "num_literals", "num_vars"]). Would cause compile error.

O-notation not parseable. Overhead expressions use O(T) (e.g., num_vars = n + P + O(T)). The #[reduction(overhead)] macro requires concrete symbolic expressions parseable by the Pratt parser — Big-O notation is not valid. Must provide exact formulas.

Additional issues:

• num_literals is a valid Satisfiability size field but not in the overhead table
• Symbol T defined loosely as "total terms after substitution" — needs precise formula
• Example overhead verification (3P + 2*m = 10) doesn't match the table formula (3P + O(T)), highlighting the ambiguity

Required fixes

1. Change num_variables → num_vars in overhead table
2. Replace O(T) with exact expressions (e.g., for P product terms and m equations with average L terms: num_vars = n + P + sum_of_chain_lengths, num_clauses = 3 * P + 4 * sum_of_chain_lengths + ...)
3. Add num_literals to overhead table
4. Define T precisely or express overhead in terms of source getters

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	⚠️ Warn	Source problem MultivariateQuadratic does not exist in the codebase — this rule requires implementing the model first
Non-trivial	✅ Pass	Tseitin transformation + XOR-to-CNF chain encoding constitute genuine structural transformation
Correctness	⚠️ Warn	References exist but relevance is indirect; the Courtois & Meier paper does not describe the MQ→SAT reduction itself
Well-written	❌ Fail	Size overhead uses asymptotic O() notation instead of exact formulas; several notation and completeness issues

Overall: 1 passed, 2 warnings, 1 failed

---

Usefulness

The source problem MultivariateQuadratic is not currently implemented in the reduction graph (pred show MultivariateQuadratic fails). Since the model does not exist, no path from MQ to SAT can be checked. If the model were added, this would be a novel reduction connecting a new problem to SAT.

However, the issue's motivation mentions "this is the reverse of SAT→MQ" — but no SAT→MQ reduction exists in the codebase either. The claim of "polynomial-time equivalence" is correct for MQ over F₂ and SAT, but neither direction is currently implemented.

Verdict: Pass (novel reduction), but warn that the source model must be implemented first.

Non-trivial

The reduction involves genuine structural transformation:

• Tseitin transformation to encode AND gates (product terms xᵢxⱼ) as auxiliary variables with 3 CNF clauses each
• XOR-to-CNF chain encoding that introduces chaining variables to convert k-literal XOR constraints into O(k) CNF clauses
• Solution extraction requires only reading original variable values (auxiliary variables are forced by Tseitin clauses)

This is not a variable substitution, subtype coercion, or identity reduction. The gadget construction is standard and well-understood in the SAT community.

Verdict: Pass.

Correctness

Reference 1: Courtois & Meier (2003), "Algebraic Attacks on Stream Ciphers with Linear Feedback," EUROCRYPT 2003.

• Paper exists and is correctly cited (LNCS vol. 2656, Springer).
• However, this paper is about algebraic attacks on stream ciphers — it reduces cipher cryptanalysis to solving overdefined multivariate polynomial systems. It does not describe the MQ→SAT reduction procedure presented in this issue. The connection is indirect: the paper motivates why one might want to solve MQ instances, but does not provide the reduction algorithm.

Reference 2: Bard (2009), Algebraic Cryptanalysis, Springer.

• Book exists and is correctly cited (ISBN 978-0-387-88756-2).
• The book covers converting polynomial systems to SAT and using SAT solvers for cryptanalysis. This is the most relevant reference for the actual reduction procedure, though it is a 392-page textbook — the issue does not specify which chapter or section describes the construction.

Reference 3: Tseitin (1983), "On the Complexity of Derivation in Propositional Calculus."

• Paper exists and is correctly cited (Springer, doi:10.1007/978-3-642-81955-1_28).
• Note: The original paper is from 1968 (in Russian); the 1983 date refers to the English translation in "Automation of Reasoning." The Tseitin transformation described in the issue is indeed from this paper. The citation is valid.

Assessment: The reduction algorithm described is mathematically correct — the Tseitin encoding of AND gates and the chain-based XOR-to-CNF conversion are standard, well-established techniques. However, none of the three references directly describes this specific MQ→SAT reduction as a complete procedure. The Courtois & Meier paper is tangentially related at best.

Verdict: Warn — the algorithm itself is correct, but the references do not directly support the specific reduction procedure. A more appropriate reference would be Bard (2009) with a specific chapter citation, or a paper that explicitly converts MQ systems to SAT (e.g., "Efficient Methods for Conversion and Solution of Sparse Systems of Low-Degree Multivariate Polynomials over GF(2) via SAT-Solvers" by Bard, Courtois, and Jefferson, 2007, ePrint 2007/024).

Well-written

4a: Information Completeness
All required sections are present (Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, Example). No placeholder text.

4b: Algorithm Completeness
The algorithm is detailed and step-by-step, covering:

• Variable mapping (original + product auxiliary variables)
• Tseitin encoding (3 clauses per product)
• XOR-to-CNF conversion (base case k=2, general case k≥3 with chaining)
• Constant term handling (c=1 case)
• Solution extraction

The algorithm is implementable. However, the "Alternative (more efficient): Use XOR-SAT solver" section is irrelevant to the reduction implementation — it suggests using a different solver backend rather than describing the reduction.

4c: Symbol and Notation Consistency — ISSUES FOUND:

1. Symbols P and T are not code-compatible metric names. The overhead table uses P (number of product terms) and T (total terms), but the target problem Satisfiability has size fields num_vars, num_clauses, and num_literals. The overhead table must use these code metric names.

2. O() notation is not allowed in overhead formulas. The overhead table states n + P + O(T) and 3P + O(T). The #[reduction(overhead = {...})] macro requires exact symbolic expressions (e.g., "num_vars + num_products + 4 * total_terms"), not asymptotic bounds. The constant factors hidden in O(T) must be spelled out.

3. The "Detailed breakdown" contradicts the table. The breakdown says "Total variables: n + P + O(T)" but the XOR chain encoding introduces exactly (k-2) auxiliary variables per k-literal XOR equation. The exact formula should be derivable.

4d: Example Quality
The example is good — small (3 variables, 2 equations), fully worked through all steps, with correct clause counts. The overhead verification at the bottom is a nice touch. However, the example only exercises the k=2 base case for XOR encoding (both equations reduce to 2-literal XORs). A slightly larger example with k≥3 would better exercise the chain encoding.

Verdict: Fail — the overhead table uses O() notation instead of exact formulas, and the code metric names do not match the target problem's size_fields (num_vars, num_clauses, num_literals).

Recommendations

1. Replace O() notation with exact formulas. Each k-literal XOR uses (k-2) chain variables and 4(k-2)+2 clauses (for k≥3) or 2 clauses (for k=2). Express the total in terms of source problem parameters.
2. Use target problem metric names: num_vars, num_clauses (and optionally num_literals) instead of P, T, n.
3. Add a more specific reference for the MQ→SAT conversion. Consider citing Bard, Courtois & Jefferson (2007), "Efficient Methods for Conversion and Solution of Sparse Systems of Low-Degree Multivariate Polynomials over GF(2) via SAT-Solvers" (ePrint 2007/024), which directly addresses this conversion.
4. Remove the "Alternative: XOR-SAT solver" section or move it to Notes — it is not part of the reduction algorithm and may confuse implementers.
5. The source model MultivariateQuadratic must be implemented first before this rule can be added. Consider filing a [Model] issue for it.