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). 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>*)
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.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
