| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/CVP_Hardness/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 937 B |
|
Quelle Partition.thySprache: Isabelle |
|||||||||||||||
|
theory Partition imports Main Reduction begin section ‹Partition Problem› text ‹The Partition Problem is a widely known NP-hard problem. : Reduction proof to SAT› definition is_partition :: "int list ==> nat set ==> bool" where "is_partition a I = (I ⊆ {0..<length a} ∧ (∑i∈I. a ! i) = (∑i∈({0..<length a}-I). definition partition_problem :: "(int list) set " where "partition_problem = {a. ∃I. I ⊆ {0..<length a} ∧ (∑i∈I. a ! i) = (∑i∈({0..<length a}-I). a ! i)}" definition partition_problem_nonzero :: "(int list) set " where "partition_problem_nonzero = {a. ∃I. I ⊆ {0..<length a} ∧ length a > 0 ∧ (∑i∈I. a ! i) = (∑i∈({0..<length a}-I). a ! i)}" (* text \<open>Reduction partition problem to SAT(?).\<close>*) end
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09