[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.). Together with the reverse reduction (issue #131), this establishes polynomial-time equivalence between boolean MQ and SAT. Depends on model issue #129.
Reference:

• Bard, G. V. (2009). Algebraic Cryptanalysis, Ch. 13: "Converting MQ to CNF-SAT." Springer. Directly describes the MQ-to-SAT conversion procedure.
• Tseitin, G. S. (1983). "On the complexity of derivation in propositional calculus." Core technique for encoding AND gates as CNF clauses.

Reduction Algorithm

Notation:

• Source: MQ instance over F₂ with num_variables Boolean variables x₁, ..., x_n and num_equations polynomial equations
• Let num_distinct_cross_terms = P be the number of distinct quadratic cross terms x_i x_j (i < j) appearing in the system
• Let num_terms = the total number of non-zero monomials across all equations (counting each quadratic term, linear term, and constant term in each equation)
• Target: Satisfiability instance

Variable mapping:

1. Original variables: Each MQ variable x_i ∈ F₂ maps directly to SAT variable x_i.
2. Product variables (Tseitin transformation): For each distinct product term x_i x_j appearing in the polynomials, introduce auxiliary SAT variable y_{ij} representing x_i ∧ x_j.

Constraint transformation:

For each MQ equation f_k(x) = Σ_{i<j} a_{ij} x_i x_j + Σ_i b_i x_i + c = 0 (mod 2):

Step 1: Convert to XOR form.
Replace each product x_i x_j with its auxiliary variable y_{ij}. The equation becomes a XOR of boolean variables:

y_{ij_1} ⊕ y_{ij_2} ⊕ ... ⊕ x_{l_1} ⊕ x_{l_2} ⊕ ... ⊕ c = 0

where the y's correspond to quadratic terms with coefficient 1, the x's to linear terms with coefficient 1, and c is the constant.

Step 2: Tseitin encoding for product variables.
For each product variable y_{ij}, add 3 CNF clauses enforcing y_{ij} ↔ (x_i ∧ x_j):

(¬y_{ij} ∨ x_i) ∧ (¬y_{ij} ∨ x_j) ∧ (y_{ij} ∨ ¬x_i ∨ ¬x_j)

Step 3: XOR-to-CNF chain encoding.
Convert each XOR constraint to CNF using chaining variables:

• Base case (k = 2 terms): u ⊕ v = 0 is encoded as 2 clauses:

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

• General case (k ≥ 3 terms): For ℓ₁ ⊕ ℓ₂ ⊕ ... ⊕ ℓ_k = 0, introduce chaining variables s₂, ..., s_{k-1}:

  • s₂ ↔ (ℓ₁ ⊕ ℓ₂): 4 clauses
  • s₃ ↔ (s₂ ⊕ ℓ₃): 4 clauses
  • ...
  • s_{k-1} ↔ (s_{k-2} ⊕ ℓ_{k-1}): 4 clauses
  • Final: s_{k-1} = ℓ_k: 2 clauses

  Each equivalence u ↔ (v ⊕ w) is encoded by 4 CNF clauses:

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

  Total for k-term XOR: (k - 2) chain variables, 4(k - 2) + 2 clauses.

• Constant term c = 1: If the equation has c = 1 (i.e., XOR = 1 instead of 0), flip the final enforcement: use s_{k-1} = ¬ℓ_k. For k = 2: u ⊕ v = 1 becomes (u ∨ v) ∧ (¬u ∨ ¬v).

Solution extraction:

Extract values of original variables x₁, ..., x_n from the SAT solution. Auxiliary variables (product y_{ij} and chain s_i) are discarded.

Size Overhead

Target metric (code name)	Formula
num_vars	num_variables + num_distinct_cross_terms + num_terms - 2 * num_equations
num_clauses	3 * num_distinct_cross_terms + 4 * num_terms - 6 * num_equations

Where:

• num_variables — source Boolean variables
• num_distinct_cross_terms — distinct quadratic products in the system (P)
• num_terms — total non-zero monomials across all equations
• num_equations — number of source equations

Detailed breakdown (assuming each equation has ≥ 2 terms after substitution):

• Original variables: num_variables
• Product auxiliary variables: num_distinct_cross_terms
• Chain auxiliary variables: for an equation with T_k terms, (T_k - 2) chain vars; total = num_terms - 2 * num_equations
• Total SAT variables: num_variables + num_distinct_cross_terms + num_terms - 2 * num_equations
• Tseitin clauses: 3 * num_distinct_cross_terms
• Chain clauses: for an equation with T_k terms, 4(T_k - 2) + 2 clauses; total = 4 * num_terms - 6 * num_equations
• Total SAT clauses: 3 * num_distinct_cross_terms + 4 * num_terms - 6 * num_equations

Note: The num_terms getter needs to be added to the MultivariateQuadratic model (issue #129). It counts the total number of non-zero monomial entries (quadratic terms + linear terms + constants) across all equations.

Validation Method

• Build a closed-loop test on small MultivariateQuadratic instances over F₂.
• Reduce the source MQ instance to a Satisfiability instance.
• Solve the SAT instance with brute-force search.
• Extract the x_i assignment from the SAT solution and verify that every source equation evaluates to 0 mod 2.
• Cross-check against exhaustive search on the source problem to confirm the SAT instance is satisfiable iff the MQ instance is satisfiable.

Example

Source MQ instance (F₂):

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

Step 1: Identify product terms and introduce auxiliaries.

• y₁₂ represents x₁·x₂
• y₂₃ represents x₂·x₃

Step 2: Rewrite equations as XOR.

• f₁: y₁₂ ⊕ x₃ = 0 (2 terms)
• f₂: y₂₃ ⊕ x₁ = 0 (2 terms)

Step 3: Generate CNF clauses.

Target SAT instance:

Variables: x₁, x₂, x₃, y₁₂, y₂₃

Clauses:
  # Tseitin for y₁₂ ↔ (x₁ ∧ x₂):
  (¬y₁₂ ∨ x₁)
  (¬y₁₂ ∨ x₂)
  (y₁₂ ∨ ¬x₁ ∨ ¬x₂)

  # Tseitin for y₂₃ ↔ (x₂ ∧ x₃):
  (¬y₂₃ ∨ x₂)
  (¬y₂₃ ∨ x₃)
  (y₂₃ ∨ ¬x₂ ∨ ¬x₃)

  # XOR for f₁: y₁₂ ⊕ x₃ = 0 (base case, 2 clauses):
  (y₁₂ ∨ ¬x₃)
  (¬y₁₂ ∨ x₃)

  # XOR for f₂: y₂₃ ⊕ x₁ = 0 (base case, 2 clauses):
  (y₂₃ ∨ ¬x₁)
  (¬y₂₃ ∨ x₁)

Total: 5 variables, 10 clauses

Solution:

• MQ solution: x₁=0, x₂=0, x₃=0 (satisfies both equations: 0·0+0=0, 0·0+0=0)
• SAT extension: y₁₂=0, y₂₃=0
• All 10 clauses verified satisfied.

Overhead verification:

• Source: num_variables=3, num_equations=2, num_distinct_cross_terms=2, num_terms=4 (f₁ has 2 terms, f₂ has 2 terms)
• num_vars = 3 + 2 + 4 - 2×2 = 5 ✓
• num_clauses = 3×2 + 4×4 - 6×2 = 6 + 16 - 12 = 10 ✓

Notes

• Both MQ(F₂) and SAT are NP-complete; this reduction runs in polynomial time.
• For sparse MQ systems (few terms per equation), the CNF encoding is efficient. For dense systems, SAT solvers with native XOR support (e.g., CryptoMiniSat) may be more practical since they can handle XOR constraints directly without the chain encoding overhead.

[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.

[GiggleLiu]

Fix-issue changelog

• Dropped Courtois & Meier (2003) reference (misattributed — about stream cipher attacks, not MQ→SAT); kept Bard (2009) with specific "Ch. 13: Converting MQ to CNF-SAT" citation
• Replaced O() notation in overhead with exact formulas: num_vars = num_variables + num_distinct_cross_terms + num_terms - 2 * num_equations, num_clauses = 3 * num_distinct_cross_terms + 4 * num_terms - 6 * num_equations
• Proposed num_terms getter for MultivariateQuadratic model (needs to be added to [Model] MultivariateQuadratic #129)
• Fixed target metric name: num_variables → num_vars (Satisfiability's actual getter)
• Reorganized algorithm into clear Step 1/2/3 structure with explicit XOR chain encoding details
• Moved "Alternative: XOR-SAT solver" from algorithm section to Notes
• Updated validation method to follow the codebase's closed-loop testing pattern
• Added detailed overhead verification to the example

Applied by /fix-issue.

[GiggleLiu]

Closing as part of batch cleanup.