Theory Partition

theory Partition

imports 
  Main
  Reduction
begin

section ‹Partition Problem›
text ‹The Partition Problem is a widely known NP-hard problem.
TODO: 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 ‹Reduction partition problem to SAT(?).›*)


end