132 Complexity — Subset Sum To Partition
132.1 Overview
This file states the Subset Sum and Partition decision problems over a finite type \(U\) with weights in \(\mathbb {N}\), and formalises the classical many-one reduction from Subset Sum to Partition obtained by adjoining two dummy items of weights \(2W - T\) and \(W + T\), where \(W = \sum _{a} w(a)\) is the total weight. Completeness, soundness, and the resulting equivalence are proved under the hypothesis \(T \le W\), which is needed because subtraction on \(\mathbb {N}\) truncates at \(0\).
132.2 Declarations
Given a weight function \(w : U \to \mathbb {N}\) on a finite type \(U\) and a target \(T \in \mathbb {N}\), the predicate asserts that some subset \(S \subseteq U\) has total weight exactly \(T\), i.e. \(\exists S,\ \sum _{a \in S} w(a) = T\).
Given a weight function \(v : U \to \mathbb {N}\) on a finite type \(U\), the predicate asserts that some subset \(S \subseteq U\) has the same total weight as its complement, i.e. \(\exists S,\ \sum _{b \in S} v(b) = \sum _{b \in S^{c}} v(b)\).
The weight function on the augmented universe \(U \oplus \mathrm{Bool}\) built from a Subset Sum instance \((w, T)\). Writing \(W = \sum _{a} w(a)\), it sends the original item \(\mathrm{inl}\, a\) to \(w(a)\), the first dummy item \(\mathrm{inr}\, \mathsf{true}\) to \(2W - T\), and the second dummy item \(\mathrm{inr}\, \mathsf{false}\) to \(W + T\).
Let \(w : U \to \mathbb {N}\) and \(T \in \mathbb {N}\) satisfy \(T \le \sum _{a} w(a)\). If the Subset Sum instance \((w, T)\) has a solution, then the Partition instance with weight function \(\texttt{SubsetSumToPartition.partitionWeight}\ w\ T\) on \(U \oplus \mathrm{Bool}\) has a solution.
Let \(w : U \to \mathbb {N}\) and \(T \in \mathbb {N}\) satisfy \(T \le \sum _{a} w(a)\). If the Partition instance with weight function \(\texttt{SubsetSumToPartition.partitionWeight}\ w\ T\) on \(U \oplus \mathrm{Bool}\) has a solution, then the original Subset Sum instance \((w, T)\) has a solution.
For \(w : U \to \mathbb {N}\) and \(T \in \mathbb {N}\) with \(T \le \sum _{a} w(a)\), the Subset Sum instance \((w, T)\) is solvable if and only if the Partition instance with weight function \(\texttt{SubsetSumToPartition.partitionWeight}\ w\ T\) on \(U \oplus \mathrm{Bool}\) is solvable.