Unärkodierung

• als monotone Bitfolge

  3 = [1, 1, 1, 0, 0, 0, 0, 0] mathend000#

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

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

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

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