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). 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.0 Sekunden
(vorverarbeitet am 2026-11-03)
¤
*© Formatika GbR, Deutschland
