Partition

Umbrella file for DescriptiveComplexity.Partition, Karp's PARTITION – can a family of numbers, written in binary, be split into two parts of equal sum?

It collects the definition, its isomorphism-invariance, the membership half (DescriptiveComplexity.partition_mem_NP) – the certificate guesses the split and two ripple-carry walks, one along the chosen items, one along the others, on the wide positions of DescriptiveComplexity.Numbers.Wide, and requires them to agree at the last item, which says exactly that the two sides weigh the same – and the hardness half (DescriptiveComplexity.naeSat_ordered_fo_reduction_partition), a reduction from NAE-SAT by digit blocks: one per variable, forcing an assignment, and one per clause, forcing between one and w − 1 true literals out of w.

Karp's own reduction pads a Knapsack instance with the weights 2Σ − T and Σ + T; both are arithmetic in the total, hence not first-order definable, so hardness has to start from NAE-SAT instead.

theorem DescriptiveComplexity.partition_mem_NP : NP.Mem Partition

Partition is in NP: it is Σ₁-definable, the certificate carrying the split and the two ripple-carry walks that weigh its two sides.

theorem DescriptiveComplexity.partition_NP_hard : NP.Hard Partition

Partition is NP-hard: NAE-SAT, which is NP-hard, FO-reduces to it over any linear order on the input.

theorem DescriptiveComplexity.partition_NP_complete : NP.Complete Partition

Partition is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem. Its weights are written in binary: under the unary representation the problem is solvable in polynomial time.