SAT-Kodierung: Anzahl-Constraints

count_≥k(p₁,…, p_n) = wenigstens k der n Variablen sind wahr.

Fallunterscheidung nach der ersten Variable:

count_≥k+1(p₁, p₂,…, p_n)

= p₁∧count_≥k(p₂,…, p_n)∨count_≥k+1(p₂,…, p_n).
Induktionsanfänge?
Implementierung mit Hilfsvariablen für jeden Teilausdruck (entspricht Tseitin-Transformation), insgesamt k⋅n viele.

(Übung: definiere count_=k, count_≤k)

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

2014-07-06

	count_≥k+1(p₁, p₂,…, p_n)
=	p₁∧count_≥k(p₂,…, p_n)∨count_≥k+1(p₂,…, p_n).