Partition: definition #
PARTITION (Karp 1972): can a family of numbers be split
into two parts of equal sum? It lives on FirstOrder.Language.binWeights
unchanged (DescriptiveComplexity.Problems.Knapsack.Defs), the vocabulary of
the binary encoding – items, bit positions, the bits of each weight, and a
linear order – with the target symbol simply unused: what a partition must
match is not a given number but the weight of the items it leaves out.
That absence is what makes Partition a genuinely different problem from
Knapsack rather than a special case: the number to reach, half the total, is
not part of the instance, so an interpretation cannot compute it. Hardness
therefore does not come from Knapsack by the classical two-extra-items padding
(those two weights are arithmetic in the total, hence not first-order
definable); it comes from NAE-SAT, whose not-all-equal condition is exactly
the two-sided constraint a balanced split imposes
(DescriptiveComplexity.naeSat_ordered_fo_reduction_partition).
A binary-weighted instance is a yes-instance of Partition when its order is a linear order and some set of items weighs exactly as much as the items it leaves out.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
Being a yes-instance of Partition is isomorphism-invariant.
Dependency graph
PARTITION, as a problem on binary-weighted instances: can the items be split into two parts of equal weight? The weights are written in binary, and the target symbol of the vocabulary is ignored – the number to reach is half the total, which the instance does not carry.
Equations
- DescriptiveComplexity.Partition = { Holds := fun (A : Type) (inst : FirstOrder.Language.binWeights.Structure A) => DescriptiveComplexity.HasEqualSplit A, iso_invariant := ⋯ }