Binäre Addition

[x₀,…] + [y₀,…] = [z₀,…] mathend000#

Hilfsvariablen: [c₀,…] mathend000# = mathend000# Überträge

• Anfang: HALFADD(x₀, y₀;z₀, c₀) mathend000#
• Schritt: ∀i : FULLADD(x_i, y_i, c_i;z_i, c_i+1) mathend000#
• Ende: c_w = 0 mathend000# (kein Überlauf)

Realisierung:

• HALFADD(x, y;z, c)$\iff$(z↔xor(x, y))∧(c↔x∧y) mathend000#
• FULLADD(x, y, c;z, c')$\iff$... mathend000# (zweimal HALFADD mathend000#)

dafür CNF ohne Hilfsvariablen!