SAT-Kodierung: Anzahl-Constraints

count_≥k(p₁,…, p_n) = mathend000# wenigstens k mathend000# der n mathend000# 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 mathend000# viele.

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

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

2014-03-31

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