Unärkodierung

• als monotone Bitfolge

  3 = [1, 1, 1, 0, 0, 0, 0, 0]

  x = [x₀,…] mit x₀≥x₁≥….

• Übung: Min, Max, Größer.
• unäre Addition durch Sortiernetze (!)

  (= Idee der minisat-Autoren Een/Sörenssen)

• aktuelle Anwendung: Codish et al.: Exotic Semiring Constraints, http://smt2012.loria.fr/