Binäre Addition

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

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

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

Realisierung:

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

dafür CNF ohne Hilfsvariablen!