SAT-Kodierung: Anzahl-Constraints

count_k(p₁,..., p_n) = wenigstens k der n Variablen sind wahr.

Fallunterscheidung nach erster Variablen:

count_k+1(p₁, p₂,..., p_n)

= p₁ $\displaystyle \wedge$ count_k(p₂,..., p_n) $\displaystyle \vee$ count_k+1(p₂,..., p_n).
Induktionsanfänge?
Implementierung mit Hilfsvariablen für jeden Teilausdruck (entspricht Tseitin-Transformation), insgesamt k^.n viele.

(entspr. count_=k, count_k)

Anwendung: größte unabh. Menge von Springern?

2009-06-22

	count_k+1(p₁, p₂,..., p_n)
=	p₁ $\displaystyle \wedge$ count_k(p₂,..., p_n) $\displaystyle \vee$ count_k+1(p₂,..., p_n).