[Rule] MultivariateQuadratic to ILP

[QingyunQian]

Source: MultivariateQuadratic (over F_2)
Target: ILP (Integer Linear Programming, bool variant)
Motivation: Enables solving Boolean MQ instances using mature ILP solvers. This reduction is practical for small-to-medium instances and gives a strictly linear ILP formulation. It also connects the companion model issue #129 to an existing solver-backed problem in the reduction graph.
Reference:

• Bard, G. V., Courtois, N. T., & Jefferson, C. (2007). "Efficient methods for conversion and solution of sparse systems of low-degree multivariate polynomials over GF(2) via SAT-solvers." Background reference for MQ over F_2 and algebraic cryptanalysis.
• Glover, F., & Woolsey, E. (1974). "Technical Note—Converting the 0-1 Polynomial Programming Problem to a 0-1 Linear Program." Direct reference for converting 0-1 polynomial constraints into linear integer constraints using auxiliary variables.
• McCormick, G. P. (1976). "Computability of global solutions to factorable nonconvex programs: Part I — Convex underestimating problems." Classical source for the bilinear linearization inequalities specialized here to binary variables.

Reduction Algorithm

Notation:

• Scope of this rule: the decision problem MultivariateQuadratic over F_2 from issue #129
• Source: MQ instance with num_variables = n Boolean variables and num_equations = m equations
• Let num_distinct_cross_terms = P denote the number of distinct quadratic cross terms x_i x_j with i < j that appear anywhere in the system
• Target: ILP instance over Boolean decision variables, with additional integer slack variables for parity equalities

Variable mapping:

1. Original variables: For each x_i in F_2, create a Boolean ILP variable x_i in {0, 1}.
2. Product variables (linearization): For each distinct cross term x_i x_j with i < j, introduce a Boolean ILP variable y_ij representing x_i * x_j.
3. Square terms: Over F_2, x_i^2 = x_i, so square terms become linear and need no extra variables.
4. Parity slack variables: For each equation k, introduce an integer slack variable z_k to encode the mod-2 parity condition as a standard linear equality.

Constraint transformation:

For each MQ equation over F_2,

f_k(x) = sum_{i<j} a^k_ij x_i x_j + sum_i b^k_i x_i + c_k = 0 (mod 2),

perform the following steps:

1. Linearize monomials: Replace each x_i x_j by y_ij and define

   L_k = sum_{i<j} a^k_ij y_ij + sum_i b^k_i x_i + c_k.

2. Parity to linear equality: Enforce L_k ≡ 0 (mod 2) by the integer equality

   L_k = 2 * z_k,

   where z_k is an integer variable with bounds 0 <= z_k <= floor(T_k / 2), and T_k is the maximum possible value of L_k.

3. Product consistency: For each y_ij, add the three linear constraints

   y_ij <= x_i
   y_ij <= x_j
   y_ij >= x_i + x_j - 1

   with x_i, x_j, y_ij in {0, 1}. For binary variables these constraints exactly encode y_ij = x_i x_j.

Objective:

• This is a reduction from a satisfaction problem to a feasibility ILP instance.
• The target objective can therefore be omitted, or written as a dummy objective such as minimize 0.

Solution extraction:

• Given any feasible ILP solution, read back the original variables x_i.
• Discard the auxiliary variables y_ij and z_k.
• The recovered Boolean vector x is the candidate solution for the source MultivariateQuadratic instance.
• Correctness condition: x satisfies the source iff the constructed ILP instance is feasible.

Size Overhead

Target metric (code name)	Formula
num_vars	num_variables + num_distinct_cross_terms + num_equations
num_constraints	num_equations + 3 * num_distinct_cross_terms

Where:

• num_variables is the number of source Boolean variables
• num_equations is the number of source equations
• num_distinct_cross_terms counts the distinct quadratic cross terms x_i x_j with i < j appearing in the source system

Detailed breakdown:

• Original variables: num_variables
• Product variables: num_distinct_cross_terms
• Parity slack variables: num_equations
• Total ILP variables: num_variables + num_distinct_cross_terms + num_equations
• Total ILP constraints: num_equations + 3 * num_distinct_cross_terms
• Coarse upper bound using only num_variables and num_equations: O(num_variables^2 + num_equations)

Validation Method

• Build a closed-loop test on small MQ instances over F_2.
• Reduce the source MQ instance to an ILP instance.
• Check ILP feasibility with a brute-force or exact ILP solver.
• Extract the x_i assignment from the ILP solution and verify that every source equation evaluates to 0 mod 2.
• Cross-check against exhaustive search on the source problem to confirm that the ILP instance is feasible iff the MQ instance is satisfiable.

Example

Source MQ instance (F_2):

Field: F_2 = {0, 1}
Variables: x_1, x_2
Equations:
  f_1: x_1 * x_2 + x_1 = 0 (mod 2)
  f_2: x_1 * x_2 + x_2 = 0 (mod 2)

The satisfying MQ assignments are (x_1, x_2) = (0, 0) and (1, 1).

Target ILP instance:

Variables:
  x_1, x_2 in {0,1}          (original)
  y_12 in {0,1}              (product for x_1 x_2)
  z_1, z_2 in Z, 0 <= z_1, z_2 <= 1   (parity slack)

Constraints:
  # Equation 1: x_1 x_2 + x_1 = 0 (mod 2)
  y_12 + x_1 = 2 * z_1

  # Equation 2: x_1 x_2 + x_2 = 0 (mod 2)
  y_12 + x_2 = 2 * z_2

  # Product consistency: y_12 = x_1 x_2
  y_12 <= x_1
  y_12 <= x_2
  y_12 >= x_1 + x_2 - 1

Two corresponding feasible ILP points:

1. From MQ solution (x_1, x_2) = (0, 0):

x_1 = 0, x_2 = 0, y_12 = 0, z_1 = 0, z_2 = 0

Verification:

• Equation 1: 0 + 0 = 0 = 2 * 0
• Equation 2: 0 + 0 = 0 = 2 * 0

2. From MQ solution (x_1, x_2) = (1, 1):

x_1 = 1, x_2 = 1, y_12 = 1, z_1 = 1, z_2 = 1

Verification:

• Equation 1: 1 + 1 = 2 = 2 * 1
• Equation 2: 1 + 1 = 2 = 2 * 1

Extraction check:

• Reading back only (x_1, x_2) from either feasible ILP point recovers a satisfying MQ assignment.
• The auxiliary values y_12, z_1, and z_2 are discarded after extraction.

Overhead verification for this example:

• num_variables = 2
• num_equations = 2
• num_distinct_cross_terms = 1 (only x_1 x_2 appears)
• num_vars = 2 + 1 + 2 = 5
• num_constraints = 2 + 3 * 1 = 5

Complexity notes:

• ILP solvers are highly optimized and may be faster in practice on structured instances.
• This issue is specifically for MQ over F_2; extensions to larger finite fields would require a different source model and different linearization choices.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	⚠️ Warn	Source "MultivariateQuadratic" not yet in codebase
Non-trivial	✅ Pass	McCormick linearization + parity-to-equality encoding
Correctness	⚠️ Warn	References are tangential to this specific reduction
Well-written	⚠️ Warn	Missing solution extraction; minor notation issues

Overall: 1 passed, 0 failed, 3 warnings

---

Usefulness

MultivariateQuadratic does not exist in the codebase. Requires a [Model] issue first. Once added, this would be a novel reduction connecting algebraic cryptanalysis to ILP solvers.

Non-trivial

McCormick linearization introduces auxiliary product variables y_ij with 3 inequality constraints to encode x_i·x_j for binary variables. Parity-to-equality encoding converts mod-2 equations to linear equalities with integer slack variables. Genuine structural transformation.

Correctness — WARN

Reference	Status	Notes
Bard, Courtois & Jefferson (2007)	⚠️ Tangential	Describes MQ-to-SAT reduction, not MQ-to-ILP
McCormick (1976), Math. Programming 10, 147–175	✅ Verified	McCormick envelopes for bilinear terms — correct technique but original paper addresses continuous relaxations, not binary IP

The reduction itself is mathematically correct (verified via example). The issue combines standard techniques (McCormick linearization + parity encoding) but neither reference directly describes this combined reduction.

Recommendation: Add a standard IP textbook reference (e.g., Wolsey (1998), "Integer Programming" or Williams, "Model Building in Mathematical Programming") that covers linearization of bilinear binary terms.

Well-written — WARN

All sections present. Algorithm is implementable. Example (n=2, m=2) verified correct.

Issues:

• Missing solution extraction. Should state: "Read x_i values from ILP solution; discard y_ij and z_k."
• Overhead metrics num_vars, num_constraints match ILP's size_fields ✅
• Source metrics cannot be verified (MQ model doesn't exist yet)
• Example only shows one of two MQ solutions in ILP form

Recommendations

1. Add explicit solution extraction step
2. Cite an IP textbook for the linearization technique
3. Show both MQ solutions mapped to ILP feasible points
4. File [Model] issue for MultivariateQuadratic first

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Source problem (MultivariateQuadratic) not yet in codebase; no existing path exists
Non-trivial	✅ Pass	Genuine structural transformation: McCormick linearization + parity-to-integer-equality conversion
Correctness	⚠️ Warn	Both references are real papers, but neither directly describes this exact MQ-to-ILP reduction
Well-written	⚠️ Warn	Overhead expressions use symbolic names (n, P, m) instead of source getter method names; minor notation issues

Overall: 2 passed, 0 failed, 2 warnings

---

Usefulness

The source problem MultivariateQuadratic does not yet exist in the reduction graph (companion model issue #129 is open). Since there is no existing path from MultivariateQuadratic to ILP, this reduction is novel. Pass.

Note: This rule depends on #129 being implemented first.

Non-trivial

The reduction involves two non-trivial structural transformations:

1. McCormick linearization: Each quadratic cross term x_i * x_j is replaced by an auxiliary binary variable y_ij with 3 linear constraints enforcing the product relationship. This is a genuine gadget construction.
2. Parity-to-integer-equality: The mod-2 equations are converted to standard linear equalities using integer slack variables (L_k = 2 * z_k).

This is not a simple variable relabeling or subtype coercion. Pass.

Correctness

Reference 1 — Bard, Courtois & Jefferson (2007):

• Paper verified at eprint.iacr.org/2007/024.
• Title, authors, and year all match.
• However, this paper describes converting MQ systems over GF(2) to SAT (CNF), not to ILP. The paper is relevant background for the MQ problem itself but does not describe the ILP linearization technique used in this issue.

Reference 2 — McCormick (1976):

• Paper verified at Springer, Mathematical Programming, vol. 10, pp. 147-175.
• Title, authors, and year all match.
• This paper introduces McCormick envelopes for convex relaxation of bilinear terms. The binary product linearization constraints (y_ij <= x_i, y_ij <= x_j, y_ij >= x_i + x_j - 1) are a specialization of McCormick envelopes to binary variables. This is a valid (though indirect) reference for the linearization technique.

Assessment: The individual techniques used (McCormick linearization, parity encoding via integer slack) are standard and correct in the operations research and integer programming literature. However, neither cited paper directly describes the combined MQ-to-ILP reduction as a complete construction. A textbook reference on integer programming reformulations (e.g., Wolsey's "Integer Programming") would strengthen the citations. Warn — not wrong, but the references don't directly support the full reduction as stated.

Well-written

4a — Information Completeness: All required sections are present (Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, Example). The content is substantive throughout.

4b — Algorithm Completeness: The reduction algorithm is detailed and step-by-step. Variable mapping, constraint transformation, and product consistency are all clearly specified. A programmer could implement this from the description.

4c — Symbol and Notation Consistency:

• Symbols are generally well-defined: n (variables), m (equations), P (cross terms) are introduced in the Notation section.
• The overhead table uses num_vars and num_constraints which correctly match ILP's size fields.
• However, the overhead formulas reference n, P, and m which are not getter method names on the (yet-to-be-defined) MultivariateQuadratic source type. The actual overhead expressions will need to use getter names like num_vars, num_equations, num_quadratic_cross_terms (or whatever the model defines). The issue acknowledges this: "P ... in implementation it can map to a source metric such as num_quadratic_cross_terms."

4d — Example Quality: The example is well-constructed with 2 variables and 2 equations. It shows the full reduction step-by-step with concrete ILP constraints, provides a solution with verification, and includes overhead calculation. The example is small enough to verify by hand.

Minor issues:

• The Validation Method section is somewhat vague ("Compare with direct MQ solvers", "Verify on small instances"). It should describe the closed-loop testing pattern used in this codebase (reduce, solve target with BruteForce, extract solution, verify against source).
• The scope statement "Boolean MQ over F_2" should clarify whether this is the only variant or if the source model supports other fields.

Recommendations

• Add a reference to a standard integer programming textbook (e.g., Wolsey 1998 or Nemhauser & Wolsey 1988) that explicitly covers binary product linearization.
• Align overhead formula variable names with the getter methods that will be defined in the MultivariateQuadratic model ([Model] MultivariateQuadratic #129).
• Strengthen the Validation Method section to describe the closed-loop testing pattern (reduce -> brute-force solve target -> extract solution -> verify against source).

[GiggleLiu]

Fix-issue changelog

• Added direct literature support for the MQ-to-ILP linearization by citing Glover and Woolsey (1974), while keeping McCormick (1976) for the bilinear inequalities and Bard et al. (2007) as MQ background.
• Added an explicit solution extraction section stating how to recover an MQ assignment from a feasible ILP solution.
• Rewrote the size overhead table to use source-side getter-style metric names: num_variables, num_equations, and num_distinct_cross_terms.
• Clarified the scope of the rule as the decision problem MultivariateQuadratic over F_2 and linked the dependency on issue [Model] MultivariateQuadratic #129.
• Strengthened the validation method to match the repo's closed-loop testing pattern.
• Expanded the worked example to show both satisfying MQ assignments and their corresponding feasible ILP points.

Applied by /fix-issue.