| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/CVP_Hardness/ (Linux Kernel Version 6.17.9©) Datei vom 31.4.2026 mit Größe 937 B |
|
Impressum Partition.thy Sprache: 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
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet am 2026-11-03) ¤*Bot Zugriff |
|
||||||||||||||||||||||||
2026-11-01