XOR-SAT in polynomial time

The input is an ordinary list of parity equations on natural-number variable labels, with arbitrary repetitions and Boolean right-hand sides. Labels use the existing binary encNat, equations use the existing pair encoding, and systems use the existing framed-list encoding. No bound on the numerical value of a variable label is imposed.

The compiler lists the occurring labels without duplicates and computes each coefficient as the parity of its occurrences. This gives a dense system of polynomial size, decided by the native Gaussian-elimination algorithm in XORSAT.Dense. The semantics count repeated occurrences modulo two. Both constant equations and the empty system are supported.

This implements the normalization and elimination argument after [Che06], Theorem 4.3, printed p. 16 (arXiv version 1). The separate affine normal-form theorem does not assert an efficient transformation of a variable truth table into equations: for fixed relation templates, the chosen equations are fixed independently of the input.

Main definitions

• Cslib.Complexity.XORSAT.encoding: lists of equations with binary variable labels.
• Cslib.Complexity.XORSAT.compile: compress labels and cancel repeated occurrences.
• Cslib.Complexity.XORSAT.solve: compile, then perform Gaussian elimination.
• Cslib.Complexity.XORSAT: the satisfiable systems.

Main results

• Cslib.Complexity.XORSAT.solve_eq_true_iff: correctness for ordinary parity systems.
• Cslib.Complexity.XORSAT.computableInPolyTime_solve: a native multi-tape polynomial-time certificate.
• Cslib.Complexity.XORSAT.mem_P: ordinary XOR-SAT is in P.

@[reducible, inline]

abbrev Cslib.Complexity.XORSAT.System : Type

A conjunction of parity equations on arbitrarily large natural-number variable labels.

def Cslib.Complexity.XORSAT.equationEncoding : Logic.PL.AffineEquation ℕ ↪ List Bool

A row is encoded by a framed list of binary labels and a Boolean right-hand side.

def Cslib.Complexity.XORSAT.encoding : System ↪ List Bool

Ordinary framed-list encoding of sparse equations with binary labels.

def Cslib.Complexity.XORSAT.labels (F : System) : List ℕ

The occurring variable labels, each retained once, in order of first occurrence.

def Cslib.Complexity.XORSAT.coefficient (vs : List ℕ) (v : ℕ) : Bool

The coefficient of a variable is the parity of its occurrences.

def Cslib.Complexity.XORSAT.compile (F : System) : Dense.Input

Compress occurring labels, keeping one Boolean coefficient for each label.

def Cslib.Complexity.XORSAT.solve (F : System) : Bool

Native dense Gaussian elimination after compression of binary variable labels.

def Cslib.Complexity.XORSAT.Satisfiable (F : System) : Prop

Ordinary satisfiability, with no restriction on the assignment away from occurring labels.

theorem Cslib.Complexity.XORSAT.mem_labels {F : System} {v : ℕ} : v ∈ labels F ↔ ∃ e ∈ F, v ∈ e.1

The compressed label list contains precisely the occurring labels.

theorem Cslib.Complexity.XORSAT.nodup_labels (F : System) : (labels F).Nodup

There is one compressed coordinate per distinct occurring variable.

theorem Cslib.Complexity.XORSAT.length_labels_le (F : System) : (labels F).length ≤ (List.flatMap Prod.fst F).length

Compression allocates at most one column per variable occurrence in the input.

theorem Cslib.Complexity.XORSAT.width_compile (F : System) : Dense.Width (compile F).width (compile F).rows

Every compiled row has exactly the declared width.

theorem Cslib.Complexity.XORSAT.dot_compile_row (F : System) (e : Logic.PL.AffineEquation ℕ) (he : e ∈ F) (a : ℕ → Bool) : Dense.dot (List.map (coefficient e.1) (labels F)) (List.map a (labels F)) = (List.map a e.1).sum

Compiled rows evaluate exactly as their sparse input equations, including repetitions.

theorem Cslib.Complexity.XORSAT.holds_compile (F : System) (a : ℕ → Bool) : Dense.Holds (compile F).rows (List.map a (labels F)) ↔ Logic.PL.AffineSystem.Holds F a

The compiler preserves the satisfaction relation on every assignment.

theorem Cslib.Complexity.XORSAT.satisfiable_compile_iff (F : System) : Dense.Satisfiable (compile F).width (compile F).rows ↔ Satisfiable F

Sparse satisfiability is equivalent to satisfiability of the compressed dense system.

theorem Cslib.Complexity.XORSAT.solve_eq_true_iff (F : System) : solve F = true ↔ Satisfiable F

The executable solver decides ordinary sparse systems with binary variable labels.

theorem Cslib.Complexity.XORSAT.computableInPolyTime_compile : Turing.MultiTapeTM.ComputableInPolyTime compile encoding Dense.encInput

Label compression is itself a native polynomial-time computation. Binary labels are only compared, never expanded into a table indexed by their numerical value.

theorem Cslib.Complexity.XORSAT.computableInPolyTime_solve : Turing.MultiTapeTM.ComputableInPolyTime solve encoding Turing.MultiTapeTM.encBool

Ordinary XOR-SAT is decided in polynomial time by native multi-tape machines.

def Cslib.Complexity.XORSAT : Set XORSAT.System

Ordinary XOR-SAT: the satisfiable systems of parity equations.

theorem Cslib.Complexity.mem_XORSAT {F : XORSAT.System} : F ∈ XORSAT ↔ XORSAT.Satisfiable F

theorem Cslib.Complexity.XORSAT.mem_P : XORSAT ∈ P encoding

Ordinary systems of affine parity equations, with sparse binary variable labels, are in P.