Binäre Addition

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

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

• Anfang: HALFADD(x₀, y₀;z₀, c₀)
• Schritt: $\forall$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 $\leftrightarrow$ xor(x, y)) $\wedge$ (c $\leftrightarrow$ x $\wedge$ y)
• FULLADD(x, y, c;z, c')$\iff$... (zweimal HALFADD)

dafür CNF ohne Hilfsvariablen!